Write the Predicate

Start by adding a new predicate called Increment to the contract/src/contract.pnt file:

predicate Increment() {

}

Storage

The first thing we want to do within this predicate is to read the counter storage value:

predicate Increment() {
    let counter: int = mut storage::counter;
}

Constraint

Let's add our first constraint:

predicate Increment() {
    let counter: int = mut storage::counter;

    constraint counter' == counter + 1;
}

A constraint is a boolean expression which must be true for the predicate to be satisfied.
This constraint says that the post-state of the counter must be equal to the pre-state plus one.

Note: The post-state value of the counter storage variable is denoted by counter'. The trailing apostrophe ' is the syntax for accessing the post-state value of a storage variable.

But there is a problem with this constraint.
What if the pre-state of the counter is not yet set to anything?

We can use a nil check to handle this case:

predicate Increment() {
    let counter: int = mut storage::counter;

    constraint counter == nil && counter' == 1;
}

This says that if the pre-state of the counter is nil then the post-state must be 1.

Now let's put it all together:

predicate Increment() {
    let counter: int = mut storage::counter;

    constraint (counter == nil && counter' == 1) || counter' == counter + 1;
}

This constraint is satisfied if either the counter pre-state is nil and the post-state is 1, or the counter pre-state is n and the post-state is n + 1.

Your complete contract/src/contract.pnt file should look like this:

storage {
    counter: int,
}

predicate Increment() {
    let counter: int = mut storage::counter;

    constraint (counter == nil && counter' == 1) || counter' == counter + 1;
}

Congratulations on writing your first pint predicate!