Merge pull request #2563 from GaloisInc/mir-vec-of

MIR: Add `mir_vec_of` command

Author: qsctr

CHANGES.md

@@ -87,6 +87,9 @@ support compositional verification using techniques similar to SAW.
 * Add new SAWScript MIR commands `mir_elem_value` and `mir_elem_ref` for
   indexing into arrays and references to arrays.
 
+* Add a new SAWScript MIR command `mir_vec_of` for creating Rust `Vec` values in
+  specifications.
+
 * Support writing MIR specifications involving raw pointers. This is done with
   the new SAWScript commands `mir_raw_ptr_const`, `mir_raw_ptr_mut`,
   `mir_alloc_raw_ptr_const`, and `mir_alloc_raw_ptr_mut`, which are similar to

cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs

@@ -23,6 +23,7 @@ module CryptolSAWCore.CryptolEnv
   , bindType
   , bindInteger
   , parseTypedTerm
+  , pExprToTypedTerm
   , parseDecls
   , parseSchema
   , declareName
@@ -645,11 +646,17 @@ parseTypedTerm ::
   (?fileReader :: FilePath -> IO ByteString) =>
   SharedContext -> CryptolEnv -> InputText -> IO TypedTerm
 parseTypedTerm sc env input = do
-  let modEnv = eModuleEnv env
-
   -- Parse
   pexpr <- ioParseExpr input
 
+  pExprToTypedTerm sc env pexpr
+
+pExprToTypedTerm ::
+  (?fileReader :: FilePath -> IO ByteString) =>
+  SharedContext -> CryptolEnv -> P.Expr P.PName -> IO TypedTerm
+pExprToTypedTerm sc env pexpr = do
+  let modEnv = eModuleEnv env
+
   ((expr, schema), modEnv') <- liftModuleM modEnv $ do
 
     -- Eliminate patterns

deps/cryptol

@@ -1138,7 +1138,7 @@ Note that we are passing _references_ of arrays to `mir_slice_value` and
 `mir_slice_range_value`. It would be an error to pass a bare array to these
 functions, so the following specification would be invalid:
 
-:::
+:::{code-block} sawscript
 let f_fail_spec_ = do {
   let arr = mir_term {{ [1, 2, 3, 4, 5] : [5][32] }};
 
@@ -1264,6 +1264,29 @@ On the other hand, SAW will allow you define a slice of the form
 the responsibility of the SAW user to ensure that `mir_str_slice_range` indices
 align with character boundaries.
 
+### MIR `Vec`s
+
+[`Vec`](https://doc.rust-lang.org/std/vec/struct.Vec.html) is a commonly used
+data type in the Rust standard library. `Vec` values can be created from array
+values in MIR specifications with the following command:
+
+- `mir_vec_of : String -> MIRType -> MIRValue -> MIRSetup MIRValue`
+
+The `String` argument is used as a prefix for naming the internal symbolic
+variables created as part of the `Vec` struct (think of it just as a name you
+give to the `Vec` variable). The `MIRType` argument is the element type of the
+`Vec`. The `MIRValue` argument is the contents of the `Vec`, which must be a MIR
+array value whose element type matches the `MIRType` argument. Note that this
+could either be created with `mir_array_value` or obtained from a `Term` like a
+fresh variable or a Cryptol sequence expression.
+
+`Vec` is just a regular struct and not a special language construct, so
+technically you could write specifications for `Vec`s just using the primitive
+MIR specification commands (in fact, this is what `mir_vec_of` does internally).
+However, you would need to explicitly specify all the internal details and
+invariants of `Vec`, and that can get quite messy. Therefore, this command
+exists for convenience reasons.
+
 ### Finding MIR algebraic data types
 
 We collectively refer to MIR `struct`s and `enum`s together as _algebraic data

doc/pdfs/llvm-java-verification-with-saw.pdf

@@ -24,6 +24,6 @@
 #    - the devel version can then be bumped to the current day if needed
 #
 
-# BSD/Linux: date +%s -d "07/23/2025 00:00:00 GMT"
-# OSX: date -j -f "%m/%d/%Y %H:%M:%S %Z" "7/23/2025 00:00:00 GMT" +%s
-SOURCE_DATE_EPOCH=1753228800
+# BSD/Linux: date +%s -d "08/22/2025 00:00:00 GMT"
+# OSX: date -j -f "%m/%d/%Y %H:%M:%S %Z" "8/22/2025 00:00:00 GMT" +%s
+SOURCE_DATE_EPOCH=1755820800

doc/pdfs/rust-verification-with-saw.pdf

@@ -1,3 +1,7 @@
 versions
    rustc 1.86.0-nightly (9cd60bd2c 2025-02-15)
-   mir-json ae8c20d96b874ee977b5fba0f02059d6593943a8 from 2025-08-06
+   mir-json mtime: Aug 21 23:14:39 2025
+   mir-json version from cargo: mir-json v0.1.0
+   probable mir-json commit: 753fe4b97b59035adc204aa426a3ae44b44822b9 from Mon Aug 18 12:31:05 2025 and/or Mon Aug 18 12:31:05 2025
+versions-notes
+   Generated by update-from.sh version 1