Cryptol support for crux-mir-comp

[spernsteiner]

The major change in this branch is adding support for calling Cryptol functions from Rust in crux-mir-comp. Symbolic tests can use the cryptol! macro to declare Rust bindings for Cryptol functions. Example:

cryptol! {
    path "Primitive::Keyless::Hash::SHA256";

    pub fn message_schedule(m: [u32; 16]) -> [u32; 64]
        = "messageSchedule_Common";
    pub fn message_schedule_one(a: u32, b: u32, c: u32, d: u32) -> u32
        = r#" \a b c (d : [32]) -> d + sigma_0 c + b + sigma_1 a "#;
}

With these declarations, calling message_schedule invokes the Cryptol function messageSchedule_Common (of type [16][32] -> [64][32]) from the module Primitive::Keyless::Hash::SHA256, and calling message_schedule_one invokes the Cryptol lambda expression given as a string (which uses sigma_0 and sigma_1 imported from the same module).

Bindings are typechecked on first use. Cryptol functions can use bit, array, and tuple types; the Rust signature must use the corresponding bool, array, and tuple types. For convenience, bitvectors such as the Cryptol type [32] can match not only the Rust type [bool; 32] but also u32 and i32.

This branch also includes several smaller changes that were necessary to get compositional verification against Cryptol specs working in practice (specifically, on ring's SHA256 implementation):

• Add a workaround for imperfect what4 -> saw-core -> what4 round-tripping. Defining a MethodSpec in crux-mir-comp involves converting what4 exprs from the Crucible state into saw-core terms to be stored in the MethodSpec. Applying the MethodSpec override then converts those saw-core terms back to what4. In some cases, this what4 -> saw-core -> what4 round trip can produce an equivalent but non-identical expression, which causes problems for compositional crypto verification, as it requires certain pairs of subexpressions to be identical in order to get decent solver performance. So this branch introduces a new function, fn munge<T>(x: T) -> T, which converts every what4 expr in x to saw-core and back. This operation seems to be idempotent, so it's safe to use even on expressions where some parts were already round-tripped due to calling a MethodSpec override, and I was able to get the Ring SHA256 verification to pass by wrapping both the "real" and Cryptol/spec sides of each equality in calls to munge.

• Equalities in postconditions are now converted into substitutions when possible. With our current approach to compositional verification, the overrides derived from equivalence tests typically look like this:

  // Test case:
  let y = rust_func(x);
  assert!(y == cryptol_func(x));
  
  // Override:
  let y = Symbolic::symbolic("result");
  assert!(y == cryptol_func(x));
  return y;

  It seems neither Yices nor Z3 will reliably substitute for y (effectively converting the override to return cryptol_func(x);). So we now recognize postconditions of this form and do the substitution explicitly in the override. (Specifically, we check for var == expr at the what4 level, so it works even for types like (u32, u32) that involve multiple what4 variables/expressions.)

• Add support for Rust's #[repr(transparent)] attribute. This attribute can be applied to a newtype (a struct with only one non-zero-sized field) to ensure that the newtype has the same representation in memory as the type that it wraps. With this change, #[repr(transparent)] guarantees that the newtype and the inner type have the same Crucible representation, enabling some no-op transmutes and pointer casts that were previously forbidden.

  #[repr(transparent)] newtypes are used in GenericArray and core::num::Wrapping, which appear in some crypto code.

• Add support for slice (&[T]) arguments in MethodSpecs. These are simply treated as a pair (&T, usize) of a reference and a length.

  This unfortunately makes for MethodSpecs that are quite strict by default: if the user's test case invokes f(&xs[1..3]), then the MethodSpec derived from that test case will require the argument slice to have length exactly 2 and to have at least one accessible element at offset -1. But relaxing these restrictions would require weakening the preconditions of the orginal test case written by the user, which doesn't seem feasible.

• Add overrides for additional Rust intrinsics (unchecked arithmetic and rotate_left/right).

The related changes to ordinary crux-mir are in GaloisInc/crucible#749

[atomb]

This is a super nice feature enhancement. As mentioned in a couple of comments, I wonder whether some of the What4 <-> SAWCore code could go into the saw-core-what4 package (probably as a future PR, and maybe along with some similar code from the saw-script package).

[atomb]

It's perhaps interesting to note that the first version of SAWScript separated equality assertions from other assertions in the MethodSpec datatype (by having different user-visible primitives for stating them) for performance reasons. I wonder whether we should return to that.

[atomb]

I wonder whether this should be moved into What4. It seems like it could be useful in other contexts.

[atomb]

This and a lot of the other, similar functions in this module seem like they could also be very broadly useful. It might even be worth having a What4-SAWCore integration package that included all these conversions back and forth. Centralizing that could make it easier to identify how to do the conversions as sparingly and effectively as possible.

[atomb]

On second thought, the existing saw-core-what4 package might be a good place for these sorts of functions.