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 {
    state counter: int = storage::counter;
}

When a storage value is read like this there are actually two values read:

• The pre-state value of the storage, denoted by counter.
• The post-state value of the storage, denoted by counter'. (Notice the apostrophe ').

Constraint

Let's add our first constraint:

predicate Increment {
    state counter: int = 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.

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 {
    state counter: int = 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 {
    state counter: int = 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 {
    state counter: int = storage::counter;

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

Congratulations on writing your first pint predicate!