search

GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 123 forks source link

Panic: type cannot be demoted inf - inf #1696

Open weaversa opened 3 months ago

weaversa commented 3 months ago

Help...related to #1693.

f : {m, n} (n < m) => [m] -> [n]
f x = take x
Cryptol> f (zero : [inf]) : [inf]
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< ---------------------------------------------------
  Revision:  UNKNOWN
  Branch:    UNKNOWN
  Location:  [Eval] evalTF
  Message:   type cannot be demoted
             inf - inf
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.1.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Backend/Monad.hs:410:17 in cryptol-3.1.0.99-inplace:Cryptol.Backend.Monad
  evalPanic, called at src/Cryptol/Eval/Type.hs:244:25 in cryptol-3.1.0.99-inplace:Cryptol.Eval.Type
%< ---------------------------------------------------
weaversa commented 3 months ago

take outside of a function seems to work just fine.

Cryptol> take (zero : [inf]) : [inf]
[False, False, False, False, False, ...]
yav commented 3 months ago

This is due to an incorrect simplification rule: a = ?x + b ~> ?x = a - b. This is only valid when b is finite, but this additional check was missing. PR #1697 fixes this, and under this PR the original definition of f is rejected, because there is no way to infer the back argument to pass to take.

yav commented 3 months ago

I am looking into why take is working on its own. I suspect it is either another incorrect rule or, perhaps, we are somehow defaulting the back argument to 0.