Error: not a sequence #1283
Description
From this file, csa.cry:
csa : {a} (fin a) => [a] -> [a] -> [a] -> ([a+1], [a+1])
csa X Y Z = (S, C)
where
S = [0] # [x^y^z | x <- X | y <- Y | z <- Z]
C = [x/\y \/ x/\z \/ y/\z | x <- X | y <- Y | z <- Z] # [0]
csa_correct : {a} (fin a) => [a] -> [a] -> [a] -> Bit
csa_correct a b c = (0#a) + (0#b) + (0#c) == x + y
where (x,y) = csa a b c
property csa_0 = csa_correct`{0}
property csa_1 = csa_correct`{1}
property csa_8 = csa_correct`{8}
property csa_32 = csa_correct`{32}
I receive an error running in the current Cryptol Docker image:
% docker run -v `pwd`:/code galoisinc/cryptol --command ":prove" /code/csa.cry
Loading module Cryptol
Loading module Main
:prove csa_0
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] fromSeq
Message: not a sequence
ccatV left
CallStack (from HasCallStack):
panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.10.0-inplace:Cryptol.Utils.Panic
panic, called at src/Cryptol/Backend/Monad.hs:338:17 in cryptol-2.10.0-inplace:Cryptol.Backend.Monad
evalPanic, called at src/Cryptol/Eval/Value.hs:507:18 in cryptol-2.10.0-inplace:Cryptol.Eval.Value
%< ---------------------------------------------------