Merge pull request #2021 from GaloisInc/rust-tutorial-improvements

Rust tutorial improvements

doc/rust-tutorial/rust-tutorial.md

@@ -230,20 +230,30 @@ Although the resulting JSON file contains a definition for `id_u8`, it does
 _not_ contain a definition for the generic `id` function. As a result, SAW will
 only be able to verify the `id_u8` function from this file. If you are ever in
 doubt about which functions are accessible for verification with SAW, you can
-check this with `jq .roots` like so:
+check this with `jq` like so:
 
 ```
-$ jq .roots generics-take-2.linked-mir.json
+$ jq '.intrinsics | map(.name)' generics-take-2.linked-mir.json
 [
-  "generics_take_2/8b1bf337::id_u8"
+  "generics_take_2/8b1bf337::id_u8",
+  "generics_take_2/8b1bf337::id::_instaddce72e1232152c[0]"
 ]
 ```
 
-Here, "roots" can be thought of as entrypoints that are visible to SAW. Note
-that `saw-rustc` will optimize away all definitions that are not accessible
-from one of the roots. This explains why the original program that only defined
-a generic `id` function resulted in a definition-less JSON file, as that
-program did not contain any roots.
+Here, "intrinsics" are monomorphic functions that are visible to SAW. Note that
+`saw-rustc` will optimize away all definitions that are not accessible from one
+of these intrinsic functions. This explains why the original program that only
+defined a generic `id` function resulted in a definition-less JSON file, as
+that program did not contain monomorphic functions (and therefore no
+intrinsics).
+
+Generally speaking, we prefer to verify functions that are defined directly in
+the Rust source code, such as `id_u8`, as these functions' names are more
+stable than the specialized versions of functions that the compiler generates,
+such as `id::_instaddce72e1232152c[0]`. Do note that SAW is capable of
+verifying both types of functions, however. (We will see an example of
+verifying an autogenerated function in the Salsa20 case study later in this
+tutorial.)
 
 ### Identifiers
 
@@ -1077,10 +1087,16 @@ As an example, a much shorter way to write the spec above using
 $include 42-48 code/structs.saw
 ```
 
-That's it! Note that the string `"z"` is used as a prefix for all fresh names
+That's it! Note that the string `"b"` is used as a prefix for all fresh names
 that `mir_fresh_expanded_value` generates, so if SAW produces a counterexample
 involving this symbolic struct value, one can expect to see names such as
-`z_0`, `z_1`, etc. for the fields of the struct.
+`b_0`, `b_1`, etc. for the fields of the struct.
+
+`mir_fresh_expanded_value` makes it easier to construct large, compound values
+that consist of many smaller, inner values. The drawback is that you can't
+refer to these inner values in the postconditions of a spec. As a result, there
+are some functions for which `mir_fresh_expanded_value` isn't suitable, so keep
+this in mind before reaching for it.
 
 ### Enum types
 
@@ -1245,7 +1261,7 @@ different lengths. Here is a slight modification to this spec that declares it
 to take a slice of length 5 rather than a slice of length 2:
 
 ```
-$include 9-19 code/slices.saw
+$include 19-29 code/slices.saw
 ```
 
 Both of these examples declare a slice whose length matches the length of the
@@ -1376,7 +1392,7 @@ $include 5-13 code/overrides.saw
 ```
 
 There's nothing that different about this particular proof from the proofs
-we've seen before. The only notable different is that we bind the result of
+we've seen before. The only notable difference is that we bind the result of
 calling `mir_verify` to a `MIRSpec` value that we name `g_ov` (short for "`g`
 override"). This part is important, as we will need to use `g_ov` shortly.
 
@@ -1659,7 +1675,7 @@ For example, here is how one can unsafely assume `g_spec` and use it in a
 compositional proof of `f_spec`:
 
 ```
-$include 21-22 code/overrides-fail.saw
+$include 21-22 code/overrides-unsafe.saw
 ```
 
 It should be emphasized that when we say "`unsafe`", we really mean it.
@@ -1706,8 +1722,8 @@ String -> MIRValue
 In this case, `mir_static_initializer "statics::ANSWER"` is equivalent to
 writing `mir_term {{ 42 : [32] }}`, so this spec is also valid:
 
-``` {.rs}
-$include 14-18 code/statics.rs
+```
+$include 14-18 code/statics.saw
 ```
 
 Like `mir_verify`, the `mir_static_initializer` function expects a full