The count strategy

The count strategy can be applied to fields of type nat.

fields {
    #[sharding(count)]
    pub field: nat,
}

Tokens. VerusSync creates a fresh token type, tok, named State::field where State is the name of the VerusSync system and field is the name of the field.

The token type tok implements the CountToken trait. Each token has a count() value, and these tokens “fungible” in the sense that they can be combined and split, numbers combining additively.

Relationship between global field value and the token. The global value of the field is the sum of the counts of all the tokens.

Manipulation of the field

Quick Reference

In the following table, n: nat.

Initializing the field

Initializing the field is done with the usual init statement (as it for all strategies).

init field = n;

The instance-init function will return a token of type tok with count() equal to n.

Adding a token (increasing the count)

To write an operation that creates a token, equivalently, adding to the total count, write,

add field += (n);

The resulting token exchange function will return a token of type tok with count() equal to n.

Removing a token

To write an operation that removes a token, equivalently, decreasing the total count, updating the field’s value from true to false, write, inside any transition! operation:

remove field -= (n);

The resulting exchange function will consume a tok token with count() equal to n as a parameter.

Checking the value of the token

To check the value of the token without removing it, write, inside any transition!, readonly! or property! operation:

have field >= (n);

The resulting exchange function will accept an immutable reference &tok (that is, it takes the token as input but does not consume it).

Example

TODO