The map strategy

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

fields {
    #[sharding(map)]
    pub field: Map<K, 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 UniqueKeyValueToken<V> trait.

For dealing with collections of tokens, VerusSync uses MapToken<K, V, tok>. It also creates a type alias for this type by appending _map to the field name, e.g., State::field_map.

Relationship between global field value and the token. Every token represents a single key-value pair (given by the .key() and .value() functions on the UniqueKeyValueToken<V> trait). The value of the field on the global state is the map given by the collection of key-value pairs.

Manipulation of the field

Quick Reference

In the following table, k: K, v: v, and m: Map<K, V>.

Initializing the field

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

init field = m;

The instance-init function will return a token token of type MapToken<K, V, tok>, where token.map() == m.

Adding a token

To write an operation that creates a token with key-value pair k, v, equivalently, inserting the pair k, v into the map, write, inside any transition! operation:

add field += [k => v];

This operation has an inherent safety condition that k is not in the domain of the pre-state value of the map. The resulting token exchange function will return a token of type tok and with key() equal to k and value() equal to v.

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

add field += [k => v]
by {
    // proof goes here
};

Removing a token

To write an operation that removes a token with key-value pair k, v, equivalently, removing the pair k, v from the map, write, inside any transition! operation:

remove field -= [k => v];

The resulting exchange function will consume a tok token with key() equal to k and value() equal to v.

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

remove field -= [k => let $pat];

This will require the prior value of field[k] to match $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 key and value of the token without removing it, write, inside any transition!, readonly! or property! operation:

have field >= [k => 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 >= [k => let $pat];

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

Updating a token

To update the value of a map token, first remove it, then add it, in sequence.

remove field -= [k => let _];
add field += [k => v];

Operations that manipulate collections of tokens

You can also write versions of the above operations that operate on variable-sized collections of tokens rather than singleton key-value pairs. Such token collections are managed as MapToken<K, V, tok> objects.

The operations below are equivalent to the above versions whenever m == map![k => v], and they are all no-ops when m == map![].

To create a MapToken<K, V, tok> where tok.map() == m:

add field += (m);

To consume a MapToken<K, V, tok> where tok.map() == m:

remove field -= (m);

To check the value of a &MapToken<K, V, tok> where tok.map() == m:

have field >= (m);

Example

TODO