You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We get a panic from the symbolic backend when we try to :prove a predicate involving a symbolic if-then-else on two records with the same fields written in different orders:
Cryptol> :prove \x -> (if x then { a = True, b = False } else { b = False, a = True }).a
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues
%< ---------------------------------------------------
Revision: ce0365fb80e66bf0aa844b0dac86d6d1777809fb
Branch: master (uncommited files present)
Location: Cryptol.Symbolic.Value
Message: mergeValue.mergeField: incompatible values
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/Value.hs:148:9 in cryptol-2.8.1-inplace:Cryptol.Symbolic.Value
%< ---------------------------------------------------
The code for mergeValue was assuming that we normalize the field order of all record expressions alphabetically, but it turns out that we don't do that.
Probably the right way to fix problems like this once and for all is to use a Map instead of a list of pairs in the VRecord constructor.
The text was updated successfully, but these errors were encountered:
We get a panic from the symbolic backend when we try to
:prove
a predicate involving a symbolic if-then-else on two records with the same fields written in different orders:The code for
mergeValue
was assuming that we normalize the field order of all record expressions alphabetically, but it turns out that we don't do that.Probably the right way to fix problems like this once and for all is to use a
Map
instead of a list of pairs in theVRecord
constructor.The text was updated successfully, but these errors were encountered: