Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Panic due to missing Field/Round instances in cryptol-verifier #763

Closed
brianhuffman opened this issue Jul 2, 2020 · 1 comment
Closed

Comments

@brianhuffman
Copy link
Contributor

sawscript> {{ recip : Rational -> Rational }}
saw: You have encountered a bug in cryptol-verifier's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol-verifier/issues

%< ---------------------------------------------------
  Revision:  54a754c0de22f00c580c2d4835ada906ed5be9eb
  Branch:    update-cryptol (uncommited files present)
  Location:  proveProp
  Message:   Field Rational
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-verifier-0.1-Ls5lX129NPzJfQFRDA1ukY:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:555:17 in cryptol-verifier-0.1-Ls5lX129NPzJfQFRDA1ukY:Verifier.SAW.Cryptol
  proveProp, called at src/Verifier/SAW/Cryptol.hs:844:23 in cryptol-verifier-0.1-Ls5lX129NPzJfQFRDA1ukY:Verifier.SAW.Cryptol
%< ---------------------------------------------------
sawscript> {{ roundAway : Rational -> Integer }}
saw: You have encountered a bug in cryptol-verifier's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol-verifier/issues

%< ---------------------------------------------------
  Revision:  54a754c0de22f00c580c2d4835ada906ed5be9eb
  Branch:    update-cryptol (uncommited files present)
  Location:  proveProp
  Message:   Round Rational
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Cryptol/Panic.hs:13:9 in cryptol-verifier-0.1-Ls5lX129NPzJfQFRDA1ukY:Verifier.SAW.Cryptol.Panic
  panic, called at src/Verifier/SAW/Cryptol.hs:555:17 in cryptol-verifier-0.1-Ls5lX129NPzJfQFRDA1ukY:Verifier.SAW.Cryptol
  proveProp, called at src/Verifier/SAW/Cryptol.hs:844:23 in cryptol-verifier-0.1-Ls5lX129NPzJfQFRDA1ukY:Verifier.SAW.Cryptol
%< ---------------------------------------------------
@brianhuffman
Copy link
Contributor Author

This was fixed in #804 when saw-script incorporated GaloisInc/cryptol-verifier#30. The cryptol-saw-core translator now implements those missing class dictionaries.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant