Organize reference pages for prover modes (#2613)

Author: tjhance

source/docs/guide/src/SUMMARY.md

@@ -157,15 +157,21 @@
     - [The `is` operator](./reference-is.md)
     - [The `matches` operator](./reference-matches.md)
     - [`decreases_to!`](./reference-decreases-to.md)
-- [Proof features]()
-  - [assert and assume]()
-  - [assert ... by](./reference-assert-by.md)
-  - [assert forall ... by](./reference-assert-forall-by.md)
-  - [assert ... by(bit_vector)](./reference-assert-by-bit-vector.md)
-  - [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)
+- [Proofs]()
+  - [Proof statements]()
+    - [assert](./reference-assert.md)
+    - [assume](./reference-assume.md)
+    - [assert ... by](./reference-assert-by.md)
+    - [assert forall ... by](./reference-assert-forall-by.md)
+    - [assert ... by(...)](./reference-assert-by-prover.md)
+    - [reveal, reveal_with_fuel, hide](./reference-reveal-hide.md)
+    - [reveal_strlit](./reference-reveal-strlit.md)
+  - [Prover modes]()
+    - ["default" mode]()
+    - [`bit_vector`](./reference-prover-mode-bit-vector.md)
+    - [`nonlinear`](./reference-prover-mode-nonlinear.md)
+    - [`integer_ring`](./reference-prover-mode-integer-ring.md)
+    - [`compute`/`compute_only`](./reference-prover-mode-compute.md)
 - [Function specifications]()
   - [Function Signatures]()
     - [Exec fn signature](./reference-exec-signature.md)

source/docs/guide/src/external_trait_specifications.md

@@ -9,14 +9,21 @@ for this purpose:
 
 ## Soundness warning
 
-**Be cautious when adding specifications to external traits.** All implementations
-of the trait — including those in unverified code, even code that hasn't been written yet — are
-assumed to uphold the specification. For example, if you verify a crate with
-`pub fn test<A: Formatter>(...)`, Verus assumes that whatever type instantiates `A` will
-satisfy the `Formatter` specification, even if that type comes from an unverified crate.
-This is a contract on both current and future unverified code.
-
-[See below](#the-obeys_-pattern-in-vstd) for a useful pattern (employed by `vstd`) for mitigating this soundness risk.
+> [!CAUTION]
+> Since the `assume_specification` statement is unchecked, it can easily be used to subvert
+> Verus's guarantees.
+>
+> Further, specifying traits correctly is often even more difficult than specifying ordinary
+> functions.
+>
+> All implementations
+> of the trait — including those in unverified code, even code that hasn't been written yet — are
+> assumed to uphold the specification. For example, if you verify a crate with
+> `pub fn test<A: Formatter>(...)`, Verus assumes that whatever type instantiates `A` will
+> satisfy the `Formatter` specification, even if that type comes from an unverified crate.
+> This is a contract on both current and future unverified code.
+>
+> [See below](#the-obeys_-pattern-in-vstd) for a useful pattern (employed by `vstd`) for mitigating this soundness risk.
 
 ## Basic external trait specification
 

source/docs/guide/src/reference-assert-by-nonlinear.md

@@ -0,0 +1,52 @@
+# assert ... by(...)
+
+The `assert ... by` statement is used to invoke a specialized _prover mode_ for proving
+the given assertion.
+
+### Syntax
+
+We divide the prover modes into "solver modes" (which invoke a solver) and "interpreter modes" (which invoke the interpreter).
+
+```verus-grammar
+V@[assert_by_prover_stmt] ::=
+    assert ( V@[spec_expr] ) by ( V@[assert_by_solver_mode] ) V@[assert_by_prover_requires]? ;
+  | assert ( V@[spec_expr] ) by ( V@[assert_by_interpreter_mode] );
+
+V@[assert_by_solver_mode] ::= nonlinear_arith | bit_vector;
+V@[assert_by_interpreter_mode] ::= compute | compute_only;
+
+V@[assert_by_prover_requires] ::=
+    requires (V@[spec_expr],)+
+```
+
+> [!NOTE]
+> At present, the [`integer_ring`](./reference-prover-mode-integer-ring.md) prover mode may only
+> be used in a [proof function declaration](./reference-proof-signature.md),
+> not in an assert-by.
+
+### Proof operation
+
+**Solver modes.**
+For `nonlinear_arith` and `bit_vector` modes,
+Verus attempts to prove the given predicate via the specified solver
+(the [`nonlinear_arith` solver](./reference-prover-mode-nonlinear.md)
+or the [`bit_vector` solver](./reference-prover-mode-bit-vector.md)).
+The predicate is proved in isolation, absent any surrounding context.
+
+Specifically, for a statement
+<code>assert ( Q ) by ( V@[assert_by_solver_mode] )</code>,
+Verus tries to prove `Q` using the solver, and then assumes `Q` for the subsequent code.
+
+If a `requires P` clause is additionally provides, then Verus:
+
+ * Proves `P` using the default solver (with full context available)
+ * Proves `P ==> Q` using the specified solver (in isolation)
+ * And finally assumes `Q` for subsequent code.
+
+**Interpreter modes.**
+For `compute` and `compute_only` modes, Verus uses its [specification interpreter](./reference-prover-mode-compute.md) to simplify the expression `Q` as much as possible, yielding an expression `Q'`.
+
+ * For `compute_only`, Verus will check that `Q'` is the boolean value `true`, and then assumes
+   the given predicate for all subsequent code.
+ * For `compute`, Verus will replace the assert-by statement with `assert(Q')`, which then behaves
+   like an ordinary [`assert`](./reference-assert.md).

source/docs/guide/src/reference-assert-by-prover.md

@@ -0,0 +1,12 @@
+# `assert`
+
+### Syntax
+
+```verus-grammar
+V@[assert] ::= assert (V@[spec_expr]) ;
+```
+
+### Proof operation
+
+Prove the given expression using the default solver, and then assume the predicate for
+subsequence code.

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

@@ -1,5 +1,11 @@
 # assume_specification
 
+> [!CAUTION]
+> Since the `assume_specification` statement is unchecked, it can easily be used to subvert
+> Verus's guarantees.
+>
+> Be sure to read our [advice on interacting with unverified code](./interacting-with-unverified-code.md).
+
 The `assume_specification` directive tells Verus to use the given specification for the given function.
 Verus assumes that this specification holds **without proof**.
 

source/docs/guide/src/reference-assume-specification.md

@@ -0,0 +1,25 @@
+# `assume`
+
+<!-- TODO: Should decide whether or not the presence of an assume still gives guarantees about the subset of program executions where the assumption holds. -->
+
+> [!CAUTION]
+> Since the `assume` statement is unchecked, it can easily be used to subvert Verus's guarantees.
+> In particular, successful "verification" by Verus provides **no guarantees** on the program
+> if it includes any `assume` statements, unless those `assume` statements could in principle
+> be replaced by a successful `assert` statement.
+>
+> The `assume` statement is most useful during _intermediate_ stages of development,
+> e.g., within an [assert/assume-driven proof-development process](./assert_assume.md).
+
+> [!TIP]
+> The `--no-cheating` flag can be used to disallow `assume` statements.
+
+### Syntax
+
+```verus-grammar
+V@[assume] ::= assume (V@[spec_expr]) ;
+```
+
+### Proof operation
+
+Assume the given predicate without proof.

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

@@ -6,7 +6,7 @@ The general form of a `proof` function signature takes the form:
 V@[proof_fn_item] ::= V@[proof_fn_proved] | V@[proof_fn_axiom]
 
 V@[proof_fn_proved] ::=
-    R@[visibility]? broadcast? proof fn R@[function_name] R@[generics]?(R@[args...]) ( -> V@[proof_return_type] )?
+    R@[visibility]? broadcast? proof fn R@[function_name] R@[generics]?(R@[args...]) ( by(function_prover_mode) )? ( -> V@[proof_return_type] )?
         R@[where_clause]?
         V@[requires_clause]?
         V@[ensures_clause]?
@@ -25,6 +25,8 @@ V@[proof_fn_axiom] ::=
         V@[decreases_clause]?
         ;
 
+V@[function_prover_mode]    ::= integer_ring | bit_vector | nonlinear_arith
+
 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]
@@ -54,3 +56,10 @@ All arguments and return values need to have `ghost` or `tracked` mode.
 Arguments are `ghost` by default, and they can be declared `tracked` with the `tracked` keyword.
 
 See [here](./reference-var-modes.md#cheat-sheet) for more information.
+
+## Function prover mode
+
+If the V@[function_prover_mode] is provided, the proof is dispatched via the given solver
+([`integer_ring`](./reference-prover-mode-integer-ring.md),
+[`bit_vector`](./reference-prover-mode-bit-vector.md),
+or [`nonlinear_arith`](./reference-prover-mode-nonlinear.md)).

source/docs/guide/src/reference-proof-signature.md

@@ -1,28 +1,38 @@
-# assert ... by(bit_vector)
+# The `bit_vector` prover mode
 
-Invoke Verus's bitvector solver to prove the given predicate.
-This is particularly useful for bitwise operators
-and integer arithmetic on finite-width integers.
-Internally, the solver uses a technique called _bit-blasting_, which represents each numeric variable
-by its binary representation as a bit vector, and every operation as a boolean circuit.
+> [!TIP]
+> See the [guide page](./bitvec.md) for practical tips on using the `bit_vector` solver.
 
+### Methods of invocation
 
+**By assertion.**
+The `bit_vector` solver can be invoked via an [`assert-by` statement](./reference-assert-by-prover.md):
+
+```
+assert(Q) by(bit_vector);
 ```
-assert(P) by(bit_vector);
+
+Proves `Q` via the the `bit_vector` solver.
+
 ```
+assert(Q) by(bit_vector) requires P;
+```
+
+Proves `P ==> Q` via the the `bit_vector` solver.
+
+**As a proof function.**
+The `bit_vector` solver can be invoked with a `by(bit_vector)` on a [proof function](./reference-proof-signature.md).
 
 ```
-assert(P) by(bit_vector)
-  requires Q;
+proof fn example(...) by(bit_vector)
+    requires P
+    ensures Q
+{ }
 ```
 
-The prover does not have access to any prior context except that which is given in
-the `requires` clause, if provided. If the `requires` clause is provided, then the
-bit vector solver attempts to prove `Q ==> P`. Verus will also check (using its normal solver)
-that `Q` holds from the prior proof context.
+This proves `P ==> Q` via the `bit_vector` solver.
 
-The expressions `P` and `Q` may only contain expressions that the bit solver understands.
-This includes:
+### Supported predicates
 
  * Variables of type `bool` or finite-width integer types (`u64`, `i64`, `usize`, etc.)
    * All free variables are treated symbolically. Even if a variable is defined via a `let`
@@ -36,16 +46,17 @@ This includes:
  * Boolean operators (`&&`, `||`, `^`) and conditional expressions
  * The `usize::BITS` constant
 
-## Internal operation
+## Solver operation
 
 Verus's bitvector solver encodes the expression by representing all integers using an SMT "bitvector" type.
 Most of the above constraints arise 
 because of the fact that Verus has to choose a fixed bitwidth for any given expression.
 
 Note that, although the bitvector solver cannot handle free variables of type
-`int` or `nat`, it _can_ handle other kinds of expressions that are typed `int` or `nat`.
+`int` or `nat`, it _can_ handle some expressions that are typed `int` or `nat` provided
+Verus can bound the the bitwidth needed to represent the number.
 For example, if `x` and `y` have type `u64`, then `x + y` has type `int`,
-but the Verus bitvector solver knows that `x + y` is representable with 65 bits.
+but the Verus knows that `x + y` is representable with 65 bits.
 
 ### Handling `usize` and `isize`
 

…de/src/reference-assert-by-bit-vector.md …/src/reference-prover-mode-bit-vector.mdsource/docs/guide/src/reference-assert-by-bit-vector.md renamed to source/docs/guide/src/reference-prover-mode-bit-vector.md source/docs/guide/src/reference-assert-by-bit-vector.md renamed to source/docs/guide/src/reference-prover-mode-bit-vector.md

@@ -1,15 +1,30 @@
-# assert ... by(compute) / by(compute_only)
+# The compute mode
 
-See [this section of the tutorial](./assert_by_compute.md) for motivation and an example.
+> [!TIP]
+> See the [guide page](./assert_by_compute.md) for practical tips on using this feature.
 
-A statement of the form:
+### Methods of invocation
 
+**By assertion.**
+The `nonlinear_arith` solver can be invoked via an [`assert-by` statement](./reference-assert-by-prover.md):
+
+```
+assert(Q) by(compute_only);
 ```
-assert(P) by(compute_only);
+
+Proves `Q` by simplifying it via the interpreter and checking
+if the result is the boolean value `true`.
+
 ```
+assert(Q) by(compute);
+```
+
+Proves `Q` by simplifying it via the interpreter to an expression `Q'` and replacing
+the statement with `assert(Q);`.
+
+### Interpreter operation
 
-Will evaluate the expression `P` as far a possible, and Verus accepts the result if it
-evaluates to the boolean expression `true`. It unfolds function definitions and evaluates
+The interpreter unfolds function definitions and evaluates
 arithmetic expressions. It is capable of some symbolic manipulation, but it does not handle
 algebraic laws like `a + b == b + a`, and it works best when evaluating constant expressions.
 
@@ -27,7 +42,7 @@ to finish the problem through the normal solver. So for example, if after expans
 `P` results in a trivial expression like `a+b == b+a`, then it should be solved
 with `by(compute)`.
 
-### Memoization
+### Configurating the evaluation strategy
 
 The [`#[verifier::memoize]` attribute](./reference-attributes.md#verifiermemoize) can be used to mark
 certain functions for [memoizing](https://en.wikipedia.org/wiki/Memoization).