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 on loading foreign declarations with recursive cryptol implementations #1567

Closed
qsctr opened this issue Aug 24, 2023 · 0 comments · Fixed by #1568
Closed

Panic on loading foreign declarations with recursive cryptol implementations #1567

qsctr opened this issue Aug 24, 2023 · 0 comments · Fixed by #1568
Assignees
Labels
bug Something not working correctly

Comments

@qsctr
Copy link
Contributor

qsctr commented Aug 24, 2023

Forgot to change this when adding support for cryptol implementations of foreign functions

foreign f : Bit -> Bit
f x = ~ g x

foreign g : Bit -> Bit
g x = ~ f x
Cryptol> :l test.cry
Loading module Cryptol
Loading module Main
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  7f7ec412eaa876989bdaa41e08a683dc19045f48
  Branch:    foreign-cryptol-def (uncommited files present)
  Location:  [Eval] Unexpected foreign declaration in recursive group
  Message:   (at test.cry:2:1--2:2, Main::f)
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.0.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Backend/Monad.hs:410:17 in cryptol-3.0.0.99-inplace:Cryptol.Backend.Monad
  evalPanic, called at src/Cryptol/Eval.hs:437:21 in cryptol-3.0.0.99-inplace:Cryptol.Eval
%< --------------------------------------------------- 
@qsctr qsctr added the bug Something not working correctly label Aug 24, 2023
@qsctr qsctr self-assigned this Aug 24, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant