The persistent_bool strategy

The persistent_bool strategy can be applied to fields of type bool.

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

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 SimpleToken<V> trait.

Relationship between global field value and the token. When field is false, this corresponds to no token existing, while when field is true, this corresponds to at least one token existing. The token doesn’t contain any additional data. Having multiple such tokens at the same time is an impossible state.

Since the tokens are Copy, there can be any number of such tokens for any given key.

Manipulation of the field

Quick Reference

In the following table, b: bool.

Initializing the field

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

init field = b;

The instance-init function will return a token of type Option<tok>, related as follows:

Adding a token

To write an operation that creates a token, write, inside any transition! operation:

add field (union)= true;

The resulting token exchange function will return a token of type tok and with value v.

In other words, you can create a token at any time, regardless of the current value of the field. The only requirement is that (as always) the invariants of the system must be preserved.

Observing that the token exists

To observe that the token exists, write, inside any transition!, readonly! or property! operation:

have field >= true;

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

Operations that manipulate optional tokens

You can also write versions of the above operations that operate on optional tokens. The operations below are equivalent to the above versions whenever opt_v == Some(v), and they are all no-ops when opt_v == None.

To create an Option<tok>:

add field (union)= (b);

To observe the token &Option<tok>:

have field >= (b);

The value of b is related to the value of Option<tok> as they are for initialization.

Example

TODO