Statically-Sized Storage Types
All storage variables in a Pint contract must be declared inside a storage
block, and there can
only be a single storage
block in a Pint contract. The storage
block is optional and can be
skipped if the contract does not need to manage any state, but such contracts are generally not very
useful.
Here's an example of a storage
block:
storage {
x: int,
a: b256,
t: { int, bool },
y: bool,
w: int,
arr: { int, int }[3],
v: { int, { bool, b256 } },
}
A storage
starts with the keyword storage
and followed by a comma-separated list of variable
declarations inside curly brackets. Each variable declaration is an identifier annotated with a
type. In this chapter, we're only looking at storage variables that have statically-sized types,
i.e., types that have known sizes and layouts at compile time. This pretty much covers every type we
discussed so far! In the next chapter, we will introduce new storage-only types that are dynamically
sized.
Back to the example above, the declared storage
block is fairly simple. It contains three
variables that have primitive types and one variable that has a compound type (a tuple). Unlike
decision variables, storage variables do not accept an initializer and must have a type
annotation.
Accessing Storage Variables
Storage variables are not useful unless we can read them and/or propose modifications to them. Recall that Pint is a declarative constraint-based language, and therefore, does not allow "writing" directly to a storage variable. Writing directly to storage is a concept you might be familiar with from other smart contract languages like Solidity, so you might be asking yourself the following question: "if I can't write directly to storage variables, how will their values ever change? How will the state of the blockchain ever change?"
The answer to these questions lies at the core of what makes Pint and declarative blockchains
actually declarative. Pint has no concept of "updating" state (or even decision variables for
that matter). Pint simply expresses a desired outcome using constraint
statements and relies on
solutions to actually propose state changes.
In order to express a desired outcome for a given storage variable, two things are needed:
- A way to read the current value of the variable.
- A way to express the future value of the variable.
Reading a Storage Variable
Reading a storage variable should not be an unfamiliar concept to you if you've worked with other
smart contract languages before like Solidity. The syntax for reading a
storage variable in Pint requires the storage
keyword again:
state x = storage::x;
state a = storage::a;
state t = storage::t;
state t_1 = storage::t.1;
state arr_2_1 = storage::arr[2].1;
A few things to note here:
- Storage read expressions always start with
storage::
followed by the name of the variable we're trying to read. Thestorage::
syntax means we're switching namespaces to that of thestorage
block. - Each storage read expression is used to initialize a
state
variable. In fact, storage read expressions can only ever be used to initializestate
variables. Using a storage read expression in other contexts, such as inconstraint storage::x == 5
, is illegal. - Fields or elements of a compound type in storage can be accessed individually, as in
storage::t.1
andstorage::arr[2].1
.
We haven't really explained what a state
variable is so this is probably a good time to do so.
State Variables
A state variable is a special type of variables that can only hold values read from storage. A
state
variable must always have an initializer and that initializer can only be a storage read
expression. Type annotations for state
declarations are optional:
state not_annotated = storage::x;
state annotated: b256 = storage::a;
Once a state
variable is declared, it can be used anywhere in its scope as if it were a decision
variable:
state t_0 = storage::t.0;
state y = storage::y;
constraint y && t_0 >= 42;
This is an example where two state variables are declared and later constrained as if they were
decision variables. One important distinction to note here is that state
variables are not
actually unknown. By definition, decision variables are unknown at compile time and at
solve-time and they only become known after the solving process is finished (if a solution is
found). In contrast, state
variables, while unknown at compile time, are actually known at
solve-time: right before the solving process starts, every storage read expression is evaluated by
directly inspecting the blockchain. The result is then assigned to the corresponding state
variable which becomes known in preparation for solving.
Next State
Recall that expressing a desired outcome for a given storage variable also requires a way to express the future value of the variable.
In most imperative languages, statements like x = x + 1
are commonly used to mean "update the
value of x
to be equal to the current value of x
plus 1
". Because Pint is a constraint-based
declarative language where the order of statements does not matter and there is no sequential
execution, statements like x = x + 1
cannot be written and are not logical. Instead, Pint offers a
special syntax, reserved for state
variables, that means "the future value of". Here's an example:
state bal = mut storage::x;
constraint bal' >= bal + 42;
Here, bal'
, unlike bal
, is actually unknown at solve-time. That is, bal'
must be solved for as
if it were a decision variable and every solution must include a proposed value for bal'
. If, for
example, the value of bal
was read to be 100
at solve-time, a solver might propose that the next
value of bal
should be 150
(i.e. bal' = 150
) which would be a valid solution because 150 >= 100 + 42
(assuming all other constraints in the predicate are also satisfied).
"Mutable" Storage Accesses
In the previous section, you may have noticed that we added the mut
keyword before storage::x
in
the state
declaration. In Pint, storage locations are non-mutable by default. That is, solvers
cannot propose new values for a storage location unless they are solving a predicate that allows
the storage location to be mutable. This is accomplished using the mut
keyword added before a
storage access. In the example of the previous section, because mut
was added before storage::x
,
a solver can now propose a state mutation that updates the value of x
.
When the mut
keyword as added before a storage access into a compound type, mutability applies
only to the portion of the compound type that is being accessed. For example, in the example
below:
state inner: { bool, b256 } = mut storage::v.1;
v.1
is a storage access into nested tuple v
defined in the storage
block declared earlier.
Here, both v.1.0
( a bool
) and v.1.1
(a b256
) are both allowed to be mutated, but v.0
is
not allowed to be.
"Empty" State
You may be wondering what happens if a storage variable was never previously updated but was read
anyways. In this case, there is no value stored at that storage variable and nothing can be read.
To help you reason about this, Pint provides the literal nil
to represent the absence of a
value. For example,
state w = mut storage::w;
var value: int = (w == nil ? 0 : w);
In the example above, we first check if w
is nil
before attempting to read it. If it is nil
(i.e. currently has no value), then we constrain value
to 0
. Otherwise, we constrain it to the
non-empty value of w
. Without checking if w
is nil
first, and if we're not sure whether w
has a value or not, then it is possible that the state read operation will panic.
It is also possible to update a state
variable to nil
using the "next state" operator:
if w != nil {
constraint w' == nil;
}
Here, if w
currently has a value, then we constrain the next value of w
to be nil
.
This concludes our overview on storage which only focused on statically-sized storage types. In the next chapter, we will cover dynamically-sized storage types which offer a lot more flexibility.