Rust tutorial: Clarify that SAW can verify autogenerated functions

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