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>,
}

This creates a token type, State::field, which a field value: V. 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.

Quick Reference

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<State::field>, 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 State::field 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 State::field 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 &State::field (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. These operations are equivalent to above versions whenever opt_v = Some(v), and they are all no-ops when opt_v = None.

To create an Option<State::field>:

add field += (opt_v);

To consume an Option<State::field>:

remove field -= (opt_v);

To check the value of an Option<State::field>:

have field >= (opt_v);

The value of opt_v is related to the value of Option<State::field> 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() {
    #[verifier::proof]
    let (Tracked(instance), Tracked(mut token_exists), Tracked(token_opt)) =
        State::Instance::initialize(5);
    #[verifier::proof]
    let 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`
    #[verifier::proof]
    let 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
}