scCryptolType: unsupported type (var_blk1!_89 : Prelude.Nat)

[weaversa]

$ saw bignum.saw
...
...
...
You have encountered a bug in cryptol-verifier's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol-verifier/issues

%< --------------------------------------------------- 
  Revision:  315a6d201bbc002bb5e414945e885db5d9958444
  Branch:    HEAD
  Location:  scCryptolType
  Message:   scCryptolType: unsupported type (var_blk1!_89 : Prelude.Nat)
-> (var_off1!_90 : Prelude.Vec 64 Prelude.Bool)
-> Prelude.Bool
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-verifier-0.1-aALHfjF4GzKez0Qlpznm1:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:1158:19 in cryptol-verifier-0.1-aALHfjF4GzKez0Qlpznm1:Verifier.SAW.Cryptol
%< --------------------------------------------------- 

scCryptolType.tar.gz

[weaversa]

I ran into another one of these. Much simpler example attached (run saw xxhash.saw). It seems this panic happens when an unallocated pointer is passed to the function. Passing crucible-null instead allows the proof to succeed (see example below).

panic.tar.gz

[brianhuffman]

This is annoying. You can see what's going on if you put a print_goal statement in a do block before the z3 proof tactic in the verification command. You'll see that the proof goal mentions a variable named car_blk0!_52 which has type Nat:

[21:23:00.538] Goal XXH32 (safety assertion:):
[21:23:00.538] let { x@1 = Prelude.bvNat 64 0
      x@2 = Prelude.equalNat 0 var_blk0!_52
      x@3 = Prelude.bvEq 64 x@1 var_off0!_53
      x@4 = Prelude.and x@2 x@3
    }
 in Prelude.EqTrue
      (Prelude.implies Prelude.True
         (Prelude.implies
            (Prelude.and
               (Prelude.not (Prelude.ite Prelude.Bool x@2 x@3 x@4))
               (Prelude.bvult 64 (Prelude.bvNat 64 15) length))
            (Prelude.or x@4
               (Prelude.and (Prelude.equalNat 1 var_blk0!_52)
                  (Prelude.not (Prelude.bvult 64 x@1 var_off0!_53))))))

The Nat-typed variable comes from the block ID of the symbolic pointer. (For an allocated pointer, the block ID would be a concrete number.) A Nat-typed variable shouldn't be a problem in and of itself, but it seems that somewhere in saw-script there is some code that expects proof goals to only mention variables that have types that come from Cryptol. We should really never be using that scCryptolType function anywhere, as it is so fragile and can cause panics.

[brianhuffman]

As I mentioned in the thread for #31 (a duplicate of this issue), bisection shows that the panic from the cryptol-verifier package was fixed in GaloisInc/saw-script@f7bb948, which was part of GaloisInc/saw-script#728.

However, the proof still fails for a different reason, which is that crucible_fresh_pointer creates a symbolic saw-core variable of type Nat, and the saw-core backends can't handle symbolic variables of type Nat. I'll open a separate saw-script ticket for that.