The storage_map strategy

The storage_map strategy can be applied to fields of type Map<K, Tok> for any types K and Tok.

fields {
    #[sharding(storage_map)]
    pub field: Map<K, 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_map, the VerusSync gains the ability to “store” tokens of the given type Tok. Multiple such tokens can be stored, and they are indexed by keys of type K.

For example, if the field has value [1 => tok1, 4 => tok2], then that means tok1 and tok2 are stored.

Manipulation of the field

Quick Reference

In the following table, k: K, tok: Tok, and map_toks: Map<K, Tok>.

Initializing the field

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

init field = map_toks;

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

Performing a deposit

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

deposit field += [ k => tok ];

This sets the map value at key k to tok. The resulting token operation then takes a token equal to tok as input.

The deposit instruction has an inherent safety condition that key is not already present 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 += [ k => tok ];
by {
    // proof goes here
};

Performing a withdraw

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

withdraw field -= [ k => 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 contains the key-value pair k, 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 -= [ k => 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 -= [ k => let $pat ];

In this case, the inherent safety condition is that the field map contains the key k and that the corresponding 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[k];
withdraw field -= [ k => 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 >= [ k => 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 contains the key-value pair k, 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 >= [ k => tok ];
by {
    // proof goes here
};

Operations that manipulate collections of 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 map_toks == [ k => tok ], and they are all no-ops when map_toks == map![].

To deposit an Map<K, Tok>:

deposit field += (map_toks);

To withdraw an Map<K, Tok>:

remove field -= (map_toks);

To obtain an &Map<K, Tok>:

guard field >= (map_toks);

Example

TODO