From 1770e524adfd96e5e05c6046d7a379f6ffd8cfd5 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 31 Jan 2024 09:30:59 -0500 Subject: [PATCH 1/5] Rust tutorial: s/notable different/notable difference/ --- doc/rust-tutorial/rust-tutorial.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/rust-tutorial/rust-tutorial.md b/doc/rust-tutorial/rust-tutorial.md index e023cf5b72..fa0ecc38fe 100644 --- a/doc/rust-tutorial/rust-tutorial.md +++ b/doc/rust-tutorial/rust-tutorial.md @@ -1376,7 +1376,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. From 142b9616d251e1f346f1f17b92e9464fac2fc826 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 31 Jan 2024 09:30:27 -0500 Subject: [PATCH 2/5] Rust tutorial: Fix incorrect $include lines --- doc/rust-tutorial/rust-tutorial.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/rust-tutorial/rust-tutorial.md b/doc/rust-tutorial/rust-tutorial.md index fa0ecc38fe..0023f5c3b6 100644 --- a/doc/rust-tutorial/rust-tutorial.md +++ b/doc/rust-tutorial/rust-tutorial.md @@ -1245,7 +1245,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 @@ -1659,7 +1659,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 +1706,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 From 71b35376994d97f64ad35682a28117a75b1ad255 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 31 Jan 2024 09:36:53 -0500 Subject: [PATCH 3/5] Rust tutorial: Use correct prefix in mir_fresh_expanded_value section --- doc/rust-tutorial/rust-tutorial.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/rust-tutorial/rust-tutorial.md b/doc/rust-tutorial/rust-tutorial.md index 0023f5c3b6..b92d5d466a 100644 --- a/doc/rust-tutorial/rust-tutorial.md +++ b/doc/rust-tutorial/rust-tutorial.md @@ -1077,10 +1077,10 @@ 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. ### Enum types From 976c30675436099b82043252a269b961059e24ec Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 31 Jan 2024 09:40:44 -0500 Subject: [PATCH 4/5] Rust tutorial: Mention downsides of mir_fresh_expanded_value --- doc/rust-tutorial/rust-tutorial.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/doc/rust-tutorial/rust-tutorial.md b/doc/rust-tutorial/rust-tutorial.md index b92d5d466a..e7838e5a1e 100644 --- a/doc/rust-tutorial/rust-tutorial.md +++ b/doc/rust-tutorial/rust-tutorial.md @@ -1082,6 +1082,12 @@ 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 `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 Besides structs, another form of ADT that Rust supports are enums. Each enum From 481a1c3b715e300dcbc95cf8202cfa3f38d5fb13 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 31 Jan 2024 09:53:40 -0500 Subject: [PATCH 5/5] Rust tutorial: Clarify that SAW can verify autogenerated functions --- doc/rust-tutorial/rust-tutorial.md | 26 ++++++++++++++++++-------- 1 file changed, 18 insertions(+), 8 deletions(-) diff --git a/doc/rust-tutorial/rust-tutorial.md b/doc/rust-tutorial/rust-tutorial.md index e7838e5a1e..81d54fbb02 100644 --- a/doc/rust-tutorial/rust-tutorial.md +++ b/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