Flesh out the reference section for spec expressions

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"

source/docs/guide/src/SUMMARY.md

@@ -137,8 +137,8 @@
   - [Spec and proof attributes for exec functions](exec_attr.md)
     - [Automatic exec to spec functions](exec_to_spec.md)
 - [Spec expressions](./spec-expressions.md)
-  - [Rust subset](./spec-rust-subset.md)
   - [Operator Precedence](./spec-operator-precedence.md)
+  - [Rust subset](./spec-rust-subset.md)
   - [Arithmetic](./spec-arithmetic.md)
   - [Bit operators](./spec-bit-ops.md)
   - [Coercion with `as`](./reference-as.md)
@@ -152,7 +152,11 @@
   - [Trigger annotations](./trigger-annotations.md)
   - [The view function `@`](./reference-at-sign.md)
   - [Spec index operator `[]`](./reference-spec-index.md)
+  - [The `has` operator](./reference-has.md)
+  - [The `is` operator](./reference-is.md)
+  - [The `matches` operator](./reference-matches.md)
   - [`decreases_to!`](./reference-decreases-to.md)
+- [Types](./reference-types.md)
 - [Proof features]()
   - [assert and assume]()
   - [assert ... by](./reference-assert-by.md)
@@ -161,6 +165,7 @@
   - [assert ... by(nonlinear_arith)](./reference-assert-by-nonlinear.md)
   - [assert ... by(compute) / by(compute_only)](./reference-assert-by-compute.md)
   - [reveal, reveal_with_fuel, hide](./reference-reveal-hide.md)
+  - [reveal_strlit](./reference-reveal-strlit.md)
 - [Function specifications]()
   - [Function Signatures]()
     - [Exec fn signature](./reference-exec-signature.md)
@@ -189,7 +194,6 @@
   - [`global`](./reference-global.md)
 - [Misc. Rust features]()
   - [Statics](./static.md)
-  - [char](./char.md)
   - [Unions](./reference-unions.md)
   - [Pointers and cells](./reference-pointers-cells.md)
 - [Command line]()

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))]

source/docs/guide/src/prefix-and-or.md

@@ -1,3 +1,35 @@
 # Prefix and/or (`&&&` and `|||`)
 
-The prefix and/or operators (`&&&` and `|||`) are explained in [Expressions and operators for specifications](operators.md).
+For an introduction, see [Expressions and operators for specifications](operators.md).
+
+### Syntax
+
+```verus-grammar
+V@[prefix_and_expr] ::= (&&&  V@[spec_expr])+
+V@[prefix_or_expr]  ::= (|||  V@[spec_expr])+
+```
+
+Each operand is introduced by its operator as a prefix. `&&&` is the prefix conjunction
+and `|||` is the prefix disjunction. Both bind looser than all other binary operators
+(see [operator precedence](./spec-operator-precedence.md)).
+
+### Typing
+
+Each operand must have type `bool`. The expression returns `bool`.
+
+### Semantics
+
+`&&&` and `|||` are shorthand for `&&` and `||`, written in prefix form. A sequence of
+`&&&`-prefixed operands is equivalent to the corresponding infix conjunction, and likewise
+for `|||`:
+
+```
+&&& P &&& Q &&& R  ≡  P && Q && R
+||| P ||| Q ||| R  ≡  P || Q || R
+```
+
+As all spec expressions are pure and effectless, there is no notion of short-circuiting.
+
+The main motivation for these operators is readability: when writing a large conjunction
+or disjunction (such as a precondition or an invariant), the leading-prefix style makes it
+easy to add, remove, or reorder clauses without adjusting punctuation elsewhere.

source/docs/guide/src/ref-extensional-equality.md

@@ -1,4 +1,27 @@
 # Extensional equality (`=~=` and `=~~=`)
 
-The extensional equality operators `=~=` and `=~~=` are explained in
-[Extensional equality](extensional_equality.md).
+The **shallow extensional equality operator** `=~=` 
+and **deep extensional equality operator** `=~~=` are both equivalent to
+[spec equality (`==`)](./spec-equality.md).
+
+These operators are distinguished only by their impact on the proof search.
+Specifically, the use of the `=~=` and `=~~=` operators will trigger the application of
+"extensional equality" operators.
+
+See [the guide page](extensional_equality.md) for an introductory explanation with motivation.
+
+### Syntax
+
+```verus-grammar
+V@[ext_eq_expr] ::= V@[spec_expr] =~=  V@[spec_expr]
+              | V@[spec_expr] =~~= V@[spec_expr]
+```
+
+### Typing
+
+The extensional equality operator requires both the left-hand side and right-hand side
+to have the same type. The expression returns a [`bool`](./reference-types#bool).
+
+### Semantics
+
+The operator is equivalent to [spec equality](./spec-equality.md).

source/docs/guide/src/reference-as.md

@@ -1,7 +1,14 @@
 # Coercion with `as`
 
-In spec code, any "integer type" may be coerced to any other integer type via `as`.
-For the sake of this page, "integer type" means any of the following:
+## Syntax
+
+```verus-grammar
+V@[as_expr] ::= V@[spec_expr] as R@[type]
+```
+
+## Coercions on integer types and `char`
+
+Any of the following types may be coerced to any of the other types:
 
  * `i8`, `i16`, `i32`, `i64`, `i128`, `isize`
  * `u8`, `u16`, `u32`, `u64`, `u128`, `usize`
@@ -13,7 +20,7 @@ Note that this is more permissive than `as` in Rust exec code. For example, Rust
 not permit using `as` to cast from a `u16` to a `char`, but this is allowed in Verus
 spec code.
 
-## Definition
+### Definition
 
 Verus defines `as`-casting as follows:
 
@@ -24,11 +31,39 @@ 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
 [the bit-vector solver](./reference-assert-by-bit-vector.md)
 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.

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.

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.

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@[exec_return_type] )?
+        R@[where_clause]?
+        V@[requires_clause]?
+        V@[ensures_clause]?
+        V@[returns_clause]?
+        V@[invariants_clause]?
+        V@[unwind_clause]?
+        ;
+```
 
 It is intended to look like an ordinary Rust function signature with a [Verus specification](./reference-exec-signature.md), except instead of having a name, it refers to a different function by path.
 
 For associated functions and methods, the <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       |
+
+

source/docs/guide/src/reference-at-sign.md

@@ -1,6 +1,22 @@
 # The view function `@`
 
-The expression `expr@` is a shorthand for `expr.view()`. The `view()` function is a Verus
-convention for the abstraction of an exec-mode object, usually [defined by the `View` trait](https://verus-lang.github.io/verus/verusdoc/vstd/view/trait.View.html).
-However, the expansion of the `@` syntax is purely syntactic, so it does not necessarily
-correspond to the trait function.
+### Syntax
+
+```verus-grammar
+V@[view_expr] ::= V@[spec_expr] @
+```
+
+### Desugaring
+
+The expression `expr@` desugars to the expression `expr.view()`, which is resolved as normal via
+Rust's [method resolution](https://doc.rust-lang.org/reference/expressions/method-call-expr.html).
+This usually, but not always, resolves to the `view` method [defined by the `View` trait](https://verus-lang.github.io/verus/verusdoc/vstd/view/trait.View.html).
+
+### Use cases
+
+By convention, the `view()` function is a Verus
+convention for the abstraction of an exec-mode object.
+See, for example:
+
+ * [Using view to reason about `Vec`](./exec_lib.md)
+ * [Defining a view function](./container_bst_first_draft.md#the-abstract-view)