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
+[`UniqueSimpleToken`](https://verus-lang.github.io/verus/verusdoc/vstd/tokens/trait.UniqueSimpleToken.html) trait.
+
+**Relationship between global field value and the token.**
+When `field` is `false`, this corresponds to no token existing, while
+when `field` is `true`, this corresponds to a token existing.
+The token doesn't contain any additional data.
+Having multiple such tokens at the same time is an impossible state.
+
+## Manipulation of the field
+
+### Quick Reference
+
+In the following table, `b: bool`.
+
+| Command | +Meaning in transition | +Exchange Fn Parameter | +
|---|---|---|
init field = b; |
+ init field = b; |
+ Output Option<tok> |
+
remove field -= true; |
+ require field == true;update field = false; |
+ Input tok |
+
have field >= true; |
+ require field == true; |
+ Input &tok |
+
add field += true; |
+ assert field == false;update field = true; |
+ Output tok |
+
remove field -= (b); |
+ require (b ==> field);
+update field = field && !b; |
+ Input Option<tok> |
+
have field >= (b); |
+ require (b ==> field); |
+ Input &Option<tok> |
+
add field += (b); |
+ assert !(field && b);
+update field = field || b; |
+ Output Option<tok> |
+
Option<tok>,
+related as follows:
+
+value of b: bool |
+ value of optional token Option<tok> |
+
|---|---|
false |
+ None |
+
true |
+ Some(tok) where tok.value() == v |
+
tok.
+
+### Removing a token
+
+To write an operation that _removes_ a token,
+equivalently,
+updating the field's value from `true` to `false`, write, inside any `transition!`
+operation:
+
+```rust
+remove field -= true;
+```
+
+The resulting exchange function will consume a tok token
+as a parameter.
+
+### Checking the value of the token
+
+To check the value of the token without removing it,
+write, inside any `transition!`, `readonly!` or `property!` operation:
+
+```rust
+have field >= true;
+```
+
+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 optional 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 `b == true`,
+and they are all no-ops when `b == false`.
+
+To create an Option<tok>:
+
+```rust
+add field += (b);
+```
+
+To consume an Option<tok>:
+
+```rust
+remove field -= (b);
+```
+
+To check the value of an &Option<tok>:
+
+```rust
+have field >= (b);
+```
+
+
+The value of `b` is related to the value of
+Option<tok>
+as [they are for initialization](#initializing-the-field).
+
+## Example
+
+TODO
diff --git a/source/docs/state_machines/src/strategy-count.md b/source/docs/state_machines/src/strategy-count.md
new file mode 100644
index 000000000..a60eb0efb
--- /dev/null
+++ b/source/docs/state_machines/src/strategy-count.md
@@ -0,0 +1,118 @@
+# The `count` strategy
+
+The `count` strategy can be applied to fields of type `nat`.
+
+```rust
+fields {
+ #[sharding(count)]
+ pub field: nat,
+}
+```
+
+**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
+[`CountToken`](https://verus-lang.github.io/verus/verusdoc/vstd/tokens/trait.CountToken.html) trait.
+Each token has a `count()` value, and these tokens
+"fungible" in the sense that they can be combined and split, numbers
+combining additively.
+
+**Relationship between global field value and the token.**
+The global value of the `field` is the sum of the counts of all the tokens.
+
+## Manipulation of the field
+
+### Quick Reference
+
+In the following table, `n: nat`.
+
+| Command | +Meaning in transition | +Exchange Fn Parameter | +
|---|---|---|
init field = n; |
+ init field = n; |
+ Output tok |
+
remove field -= (n); |
+ require field >= n;update field = field - n; |
+ Input tok |
+
have field >= n; |
+ require field >= n; |
+ Input &tok |
+
add field += n; |
+ update field = field + n; |
+ Output tok |
+
tok
+with `count()` equal to `n`.
+
+### Adding a token (increasing the count)
+
+To write an operation that _creates_ a token,
+equivalently, adding to the total count, write,
+
+```rust
+add field += (n);
+```
+
+The resulting token exchange function will return a token of type tok
+with `count()` equal to `n`.
+
+### Removing a token
+
+To write an operation that _removes_ a token,
+equivalently, decreasing the total count,
+updating the field's value from `true` to `false`, write, inside any `transition!`
+operation:
+
+```rust
+remove field -= (n);
+```
+
+The resulting exchange function will consume a tok token
+with `count()` equal to `n`
+as a parameter.
+
+### Checking the value of the token
+
+To check the value of the token without removing it,
+write, inside any `transition!`, `readonly!` or `property!` operation:
+
+```rust
+have field >= (n);
+```
+
+The resulting exchange function will accept an immutable reference
+&tok (that is, it takes the token as input but does not consume it).
+
+## Example
+
+TODO
diff --git a/source/docs/state_machines/src/strategy-map.md b/source/docs/state_machines/src/strategy-map.md
index aaee424dd..be42dd044 100644
--- a/source/docs/state_machines/src/strategy-map.md
+++ b/source/docs/state_machines/src/strategy-map.md
@@ -188,7 +188,7 @@ To consume a MapToken<K, V, tok> where `tok.map() == m`:
+To check the value of a &MapToken<K, V, tok> where `tok.map() == m`:
```rust
have field >= (m);
diff --git a/source/docs/state_machines/src/strategy-multiset.md b/source/docs/state_machines/src/strategy-multiset.md
index 1776af6fe..9e0ea7f53 100644
--- a/source/docs/state_machines/src/strategy-multiset.md
+++ b/source/docs/state_machines/src/strategy-multiset.md
@@ -157,7 +157,7 @@ To consume a MultisetToken<K, V, tok> where `tok.multiset() == m`:
+To check the value of a &MultisetToken<K, V, tok> where `tok.multiset() == m`:
```rust
have field >= (m);
diff --git a/source/docs/state_machines/src/strategy-not-tokenized.md b/source/docs/state_machines/src/strategy-not-tokenized.md
new file mode 100644
index 000000000..c471e5593
--- /dev/null
+++ b/source/docs/state_machines/src/strategy-not-tokenized.md
@@ -0,0 +1,49 @@
+# not_tokenized
+
+The `not_tokenized` strategy can be applied to fields of any type `V`.
+
+```rust
+fields {
+ #[sharding(not_tokenized)]
+ pub field: V,
+}
+```
+
+This results in **no** token types associated to the field `field`.
+
+It is often useful as a convenient alternative when you would otherwise need an
+existential variable in the VerusSync invariant.
+
+## Manipulation of the field
+
+### Initializing the field
+
+Initializing the field is done with the usual `init` statement (as it for all strategies).
+
+```rust
+init field = v;
+```
+
+Of course, the instance-init function does not emit any tokens for this instruction.
+
+### Reading the field
+
+Reading the field can be done by writing `pre.field`. Notably, this causes the resulting
+operation to be non-deterministic in its input arguments. Therefore, `pre.field` can
+only be accessed in a [`birds_eye` context](./birds-eye.md).
+
+### Updating the field
+
+The field can always be updated with an `update` statement in any `transition!` operation.
+
+```rust
+update field = v;
+```
+
+This does not result in any token inputs or token outputs, and it has no effect on the
+signature of the token operation. The `update` instruction may be required in order to
+preserve the system invariant.
+
+## Example
+
+TODO
diff --git a/source/docs/state_machines/src/strategy-option.md b/source/docs/state_machines/src/strategy-option.md
index 7d21b2f81..072d1d3f4 100644
--- a/source/docs/state_machines/src/strategy-option.md
+++ b/source/docs/state_machines/src/strategy-option.md
@@ -91,7 +91,7 @@ related as follows:
value of opt_v: V |
+ value of opt_v: Option<V> |
value of optional token Option<tok> |
||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Command | +Meaning in transition | +Exchange Fn Parameter | +
|---|---|---|
init field = opt_tok; |
+ init field = opt_tok; |
+ Input Option<Tok> |
+
deposit field += Some(tok); |
+ assert field == None;update field = Some(tok); |
+ Input Tok |
+
guard field >= Some(tok); |
+ assert field == Some(tok); |
+ Output &Tok |
+
withdraw field -= Some(tok); |
+ assert field == Some(tok);update field = None; |
+ Output Tok |
+
deposit field += opt_tok; |
+ assert field == None || opt_tok == None;update field = opt_tok; |
+ Input Option<Tok> |
+
guard field >= opt_tok; |
+ assert opt_tok.is_some() ==> field == opt_tok; |
+ Output &Option<Tok> |
+
withdraw field -= opt_tok; |
+ assert opt_tok.is_some() ==> field == opt_tok;update field = if opt_tok == None { field } else { None }; |
+ Output Option<Tok> |
+
Option<Tok>,
+equal to the value of `opt_tok`.
+
+That is, if `opt_tok` is `None`, then the initial state has nothing "stored" and passing `None` to the constructor is trivial;
+if `opt_tok` is `Some(tok)`, then the initial state has `tok` "stored" and it must be supplied via the input argument for the constructor.
+
+### Performing a deposit
+
+To deposit a token tok: Tok, use the `deposit` statement in any `transition!` operation:
+
+```
+deposit field += Some(tok);
+```
+
+This sets the field value to `Some(tok)`. The resulting token operation then takes a token equal to `tok` as input.
+
+The `deposit` instruction has an inherent safety condition that `field` is `None` 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:
+
+```rust
+deposit field += Some(v)
+by {
+ // proof goes here
+};
+```
+
+### Performing a withdraw
+
+To withdraw a token tok: Tok, use the `withdraw` statement in any `transition!` operation:
+
+```
+withdraw field -= Some(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` is `Some(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:
+
+```rust
+withdraw field -= Some(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 -= Some(let $pat);
+```
+
+In this case, the inherent safety condition is that the `field` value is `Some` and that
+the inner 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`](./birds_eye.md)
+binders. Specifically, the pattern-matching variant is equivalent to:
+
+```
+birds_eye let stored_value = pre.field.unwrap();
+withdraw field -= Some(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 >= Some(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` is `Some(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:
+
+```rust
+guard field >= Some(tok)
+by {
+ // proof goes here
+};
+```
+
+### Operations that manipulate optional 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 `opt_tok == Some(tok)`,
+and they are all no-ops when `opt_tok == None`.
+
+To deposit an Option<Tok>:
+
+```rust
+deposit field += (opt_tok);
+```
+
+To withdraw an Option<Tok>:
+
+```rust
+remove field -= (opt_tok);
+```
+
+To obtain an &Option<Tok>:
+
+```rust
+guard field >= (opt_v);
+```
+
+## Example
+
+TODO
diff --git a/source/docs/state_machines/src/strategy-variable.md b/source/docs/state_machines/src/strategy-variable.md
index 2150860bd..855bd4209 100644
--- a/source/docs/state_machines/src/strategy-variable.md
+++ b/source/docs/state_machines/src/strategy-variable.md
@@ -49,7 +49,7 @@ If it's read _and_ modified, it will be input as a
### Updating the field
-Updating the field is done with the `update` statement:
+Updating the field is done with the `update` statement in any `transition!` operation:
```rust
update field = v;