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.
Verifying a container library: Binary Search Tree
20.1.
First draft
20.2.
Encapsulating well-formedness with type invariants
20.3.
Making it generic
20.4.
Implementing Clone
20.5.
Full source for the examples
21.
Understanding the guarantees of a verified program
21.1.
Assumptions and trusted components
21.2.
Memory safety is conditional on verification
21.3.
Calling verified code from unverified code
Installation, configuration, and tooling
22.
Installation and setup
22.1.
IDE Support
22.2.
Installing and configuring Singular
23.
Project setup and development
23.1.
Working with crates
23.2.
Invoking Verus code from Rust
23.3.
Documentation with Rustdoc
Reference
24.
Supported and unsupported Rust features
25.
Verus syntax by example
26.
Modes
26.1.
Function modes
26.2.
Variable modes
27.
Spec expressions
27.1.
Rust subset
27.2.
Operator Precedence
27.3.
Arithmetic
27.4.
Bit operators
27.5.
Coercion with as
27.6.
Spec equality (==)
27.7.
Extensional equality (=~=, =~~=)
27.8.
Prefix and/or (&&& and |||)
27.9.
Chained operators
27.10.
Implication (==>, <==, and <==>)
27.11.
Quantifiers (forall, exists)
27.12.
Such that (choose)
27.13.
Trigger annotations
27.14.
The view function @
27.15.
Spec index operator []
27.16.
decreases_to!
28.
Proof features
28.1.
assert and assume
28.2.
assert ... by
28.3.
assert forall ... by
28.4.
assert ... by(bit_vector)
28.5.
assert ... by(nonlinear_arith)
28.6.
assert ... by(compute) / by(compute_only)
28.7.
reveal, reveal_with_fuel, hide
29.
Function specifications
29.1.
requires / ensures
29.2.
opens_invariants
29.3.
no_unwind
29.4.
Traits and signature inheritance
29.5.
Specifications on FnOnce
29.6.
recommends
30.
Loop specifications
30.1.
invariant
30.2.
invariant_except_break / ensures
31.
Recursion and termination
31.1.
decreases ... when ... via ...
31.2.
Datatype ordering
31.3.
Cyclic definitions
32.
Type invariants
33.
Attribute list
34.
The "global" directive
35.
Misc. Rust features
35.1.
Statics
35.2.
char
35.3.
Unions
35.4.
Pointers and cells
36.
Command line
36.1.
--record
37.
Planned future work
Light (default)
Rust
Coal
Navy
Ayu
Verus Tutorial and Reference
Higher-order executable functions
Here we discuss the use of higher order functions via closures and other function types in Rust.