Verus overview
Getting started
1.
Getting started
Tutorial: Fundamentals
2.
Basic specifications
2.1.
assert, requires, ensures, ghost code
2.2.
Expressions and operators for specifications
2.3.
Integers and arithmetic
2.4.
Equality
3.
Specification code, proof code, executable code
3.1.
spec functions
3.2.
proof functions, proof blocks, assert-by
3.3.
spec functions vs. proof functions, recommends
3.4.
Ghost code vs. exec code
3.5.
const declarations
4.
Recursion and loops
4.1.
Recursive spec functions, decreases, fuel
4.2.
Recursive exec and proof functions, proofs by induction
4.3.
Loops and invariants
4.3.1.
Loops with break
4.4.
Lexicographic decreases clauses and mutual recursion
5.
Datatypes: struct and enum
5.1.
Struct
5.2.
Enum
6.
Libraries
6.1.
Specification libraries: Seq, Set, Map
6.2.
Executable libraries: Vec
7.
Spec closures
Tutorial: Understanding the prover
8.
Using assert and assume to develop proofs
9.
Quantifiers
9.1.
forall and triggers
9.2.
Multiple variables, multiple triggers, matching loops
9.3.
exists and choose
9.4.
Proofs about forall and exists
9.5.
Example: binary search
9.6.
Ambient (broadcast) lemmas
10.
SMT solving, automation, and where automation fails
10.1.
What's decidable, what's undecidable, what's fast, what's slow
10.2.
Integers and nonlinear arithmetic
10.3.
Bit vectors and bitwise operations
10.4.
forall and exists: writing and using triggers, inline functions
10.5.
Recursive functions
10.6.
Extensional equality
10.7.
Libraries: incomplete axioms for Seq, Set, Map
11.
Managing proof performance and why it's critical
11.1.
Measuring verification performance
11.2.
Quantifier profiling
11.3.
Modules, hiding, opaque, reveal
11.4.
Hiding local proofs with assert (...) by { ... }
11.5.
Structured proof by calculation
11.6.
Proof by computation
11.7.
Spinning off separate SMT queries
11.8.
Breaking proofs into smaller pieces
12.
Checklist: what to do when proofs go wrong
Tutorial: Verification and Rust
13.
Mutation, references, and borrowing
13.1.
Requires and ensures with mutable references
13.2.
Assertions containing mutable references
14.
Traits
15.
Higher-order executable functions
15.1.
Passing functions as values
15.2.
Closures
16.
Ghost and tracked variables
17.
Strings
17.1.
String library
17.2.
String literals
18.
Macros
19.
Unsafe code & complex ownership
19.1.
Cells / interior mutability
19.2.
Pointers
19.3.
Concurrency
20.
Understanding the guarantees of a verified program
20.1.
Assumptions and trusted components
20.2.
Memory safety is conditional on verification
20.3.
Calling verified code from unverified code
Installation, configuration, and tooling
21.
Installation and setup
21.1.
IDE Support
21.2.
Installing and configuring Singular
22.
Project setup and development
22.1.
Working with crates
22.2.
Invoking Verus code from Rust
22.3.
Documentation with Rustdoc
Reference
23.
Supported and unsupported Rust features
24.
Verus syntax by example
25.
Modes
25.1.
Function modes
25.2.
Variable modes
26.
Spec expressions
26.1.
Rust subset
26.2.
Operator Precedence
26.3.
Arithmetic
26.4.
Bit operators
26.5.
Coercion with as
26.6.
Spec equality (==)
26.7.
Extensional equality (=~=, =~~=)
26.8.
Prefix and/or (&&& and |||)
26.9.
Chained operators
26.10.
Implication (==>, <==, and <==>)
26.11.
Quantifiers (forall, exists)
26.12.
Such that (choose)
26.13.
Trigger annotations
26.14.
The view function @
26.15.
Spec index operator []
26.16.
decreases_to!
27.
Proof features
27.1.
assert and assume
27.2.
assert ... by
27.3.
assert forall ... by
27.4.
assert ... by(bit_vector)
27.5.
assert ... by(nonlinear_arith)
27.6.
assert ... by(compute) / by(compute_only)
27.7.
reveal, reveal_with_fuel, hide
28.
Function specifications
28.1.
requires / ensures
28.2.
opens_invariants
28.3.
no_unwind
28.4.
Traits and signature inheritance
28.5.
Specifications on FnOnce
28.6.
recommends
29.
Loop specifications
29.1.
invariant
29.2.
invariant_except_break / ensures
30.
Recursion and termination
30.1.
decreases ... when ... via ...
30.2.
Datatype ordering
30.3.
Cyclic definitions
31.
Type invariants
32.
Attribute list
33.
The "global" directive
34.
Misc. Rust features
34.1.
Statics
34.2.
char
34.3.
Unions
34.4.
Pointers and cells
35.
Command line
35.1.
--record
36.
Planned future work
Light (default)
Rust
Coal
Navy
Ayu
Verus Tutorial and Reference
Such that (
choose
)
The such-that operator (
choose
) is explained in
exists and choose
.