Encountered a bug in cryptol's implementation

[NLMalloy]

Received the following error running the proof on this branch
https://github.com/NLMalloy/s2n/tree/client_authentication

rfc_handshake_tls12> :prove tls12rfcSimulatesS2N `{16}
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  3038eacf5423113e9ec3b203b9600a25f1e2939f
  Branch:    HEAD
  Location:  Cryptol.Symbolic.sat
  Message:   unable to make assignment into expression
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.8.1-DvzTBEgJTnpHnZ3gCrRVwh:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Symbolic.hs:225:32 in cryptol-2.8.1-DvzTBEgJTnpHnZ3gCrRVwh:Cryptol.Symbolic
%< --------------------------------------------------- 

[brianhuffman]

As it turns out, this is a problem having to do with field name order in record types. Some parts of the code sort record fields alphabetically by name, while others don't, and yet other parts of the code assume that field names must match up in the same order. This is quite similar to issue #667, which I fixed a few months ago.

I should have a patch ready pretty soon.

As a temporary workaround you could sort the field names of your record types alphabetically in your Cryptol code; I haven't tried it, but I expect this would fix the problem.

[brianhuffman]

Here's a small example that exhibits the same error:

Cryptol> :sat \(x : {b:Bit, a:Bit}) -> x.a == x.b
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< ---------------------------------------------------
  Revision:  c83f8317632d50b5909e4e9706b6e46c01110409
  Branch:    master (uncommited files present)
  Location:  Cryptol.Symbolic.sat
  Message:   unable to make assignment into expression
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.8.1-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Symbolic/SBV.hs:199:32 in cryptol-2.8.1-inplace:Cryptol.Symbolic.SBV
%< ---------------------------------------------------

[robdockins]

I did a little looking into this, the problem seems to be in Cryptol.Eval.Concrete.toExpr, where we have the case:

    (TRec tfs, VRecord vfs) -> do
      let fns = Map.keys vfs
      guard (map fst tfs == fns)
      fes <- zipWithM go (map snd tfs) =<< lift (sequence (Map.elems vfs))
      return $ ERec (zip fns fes)

If tfs are not in sorted order, this will fail. We can fix this by sorting the list before doing the following steps.

However, it seems to me like the problem is mainly that the datatype for types represents records as a list of (Ident, Type) pairs. Shouldn't we just make this a Map Ident Type to more accurately indicate the order-independent intent?

[robdockins]

The link above is currently giving me a 404.

[brianhuffman]

PR #703 fixes the small example that I posted above, but it still fails on the original example with a different error message:

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

%< ---------------------------------------------------
  Revision:  9747f71bfa1af8d43703f8c2b3f111bc02b80c92
  Branch:    issue702 (uncommited files present)
  Location:  Cryptol.Symbolic.parseValue
  Message:   empty FTBit
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.8.1-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Symbolic/SBV.hs:255:23 in cryptol-2.8.1-inplace:Cryptol.Symbolic.SBV
%< ---------------------------------------------------

I'm working on coming up with a minimized example that we can use as a regression test.

[brianhuffman]

Here's a minimized example:

type T = { b : [32], a : [8] }
property bug (t : T) = False

Main> :prove bug
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< ---------------------------------------------------
  Revision:  9747f71bfa1af8d43703f8c2b3f111bc02b80c92
  Branch:    issue702 (uncommited files present)
  Location:  Cryptol.Symbolic.parseValue
  Message:   empty FTBit
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.8.1-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Symbolic/SBV.hs:255:23 in cryptol-2.8.1-inplace:Cryptol.Symbolic.SBV
%< ---------------------------------------------------

If you change the field names of type T so that they are in alphabetical order, then the :prove command doesn't panic, and returns a counterexample.

[NLMalloy]

The link above is currently giving me a 404.

Ah when i merged my PR, I deleted the remote branch out of habit. I still have it locally. Do you need me to push it up remotely again?

[brianhuffman]

We shouldn't need it any more; I still had a copy locally, and I used it to generate the minimized example above. We'll use the minimized examples as part of our suite of regression tests.