Verus overview
Getting started
1.
Getting started
1.1.
... on the command line
1.2.
... with VSCode
Tutorial: Fundamentals
2.
Using Verus within Rust
3.
Basic specifications
3.1.
assert, requires, ensures, ghost code
3.2.
Expressions and operators for specifications
3.3.
Integers and arithmetic
3.4.
Equality
4.
Specification code, proof code, executable code
4.1.
spec functions
4.2.
proof functions, proof blocks, assert-by
4.3.
spec functions vs. proof functions, recommends
4.4.
Ghost code vs. exec code
4.5.
const declarations
4.6.
Putting it all together
5.
Recursion and loops
5.1.
Recursive spec functions, decreases, fuel
5.2.
Recursive exec and proof functions, proofs by induction
5.2.1.
Lightweight termination checking
5.3.
Loops and invariants
5.3.1.
Loops with break
5.3.2.
For Loops
5.4.
Lexicographic decreases clauses and mutual recursion
6.
Datatypes: struct and enum
6.1.
Struct
6.2.
Enum
7.
Libraries
7.1.
Specification libraries: Seq, Set, Map
7.2.
Executable libraries: Vec
8.
Spec closures
Tutorial: Understanding the prover
9.
Developing proofs
9.1.
Using assert and assume
9.2.
Devising loop invariants
9.3.
Proving absence of overflow
10.
Quantifiers
10.1.
forall and triggers
10.2.
Multiple variables, multiple triggers, matching loops
10.3.
exists and choose
10.4.
Proofs about forall and exists
10.5.
Example: binary search
10.6.
Ambient (broadcast) lemmas
11.
SMT solving, automation, and where automation fails
11.1.
What's decidable, what's undecidable, what's fast, what's slow
11.2.
Integers and nonlinear arithmetic
11.3.
Bit vectors and bitwise operations
11.4.
forall and exists: writing and using triggers, inline functions
11.5.
Recursive functions
11.6.
Extensional equality
11.7.
Libraries: incomplete axioms for Seq, Set, Map
12.
Managing proof performance and why it's critical
12.1.
Measuring verification performance
12.2.
Quantifier profiling
12.3.
Modules, hiding, opaque, reveal
12.4.
Hiding local proofs with assert (...) by { ... }
12.5.
Structured proofs by calculation
12.6.
Proof by computation
12.7.
Spinning off separate SMT queries
12.8.
Breaking proofs into smaller pieces
13.
Checklist: what to do when proofs go wrong
Tutorial: Verification and Rust
14.
Mutation, references, and borrowing
14.1.
Requires and ensures with mutable references
14.2.
Assertions containing mutable references
15.
Traits
16.
Higher-order executable functions
16.1.
Passing functions as values
16.2.
Closures
17.
Ghost and tracked variables
18.
Strings
18.1.
String library
18.2.
String literals
19.
Macros
20.
Unsafe code & complex ownership
20.1.
Cells / interior mutability
20.2.
Pointers
20.3.
Concurrency
21.
Verifying a container library: Binary Search Tree
21.1.
First draft
21.2.
Encapsulating well-formedness with type invariants
21.3.
Making it generic
21.4.
Implementing Clone
21.5.
Full source for the examples
22.
Interacting with unverified code
22.1.
Calling unverified code from verified code
22.2.
Calling verified code from unverified code
23.
Understanding the guarantees of a verified program
23.1.
Assumptions and trusted components
23.2.
Memory safety is conditional on verification
23.3.
Calling verified code from unverified code
Installation, configuration, and tooling
24.
Installation and setup
24.1.
IDE Support
24.2.
Installing and configuring Singular
25.
Project setup and development
25.1.
Working with crates
25.2.
Invoking Verus code from Rust
25.3.
Documentation with Rustdoc
Reference
26.
Supported and unsupported Rust features
27.
Verus syntax by example
28.
Modes
28.1.
Function modes
28.2.
Variable modes
29.
Spec expressions
29.1.
Rust subset
29.2.
Operator Precedence
29.3.
Arithmetic
29.4.
Bit operators
29.5.
Coercion with as
29.6.
Spec equality (==)
29.7.
Extensional equality (=~=, =~~=)
29.8.
Prefix and/or (&&& and |||)
29.9.
Chained operators
29.10.
Implication (==>, <==, and <==>)
29.11.
Quantifiers (forall, exists)
29.12.
Such that (choose)
29.13.
Trigger annotations
29.14.
The view function @
29.15.
Spec index operator []
29.16.
decreases_to!
30.
Proof features
30.1.
assert and assume
30.2.
assert ... by
30.3.
assert forall ... by
30.4.
assert ... by(bit_vector)
30.5.
assert ... by(nonlinear_arith)
30.6.
assert ... by(compute) / by(compute_only)
30.7.
reveal, reveal_with_fuel, hide
31.
Function specifications
31.1.
Function Signatures
31.1.1.
Exec fn signature
31.1.2.
Proof fn signature
31.1.3.
Spec fn signature
31.2.
Signature clauses
31.2.1.
requires / ensures
31.2.2.
returns
31.2.3.
opens_invariants
31.2.4.
no_unwind
31.2.5.
recommends
31.3.
Traits and signature inheritance
31.4.
Specifications on FnOnce
32.
Loop specifications
32.1.
invariant
32.2.
invariant_except_break / ensures
33.
Recursion and termination
33.1.
decreases ... when ... via ...
33.2.
Datatype ordering
33.3.
Cyclic definitions
34.
Type invariants
35.
Attribute list
36.
Directives
36.1.
assume_specification
36.2.
global
37.
Misc. Rust features
37.1.
Statics
37.2.
char
37.3.
Unions
37.4.
Pointers and cells
38.
Command line
38.1.
--record
39.
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.