VerusSync guide: add more strategy reference pages

source/docs/state_machines/src/SUMMARY.md

@@ -43,11 +43,17 @@
     - [Macro-generated code (TODO)](./macro-generated-reference.md)
     - [State Machine Refinements (TODO)](./refinements-reference.md)
 
-  - [Tokenization](./tokenization-reference.md)
-    - [Strategy Reference](strategy-reference.md)
-      - [`variable`](strategy-variable.md)
-      - [`option`](strategy-option.md)
-      - [`map`](strategy-map.md)
-      - [`set`](strategy-set.md)
-      - [`multiset`](strategy-multiset.md)
+  - [VerusSync](./tokenization-reference.md)
+    - [Strategy Reference](./strategy-reference.md)
+      - [`variable`](./strategy-variable.md)
+      - [`option`](./strategy-option.md)
+      - [`map`](./strategy-map.md)
+      - [`set`](./strategy-set.md)
+      - [`multiset`](./strategy-multiset.md)
+      - [`bool`](./strategy-bool.md)
+      - [`count`](./strategy-count.md)
+      - [`not_tokenized`](./strategy-not-tokenized.md)
+      - [`storage_option`](./strategy-storage-option.md)
+    - [Operation definitions](./operations.md)
+      - [`birds_eye`](./birds-eye.md)
     - [Formalism of Tokenization by monoids (TODO)](./monoid-formalism.md)

source/docs/state_machines/src/birds-eye.md

@@ -0,0 +1,50 @@
+# The `birds_eye` command
+
+The `birds_eye` keyword can be used to allow unrestricted reads of the `pre` variable
+without impacting the tokens that are input or output in the operation.
+
+Specifically, `let` statements in transitions may be prefixed with the `birds_eye` annotation.
+
+```
+birds_eye let $var_name = $expr
+```
+
+The expression on the right-hand side may access `pre.field` for any field.
+A `birds_eye` let can be used in any `transition!`, `readonly!`, or `property!` operation.
+
+Though `birds_eye` allows accessing all fields, it is particularly useful for fields using
+the [`not_tokenized`](./strategy-not-tokenized.md) strategy or storage-based strategies.
+
+### Impact on determinism
+
+Ordinarily, VerusSync operations are deterministic in the input arguments and input tokens,
+a property enforced by various strategy-specific restrictions on how fields may be manipulated.
+However, when `birds_eye` is used, operations may become nondeterminstic.
+
+### Restrictions
+
+There are two main restrictions:
+
+ 1. No preconditions can depend on a `birds_eye` variable. This means that `require`,
+    `remove`, `have`, and `deposit` statements cannot depend on a `birds_eye` value.
+    Since this nondeterministic information is not available at the beginning of the token
+    operation, there would be no way to create a well-formed precondition.
+
+ 2. No `guard` operation can depend on a `birds_eye` variable. This is crucial for soundness;
+    the value being guarded must be deterministic as otherwise, the output token `&Tok`
+    might become invalid before its lifetime expires.
+
+These restrictions are currently implemented by a coarse-grained dependency analysis
+determined primarily by the order of statements, rather than the actual uses of variables.
+Dependency analysis may be made more precise in the future.
+
+### Impact on resulting ghost token operation
+
+The presencne of a `birds_eye` let-statement does not impact the tokens that are input
+or output. It does, however, create extra (ghost) out-parameters for the fields that
+are referenced inside `birds_eye`. This allows the operation's postconditions to
+refer to these nondeterministic values.
+
+## Example
+
+TODO

source/docs/state_machines/src/operations.md

@@ -0,0 +1 @@
+# Operations

source/docs/state_machines/src/strategy-bool.md

@@ -0,0 +1,177 @@
+# The `bool` strategy
+
+The `bool` strategy can be applied to fields of type `bool`.
+
+```rust
+fields {
+    #[sharding(bool)]
+    pub field: bool,
+}
+```
+
+**Tokens.**
+VerusSync creates a fresh token type, <code style="font-style: italic; color: #408040">tok</code>,
+named `State::field` where `State` is the name of the VerusSync system and `field` is the name of the field.
+
+The token type <code style="font-style: italic; color: #408040">tok</code> 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`.
+
+<div class="table-wrapper" style="font-size: 13px"><table>
+  <colgroup>
+     <col span="1" style="width: 40%;">
+     <col span="1" style="width: 45%;">
+     <col span="1" style="width: 15%;">
+  </colgroup>
+  <thead>
+    <tr>
+      <th>Command</th>
+      <th>Meaning in transition</th>
+      <th>Exchange Fn Parameter</th>
+    </tr>
+  </thead>
+  <tbody>
+    <tr><td></td><td></td><td></td></tr>
+    <tr>
+      <td><code>init field = b;</code></td>
+      <td><code>init field = b;</code></td>
+      <td>Output <code>Option&lt;<span style="font-style: italic; color: #408040">tok</span>&gt;</code></td>
+    </tr> <tr>
+      <td><code>remove field -= true;</code></td>
+      <td><code>require field == true;</code><br><code>update field = false;</code></td>
+      <td>Input <code><span style="font-style: italic; color: #408040">tok</span></code></td>
+    </tr> <tr>
+      <td><code>have field &gt;= true;</code></td>
+      <td><code>require field == true;</code></td>
+      <td>Input <code>&amp;<span style="font-style: italic; color: #408040">tok</span></code></td>
+    </tr> <tr>
+      <td><code>add field += true;</code></td>
+      <td><code>assert field == false;</code><br><code>update field = true;</code></td>
+      <td>Output <code><span style="font-style: italic; color: #408040">tok</span></code></td>
+    </tr> <tr>
+      <td><code>remove field -= (b);</code></td>
+      <td><code style="white-space: pre">require (b ==> field);
+update field = field && !b;</code></td>
+      <td>Input <code>Option&lt;<span style="font-style: italic; color: #408040">tok</span>&gt;</code></td>
+    </tr> <tr>
+      <td><code>have field &gt;= (b);</code></td>
+      <td><code>require (b ==> field);</code></td>
+      <td>Input <code>&amp;Option&lt;<span style="font-style: italic; color: #408040">tok</span>&gt;</code></td>
+    </tr> <tr>
+      <td><code>add field += (b);</code></td>
+      <td><code style="white-space: pre">assert !(field && b);
+update field = field || b;</code></td>
+      <td>Output <code>Option&lt;<span style="font-style: italic; color: #408040">tok</span>&gt;</code></td>
+    </tr>
+  </tbody>
+</table></div>
+
+### Initializing the field
+
+Initializing the field is done with the usual `init` statement (as it for all strategies).
+
+```rust
+init field = b;
+```
+
+The instance-init function will return a token of type <code>Option&lt;<span style="font-style: italic; color: #408040">tok</span>&gt;</code>,
+related as follows:
+
+<table>
+  <tr>
+    <th>value of <code>b: bool</code></th>
+    <th>&nbsp;&nbsp;&nbsp;value of optional token <code>Option&lt;<span style="font-style: italic; color: #408040">tok</span>></code></th>
+  </tr>
+  <tr>
+    <td><code>false</code></td>
+    <td><code>None</code></td>
+  </tr>
+  <tr>
+    <td><code>true</code></td>
+    <td><code>Some(tok)</code> where <code>tok.value() == v</code></td>
+  </tr>
+</table>
+
+### Adding a token
+
+To write an operation that _creates_ a token,
+equivalently,
+updating the field's value from `false` to `true`, write, inside any `transition!`
+operation:
+
+```rust
+add field += true;
+```
+
+This operation has an inherent safety condition that the prior value of `field` is `false`.
+The resulting token exchange function will return a token of type <code><span style="font-style: italic; color: #408040">tok</span></code>.
+
+### 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 <code><span style="font-style: italic; color: #408040">tok</span></code> 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
+<code>&amp;<span style="font-style: italic; color: #408040">tok</span></code> (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 <code>Option&lt;<span style="font-style: italic; color: #408040">tok</span>&gt;</code>:
+
+```rust
+add field += (b);
+```
+
+To consume an <code>Option&lt;<span style="font-style: italic; color: #408040">tok</span>&gt;</code>:
+
+```rust
+remove field -= (b);
+```
+
+To check the value of an <code>&amp;Option&lt;<span style="font-style: italic; color: #408040">tok</span>&gt;</code>:
+
+```rust
+have field >= (b);
+```
+
+
+The value of `b` is related to the value of
+<code>Option&lt;<span style="font-style: italic; color: #408040">tok</span>&gt;</code>
+as [they are for initialization](#initializing-the-field).
+
+## Example
+
+TODO

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, <code style="font-style: italic; color: #408040">tok</code>,
+named `State::field` where `State` is the name of the VerusSync system and `field` is the name of the field.
+
+The token type <code style="font-style: italic; color: #408040">tok</code> 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`.
+
+<div class="table-wrapper" style="font-size: 13px"><table>
+  <colgroup>
+     <col span="1" style="width: 40%;">
+     <col span="1" style="width: 45%;">
+     <col span="1" style="width: 15%;">
+  </colgroup>
+  <thead>
+    <tr>
+      <th>Command</th>
+      <th>Meaning in transition</th>
+      <th>Exchange Fn Parameter</th>
+    </tr>
+  </thead>
+  <tbody>
+    <tr><td></td><td></td><td></td></tr>
+    <tr>
+      <td><code>init field = n;</code></td>
+      <td><code>init field = n;</code></td>
+      <td>Output <code><span style="font-style: italic; color: #408040">tok</span></code></td>
+    </tr> <tr>
+      <td><code>remove field -= (n);</code></td>
+      <td><code>require field >= n;</code><br><code>update field = field - n;</code></td>
+      <td>Input <code><span style="font-style: italic; color: #408040">tok</span></code></td>
+    </tr> <tr>
+      <td><code>have field &gt;= n;</code></td>
+      <td><code>require field >= n;</code></td>
+      <td>Input <code>&amp;<span style="font-style: italic; color: #408040">tok</span></code></td>
+    </tr> <tr>
+      <td><code>add field += n;</code></td>
+      <td><code>update field = field + n;</code></td>
+      <td>Output <code><span style="font-style: italic; color: #408040">tok</span></code></td>
+    </tr>
+  </tbody>
+</table></div>
+
+### Initializing the field
+
+Initializing the field is done with the usual `init` statement (as it for all strategies).
+
+```rust
+init field = n;
+```
+
+The instance-init function will return a token of type <code><span style="font-style: italic; color: #408040">tok</span></code>
+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 <code><span style="font-style: italic; color: #408040">tok</span></code>
+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 <code><span style="font-style: italic; color: #408040">tok</span></code> 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
+<code>&amp;<span style="font-style: italic; color: #408040">tok</span></code> (that is, it takes the token as input but does not consume it).
+
+## Example
+
+TODO

source/docs/state_machines/src/strategy-map.md

@@ -188,7 +188,7 @@ To consume a <a href="https://verus-lang.github.io/verus/verusdoc/vstd/tokens/st
 remove field -= (m);
 ```
 
-To check the value of a <a href="https://verus-lang.github.io/verus/verusdoc/vstd/tokens/struct.MapToken.html"><code>MapToken&lt;K, V, <span style="font-style: italic; color: #408040">tok</span>&gt;</code></a> where `tok.map() == m`:
+To check the value of a <code>&amp;<a href="https://verus-lang.github.io/verus/verusdoc/vstd/tokens/struct.MapToken.html">MapToken&lt;K, V, <span style="font-style: italic; color: #408040">tok</span>&gt;</a></code> where `tok.map() == m`:
 
 ```rust
 have field >= (m);

source/docs/state_machines/src/strategy-multiset.md

@@ -157,7 +157,7 @@ To consume a <a href="https://verus-lang.github.io/verus/verusdoc/vstd/tokens/st
 remove field -= (m);
 ```
 
-To check the value of a <a href="https://verus-lang.github.io/verus/verusdoc/vstd/tokens/struct.MultisetToken.html"><code>MultisetToken&lt;K, V, <span style="font-style: italic; color: #408040">tok</span>&gt;</code></a> where `tok.multiset() == m`:
+To check the value of a <code>&amp;<a href="https://verus-lang.github.io/verus/verusdoc/vstd/tokens/struct.MultisetToken.html">MultisetToken&lt;K, V, <span style="font-style: italic; color: #408040">tok</span>&gt;</a></code> where `tok.multiset() == m`:
 
 ```rust
 have field >= (m);