Intro
User Guide
1.
Tokenized State Machines
1.1.
High-Level Idea
1.2.
Guide by example
1.2.1.
Counting to 2
1.2.1.1.
Unverified Source
1.2.1.2.
Verified Source
1.2.2.
Counting to n
1.2.2.1.
Unverified Source
1.2.2.2.
Verified Source
1.2.3.
Producer-consumer queue
1.2.3.1.
Unverified Source
1.2.3.2.
Verified Source
1.2.4.
Reference-counted smart pointer
1.2.4.1.
Unverified Source
1.2.4.2.
Verified Source
1.2.4.3.
Exercises
1.3.
Guide TODO
1.3.1.
Counting to n (again) (TODO)
1.3.2.
Hash table (TODO)
1.3.3.
Reader-writer lock (TODO)
Reference
2.
State Machines
2.1.
State Machine Basics
2.2.
State Machine Macro Syntax (TODO)
2.3.
Transition Language
2.4.
Invariants and Inductive Proofs
2.5.
Macro-generated code (TODO)
2.6.
State Machine Refinements (TODO)
3.
VerusSync
3.1.
Strategy Reference
3.1.1.
variable
3.1.2.
constant
3.1.3.
option
3.1.4.
map
3.1.5.
set
3.1.6.
multiset
3.1.7.
bool
3.1.8.
count
3.1.9.
persistent_option
3.1.10.
persistent_map
3.1.11.
persistent_set
3.1.12.
persistent_bool
3.1.13.
persistent_count
3.1.14.
not_tokenized
3.1.15.
storage_option
3.1.16.
storage_map
3.2.
Operation definitions
3.2.1.
birds_eye
3.3.
Formalism of Tokenization by monoids (TODO)
Light (default)
Rust
Coal
Navy
Ayu
Verus Transition Systems
Counting to n (again) (TODO)