From d11ad6e0e145efc4b47957e9831228e841fb0280 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Mon, 18 May 2026 13:45:36 +0200
Subject: [PATCH 01/22] work on reference page for types in spec mode

---
 source/docs/guide/src/SUMMARY.md         |   1 +
 source/docs/guide/src/reference-types.md | 131 +++++++++++++++++++++++
 2 files changed, 132 insertions(+)
 create mode 100644 source/docs/guide/src/reference-types.md

diff --git a/source/docs/guide/src/SUMMARY.md b/source/docs/guide/src/SUMMARY.md
index b86dabad7e..321e10aba4 100644
--- a/source/docs/guide/src/SUMMARY.md
+++ b/source/docs/guide/src/SUMMARY.md
@@ -153,6 +153,7 @@
   - [The view function `@`](./reference-at-sign.md)
   - [Spec index operator `[]`](./reference-spec-index.md)
   - [`decreases_to!`](./reference-decreases-to.md)
+- [Types](./reference-types.md)
 - [Proof features]()
   - [assert and assume]()
   - [assert ... by](./reference-assert-by.md)
diff --git a/source/docs/guide/src/reference-types.md b/source/docs/guide/src/reference-types.md
new file mode 100644
index 0000000000..6f6a2c045e
--- /dev/null
+++ b/source/docs/guide/src/reference-types.md
@@ -0,0 +1,131 @@
+# Spec representations 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`.
+
+Every type is represented as an integer (i.e., an element of ℤ) together with an implied bound
+if necessary:
+
+ * `int`: `(-∞, ∞)` (i.e., no bound)
+ * `nat`: `[0, ∞)`
+ * `uN`: <code>&#x5b;0, 2<sup>N</sup>)</code>
+ * `iN`: <code>&#x5b;-2<sup>N-1</sup>, 2<sup>N-1</sup>)</code>
+ * `usize`: <code>&#x5b;0, 2<sup>N</sup>)</code> where `N` is the platform's word size in bits
+ * `isize`: <code>&#x5b;-2<sup>N-1</sup>, 2<sup>N-1</sup>)</code> where `N` is the platform's word size in bits
+
+For `isize` and `usize`, assumptions of the platform word size is configurable
+via the [`global` directive](http://localhost:3000/reference-global.html#with-usize-and-isize).
+
+Integer types are inter-covertible using [`as`-casts](./reference-as.md).
+
+For all integer types, spec equality is defined as integer equality.
+
+## Bool
+
+A boolean is either `true` or `false`.
+
+Verus defines 
+
+For `bool`, spec equality is defined as boolean equivalence.
+
+## Char
+
+A `char` is treated as an [integer type](#integer-types) with a bespoke validity range.
+Verus follows the [Rust specification for a `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.
+
+That is, Verus treats `char` as an element of ℤ from:
+
+`[0, 0xD7ff] ∪ [0xE000, 0x10FFFF]`
+
+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.
+
+For `char`, spec equality is defined as integer equality.
+
+
+## Tuple
+
+## Box (`Box<T>`)
+
+## Shared reference (`&T`)
+
+## Mutable reference (`&mut T`)
+
+In spec code, one reasons about a mutable reference `x: &mut T` through 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).
+
+
+See [the guide page](./mutable-references.md)
+for practical information on using mutable references.
+
+> **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.
+
+> **Note:** Equality of mutable references in spec code is not the same as equality of mutable references in exec code.
+> Exec comparisons only compare the values behind the pointers. In spec code, mutable references
+> with different origins are **never** equal, not even if they have the same value, final value,
+> and address. In particular, a reborrow is not equal to the mutable borrow it is borrowed from.
+
+> **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<Ghost<&'static mut Rec>>,
+> }
+>
+> 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 <code>*final(x)</code> 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.
+
+> **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.
+
+
+## Pointer (`*const T` and `*mut T`)
+
+In spec code, a pointer `ptr: *mut T` or `ptr: *const T` is defined by three pieces of data:
+
+ * `ptr.addr()` of type `usize`: The address of the pointer
+ * `ptr@.metadata` of type [`<T as Pointee>::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)
+
+Verus treats pointers obey extentional equality: if two pointers are equal in the above three properties,
+then the pointers are equal.
+
+See the [`raw_ptr`](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/index.html) vstd librararies for reasoning about pointer accesses.
+
+> **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.
+
+> **Note:** Verus treats `*const T` and `*mut T` identically, except for the usual differences
+> in [variance](https://doc.rust-lang.org/reference/subtyping.html?#variance).
+> Casting `*const T` to `*mut T` and vice versa is semantically a no-op.
+
+## `String` and `str`
+

From 7f92801f070b8defba47768cdb8b8b6c6434a6e0 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Mon, 18 May 2026 18:01:38 +0200
Subject: [PATCH 02/22] stuff

---
 .../guide/src/ref-extensional-equality.md     |  11 +-
 source/docs/guide/src/reference-as.md         |  37 +++-
 source/docs/guide/src/reference-types.md      | 209 ++++++++++++++----
 3 files changed, 207 insertions(+), 50 deletions(-)

diff --git a/source/docs/guide/src/ref-extensional-equality.md b/source/docs/guide/src/ref-extensional-equality.md
index 705c42143d..447407ab19 100644
--- a/source/docs/guide/src/ref-extensional-equality.md
+++ b/source/docs/guide/src/ref-extensional-equality.md
@@ -1,4 +1,11 @@
 # 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.
diff --git a/source/docs/guide/src/reference-as.md b/source/docs/guide/src/reference-as.md
index 65a34e6e51..058c9cace9 100644
--- a/source/docs/guide/src/reference-as.md
+++ b/source/docs/guide/src/reference-as.md
@@ -1,7 +1,8 @@
 # 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:
+## 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 +14,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 +25,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 +33,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-types.md b/source/docs/guide/src/reference-types.md
index 6f6a2c045e..94ec109e65 100644
--- a/source/docs/guide/src/reference-types.md
+++ b/source/docs/guide/src/reference-types.md
@@ -1,82 +1,171 @@
-# Spec representations of types
+# Spec 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`.
 
-Every type is represented as an integer (i.e., an element of ℤ) together with an implied bound
-if necessary:
+**Mathematical interpretation.**
+Every integer type is represented as an integer (i.e., an element of ℤ) together with a range of accepted values:
 
- * `int`: `(-∞, ∞)` (i.e., no bound)
- * `nat`: `[0, ∞)`
- * `uN`: <code>&#x5b;0, 2<sup>N</sup>)</code>
- * `iN`: <code>&#x5b;-2<sup>N-1</sup>, 2<sup>N-1</sup>)</code>
- * `usize`: <code>&#x5b;0, 2<sup>N</sup>)</code> where `N` is the platform's word size in bits
- * `isize`: <code>&#x5b;-2<sup>N-1</sup>, 2<sup>N-1</sup>)</code> where `N` is the platform's word size in bits
+| Type    | Bound |
+|---------|-------|
+| `int`   | `(-∞, ∞)` (i.e., no bound) |
+| `nat`   | `[0, ∞)` |
+| `uN`    | <code>&#x5b;0, 2<sup>N</sup>)</code> |
+| `iN`    | <code>&#x5b;-2<sup>N-1</sup>, 2<sup>N-1</sup>)</code> |
+| `usize` | <code>&#x5b;0, 2<sup>usize::BITS</sup>)</code> |
+| `isize` | <code>&#x5b;-2<sup>isize::BITS-1</sup>, 2<sup>isize::BITS-1</sup>)</code>  |
 
-For `isize` and `usize`, assumptions of the platform word size is configurable
+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).
 
-Integer types are inter-covertible using [`as`-casts](./reference-as.md).
+**Spec equality.** Spec equality on integers is defined as integer equality.
 
-For all integer types, spec equality 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
 
-A boolean is either `true` or `false`.
+**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.
 
-Verus defines 
+**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.
 
-For `bool`, spec equality is defined as boolean equivalence.
 
 ## Char
 
-A `char` is treated as an [integer type](#integer-types) with a bespoke validity range.
-Verus follows the [Rust specification for a `char`](https://doc.rust-lang.org/std/primitive.char.html):
+**Mathematical interpreation.**
+A `char` is interpreted as an [integer type](#integer-types) with a bespoke validity range:
 
-> 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.
+| Type    | Bound |
+|---------|-------|
+| `int`   | `[0, 0xD7ff] ∪ [0xE000, 0x10FFFF]` |
 
-That is, Verus treats `char` as an element of ℤ from:
+This is consistent with the
+[Rust definition of a `char`](https://doc.rust-lang.org/std/primitive.char.html)
+as a "Unicode scalar value":
 
-`[0, 0xD7ff] ∪ [0xE000, 0x10FFFF]`
+> 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.
 
-In spec code, a `char` is inter-covertible with the integer types using [`as`-casts](./reference-as.md).
+**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.
 
-For `char`, spec equality is defined as integer equality.
+## Box (`Box<T>`)
 
+**Mathematical interpretation.**
+A `Box<T>` is interpreted identically to `T` with no additional metadata.
 
-## Tuple
+**Spec equality.**
+Spec equality on `Box<T>` is inherited from spec equality on `T`.
 
-## Box (`Box<T>`)
+**Spec operators.**
+Boxing operations `Box::new` and unboxing operations (`*x`) are semantically the identity function.
 
 ## Shared reference (`&T`)
 
-## Mutable reference (`&mut T`)
+**Mathematical interpretation.**
+A `&T` is interpreted identically to `T` with no additional metadata.
 
-In spec code, one reasons about a mutable reference `x: &mut T` through values:
+**Spec equality.**
+Spec equality on `&T` is inherited from spec equality on `T`.
 
- * `*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).
+**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.
 
-> **Note:** Equality of mutable references in spec code is not the same as equality of mutable references in exec code.
-> Exec comparisons only compare the values behind the pointers. In spec code, mutable references
-> with different origins are **never** equal, not even if they have the same value, final value,
-> and address. In particular, a reborrow is not equal to the mutable borrow it is borrowed from.
+**Additional notes.**
 
 > **Note:** Verus does not insert "implicit reborrows" for spec-mode uses of a mutable reference.
 
@@ -103,29 +192,61 @@ for practical information on using mutable references.
 > [decreases-to](./reference-decreases-to.md), i.e., recursion through the `final` value is
 > not considered to be well-founded recursion.
 
-> **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.
-
+## Raw Pointer (`*const T` and `*mut T`)
 
-## 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.
 
-In spec code, a pointer `ptr: *mut T` or `ptr: *const T` is defined by three pieces of data:
+**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 [`<T as Pointee>::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)
 
-Verus treats pointers obey extentional equality: if two pointers are equal in the above three properties,
-then the pointers are equal.
+> **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.
 
-See the [`raw_ptr`](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/index.html) vstd librararies for reasoning about pointer accesses.
+**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.
 
-> **Note:** Verus treats `*const T` and `*mut T` identically, except for the usual differences
-> in [variance](https://doc.rust-lang.org/reference/subtyping.html?#variance).
-> Casting `*const T` to `*mut T` and vice versa is semantically a no-op.
+**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 <code>Seq&lt;<a href="#char">char</a>&gt;</code>.
+
+> **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()`.
+
+
+
+## Slices and arrays
+
+
+## Mode wrappers: `Ghost` and `Tracked`

From 3b1d0896cb72d695b4d45998dce0b719d3bf1727 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 19 May 2026 12:38:02 +0200
Subject: [PATCH 03/22] add verus-grammar script

---
 source/docs/guide/book.toml                   |   3 +
 .../guide/src/reference-exec-signature.md     |  30 ++---
 source/docs/guide/src/spec-choose.md          |  58 ++++++++-
 source/docs/guide/src/spec-quantifiers.md     |  85 ++++++++++++-
 source/docs/guide/verus-grammar.py            | 112 ++++++++++++++++++
 5 files changed, 266 insertions(+), 22 deletions(-)
 create mode 100644 source/docs/guide/verus-grammar.py

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/reference-exec-signature.md b/source/docs/guide/src/reference-exec-signature.md
index b66981e78a..d921296177 100644
--- a/source/docs/guide/src/reference-exec-signature.md
+++ b/source/docs/guide/src/reference-exec-signature.md
@@ -2,37 +2,33 @@
 
 The general form of an `exec` function signature takes the form:
 
-<pre>
-<code class="hljs">fn <span style="color: #800000; font-style: italic">function_name</span> <span style="color: #800000; font-style: italic">generics</span><sup>?</sup>(<span style="color: #800000; font-style: italic">args...</span>) -&gt; <span style="color: #800000; font-style: italic">return_type_and_name</span><sup>?</sup>
-    <span style="color: #800000; font-style: italic">where_clause</span><sup>?</sup>
-    <span style="color: #000080; font-style: italic">requires_clause</span><sup>?</sup>
-    <span style="color: #000080; font-style: italic">ensures_clause</span><sup>?</sup>
-    <span style="color: #000080; font-style: italic">returns_clause</span><sup>?</sup>
-    <span style="color: #000080; font-style: italic">invariants_clause</span><sup>?</sup>
-    <span style="color: #000080; font-style: italic">unwind_clause</span><sup>?</sup>
-</code>
-</pre>
+```verus-grammar
+fn R@[function_name] R@[generics]?(R@[args...]) -> R@[return_type_and_name]?
+    R@[where_clause]?
+    V@[requires_clause]?
+    V@[ensures_clause]?
+    V@[returns_clause]?
+    V@[invariants_clause]?
+    V@[unwind_clause]?
+```
 
 ## Function specification
 
 The elements of the function specification are given by the signature clauses.
 
 **The precondition.**
-The <code class="hljs"><span style="color: #000080; font-style: italic">requires_clause</span></code> is the precondition.
+The V@[requires_clause] is the precondition.
 
 **The postcondition.**
-The <code class="hljs"><span style="color: #000080; font-style: italic">ensures_clause</span></code>
-and the
-<code class="hljs"><span style="color: #000080; font-style: italic">returns_clause</span></code>
-together form the postcondition.
+The V@[ensures_clause] and the V@[returns_clause] together form the postcondition.
 
 **The invariants.**
-The <code class="hljs"><span style="color: #000080; font-style: italic">invariants_clause</span></code> 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 <code class="hljs"><span style="color: #000080; font-style: italic">unwind_clause</span></code> 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/spec-choose.md b/source/docs/guide/src/spec-choose.md
index 2a8fb396b4..15a2dbdf64 100644
--- a/source/docs/guide/src/spec-choose.md
+++ b/source/docs/guide/src/spec-choose.md
@@ -1,3 +1,59 @@
 # 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 epsilon or the
+[such-that operator](https://en.wikipedia.org/wiki/Epsilon_calculus)).
+
+## Syntax
+
+```
+ChooseExpr ::= "choose" "|" BoundVar ("," BoundVar)* "|" SpecExpr
+BoundVar   ::= Ident ":" Type
+```
+
+`SpecExpr` is a spec-mode `bool` expression. When multiple variables are bound, the result
+is a tuple `(T1, T2, ...)`.
+
+## 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 arbitrary but 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).
+
+Therefore, to use the result of `choose|x: T| P(x)` 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))`.
+
+## Examples
+
+```rust
+// Requires a proof that such an i exists; choose picks one.
+proof fn get_zero_index(s: Seq<int>) -> (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);
+```
+
+## Relationship to `exists`
+
+`choose` and `exists` are complementary:
+
+- `exists|x: T| P(x)` asserts that a satisfying value *exists*.
+- `choose|x: T| P(x)` *extracts* a satisfying value, given that one exists.
+
+Triggers on a `choose` expression work the same way as on `exists`: Verus uses them to
+find a witness in the proof context. See [Trigger annotations](./trigger-annotations.md)
+for details.
diff --git a/source/docs/guide/src/spec-quantifiers.md b/source/docs/guide/src/spec-quantifiers.md
index 72d21547b6..de5b4a6518 100644
--- a/source/docs/guide/src/spec-quantifiers.md
+++ b/source/docs/guide/src/spec-quantifiers.md
@@ -1,6 +1,83 @@
 # 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 with type `bool`.
+
+## forall
+
+**Syntax:**
+
+```
+ForallExpr ::= "forall" "|" BoundVar ("," BoundVar)* "|" SpecExpr
+BoundVar   ::= Ident ":" Type
+```
+
+`SpecExpr` is a spec-mode `bool` expression. The bound variables are in scope in `SpecExpr`
+and are also spec-mode.
+
+**Semantics:** `forall|x: T| P(x)` is `true` if and only if `P(x)` is `true` for every
+value `x` of type `T`.
+
+**Example:**
+
+```rust
+// All elements of s are positive
+forall|i: int| 0 <= i < s.len() ==> s[i] > 0
+```
+
+## exists
+
+**Syntax:**
+
+```
+ExistsExpr ::= "exists" "|" BoundVar ("," BoundVar)* "|" SpecExpr
+BoundVar   ::= Ident ":" Type
+```
+
+**Semantics:** `exists|x: T| P(x)` is `true` if and only if there is at least one value
+`x` of type `T` for which `P(x)` is `true`. The dual identity holds:
+`exists|x: T| P(x)` is equivalent to `!forall|x: T| !P(x)`.
+
+**Example:**
+
+```rust
+// Some element of s is zero
+exists|i: int| 0 <= i < s.len() && s[i] == 0
+```
+
+## Multiple bound variables
+
+Both `forall` and `exists` support binding multiple variables simultaneously.
+This 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 |
+
+A trigger expression must be a function call, a field access, or a bitwise operator —
+arithmetic and boolean operators are not valid triggers.
+
+For full details on how Verus selects and validates trigger groups, see
+[Trigger annotations](./trigger-annotations.md).
diff --git a/source/docs/guide/verus-grammar.py b/source/docs/guide/verus-grammar.py
new file mode 100644
index 0000000000..cd4398e580
--- /dev/null
+++ b/source/docs/guide/verus-grammar.py
@@ -0,0 +1,112 @@
+#!/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]  ->  <span style="color: #000080; font-style: italic">text</span>
+  R@[text]  ->  <span style="color: #800000; font-style: italic">text</span>
+
+verus-grammar fenced blocks are also converted to:
+  <pre class="verus-grammar"><code>...</code></pre>
+"""
+
+import html
+import json
+import re
+import sys
+
+# Used inside verus-grammar blocks (already in <pre><code> context).
+BLOCK_TRANSFORMS = [
+    (re.compile(r'V@\[([^\]]*)\]'),
+     r'<span style="color: #000080; font-style: italic">\1</span>'),
+    (re.compile(r'R@\[([^\]]*)\]'),
+     r'<span style="color: #800000; font-style: italic">\1</span>'),
+]
+
+# Used in prose — adds a <code> wrapper for monospace font.
+PROSE_TRANSFORMS = [
+    (re.compile(r'V@\[([^\]]*)\]'),
+     r'<code><span style="color: #000080; font-style: italic">\1</span></code>'),
+    (re.compile(r'R@\[([^\]]*)\]'),
+     r'<code><span style="color: #800000; font-style: italic">\1</span></code>'),
+]
+
+# Matches fenced code blocks (``` or ~~~). The closing fence must use the
+# same fence character sequence as the opening (via back-reference).
+FENCED_BLOCK_RE = re.compile(
+    r'^(?P<fence>`{3,}|~{3,})(?P<info>[^\n]*)\n(?P<body>.*?)^(?P=fence)[ \t]*\n?',
+    re.MULTILINE | re.DOTALL,
+)
+
+# Matches inline code spans (simplified: same-delimiter open and close).
+INLINE_CODE_RE = re.compile(r'`+[^`\n]*`+')
+
+
+def apply_transforms(text, transforms):
+    for pattern, replacement in transforms:
+        text = pattern.sub(replacement, text)
+    return text
+
+
+def transform_prose(text):
+    """Apply V@/R@ transforms to prose, skipping inline code spans."""
+    result = []
+    last_end = 0
+    for m in INLINE_CODE_RE.finditer(text):
+        result.append(apply_transforms(text[last_end:m.start()], PROSE_TRANSFORMS))
+        result.append(m.group(0))
+        last_end = m.end()
+    result.append(apply_transforms(text[last_end:], PROSE_TRANSFORMS))
+    return ''.join(result)
+
+
+def transform_content(content):
+    result = []
+    last_end = 0
+
+    for m in FENCED_BLOCK_RE.finditer(content):
+        # Transform the prose segment before this fenced block.
+        result.append(transform_prose(content[last_end:m.start()]))
+
+        info = m.group('info').strip()
+        body = m.group('body')
+
+        if info == 'verus-grammar':
+            # HTML-escape first so the raw body text is safe, then apply
+            # transforms to inject the <span> markup, then superscript '?'.
+            transformed = apply_transforms(html.escape(body), BLOCK_TRANSFORMS)
+            transformed = transformed.replace('?', '<sup>?</sup>')
+            result.append(f'<pre class="verus-grammar"><code>{transformed}</code></pre>\n')
+        else:
+            # Leave all other fenced blocks entirely untouched.
+            result.append(m.group(0))
+
+        last_end = m.end()
+
+    # Transform any trailing prose after the last fenced block.
+    result.append(transform_prose(content[last_end:]))
+    return ''.join(result)
+
+
+def walk_item(item):
+    if 'Chapter' in item:
+        chapter = item['Chapter']
+        chapter['content'] = transform_content(chapter['content'])
+        for sub_item in chapter.get('sub_items', []):
+            walk_item(sub_item)
+
+
+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)
+
+    _context, book = json.load(sys.stdin)
+    for section in book.get('sections', []):
+        walk_item(section)
+    print(json.dumps(book))
+
+
+if __name__ == '__main__':
+    main()

From b5c547d7e305039804206abe6bd76d80ddc21bfc Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 19 May 2026 12:44:44 +0200
Subject: [PATCH 04/22] more updates

---
 source/docs/guide/src/spec-choose.md      | 5 ++---
 source/docs/guide/src/spec-quantifiers.md | 5 ++---
 2 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/source/docs/guide/src/spec-choose.md b/source/docs/guide/src/spec-choose.md
index 15a2dbdf64..20d32f523b 100644
--- a/source/docs/guide/src/spec-choose.md
+++ b/source/docs/guide/src/spec-choose.md
@@ -8,9 +8,8 @@ a given predicate. It is the Hilbert choice operator (also known as epsilon or t
 
 ## Syntax
 
-```
-ChooseExpr ::= "choose" "|" BoundVar ("," BoundVar)* "|" SpecExpr
-BoundVar   ::= Ident ":" Type
+```verus-grammar
+V@[choose_expr] ::= choose |R@[binders...]| V@[spec_expr]
 ```
 
 `SpecExpr` is a spec-mode `bool` expression. When multiple variables are bound, the result
diff --git a/source/docs/guide/src/spec-quantifiers.md b/source/docs/guide/src/spec-quantifiers.md
index de5b4a6518..fff43c9c04 100644
--- a/source/docs/guide/src/spec-quantifiers.md
+++ b/source/docs/guide/src/spec-quantifiers.md
@@ -10,9 +10,8 @@ Both `forall` and `exists` are **spec-mode only** expressions with type `bool`.
 
 **Syntax:**
 
-```
-ForallExpr ::= "forall" "|" BoundVar ("," BoundVar)* "|" SpecExpr
-BoundVar   ::= Ident ":" Type
+```verus-grammar
+V@[forall_expr] ::= forall |R@[binders...]| V@[spec_expr]
 ```
 
 `SpecExpr` is a spec-mode `bool` expression. The bound variables are in scope in `SpecExpr`

From 8be63e693c858e4bd800b627858b3a86cafd692a Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 19 May 2026 13:01:30 +0200
Subject: [PATCH 05/22] add grammar blocks

---
 source/docs/guide/src/prefix-and-or.md         | 14 +++++++++++++-
 .../docs/guide/src/ref-extensional-equality.md |  7 +++++++
 source/docs/guide/src/reference-as.md          |  6 ++++++
 source/docs/guide/src/reference-at-sign.md     |  6 ++++++
 source/docs/guide/src/reference-chained-op.md  |  7 +++++++
 .../docs/guide/src/reference-decreases-to.md   |  6 ++++++
 source/docs/guide/src/reference-implication.md |  8 ++++++++
 source/docs/guide/src/reference-spec-index.md  |  6 ++++++
 source/docs/guide/src/spec-arithmetic.md       | 11 +++++++++++
 source/docs/guide/src/spec-bit-ops.md          | 10 ++++++++++
 source/docs/guide/src/spec-equality.md         | 13 ++++++++++++-
 source/docs/guide/src/spec-expressions.md      | 18 ++++++++++++++++++
 .../docs/guide/src/spec-operator-precedence.md | 10 ++++++++++
 source/docs/guide/src/spec-rust-subset.md      | 18 ++++++++++++++++++
 source/docs/guide/src/trigger-annotations.md   | 14 ++++++++++++++
 15 files changed, 152 insertions(+), 2 deletions(-)

diff --git a/source/docs/guide/src/prefix-and-or.md b/source/docs/guide/src/prefix-and-or.md
index 798cd7d4f2..1ef29cbf09 100644
--- a/source/docs/guide/src/prefix-and-or.md
+++ b/source/docs/guide/src/prefix-and-or.md
@@ -1,3 +1,15 @@
 # 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)), making them convenient for
+writing large conjunctions or disjunctions without parenthesization.
diff --git a/source/docs/guide/src/ref-extensional-equality.md b/source/docs/guide/src/ref-extensional-equality.md
index 447407ab19..9ab3dea2ee 100644
--- a/source/docs/guide/src/ref-extensional-equality.md
+++ b/source/docs/guide/src/ref-extensional-equality.md
@@ -9,3 +9,10 @@ Specifically, the use of the `=~=` and `=~~=` operators will trigger the applica
 "extensional equality" operators.
 
 See [the guide page](extensional_equality.md) for an introductory explanation.
+
+## Syntax
+
+```verus-grammar
+V@[ext_eq_expr] ::= V@[spec_expr] =~=  V@[spec_expr]
+                  | V@[spec_expr] =~~= V@[spec_expr]
+```
diff --git a/source/docs/guide/src/reference-as.md b/source/docs/guide/src/reference-as.md
index 058c9cace9..b3ce0337dd 100644
--- a/source/docs/guide/src/reference-as.md
+++ b/source/docs/guide/src/reference-as.md
@@ -1,5 +1,11 @@
 # Coercion with `as`
 
+## 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:
diff --git a/source/docs/guide/src/reference-at-sign.md b/source/docs/guide/src/reference-at-sign.md
index 2e90ff5fd8..f444b8f283 100644
--- a/source/docs/guide/src/reference-at-sign.md
+++ b/source/docs/guide/src/reference-at-sign.md
@@ -1,5 +1,11 @@
 # The view function `@`
 
+## Syntax
+
+```verus-grammar
+V@[view_expr] ::= R@[expr] @
+```
+
 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
diff --git a/source/docs/guide/src/reference-chained-op.md b/source/docs/guide/src/reference-chained-op.md
index 2bdcdd0b58..03ba570c69 100644
--- a/source/docs/guide/src/reference-chained-op.md
+++ b/source/docs/guide/src/reference-chained-op.md
@@ -1,5 +1,12 @@
 # Chained operators
 
+## Syntax
+
+```verus-grammar
+V@[chained_expr] ::= V@[spec_expr] (V@[cmp_op] V@[spec_expr])+
+V@[cmp_op]       ::= < | <= | > | >= | ==
+```
+
 In spec code, equality and inequality operators can be chained. For example,
 `a <= b < c`
 is equivalent to
diff --git a/source/docs/guide/src/reference-decreases-to.md b/source/docs/guide/src/reference-decreases-to.md
index d35c36c803..ee5c1b5951 100644
--- a/source/docs/guide/src/reference-decreases-to.md
+++ b/source/docs/guide/src/reference-decreases-to.md
@@ -13,6 +13,12 @@ is used to check the `decreases` measure for spec functions.
 See [this tutorial chapter](./lex_mutual.md) for an introductory discussion of
 lexicographic-decreases.
 
+## Syntax
+
+```verus-grammar
+V@[decreases_to_expr] ::= decreases_to!( V@[spec_expr] (, V@[spec_expr])* => V@[spec_expr] (, V@[spec_expr])* )
+```
+
 ## Definition
 
 We say that
diff --git a/source/docs/guide/src/reference-implication.md b/source/docs/guide/src/reference-implication.md
index 3c806fcfef..edbfc827ad 100644
--- a/source/docs/guide/src/reference-implication.md
+++ b/source/docs/guide/src/reference-implication.md
@@ -1,5 +1,13 @@
 # Implication (==&gt;, &lt;==, and &lt;==&gt;)
 
+## Syntax
+
+```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]
+```
+
 The operator `P ==> Q`, read _P implies Q_, is equivalent to `!P || Q`.
 
 This can also be written backwards: `Q <== P` is equivalent to `P ==> Q`.
diff --git a/source/docs/guide/src/reference-spec-index.md b/source/docs/guide/src/reference-spec-index.md
index d0bc924d68..462458ebe9 100644
--- a/source/docs/guide/src/reference-spec-index.md
+++ b/source/docs/guide/src/reference-spec-index.md
@@ -1,5 +1,11 @@
 # Spec index operator []
 
+## Syntax
+
+```verus-grammar
+V@[spec_index_expr] ::= V@[spec_expr] [ V@[spec_expr] ]
+```
+
 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).
 
diff --git a/source/docs/guide/src/spec-arithmetic.md b/source/docs/guide/src/spec-arithmetic.md
index 75ba5aa0a6..1d20ac7d05 100644
--- a/source/docs/guide/src/spec-arithmetic.md
+++ b/source/docs/guide/src/spec-arithmetic.md
@@ -6,6 +6,17 @@ This page is **does not apply** to arithmetic is _executable Rust code_.
 For an introduction to Verus arithmetic, see
 [Integers and arithmetic](./integers.md).
 
+## 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]
+```
+
 ## Type widening
 
 In spec code, the results of arithmetic are automatically widened to avoid overflow or wrapping.
diff --git a/source/docs/guide/src/spec-bit-ops.md b/source/docs/guide/src/spec-bit-ops.md
index 7b327fb1d5..0a38e05443 100644
--- a/source/docs/guide/src/spec-bit-ops.md
+++ b/source/docs/guide/src/spec-bit-ops.md
@@ -1,5 +1,15 @@
 # Bit operators
 
+## Syntax
+
+```verus-grammar
+V@[bit_and_expr] ::= V@[spec_expr] &  V@[spec_expr]
+V@[bit_or_expr]  ::= V@[spec_expr] |  V@[spec_expr]
+V@[bit_xor_expr] ::= V@[spec_expr] ^  V@[spec_expr]
+V@[shl_expr]     ::= V@[spec_expr] << V@[spec_expr]
+V@[shr_expr]     ::= V@[spec_expr] >> V@[spec_expr]
+```
+
 ## Definitions
 
 ### `&`, `|`, and `^`
diff --git a/source/docs/guide/src/spec-equality.md b/source/docs/guide/src/spec-equality.md
index 0c8a9cfd34..f891c7f549 100644
--- a/source/docs/guide/src/spec-equality.md
+++ b/source/docs/guide/src/spec-equality.md
@@ -1,3 +1,14 @@
 # Spec equality (`==`)
 
-The spec equality operator `==` is explained in [Equality](./equality.md).
+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]
+```
+
+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.
+The `!=` operator is its negation.
diff --git a/source/docs/guide/src/spec-expressions.md b/source/docs/guide/src/spec-expressions.md
index aa8968ea07..64fd9c8efa 100644
--- a/source/docs/guide/src/spec-expressions.md
+++ b/source/docs/guide/src/spec-expressions.md
@@ -2,3 +2,21 @@
 
 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@[rust_subset_expr]
+                | V@[arith_expr]
+                | V@[equality_expr]
+                | V@[ext_eq_expr]
+                | V@[implication_expr]
+                | V@[prefix_and_expr]
+                | V@[prefix_or_expr]
+                | V@[forall_expr]
+                | V@[exists_expr]
+                | V@[choose_expr]
+                | V@[view_expr]
+                | V@[spec_index_expr]
+                | V@[decreases_to_expr]
+```
diff --git a/source/docs/guide/src/spec-operator-precedence.md b/source/docs/guide/src/spec-operator-precedence.md
index e1d177bc9e..c34907716b 100644
--- a/source/docs/guide/src/spec-operator-precedence.md
+++ b/source/docs/guide/src/spec-operator-precedence.md
@@ -1,5 +1,15 @@
 # Operator Precedence
 
+## Syntax
+
+```verus-grammar
+V@[spec_expr] ::= V@[spec_expr] R@[binary_op] V@[spec_expr]
+                | R@[unary_op] V@[spec_expr]
+                | ( V@[spec_expr] )
+```
+
+The table below defines operator precedence from tightest-binding (top) to loosest-binding (bottom).
+
 | Operator                 | Associativity         |
 |--------------------------|-----------------------|
 | **Binds tighter**                                |
diff --git a/source/docs/guide/src/spec-rust-subset.md b/source/docs/guide/src/spec-rust-subset.md
index e27232c2b1..a8de6b8ee0 100644
--- a/source/docs/guide/src/spec-rust-subset.md
+++ b/source/docs/guide/src/spec-rust-subset.md
@@ -3,6 +3,24 @@
 Much of the spec language looks like a subset of the Rust language, though
 there are some subtle differences.
 
+## Syntax
+
+```verus-grammar
+V@[rust_subset_expr] ::= R@[literal]
+                       | R@[path]
+                       | R@[path] ( V@[spec_expr]* )
+                       | V@[spec_expr] . R@[field]
+                       | let R@[pattern] = V@[spec_expr]; V@[spec_expr]
+                       | if V@[spec_expr] { V@[spec_expr] } else { V@[spec_expr] }
+                       | if let R@[pattern] = R@[expr] { V@[spec_expr] } else { V@[spec_expr] }
+                       | match R@[expr] { R@[match_arms] }
+                       | V@[spec_expr] && V@[spec_expr]
+                       | V@[spec_expr] || V@[spec_expr]
+                       | ! V@[spec_expr]
+                       | & V@[spec_expr]
+                       | * V@[spec_expr]
+```
+
 ### Function calls
 
 Only pure function calls are allowed (i.e., calls to other `spec` functions or
diff --git a/source/docs/guide/src/trigger-annotations.md b/source/docs/guide/src/trigger-annotations.md
index 8b882f4698..e5e133d0d2 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]  ::= #![trigger V@[spec_expr] (, V@[spec_expr])*]
+                         | #![auto]
+                         | #![all_triggers]
+V@[inner_trigger_attr] ::= #[trigger] V@[spec_expr]
+                         | #[trigger(R@[n])] V@[spec_expr]
+```
+
+V@[root_trigger_attr] annotations appear at the start of the quantifier body and configure
+trigger selection for the whole quantifier. V@[inner_trigger_attr] 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

From b85a516d5ea55edc34420e540d01a87e7941863b Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 19 May 2026 13:50:28 +0200
Subject: [PATCH 06/22] more tweaks

---
 source/docs/guide/src/prefix-and-or.md        |  2 +-
 .../guide/src/ref-extensional-equality.md     |  2 +-
 source/docs/guide/src/spec-arithmetic.md      | 10 +--
 source/docs/guide/src/spec-bit-ops.md         | 10 +--
 source/docs/guide/src/spec-equality.md        |  2 +-
 source/docs/guide/src/spec-expressions.md     | 26 +++----
 .../guide/src/spec-operator-precedence.md     |  4 +-
 source/docs/guide/src/spec-rust-subset.md     | 73 +++++++++++++++----
 source/docs/guide/src/trigger-annotations.md  |  6 +-
 9 files changed, 88 insertions(+), 47 deletions(-)

diff --git a/source/docs/guide/src/prefix-and-or.md b/source/docs/guide/src/prefix-and-or.md
index 1ef29cbf09..25d548ee75 100644
--- a/source/docs/guide/src/prefix-and-or.md
+++ b/source/docs/guide/src/prefix-and-or.md
@@ -6,7 +6,7 @@ For an introduction, see [Expressions and operators for specifications](operator
 
 ```verus-grammar
 V@[prefix_and_expr] ::= (&&&  V@[spec_expr])+
-V@[prefix_or_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
diff --git a/source/docs/guide/src/ref-extensional-equality.md b/source/docs/guide/src/ref-extensional-equality.md
index 9ab3dea2ee..a7aac68cad 100644
--- a/source/docs/guide/src/ref-extensional-equality.md
+++ b/source/docs/guide/src/ref-extensional-equality.md
@@ -14,5 +14,5 @@ See [the guide page](extensional_equality.md) for an introductory explanation.
 
 ```verus-grammar
 V@[ext_eq_expr] ::= V@[spec_expr] =~=  V@[spec_expr]
-                  | V@[spec_expr] =~~= V@[spec_expr]
+              | V@[spec_expr] =~~= V@[spec_expr]
 ```
diff --git a/source/docs/guide/src/spec-arithmetic.md b/source/docs/guide/src/spec-arithmetic.md
index 1d20ac7d05..119dc939e3 100644
--- a/source/docs/guide/src/spec-arithmetic.md
+++ b/source/docs/guide/src/spec-arithmetic.md
@@ -10,11 +10,11 @@ For an introduction to Verus arithmetic, see
 
 ```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@[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]
 ```
 
 ## Type widening
diff --git a/source/docs/guide/src/spec-bit-ops.md b/source/docs/guide/src/spec-bit-ops.md
index 0a38e05443..2530e21d20 100644
--- a/source/docs/guide/src/spec-bit-ops.md
+++ b/source/docs/guide/src/spec-bit-ops.md
@@ -3,11 +3,11 @@
 ## Syntax
 
 ```verus-grammar
-V@[bit_and_expr] ::= V@[spec_expr] &  V@[spec_expr]
-V@[bit_or_expr]  ::= V@[spec_expr] |  V@[spec_expr]
-V@[bit_xor_expr] ::= V@[spec_expr] ^  V@[spec_expr]
-V@[shl_expr]     ::= V@[spec_expr] << V@[spec_expr]
-V@[shr_expr]     ::= V@[spec_expr] >> V@[spec_expr]
+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]
 ```
 
 ## Definitions
diff --git a/source/docs/guide/src/spec-equality.md b/source/docs/guide/src/spec-equality.md
index f891c7f549..a2cccad9c8 100644
--- a/source/docs/guide/src/spec-equality.md
+++ b/source/docs/guide/src/spec-equality.md
@@ -6,7 +6,7 @@ For an introduction, see [Equality](./equality.md).
 
 ```verus-grammar
 V@[equality_expr] ::= V@[spec_expr] == V@[spec_expr]
-                    | V@[spec_expr] != V@[spec_expr]
+                | V@[spec_expr] != V@[spec_expr]
 ```
 
 In spec mode, `==` is mathematical equality — it is not the same as `==` in exec code,
diff --git a/source/docs/guide/src/spec-expressions.md b/source/docs/guide/src/spec-expressions.md
index 64fd9c8efa..154f7fbfd4 100644
--- a/source/docs/guide/src/spec-expressions.md
+++ b/source/docs/guide/src/spec-expressions.md
@@ -6,17 +6,17 @@ specification expressions. This section discusses those operators.
 ## Syntax
 
 ```verus-grammar
-V@[spec_expr] ::= V@[rust_subset_expr]
-                | V@[arith_expr]
-                | V@[equality_expr]
-                | V@[ext_eq_expr]
-                | V@[implication_expr]
-                | V@[prefix_and_expr]
-                | V@[prefix_or_expr]
-                | V@[forall_expr]
-                | V@[exists_expr]
-                | V@[choose_expr]
-                | V@[view_expr]
-                | V@[spec_index_expr]
-                | V@[decreases_to_expr]
+V@[spec_expr] ::= V@[arith_expr]
+            | V@[bit_expr]
+            | V@[equality_expr]
+            | V@[ext_eq_expr]
+            | V@[implication_expr]
+            | V@[prefix_and_expr]
+            | V@[prefix_or_expr]
+            | V@[forall_expr]
+            | V@[exists_expr]
+            | V@[choose_expr]
+            | V@[view_expr]
+            | V@[spec_index_expr]
+            | V@[decreases_to_expr]
 ```
diff --git a/source/docs/guide/src/spec-operator-precedence.md b/source/docs/guide/src/spec-operator-precedence.md
index c34907716b..7dc4534729 100644
--- a/source/docs/guide/src/spec-operator-precedence.md
+++ b/source/docs/guide/src/spec-operator-precedence.md
@@ -4,8 +4,8 @@
 
 ```verus-grammar
 V@[spec_expr] ::= V@[spec_expr] R@[binary_op] V@[spec_expr]
-                | R@[unary_op] V@[spec_expr]
-                | ( V@[spec_expr] )
+            | R@[unary_op] V@[spec_expr]
+            | ( V@[spec_expr] )
 ```
 
 The table below defines operator precedence from tightest-binding (top) to loosest-binding (bottom).
diff --git a/source/docs/guide/src/spec-rust-subset.md b/source/docs/guide/src/spec-rust-subset.md
index a8de6b8ee0..6c5faf435a 100644
--- a/source/docs/guide/src/spec-rust-subset.md
+++ b/source/docs/guide/src/spec-rust-subset.md
@@ -3,53 +3,88 @@
 Much of the spec language looks like a subset of the Rust language, though
 there are some subtle differences.
 
-## Syntax
+### Function calls
+
+**Syntax:**
 
 ```verus-grammar
-V@[rust_subset_expr] ::= R@[literal]
-                       | R@[path]
-                       | R@[path] ( V@[spec_expr]* )
-                       | V@[spec_expr] . R@[field]
-                       | let R@[pattern] = V@[spec_expr]; V@[spec_expr]
-                       | if V@[spec_expr] { V@[spec_expr] } else { V@[spec_expr] }
-                       | if let R@[pattern] = R@[expr] { V@[spec_expr] } else { V@[spec_expr] }
-                       | match R@[expr] { R@[match_arms] }
-                       | V@[spec_expr] && V@[spec_expr]
-                       | V@[spec_expr] || V@[spec_expr]
-                       | ! V@[spec_expr]
-                       | & V@[spec_expr]
-                       | * V@[spec_expr]
+V@[fn_call_expr] ::= R@[path] ( V@[spec_expr]* )
 ```
 
-### Function calls
-
 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@[let_expr] ::= let R@[pattern] = V@[spec_expr]; 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] = R@[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
@@ -57,6 +92,12 @@ operations however.
 
 ### Box
 
+**Syntax:**
+
+```verus-grammar
+V@[box_new_expr] ::= Box::new( V@[spec_expr] )
+```
+
 Verus special-cases `Box<T>` 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 e5e133d0d2..8fe27c7928 100644
--- a/source/docs/guide/src/trigger-annotations.md
+++ b/source/docs/guide/src/trigger-annotations.md
@@ -13,10 +13,10 @@ This page explains the procedure Verus uses to determine these triggers from Ver
 
 ```verus-grammar
 V@[root_trigger_attr]  ::= #![trigger V@[spec_expr] (, V@[spec_expr])*]
-                         | #![auto]
-                         | #![all_triggers]
+                     | #![auto]
+                     | #![all_triggers]
 V@[inner_trigger_attr] ::= #[trigger] V@[spec_expr]
-                         | #[trigger(R@[n])] V@[spec_expr]
+                     | #[trigger(R@[n])] V@[spec_expr]
 ```
 
 V@[root_trigger_attr] annotations appear at the start of the quantifier body and configure

From 9c4e940978a5cb1ae8ca0345dc986ac9c6b716af Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 19 May 2026 14:01:23 +0200
Subject: [PATCH 07/22] magic hyperlinking

---
 source/docs/guide/src/spec-quantifiers.md |   5 +-
 source/docs/guide/verus-grammar.py        | 159 ++++++++++++++++------
 2 files changed, 116 insertions(+), 48 deletions(-)

diff --git a/source/docs/guide/src/spec-quantifiers.md b/source/docs/guide/src/spec-quantifiers.md
index fff43c9c04..d1af9f051c 100644
--- a/source/docs/guide/src/spec-quantifiers.md
+++ b/source/docs/guide/src/spec-quantifiers.md
@@ -31,9 +31,8 @@ forall|i: int| 0 <= i < s.len() ==> s[i] > 0
 
 **Syntax:**
 
-```
-ExistsExpr ::= "exists" "|" BoundVar ("," BoundVar)* "|" SpecExpr
-BoundVar   ::= Ident ":" Type
+```verus-grammar
+V@[exists_expr] ::= exists |R@[binders...]| V@[spec_expr]
 ```
 
 **Semantics:** `exists|x: T| P(x)` is `true` if and only if there is at least one value
diff --git a/source/docs/guide/verus-grammar.py b/source/docs/guide/verus-grammar.py
index cd4398e580..1138ba77cc 100644
--- a/source/docs/guide/verus-grammar.py
+++ b/source/docs/guide/verus-grammar.py
@@ -7,94 +7,162 @@
   V@[text]  ->  <span style="color: #000080; font-style: italic">text</span>
   R@[text]  ->  <span style="color: #800000; font-style: italic">text</span>
 
+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:
   <pre class="verus-grammar"><code>...</code></pre>
 """
 
 import html
 import json
+import os
 import re
 import sys
 
-# Used inside verus-grammar blocks (already in <pre><code> context).
-BLOCK_TRANSFORMS = [
-    (re.compile(r'V@\[([^\]]*)\]'),
-     r'<span style="color: #000080; font-style: italic">\1</span>'),
-    (re.compile(r'R@\[([^\]]*)\]'),
-     r'<span style="color: #800000; font-style: italic">\1</span>'),
-]
-
-# Used in prose — adds a <code> wrapper for monospace font.
-PROSE_TRANSFORMS = [
-    (re.compile(r'V@\[([^\]]*)\]'),
-     r'<code><span style="color: #000080; font-style: italic">\1</span></code>'),
-    (re.compile(r'R@\[([^\]]*)\]'),
-     r'<code><span style="color: #800000; font-style: italic">\1</span></code>'),
-]
-
-# Matches fenced code blocks (``` or ~~~). The closing fence must use the
-# same fence character sequence as the opening (via back-reference).
+# Matches fenced code blocks (``` or ~~~).
 FENCED_BLOCK_RE = re.compile(
     r'^(?P<fence>`{3,}|~{3,})(?P<info>[^\n]*)\n(?P<body>.*?)^(?P=fence)[ \t]*\n?',
     re.MULTILINE | re.DOTALL,
 )
 
-# Matches inline code spans (simplified: same-delimiter open and close).
 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'<span id="{anchor}" style="color: {V_COLOR}; '
+                f'font-style: italic">{name}</span>')
+    return f'<span style="color: {V_COLOR}; font-style: italic">{name}</span>'
+
+
+def r_span(name):
+    return f'<span style="color: {R_COLOR}; font-style: italic">{name}</span>'
+
+
+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'
+
 
-def apply_transforms(text, transforms):
-    for pattern, replacement in transforms:
-        text = pattern.sub(replacement, text)
+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)
+
+    for section in book.get('sections', []):
+        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] ::=  →  <span id="grammar-name">name</span> ::=
+    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'<a href="{rel}#grammar-{name}">{span}</a>'
+        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('?', '<sup>?</sup>')
+    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'<code>{v_span(name)}</code>'
+        if name in definitions:
+            target = definitions[name]
+            rel = compute_relative_link(current_path, target)
+            return f'<a href="{rel}#grammar-{name}">{span}</a>'
+        return span
+
+    text = V_AT_RE.sub(replace_v, text)
+    text = R_AT_RE.sub(lambda m: f'<code>{r_span(m.group(1))}</code>', text)
     return text
 
 
-def transform_prose(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(apply_transforms(text[last_end:m.start()], PROSE_TRANSFORMS))
+        result.append(transform_prose_segment(text[last_end:m.start()], current_path, definitions))
         result.append(m.group(0))
         last_end = m.end()
-    result.append(apply_transforms(text[last_end:], PROSE_TRANSFORMS))
+    result.append(transform_prose_segment(text[last_end:], current_path, definitions))
     return ''.join(result)
 
 
-def transform_content(content):
+def transform_content(content, current_path, definitions):
     result = []
     last_end = 0
-
     for m in FENCED_BLOCK_RE.finditer(content):
-        # Transform the prose segment before this fenced block.
-        result.append(transform_prose(content[last_end:m.start()]))
-
+        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':
-            # HTML-escape first so the raw body text is safe, then apply
-            # transforms to inject the <span> markup, then superscript '?'.
-            transformed = apply_transforms(html.escape(body), BLOCK_TRANSFORMS)
-            transformed = transformed.replace('?', '<sup>?</sup>')
+            transformed = transform_block_body(body, current_path, definitions)
             result.append(f'<pre class="verus-grammar"><code>{transformed}</code></pre>\n')
         else:
-            # Leave all other fenced blocks entirely untouched.
             result.append(m.group(0))
-
         last_end = m.end()
-
-    # Transform any trailing prose after the last fenced block.
-    result.append(transform_prose(content[last_end:]))
+    result.append(transform_prose(content[last_end:], current_path, definitions))
     return ''.join(result)
 
 
-def walk_item(item):
+def walk_item(item, definitions):
     if 'Chapter' in item:
         chapter = item['Chapter']
-        chapter['content'] = transform_content(chapter['content'])
-        for sub_item in chapter.get('sub_items', []):
-            walk_item(sub_item)
+        path = chapter.get('path') or ''
+        chapter['content'] = transform_content(chapter['content'], path, definitions)
+        for sub in chapter.get('sub_items', []):
+            walk_item(sub, definitions)
 
 
 def main():
@@ -103,8 +171,9 @@ def main():
         sys.exit(0 if renderer == 'html' else 1)
 
     _context, book = json.load(sys.stdin)
+    definitions = collect_definitions(book)
     for section in book.get('sections', []):
-        walk_item(section)
+        walk_item(section, definitions)
     print(json.dumps(book))
 
 

From 4744ec643721738b238607b03e94589907af1704 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 19 May 2026 14:42:30 +0200
Subject: [PATCH 08/22] more stuff

---
 .../guide/src/ref-extensional-equality.md     |  11 +-
 .../guide/src/reference-exec-signature.md     |  15 +--
 source/docs/guide/src/reference-types.md      |   2 +-
 source/docs/guide/src/spec-arithmetic.md      |  22 ++--
 source/docs/guide/src/spec-bit-ops.md         |  15 ++-
 source/docs/guide/src/spec-equality.md        |  21 +++-
 source/docs/guide/src/spec-expressions.md     |  20 +++-
 source/docs/guide/src/spec-rust-subset.md     |   5 +-
 source/docs/guide/verus-grammar.py            | 100 ++++++++++++++++++
 9 files changed, 180 insertions(+), 31 deletions(-)

diff --git a/source/docs/guide/src/ref-extensional-equality.md b/source/docs/guide/src/ref-extensional-equality.md
index a7aac68cad..a3010f9d69 100644
--- a/source/docs/guide/src/ref-extensional-equality.md
+++ b/source/docs/guide/src/ref-extensional-equality.md
@@ -10,9 +10,18 @@ Specifically, the use of the `=~=` and `=~~=` operators will trigger the applica
 
 See [the guide page](extensional_equality.md) for an introductory explanation.
 
-## Syntax
+### 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-exec-signature.md b/source/docs/guide/src/reference-exec-signature.md
index d921296177..1a1551f963 100644
--- a/source/docs/guide/src/reference-exec-signature.md
+++ b/source/docs/guide/src/reference-exec-signature.md
@@ -3,13 +3,14 @@
 The general form of an `exec` function signature takes the form:
 
 ```verus-grammar
-fn R@[function_name] R@[generics]?(R@[args...]) -> R@[return_type_and_name]?
-    R@[where_clause]?
-    V@[requires_clause]?
-    V@[ensures_clause]?
-    V@[returns_clause]?
-    V@[invariants_clause]?
-    V@[unwind_clause]?
+V@[fn_with_verus_sig] :=
+    fn R@[function_name] R@[generics]?(R@[args...]) -> R@[return_type_and_name]?
+        R@[where_clause]?
+        V@[requires_clause]?
+        V@[ensures_clause]?
+        V@[returns_clause]?
+        V@[invariants_clause]?
+        V@[unwind_clause]?
 ```
 
 ## Function specification
diff --git a/source/docs/guide/src/reference-types.md b/source/docs/guide/src/reference-types.md
index 94ec109e65..85b9523dff 100644
--- a/source/docs/guide/src/reference-types.md
+++ b/source/docs/guide/src/reference-types.md
@@ -1,4 +1,4 @@
-# Spec interpretations of types
+# Mathematical interpretations of types
 
 ## Integer types
 
diff --git a/source/docs/guide/src/spec-arithmetic.md b/source/docs/guide/src/spec-arithmetic.md
index 119dc939e3..1e7e1993e1 100644
--- a/source/docs/guide/src/spec-arithmetic.md
+++ b/source/docs/guide/src/spec-arithmetic.md
@@ -6,7 +6,7 @@ This page is **does not apply** to arithmetic is _executable Rust code_.
 For an introduction to Verus arithmetic, see
 [Integers and arithmetic](./integers.md).
 
-## Syntax
+### Syntax
 
 ```verus-grammar
 V@[arith_expr] ::= V@[spec_expr] + V@[spec_expr]
@@ -15,9 +15,13 @@ 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@[spec_expr]
+             | V@[spec_expr] >= V@[spec_expr]
+             | V@[spec_expr] >  V@[spec_expr]
 ```
 
-## Type widening
+### 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
@@ -27,7 +31,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   |
 |-----------|---------------------|----------------------|-------------|----------------------|
 | `<=` `<` `>=` `>`        | t<sub>1</sub>     | t<sub>2</sub>        | bool        |         |
-| `==` `!=`   | t<sub>1</sub>     | t<sub>2</sub>        | bool        |         |
 | `+`         | t<sub>1</sub>     | t<sub>2</sub>        | int         | except for nat + nat |
 | `+`         | nat               | nat                  | nat         |         |
 | `-`         | t<sub>1</sub>     | t<sub>2</sub>        | int         |         |
@@ -39,11 +42,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           |         |
-| `&` <code>&#124;</code> `^` | t | t | t | |
-| `<<` `>>`   | t<sub>1</sub>     | t<sub>2</sub>        | t<sub>1</sub> |         |
 
-## 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.
 
@@ -70,7 +76,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 2530e21d20..523b664d21 100644
--- a/source/docs/guide/src/spec-bit-ops.md
+++ b/source/docs/guide/src/spec-bit-ops.md
@@ -1,6 +1,6 @@
 # Bit operators
 
-## Syntax
+### Syntax
 
 ```verus-grammar
 V@[bit_expr] ::= V@[spec_expr]  &  V@[spec_expr]
@@ -10,9 +10,16 @@ V@[bit_expr] ::= V@[spec_expr]  &  V@[spec_expr]
            | V@[spec_expr]  >> V@[spec_expr]
 ```
 
-## Definitions
+### Typing
 
-### `&`, `|`, and `^`
+| operation | LHS type            | RHS type             | result type | notes   |
+|-----------|---------------------|----------------------|-------------|----------------------|
+| `&` <code>&#124;</code> `^` | t | t | t | |
+| `<<` `>>`   | t<sub>1</sub>     | t<sub>2</sub>        | t<sub>1</sub> |         |
+
+### 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.
@@ -22,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-equality.md b/source/docs/guide/src/spec-equality.md
index a2cccad9c8..c525e7da8b 100644
--- a/source/docs/guide/src/spec-equality.md
+++ b/source/docs/guide/src/spec-equality.md
@@ -1,14 +1,27 @@
 # Spec equality (`==`)
 
+> **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
+### Syntax
 
 ```verus-grammar
 V@[equality_expr] ::= V@[spec_expr] == V@[spec_expr]
                 | V@[spec_expr] != V@[spec_expr]
 ```
 
-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.
-The `!=` operator is its negation.
+### 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 154f7fbfd4..6d20a9ac4c 100644
--- a/source/docs/guide/src/spec-expressions.md
+++ b/source/docs/guide/src/spec-expressions.md
@@ -6,11 +6,26 @@ specification expressions. This section discusses those operators.
 ## Syntax
 
 ```verus-grammar
-V@[spec_expr] ::= V@[arith_expr]
+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@[bit_expr]
             | V@[equality_expr]
             | V@[ext_eq_expr]
-            | V@[implication_expr]
             | V@[prefix_and_expr]
             | V@[prefix_or_expr]
             | V@[forall_expr]
@@ -19,4 +34,5 @@ V@[spec_expr] ::= V@[arith_expr]
             | V@[view_expr]
             | V@[spec_index_expr]
             | V@[decreases_to_expr]
+            | ( V@[spec_expr] )
 ```
diff --git a/source/docs/guide/src/spec-rust-subset.md b/source/docs/guide/src/spec-rust-subset.md
index 6c5faf435a..2ec56e5597 100644
--- a/source/docs/guide/src/spec-rust-subset.md
+++ b/source/docs/guide/src/spec-rust-subset.md
@@ -19,7 +19,8 @@ functions marked with the `when_used_as_spec` directive).
 **Syntax:**
 
 ```verus-grammar
-V@[let_expr] ::= let R@[pattern] = V@[spec_expr]; V@[spec_expr]
+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.
@@ -30,7 +31,7 @@ Spec expressions support `let`-bindings, but not `let mut`-bindings.
 
 ```verus-grammar
 V@[if_expr]     ::= if V@[spec_expr] { V@[spec_expr] } else { V@[spec_expr] }
-V@[if_let_expr] ::= if let R@[pattern] = R@[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] }
 ```
 
diff --git a/source/docs/guide/verus-grammar.py b/source/docs/guide/verus-grammar.py
index 1138ba77cc..725279e1be 100644
--- a/source/docs/guide/verus-grammar.py
+++ b/source/docs/guide/verus-grammar.py
@@ -13,6 +13,14 @@
 
 verus-grammar fenced blocks are also converted to:
   <pre class="verus-grammar"><code>...</code></pre>
+
+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
@@ -56,6 +64,10 @@ def compute_relative_link(from_path, 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
@@ -165,11 +177,99 @@ def walk_item(item, definitions):
             walk_item(sub, definitions)
 
 
+# ---------------------------------------------------------------------------
+# check subcommand
+# ---------------------------------------------------------------------------
+
+def check_mode():
+    """
+    Scan src/*.md, then report:
+      (1) grammar items defined but never referenced elsewhere
+      (2) grammar items referenced but never defined
+    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 = {}
+    # references[name] = sorted list of filenames where V@[name] appears
+    # as a non-definition occurrence (in prose or on the RHS of a rule)
+    references = {}
+
+    def add_ref(name, filename):
+        references.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 before this block
+            for vm in V_AT_RE.finditer(content[last_end:m.start()]):
+                add_ref(vm.group(1), filename)
+
+            if m.group('info').strip() == 'verus-grammar':
+                body = m.group('body')
+                # Collect definitions (LHS of ::=)
+                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
+                # Collect references (all V@[name] that are not definitions)
+                for vm in V_AT_RE.finditer(body):
+                    if vm.start() not in def_starts:
+                        add_ref(vm.group(1), filename)
+
+            last_end = m.end()
+
+        # Trailing prose
+        for vm in V_AT_RE.finditer(content[last_end:]):
+            add_ref(vm.group(1), filename)
+
+    defined = set(definitions)
+    referenced = set(references)
+
+    undefined = sorted(referenced - defined)
+    unreferenced = sorted(defined - referenced)
+
+    if undefined:
+        print("Grammar items mentioned but not defined:")
+        for name in undefined:
+            locs = ', '.join(sorted(references[name]))
+            print(f"  V@[{name}]  (in {locs})")
+    else:
+        print("No undefined grammar item references.")
+
+    print()
+
+    if unreferenced:
+        print("Grammar items defined but never referenced:")
+        for name in unreferenced:
+            print(f"  V@[{name}]  (defined in {definitions[name]})")
+    else:
+        print("No unreferenced grammar item definitions.")
+
+    return 1 if (undefined or unreferenced) 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', []):

From 6d71737f5deba8286c2508c373cb924434fa748c Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 19 May 2026 14:52:23 +0200
Subject: [PATCH 09/22] add more typing and semantics sections

---
 source/docs/guide/src/SUMMARY.md              |  2 +-
 source/docs/guide/src/prefix-and-or.md        | 26 ++++++++--
 source/docs/guide/src/reference-chained-op.md | 27 +++++++---
 .../docs/guide/src/reference-implication.md   | 32 +++++++++---
 source/docs/guide/src/spec-choose.md          | 44 +++++++----------
 .../guide/src/spec-operator-precedence.md     |  8 ---
 source/docs/guide/src/spec-quantifiers.md     | 49 ++++++-------------
 7 files changed, 103 insertions(+), 85 deletions(-)

diff --git a/source/docs/guide/src/SUMMARY.md b/source/docs/guide/src/SUMMARY.md
index 321e10aba4..becf9469cb 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)
diff --git a/source/docs/guide/src/prefix-and-or.md b/source/docs/guide/src/prefix-and-or.md
index 25d548ee75..f414e301c9 100644
--- a/source/docs/guide/src/prefix-and-or.md
+++ b/source/docs/guide/src/prefix-and-or.md
@@ -2,7 +2,7 @@
 
 For an introduction, see [Expressions and operators for specifications](operators.md).
 
-## Syntax
+### Syntax
 
 ```verus-grammar
 V@[prefix_and_expr] ::= (&&&  V@[spec_expr])+
@@ -11,5 +11,25 @@ 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)), making them convenient for
-writing large conjunctions or disjunctions without parenthesization.
+(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/reference-chained-op.md b/source/docs/guide/src/reference-chained-op.md
index 03ba570c69..92a535243e 100644
--- a/source/docs/guide/src/reference-chained-op.md
+++ b/source/docs/guide/src/reference-chained-op.md
@@ -1,16 +1,29 @@
 # Chained operators
 
-## Syntax
+### Syntax
 
 ```verus-grammar
 V@[chained_expr] ::= V@[spec_expr] (V@[cmp_op] V@[spec_expr])+
 V@[cmp_op]       ::= < | <= | > | >= | ==
 ```
 
-In spec code, equality and inequality operators can be chained. For example,
-`a <= b < c`
-is equivalent to
-`a <= b && b < c`.
+### Typing
 
-Chained inequalities support `<`, `<=`, `>`, `>=`, and `==`, and support sequences of chained
-operators of arbitrary length.
+All operands in a chained expression must have compatible types (the same rules apply
+pairwise as for non-chained comparisons). 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-implication.md b/source/docs/guide/src/reference-implication.md
index edbfc827ad..9851966f3b 100644
--- a/source/docs/guide/src/reference-implication.md
+++ b/source/docs/guide/src/reference-implication.md
@@ -1,6 +1,5 @@
-# Implication (==&gt;, &lt;==, and &lt;==&gt;)
-
-## Syntax
+# Implication (`==>`, `<==`, and `<==>`)
+### Syntax
 
 ```verus-grammar
 V@[implies_expr] ::= V@[spec_expr] ==>  V@[spec_expr]
@@ -8,10 +7,27 @@ V@[explies_expr] ::= V@[spec_expr] <==  V@[spec_expr]
 V@[iff_expr]     ::= V@[spec_expr] <==> V@[spec_expr]
 ```
 
-The operator `P ==> Q`, read _P implies Q_, is equivalent to `!P || Q`.
+### Typing
+
+All three operators require both sides to have type `bool` and return `bool`.
+
+### Semantics
 
-This can also be written backwards: `Q <== P` is equivalent to `P ==> Q`.
+`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
+```
 
-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 `==`.
+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/spec-choose.md b/source/docs/guide/src/spec-choose.md
index 20d32f523b..1d027c2109 100644
--- a/source/docs/guide/src/spec-choose.md
+++ b/source/docs/guide/src/spec-choose.md
@@ -3,33 +3,38 @@
 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 epsilon or the
+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
+### Syntax
 
 ```verus-grammar
 V@[choose_expr] ::= choose |R@[binders...]| V@[spec_expr]
 ```
 
-`SpecExpr` is a spec-mode `bool` expression. When multiple variables are bound, the result
-is a tuple `(T1, T2, ...)`.
+### Typing
 
-## Semantics
+The body V@[spec_expr] must have type `bool`. The bound variables are available as spec-mode
+variables within the body. With a single binder `x: T`, the expression has type `T`. With
+multiple binders, the expression has tuple type `(T1, T2, ...)`.
+
+### 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 arbitrary but 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).
+- 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))`.
 
-Therefore, to use the result of `choose|x: T| P(x)` 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.
 
-## Examples
+**Example:**
 
 ```rust
 // Requires a proof that such an i exists; choose picks one.
@@ -45,14 +50,3 @@ proof fn get_zero_index(s: Seq<int>) -> (i: int)
 // Multiple variables — result is a tuple.
 let (i, j): (int, int) = choose|i: int, j: int| less_than(i, j);
 ```
-
-## Relationship to `exists`
-
-`choose` and `exists` are complementary:
-
-- `exists|x: T| P(x)` asserts that a satisfying value *exists*.
-- `choose|x: T| P(x)` *extracts* a satisfying value, given that one exists.
-
-Triggers on a `choose` expression work the same way as on `exists`: Verus uses them to
-find a witness in the proof context. See [Trigger annotations](./trigger-annotations.md)
-for details.
diff --git a/source/docs/guide/src/spec-operator-precedence.md b/source/docs/guide/src/spec-operator-precedence.md
index 7dc4534729..648fbc4d60 100644
--- a/source/docs/guide/src/spec-operator-precedence.md
+++ b/source/docs/guide/src/spec-operator-precedence.md
@@ -1,13 +1,5 @@
 # Operator Precedence
 
-## Syntax
-
-```verus-grammar
-V@[spec_expr] ::= V@[spec_expr] R@[binary_op] V@[spec_expr]
-            | R@[unary_op] V@[spec_expr]
-            | ( V@[spec_expr] )
-```
-
 The table below defines operator precedence from tightest-binding (top) to loosest-binding (bottom).
 
 | Operator                 | Associativity         |
diff --git a/source/docs/guide/src/spec-quantifiers.md b/source/docs/guide/src/spec-quantifiers.md
index d1af9f051c..ae21a225cd 100644
--- a/source/docs/guide/src/spec-quantifiers.md
+++ b/source/docs/guide/src/spec-quantifiers.md
@@ -4,52 +4,35 @@ 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 with type `bool`.
+Both `forall` and `exists` are **spec-mode only** expressions.
 
-## forall
-
-**Syntax:**
+### Syntax
 
 ```verus-grammar
 V@[forall_expr] ::= forall |R@[binders...]| V@[spec_expr]
+V@[exists_expr] ::= exists |R@[binders...]| V@[spec_expr]
 ```
 
-`SpecExpr` is a spec-mode `bool` expression. The bound variables are in scope in `SpecExpr`
-and are also spec-mode.
+The body V@[spec_expr] may be preceded by [trigger annotations](./trigger-annotations.md).
 
-**Semantics:** `forall|x: T| P(x)` is `true` if and only if `P(x)` is `true` for every
-value `x` of type `T`.
+### Typing
 
-**Example:**
+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`.
 
-```rust
-// All elements of s are positive
-forall|i: int| 0 <= i < s.len() ==> s[i] > 0
-```
+### Semantics
 
-## exists
+`forall|x: T| P(x)` is `true` if and only if `P(x)` is `true` for every value `x` of type `T`.
 
-**Syntax:**
+`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:
 
-```verus-grammar
-V@[exists_expr] ::= exists |R@[binders...]| V@[spec_expr]
 ```
-
-**Semantics:** `exists|x: T| P(x)` is `true` if and only if there is at least one value
-`x` of type `T` for which `P(x)` is `true`. The dual identity holds:
-`exists|x: T| P(x)` is equivalent to `!forall|x: T| !P(x)`.
-
-**Example:**
-
-```rust
-// Some element of s is zero
-exists|i: int| 0 <= i < s.len() && s[i] == 0
+exists|x: T| P(x)  ≡  !forall|x: T| !P(x)
 ```
 
-## Multiple bound variables
-
-Both `forall` and `exists` support binding multiple variables simultaneously.
-This is equivalent to nesting single-variable quantifiers:
+Both quantifiers support binding multiple variables simultaneously, which is equivalent to
+nesting single-variable quantifiers:
 
 ```rust
 // These two are equivalent:
@@ -57,10 +40,10 @@ forall|i: int, j: int| i < j ==> f(i) <= f(j)
 forall|i: int| forall|j: int| i < j ==> f(i) <= f(j)
 ```
 
-## Triggers
+### 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
+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

From 21424c89d9a59ce36bad32c326fb25073a6087af Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 19 May 2026 14:59:41 +0200
Subject: [PATCH 10/22] more fixes

---
 source/docs/guide/src/ref-extensional-equality.md | 2 +-
 source/docs/guide/src/spec-bit-ops.md             | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/source/docs/guide/src/ref-extensional-equality.md b/source/docs/guide/src/ref-extensional-equality.md
index a3010f9d69..5ee780dce5 100644
--- a/source/docs/guide/src/ref-extensional-equality.md
+++ b/source/docs/guide/src/ref-extensional-equality.md
@@ -8,7 +8,7 @@ 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.
+See [the guide page](extensional_equality.md) for an introductory explanation with motivation.
 
 ### Syntax
 
diff --git a/source/docs/guide/src/spec-bit-ops.md b/source/docs/guide/src/spec-bit-ops.md
index 523b664d21..b143f7405b 100644
--- a/source/docs/guide/src/spec-bit-ops.md
+++ b/source/docs/guide/src/spec-bit-ops.md
@@ -12,10 +12,10 @@ V@[bit_expr] ::= V@[spec_expr]  &  V@[spec_expr]
 
 ### Typing
 
-| operation | LHS type            | RHS type             | result type | notes   |
-|-----------|---------------------|----------------------|-------------|----------------------|
-| `&` <code>&#124;</code> `^` | t | t | t | |
-| `<<` `>>`   | t<sub>1</sub>     | t<sub>2</sub>        | t<sub>1</sub> |         |
+| operation | LHS type            | RHS type             | result type   |
+|-----------|---------------------|----------------------|---------------|
+| `&` <code>&#124;</code> `^` | t | t                    | t             |
+| `<<` `>>`   | t<sub>1</sub>     | t<sub>2</sub>        | t<sub>1</sub> |
 
 ### Semantics
 

From 232d11f115605a4d5dce36046caaffd278a13751 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 19 May 2026 15:08:26 +0200
Subject: [PATCH 11/22] more fixes

---
 source/docs/guide/src/reference-at-sign.md      |  2 +-
 source/docs/guide/src/reference-decreases-to.md |  9 +++++++--
 source/docs/guide/src/spec-choose.md            |  6 ++++--
 source/docs/guide/src/spec-expressions.md       |  2 ++
 source/docs/guide/src/spec-quantifiers.md       |  5 +----
 source/docs/guide/src/trigger-annotations.md    | 10 +++++-----
 source/docs/guide/verus-grammar.py              | 15 ++-------------
 7 files changed, 22 insertions(+), 27 deletions(-)

diff --git a/source/docs/guide/src/reference-at-sign.md b/source/docs/guide/src/reference-at-sign.md
index f444b8f283..be763c4cbe 100644
--- a/source/docs/guide/src/reference-at-sign.md
+++ b/source/docs/guide/src/reference-at-sign.md
@@ -3,7 +3,7 @@
 ## Syntax
 
 ```verus-grammar
-V@[view_expr] ::= R@[expr] @
+V@[view_expr] ::= V@[spec_expr] @
 ```
 
 The expression `expr@` is a shorthand for `expr.view()`. The `view()` function is a Verus
diff --git a/source/docs/guide/src/reference-decreases-to.md b/source/docs/guide/src/reference-decreases-to.md
index ee5c1b5951..bcebde8950 100644
--- a/source/docs/guide/src/reference-decreases-to.md
+++ b/source/docs/guide/src/reference-decreases-to.md
@@ -13,13 +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.
 
-## Syntax
+### Syntax
 
 ```verus-grammar
 V@[decreases_to_expr] ::= decreases_to!( V@[spec_expr] (, V@[spec_expr])* => V@[spec_expr] (, V@[spec_expr])* )
 ```
 
-## Definition
+### 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
 <code>e<sub>1</sub>, e<sub>2</sub>, ..., e<sub>n</sub></code>
diff --git a/source/docs/guide/src/spec-choose.md b/source/docs/guide/src/spec-choose.md
index 1d027c2109..2145bb1787 100644
--- a/source/docs/guide/src/spec-choose.md
+++ b/source/docs/guide/src/spec-choose.md
@@ -15,8 +15,10 @@ V@[choose_expr] ::= choose |R@[binders...]| V@[spec_expr]
 ### Typing
 
 The body V@[spec_expr] must have type `bool`. The bound variables are available as spec-mode
-variables within the body. With a single binder `x: T`, the expression has type `T`. With
-multiple binders, the expression has tuple type `(T1, T2, ...)`.
+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
 
diff --git a/source/docs/guide/src/spec-expressions.md b/source/docs/guide/src/spec-expressions.md
index 6d20a9ac4c..9afa4cec47 100644
--- a/source/docs/guide/src/spec-expressions.md
+++ b/source/docs/guide/src/spec-expressions.md
@@ -31,6 +31,8 @@ V@[spec_expr] ::= V@[fn_call_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@[decreases_to_expr]
diff --git a/source/docs/guide/src/spec-quantifiers.md b/source/docs/guide/src/spec-quantifiers.md
index ae21a225cd..fb87ab51c1 100644
--- a/source/docs/guide/src/spec-quantifiers.md
+++ b/source/docs/guide/src/spec-quantifiers.md
@@ -25,7 +25,7 @@ variables within the body. Both `forall` and `exists` expressions have type `boo
 `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:
+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)
@@ -57,8 +57,5 @@ automatically, or they can be specified explicitly using annotations on the quan
 | `#![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 |
 
-A trigger expression must be a function call, a field access, or a bitwise operator —
-arithmetic and boolean operators are not valid triggers.
-
 For full details on how Verus selects and validates trigger groups, see
 [Trigger annotations](./trigger-annotations.md).
diff --git a/source/docs/guide/src/trigger-annotations.md b/source/docs/guide/src/trigger-annotations.md
index 8fe27c7928..ada94cf8df 100644
--- a/source/docs/guide/src/trigger-annotations.md
+++ b/source/docs/guide/src/trigger-annotations.md
@@ -12,11 +12,11 @@ This page explains the procedure Verus uses to determine these triggers from Ver
 ## Syntax
 
 ```verus-grammar
-V@[root_trigger_attr]  ::= #![trigger V@[spec_expr] (, V@[spec_expr])*]
-                     | #![auto]
-                     | #![all_triggers]
-V@[inner_trigger_attr] ::= #[trigger] V@[spec_expr]
-                     | #[trigger(R@[n])] V@[spec_expr]
+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] annotations appear at the start of the quantifier body and configure
diff --git a/source/docs/guide/verus-grammar.py b/source/docs/guide/verus-grammar.py
index 725279e1be..3c2597ce5d 100644
--- a/source/docs/guide/verus-grammar.py
+++ b/source/docs/guide/verus-grammar.py
@@ -193,8 +193,8 @@ def check_mode():
 
     # definitions[name] = filename where V@[name] ::= first appears
     definitions = {}
-    # references[name] = sorted list of filenames where V@[name] appears
-    # as a non-definition occurrence (in prose or on the RHS of a rule)
+    # references[name] = set of filenames where V@[name] appears
+    # as a non-definition occurrence inside a verus-grammar block
     references = {}
 
     def add_ref(name, filename):
@@ -206,12 +206,7 @@ def add_ref(name, filename):
         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 before this block
-            for vm in V_AT_RE.finditer(content[last_end:m.start()]):
-                add_ref(vm.group(1), filename)
-
             if m.group('info').strip() == 'verus-grammar':
                 body = m.group('body')
                 # Collect definitions (LHS of ::=)
@@ -226,12 +221,6 @@ def add_ref(name, filename):
                     if vm.start() not in def_starts:
                         add_ref(vm.group(1), filename)
 
-            last_end = m.end()
-
-        # Trailing prose
-        for vm in V_AT_RE.finditer(content[last_end:]):
-            add_ref(vm.group(1), filename)
-
     defined = set(definitions)
     referenced = set(references)
 

From 9b657dfc7973c17ad0d48b43dad6cb661a16fd01 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 19 May 2026 15:18:03 +0200
Subject: [PATCH 12/22] more fixes

---
 source/docs/guide/src/spec-arithmetic.md      |  9 ++--
 source/docs/guide/src/spec-choose.md          |  2 +
 source/docs/guide/src/spec-expressions.md     |  1 +
 .../guide/src/spec-operator-precedence.md     | 46 +++++++++----------
 source/docs/guide/src/spec-quantifiers.md     |  2 +-
 source/docs/guide/src/trigger-annotations.md  |  4 +-
 6 files changed, 34 insertions(+), 30 deletions(-)

diff --git a/source/docs/guide/src/spec-arithmetic.md b/source/docs/guide/src/spec-arithmetic.md
index 1e7e1993e1..3ed9d4d6d2 100644
--- a/source/docs/guide/src/spec-arithmetic.md
+++ b/source/docs/guide/src/spec-arithmetic.md
@@ -15,10 +15,11 @@ 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@[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
diff --git a/source/docs/guide/src/spec-choose.md b/source/docs/guide/src/spec-choose.md
index 2145bb1787..4154fd5147 100644
--- a/source/docs/guide/src/spec-choose.md
+++ b/source/docs/guide/src/spec-choose.md
@@ -12,6 +12,8 @@ a given predicate. It is the Hilbert choice operator (also known as the epsilon
 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
diff --git a/source/docs/guide/src/spec-expressions.md b/source/docs/guide/src/spec-expressions.md
index 9afa4cec47..3fb9452585 100644
--- a/source/docs/guide/src/spec-expressions.md
+++ b/source/docs/guide/src/spec-expressions.md
@@ -23,6 +23,7 @@ V@[spec_expr] ::= V@[fn_call_expr]
             | V@[explies_expr]
             | V@[iff_expr]
             | V@[arith_expr]
+            | V@[ineq_expr]
             | V@[bit_expr]
             | V@[equality_expr]
             | V@[ext_eq_expr]
diff --git a/source/docs/guide/src/spec-operator-precedence.md b/source/docs/guide/src/spec-operator-precedence.md
index 648fbc4d60..a4b48ffdf4 100644
--- a/source/docs/guide/src/spec-operator-precedence.md
+++ b/source/docs/guide/src/spec-operator-precedence.md
@@ -2,29 +2,29 @@
 
 The table below defines operator precedence from tightest-binding (top) to loosest-binding (bottom).
 
-| 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                  |
-| [<code>&#124;</code>](./spec-bit-ops.md)                   | left                  |
-| [`!==` `==` `!=`](./spec-equality.md) `<=` `<` `>=` `>`  | requires parentheses  |
-| `&&`                       | left                  |
-| <code>&#124;&#124;</code>             | 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                  |
-| [<code>&#124;&#124;&#124;</code>](./prefix-and-or.md)       | left                  |
-| **Binds looser**                                 |
+| Operator                                                                             | Associativity        | Grammar                                                 |
+|--------------------------------------------------------------------------------------|----------------------|---------------------------------------------------------|
+| **Binds tighter**                                                                    |                      |                                                         |
+| [`.` `->`](./datatypes_struct.md)                                                    | left                 |                                                         |
+| [`is` `matches`](./datatypes_enum.md)                                                | left                 |                                                         |
+| [`*` `/` `%`](./spec-arithmetic.md)                                                  | left                 | V@[arith_expr]                                          |
+| [`+` `-`](./spec-arithmetic.md)                                                      | left                 | V@[arith_expr]                                          |
+| [`<<` `>>`](./spec-bit-ops.md)                                                       | left                 | V@[shl_expr] V@[shr_expr]                               |
+| [`&`](./spec-bit-ops.md)                                                             | left                 | V@[bit_and_expr]                                        |
+| [`^`](./spec-bit-ops.md)                                                             | left                 | V@[bit_xor_expr]                                        |
+| [<code>&#124;</code>](./spec-bit-ops.md)                                             | left                 | V@[bit_or_expr]                                         |
+| [`!==` `==` `!=`](./spec-equality.md) `<=` `<` `>=` `>`                              | requires parentheses | V@[equality_expr] V@[ineq_expr]                         |
+| `&&`                                                                                 | left                 | V@[and_expr]                                            |
+| <code>&#124;&#124;</code>                                                            | 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]                                     |
+| [<code>&#124;&#124;&#124;</code>](./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 fb87ab51c1..d2278f4e33 100644
--- a/source/docs/guide/src/spec-quantifiers.md
+++ b/source/docs/guide/src/spec-quantifiers.md
@@ -13,7 +13,7 @@ V@[forall_expr] ::= forall |R@[binders...]| V@[spec_expr]
 V@[exists_expr] ::= exists |R@[binders...]| V@[spec_expr]
 ```
 
-The body V@[spec_expr] may be preceded by [trigger annotations](./trigger-annotations.md).
+The body V@[spec_expr] may include [trigger annotations](./trigger-annotations.md).
 
 ### Typing
 
diff --git a/source/docs/guide/src/trigger-annotations.md b/source/docs/guide/src/trigger-annotations.md
index ada94cf8df..1c869f5db9 100644
--- a/source/docs/guide/src/trigger-annotations.md
+++ b/source/docs/guide/src/trigger-annotations.md
@@ -19,8 +19,8 @@ V@[inner_trigger_attr_expr] ::= #[trigger] V@[spec_expr]
                           | #[trigger(R@[n])] V@[spec_expr]
 ```
 
-V@[root_trigger_attr] annotations appear at the start of the quantifier body and configure
-trigger selection for the whole quantifier. V@[inner_trigger_attr] annotations appear on
+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

From a4a3e3d34f2c4c9ac022891e329cad9e606099c0 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 19 May 2026 15:22:07 +0200
Subject: [PATCH 13/22] another fix to the check script

---
 source/docs/guide/verus-grammar.py | 81 ++++++++++++++++++++++--------
 1 file changed, 61 insertions(+), 20 deletions(-)

diff --git a/source/docs/guide/verus-grammar.py b/source/docs/guide/verus-grammar.py
index 3c2597ce5d..28672bed36 100644
--- a/source/docs/guide/verus-grammar.py
+++ b/source/docs/guide/verus-grammar.py
@@ -181,11 +181,24 @@ def walk_item(item, 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 defined but never referenced elsewhere
-      (2) grammar items referenced but never defined
+      (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__))
@@ -193,12 +206,16 @@ def check_mode():
 
     # definitions[name] = filename where V@[name] ::= first appears
     definitions = {}
-    # references[name] = set of filenames where V@[name] appears
-    # as a non-definition occurrence inside a verus-grammar block
-    references = {}
+    # 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_ref(name, filename):
-        references.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'):
@@ -206,45 +223,69 @@ def add_ref(name, filename):
         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')
-                # Collect definitions (LHS of ::=)
                 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
-                # Collect references (all V@[name] that are not definitions)
                 for vm in V_AT_RE.finditer(body):
                     if vm.start() not in def_starts:
-                        add_ref(vm.group(1), filename)
+                        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)
-    referenced = set(references)
 
-    undefined = sorted(referenced - defined)
-    unreferenced = sorted(defined - referenced)
+    undefined_grammar = sorted(set(grammar_refs) - defined)
+    unreferenced = sorted(defined - set(grammar_refs))
+    undefined_prose = sorted(set(prose_refs) - defined)
 
-    if undefined:
-        print("Grammar items mentioned but not defined:")
-        for name in undefined:
-            locs = ', '.join(sorted(references[name]))
+    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 item references.")
+        print("No undefined grammar-block references.")
 
     print()
 
     if unreferenced:
-        print("Grammar items defined but never referenced:")
+        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.")
 
-    return 1 if (undefined or unreferenced) else 0
+    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
 
 
 # ---------------------------------------------------------------------------

From c32c4526b99cebdf69eac07015c13574dc3420ac Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 19 May 2026 15:38:55 +0200
Subject: [PATCH 14/22] superscripts

---
 source/docs/guide/src/reference-types.md          | 5 -----
 source/docs/guide/src/spec-arithmetic.md          | 4 ++--
 source/docs/guide/src/spec-operator-precedence.md | 8 ++++----
 source/docs/guide/src/spec-rust-subset.md         | 6 +++---
 source/docs/guide/verus-grammar.py                | 5 +++++
 5 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/source/docs/guide/src/reference-types.md b/source/docs/guide/src/reference-types.md
index 85b9523dff..91a1172dbe 100644
--- a/source/docs/guide/src/reference-types.md
+++ b/source/docs/guide/src/reference-types.md
@@ -245,8 +245,3 @@ Verus supports [string literal expressions](https://doc.rust-lang.org/reference/
 The primary spec operator for strings is the "view" operator, `s@` or `s.view()`.
 
 
-
-## Slices and arrays
-
-
-## Mode wrappers: `Ghost` and `Tracked`
diff --git a/source/docs/guide/src/spec-arithmetic.md b/source/docs/guide/src/spec-arithmetic.md
index 3ed9d4d6d2..fcf0cf9463 100644
--- a/source/docs/guide/src/spec-arithmetic.md
+++ b/source/docs/guide/src/spec-arithmetic.md
@@ -9,10 +9,10 @@ For an introduction to Verus arithmetic, see
 ### Syntax
 
 ```verus-grammar
-V@[arith_expr] ::= V@[spec_expr] + V@[spec_expr]
+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@[spec_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 a4b48ffdf4..177f3a2d17 100644
--- a/source/docs/guide/src/spec-operator-precedence.md
+++ b/source/docs/guide/src/spec-operator-precedence.md
@@ -9,10 +9,10 @@ The table below defines operator precedence from tightest-binding (top) to loose
 | [`is` `matches`](./datatypes_enum.md)                                                | left                 |                                                         |
 | [`*` `/` `%`](./spec-arithmetic.md)                                                  | left                 | V@[arith_expr]                                          |
 | [`+` `-`](./spec-arithmetic.md)                                                      | left                 | V@[arith_expr]                                          |
-| [`<<` `>>`](./spec-bit-ops.md)                                                       | left                 | V@[shl_expr] V@[shr_expr]                               |
-| [`&`](./spec-bit-ops.md)                                                             | left                 | V@[bit_and_expr]                                        |
-| [`^`](./spec-bit-ops.md)                                                             | left                 | V@[bit_xor_expr]                                        |
-| [<code>&#124;</code>](./spec-bit-ops.md)                                             | left                 | V@[bit_or_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]                                            |
+| [<code>&#124;</code>](./spec-bit-ops.md)                                             | left                 | V@[bit_expr]                                            |
 | [`!==` `==` `!=`](./spec-equality.md) `<=` `<` `>=` `>`                              | requires parentheses | V@[equality_expr] V@[ineq_expr]                         |
 | `&&`                                                                                 | left                 | V@[and_expr]                                            |
 | <code>&#124;&#124;</code>                                                            | left                 | V@[or_expr]                                             |
diff --git a/source/docs/guide/src/spec-rust-subset.md b/source/docs/guide/src/spec-rust-subset.md
index 2ec56e5597..0d3725f75d 100644
--- a/source/docs/guide/src/spec-rust-subset.md
+++ b/source/docs/guide/src/spec-rust-subset.md
@@ -66,10 +66,10 @@ This is not the same thing as `==` in exec-mode; see [more on `==`](./spec-equal
 **Syntax:**
 
 ```verus-grammar
-V@[arith_expr] ::= V@[spec_expr] + V@[spec_expr]
+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@[spec_expr] % V@[spec_expr]
 ```
@@ -83,7 +83,7 @@ and `nat` types. See [more on arithmetic](./spec-arithmetic.md).
 
 ```verus-grammar
 V@[ref_expr]   ::= & V@[spec_expr]
-V@[deref_expr] ::= * V@[spec_expr]
+V@[deref_expr] ::= \* V@[spec_expr]
 ```
 
 Verus attempts to ignore `Box` and references as much as possible in spec mode.
diff --git a/source/docs/guide/verus-grammar.py b/source/docs/guide/verus-grammar.py
index 28672bed36..5410104265 100644
--- a/source/docs/guide/verus-grammar.py
+++ b/source/docs/guide/verus-grammar.py
@@ -120,6 +120,11 @@ def replace_v_ref(m):
     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('?', '<sup>?</sup>')
+    body = body.replace('+', '<sup>+</sup>')
+    body = body.replace('*', '<sup>*</sup>')
+    body = body.replace('\\<sup>+</sup>', '+')
+    body = body.replace('\\<sup>*</sup>', '*')
+    body = body.replace('\\<sup>?</sup>', '?')
     return body
 
 

From 756ecd212a08056a14ffc9061bb606002c345e20 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Tue, 19 May 2026 20:22:38 +0200
Subject: [PATCH 15/22] correct the typing for chained ops

---
 source/docs/guide/src/reference-chained-op.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/source/docs/guide/src/reference-chained-op.md b/source/docs/guide/src/reference-chained-op.md
index 92a535243e..883ffdb393 100644
--- a/source/docs/guide/src/reference-chained-op.md
+++ b/source/docs/guide/src/reference-chained-op.md
@@ -9,8 +9,8 @@ V@[cmp_op]       ::= < | <= | > | >= | ==
 
 ### Typing
 
-All operands in a chained expression must have compatible types (the same rules apply
-pairwise as for non-chained comparisons). The expression returns `bool`.
+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.
 

From d5097fd41a8249216632c92e36defcfadc54dd6f Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Wed, 20 May 2026 09:45:10 +0200
Subject: [PATCH 16/22] add a 'has' page and tweak the view and index pages

---
 source/docs/guide/src/SUMMARY.md              |  1 +
 source/docs/guide/src/reference-at-sign.md    | 20 +++++++++++++-----
 source/docs/guide/src/reference-has.md        | 21 +++++++++++++++++++
 source/docs/guide/src/reference-spec-index.md | 14 +++++++------
 source/docs/guide/src/spec-expressions.md     |  1 +
 5 files changed, 46 insertions(+), 11 deletions(-)
 create mode 100644 source/docs/guide/src/reference-has.md

diff --git a/source/docs/guide/src/SUMMARY.md b/source/docs/guide/src/SUMMARY.md
index becf9469cb..e23570f77c 100644
--- a/source/docs/guide/src/SUMMARY.md
+++ b/source/docs/guide/src/SUMMARY.md
@@ -152,6 +152,7 @@
   - [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)
   - [`decreases_to!`](./reference-decreases-to.md)
 - [Types](./reference-types.md)
 - [Proof features]()
diff --git a/source/docs/guide/src/reference-at-sign.md b/source/docs/guide/src/reference-at-sign.md
index be763c4cbe..d9afc4913e 100644
--- a/source/docs/guide/src/reference-at-sign.md
+++ b/source/docs/guide/src/reference-at-sign.md
@@ -1,12 +1,22 @@
 # The view function `@`
 
-## Syntax
+### Syntax
 
 ```verus-grammar
 V@[view_expr] ::= V@[spec_expr] @
 ```
 
-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.
+### 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-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-spec-index.md b/source/docs/guide/src/reference-spec-index.md
index 462458ebe9..55679361d7 100644
--- a/source/docs/guide/src/reference-spec-index.md
+++ b/source/docs/guide/src/reference-spec-index.md
@@ -1,17 +1,19 @@
 # Spec index operator []
 
-## Syntax
+### Syntax
 
 ```verus-grammar
 V@[spec_index_expr] ::= V@[spec_expr] [ V@[spec_expr] ]
 ```
 
-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).
+### Desugaring
 
-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.
+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/spec-expressions.md b/source/docs/guide/src/spec-expressions.md
index 3fb9452585..cb686f69a0 100644
--- a/source/docs/guide/src/spec-expressions.md
+++ b/source/docs/guide/src/spec-expressions.md
@@ -36,6 +36,7 @@ V@[spec_expr] ::= V@[fn_call_expr]
             | V@[inner_trigger_attr_expr]
             | V@[view_expr]
             | V@[spec_index_expr]
+            | V@[has_expr]
             | V@[decreases_to_expr]
             | ( V@[spec_expr] )
 ```

From e05e70c907a8178512cb72df065a591b813b35f3 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Wed, 20 May 2026 10:15:58 +0200
Subject: [PATCH 17/22] add pages for 'is' and 'matches'

---
 source/docs/guide/src/SUMMARY.md              |  2 ++
 source/docs/guide/src/reference-is.md         | 28 +++++++++++++++
 source/docs/guide/src/reference-matches.md    | 36 +++++++++++++++++++
 .../guide/src/spec-operator-precedence.md     |  2 +-
 4 files changed, 67 insertions(+), 1 deletion(-)
 create mode 100644 source/docs/guide/src/reference-is.md
 create mode 100644 source/docs/guide/src/reference-matches.md

diff --git a/source/docs/guide/src/SUMMARY.md b/source/docs/guide/src/SUMMARY.md
index e23570f77c..7303c5d08c 100644
--- a/source/docs/guide/src/SUMMARY.md
+++ b/source/docs/guide/src/SUMMARY.md
@@ -153,6 +153,8 @@
   - [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]()
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/spec-operator-precedence.md b/source/docs/guide/src/spec-operator-precedence.md
index 177f3a2d17..2ff85462a1 100644
--- a/source/docs/guide/src/spec-operator-precedence.md
+++ b/source/docs/guide/src/spec-operator-precedence.md
@@ -6,7 +6,7 @@ The table below defines operator precedence from tightest-binding (top) to loose
 |--------------------------------------------------------------------------------------|----------------------|---------------------------------------------------------|
 | **Binds tighter**                                                                    |                      |                                                         |
 | [`.` `->`](./datatypes_struct.md)                                                    | left                 |                                                         |
-| [`is` `matches`](./datatypes_enum.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]                                            |

From ecb98a3d1cc86f3eb22f4b26d41be942082b62b3 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Wed, 20 May 2026 11:28:10 +0200
Subject: [PATCH 18/22] more cleanup

---
 source/docs/guide/src/SUMMARY.md              |  2 +-
 source/docs/guide/src/char.md                 | 17 --------
 source/docs/guide/src/reference-assert-by.md  | 14 ++++++-
 .../guide/src/reference-assert-forall-by.md   | 40 +++++++++----------
 .../guide/src/reference-exec-signature.md     |  4 +-
 .../guide/src/reference-proof-signature.md    | 40 +++++++++++++------
 .../docs/guide/src/reference-reveal-hide.md   | 10 +++++
 .../docs/guide/src/reference-reveal-strlit.md | 22 ++++++++++
 .../guide/src/reference-spec-signature.md     | 14 +++----
 9 files changed, 101 insertions(+), 62 deletions(-)
 delete mode 100644 source/docs/guide/src/char.md
 create mode 100644 source/docs/guide/src/reference-reveal-strlit.md

diff --git a/source/docs/guide/src/SUMMARY.md b/source/docs/guide/src/SUMMARY.md
index 7303c5d08c..663f5e7893 100644
--- a/source/docs/guide/src/SUMMARY.md
+++ b/source/docs/guide/src/SUMMARY.md
@@ -165,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)
@@ -193,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/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-exec-signature.md b/source/docs/guide/src/reference-exec-signature.md
index 1a1551f963..e725dc4a43 100644
--- a/source/docs/guide/src/reference-exec-signature.md
+++ b/source/docs/guide/src/reference-exec-signature.md
@@ -3,8 +3,8 @@
 The general form of an `exec` function signature takes the form:
 
 ```verus-grammar
-V@[fn_with_verus_sig] :=
-    fn R@[function_name] R@[generics]?(R@[args...]) -> R@[return_type_and_name]?
+V@[exec_fn_with_verus_sig] ::=
+    R@[visibility]? exec? fn R@[function_name] R@[generics]?(R@[args...]) ( -> V@[return_type_and_name] )?
         R@[where_clause]?
         V@[requires_clause]?
         V@[ensures_clause]?
diff --git a/source/docs/guide/src/reference-proof-signature.md b/source/docs/guide/src/reference-proof-signature.md
index fe21e858f1..df584b7566 100644
--- a/source/docs/guide/src/reference-proof-signature.md
+++ b/source/docs/guide/src/reference-proof-signature.md
@@ -2,31 +2,45 @@
 
 The general form of a `proof` function signature takes the form:
 
-<pre>
-<code class="hljs">proof fn <span style="color: #800000; font-style: italic">function_name</span> <span style="color: #800000; font-style: italic">generics</span><sup>?</sup>(<span style="color: #800000; font-style: italic">args...</span>) -&gt; <span style="color: #800000; font-style: italic">return_type_and_name</span><sup>?</sup>
-    <span style="color: #800000; font-style: italic">where_clause</span><sup>?</sup>
-    <span style="color: #000080; font-style: italic">requires_clause</span><sup>?</sup>
-    <span style="color: #000080; font-style: italic">ensures_clause</span><sup>?</sup>
-    <span style="color: #000080; font-style: italic">returns_clause</span><sup>?</sup>
-    <span style="color: #000080; font-style: italic">invariants_clause</span><sup>?</sup>
-</code>
-</pre>
+```verus-grammar
+V@[proof_fn_with_verus_sig] ::= V@[proof_fn_proved] | V@[proof_fn_axiom]
+
+V@[proof_fn_proved] ::=
+    R@[visibility]? proof fn R@[function_name] R@[generics]?(R@[args...]) ( -> V@[return_type_and_name] )?
+        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]? axiom fn R@[function_name] R@[generics]?(R@[args...]) ( -> V@[return_type_and_name] )?
+        R@[where_clause]?
+        V@[requires_clause]?
+        V@[ensures_clause]?
+        V@[returns_clause]?
+        V@[invariants_clause]?
+        V@[decreases_clause]?
+        ;
+```
 
 ## Function specification
 
 The elements of the function specification are given by the signature clauses.
 
 **The precondition.**
-The <code class="hljs"><span style="color: #000080; font-style: italic">requires_clause</span></code> is the precondition.
+The V@[requires_clause] is the precondition.
 
 **The postcondition.**
-The <code class="hljs"><span style="color: #000080; font-style: italic">ensures_clause</span></code>
+The V@[ensures_clause]
 and the
-<code class="hljs"><span style="color: #000080; font-style: italic">returns_clause</span></code>
+V@[returns_clause]
 together form the postcondition.
 
 **The invariants.**
-The <code class="hljs"><span style="color: #000080; font-style: italic">invariants_clause</span></code> 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-signature.md b/source/docs/guide/src/reference-spec-signature.md
index 69c0cdc463..28f167058e 100644
--- a/source/docs/guide/src/reference-spec-signature.md
+++ b/source/docs/guide/src/reference-spec-signature.md
@@ -2,13 +2,13 @@
 
 The general form of a `spec` function signature takes the form:
 
-<pre>
-<code class="hljs">spec fn <span style="color: #800000; font-style: italic">function_name</span> <span style="color: #800000; font-style: italic">generics</span><sup>?</sup>(<span style="color: #800000; font-style: italic">args...</span>) -&gt; <span style="color: #800000; font-style: italic">return_type</span><sup>?</sup>
-    <span style="color: #800000; font-style: italic">where_clause</span><sup>?</sup>
-    <span style="color: #000080; font-style: italic">recommends_clause</span><sup>?</sup>
-    <span style="color: #000080; font-style: italic">decreases_clause</span><sup>?</sup>
-</code>
-</pre>
+```verus-grammar
+V@[spec_fn_with_verus_sig] ::=
+    R@[visibility]? spec fn R@[function_name] R@[generics]?(R@[args...]) -> R@[type]
+        R@[where_clause]?
+        V@[recommends_clause]?
+        V@[decreases_clause]?
+```
 
 ## The `recommends` clause
 

From 8fb8f8f744c7c4e9e15f2f31e98c1b694f04ae3e Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Wed, 20 May 2026 11:48:55 +0200
Subject: [PATCH 19/22] more cleanup and updating pages

---
 .../src/reference-assume-specification.md     | 47 ++++++++++++++-----
 source/docs/guide/src/reference-global.md     | 10 ++--
 2 files changed, 41 insertions(+), 16 deletions(-)

diff --git a/source/docs/guide/src/reference-assume-specification.md b/source/docs/guide/src/reference-assume-specification.md
index ace5ab9c3d..26924cb17c 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:
 
-<pre>
-<code class="hljs">assume_specification <span style="color: #800000; font-style: italic">generics</span><sup>?</sup> [ <span style="color: #800000; font-style: italic">function_path</span> ] (<span style="color: #800000; font-style: italic">args...</span>) -&gt; <span style="color: #800000; font-style: italic">return_type_and_name</span><sup>?</sup>
-    <span style="color: #800000; font-style: italic">where_clause</span><sup>?</sup>
-    <span style="color: #800000; font-style: italic">requires_clause</span><sup>?</sup>
-    <span style="color: #800000; font-style: italic">ensures_clause</span><sup>?</sup>
-    <span style="color: #800000; font-style: italic">returns_clause</span><sup>?</sup>
-    <span style="color: #800000; font-style: italic">invariants_clause</span><sup>?</sup>
-    <span style="color: #800000; font-style: italic">unwind_clause</span><sup>?</sup>
-    ;
-</code>
-</pre>
+```verus-grammar
+assume_specification_item ::=
+    visibility? assume_specification R@[generics]? [ R@[function_path] ] (R@[args...]) ( -> V@[return_type_and_name] )?
+        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 <code><span style="color: #800000; font-style: italic">function_path</span></code> should have the form `Type::method_name`,
 using "turbofish syntax" for the type (e.g., `Vec::<T>`).
-For trait methods, the <code><span style="color: #800000; font-style: italic">function_path</span></code> should use the "qualified self" form, `<Type as Trait>::method_name`.
+For trait methods, the <code><span style="color: #800000; font-style: italic">function_path</span></code> should use the ["qualified self"](https://doc.rust-lang.org/reference/paths.html#qualified-paths) form, `<Type as Trait>::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 [<bool as Clone>::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-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::<T>() == n` and `align_of::<T> == m` for use in Verus proofs
+ * Exports one or both of the axioms `size_of::<T>() == n` and `align_of::<T> == 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

From 36897a0681a485bda71c659a70364d6e57531036 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Wed, 20 May 2026 13:24:36 +0200
Subject: [PATCH 20/22] more cleanup

---
 source/docs/guide/src/erasure.md              |  2 +-
 source/docs/guide/src/reference-decreases.md  |  7 ++--
 .../guide/src/reference-exec-signature.md     |  8 +++--
 .../guide/src/reference-proof-signature.md    | 10 ++++--
 .../guide/src/reference-spec-signature.md     | 34 +++++++++++++++++--
 source/docs/guide/src/reference-unions.md     |  2 +-
 source/docs/guide/src/spec-rust-subset.md     |  2 +-
 7 files changed, 50 insertions(+), 15 deletions(-)

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/reference-decreases.md b/source/docs/guide/src/reference-decreases.md
index 02bf3c3090..f0a224efe1 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@[verus_expr],+ ( when V@[verus_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 e725dc4a43..54f00ab144 100644
--- a/source/docs/guide/src/reference-exec-signature.md
+++ b/source/docs/guide/src/reference-exec-signature.md
@@ -3,14 +3,18 @@
 The general form of an `exec` function signature takes the form:
 
 ```verus-grammar
-V@[exec_fn_with_verus_sig] ::=
-    R@[visibility]? exec? fn R@[function_name] R@[generics]?(R@[args...]) ( -> V@[return_type_and_name] )?
+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
diff --git a/source/docs/guide/src/reference-proof-signature.md b/source/docs/guide/src/reference-proof-signature.md
index df584b7566..e356b2f653 100644
--- a/source/docs/guide/src/reference-proof-signature.md
+++ b/source/docs/guide/src/reference-proof-signature.md
@@ -3,10 +3,10 @@
 The general form of a `proof` function signature takes the form:
 
 ```verus-grammar
-V@[proof_fn_with_verus_sig] ::= V@[proof_fn_proved] | V@[proof_fn_axiom]
+V@[proof_fn_item] ::= V@[proof_fn_proved] | V@[proof_fn_axiom]
 
 V@[proof_fn_proved] ::=
-    R@[visibility]? proof fn R@[function_name] R@[generics]?(R@[args...]) ( -> V@[return_type_and_name] )?
+    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]?
@@ -16,7 +16,7 @@ V@[proof_fn_proved] ::=
     { V@[proof_stmt]* }
 
 V@[proof_fn_axiom] ::=
-    R@[visibility]? axiom fn R@[function_name] R@[generics]?(R@[args...]) ( -> V@[return_type_and_name] )?
+    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]?
@@ -24,6 +24,10 @@ V@[proof_fn_axiom] ::=
         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
diff --git a/source/docs/guide/src/reference-spec-signature.md b/source/docs/guide/src/reference-spec-signature.md
index 28f167058e..2b084656b3 100644
--- a/source/docs/guide/src/reference-spec-signature.md
+++ b/source/docs/guide/src/reference-spec-signature.md
@@ -3,11 +3,15 @@
 The general form of a `spec` function signature takes the form:
 
 ```verus-grammar
-V@[spec_fn_with_verus_sig] ::=
-    R@[visibility]? spec fn R@[function_name] R@[generics]?(R@[args...]) -> R@[type]
+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@[decreases_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.
+ * <code>open(R@[visibility])</code> 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-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, T>(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-rust-subset.md b/source/docs/guide/src/spec-rust-subset.md
index 0d3725f75d..e3e03bd8c9 100644
--- a/source/docs/guide/src/spec-rust-subset.md
+++ b/source/docs/guide/src/spec-rust-subset.md
@@ -8,7 +8,7 @@ there are some subtle differences.
 **Syntax:**
 
 ```verus-grammar
-V@[fn_call_expr] ::= R@[path] ( V@[spec_expr]* )
+V@[fn_call_expr] ::= R@[path] ( V@[spec_expr],* )
 ```
 
 Only pure function calls are allowed (i.e., calls to other `spec` functions or

From ce5cbaacde98815a1450382ee33f8ea0f04dd9a9 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Wed, 20 May 2026 14:03:52 +0200
Subject: [PATCH 21/22] fix chained_expr (should always have at least 2
 comparisons)

---
 source/docs/guide/src/reference-chained-op.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/source/docs/guide/src/reference-chained-op.md b/source/docs/guide/src/reference-chained-op.md
index 883ffdb393..c2de9be9d9 100644
--- a/source/docs/guide/src/reference-chained-op.md
+++ b/source/docs/guide/src/reference-chained-op.md
@@ -3,7 +3,7 @@
 ### Syntax
 
 ```verus-grammar
-V@[chained_expr] ::= V@[spec_expr] (V@[cmp_op] V@[spec_expr])+
+V@[chained_expr] ::= V@[spec_expr] V@[cmp_op] V@[spec_expr] (V@[cmp_op] V@[spec_expr])+
 V@[cmp_op]       ::= < | <= | > | >= | ==
 ```
 

From c29a47581f58bc19b2a3343204b9448736865a6c Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Wed, 20 May 2026 14:28:49 +0200
Subject: [PATCH 22/22] fixes

---
 source/docs/guide/src/reference-assume-specification.md | 2 +-
 source/docs/guide/src/reference-decreases.md            | 2 +-
 source/docs/guide/src/spec-expressions.md               | 2 ++
 source/docs/guide/verus-grammar.py                      | 5 +++++
 4 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/source/docs/guide/src/reference-assume-specification.md b/source/docs/guide/src/reference-assume-specification.md
index 26924cb17c..aa112ff2b9 100644
--- a/source/docs/guide/src/reference-assume-specification.md
+++ b/source/docs/guide/src/reference-assume-specification.md
@@ -18,7 +18,7 @@ The general form of this directive is:
 
 ```verus-grammar
 assume_specification_item ::=
-    visibility? assume_specification R@[generics]? [ R@[function_path] ] (R@[args...]) ( -> V@[return_type_and_name] )?
+    visibility? assume_specification R@[generics]? [ R@[function_path] ] (R@[args...]) ( -> V@[exec_return_type] )?
         R@[where_clause]?
         V@[requires_clause]?
         V@[ensures_clause]?
diff --git a/source/docs/guide/src/reference-decreases.md b/source/docs/guide/src/reference-decreases.md
index f0a224efe1..b385759086 100644
--- a/source/docs/guide/src/reference-decreases.md
+++ b/source/docs/guide/src/reference-decreases.md
@@ -15,7 +15,7 @@ the form:
 
 ```verus-grammar
 V@[spec_decreases_clause] ::=
-    decreases V@[verus_expr],+ ( when V@[verus_expr] )?  ( via R@[function_ident] )?
+    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/spec-expressions.md b/source/docs/guide/src/spec-expressions.md
index cb686f69a0..8ec15d2d04 100644
--- a/source/docs/guide/src/spec-expressions.md
+++ b/source/docs/guide/src/spec-expressions.md
@@ -37,6 +37,8 @@ V@[spec_expr] ::= V@[fn_call_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/verus-grammar.py b/source/docs/guide/verus-grammar.py
index 5410104265..5f75591cd1 100644
--- a/source/docs/guide/verus-grammar.py
+++ b/source/docs/guide/verus-grammar.py
@@ -92,8 +92,11 @@ def walk(item):
             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
 
 
@@ -309,6 +312,8 @@ def main():
     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))