The persistent_option strategy

The persistent_option strategy can be applied to fields of type Option<V> for any type V.

fields {
    #[sharding(persistent_option)]
    pub field: Option<V>,
}

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 ValueToken<V> trait. It also implements Copy.

Relationship between global field value and the token. When field is None, this corresponds to no token existing, while when field is Some(v), this corresponds to a token of value v existing. Since the token is Copy, there can be any number of such tokens. Once set to a particular Some(_) value, it can never be set to a different one; i.e., it can only be set None -> Some.

Manipulation of the field

Quick Reference

In the following table, v: V and v_opt: Option<V>.

Command Meaning in transition Exchange Fn Parameter
init field = v_opt; init field = v_opt; Output Option<tok>
have field >= Some(v); require field == Some(v); Input &tok
add field (union)= Some(v); assert field == None || field == Some(v);
update field = Some(v);		 Output tok
have field >= (v_opt); require v_opt == None || field == v_opt; Input &Option<tok>
add field (union)= (v_opt); assert field == None || v_opt == None || field == v_opt; update field = if v_opt == None { field } else { v_opt }; Output Option<tok>

Initializing the field

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

init field = opt_v;

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

value of opt_v: Option<V>    value of optional token Option<tok>
None None
Some(v) Some(tok) where tok.value() == v

Adding a token

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

add field (union)= Some(v);

This operation has an inherent safety condition that the prior value of field is either None or is already Some(v). The resulting token exchange function will return a token of type tok and with value v.

In other words, you can create a token only if the existing value is None (no tokens have been created yet) or already equal to Some(v) (all existing tokens agree with the new token on the value).

If you require manual proof to prove the inherent safety condition, you can add an optional by clause:

add field (union)= Some(v)
by {
    // proof goes here
};

Checking the value of the token

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

have field >= Some(v);

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

Instead of specifying v as an exact expression, you can also pattern-match by using the let keyword.

have field >= Some(let $pat);

This will require the prior value of field to match Some($pat), and this statement binds all the variables in $pat for use later in the transition.

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)= (opt_v);

To check the value of an &Option<tok>:

have field >= (opt_v);

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

Example

TODO