The option strategy

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

fields {
    #[sharding(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 UniqueValueToken<V> trait.

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. Having multiple such tokens at the same time is an impossible state.

Manipulation of the field

Quick Reference

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

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:

Adding a token

To write an operation that creates a token with value v, equivalently, updating the field’s value from None to Some(v), write, inside any transition! operation:

add field += Some(v);

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

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

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

Removing a token

To write an operation that removes a token with value v, equivalently, updating the field’s value from Some(v) to None, write, inside any transition! operation:

remove field -= Some(v);

The resulting exchange function will consume a tok token with value v as a parameter.

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

remove 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.

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 >= 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.

Updating a token

To update the value of an option token, first remove it, then add it, in sequence.

remove field -= Some(let _);
add field += Some(new_v);

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

To consume an Option<tok>:

remove field -= (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

tokenized_state_machine!{ State {
    fields {
        #[sharding(variable)]
        pub token_exists: bool,

        #[sharding(option)]
        pub field: Option<int>,
    }

    #[invariant]
    pub fn token_exists_correct(&self) -> bool {
        self.token_exists <==> self.field.is_Some()
    }

    init!{
        initialize(v: int) {
            init field = Option::Some(v);
            init token_exists = true;
        }
    }

    transition!{
        add_token(v: int) {
            require !pre.token_exists;
            update token_exists = true;

            add field += Some(v);
        }
    }

    transition!{
        remove_token() {
            remove field -= Some(let _);

            assert pre.token_exists;
            update token_exists = false;
        }
    }

    transition!{
        have_token() {
            have field >= Some(let _);

            assert pre.token_exists;
        }
    }

    #[inductive(initialize)]
    fn initialize_inductive(post: Self, v: int) { }

    #[inductive(add_token)]
    fn add_token_inductive(pre: Self, post: Self, v: int) { }

    #[inductive(remove_token)]
    fn remove_token_inductive(pre: Self, post: Self) { }

    #[inductive(have_token)]
    fn have_token_inductive(pre: Self, post: Self) { }
}}

proof fn option_example() {
    let tracked (Tracked(instance), Tracked(mut token_exists), Tracked(token_opt)) =
        State::Instance::initialize(5);

    let tracked token = token_opt.tracked_unwrap();
    assert(token.value() == 5);

    instance.have_token(&token_exists, &token);
    assert(token_exists.value() == true);

    instance.remove_token(&mut token_exists, token);  // consumes token
    assert(token_exists.value() == false);            // updates token_exists to `false`

    let tracked token = instance.add_token(19, &mut token_exists);
    assert(token_exists.value() == true);  // updates token_exists to `true`
    assert(token.value() == 19);           // new token has value 19
}