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>
.
Command | Meaning in transition | Exchange Fn Parameter |
---|---|---|
init field = map_toks; |
init field = map_toks; |
Input Map<K, Tok> |
deposit field += [ k => tok ]; |
assert !field.dom().contains(k); update field = field.insert(k, tok); |
Input Tok |
guard field >= [ k => tok ]; |
assert field.dom().contains(k) && field[k] == tok; |
Output &Tok |
withdraw field -= [ k => tok ]; |
assert field.dom().contains(k) && field[k] == tok; update field = field.remove(k); |
Output Tok |
deposit field += map_toks; |
assert field.dom().disjoint(map_toks.dom()); update field = field.union_prefer_right(map_toks);
|
Input Map<K, Tok> |
guard field >= map_toks; |
assert map_toks.submap_of(field); |
Output &Map<K, Tok> |
withdraw field -= map_toks; |
assert map_toks.submap_of(field); update field = field.remove_keys(map_toks.dom()); |
Output 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
use a map map_toks
: Map<K, Tok>
,
instead of an individual key-value pair (typically you’ll need to pass map_toks
in as an argument to your transition).
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 map_toks:
Map<K, Tok>
:
deposit field += (map_toks);
To withdraw map_toks:
Map<K, Tok>
:
remove field -= (map_toks);
To obtain map_toks:
&Map<K, Tok>
:
guard field >= (map_toks);
Example
TODO