Typechecker gap in mir_assert

[sauclovian-g]

Using a complicated model (from Formal VerSo) I got this:

[19:25:03.498] Checking proof obligations soroban_auth_contract/4cc1c170::{impl#4}[0]::increment[0] ...
[19:25:03.506] Stack trace:
"soroban_verify" (.../example-proofs/auth.saw:79:1-79:15)
"mir_verify" (.../lib/soroban.saw:2653:4-2653:14)
"w4" (.../example-proofs/auth.saw:89:11-89:13)
Could not evaluate primitive Prelude.and
On argument 2
expected Bool

which should not happen.

The fix for the type error was this:

-  mir_assert {{ Values::symbol_eq key.0 countersym }};
+  mir_assert {{ Values::symbol_eq key.0 countersym heap }};

IOW, the type of the expression in mir_assert was T -> Bool instead of Bool but this wasn't found by the typechecker.

Not sure yet if the problem is actually attached to mir_assert or if it's something about the Cryptol expression.

[RyanGlScott]

I'd be interested to see a minimal example that triggers this. Although I wasn't able to come up with one myself, I did come up with a similarly buggy example:

// test.c
int f(int x) {
  return x;
}

// test.rs
pub fn f(x: u32) -> u32 {
    x
}

// test.saw
enable_experimental;

let
{{
foo : () -> Bit
foo _ = True
}};

let f_mir_spec = do {
  x <- mir_fresh_var "x" mir_u32;
  mir_assert {{ foo }};
  mir_execute_func [mir_term x];
  mir_return (mir_term x);
};

llvm <- mir_load_module "test.linked-mir.json";
mir_verify llvm "test::f" [] false f_mir_spec z3;

let f_llvm_spec = do {
  x <- llvm_fresh_var "x" (llvm_int 32);
  llvm_assert {{ foo }};
  llvm_execute_func [llvm_term x];
  llvm_return (llvm_term x);
};

mir <- llvm_load_module "test.bc";
llvm_verify mir "f" [] false f_llvm_spec z3;

Running this SAW script yields:

$ ~/Software/saw-1.2/bin/saw test.saw
[21:32:40.507] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[21:32:40.583] Verifying test/a774ef13::f[0] ...
[21:32:40.591] Simulating test/a774ef13::f[0] ...
[21:32:40.592] Checking proof obligations test/a774ef13::f[0] ...
[21:32:40.592] Proof succeeded! test/a774ef13::f[0]
[21:32:40.618] Verifying f ...
[21:32:40.619] Simulating f ...
[21:32:40.619] Verifier.SAW.Simulator.Concrete.toBool <<fun>>
CallStack (from HasCallStack):
  error, called at src/Verifier/SAW/Simulator/Concrete.hs:85:12 in saw-core-0.1-inplace:Verifier.SAW.Simulator.Concrete

Two problems here:

1. Although f_mir_spec asserts foo (which is not of type Bit), the call to mir_assert {{ foo }} somehow succeeds. Clearly, that should not happen.
2. f_llvm_spec also asserts foo, and at least it crashes. The error message it gives is pretty incomprehensible unless you know saw-core's implementation, however.

I agree that we should make {llvm,mir}_assert typecheck its argument, which should address both of these issues.

[sauclovian-g]

I had guessed that the Prelude.and behavior could be tickled by asserting more than one thing (so that the full assertion is stuff && foo) and isn't inherently any more interesting. However, that seems not to be the case; asserting something else as well doesn't change the behavior, including things that can't just be simplified away.

However, it seems the problem is not that the argument isn't being typechecked; something more subtle is going on. If you assert True && foo (or foo && True, or other more complicated things) it fails to typecheck (in both cases).

I will take a shot at cutting down the Formal VerSo model and see if I can get a reasonably self-contained example that fails as above; if nothing else the boundaries of where it does and doesn't fail to typecheck will probably help with understanding what's going on.