diff --git a/source/docs/guide/book.toml b/source/docs/guide/book.toml
index 0f02ac4ec5..486368913b 100644
--- a/source/docs/guide/book.toml
+++ b/source/docs/guide/book.toml
@@ -11,3 +11,6 @@ smart-punctuation = true
[output.html.playground]
runnable = false
+
+[preprocessor.verus-grammar]
+command = "python3 verus-grammar.py"
diff --git a/source/docs/guide/src/SUMMARY.md b/source/docs/guide/src/SUMMARY.md
index b86dabad7e..663f5e7893 100644
--- a/source/docs/guide/src/SUMMARY.md
+++ b/source/docs/guide/src/SUMMARY.md
@@ -137,8 +137,8 @@
- [Spec and proof attributes for exec functions](exec_attr.md)
- [Automatic exec to spec functions](exec_to_spec.md)
- [Spec expressions](./spec-expressions.md)
- - [Rust subset](./spec-rust-subset.md)
- [Operator Precedence](./spec-operator-precedence.md)
+ - [Rust subset](./spec-rust-subset.md)
- [Arithmetic](./spec-arithmetic.md)
- [Bit operators](./spec-bit-ops.md)
- [Coercion with `as`](./reference-as.md)
@@ -152,7 +152,11 @@
- [Trigger annotations](./trigger-annotations.md)
- [The view function `@`](./reference-at-sign.md)
- [Spec index operator `[]`](./reference-spec-index.md)
+ - [The `has` operator](./reference-has.md)
+ - [The `is` operator](./reference-is.md)
+ - [The `matches` operator](./reference-matches.md)
- [`decreases_to!`](./reference-decreases-to.md)
+- [Types](./reference-types.md)
- [Proof features]()
- [assert and assume]()
- [assert ... by](./reference-assert-by.md)
@@ -161,6 +165,7 @@
- [assert ... by(nonlinear_arith)](./reference-assert-by-nonlinear.md)
- [assert ... by(compute) / by(compute_only)](./reference-assert-by-compute.md)
- [reveal, reveal_with_fuel, hide](./reference-reveal-hide.md)
+ - [reveal_strlit](./reference-reveal-strlit.md)
- [Function specifications]()
- [Function Signatures]()
- [Exec fn signature](./reference-exec-signature.md)
@@ -189,7 +194,6 @@
- [`global`](./reference-global.md)
- [Misc. Rust features]()
- [Statics](./static.md)
- - [char](./char.md)
- [Unions](./reference-unions.md)
- [Pointers and cells](./reference-pointers-cells.md)
- [Command line]()
diff --git a/source/docs/guide/src/char.md b/source/docs/guide/src/char.md
deleted file mode 100644
index f719df8288..0000000000
--- a/source/docs/guide/src/char.md
+++ /dev/null
@@ -1,17 +0,0 @@
-# The `char` primitive
-
-Citing the [Rust documentation on `char`](https://doc.rust-lang.org/std/primitive.char.html):
-
-> A char is a ‘Unicode scalar value’, which is any ‘Unicode code point’ other than a surrogate code point. This has a fixed numerical definition: code points are in the range 0 to 0x10FFFF, inclusive. Surrogate code points, used by UTF-16, are in the range 0xD800 to 0xDFFF.
-
-Verus treats `char` similarly to bounded integer primitives like `u64` or `u32`: We represent
-`char` as an integer. A `char` always carries an invariant that it is in the prescribed set
-of allowed values:
-
-`[0, 0xD7ff] ∪ [0xE000, 0x10FFFF]`
-
-In spec code, chars can be [cast to and from other integer types using `as`](./reference-as.md).
-This is more
-permissive than exec code, which disallows many of these coercions.
-As with other coercions, the result may be undefined if the integer being coerced does not
-fit in the target range.
diff --git a/source/docs/guide/src/erasure.md b/source/docs/guide/src/erasure.md
index 6bb825f7e8..eae0f0bcd7 100644
--- a/source/docs/guide/src/erasure.md
+++ b/source/docs/guide/src/erasure.md
@@ -39,7 +39,7 @@ pub mod test_mod {
}
```
-Anoter use-case for the `verus_only` flag is setting attributes that only make sense during verification.
+Another use-case for the `verus_only` flag is setting attributes that only make sense during verification.
For instance, the code below sets the `verifier::loop_isolation` option to false for the file, only if `verus_only` is set:
```rust
#![cfg_attr(verus_only, verus::loop_isolation(false))]
diff --git a/source/docs/guide/src/prefix-and-or.md b/source/docs/guide/src/prefix-and-or.md
index 798cd7d4f2..f414e301c9 100644
--- a/source/docs/guide/src/prefix-and-or.md
+++ b/source/docs/guide/src/prefix-and-or.md
@@ -1,3 +1,35 @@
# Prefix and/or (`&&&` and `|||`)
-The prefix and/or operators (`&&&` and `|||`) are explained in [Expressions and operators for specifications](operators.md).
+For an introduction, see [Expressions and operators for specifications](operators.md).
+
+### Syntax
+
+```verus-grammar
+V@[prefix_and_expr] ::= (&&& V@[spec_expr])+
+V@[prefix_or_expr] ::= (||| V@[spec_expr])+
+```
+
+Each operand is introduced by its operator as a prefix. `&&&` is the prefix conjunction
+and `|||` is the prefix disjunction. Both bind looser than all other binary operators
+(see [operator precedence](./spec-operator-precedence.md)).
+
+### Typing
+
+Each operand must have type `bool`. The expression returns `bool`.
+
+### Semantics
+
+`&&&` and `|||` are shorthand for `&&` and `||`, written in prefix form. A sequence of
+`&&&`-prefixed operands is equivalent to the corresponding infix conjunction, and likewise
+for `|||`:
+
+```
+&&& P &&& Q &&& R ≡ P && Q && R
+||| P ||| Q ||| R ≡ P || Q || R
+```
+
+As all spec expressions are pure and effectless, there is no notion of short-circuiting.
+
+The main motivation for these operators is readability: when writing a large conjunction
+or disjunction (such as a precondition or an invariant), the leading-prefix style makes it
+easy to add, remove, or reorder clauses without adjusting punctuation elsewhere.
diff --git a/source/docs/guide/src/ref-extensional-equality.md b/source/docs/guide/src/ref-extensional-equality.md
index 705c42143d..5ee780dce5 100644
--- a/source/docs/guide/src/ref-extensional-equality.md
+++ b/source/docs/guide/src/ref-extensional-equality.md
@@ -1,4 +1,27 @@
# Extensional equality (`=~=` and `=~~=`)
-The extensional equality operators `=~=` and `=~~=` are explained in
-[Extensional equality](extensional_equality.md).
+The **shallow extensional equality operator** `=~=`
+and **deep extensional equality operator** `=~~=` are both equivalent to
+[spec equality (`==`)](./spec-equality.md).
+
+These operators are distinguished only by their impact on the proof search.
+Specifically, the use of the `=~=` and `=~~=` operators will trigger the application of
+"extensional equality" operators.
+
+See [the guide page](extensional_equality.md) for an introductory explanation with motivation.
+
+### Syntax
+
+```verus-grammar
+V@[ext_eq_expr] ::= V@[spec_expr] =~= V@[spec_expr]
+ | V@[spec_expr] =~~= V@[spec_expr]
+```
+
+### Typing
+
+The extensional equality operator requires both the left-hand side and right-hand side
+to have the same type. The expression returns a [`bool`](./reference-types#bool).
+
+### Semantics
+
+The operator is equivalent to [spec equality](./spec-equality.md).
diff --git a/source/docs/guide/src/reference-as.md b/source/docs/guide/src/reference-as.md
index 65a34e6e51..b3ce0337dd 100644
--- a/source/docs/guide/src/reference-as.md
+++ b/source/docs/guide/src/reference-as.md
@@ -1,7 +1,14 @@
# Coercion with `as`
-In spec code, any "integer type" may be coerced to any other integer type via `as`.
-For the sake of this page, "integer type" means any of the following:
+## Syntax
+
+```verus-grammar
+V@[as_expr] ::= V@[spec_expr] as R@[type]
+```
+
+## Coercions on integer types and `char`
+
+Any of the following types may be coerced to any of the other types:
* `i8`, `i16`, `i32`, `i64`, `i128`, `isize`
* `u8`, `u16`, `u32`, `u64`, `u128`, `usize`
@@ -13,7 +20,7 @@ Note that this is more permissive than `as` in Rust exec code. For example, Rust
not permit using `as` to cast from a `u16` to a `char`, but this is allowed in Verus
spec code.
-## Definition
+### Definition
Verus defines `as`-casting as follows:
@@ -24,7 +31,7 @@ Verus defines `as`-casting as follows:
lower N bits for the appropriate N, then interpreting the result as a signed or unsigned
integer.
-## Reasoning about truncation
+### Reasoning about truncation
The definition of truncation is _not_ exported in Verus's default prover mode
(i.e., it behaves as if it is unspecified). To reason about truncation, use
@@ -32,3 +39,31 @@ The definition of truncation is _not_ exported in Verus's default prover mode
or the [compute solver](./reference-assert-by-compute.md).
Also note that the value of N for `usize` and `isize` may be [configured with the `global` directive](./reference-global.md).
+
+## Coercions on pointers
+
+### Pointers to integers
+
+You can coerce any pointer to any integer type. For a pointer `ptr: *mut T` or `ptr: *const T`,
+the expression `ptr as INT_TYPE` is equivalent to `ptr.addr() as INT_TYPE`.
+
+> **Note:** Using `ptr.addr()` explicitly is often clearer than an `as`-cast.
+
+> **Note:** Verus does not support casting an integer to a pointer using `as`. Instead, use a function like [`with_addr`](https://verus-lang.github.io/verus/verusdoc/vstd/std_specs/struct.VstdSpecsForRustStdLib.html#method._verus_external_fn_specification_1018__60__32__42__32_mut_32_T_32__62__32__58__58__32_with__addr) or [`with_exposed_provenance`](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/fn.with_exposed_provenance.html).
+
+### Pointers to pointers
+
+Verus supports some pointer-to-pointer coercions, including between `*const` and `*mut` pointers:
+
+ * `*mut T` to `*const T` (identity function)
+ * `*const T` to `*mut T` (identity function)
+
+And other kinda of coercions:
+
+ * `*mut T` to `*mut S` for any `S: Sized` ([spec](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/fn.spec_cast_ptr_to_thin_ptr.html))
+ * `*mut [T; N]` to `*mut [T]` ([spec](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/fn.spec_cast_array_ptr_to_slice_ptr.html))
+ * `*mut [T]` to `*mut [U]` ([spec](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/fn.spec_cast_slice_ptr_to_slice_ptr.html))
+ * `*mut [T]` to `*mut str` ([spec](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/fn.spec_cast_slice_ptr_to_str_ptr.html))
+ * `*mut str` to `*mut [T]` ([spec](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/fn.spec_cast_str_ptr_to_slice_ptr.html))
+
+And the equivalent set of casts for `*const` pointers.
diff --git a/source/docs/guide/src/reference-assert-by.md b/source/docs/guide/src/reference-assert-by.md
index d3ea7fff02..9163431151 100644
--- a/source/docs/guide/src/reference-assert-by.md
+++ b/source/docs/guide/src/reference-assert-by.md
@@ -1,6 +1,16 @@
# assert ... by
-The `assert ... by` statement is used to encapsulate a proof. For a boolean `spec` expression, `P`, one writes:
+The `assert ... by` statement is used to encapsulate a proof.
+
+### Syntax
+
+```verus-grammar
+V@[assert_by_stmt] ::= assert ( V@[spec_expr] ) by { V@[proof_stmt]* }
+```
+
+### Proof operation
+
+For a boolean predicate `P`:
```rust
assert(P) by {
@@ -9,7 +19,7 @@ assert(P) by {
// ... remainder
```
-Verus will validate the proof and then attempt to use it to prove the P.
+Verus will validate the proof and then attempt to use it to prove `P`.
The contents of the proof, however, will not be included in the context used to
prove the remainder.
Only `P` will be introduced into the context for the remainder.
diff --git a/source/docs/guide/src/reference-assert-forall-by.md b/source/docs/guide/src/reference-assert-forall-by.md
index 173fd064d6..d81198155e 100644
--- a/source/docs/guide/src/reference-assert-forall-by.md
+++ b/source/docs/guide/src/reference-assert-forall-by.md
@@ -3,29 +3,29 @@
The `assert forall ... by` statement is used to write a proof of a `forall` expression
while introducing the quantified variables into the context.
-```rust
-assert forall |idents| P by {
- // ... proof here
-}
-// ... remainder
+### Syntax
+
+```verus-grammar
+V@[assert_by_forall_stmt] ::=
+ assert forall |R@[binders]| (V@[spec_expr] implies)? V@[spec_expr] by { V@[proof_stmt]* }
```
-Much like an ordinary [`assert ... by`](./reference-assert-by.md) statement, the proof
-inside the body does not enter the context for the remainder of the proof.
-Only the `forall |idents| P` expression enters the context.
-Furthermore, within the proof body, the variables in the `idents` may be
+Note the lack of parentheses, in contrast to the ordinary `assert` statements.
-Note that the **parentheses _must_ be left off**, in contrast to other kinds of `assert` statements.
+### Typing
-For convenience, you can use `implies` to introduce a hypothesis automatically into
-the proof block:
+The spec expressions and proof body may refer to variables bound in the R@[binders].
+The spec expressions must have type `bool`.
-```rust
-assert forall |idents| H implies P by {
- // ... proof here
-}
-// ... remainder
-```
+### Proof operation
-This will make `H` available in the proof block, so you only have to prove `P`.
-In the end, the predicate `forall |idents| H ==> P` will be proved.
+For an `assert forall` statement of the form `assert forall |binders| P implies Q`,
+the predicate `P` is introduced as a hypothesis for the proof body, and the objective of the proof
+body is to prove `Q`. In the end, the predicate `forall |binders| P ==> Q` is proved,
+which is available in the context for the remainder of the proof.
+
+The simplified form `assert forall |binders| Q` is equivalent to
+`assert forall |binders| true implies Q`.
+
+Much like an ordinary [`assert ... by`](./reference-assert-by.md) statement, the proof
+inside the body does not enter the context for the remainder of the proof.
diff --git a/source/docs/guide/src/reference-assume-specification.md b/source/docs/guide/src/reference-assume-specification.md
index ace5ab9c3d..aa112ff2b9 100644
--- a/source/docs/guide/src/reference-assume-specification.md
+++ b/source/docs/guide/src/reference-assume-specification.md
@@ -16,23 +16,23 @@ as its corresponding function. However:
The general form of this directive is:
-
-assume_specification generics? [ function_path ] (args...) -> return_type_and_name?
- where_clause?
- requires_clause?
- ensures_clause?
- returns_clause?
- invariants_clause?
- unwind_clause?
- ;
-
-
+```verus-grammar
+assume_specification_item ::=
+ visibility? assume_specification R@[generics]? [ R@[function_path] ] (R@[args...]) ( -> V@[exec_return_type] )?
+ R@[where_clause]?
+ V@[requires_clause]?
+ V@[ensures_clause]?
+ V@[returns_clause]?
+ V@[invariants_clause]?
+ V@[unwind_clause]?
+ ;
+```
It is intended to look like an ordinary Rust function signature with a [Verus specification](./reference-exec-signature.md), except instead of having a name, it refers to a different function by path.
For associated functions and methods, the function_path should have the form `Type::method_name`,
using "turbofish syntax" for the type (e.g., `Vec::`).
-For trait methods, the function_path should use the "qualified self" form, `::method_name`.
+For trait methods, the function_path should use the ["qualified self"](https://doc.rust-lang.org/reference/paths.html#qualified-paths) form, `::method_name`.
The signature must be the same as the function in question, including arguments, return type, generics, and trait bounds.
All arguments should be named and should _not_ use `self`.
@@ -72,3 +72,26 @@ To apply to `clone` for a specific type:
pub assume_specification [::clone](b: &bool) -> (res: bool)
ensures res == b;
```
+
+### Type signature matching
+
+Verus requires the type signature and trait bounds to match exactly.
+If these do not line up, you will get an error message displaying the mismatched signature or mismatched trait bounds.
+It can sometimes be nontrivial to get these to line up due to differences in the source form and the internal form.
+
+Tips:
+
+1. It usually helps to make all lifetime variables (e.g., `'a`) explicit.
+
+2. The `Sized` trait is somewhat complex, as the source form of `Sized`-bounds doesn't always look like
+ Rust's internal represenation of the trait bound. This is also complicated by unstable `Sized` features.
+ As of Rust 1.95.0, these are related as follows:
+
+| Source bound | Internal bound |
+|-------------------|----------------|
+| No bound | `T: Sized` |
+| `T: Sized` | `T: Sized` |
+| `T: ?Sized` | `T: MetaSized` |
+| `T: PointeeSized` | No bound |
+
+
diff --git a/source/docs/guide/src/reference-at-sign.md b/source/docs/guide/src/reference-at-sign.md
index 2e90ff5fd8..d9afc4913e 100644
--- a/source/docs/guide/src/reference-at-sign.md
+++ b/source/docs/guide/src/reference-at-sign.md
@@ -1,6 +1,22 @@
# The view function `@`
-The expression `expr@` is a shorthand for `expr.view()`. The `view()` function is a Verus
-convention for the abstraction of an exec-mode object, usually [defined by the `View` trait](https://verus-lang.github.io/verus/verusdoc/vstd/view/trait.View.html).
-However, the expansion of the `@` syntax is purely syntactic, so it does not necessarily
-correspond to the trait function.
+### Syntax
+
+```verus-grammar
+V@[view_expr] ::= V@[spec_expr] @
+```
+
+### Desugaring
+
+The expression `expr@` desugars to the expression `expr.view()`, which is resolved as normal via
+Rust's [method resolution](https://doc.rust-lang.org/reference/expressions/method-call-expr.html).
+This usually, but not always, resolves to the `view` method [defined by the `View` trait](https://verus-lang.github.io/verus/verusdoc/vstd/view/trait.View.html).
+
+### Use cases
+
+By convention, the `view()` function is a Verus
+convention for the abstraction of an exec-mode object.
+See, for example:
+
+ * [Using view to reason about `Vec`](./exec_lib.md)
+ * [Defining a view function](./container_bst_first_draft.md#the-abstract-view)
diff --git a/source/docs/guide/src/reference-chained-op.md b/source/docs/guide/src/reference-chained-op.md
index 2bdcdd0b58..c2de9be9d9 100644
--- a/source/docs/guide/src/reference-chained-op.md
+++ b/source/docs/guide/src/reference-chained-op.md
@@ -1,9 +1,29 @@
# Chained operators
-In spec code, equality and inequality operators can be chained. For example,
-`a <= b < c`
-is equivalent to
-`a <= b && b < c`.
+### Syntax
-Chained inequalities support `<`, `<=`, `>`, `>=`, and `==`, and support sequences of chained
-operators of arbitrary length.
+```verus-grammar
+V@[chained_expr] ::= V@[spec_expr] V@[cmp_op] V@[spec_expr] (V@[cmp_op] V@[spec_expr])+
+V@[cmp_op] ::= < | <= | > | >= | ==
+```
+
+### Typing
+
+All operands in a chained expression must be [integer types](./reference-types.md#integer-types).
+The expression returns `bool`.
+
+Chained operators are only available in spec mode.
+
+### Semantics
+
+A chained comparison desugars into the conjunction of all adjacent pairs, with each
+intermediate value shared between consecutive comparisons:
+
+```
+a op1 b op2 c op3 d ≡ a op1 b && b op2 c && c op3 d
+```
+
+For example, `a <= b < c` is equivalent to `a <= b && b < c`.
+
+The supported operators are `<`, `<=`, `>`, `>=`, and `==`, and they may be mixed
+freely within a single chain.
diff --git a/source/docs/guide/src/reference-decreases-to.md b/source/docs/guide/src/reference-decreases-to.md
index d35c36c803..bcebde8950 100644
--- a/source/docs/guide/src/reference-decreases-to.md
+++ b/source/docs/guide/src/reference-decreases-to.md
@@ -13,7 +13,18 @@ is used to check the `decreases` measure for spec functions.
See [this tutorial chapter](./lex_mutual.md) for an introductory discussion of
lexicographic-decreases.
-## Definition
+### Syntax
+
+```verus-grammar
+V@[decreases_to_expr] ::= decreases_to!( V@[spec_expr] (, V@[spec_expr])* => V@[spec_expr] (, V@[spec_expr])* )
+```
+
+### Typing
+
+The two expression lists on either side of `=>` must have the same number of items.
+There are no other typing requirements.
+
+### Semantics
We say that
e1, e2, ..., en
diff --git a/source/docs/guide/src/reference-decreases.md b/source/docs/guide/src/reference-decreases.md
index 02bf3c3090..b385759086 100644
--- a/source/docs/guide/src/reference-decreases.md
+++ b/source/docs/guide/src/reference-decreases.md
@@ -13,10 +13,9 @@ A function is _recursive_ if it is in some mutually recursive collection.
A recursive spec function is required to supply a `decreases` clause, which takes
the form:
-```rust
-decreases EXPR_1, ...
- [ when BOOL_EXPR ]?
- [ via FUNCTION_NAME ]?
+```verus-grammar
+V@[spec_decreases_clause] ::=
+ decreases V@[spec_expr],+ ( when V@[spec_expr] )? ( via R@[function_ident] )?
```
The sequence of expressions in the decreases clause is the _decreases-measure_.
diff --git a/source/docs/guide/src/reference-exec-signature.md b/source/docs/guide/src/reference-exec-signature.md
index b66981e78a..54f00ab144 100644
--- a/source/docs/guide/src/reference-exec-signature.md
+++ b/source/docs/guide/src/reference-exec-signature.md
@@ -2,37 +2,38 @@
The general form of an `exec` function signature takes the form:
-
-fn function_name generics?(args...) -> return_type_and_name?
- where_clause?
- requires_clause?
- ensures_clause?
- returns_clause?
- invariants_clause?
- unwind_clause?
-
-
+```verus-grammar
+V@[exec_fn_item] ::=
+ R@[visibility]? exec? fn R@[function_name] R@[generics]?(R@[args...]) ( -> V@[exec_return_type] )?
+ R@[where_clause]?
+ V@[requires_clause]?
+ V@[ensures_clause]?
+ V@[returns_clause]?
+ V@[invariants_clause]?
+ V@[unwind_clause]?
+
+V@[exec_return_type] ::= V@[exec_return_type_named] | V@[exec_return_type_anon]
+V@[exec_return_type_named] ::= ( R@[pattern] : R@[type] )
+V@[exec_return_type_anon] ::= R@[type]
+```
## Function specification
The elements of the function specification are given by the signature clauses.
**The precondition.**
-The requires_clause is the precondition.
+The V@[requires_clause] is the precondition.
**The postcondition.**
-The ensures_clause
-and the
-returns_clause
-together form the postcondition.
+The V@[ensures_clause] and the V@[returns_clause] together form the postcondition.
**The invariants.**
-The invariants_clause specifies what invariants can be opened by the function.
+The V@[invariants_clause] specifies what invariants can be opened by the function.
For exec functions, the default is `open_invariants any`.
See [this page](./reference-opens-invariants.md) for more details.
**Unwinding.**
-The unwind_clause specifies whether the function might exit "abnormally" by unwinding,
+The V@[unwind_clause] specifies whether the function might exit "abnormally" by unwinding,
and under what conditions that can happen.
See [this page](./reference-unwind-sig.md) for more details.
diff --git a/source/docs/guide/src/reference-global.md b/source/docs/guide/src/reference-global.md
index a0b5c503f3..b7f3b14db1 100644
--- a/source/docs/guide/src/reference-global.md
+++ b/source/docs/guide/src/reference-global.md
@@ -14,13 +14,15 @@ This information can be provided to Verus as needed using the `global` directive
For a type `T`, and integer literals `n` or `m`, the `global` directive is a Verus item
that takes the form:
-```rust
-global layout T is size == n, align == m;
+```verus-grammar
+V@[global_item] ::= global layout R@[T:type] is size == R@[n:int_literal], align == R@[m:int_literal]
+ | global layout R@[T:type] is size == R@[n:int_literal]
+ | global layout R@[T:type] is align == R@[m:int_literal]
```
-Either `size` or `align` may be omitted. The global directive both:
+The global directive both:
- * Exports the axioms `size_of::() == n` and `align_of:: == m` for use in Verus proofs
+ * Exports one or both of the axioms `size_of::() == n` and `align_of:: == m` for use in Verus proofs
* Creates a "static" check ensuring the given values are actually correct when compiled.
Note that the second check _only_ happens when codegen is run; an "ordinary" verification pass will
diff --git a/source/docs/guide/src/reference-has.md b/source/docs/guide/src/reference-has.md
new file mode 100644
index 0000000000..bf1c5b9d9d
--- /dev/null
+++ b/source/docs/guide/src/reference-has.md
@@ -0,0 +1,21 @@
+# The `has` operator
+
+### Syntax
+
+```verus-grammar
+V@[has_expr] ::= V@[spec_expr] has V@[spec_expr]
+ | V@[spec_expr] !has V@[spec_expr]
+```
+
+### Desugaring
+
+In spec code, the expression `expr1 has expr2` desguars to `expr1.spec_has(expr2)`, which is resolved as normal via Rust's [method resolution](https://doc.rust-lang.org/reference/expressions/method-call-expr.html).
+
+Likewise, the expression `expr1 !has expr2` desugars to `!expr1.spec_has(expr2)`.
+
+### Use cases
+
+For example:
+
+ * [`spec_has` for a `Set`](https://verus-lang.github.io/verus/verusdoc/vstd/set/struct.Set.html#method.spec_has)
+ * [`spec_has` for a `Multiset`](https://verus-lang.github.io/verus/verusdoc/vstd/multiset/struct.Multiset.html#method.spec_has)
diff --git a/source/docs/guide/src/reference-implication.md b/source/docs/guide/src/reference-implication.md
index 3c806fcfef..9851966f3b 100644
--- a/source/docs/guide/src/reference-implication.md
+++ b/source/docs/guide/src/reference-implication.md
@@ -1,9 +1,33 @@
-# Implication (==>, <==, and <==>)
+# Implication (`==>`, `<==`, and `<==>`)
+### Syntax
-The operator `P ==> Q`, read _P implies Q_, is equivalent to `!P || Q`.
+```verus-grammar
+V@[implies_expr] ::= V@[spec_expr] ==> V@[spec_expr]
+V@[explies_expr] ::= V@[spec_expr] <== V@[spec_expr]
+V@[iff_expr] ::= V@[spec_expr] <==> V@[spec_expr]
+```
-This can also be written backwards: `Q <== P` is equivalent to `P ==> Q`.
+### Typing
-Finally, `P <==> Q` is equivalent to `P == Q`. It is sometimes useful for readability,
-and because `<==>` has the same syntactic precedence as `==>`
-rather than the precedence of `==`.
+All three operators require both sides to have type `bool` and return `bool`.
+
+### Semantics
+
+`P ==> Q`, read _P implies Q_, is `true` whenever `P` is `false` or `Q` is `true`:
+
+```
+P ==> Q ≡ !P || Q
+```
+
+`P <== Q` (_P is implied by Q_) is the converse: it is equivalent to `Q ==> P`. It is
+sometimes useful for readability when the consequent is more naturally written first.
+
+`P <==> Q` (_P if and only if Q_) is true when both sides have the same truth value:
+
+```
+P <==> Q ≡ P == Q
+```
+
+Note that `<==>` has the same syntactic [precedence](./spec-operator-precedence.md) as `==>`
+rather than the tighter precedence of `==`, so it can often be used without extra parentheses
+in contexts where `==` would require them.
diff --git a/source/docs/guide/src/reference-is.md b/source/docs/guide/src/reference-is.md
new file mode 100644
index 0000000000..0109be6678
--- /dev/null
+++ b/source/docs/guide/src/reference-is.md
@@ -0,0 +1,28 @@
+# The `is` operator
+
+### Syntax
+
+```verus-grammar
+V@[is_expr] ::= V@[spec_expr] is R@[ident]
+ | V@[spec_expr] !is R@[ident]
+```
+
+### Typing
+
+The left hand side should be an expression with some enum type, and the right hand side should
+be an (unqualified) identifier of a variant of that enum. The V@[is_expr] has type `bool`.
+
+### Semantics
+
+An `is` expression returns `true` if the left hand side matches the named variant.
+A `!is` expression returns the negation.
+
+### Example
+
+```rust
+fn test() {
+ let x = Some(5);
+ assert(x is Some);
+ assert(x !is None);
+}
+```
diff --git a/source/docs/guide/src/reference-matches.md b/source/docs/guide/src/reference-matches.md
new file mode 100644
index 0000000000..9caade4926
--- /dev/null
+++ b/source/docs/guide/src/reference-matches.md
@@ -0,0 +1,36 @@
+# The `matches` operator
+
+### Syntax
+
+```verus-grammar
+V@[matches_expr] ::= V@[spec_expr] matches R@[pattern] && V@[spec_expr]
+ | V@[spec_expr] matches R@[pattern] ==> V@[spec_expr]
+```
+
+### Typing
+
+The left-hand side should be of a type that matches the R@[pattern], while the right-hand
+side should have type `bool`.
+The right-hand side may reference variables bound by the pattern.
+
+The V@[matches_expr] as a whole has type `bool`.
+
+### Semantics
+
+The "matches-and" expression `expr matches pat && condition` is equivalent to:
+
+```rust
+match expr {
+ pat => condition,
+ _ => false,
+}
+```
+
+The "matches-implies" expression `expr matches pat ==> condition` is equivalent to:
+
+```rust
+match expr {
+ pat => condition,
+ _ => true,
+}
+```
diff --git a/source/docs/guide/src/reference-proof-signature.md b/source/docs/guide/src/reference-proof-signature.md
index fe21e858f1..e356b2f653 100644
--- a/source/docs/guide/src/reference-proof-signature.md
+++ b/source/docs/guide/src/reference-proof-signature.md
@@ -2,31 +2,49 @@
The general form of a `proof` function signature takes the form:
-
-proof fn function_name generics?(args...) -> return_type_and_name?
- where_clause?
- requires_clause?
- ensures_clause?
- returns_clause?
- invariants_clause?
-
-
+```verus-grammar
+V@[proof_fn_item] ::= V@[proof_fn_proved] | V@[proof_fn_axiom]
+
+V@[proof_fn_proved] ::=
+ R@[visibility]? broadcast? proof fn R@[function_name] R@[generics]?(R@[args...]) ( -> V@[proof_return_type] )?
+ R@[where_clause]?
+ V@[requires_clause]?
+ V@[ensures_clause]?
+ V@[returns_clause]?
+ V@[invariants_clause]?
+ V@[decreases_clause]?
+ { V@[proof_stmt]* }
+
+V@[proof_fn_axiom] ::=
+ R@[visibility]? broadcast? axiom fn R@[function_name] R@[generics]?(R@[args...]) ( -> V@[proof_return_type] )?
+ R@[where_clause]?
+ V@[requires_clause]?
+ V@[ensures_clause]?
+ V@[returns_clause]?
+ V@[invariants_clause]?
+ V@[decreases_clause]?
+ ;
+
+V@[proof_return_type] ::= V@[proof_return_type_named] | V@[proof_return_type_anon]
+V@[proof_return_type_named] ::= ( tracked? R@[pattern] : R@[type] )
+V@[proof_return_type_anon] ::= R@[type]
+```
## Function specification
The elements of the function specification are given by the signature clauses.
**The precondition.**
-The requires_clause is the precondition.
+The V@[requires_clause] is the precondition.
**The postcondition.**
-The ensures_clause
+The V@[ensures_clause]
and the
-returns_clause
+V@[returns_clause]
together form the postcondition.
**The invariants.**
-The invariants_clause specifies what invariants can be opened by the function.
+The V@[invariants_clause] specifies what invariants can be opened by the function.
For proof functions, the default is `open_invariants none`.
See [this page](./reference-opens-invariants.md) for more details.
diff --git a/source/docs/guide/src/reference-reveal-hide.md b/source/docs/guide/src/reference-reveal-hide.md
index 006416334c..fe77bc4477 100644
--- a/source/docs/guide/src/reference-reveal-hide.md
+++ b/source/docs/guide/src/reference-reveal-hide.md
@@ -1,5 +1,15 @@
# `reveal`, `reveal_with_fuel`, `hide`
+### Syntax
+
+```verus-grammar
+V@[reveal_stmt] ::= reveal ( R@[path] ) ;
+V@[reveal_with_fuel_stmt] ::= reveal_with_fuel ( R@[path] , R@[int_literal] ) ;
+V@[hide_stmt] ::= hide ( R@[path] ) ;
+```
+
+### Proof operation
+
These attributes control whether and how Verus will unfold the definition of a spec function
while solving. For a spec function `f`:
diff --git a/source/docs/guide/src/reference-reveal-strlit.md b/source/docs/guide/src/reference-reveal-strlit.md
new file mode 100644
index 0000000000..3e5b7d8405
--- /dev/null
+++ b/source/docs/guide/src/reference-reveal-strlit.md
@@ -0,0 +1,22 @@
+# `reveal_strlit`
+
+### Syntax
+
+```verus-grammar
+V@[reveal_strlit_stmt] ::= reveal_strlit ( R@[string_literal] ) ;
+```
+
+### Proof operation
+
+This reveals the contents of the string literal to the prover, including the length and
+the sequence of characters that compose the string.
+
+### Example
+
+```rust
+fn test() {
+ let s = "abc";
+ proof { reveal_strlit("abc"); }
+ assert(s@[0] == 'a');
+}
+```
diff --git a/source/docs/guide/src/reference-spec-index.md b/source/docs/guide/src/reference-spec-index.md
index d0bc924d68..55679361d7 100644
--- a/source/docs/guide/src/reference-spec-index.md
+++ b/source/docs/guide/src/reference-spec-index.md
@@ -1,11 +1,19 @@
# Spec index operator []
-In spec expressions, the index operator is treated differently than
-in exec expressions, where it corresponds to the [usual Rust index operator](https://doc.rust-lang.org/std/ops/trait.Index.html).
+### Syntax
-Specifically, in a spec expression, the expression `expr[i]` is a shorthand for
-`expr.spec_index(i)`. This is a purely syntactic transformation, and there is no
-particular trait.
+```verus-grammar
+V@[spec_index_expr] ::= V@[spec_expr] [ V@[spec_expr] ]
+```
+
+### Desugaring
+
+In spec code, the expression `expr[i]` desguars to `expr.spec_index(i)`, which is resolved as normal via Rust's [method resolution](https://doc.rust-lang.org/reference/expressions/method-call-expr.html).
+
+> **Note:** This is different than the index operator in executable code,
+> where it is either a [place expression](https://doc.rust-lang.org/reference/expressions.html#place-expressions-and-value-expressions) indexing into a slice or an array, or is overloaded via the [`Index`](https://doc.rust-lang.org/std/ops/trait.Index.html) or [`IndexMut`](https://doc.rust-lang.org/std/ops/trait.IndexMut.html) traits.
+
+### Use cases
For example:
diff --git a/source/docs/guide/src/reference-spec-signature.md b/source/docs/guide/src/reference-spec-signature.md
index 69c0cdc463..2b084656b3 100644
--- a/source/docs/guide/src/reference-spec-signature.md
+++ b/source/docs/guide/src/reference-spec-signature.md
@@ -2,13 +2,17 @@
The general form of a `spec` function signature takes the form:
-
-spec fn function_name generics?(args...) -> return_type?
- where_clause?
- recommends_clause?
- decreases_clause?
-
-
+```verus-grammar
+V@[spec_fn_item] ::=
+ R@[visibility]? uninterp? V@[openness]? spec fn R@[function_name] R@[generics]?(R@[args...]) -> R@[type]
+ R@[where_clause]?
+ V@[recommends_clause]?
+ V@[spec_decreases_clause]?
+
+V@[openness] ::= closed
+ | open
+ | open ( R@[visibility] )
+```
## The `recommends` clause
@@ -25,3 +29,27 @@ to the domain.
See [the reference page for `decreases`](./reference-decreases.md) for more information,
or see [the guide page on recursive functions](./recursion.md) for motivation and overview.
+
+## The openness clause
+
+Openness defines the visibility of the body, which may be more restricted than the visibility
+of the function name. Specifically:
+
+ * `open` means the body is visible everywhere, to all crates.
+ * open(R@[visibility]) means the body is visible to the given visibility specifier.
+ * e.g., `open(crate)`, `open(self)`, `open(super)`, `open(in some::module::path)`
+ * `closed` means the body is visible only to module where the function is defined, i.e., it is equivalent to `open(self)`.
+
+The openness specifier is required whenever the body is given.
+
+## The `uninterp` specifier
+
+The `uninterp` specifier declares the function as _uninterpreted_, meaning the body of the
+spec function is not given.
+
+> **Note.** Uninterpreted functions are usually not useful unless they are used
+> in combination with axioms that define the properties of the function. A common use case
+> for an interpreted function is to define the spec interpretation of a type from a
+> trusted (i.e., unverified) library.
+>
+> Do note, however, that `uninterp` functions are always sound to _declare_.
diff --git a/source/docs/guide/src/reference-types.md b/source/docs/guide/src/reference-types.md
new file mode 100644
index 0000000000..91a1172dbe
--- /dev/null
+++ b/source/docs/guide/src/reference-types.md
@@ -0,0 +1,247 @@
+# Mathematical interpretations of types
+
+## Integer types
+
+Verus integer types include the standard Rust primitive types (`u8`, `u16`, `u32`, `u64`, `u128`, `usize`, `i8`, `i16`, `i132`, `i64`, `i128`, and `isize`) together with Verus builtin types
+`int` and `nat`.
+
+**Mathematical interpretation.**
+Every integer type is represented as an integer (i.e., an element of ℤ) together with a range of accepted values:
+
+| Type | Bound |
+|---------|-------|
+| `int` | `(-∞, ∞)` (i.e., no bound) |
+| `nat` | `[0, ∞)` |
+| `uN` | [0, 2N) |
+| `iN` | [-2N-1, 2N-1) |
+| `usize` | [0, 2usize::BITS) |
+| `isize` | [-2isize::BITS-1, 2isize::BITS-1) |
+
+For `isize` and `usize`, assumptions of the platform word size (`usize::BITS`, or equivalently, `isize::BITS`) is configurable
+via the [`global` directive](http://localhost:3000/reference-global.html#with-usize-and-isize).
+
+**Spec equality.** Spec equality on integers is defined as integer equality.
+
+**Literal expressions**
+Spec code accepts integer literals both for standard types (`u8`, `i8`, etc.) and Verus-specific types (`nat` and `int`).
+Types are inferred for bare literals, but the types may be made explicit (e.g., `1u8` or `1nat`).
+
+**Spec operators**
+
+* Integer types are inter-covertible using [`as`-casts](./reference-as.md).
+* Verus supports [standard arithmetic operators](./spec-arithmetic.md).
+* Verus supports [bit arithmetic operators](./spec-bit-ops.md).
+
+## Bool
+
+**Mathematical interpretation.**
+A `bool` is represented by a standard boolean value, `true` or `false`.
+
+**Spec equality.** Spec equality on `bool` is defined by standard boolean equivalence.
+
+**Literal expressions.** Both `true` and `false` are valid literals.
+
+**Spec operators.**
+Besides the standard `&&` and `||`, Verus supports some additional boolean operators that are
+standard in logic, including [`implication and equivalence`](./reference-implication.md) (`==>`, `<==` and `<==>`) and [low-predence variations](./prefix-and-or.md) of conjunctions and disjunction.
+
+
+## Char
+
+**Mathematical interpreation.**
+A `char` is interpreted as an [integer type](#integer-types) with a bespoke validity range:
+
+| Type | Bound |
+|---------|-------|
+| `int` | `[0, 0xD7ff] ∪ [0xE000, 0x10FFFF]` |
+
+This is consistent with the
+[Rust definition of a `char`](https://doc.rust-lang.org/std/primitive.char.html)
+as a "Unicode scalar value":
+
+> A char is a ‘[Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value)’, which is any ‘[Unicode code point](https://www.unicode.org/glossary/#code_point)’ other than a [surrogate code point](https://www.unicode.org/glossary/#surrogate_code_point). This has a fixed numerical definition: code points are in the range 0 to 0x10FFFF, inclusive. Surrogate code points, used by UTF-16, are in the range 0xD800 to 0xDFFF.
+
+**Spec equality.** For `char`, spec equality is defined as integer equality.
+
+**Literal expressions.** Standard [`char` literals](https://doc.rust-lang.org/reference/tokens.html#character-literals) are accepted in spec code.
+
+**Spec operators.** In spec code, a `char` is inter-covertible with the integer types using [`as`-casts](./reference-as.md).
+This is more
+permissive than exec code, which disallows many of these coercions.
+As with other coercions, the result may be undefined if the integer being coerced does not
+fit in the target range.
+
+## Box (`Box`)
+
+**Mathematical interpretation.**
+A `Box` is interpreted identically to `T` with no additional metadata.
+
+**Spec equality.**
+Spec equality on `Box` is inherited from spec equality on `T`.
+
+**Spec operators.**
+Boxing operations `Box::new` and unboxing operations (`*x`) are semantically the identity function.
+
+## Shared reference (`&T`)
+
+**Mathematical interpretation.**
+A `&T` is interpreted identically to `T` with no additional metadata.
+
+**Spec equality.**
+Spec equality on `&T` is inherited from spec equality on `T`.
+
+**Spec operators.**
+Borrowing operations `&x` and dereferencing operations (`*x`) are semantically the identity function.
+
+## Mutable reference (`&mut T`)
+
+Our encoding for mutable references is based on the [RustHorn encoding](https://dl.acm.org/doi/10.1145/3462205).
+See [the guide page](./mutable-references.md)
+for practical information on using mutable references.
+
+> **Note:** Verus used to treat mutable references very differently before 2026-05-03 release.
+> See [the migration guide](https://github.com/verus-lang/verus/blob/main/source/docs/migration-mut-ref.md) for more information about the transition.
+
+
+**Mathematical interpretation.**
+A `&mut T` is interpreted as an abstract type.
+It is guaranteed to be compatible with a surjective function `(&mut T) -> (T, *mut T, BorrowId)`.
+At this time, there is no built-in support for explicitly reasoning about the pointer or about the "BorrowId".
+
+**Spec equality.**
+There is no extensional notion of equality for mutable references, and there is currently
+no way to prove equality except via basic reflexivity.
+
+This means that even if two mutables have the same current value, final value, and address,
+they are not necessarily equal. In particular, a reborrow is not equal to the mutable borrow
+it is borrowed from.
+For two references to compare equal, they must originate from the same borrow instruction.
+
+```rust
+fn example() {
+ let mut a = 0;
+ let mut b = 0;
+
+ let a_ref1 = &mut a;
+ let a_ref2 = &mut a;
+
+ assert(a_ref1 == a_ref1); // ok, basic reflexivity
+ assert(a_ref1 == a_ref2); // not ok; these originate from different borrows
+}
+```
+
+However, it is still not sufficient for two mutable references to originate from
+the same point. Two snapshots taken at different times will compare unequal if
+the mutable reference was updated in between:
+
+```rust
+fn example2() {
+ let mut a = 0;
+ let a_ref = &mut a;
+
+ let ghost snapshot1 = a_ref;
+ let ghost snapshot2 = a_ref;
+
+ *a_ref = 30;
+
+ let ghost snapshot3 = a_ref;
+
+ assert(snapshot1 == snapshot2); // ok, a_ref is unchanged between the two snapshots
+ assert(snapshot1 == snapshot3); // not ok, a_ref was changed between the two snapshots
+}
+```
+
+> **Note:** Equality of mutable references in spec code is not the same as equality of mutable references in exec code. In exec code, equality on mutable references is defined by equality on the referred-to values.
+
+**Spec operators.**
+In spec code, one reasons about a mutable reference `x: &mut T` through two key values:
+
+ * `*x`: the current value behind the mutable reference.
+ * `*final(x)`: the final value the mutable reference will point to when it expires.
+ This value is considered [prophetic](./reference-attributes.md#verifierprophetic).
+
+> **Note:** In postconditions, you may be required to write `*old(x)` instead of `*x`
+> where `x: &mut T` is an input to the function.
+> This has no meaning at a formal level;
+> it is only used to prevent user confusion regarding which value `*x` refers to.
+
+**Additional notes.**
+
+> **Note:** Verus does not insert "implicit reborrows" for spec-mode uses of a mutable reference.
+
+> **Note:** Through spec-snapshots, it is possible to create self-referential mutable references
+> via the `final` operator.
+>
+> ```rust
+> struct Rec {
+> g: Option>,
+> }
+>
+> fn test() {
+> let mut r = Rec { g: None };
+>
+> let mut r_ref = &mut r;
+> *r_ref = Rec { g: Some(Ghost(r_ref)) };
+>
+> assert(r.g.is_some());
+> assert(r == *final(r.g.unwrap()@)); // cycle
+> }
+> ```
+>
+> As a result, Verus does not treat *final(x) as a subfield of `x` for the purposes of
+> [decreases-to](./reference-decreases-to.md), i.e., recursion through the `final` value is
+> not considered to be well-founded recursion.
+
+## Raw Pointer (`*const T` and `*mut T`)
+
+This page only discusses the raw pointer types.
+See the [`raw_ptr`](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/index.html) vstd librararies for practical information on reasoning with pointers.
+
+**Mathematical interpretation.**
+In spec code, a pointer `ptr: *mut T` or `ptr: *const T` is defined as a triple of three
+pieces of data:
+
+ * `ptr.addr()` of type `usize`: The address of the pointer
+ * `ptr@.metadata` of type [`::Metadata`](https://doc.rust-lang.org/std/ptr/trait.Pointee.html)
+ * `ptr@.provenance` of abstract type [`Provenance`](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/struct.Provenance.html)
+
+> **Note:** Verus treats `*const T` and `*mut T` identically. Though they differ
+> in [variance](https://doc.rust-lang.org/reference/subtyping.html?#variance), this does
+> not impact their mathematical, spec-level interpretation.
+> Casting `*const T` to `*mut T` and vice versa is semantically a no-op.
+
+**Spec equality.**
+Two pointers are equal if the address, metadata, and provenance are equal.
+
+> **Note:** Equality of pointers in spec code is not the same as equality of pointers in exec code.
+> Exec comparisons only compare the address and metadata, while spec comparisons also compare provenance.
+
+**Spec operators.**
+
+ * `ptr.addr()`, `ptr@.metadata`, and `ptr@.provenance` can be used to obtain the constituent parts of a tuple.
+ * [`ptr_from_data`](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/fn.ptr_from_data.html) can be used to build a pointer from its constituent parts.
+
+## `String` and `str`
+
+**Mathematical interpretation.**
+`String` and `str` are each represented as an abstract type.
+It is guaranteed that this type is consistent with a surjective `view` function
+to Seq<char>.
+
+> **Note:** In Rust, it is possible to obtain a `str` whose bytes do not form a valid UTF-8
+> encoding, using, e.g., [`from_utf8_unchecked`](https://doc.rust-lang.org/std/string/struct.String.html#method.from_utf8_unchecked) or [`as_bytes_mut`](https://doc.rust-lang.org/std/string/struct.String.html#method.as_bytes_mut), though such functions are unsafe, and creating ill-formed strings can easily lead to UB. Verus does not currently support ill-formed strings, and thus `String`/`str` values are assumed to contain valid UTF-8.
+
+**Spec equality.**
+`String` and `str` do not exhibit extensional equality. To reason about equality, always
+use the `view` function.
+
+**Literal expressions.**
+Verus supports [string literal expressions](https://doc.rust-lang.org/reference/tokens.html#grammar-STRING_LITERAL) in spec code.
+
+> **Note:** The contents of string literals are opaque to the prover by default. Use [`reveal_strlit`](./reference-reveal-strlit.md) to expose the contents of a string literal.
+
+**Spec operators.**
+
+The primary spec operator for strings is the "view" operator, `s@` or `s.view()`.
+
+
diff --git a/source/docs/guide/src/reference-unions.md b/source/docs/guide/src/reference-unions.md
index 5b323d7d08..3dd7f72a36 100644
--- a/source/docs/guide/src/reference-unions.md
+++ b/source/docs/guide/src/reference-unions.md
@@ -10,7 +10,7 @@ i.e., it checks that `u` is the correct "variant".
In spec-mode, you can use the built-in spec operators `is_variant` and `get_union_field`
to reason about a union. Both operators refer to the field name via _string literals_.
- * `is_variant(u, "field_name")` returns true if `u` is in the `"field_name"` variant.
+ * `is_variant(u, "field_name")` returns true if `u` has a well-formed field `"field_name"`.
* `get_union_field::(u, "field_name")` returns a value of type `T`, where
`T` is the type of `"field_name"`. (Verus will error if `T` does not match between
the union and the generic parameter `T` of the operator.)
diff --git a/source/docs/guide/src/spec-arithmetic.md b/source/docs/guide/src/spec-arithmetic.md
index 75ba5aa0a6..fcf0cf9463 100644
--- a/source/docs/guide/src/spec-arithmetic.md
+++ b/source/docs/guide/src/spec-arithmetic.md
@@ -6,7 +6,23 @@ This page is **does not apply** to arithmetic is _executable Rust code_.
For an introduction to Verus arithmetic, see
[Integers and arithmetic](./integers.md).
-## Type widening
+### Syntax
+
+```verus-grammar
+V@[arith_expr] ::= V@[spec_expr] \+ V@[spec_expr]
+ | V@[spec_expr] - V@[spec_expr]
+ | - V@[spec_expr]
+ | V@[spec_expr] \* V@[spec_expr]
+ | V@[spec_expr] / V@[spec_expr]
+ | V@[spec_expr] % V@[spec_expr]
+
+V@[ineq_expr] ::= | V@[spec_expr] <= V@[spec_expr]
+ | V@[spec_expr] < V@[spec_expr]
+ | V@[spec_expr] >= V@[spec_expr]
+ | V@[spec_expr] > V@[spec_expr]
+```
+
+### Typing
In spec code, the results of arithmetic are automatically widened to avoid overflow or wrapping.
The types of various operators, given as functions of the input types, are summarized in
@@ -16,7 +32,6 @@ Note that in most cases, the types of the inputs are not required to be the same
| operation | LHS type | RHS type | result type | notes |
|-----------|---------------------|----------------------|-------------|----------------------|
| `<=` `<` `>=` `>` | t1 | t2 | bool | |
-| `==` `!=` | t1 | t2 | bool | |
| `+` | t1 | t2 | int | except for nat + nat |
| `+` | nat | nat | nat | |
| `-` | t1 | t2 | int | |
@@ -28,11 +43,14 @@ Note that in most cases, the types of the inputs are not required to be the same
| `add(_, _)` | t | t | t | |
| `sub(_, _)` | t | t | t | |
| `mul(_, _)` | t | t | t | |
-| `&` | `^` | t | t | t | |
-| `<<` `>>` | t1 | t2 | t1 | |
-## Definitions: Quotient and remainder
+### Semantics
+Due to type-widening, the result of any arithmetic operator is the exact result of the arithmetic
+without any consideration for overflow or truncation, with the exception of the named
+`add`, `sub`, and `mul` operators, which truncate.
+
+**Quotient and remainder.**
In Verus specifications, `/` and `%` are defined by [Euclidean division](https://en.wikipedia.org/wiki/Euclidean_division). Euclidean division may differ from the usual Rust `/` and `%` operators
when operands are negative.
@@ -59,7 +77,3 @@ usable in spec expressions:
* Exponentiation ([`vstd::arithmetic::power::pow`](https://verus-lang.github.io/verus/verusdoc/vstd/arithmetic/power/fn.pow.html))
* Power of two ([`vstd::arithmetic::power2::pow2`](https://verus-lang.github.io/verus/verusdoc/vstd/arithmetic/power2/fn.pow2.html))
* Integer logarithm ([`vstd::arithmetic::logarithm::log`](https://verus-lang.github.io/verus/verusdoc/vstd/arithmetic/logarithm/fn.log.html))
-
-## Bitwise ops
-
-See [bitwise operators](./spec-bit-ops.md).
diff --git a/source/docs/guide/src/spec-bit-ops.md b/source/docs/guide/src/spec-bit-ops.md
index 7b327fb1d5..b143f7405b 100644
--- a/source/docs/guide/src/spec-bit-ops.md
+++ b/source/docs/guide/src/spec-bit-ops.md
@@ -1,8 +1,25 @@
# Bit operators
-## Definitions
+### Syntax
-### `&`, `|`, and `^`
+```verus-grammar
+V@[bit_expr] ::= V@[spec_expr] & V@[spec_expr]
+ | V@[spec_expr] | V@[spec_expr]
+ | V@[spec_expr] ^ V@[spec_expr]
+ | V@[spec_expr] << V@[spec_expr]
+ | V@[spec_expr] >> V@[spec_expr]
+```
+
+### Typing
+
+| operation | LHS type | RHS type | result type |
+|-----------|---------------------|----------------------|---------------|
+| `&` | `^` | t | t | t |
+| `<<` `>>` | t1 | t2 | t1 |
+
+### Semantics
+
+**`&`, `|`, and `^`**.
These have the usual meaning: bitwise-OR, bitwise-AND, and bitwise-XOR. Verus, like Rust, requires the input operands to be the same
type, even in specification code.
@@ -12,7 +29,7 @@ these operations are independent of bitwidth.
This is true even for negative operands, as a result of the way two's complement
[sign-extension](https://en.wikipedia.org/wiki/Sign_extension) works.
-### `>>` and `<<`
+**`>>` and `<<`**.
Verus specifications, like Rust, does not require the left and right sides of a _shift_ operator
to be the same type. Shift is unspecified when the right-hand side is negative.
diff --git a/source/docs/guide/src/spec-choose.md b/source/docs/guide/src/spec-choose.md
index 2a8fb396b4..4154fd5147 100644
--- a/source/docs/guide/src/spec-choose.md
+++ b/source/docs/guide/src/spec-choose.md
@@ -1,3 +1,56 @@
# Such that (`choose`)
-The such-that operator (`choose`) is explained in [exists and choose](exists.md).
+For an intuition-guided introduction, see [exists and choose](exists.md).
+
+`choose` is a **spec-mode only** expression that returns an arbitrary value satisfying
+a given predicate. It is the Hilbert choice operator (also known as the epsilon operator or
+[such-that operator](https://en.wikipedia.org/wiki/Epsilon_calculus)).
+
+### Syntax
+
+```verus-grammar
+V@[choose_expr] ::= choose |R@[binders...]| V@[spec_expr]
+```
+
+The body V@[spec_expr] may include [trigger annotations](./trigger-annotations.md).
+
+### Typing
+
+The body V@[spec_expr] must have type `bool`. The bound variables are available as spec-mode
+variables within the body. The return type depends on the number of binders:
+
+ * For a single binder `x: T`, the expression has type `T`.
+ * For multiple binders `x: T, y: U, ...`, the expression has tuple type `(T, U, ...)`.
+
+### Semantics
+
+`choose|x: T| P(x)` evaluates to some value of type `T`:
+
+- If there exists a value `x` of type `T` such that `P(x)` is `true`, `choose` returns one
+ such value. The choice is deterministic: the same expression always returns the same value.
+- If no such value exists, `choose` returns an arbitrary value of type `T` with no guarantee
+ that `P` holds of it.
+
+To use the result with the guarantee that `P` holds, you must separately establish
+`exists|x: T| P(x)`. Verus will then allow you to conclude `P(choose|x: T| P(x))`.
+
+`choose` and `exists` are complementary: `exists|x: T| P(x)` asserts that a satisfying value
+*exists*, while `choose|x: T| P(x)` *extracts* one. Triggers on `choose` work the same way
+as on `exists`; see [Trigger annotations](./trigger-annotations.md) for details.
+
+**Example:**
+
+```rust
+// Requires a proof that such an i exists; choose picks one.
+proof fn get_zero_index(s: Seq) -> (i: int)
+ requires exists|i: int| 0 <= i < s.len() && s[i] == 0,
+ ensures 0 <= i < s.len() && s[i] == 0,
+{
+ choose|i: int| 0 <= i < s.len() && s[i] == 0
+}
+```
+
+```rust
+// Multiple variables — result is a tuple.
+let (i, j): (int, int) = choose|i: int, j: int| less_than(i, j);
+```
diff --git a/source/docs/guide/src/spec-equality.md b/source/docs/guide/src/spec-equality.md
index 0c8a9cfd34..c525e7da8b 100644
--- a/source/docs/guide/src/spec-equality.md
+++ b/source/docs/guide/src/spec-equality.md
@@ -1,3 +1,27 @@
# Spec equality (`==`)
-The spec equality operator `==` is explained in [Equality](./equality.md).
+> **Note:** In spec mode, `==` is mathematical equality — it is not the same as `==` in exec code,
+which dispatches to the [`PartialEq`](https://doc.rust-lang.org/std/cmp/trait.PartialEq.html) trait.
+
+For an introduction, see [Equality](./equality.md).
+
+### Syntax
+
+```verus-grammar
+V@[equality_expr] ::= V@[spec_expr] == V@[spec_expr]
+ | V@[spec_expr] != V@[spec_expr]
+```
+
+### Typing
+
+The expression is well-typed if both the left-hand side and right-hand side have the same type.
+
+In some cases, Verus may accept `==` as well-typed when both sides have the same
+[mathematical interpretation](./spec-types.md). For example:
+
+ * Two [integer types](./reference-types.md#integer-types) can always be compared.
+ * `T` can be compared to `&T`.
+
+### Semantics
+
+The `==` operator returns `true` iff the two sides are equivalent in their [mathematical interpretation](./spec-types.md). The `!=` operator is the negation.
diff --git a/source/docs/guide/src/spec-expressions.md b/source/docs/guide/src/spec-expressions.md
index aa8968ea07..8ec15d2d04 100644
--- a/source/docs/guide/src/spec-expressions.md
+++ b/source/docs/guide/src/spec-expressions.md
@@ -2,3 +2,43 @@
Many built-in operators are in spec mode, i.e., they can be used in
specification expressions. This section discusses those operators.
+
+## Syntax
+
+```verus-grammar
+V@[spec_expr] ::= V@[fn_call_expr]
+ | V@[and_expr]
+ | V@[or_expr]
+ | V@[not_expr]
+ | V@[if_expr]
+ | V@[if_let_expr]
+ | V@[match_expr]
+ | V@[spec_block_expr]
+ | V@[as_expr]
+ | V@[box_new_expr]
+ | V@[ref_expr]
+ | V@[deref_expr]
+ | V@[chained_expr]
+ | V@[implies_expr]
+ | V@[explies_expr]
+ | V@[iff_expr]
+ | V@[arith_expr]
+ | V@[ineq_expr]
+ | V@[bit_expr]
+ | V@[equality_expr]
+ | V@[ext_eq_expr]
+ | V@[prefix_and_expr]
+ | V@[prefix_or_expr]
+ | V@[forall_expr]
+ | V@[exists_expr]
+ | V@[choose_expr]
+ | V@[root_trigger_attr_expr]
+ | V@[inner_trigger_attr_expr]
+ | V@[view_expr]
+ | V@[spec_index_expr]
+ | V@[has_expr]
+ | V@[is_expr]
+ | V@[matches_expr]
+ | V@[decreases_to_expr]
+ | ( V@[spec_expr] )
+```
diff --git a/source/docs/guide/src/spec-operator-precedence.md b/source/docs/guide/src/spec-operator-precedence.md
index e1d177bc9e..2ff85462a1 100644
--- a/source/docs/guide/src/spec-operator-precedence.md
+++ b/source/docs/guide/src/spec-operator-precedence.md
@@ -1,28 +1,30 @@
# Operator Precedence
-| Operator | Associativity |
-|--------------------------|-----------------------|
-| **Binds tighter** |
-| [`.` `->`](./datatypes_struct.md) | left |
-| [`is` `matches`](./datatypes_enum.md) | left |
-| [`*` `/` `%`](./spec-arithmetic.md) | left |
-| [`+` `-`](./spec-arithmetic.md) | left |
-| [`<<` `>>`](./spec-bit-ops.md) | left |
-| [`&`](./spec-bit-ops.md) | left |
-| [`^`](./spec-bit-ops.md) | left |
-| [|](./spec-bit-ops.md) | left |
-| [`!==` `==` `!=`](./spec-equality.md) `<=` `<` `>=` `>` | requires parentheses |
-| `&&` | left |
-| || | left |
-| [`==>`](./reference-implication.md) | right |
-| [`<==`](./reference-implication.md) | left |
-| [`<==>`](./reference-implication.md) | requires parentheses |
-| `..` | left |
-| `=` | right |
-| closures; [`forall`, `exists`](./spec-quantifiers.md); [`choose`](./spec-choose.md) | right |
-| [`&&&`](./prefix-and-or.md) | left |
-| [|||](./prefix-and-or.md) | left |
-| **Binds looser** |
+The table below defines operator precedence from tightest-binding (top) to loosest-binding (bottom).
+
+| Operator | Associativity | Grammar |
+|--------------------------------------------------------------------------------------|----------------------|---------------------------------------------------------|
+| **Binds tighter** | | |
+| [`.` `->`](./datatypes_struct.md) | left | |
+| `has`, [`is`, `matches`](./datatypes_enum.md) | left | V@[has_expr] V@[is_expr] V@[matches_expr] |
+| [`*` `/` `%`](./spec-arithmetic.md) | left | V@[arith_expr] |
+| [`+` `-`](./spec-arithmetic.md) | left | V@[arith_expr] |
+| [`<<` `>>`](./spec-bit-ops.md) | left | V@[bit_expr] |
+| [`&`](./spec-bit-ops.md) | left | V@[bit_expr] |
+| [`^`](./spec-bit-ops.md) | left | V@[bit_expr] |
+| [|](./spec-bit-ops.md) | left | V@[bit_expr] |
+| [`!==` `==` `!=`](./spec-equality.md) `<=` `<` `>=` `>` | requires parentheses | V@[equality_expr] V@[ineq_expr] |
+| `&&` | left | V@[and_expr] |
+| || | left | V@[or_expr] |
+| [`==>`](./reference-implication.md) | right | V@[implies_expr] |
+| [`<==`](./reference-implication.md) | left | V@[explies_expr] |
+| [`<==>`](./reference-implication.md) | requires parentheses | V@[iff_expr] |
+| `..` | left | |
+| `=` | right | |
+| closures; [`forall`, `exists`](./spec-quantifiers.md); [`choose`](./spec-choose.md) | right | V@[forall_expr] V@[exists_expr] V@[choose_expr] |
+| [`&&&`](./prefix-and-or.md) | left | V@[prefix_and_expr] |
+| [|||](./prefix-and-or.md) | left | V@[prefix_or_expr] |
+| **Binds looser** | | |
All operators that are from ordinary Rust have the same precedence-ordering as in
ordinary Rust.
diff --git a/source/docs/guide/src/spec-quantifiers.md b/source/docs/guide/src/spec-quantifiers.md
index 72d21547b6..d2278f4e33 100644
--- a/source/docs/guide/src/spec-quantifiers.md
+++ b/source/docs/guide/src/spec-quantifiers.md
@@ -1,6 +1,61 @@
# Spec quantifiers (`forall`, `exists`)
-Quantifiers are explained in the [Quantifiers](quants.md) part of the
-tutorial. Specifically, `forall` is explained in [forall and
-triggers](forall.md) and `exists` is explained in [exists and
-choose](exists.md).
+For an intuition-guided introduction to quantifiers and triggers, see the
+[Quantifiers](quants.md) tutorial, specifically [forall and triggers](forall.md)
+and [exists and choose](exists.md).
+
+Both `forall` and `exists` are **spec-mode only** expressions.
+
+### Syntax
+
+```verus-grammar
+V@[forall_expr] ::= forall |R@[binders...]| V@[spec_expr]
+V@[exists_expr] ::= exists |R@[binders...]| V@[spec_expr]
+```
+
+The body V@[spec_expr] may include [trigger annotations](./trigger-annotations.md).
+
+### Typing
+
+The body V@[spec_expr] must have type `bool`. The bound variables are available as spec-mode
+variables within the body. Both `forall` and `exists` expressions have type `bool`.
+
+### Semantics
+
+`forall|x: T| P(x)` is `true` if and only if `P(x)` is `true` for every value `x` of type `T`.
+
+`exists|x: T| P(x)` is `true` if and only if there exists at least one value `x` of type `T`
+such that `P(x)` is `true`. The two are duals, and because Verus uses classical logic:
+
+```
+exists|x: T| P(x) ≡ !forall|x: T| !P(x)
+```
+
+Both quantifiers support binding multiple variables simultaneously, which is equivalent to
+nesting single-variable quantifiers:
+
+```rust
+// These two are equivalent:
+forall|i: int, j: int| i < j ==> f(i) <= f(j)
+forall|i: int| forall|j: int| i < j ==> f(i) <= f(j)
+```
+
+### Triggers
+
+Because quantifiers range over infinite domains, the SMT solver does not enumerate all
+possible instantiations. Instead it uses *triggers*: syntactic patterns that, when matched
+by terms in the proof context, cause the quantifier to be instantiated with the matching values.
+
+Every quantifier must have at least one trigger group. Verus can choose triggers
+automatically, or they can be specified explicitly using annotations on the quantifier body:
+
+| Annotation | Meaning |
+|---|---|
+| `#[trigger]` on a sub-expression | That sub-expression is a trigger (grouped with other `#[trigger]` annotations) |
+| `#[trigger(n)]` on a sub-expression | That sub-expression is part of trigger group `n` |
+| `#![trigger expr1, expr2, ...]` at the root of the body | `expr1, expr2, ...` form a single trigger group |
+| `#![auto]` at the root of the body | Use automatic trigger selection and suppress the trigger-logging note |
+| `#![all_triggers]` at the root of the body | Use aggressive automatic trigger selection |
+
+For full details on how Verus selects and validates trigger groups, see
+[Trigger annotations](./trigger-annotations.md).
diff --git a/source/docs/guide/src/spec-rust-subset.md b/source/docs/guide/src/spec-rust-subset.md
index e27232c2b1..e3e03bd8c9 100644
--- a/source/docs/guide/src/spec-rust-subset.md
+++ b/source/docs/guide/src/spec-rust-subset.md
@@ -5,33 +5,87 @@ there are some subtle differences.
### Function calls
+**Syntax:**
+
+```verus-grammar
+V@[fn_call_expr] ::= R@[path] ( V@[spec_expr],* )
+```
+
Only pure function calls are allowed (i.e., calls to other `spec` functions or
functions marked with the `when_used_as_spec` directive).
### Let-assignment
+**Syntax:**
+
+```verus-grammar
+V@[spec_block_expr] ::= { V@[spec_let_stmt]* V@[spec_expr] }
+V@[spec_let_stmt] ::= let R@[pattern] = V@[spec_expr];
+```
+
Spec expressions support `let`-bindings, but not `let mut`-bindings.
### if / if let / match statements
+**Syntax:**
+
+```verus-grammar
+V@[if_expr] ::= if V@[spec_expr] { V@[spec_expr] } else { V@[spec_expr] }
+V@[if_let_expr] ::= if let R@[pattern] = V@[spec_expr] { V@[spec_expr] } else { V@[spec_expr] }
+V@[match_expr] ::= match R@[expr] { R@[match_arms] }
+```
+
These work as normal.
### `&&` and `||`
+**Syntax:**
+
+```verus-grammar
+V@[and_expr] ::= V@[spec_expr] && V@[spec_expr]
+V@[or_expr] ::= V@[spec_expr] || V@[spec_expr]
+V@[not_expr] ::= ! V@[spec_expr]
+```
+
These work as normal, though as all spec expressions are pure and effectless,
there is no notion of "short-circuiting".
### Equality (==)
+**Syntax:**
+
+```verus-grammar
+V@[equality_expr] ::= V@[spec_expr] == V@[spec_expr]
+ | V@[spec_expr] != V@[spec_expr]
+```
+
This is not the same thing as `==` in exec-mode; see [more on `==`](./spec-equality.md).
### Arithmetic
+**Syntax:**
+
+```verus-grammar
+V@[arith_expr] ::= V@[spec_expr] \+ V@[spec_expr]
+ | V@[spec_expr] - V@[spec_expr]
+ | - V@[spec_expr]
+ | V@[spec_expr] \* V@[spec_expr]
+ | V@[spec_expr] / V@[spec_expr]
+ | V@[spec_expr] % V@[spec_expr]
+```
+
Arithmetic works a little differently in order to operate with Verus's `int`
and `nat` types. See [more on arithmetic](./spec-arithmetic.md).
### References (&T)
+**Syntax:**
+
+```verus-grammar
+V@[ref_expr] ::= & V@[spec_expr]
+V@[deref_expr] ::= \* V@[spec_expr]
+```
+
Verus attempts to ignore `Box` and references as much as possible in spec mode.
However, you still needs to satisfy the Rust type-checker, so you may need to insert
references (`&`) or dereferences (`*`) to satisfy the checker. Verus will ignore these
@@ -39,6 +93,12 @@ operations however.
### Box
+**Syntax:**
+
+```verus-grammar
+V@[box_new_expr] ::= Box::new( V@[spec_expr] )
+```
+
Verus special-cases `Box` along with box operations like `Box::new(x)` or `*box`
so they may be used in spec mode. Like with references, these operations are ignored,
however they are often useful. For example, to create a recursive type you need to satisfy
diff --git a/source/docs/guide/src/trigger-annotations.md b/source/docs/guide/src/trigger-annotations.md
index 8b882f4698..1c869f5db9 100644
--- a/source/docs/guide/src/trigger-annotations.md
+++ b/source/docs/guide/src/trigger-annotations.md
@@ -9,6 +9,20 @@ on [multiple triggers and matching loops](./multitriggers.md).
This page explains the procedure Verus uses to determine these triggers from Verus source code.
+## Syntax
+
+```verus-grammar
+V@[root_trigger_attr_expr] ::= #![trigger V@[spec_expr] (, V@[spec_expr])*]
+ | #![auto]
+ | #![all_triggers]
+V@[inner_trigger_attr_expr] ::= #[trigger] V@[spec_expr]
+ | #[trigger(R@[n])] V@[spec_expr]
+```
+
+V@[root_trigger_attr_expr] annotations appear at the start of the quantifier body and configure
+trigger selection for the whole quantifier. V@[inner_trigger_attr_expr] annotations appear on
+specific sub-expressions within the body to mark them individually as triggers.
+
## Terminology: trigger groups and trigger expressions
Every quantifier has a number of _quantifier variables_. To control how the solver instantiates
diff --git a/source/docs/guide/verus-grammar.py b/source/docs/guide/verus-grammar.py
new file mode 100644
index 0000000000..5f75591cd1
--- /dev/null
+++ b/source/docs/guide/verus-grammar.py
@@ -0,0 +1,321 @@
+#!/usr/bin/env python3
+"""
+mdBook preprocessor for Verus grammar styling.
+
+In verus-grammar fenced code blocks and in regular prose (but NOT in other
+fenced code blocks or inline code spans), transforms:
+ V@[text] -> text
+ R@[text] -> text
+
+In verus-grammar blocks, V@[name] on the LHS of ::= gets id="grammar-name"
+so it can serve as a link target. All other V@[name] references become
+hyperlinks to the page+anchor where that item is defined (if known).
+
+verus-grammar fenced blocks are also converted to:
+ ...
+
+Usage:
+ As an mdBook preprocessor (reads [context, book] JSON from stdin):
+ python3 verus-grammar.py
+ python3 verus-grammar.py supports html
+
+ Check for broken/orphaned grammar references (reads src/*.md directly):
+ python3 verus-grammar.py check
+"""
+
+import html
+import json
+import os
+import re
+import sys
+
+# Matches fenced code blocks (``` or ~~~).
+FENCED_BLOCK_RE = re.compile(
+ r'^(?P`{3,}|~{3,})(?P[^\n]*)\n(?P.*?)^(?P=fence)[ \t]*\n?',
+ re.MULTILINE | re.DOTALL,
+)
+
+INLINE_CODE_RE = re.compile(r'`+[^`\n]*`+')
+
+# Matches a grammar definition: V@[name] optionally followed by whitespace then ::=
+DEFINITION_RE = re.compile(r'V@\[([^\]]*)\](\s*::=)')
+V_AT_RE = re.compile(r'V@\[([^\]]*)\]')
+R_AT_RE = re.compile(r'R@\[([^\]]*)\]')
+
+V_COLOR = '#000080'
+R_COLOR = '#800000'
+
+
+def v_span(name, anchor=None):
+ if anchor:
+ return (f'{name}')
+ return f'{name}'
+
+
+def r_span(name):
+ return f'{name}'
+
+
+def compute_relative_link(from_path, to_path):
+ """Return a relative .html link from one chapter path to another."""
+ from_dir = os.path.dirname(from_path) if from_path else ''
+ rel = os.path.relpath(to_path, from_dir) if from_dir else to_path
+ return os.path.splitext(rel)[0] + '.html'
+
+
+# ---------------------------------------------------------------------------
+# Preprocessor helpers
+# ---------------------------------------------------------------------------
+
+def collect_definitions(book):
+ """
+ First pass: scan every verus-grammar block and return a dict mapping
+ grammar item name -> chapter path for the first definition found.
+ """
+ definitions = {}
+
+ def scan(content, path):
+ for m in FENCED_BLOCK_RE.finditer(content):
+ if m.group('info').strip() == 'verus-grammar':
+ for dm in DEFINITION_RE.finditer(m.group('body')):
+ name = dm.group(1)
+ if name not in definitions:
+ definitions[name] = path
+
+ def walk(item):
+ if 'Chapter' in item:
+ chapter = item['Chapter']
+ path = chapter.get('path') or ''
+ if path:
+ scan(chapter['content'], path)
+ for sub in chapter.get('sub_items', []):
+ walk(sub)
+
+ # sometimes it's 'sections' and sometimes it's 'items', might depend on the mdbook version?
+ for section in book.get('sections', []):
+ walk(section)
+ for section in book.get('items', []):
+ walk(section)
+ return definitions
+
+
+def transform_block_body(body, current_path, definitions):
+ """Transform the body of a verus-grammar fenced block."""
+ body = html.escape(body)
+
+ # Definitions: V@[name] ::= → name ::=
+ def replace_definition(m):
+ name, rest = m.group(1), m.group(2)
+ return v_span(name, anchor=f'grammar-{name}') + rest
+
+ # References: V@[name] → linked span (or plain span if not in map)
+ def replace_v_ref(m):
+ name = m.group(1)
+ span = v_span(name)
+ if name in definitions:
+ target = definitions[name]
+ rel = compute_relative_link(current_path, target)
+ return f'{span}'
+ return span
+
+ body = DEFINITION_RE.sub(replace_definition, body)
+ body = V_AT_RE.sub(replace_v_ref, body)
+ body = R_AT_RE.sub(lambda m: r_span(m.group(1)), body)
+ body = body.replace('?', '?')
+ body = body.replace('+', '+')
+ body = body.replace('*', '*')
+ body = body.replace('\\+', '+')
+ body = body.replace('\\*', '*')
+ body = body.replace('\\?', '?')
+ return body
+
+
+def transform_prose_segment(text, current_path, definitions):
+ """Apply V@/R@ transforms to a prose segment (outside inline code)."""
+ def replace_v(m):
+ name = m.group(1)
+ span = f'{v_span(name)}'
+ if name in definitions:
+ target = definitions[name]
+ rel = compute_relative_link(current_path, target)
+ return f'{span}'
+ return span
+
+ text = V_AT_RE.sub(replace_v, text)
+ text = R_AT_RE.sub(lambda m: f'{r_span(m.group(1))}', text)
+ return text
+
+
+def transform_prose(text, current_path, definitions):
+ """Apply V@/R@ transforms to prose, skipping inline code spans."""
+ result = []
+ last_end = 0
+ for m in INLINE_CODE_RE.finditer(text):
+ result.append(transform_prose_segment(text[last_end:m.start()], current_path, definitions))
+ result.append(m.group(0))
+ last_end = m.end()
+ result.append(transform_prose_segment(text[last_end:], current_path, definitions))
+ return ''.join(result)
+
+
+def transform_content(content, current_path, definitions):
+ result = []
+ last_end = 0
+ for m in FENCED_BLOCK_RE.finditer(content):
+ result.append(transform_prose(content[last_end:m.start()], current_path, definitions))
+ info = m.group('info').strip()
+ body = m.group('body')
+ if info == 'verus-grammar':
+ transformed = transform_block_body(body, current_path, definitions)
+ result.append(f'{transformed}
\n')
+ else:
+ result.append(m.group(0))
+ last_end = m.end()
+ result.append(transform_prose(content[last_end:], current_path, definitions))
+ return ''.join(result)
+
+
+def walk_item(item, definitions):
+ if 'Chapter' in item:
+ chapter = item['Chapter']
+ path = chapter.get('path') or ''
+ chapter['content'] = transform_content(chapter['content'], path, definitions)
+ for sub in chapter.get('sub_items', []):
+ walk_item(sub, definitions)
+
+
+# ---------------------------------------------------------------------------
+# check subcommand
+# ---------------------------------------------------------------------------
+
+def _prose_v_names(prose_text):
+ """Yield all V@[name] names in a prose string, skipping inline code spans."""
+ last = 0
+ for m in INLINE_CODE_RE.finditer(prose_text):
+ for vm in V_AT_RE.finditer(prose_text[last:m.start()]):
+ yield vm.group(1)
+ last = m.end()
+ for vm in V_AT_RE.finditer(prose_text[last:]):
+ yield vm.group(1)
+
+
+def check_mode():
+ """
+ Scan src/*.md, then report:
+ (1) grammar items referenced in grammar blocks but not defined
+ (2) grammar items defined but never referenced from any grammar block
+ (3) grammar items referenced in prose but not defined
+ Grammar-block references count toward (2); prose references do not.
+ Returns an exit code (1 if any issues found, 0 otherwise).
+ """
+ script_dir = os.path.dirname(os.path.abspath(__file__))
+ src_dir = os.path.join(script_dir, 'src')
+
+ # definitions[name] = filename where V@[name] ::= first appears
+ definitions = {}
+ # grammar_refs[name] = set of filenames; non-definition V@[name] in grammar blocks
+ grammar_refs = {}
+ # prose_refs[name] = set of filenames; V@[name] in prose (outside all fenced blocks)
+ prose_refs = {}
+
+ def add_grammar_ref(name, filename):
+ grammar_refs.setdefault(name, set()).add(filename)
+
+ def add_prose_ref(name, filename):
+ prose_refs.setdefault(name, set()).add(filename)
+
+ for filename in sorted(os.listdir(src_dir)):
+ if not filename.endswith('.md'):
+ continue
+ with open(os.path.join(src_dir, filename)) as f:
+ content = f.read()
+
+ last_end = 0
+ for m in FENCED_BLOCK_RE.finditer(content):
+ # Prose segment before this fenced block
+ for name in _prose_v_names(content[last_end:m.start()]):
+ add_prose_ref(name, filename)
+
+ if m.group('info').strip() == 'verus-grammar':
+ body = m.group('body')
+ def_starts = set()
+ for dm in DEFINITION_RE.finditer(body):
+ name = dm.group(1)
+ def_starts.add(dm.start())
+ if name not in definitions:
+ definitions[name] = filename
+ for vm in V_AT_RE.finditer(body):
+ if vm.start() not in def_starts:
+ add_grammar_ref(vm.group(1), filename)
+
+ last_end = m.end()
+
+ # Trailing prose after the last fenced block
+ for name in _prose_v_names(content[last_end:]):
+ add_prose_ref(name, filename)
+
+ defined = set(definitions)
+
+ undefined_grammar = sorted(set(grammar_refs) - defined)
+ unreferenced = sorted(defined - set(grammar_refs))
+ undefined_prose = sorted(set(prose_refs) - defined)
+
+ issues = False
+
+ if undefined_grammar:
+ issues = True
+ print("Grammar items referenced in grammar blocks but not defined:")
+ for name in undefined_grammar:
+ locs = ', '.join(sorted(grammar_refs[name]))
+ print(f" V@[{name}] (in {locs})")
+ else:
+ print("No undefined grammar-block references.")
+
+ print()
+
+ if unreferenced:
+ issues = True
+ print("Grammar items defined but never referenced from a grammar block:")
+ for name in unreferenced:
+ print(f" V@[{name}] (defined in {definitions[name]})")
+ else:
+ print("No unreferenced grammar item definitions.")
+
+ print()
+
+ if undefined_prose:
+ issues = True
+ print("Grammar items referenced in prose but not defined:")
+ for name in undefined_prose:
+ locs = ', '.join(sorted(prose_refs[name]))
+ print(f" V@[{name}] (in {locs})")
+ else:
+ print("No undefined prose references.")
+
+ return 1 if issues else 0
+
+
+# ---------------------------------------------------------------------------
+# Entry point
+# ---------------------------------------------------------------------------
+
+def main():
+ if len(sys.argv) >= 2 and sys.argv[1] == 'supports':
+ renderer = sys.argv[2] if len(sys.argv) >= 3 else ''
+ sys.exit(0 if renderer == 'html' else 1)
+
+ if len(sys.argv) >= 2 and sys.argv[1] == 'check':
+ sys.exit(check_mode())
+
+ _context, book = json.load(sys.stdin)
+ definitions = collect_definitions(book)
+ for section in book.get('sections', []):
+ walk_item(section, definitions)
+ for section in book.get('items', []):
+ walk_item(section, definitions)
+ print(json.dumps(book))
+
+
+if __name__ == '__main__':
+ main()