Counter
The "counter" is one of the simplest smart contracts that can be written in Pint. It showcases how a contract can have multiple predicates and how it can declare and use storage. This particular implementation of the "counter" contract is different from the one we encountered in the Quickstart Guide
storage {
counter: int,
}
predicate Initialize {
var value: int;
state counter: int = mut storage::counter;
constraint counter' == value;
}
predicate Increment {
var amount: int;
state counter: int = mut storage::counter;
constraint counter' == counter + amount;
}
The contract starts by declaring a storage
block which contains a single storage variable called
counter
of type int
(i.e. integer). The contract later declares two separate predicates, each
declaring three statements. Let's walk through the first predicate named Initialize
:
- The first statement declares a decision variable. Decision variables are quite different from
"regular" variables which you might be familiar with from imperative languages. Decision
variables are variables that the solver is required to find values for. You can think of them
as "arguments" that the solver has to set such that every
constraint
in the predicate evaluates totrue
. InInitialize
, we are declaring a single decision variable calledvalue
of typeint
. This is the value that we want our counter to get initialized to. - The second statement declares a
state
variable and initializes it tomut storage::counter
. State variables are special variables that always need to be initialized to a storage access expression. The statementstate counter: int = mut storage::counter
creates a state variable calledcounter
and initializes it to the current value ofcounter
declared in thestorage
block. Themut
keyword simply indicates that the solver is allowed to propose a new value forcounter
. Ifmut
is not present, then the storage variablecounter
cannot be modified by anyone attempting to solve predicateInitialize
. - The third statement contains the core logic of this predicate. It declares that the "next
value" of
state counter
must be equal tovalue
. Note the'
notation here which can be only applied to astate
variable, and means "the next value of the state variable after a valid state transition".
The second predicate, called Increment
, has a similar structure to Initialize
. However, instead
of initializing counter
, It increments it by amount
. Note that both counter
(the current
value) and counter'
(the next value) are both used in the constraint to enforce that the next
value is dependent on the current value, which was not the case in Initialize
.
Solution
We won't go too deep into the solving process here but it's worth mentioning what a solution to this predicate might look like. Broadly speaking, a solution contains two things:
- An assignment of all the decision variables in the predicate.
- A list of all the state mutations proposed.
For example, if a user wants the value of the counter to be 42
they (or a solver acting on their
behalf) can propose a solution to Initialize
that looks like this:
# decision variables:
value: 42
# state mutations:
0: 42
This solution proposes a value of 42
for the decision variable value
and a new value of 42
for
the storage key 0
where counter
is stored (we will go over the storage data layout later!). Note
that the storage key 0
where counter
is stored can be modified by the solution because of the
mut
keyword added before storage::counter
.
A solution must also indicate which predicate is being solved using its address but we're omitting that here for simplicity.
Alternatively, a solution to Increment
can be proposed to satisfy the user requirement counter = 42
. For example, if the current value of counter
happens to be 35
, then the following solution
to Increment
can be proposed:
# decision variables:
amount: 7
# state mutations:
0: 42
It should be easy to verify that this solution satisfies the constraint counter' == counter + amount;
from Increment
.