issue702

[robdockins]

Sort the fields of a record type before comparing with the fields in a concrete value in toExpr.

Fixes #702

[brianhuffman]

Have you tested this on the s2n example from the original post of #702? On Wednesday I made a patch that did the same thing as yours, but it wasn't sufficient to make that example work (which is why I didn't make a PR). Instead it revealed a different error message:

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:  c83f8317632d50b5909e4e9706b6e46c01110409
  Branch:    master (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:258:23 in cryptol-2.8.1-inplace:Cryptol.Symbolic.SBV
%< ---------------------------------------------------

I expect that you'll find the same result with your branch.

[robdockins]

I didn't actually, oops. I suspect you're right.

[brianhuffman]

We might as well go ahead and merge this PR, because it does fix the issue covered by the regression test. But we shouldn't close #702 yet, as it seems that there might be a second bug hiding behind this first one. @robdockins, maybe you could edit your top post to remove the "fixes 702" bit, so github won't close the ticket when this PR is merged.

[robdockins]

I'd rather just fix the issue, I think. Do you have a pointer to the original spec causing the problem? I can't seem to find/reproduce. The nearest version I can find has the proof succeeding.

[brianhuffman]

It looks like the counterexamples returned by :prove and :sat commands are not preserving the field ordering that I specified:

Main> let f (x : {izquierda : Bit, derecha : Bit}) = x.izquierda && x.derecha
Main> :sat f
f {derecha = True, izquierda = True} = True

I would expect to have this instead:

Main> let f (x : {izquierda : Bit, derecha : Bit}) = x.izquierda && x.derecha
Main> :sat f
f {izquierda = True, derecha = True} = True

[robdockins]

Yeah, that's the result of ordering the fields when we construct the FinType. To get this right, we'll need to implement the "order preserving map" from #706, or not sort things here and deal with all the use sites. I think we're better off merging this now and getting the display order thing worked out when we fix #706.

[brianhuffman]

That sounds reasonable. I'll file a separate ticket for preserving the field order in type signatures and counterexamples after this PR is merged.