The storage_option strategy

The storage_option strategy can be applied to fields of type Option<Tok> for any type Tok.

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

Tokens. Usually Tok is itself some “token” type intended for tracked contexts—e.g., the token created by a different VerusSync system (or even the same VerusSync system, as recursive types are permitted), a PointsTo, or a datatype/tuple combining multiple of these.

VerusSync does not create any additional tokens for the field.

Relationship between global field value and the token. When a field is declared storage_option, the VerusSync gains the ability to “store” tokens of the given type Tok. A field value of None means nothing is stored; a field value of Some(tok) means the token tok is stored.

Manipulation of the field

Quick Reference

In the following table, tok: Tok, and opt_token: Option<Tok>.

Initializing the field

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

init field = opt_tok;

The instance-init function will take as input a token of type Option<Tok>, equal to the value of opt_tok.

That is, if opt_tok is None, then the initial state has nothing “stored” and passing None to the constructor is trivial; if opt_tok is Some(tok), then the initial state has tok “stored” and it must be supplied via the input argument for the constructor.

Performing a deposit

To deposit a token tok: Tok, use the deposit statement in any transition! operation:

deposit field += Some(tok);

This sets the field value to Some(tok). The resulting token operation then takes a token equal to tok as input.

The deposit instruction has an inherent safety condition that field is None in the pre-state. (Note: this is not strictly necessary, and the restriction may be removed later.)

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

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

Performing a withdraw

To withdraw a token tok: Tok, use the withdraw statement in any transition! operation:

withdraw field -= Some(tok);

This sets the field value to None. The resulting token operation then returns a token equal to tok in its output.

The withdraw instruction has an inherent safety condition that field is Some(tok) in the pre-state.

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

withdraw field -= Some(tok)
by {
    // proof goes here
};

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

withdraw field -= Some(let $pat);

In this case, the inherent safety condition is that the field value is Some and that the inner value matches $pat. In this case, note that the value matched on $pat is not deterministic in the input arguments of the token operation. Therefore, VerusSync considers any variables bound in $pat to implicitly be birds_eye binders. Specifically, the pattern-matching variant is equivalent to:

birds_eye let stored_value = pre.field.unwrap();
withdraw field -= Some(stored_value);
birds_eye let $pat = stored_value;

Performing a guard (obtaining a shared reference to the stored object)

To guard a token tok: Tok, use the guard statement in any property! operation:

guard field >= Some(tok);

The resulting token operation then returns a shared reference to the token equal to tok in its output. The shared reference has a lifetime bounded by the lifetimes of the input references.

The guard instruction has an inherent safety condition that field is Some(tok) in the pre-state.

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

guard field >= Some(tok)
by {
    // proof goes here
};

Operations that manipulate optional tokens

You can also write versions of the above operations that operate on an optional token opt_tok: Option<Tok>. The operations below are equivalent to the above versions whenever opt_tok == Some(tok), and they are all no-ops when opt_tok == None.

To deposit opt_tok: Option<Tok>:

deposit field += (opt_tok);

To withdraw opt_tok: Option<Tok>:

remove field -= (opt_tok);

To obtain opt_tok: &Option<Tok>:

guard field >= (opt_v);

Example

TODO