MIR bool arrays are cumbersome to use in SAW

[RyanGlScott]

Consider the following Rust function, which uses an array of bools:

// test.rs
pub fn bit_array(a : [bool; 8]) -> [bool; 8] {
    return a;
}

You would expect that SAW would be able to verify f against the following specification:

// test.saw
enable_experimental;

m <- mir_load_module "test.linked-mir.json";

let spec = do {
    a <- mir_fresh_var "a" (mir_array 8 mir_bool);

    mir_execute_func [mir_term a];

    mir_return (mir_term a);
};

mir_verify m "test::bit_array" [] false spec z3;

Surprisingly, however, it can't:

$ ~/Software/saw-1.2/bin/saw test.saw
[14:32:11.105] Loading file "/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw"
[14:32:11.123] Stack trace:
"mir_verify" (/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw:14:1-14:11)
"spec" (/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw:14:41-14:45)
mir_execute_func: Argument type mismatch
Argument position: 0
Expected type: [bool; 8]
Given type:    u8

The reason this happens is rather unfortunate:

• The first thing that mir_fresh_var does it take the supplied MIR type and convert it into its corresponding Cryptol type. In the case of mir_fresh_var "a" (mir_array 8 mir_bool), the corresponding Cryptol type is [8]Bit, i.e., [8].
• When calling mir_verify, SAW needs to check that the type of the specification (spec) matches the type of the original Rust function. It does so by (1) converting each Rust argument type in the function's type signature to its corresponding Crucible type, (2) converting each argument type passed to mir_execute_func to its corresponding Crucible type, and (3) checking if the Crucible types match.
• For (1) in the example above, the Crucible type corresponding to arrays is MirVectorRepr (see here), and the Crucible type corresponding to bool is BoolRepr (see here). Therefore, the full Crucible type correspoinding to [bool; 8] is MirVectorRepr BoolRepr.
• For (2) in the example above, we have mir_execute_func [llvm_term a], and the type of a is [8]. The Crucible type corresponding to [8] is BaseBVRepr (knownNat @8): see here. (This is the same Crucible type that you'd get for u8—more on this later.)
• For (3), the Crucible types MirVectorRepr BoolRepr and BaseBVRepr (knownNat @8) are not the same, yielding a type error. (The error message complains about [bool; 8] and u8, but these are basically just pretty-printed versions of the Crucible types.)

The key step here is in picking a Crucible type for [8]. This choice is somewhat arbitrary, as we could just as well pick BaseBVRepr (knownNat @8) or MirVectorRepr BoolRepr. Picking the former is usually the more sensible option, as it happens to correspond to the same Crucible type that is assigned to types such as u8 (see here), and these integer types are far more common that bool arrays. Unfortunately, this choice comes at the expense of making it impossible to write SAW specifications like the one above.

A handful of scattered observations:

• The reason why we have to make an arbitrary choice in the first place is because Cryptol doesn't distinguish between an 8-bit word type and an 8-bit sequence of Bits: they're both represented by the same type [8]. In this sense, Cryptol's type system is more coarse-grained than Crucible's type system, which has separate types for these.

• SAW's LLVM backend does not have an equivalent problem because LLVM's type system does not have a type that is given the Crucible type BoolRepr. The closest thing that LLVM has is the i1 type, but this is translated to the Cryptol type [1] (a 1-bit word), not Bit. As such, the LLVM types i8 and [8 x i1] would be represented by entirely different Cryptol types ([8] and [8][1], respectively).

• A workaround for this issue is to avoiding using mir_fresh_var. One way to do this is by creating fresh variables for each individual element of the bool array rather than creating a single fresh variable for the entire array, which is what the mir_fresh_expanded_value command does. That is, SAW does successfully verify the following spec:

  // test.saw
  enable_experimental;
  
  m <- mir_load_module "test.linked-mir.json";
  
  let spec = do {
      a <- mir_fresh_expanded_value "a" (mir_array 8 mir_bool);
  
      mir_execute_func [a];
  
      mir_return a;
  };
  
  mir_verify m "test::bit_array" [] false spec z3;
  

Ultimately, I suspect that fixing this issue will require us to make SAW more flexible about how we embed types into Cryptol, as proposed in #1976. This is because the types u8 and [bool; 8] have the same representation in Cryptol, but different Crucible representations. Until then, the mir_fresh_expanded_value trick mentioned above is a serviceable workaround.

Lastly, one radical idea: could we fix this issue by changing the Crucible representation of bool from BoolRepr to BaseBVRepr (knownNat @1), similarly to how LLVM's i1 type is handled? Perhaps so, but this would require changing a fair bit of code in crucible-mir to accommodate this, and it's unclear to me whether that is a good idea. In any case, we want to fix #1976 anyway, so it's likely best to pursue a solution there.

[RyanGlScott]

@Isweet suggests that we could make this work by treating BaseBVRepr and MirVectorRepr BoolRepr as belonging to the same equivalence class, and when we try to equate one with the other, performing explicit conversions where necessary. I am somewhat on the fence about needing to sprinkle conversions in various places, since this feels like we are sidestepping a design issue to some extent, but that might be one way to unblock this.

[Isweet]

@RyanGlScott, I suspect your intuition about how to work around this issue is better, so I'd recommend going with your gut rather than mine.

I'd only recommend documenting the purpose of each Crucible type (with some explanation of why they must be different).

[sauclovian-g]

We ultimately need #1976 anyway, I think.