The `multiset` strategy

The multiset strategy can be applied to fields of type Multiset<E> for any types E.

fields {
    #[sharding(multiset)]
    pub field: Multiset<E>,
}

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 UniqueElementToken<V> trait.

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

Relationship between global field value and the token. Every token represents a single element of the multiset (given by the .element() function on the UniqueElementToken<V> trait). The value of the field on the global state is the multiset given by the collection of all such elements.

Manipulation of the field

Quick Reference

In the following table, e: E and m: Multiset<E>.

Command	Meaning in transition	Exchange Fn Parameter

`init field = m;`	`init field = m;`	Output `MultisetToken<K, V, tok>`
`remove field -= { e };`	`require field.contains(e);` `update field = field.remove(e);`	Input `tok`
`have field >= { e };`	`require field.contains(e);`	Input `&tok`
`add field += { e };`	`update field = field.insert(e);`	Output `tok`
`remove field -= (m);`	`require m.subset_of(field);` `update field = field.difference_with(m);`	Input `MultisetToken<K, V, tok>`
`have field >= (m);`	`require m.subset_of(field);`	Input `&MultisetToken<K, V, tok>`
`add field += (m);`	`update field = field.add(m);`	Output `MultisetToken<K, V, tok>`

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 MultisetToken<K, V, tok>, where token.multiset() == m.

Adding a token

To write an operation that creates a token with element e, equivalently, inserting the element e into the multiset, write, inside any transition! operation:

add field += { e };

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

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

add field += { e };
by {
    // proof goes here
};

Removing a token

To write an operation that removes a token with element e, equivalently, removing the element e from the multiset, write, inside any transition! operation:

remove field -= { e };

The resulting exchange function will consume a tok token with element() equal to e.

Checking the value of the token

To check the element of the token without removing it, write, inside any transition!, readonly! or property! operation:

have field >= { e };

The resulting exchange function will accept an immutable reference &tok (that is, it takes the token as input but does not consume it).

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 elements. Such token collections are managed as MultisetToken<K, V, tok> objects.

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

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

add field += (m);

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

remove field -= (m);

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

have field >= (m);

Example

TODO

Verus Transition Systems