-
Notifications
You must be signed in to change notification settings - Fork 0
/
shatest.cry
50 lines (40 loc) · 3.43 KB
/
shatest.cry
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
module shatest where
parameter
type a : #
type constraint (fin a)
//foreign sha384 : {b} (fin b, b == 384/8) => [a][8] -> [b][8]
/*
shatest_8> sha384 "12345678"
cryptol-osx: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues
%< ---------------------------------------------------
Revision: e261894654ceb3736f8de4a671f4cafc38ed6eba
Branch: master (uncommited files present)
Location: [Eval] evalType
Message: type variable not bound
TVBound (TParam {tpUnique = 4669, tpKind = KNum, tpFlav = TPModParam (Name {nUnique = 4669, nInfo = Declared (TopModule (ModName "shatest")) UserName, nNamespace = NSType, nIdent = Ident False "a", nFixity = Nothing, nLoc = Range {from = Position {line = 5, col = 8}, to = Position {line = 5, col = 9}, source = "./shatest.cry"}}), tpInfo = TVarInfo {tvarSource = Range {from = Position {line = 5, col = 8}, to = Position {line = 5, col = 9}, source = "./shatest.cry"}, tvarDesc = TVFromModParam (Name {nUnique = 4669, nInfo = Declared (TopModule (ModName "shatest")) UserName, nNamespace = NSType, nIdent = Ident False "a", nFixity = Nothing, nLoc = Range {from = Position {line = 5, col = 8}, to = Position {line = 5, col = 9}, source = "./shatest.cry"}})}})
CallStack (from HasCallStack):
panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.13.0.99-inplace:Cryptol.Utils.Panic
panic, called at src/Cryptol/Backend/Monad.hs:410:17 in cryptol-2.13.0.99-inplace:Cryptol.Backend.Monad
evalPanic, called at src/Cryptol/Eval/Type.hs:130:20 in cryptol-2.13.0.99-inplace:Cryptol.Eval.Type
%< ---------------------------------------------------
*/
//foreign sha384 : {tmp, b} (tmp == a, fin b, b == 384/8) => [a][8] -> [b][8]
/*
shatest_8> sha384 "12345678"
cryptol-osx: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues
%< ---------------------------------------------------
Revision: e261894654ceb3736f8de4a671f4cafc38ed6eba
Branch: master (uncommited files present)
Location: [Eval] evalType
Message: type variable not bound
TVBound (TParam {tpUnique = 4669, tpKind = KNum, tpFlav = TPModParam (Name {nUnique = 4669, nInfo = Declared (TopModule (ModName "shatest")) UserName, nNamespace = NSType, nIdent = Ident False "a", nFixity = Nothing, nLoc = Range {from = Position {line = 5, col = 8}, to = Position {line = 5, col = 9}, source = "./shatest.cry"}}), tpInfo = TVarInfo {tvarSource = Range {from = Position {line = 5, col = 8}, to = Position {line = 5, col = 9}, source = "./shatest.cry"}, tvarDesc = TVFromModParam (Name {nUnique = 4669, nInfo = Declared (TopModule (ModName "shatest")) UserName, nNamespace = NSType, nIdent = Ident False "a", nFixity = Nothing, nLoc = Range {from = Position {line = 5, col = 8}, to = Position {line = 5, col = 9}, source = "./shatest.cry"}})}})
CallStack (from HasCallStack):
panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-2.13.0.99-inplace:Cryptol.Utils.Panic
panic, called at src/Cryptol/Backend/Monad.hs:410:17 in cryptol-2.13.0.99-inplace:Cryptol.Backend.Monad
evalPanic, called at src/Cryptol/Eval/Type.hs:130:20 in cryptol-2.13.0.99-inplace:Cryptol.Eval.Type
%< ---------------------------------------------------
*/
foreign sha384 : {tmp, b} (tmp == a, fin b, b == 384/8) => [tmp][8] -> [b][8]
foreign sha256 : {tmp, b} (tmp == a, fin b, b == 256/8) => [tmp][8] -> [b][8]