From 716aaa5f13b2ccbd3520af2b5380f35558c6b6c1 Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@users.noreply.github.com>
Date: Wed, 15 Jan 2025 21:01:26 -0500
Subject: [PATCH] Expand docs to illustrate how the modes work together (#1377)

---
 source/docs/guide/src/SUMMARY.md  |  1 +
 source/docs/guide/src/triangle.md | 47 +++++++++++++++++++++++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 source/docs/guide/src/triangle.md

diff --git a/source/docs/guide/src/SUMMARY.md b/source/docs/guide/src/SUMMARY.md
index 182253b67..366e95e65 100644
--- a/source/docs/guide/src/SUMMARY.md
+++ b/source/docs/guide/src/SUMMARY.md
@@ -19,6 +19,7 @@
     - [spec functions vs. proof functions, recommends](spec_vs_proof.md)
     - [Ghost code vs. exec code](ghost_vs_exec.md)
     - [const declarations](const.md)
+    - [Putting it all together](triangle.md)
 - [Recursion and loops](recursion_loops.md)
     - [Recursive spec functions, decreases, fuel](recursion.md)
     - [Recursive exec and proof functions, proofs by induction](induction.md)
diff --git a/source/docs/guide/src/triangle.md b/source/docs/guide/src/triangle.md
new file mode 100644
index 000000000..9eb3f2a79
--- /dev/null
+++ b/source/docs/guide/src/triangle.md
@@ -0,0 +1,47 @@
+# Putting It All Together
+
+To show how `spec`, `proof`, and `exec` code work together, consider the example
+below of computing the n-th [triangular number](https://en.wikipedia.org/wiki/Triangular_number).
+We'll cover this example and the features it uses in more detail in [Chapter 4](recursion_loops.md),
+so for now, let's focus on the high-level structure of the code.
+
+We use a `spec` function `triangle` to mathematically define our specification using natural numbers (`nat`)
+and a recursive description.  We then write a more efficient iterative implementation
+as the `exec` function `loop_triangle` (recall that `exec` is the default mode for functions).
+We connect the correctness of `loop_triangle`'s return value to our mathematical specification 
+in `loop_triangle`'s `ensures` clause.
+
+However, to successfully verify `loop_triangle`, we need a few more things.  First, in executable
+code, we have to worry about the possibility of arithmetic overflow.  To keep things simple here,
+we add a precondition to `loop_triangle` saying that the result needs to be less than one million,
+which means it will certainly fit into a `u32`.
+
+We also need to translate the knowledge that the final `triangle` result fits in a `u32`
+into the knowledge that each individual step of computing the result won't overflow,
+i.e., that computing `sum = sum + idx` won't overflow.  We can do this by showing
+that `triangle` is monotonic; i.e., if you increase the argument to `triangle`, the result increases too.
+Showing this property requires an [inductive proof](induction.md).  We cover inductive proofs
+later; the important thing here is that we can do this proof using a `proof` function
+(`triangle_is_monotonic`).  To invoke the results of our proof in our `exec` implementation, 
+we [assert](proof_functions.md#assert-by) that the new sum fits, and as
+justification, we  an invoke our proof with the relevant arguments.  At the
+call site, Verus will check that the preconditions for `triangle_is_monotonic`
+hold and then assume that the postconditions hold.
+
+Finally, our implementation uses a while loop, which means it requires some [loop invariants](while.md),
+which we cover later.
+
+```rust
+{{#include ../../../rust_verify/example/guide/recursion.rs:spec}}
+```
+
+```rust
+{{#include ../../../rust_verify/example/guide/recursion.rs:mono}}
+```
+
+```rust
+{{#include ../../../rust_verify/example/guide/recursion.rs:loop}}
+```
+
+
+