The persistent_map strategy

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

fields {
    #[sharding(persistent_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 KeyValueToken<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 KeyValueToken<V> trait). The value of the field on the global state is the map given by the collection of key-value pairs. Since the tokens are Copy, there can be any number of such tokens for any given key.

Of course, all such tokens for the same key will agree on the value as well. Once a key is set to a given value, this cannot be changed or removed.

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, write, inside any transition! operation:

add field (union)= [k => v];

This operation has an inherent safety condition that, if k is in the domain of the pre-state value of the map, then it has the same value v. 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 (union)= [k => v]
by {
    // proof goes here
};

Checking the value of the token

To check the key and value of the token, 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.

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 (union)= (m);

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

have field >= (m);

Example

TODO