GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-01 16:42:56 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of https://github.com/GaloisInc/cryptol

Browse Source
This commit is contained in:
Dylan McNamee 2014-09-10 14:27:26 -07:00
commit 75852a2596
59 changed files with 593 additions and 163 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
cryptol/REPL/Command.hs
View File

@ -179,12 +179,14 @@ commandList =
, CommandDescr ":module" (FilenameArg moduleCmd)
"load a module"
, CommandDescr ":check" (ExprArg qcCmd)
"use random testing to check that the argument always returns true"
, CommandDescr ":check" (ExprArg (qcCmd QCRandom))
"use random testing to check that the argument always returns true (if no argument, check all properties)"
, CommandDescr ":exhaust" (ExprArg (qcCmd QCExhaust))
"use exhaustive testing to prove that the argument always returns true (if no argument, check all properties)"
, CommandDescr ":prove" (ExprArg proveCmd)
"use an external solver to prove that the argument always returns true"
"use an external solver to prove that the argument always returns true (if no argument, check all properties)"
, CommandDescr ":sat" (ExprArg satCmd)
"use a solver to find a satisfying assignment for which the argument returns true"
"use a solver to find a satisfying assignment for which the argument returns true (if no argument, find an assignment for all properties)"
, CommandDescr ":debug_specialize" (ExprArg specializeCmd)
"do type specialization on a closed expression"
]
@ -236,21 +238,26 @@ evalCmd str = do
P.LetInput decl -> do
replEvalDecl decl
qcCmd :: String -> REPL ()
qcCmd "" =
data QCMode = QCRandom | QCExhaust deriving (Eq, Show)
-- | Randomly test a property, or exhaustively check it if the number
-- of values in the type under test is smaller than the @tests@
-- environment variable, or we specify exhaustive testing.
qcCmd :: QCMode -> String -> REPL ()
qcCmd qcMode "" =
do xs <- getPropertyNames
if null xs
then io $ putStrLn "There are no properties in scope."
else forM_ xs $ \x ->
do io $ putStr $ "property " ++ x ++ " "
qcCmd x
qcCmd qcMode x
qcCmd str =
qcCmd qcMode str =
do expr <- replParseExpr str
(val,ty) <- replEvalExpr expr
EnvNum testNum <- getUser "tests"
case TestX.testableType ty of
Just (sz,vss) | sz <= toInteger testNum ->
Just (sz,vss) | qcMode == QCExhaust || sz <= toInteger testNum ->
do io $ putStrLn "Using exhaustive testing."
let doTest _ [] = panic "We've unexpectedly run out of test cases"
[]
@ -321,8 +328,15 @@ qcCmd str =
io $ mapM_ (print . pp . E.WithBase opts) vs
return False
proveCmd :: String -> REPL ()
proveCmd "" =
do xs <- getPropertyNames
if null xs
then io $ putStrLn "There are no properties in scope."
else forM_ xs $ \x ->
do io $ putStr $ "property " ++ x ++ " "
proveCmd x
proveCmd str = do
parseExpr <- replParseExpr str
(expr, schema) <- replCheckExpr parseExpr
@ -355,6 +369,13 @@ proveCmd str = do
-- to a record whose form depends on the expression given. See ticket
-- #66 for a discussion of this design.
satCmd :: String -> REPL ()
satCmd "" =
do xs <- getPropertyNames
if null xs
then io $ putStrLn "There are no properties in scope."
else forM_ xs $ \x ->
do io $ putStr $ "property "
satCmd x
satCmd str = do
parseExpr <- replParseExpr str
(expr, schema) <- replCheckExpr parseExpr

2
cryptol/REPL/Monad.hs
View File

@ -425,7 +425,7 @@ data OptionDescr = OptionDescr
userOptions :: OptionMap
userOptions = mkOptionMap
[ OptionDescr "base" (EnvNum 10) checkBase
[ OptionDescr "base" (EnvNum 16) checkBase
"the base to display words at"
, OptionDescr "debug" (EnvBool False) (const Nothing)
"enable debugging output"

6
docs/CryptolPrims.md
View File

@ -158,9 +158,9 @@ New types:
// Abbreviations
splitBy n = split`{parts = n}
groupBy n = split`{each = n}
tail n = splitAt`{front = 1}.2
take n = splitAt`{front = n}.1
drop n = splitAt`{front = n}.2
tail n = splitAt`{front = 1}.1
take n = splitAt`{front = n}.0
drop n = splitAt`{front = n}.1
/* Also, `length` is not really needed:
length : {n,a,m} (m >= width n) => [n]a -> [m]

BIN
docs/CryptolPrims.pdf
View File

Binary file not shown.

BIN
docs/ProgrammingCryptol.pdf
View File

Binary file not shown.

4
docs/ProgrammingCryptol/appendices/Syntax.tex
View File

@ -227,8 +227,8 @@ pattern matching or by using explicit component selectors. Explicit
component selectors are written as follows:
\begin{verbatim}
(15, 20).1 == 15
(15, 20).2 == 20
(15, 20).0 == 15
(15, 20).1 == 20
{ x = 15, y = 20 }.x == 15
\end{verbatim}

20
docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
View File

@ -238,15 +238,15 @@ Here are Cryptol's responses:
semantics at the object level in different contexts.}
\paragraph*{Projecting values from tuples} Use a {\tt .} followed by
$n$ to project the $n$-th component of a tuple. Nested projection is
$n$ to project the $n+1$-th component of a tuple. Nested projection is
not supported at this time.
\begin{Exercise}\label{ex:tup:2}
Try out the following examples:
\begin{Verbatim}
(1, 2+4).0
(1, 2+4).1
(1, 2+4).2
((1, 2), False, (3-1, (4, True))).3
((1, 2), False, (3-1, (4, True))).2
\end{Verbatim}
\todo[inline]{Include a more interesting nested example here once
\href{https://www.galois.com/cryptol/ticket/220}{ticket \#220} is
@ -259,16 +259,16 @@ projection to extract the value {\tt False} from the expression:
\begin{Answer}\ansref{ex:tup:2}
Here are Cryptol's responses:
\begin{Verbatim}
Cryptol> (1, 2+4).1
Cryptol> (1, 2+4).0
1
Cryptol> (1, 2+4).2
Cryptol> (1, 2+4).1
6
Cryptol> ((1, 2), False, (3-1, (4, True))).3
Cryptol> ((1, 2), False, (3-1, (4, True))).2
(2, (4, True))
\end{Verbatim}
The required expression would be:
\begin{Verbatim}
((1, 2), (2, (4, True), 6), False).3
((1, 2), (2, (4, True), 6), False).2
\end{Verbatim}
\end{Answer}
@ -1161,8 +1161,8 @@ In Cryptol, records are simply collections of named fields. In this
sense, they are very similar to tuples (Section~\ref{sec:tuple}),
which can be thought of records without field names\footnote{In fact,
the fields of a tuple {\it can} be accessed via the dot-notation,
with their names being their 1-indexed position in the tuple. So
{\tt (1,2).2 == 2}.}. Like a tuple, the fields of a record can be of
with their names being their 0-indexed position in the tuple. So
{\tt (1,2).1 == 2}.}. Like a tuple, the fields of a record can be of
any type. We construct records by listing the fields inside
curly-braces, separated by commas. We project fields out of a record
with the usual dot-notation. Note that the order of fields in a
@ -1594,7 +1594,7 @@ in parentheses, separated by commas: {\tt (3, 5, True) : ([8], [32],
Bit)}. Tuples' types follow the same structure: {\tt (2, (False, 3),
5) : ([8], (Bit, [32]), [32])}. A tuple component can be any type:
a word, another tuple, sequence, record, etc. Again, type inference
makes writing tuple types hardly every necessary.\indTypeInference
makes writing tuple types hardly ever necessary.\indTypeInference
\paragraph*{Sequences}\indTheSequenceType A sequence is simply a
collection of homogeneous elements. If the element type is {\tt t},

4
docs/Syntax.md
View File

@ -213,8 +213,8 @@ The components of a record or a tuple may be accessed in two ways: via
pattern matching or by using explicit component selectors. Explicit
component selectors are written as follows:
(15, 20).1 == 15
(15, 20).2 == 20
(15, 20).0 == 15
(15, 20).1 == 20
{ x = 15, y = 20 }.x == 15

BIN
docs/Syntax.pdf
View File

Binary file not shown.

4
docs/Version2Changes.md
View File

@ -215,8 +215,8 @@ becomes, in version 2:
sqDiffThm : ([8], [8]) -> Bit
property sqDiffThm x y = sqDiff1 (x, y) == sqDiff2 (x, y)
The `property` keyword is just an annotation. You can apply `:check`, `:sat`
and `:prove` to any function that returns `Bit`.
The `property` keyword is just an annotation. You can apply `:check`,
`:exhaust`, `:sat` and `:prove` to any function that returns `Bit`.
Current Limitations of `:modernize`
===================================

BIN
docs/Version2Changes.pdf
View File

Binary file not shown.

308
examples/ZUC.cry Normal file
View File

@ -0,0 +1,308 @@
// Copyright (c) 2011, 2014 Galois, Inc.
// An implementation of ZUC, Version 1.5
// Version info: If the following variable is set to True, then we implement
// Version 1.5 of ZUC. Otherwise, version 1.4 is implemented. There are
// precisely two points in the implementation where the difference matters,
// search for occurrences of version1_5 to spot them.
// Note that the ZUC test vectors below will not work for version 1.4, as the
// old test vectors are no longer published.
version1_5 : Bit
version1_5 = True
// addition in GF(2^31-1) over a list of terms
add : {a} (fin a) => [a][31] -> [31]
add xs =
sums ! 0
where
sums =
[0] #
[plus (s, x) | s <- sums
| x <- xs]
// the binary addition specified in the note at the end of section 3.2
plus : ([31], [31]) -> [31]
plus (a, b) =
if sab @ 0 then sab' + 1 else sab'
where
sab : [32]
sab = ((zero : [1]) # a) + ((zero : [1]) # b)
sab' : [31]
sab' = drop sab
// The ZUC LFSR is 16 31-bit words
type LFSR = [16][31]
// Section 3.2
LFSRWithInitializationMode : ([31], LFSR) -> LFSR
LFSRWithInitializationMode (u, ss) =
ss @@ [1 .. 15] # [s16]
where
v = add [s <<< c | s <- ss @@ [15, 13, 10, 4, 0, 0]
| c <- [15, 17, 21, 20, 8, 0]]
vu = if version1_5 then add [v, u] else v ^ u
s16 = if vu == 0 then `0x7FFFFFFF else vu
// Section 3.2
LFSRWithWorkMode : LFSR -> LFSR
LFSRWithWorkMode ss =
ss @@ [1 .. 15] # [s16]
where
v = add [s <<< c | s <- ss @@ [15, 13, 10, 4, 0, 0]
| c <- [15, 17, 21, 20, 8, 0]]
s16 = if v == 0 then `0x7FFFFFFF else v
// Section 3.3
BitReorganization : LFSR -> [4][32]
BitReorganization ss =
[ hi s15 # lo s14
, lo s11 # hi s9
, lo s7 # hi s5
, lo s2 # hi s0]
where
lo : [31] -> [16]
hi : [31] -> [16]
lo x = x @@ [15 .. 30]
hi x = x @@ [0 .. 15]
[s0, s2, s5, s7, s9, s11, s14, s15] = ss @@ [0, 2, 5, 7, 9, 11, 14, 15]
// Section 3.4
F : ([3][32], [2][32]) -> ([32], [2][32])
F ([X0, X1, X2], [R1, R2]) =
(W, [R1', R2'])
where
W = (X0 ^ R1) + R2
W1 = R1 + X1
W2 = R2 ^ X2
[W1H, W1L] = split W1
[W2H, W2L] = split W2
R1' = S (L1 (W1L # W2H))
R2' = S (L2 (W2L # W1H))
// Section 3.4.1
S : [32] -> [32]
S X =
Y0 # Y1 # Y2 # Y3
where
[X0, X1, X2, X3] = split X
[Y0, Y1, Y2, Y3] = [S0 X0, S1 X1, S2 X2, S3 X3]
// Example 8
property example8 = S(0x12345678) == 0xF9C05A4E
S0 : [8] -> [8]
S1 : [8] -> [8]
S2 : [8] -> [8]
S3 : [8] -> [8]
S0 x = S0Table @ x
S1 x = S1Table @ x
S2 = S0
S3 = S1
// Table 3.1
S0Table : [256][8]
S0Table =
[0x3E, 0x72, 0x5B, 0x47, 0xCA, 0xE0, 0x00, 0x33, 0x04, 0xD1, 0x54,
0x98, 0x09, 0xB9, 0x6D, 0xCB, 0x7B, 0x1B, 0xF9, 0x32, 0xAF, 0x9D,
0x6A, 0xA5, 0xB8, 0x2D, 0xFC, 0x1D, 0x08, 0x53, 0x03, 0x90, 0x4D,
0x4E, 0x84, 0x99, 0xE4, 0xCE, 0xD9, 0x91, 0xDD, 0xB6, 0x85, 0x48,
0x8B, 0x29, 0x6E, 0xAC, 0xCD, 0xC1, 0xF8, 0x1E, 0x73, 0x43, 0x69,
0xC6, 0xB5, 0xBD, 0xFD, 0x39, 0x63, 0x20, 0xD4, 0x38, 0x76, 0x7D,
0xB2, 0xA7, 0xCF, 0xED, 0x57, 0xC5, 0xF3, 0x2C, 0xBB, 0x14, 0x21,
0x06, 0x55, 0x9B, 0xE3, 0xEF, 0x5E, 0x31, 0x4F, 0x7F, 0x5A, 0xA4,
0x0D, 0x82, 0x51, 0x49, 0x5F, 0xBA, 0x58, 0x1C, 0x4A, 0x16, 0xD5,
0x17, 0xA8, 0x92, 0x24, 0x1F, 0x8C, 0xFF, 0xD8, 0xAE, 0x2E, 0x01,
0xD3, 0xAD, 0x3B, 0x4B, 0xDA, 0x46, 0xEB, 0xC9, 0xDE, 0x9A, 0x8F,
0x87, 0xD7, 0x3A, 0x80, 0x6F, 0x2F, 0xC8, 0xB1, 0xB4, 0x37, 0xF7,
0x0A, 0x22, 0x13, 0x28, 0x7C, 0xCC, 0x3C, 0x89, 0xC7, 0xC3, 0x96,
0x56, 0x07, 0xBF, 0x7E, 0xF0, 0x0B, 0x2B, 0x97, 0x52, 0x35, 0x41,
0x79, 0x61, 0xA6, 0x4C, 0x10, 0xFE, 0xBC, 0x26, 0x95, 0x88, 0x8A,
0xB0, 0xA3, 0xFB, 0xC0, 0x18, 0x94, 0xF2, 0xE1, 0xE5, 0xE9, 0x5D,
0xD0, 0xDC, 0x11, 0x66, 0x64, 0x5C, 0xEC, 0x59, 0x42, 0x75, 0x12,
0xF5, 0x74, 0x9C, 0xAA, 0x23, 0x0E, 0x86, 0xAB, 0xBE, 0x2A, 0x02,
0xE7, 0x67, 0xE6, 0x44, 0xA2, 0x6C, 0xC2, 0x93, 0x9F, 0xF1, 0xF6,
0xFA, 0x36, 0xD2, 0x50, 0x68, 0x9E, 0x62, 0x71, 0x15, 0x3D, 0xD6,
0x40, 0xC4, 0xE2, 0x0F, 0x8E, 0x83, 0x77, 0x6B, 0x25, 0x05, 0x3F,
0x0C, 0x30, 0xEA, 0x70, 0xB7, 0xA1, 0xE8, 0xA9, 0x65, 0x8D, 0x27,
0x1A, 0xDB, 0x81, 0xB3, 0xA0, 0xF4, 0x45, 0x7A, 0x19, 0xDF, 0xEE,
0x78, 0x34, 0x60]
// Table 3.2
S1Table : [256][8]
S1Table =
[0x55, 0xC2, 0x63, 0x71, 0x3B, 0xC8, 0x47, 0x86, 0x9F, 0x3C, 0xDA,
0x5B, 0x29, 0xAA, 0xFD, 0x77, 0x8C, 0xC5, 0x94, 0x0C, 0xA6, 0x1A,
0x13, 0x00, 0xE3, 0xA8, 0x16, 0x72, 0x40, 0xF9, 0xF8, 0x42, 0x44,
0x26, 0x68, 0x96, 0x81, 0xD9, 0x45, 0x3E, 0x10, 0x76, 0xC6, 0xA7,
0x8B, 0x39, 0x43, 0xE1, 0x3A, 0xB5, 0x56, 0x2A, 0xC0, 0x6D, 0xB3,
0x05, 0x22, 0x66, 0xBF, 0xDC, 0x0B, 0xFA, 0x62, 0x48, 0xDD, 0x20,
0x11, 0x06, 0x36, 0xC9, 0xC1, 0xCF, 0xF6, 0x27, 0x52, 0xBB, 0x69,
0xF5, 0xD4, 0x87, 0x7F, 0x84, 0x4C, 0xD2, 0x9C, 0x57, 0xA4, 0xBC,
0x4F, 0x9A, 0xDF, 0xFE, 0xD6, 0x8D, 0x7A, 0xEB, 0x2B, 0x53, 0xD8,
0x5C, 0xA1, 0x14, 0x17, 0xFB, 0x23, 0xD5, 0x7D, 0x30, 0x67, 0x73,
0x08, 0x09, 0xEE, 0xB7, 0x70, 0x3F, 0x61, 0xB2, 0x19, 0x8E, 0x4E,
0xE5, 0x4B, 0x93, 0x8F, 0x5D, 0xDB, 0xA9, 0xAD, 0xF1, 0xAE, 0x2E,
0xCB, 0x0D, 0xFC, 0xF4, 0x2D, 0x46, 0x6E, 0x1D, 0x97, 0xE8, 0xD1,
0xE9, 0x4D, 0x37, 0xA5, 0x75, 0x5E, 0x83, 0x9E, 0xAB, 0x82, 0x9D,
0xB9, 0x1C, 0xE0, 0xCD, 0x49, 0x89, 0x01, 0xB6, 0xBD, 0x58, 0x24,
0xA2, 0x5F, 0x38, 0x78, 0x99, 0x15, 0x90, 0x50, 0xB8, 0x95, 0xE4,
0xD0, 0x91, 0xC7, 0xCE, 0xED, 0x0F, 0xB4, 0x6F, 0xA0, 0xCC, 0xF0,
0x02, 0x4A, 0x79, 0xC3, 0xDE, 0xA3, 0xEF, 0xEA, 0x51, 0xE6, 0x6B,
0x18, 0xEC, 0x1B, 0x2C, 0x80, 0xF7, 0x74, 0xE7, 0xFF, 0x21, 0x5A,
0x6A, 0x54, 0x1E, 0x41, 0x31, 0x92, 0x35, 0xC4, 0x33, 0x07, 0x0A,
0xBA, 0x7E, 0x0E, 0x34, 0x88, 0xB1, 0x98, 0x7C, 0xF3, 0x3D, 0x60,
0x6C, 0x7B, 0xCA, 0xD3, 0x1F, 0x32, 0x65, 0x04, 0x28, 0x64, 0xBE,
0x85, 0x9B, 0x2F, 0x59, 0x8A, 0xD7, 0xB0, 0x25, 0xAC, 0xAF, 0x12,
0x03, 0xE2, 0xF2]
// Section 3.4.2
L1 : [32] -> [32]
L1 X = X ^ X <<< 2 ^ X <<< 10 ^ X <<< 18 ^ X <<< 24
// Section 3.4.2
L2 : [32] -> [32]
L2 X = X ^ X <<< 8 ^ X <<< 14 ^ X <<< 22 ^ X <<< 30
// Section 3.5
LoadKey : ([128], [128]) -> LFSR
LoadKey (key, iv) =
[k # d # i | k <- ks
| i <- is
| d <- ds]
where
ks : [16][8]
ks = split key
is : [16][8]
is = split iv
ds : [16][15]
ds =
[ 0b100010011010111, 0b010011010111100
, 0b110001001101011, 0b001001101011110
, 0b101011110001001, 0b011010111100010
, 0b111000100110101, 0b000100110101111
, 0b100110101111000, 0b010111100010011
, 0b110101111000100, 0b001101011110001
, 0b101111000100110, 0b011110001001101
, 0b111100010011010, 0b100011110101100
]
type ZUC = (LFSR, [32], [32])
// Return an infinite sequence of ZUC states by applying the initialization step
// repeatedly. This is a generalization of section 3.6.1
InitializeZUC : ([128], [128]) -> [inf]ZUC
InitializeZUC (key, iv) =
outs
where
initLFSR = LoadKey (key, iv)
outs = [(initLFSR, 0, 0)] # [step out | out <- outs]
step (lfsr, R1, R2) =
(LFSRWithInitializationMode (drop (w >> 1), lfsr), R1', R2')
where
[X0, X1, X2, X3] = BitReorganization lfsr
(w', [R1', R2']) = F ([X0, X1, X2], [R1, R2])
w = if version1_5 then w' else w' ^ X3
// Section 3.6.2
WorkingStage : ZUC -> ZUC
WorkingStage (lfsr, R1, R2) =
(lfsr', R1', R2')
where
[X0, X1, X2, _] = BitReorganization lfsr
(_, [R1', R2']) = F ([X0, X1, X2], [R1, R2])
lfsr' = LFSRWithWorkMode lfsr
// Section 3.6.2
ProductionStage : ZUC -> ([32], ZUC)
ProductionStage (lfsr, R1, R2) =
(w ^ X3, (lfsr', R1', R2'))
where
[X0, X1, X2, X3] = BitReorganization lfsr
(w, [R1', R2']) = F ([X0, X1, X2], [R1, R2])
lfsr' = LFSRWithWorkMode lfsr
// ZUC API
ZUC : [128] -> [128] -> [inf][32]
ZUC key iv =
tail [w | (w, _) <- zucs]
where
initZuc = WorkingStage (InitializeZUC (key, iv) @ 32)
zucs = [(zero, initZuc)] # [ProductionStage zuc | (_, zuc) <- zucs]
// Test vectors
property ZUC_TestVectors =
t1 && t2 && t3 && t4
where
t1 = take (ZUC zero zero ) == [0x27BEDE74, 0x018082DA]
t2 = take (ZUC (~zero) (~zero)) == [0x0657CFA0, 0x7096398B]
t3 = take (ZUC (join [ 0x3D, 0x4C, 0x4B, 0xE9, 0x6A, 0x82, 0xFD, 0xAE
, 0xB5, 0x8F, 0x64, 0x1D, 0xB1, 0x7B, 0x45, 0x5B
])
(join [ 0x84, 0x31, 0x9A, 0xA8, 0xDE, 0x69, 0x15, 0xCA
, 0x1F, 0x6B, 0xDA, 0x6B, 0xFB, 0xD8, 0xC7, 0x66
])) == [0x14F1C272, 0x3279C419]
t4 = take ks # [ks @ 1999] == [0xED4400E7, 0x0633E5C5, 0x7A574CDB]
where
ks = ZUC (join [ 0x4D, 0x32, 0x0B, 0xFA, 0xD4, 0xC2, 0x85, 0xBF
, 0xD6, 0xB8, 0xBD, 0x00, 0xF3, 0x9D, 0x8B, 0x41
])
(join [ 0x52, 0x95, 0x9D, 0xAB, 0xA0, 0xBF, 0x17, 0x6E
, 0xCE, 0x2D, 0xC3, 0x15, 0x04, 0x9E, 0xB5, 0x74
])
// 3.3-3.6 of the implementor's test data document lists "LFSR-state at the
// beginning", which is immediately after running LoadKey.
property LoadKey_TestVectors =
[ LoadKey(k, iv) == lfsr0
| k <- ks
| iv <- ivs
| lfsr0 <- lfsr0s
] == ~0
where
ks = [ 0
, ~0
, 0x3d4c4be96a82fdaeb58f641db17b455b
, 0x4d320bfad4c285bfd6b8bd00f39d8b41
]
ivs = [ 0
, ~0
, 0x84319aa8de6915ca1f6bda6bfbd8c766
, 0x52959daba0bf176ece2dc315049eb574
]
lfsr0s = [ [ `0x0044d700, `0x0026bc00, `0x00626b00, `0x00135e00
, `0x00578900, `0x0035e200, `0x00713500, `0x0009af00
, `0x004d7800, `0x002f1300, `0x006bc400, `0x001af100
, `0x005e2600, `0x003c4d00, `0x00789a00, `0x0047ac00
]
, [ `0x7fc4d7ff, `0x7fa6bcff, `0x7fe26bff, `0x7f935eff
, `0x7fd789ff, `0x7fb5e2ff, `0x7ff135ff, `0x7f89afff
, `0x7fcd78ff, `0x7faf13ff, `0x7febc4ff, `0x7f9af1ff
, `0x7fde26ff, `0x7fbc4dff, `0x7ff89aff, `0x7fc7acff
]
, [ `0x1ec4d784, `0x2626bc31, `0x25e26b9a, `0x74935ea8
, `0x355789de, `0x4135e269, `0x7ef13515, `0x5709afca
, `0x5acd781f, `0x47af136b, `0x326bc4da, `0x0e9af16b
, `0x58de26fb, `0x3dbc4dd8, `0x22f89ac7, `0x2dc7ac66
]
, [ `0x26c4d752, `0x1926bc95, `0x05e26b9d, `0x7d135eab
, `0x6a5789a0, `0x6135e2bf, `0x42f13517, `0x5f89af6e
, `0x6b4d78ce, `0x5c2f132d, `0x5eebc4c3, `0x001af115
, `0x79de2604, `0x4ebc4d9e, `0x45f89ab5, `0x20c7ac74
]
]
// Collision attack on ZUC. Only version1.5 is resistant to it. Thus, the
// following theorem holds only when version1_5 is set to True.
//
// NB. We only compare the first output of the InitializeZUC sequence, as it
// cuts down on the problem size and is sufficient to ensure the iv's will be
// the same. That is, if this theorem fails, then so would the final iv's used
// by ZUC.
//
// Use a solver other than CVC4; Z3 and Boolector do it quickly.
property ZUC_isResistantToCollisionAttack k iv1 iv2 =
if iv1 != iv2
then InitializeZUC (k, iv1) @ 1 != InitializeZUC (k, iv2) @ 1
else True

2
src/Cryptol/Eval.hs
View File

@ -139,7 +139,7 @@ evalSel env e sel = case sel of
tupleSel n v =
case v of
VTuple vs -> vs !! (n - 1)
VTuple vs -> vs !! n
VSeq False vs -> VSeq False [ tupleSel n v1 | v1 <- vs ]
VStream vs -> VStream [ tupleSel n v1 | v1 <- vs ]
VFun f -> VFun (\x -> tupleSel n (f x))

10
src/Cryptol/Parser.y
View File

@ -145,6 +145,7 @@ import Paths_cryptol
%name expr expr
%name decl decl
%name decls decls
%name declsLayout decls_layout
%name letDecl let_decl
%name repl repl
%name modName modName
@ -318,6 +319,10 @@ vdecls :: { [Decl] }
| vdecls 'v;' decl { $3 : $1 }
| vdecls ';' decl { $3 : $1 }
decls_layout :: { [Decl] }
: 'v{' vdecls 'v}' { $2 }
| 'v{' 'v}' { [] }
repl :: { ReplInput }
: expr { ExprInput $1 }
| let_decl { LetInput $1 }
@ -748,7 +753,10 @@ parseDecl :: String -> Either ParseError Decl
parseDecl = parseDeclWith defaultConfig
parseDeclsWith :: Config -> String -> Either ParseError [Decl]
parseDeclsWith cfg = parse cfg { cfgModuleScope = False } decls
parseDeclsWith cfg = parse cfg { cfgModuleScope = ms } decls'
where (ms, decls') = case cfgLayout cfg of
Layout -> (True, declsLayout)
NoLayout -> (False, decls)
parseDecls :: String -> Either ParseError [Decl]
parseDecls = parseDeclsWith defaultConfig

4
src/Cryptol/Parser/AST.hs
View File

@ -276,8 +276,8 @@ list selectors, but they are used during the desugaring of patterns.
-}
data Selector = TupleSel Int (Maybe Int)
-- ^ One-based tuple selection.
-- Optionally specifies the shape of the tuple.
-- ^ Zero-based tuple selection.
-- Optionally specifies the shape of the tuple (one-based).
| RecordSel Name (Maybe [Name])
-- ^ Record selection.

5
src/Cryptol/Parser/LexerUtils.hs
View File

@ -18,8 +18,6 @@ import Data.Char(toLower)
import Data.Word(Word8)
import Codec.Binary.UTF8.String(encodeChar)
import Debug.Trace
data Config = Config
{ cfgSource :: !FilePath -- ^ File that we are working on
@ -270,8 +268,7 @@ layout cfg ts0 = loop implicitScope [] ts0
done ts s = (reverse (t:ts), s)
closingToken = ty == Sym ParenR
|| ty == Sym Comma
closingToken = ty `elem` [ Sym ParenR, Sym Comma, Sym BracketR, Sym CurlyR ]
virt :: Config -> Position -> TokenV -> Located Token
virt cfg pos x = Located { srcRange = Range

6
src/Cryptol/Parser/NoPat.hs
View File

@ -75,7 +75,7 @@ noPat pat =
let len = length ps
ty = TTuple (replicate len TWild)
getN a n = sel a qx (TupleSel n (Just len))
return (pTy r x ty, zipWith getN as [1..] ++ concat dss)
return (pTy r x ty, zipWith getN as [0..] ++ concat dss)
PList [] ->
do x <- newName
@ -116,8 +116,8 @@ noPat pat =
let qx = mkUnqual x
qtmp = mkUnqual tmp
bTmp = simpleBind (Located r qtmp) (EApp (ECon ECSplitAt) (EVar qx))
b1 = sel a1 qtmp (TupleSel 1 (Just 2))
b2 = sel a2 qtmp (TupleSel 2 (Just 2))
b1 = sel a1 qtmp (TupleSel 0 (Just 2))
b2 = sel a2 qtmp (TupleSel 1 (Just 2))
return (pVar r x, bTmp : b1 : b2 : ds1 ++ ds2)
PLocated p r1 -> inRange r1 (noPat p)

4
src/Cryptol/Parser/ParserUtils.hs
View File

@ -145,8 +145,8 @@ numLit x = panic "[Parser] numLit" ["invalid numeric literal", show x]
mkTupleSel :: Range -> Integer -> ParseM (Located Selector)
mkTupleSel pos n
| n == 0 = errorMessage pos
"0 is not a valid tuple selector (they start from 1)."
| n < 0 = errorMessage pos
(show n ++ " is not a valid tuple selector (they start from 0).")
| toInteger asInt /= n = errorMessage pos "Tuple selector is too large."
| otherwise = return $ Located pos $ TupleSel asInt Nothing
where asInt = fromInteger n

2
src/Cryptol/Symbolic.hs
View File

@ -305,7 +305,7 @@ evalSel sel v =
case sel of
TupleSel n _ ->
case v of
VTuple xs -> xs !! (n - 1) -- 1-based indexing
VTuple xs -> xs !! n -- 0-based indexing
VSeq b xs -> VSeq b (map (evalSel sel) xs)
VStream xs -> VStream (map (evalSel sel) xs)
VFun f -> VFun (\x -> evalSel sel (f x))

27
src/Cryptol/Testing/Random.hs
View File

@ -15,10 +15,8 @@ import Cryptol.Eval.Value (BV(..),Value,GenValue(..),ppValue,defaultPPOpts)
import Cryptol.Utils.Panic (panic)
import Cryptol.TypeCheck.AST (Name,Type(..),TCon(..),TC(..),tNoUser)
import System.Random (RandomGen, split, random, randoms, randomR)
import Data.Word (Word64)
import Data.Bits (shiftL, shiftR, (.|.), (.&.), setBit)
import Data.List (unfoldr, foldl', genericTake)
import System.Random (RandomGen, split, random, randomR)
import Data.List (unfoldr, genericTake)
import Control.Monad (forM)
type Gen g = Int -> g -> (Value, g)
@ -103,24 +101,9 @@ randomBit _ g =
-- The size parameter is assumed to vary between 1 and 100, and we use
-- it to generate smaller numbers first.
randomWord :: RandomGen g => Integer -> Gen g
randomWord w sz g =
let (g1,g2) = split g
(bits,g3) = randomR (0, div (sz * fromInteger w + 99) 100) g2
mk num new = (num `shiftL` 64) .|. toInteger (new :: Word64)
x : xs = randoms g1
-- mask most significant word, so that we don't go over `bits`
mask = let r = bits `rem` 64
shR = if r == 0 then 0 else 64 - r
in (-1) `shiftR` shR
x' = x .&. mask
val = foldl' mk 0 $ genericTake (div (bits + 63) 64) (x' : xs)
finalVal = if sz > 1 && bits > 0 then setBit val (bits - 1) else val
in (VWord (BV w finalVal), g3)
randomWord w _sz g =
let (val, g1) = randomR (0,2^w-1) g
in (VWord (BV w val), g1)
-- | Generate a random infinite stream value.
randomStream :: RandomGen g => Gen g -> Gen g

2
src/Cryptol/Transform/MonoValues.hs
View File

@ -290,7 +290,7 @@ rewDeclGroup rews dg =
) (TupleSel n (Just tupAr))
}
return (tupD : zipWith mkFunDef [ 1 .. ] polyDs)
return (tupD : zipWith mkFunDef [ 0 .. ] polyDs)
--------------------------------------------------------------------------------

6
src/Cryptol/TypeCheck/Solver/Selector.hs
View File

@ -30,7 +30,7 @@ recordType labels =
tupleType :: Int -> InferM Type
tupleType n =
do fields <- mapM (\x -> newType (ordinal x <+> text "tuple field") KType)
[ 1 .. n ]
[ 0 .. (n-1) ]
return (tTuple fields)
listType :: Int -> InferM Type
@ -86,8 +86,8 @@ solveSelector sel outerT =
case ty of
TCon (TC (TCTuple m)) ts ->
return $ do guard (1 <= n && n <= m)
return $ ts !! (n-1)
return $ do guard (0 <= n && n < m)
return $ ts !! n
TCon (TC TCSeq) [len,el] -> liftSeq len el
TCon (TC TCFun) [t1,t2] -> liftFun t1 t2

2
src/Cryptol/TypeCheck/TypeOf.hs
View File

@ -99,7 +99,7 @@ fastSchemaOf tyenv expr =
-- | Yields the return type of the selector on the given argument type.
typeSelect :: Type -> Selector -> Type
typeSelect (TCon _tctuple ts) (TupleSel i _) = ts !! (i - 1)
typeSelect (TCon _tctuple ts) (TupleSel i _) = ts !! i
typeSelect (TRec fields) (RecordSel n _) = fromJust (lookup n fields)
typeSelect (TCon _tcseq [_, a]) (ListSel _ _) = a
typeSelect ty _ = panic "Cryptol.TypeCheck.TypeOf.typeSelect"

10
tests/issues/issue006.icry.stdout
View File

@ -1,8 +1,8 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
8
8
0
120
8
0x00000008
0x00000008
0x00000000
0x00000078
0x00000008

28
tests/issues/issue066.icry.stdout
View File

@ -4,29 +4,29 @@ it : {result : Bit, arg1 : [4]}
Run-time error: no counterexample available
True
f 0 = False
f 0x0 = False
it : {result : Bit, arg1 : [4]}
{result = False, arg1 = 0}
{result = False, arg1 = 0x0}
False
f 3 = True
f 0x3 = True
it : {result : Bit, arg1 : [4]}
{result = True, arg1 = 3}
{result = True, arg1 = 0x3}
True
Unsatisfiable.
it : {result : Bit, arg1 : [4]}
Run-time error: no satisfying assignment available
g {x = 0, y = 1} = False
g {x = 0x00000000, y = 0x00000001} = False
it : {result : Bit, arg1 : {x : [32], y : [32]}}
{result = False, arg1 = {x = 0, y = 1}}
g {x = 0, y = 0} = True
{result = False, arg1 = {x = 0x00000000, y = 0x00000001}}
g {x = 0x00000000, y = 0x00000000} = True
it : {result : Bit, arg1 : {x : [32], y : [32]}}
{result = True, arg1 = {x = 0, y = 0}}
h 0 0 = False
{result = True, arg1 = {x = 0x00000000, y = 0x00000000}}
h 0x00 0x00 = False
it : {result : Bit, arg1 : [8], arg2 : [8]}
{result = False, arg1 = 0, arg2 = 0}
0
0
h 0 1 = True
{result = False, arg1 = 0x00, arg2 = 0x00}
0x00
0x00
h 0x00 0x01 = True
it : {result : Bit, arg1 : [8], arg2 : [8]}
{result = True, arg1 = 0, arg2 = 1}
{result = True, arg1 = 0x00, arg2 = 0x01}

8
tests/issues/issue081.icry.stdout
View File

@ -1,7 +1,7 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
2
11
2
11
0x2
0xb
0x2
0xb

3
tests/issues/issue083.cry Normal file
View File

@ -0,0 +1,3 @@
x : ([31], [31]) -> [32]
x (y, z) = w
where w = (zero # y) + (zero # z)

1
tests/issues/issue083.icry Normal file
View File

@ -0,0 +1 @@
:l issue083.cry

3
tests/issues/issue083.icry.stdout Normal file
View File

@ -0,0 +1,3 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main

2
tests/issues/issue084.icry.stdout
View File

@ -1,3 +1,3 @@
Loading module Cryptol
Assuming a = 5
3
0x03

2
tests/issues/issue090.icry.stdout
View File

@ -1,2 +1,2 @@
Loading module Cryptol
0
0x0

4
tests/issues/issue093.cry Normal file
View File

@ -0,0 +1,4 @@
property t0 = True
property t1 x = x == (x : [32])
property t2 x y = if (x : [32]) < (y : [32]) then y != zero else True
not_a_prop = True

4
tests/issues/issue093.icry Normal file
View File

@ -0,0 +1,4 @@
:l issue093.cry
:check
:prove
:sat

18
tests/issues/issue093.icry.stdout Normal file
View File

@ -0,0 +1,18 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
property t0 Using exhaustive testing.
0%passed 1 tests.
QED
property t1 Using random testing.
testing... 0% 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% 51% 52% 53% 54% 55% 56% 57% 58% 59% 60% 61% 62% 63% 64% 65% 66% 67% 68% 69% 70% 71% 72% 73% 74% 75% 76% 77% 78% 79% 80% 81% 82% 83% 84% 85% 86% 87% 88% 89% 90% 91% 92% 93% 94% 95% 96% 97% 98% 99%passed 100 tests.
Coverage: 0.00% (100 of 2^^32 values)
property t2 Using random testing.
testing... 0% 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% 51% 52% 53% 54% 55% 56% 57% 58% 59% 60% 61% 62% 63% 64% 65% 66% 67% 68% 69% 70% 71% 72% 73% 74% 75% 76% 77% 78% 79% 80% 81% 82% 83% 84% 85% 86% 87% 88% 89% 90% 91% 92% 93% 94% 95% 96% 97% 98% 99%passed 100 tests.
Coverage: 0.00% (100 of 2^^64 values)
property t0 Q.E.D.
property t1 Q.E.D.
property t2 Q.E.D.
property t0 = True
property t1 0x00000000 = True
property t2 0x00000000 0x00000000 = True

3
tests/issues/issue094.icry Normal file
View File

@ -0,0 +1,3 @@
let f x = (x : [8]) == x
:check f
:exhaust f

7
tests/issues/issue094.icry.stdout Normal file
View File

@ -0,0 +1,7 @@
Loading module Cryptol
Using random testing.
testing... 0% 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% 51% 52% 53% 54% 55% 56% 57% 58% 59% 60% 61% 62% 63% 64% 65% 66% 67% 68% 69% 70% 71% 72% 73% 74% 75% 76% 77% 78% 79% 80% 81% 82% 83% 84% 85% 86% 87% 88% 89% 90% 91% 92% 93% 94% 95% 96% 97% 98% 99%passed 100 tests.
Coverage: 39.06% (100 of 256 values)
Using exhaustive testing.
0% 0% 0% 1% 1% 1% 2% 2% 3% 3% 3% 4% 4% 5% 5% 5% 6% 6% 7% 7% 7% 8% 8% 8% 9% 9% 10% 10% 10% 11% 11% 12% 12% 12% 13% 13% 14% 14% 14% 15% 15% 16% 16% 16% 17% 17% 17% 18% 18% 19% 19% 19% 20% 20% 21% 21% 21% 22% 22% 23% 23% 23% 24% 24% 25% 25% 25% 26% 26% 26% 27% 27% 28% 28% 28% 29% 29% 30% 30% 30% 31% 31% 32% 32% 32% 33% 33% 33% 34% 34% 35% 35% 35% 36% 36% 37% 37% 37% 38% 38% 39% 39% 39% 40% 40% 41% 41% 41% 42% 42% 42% 43% 43% 44% 44% 44% 45% 45% 46% 46% 46% 47% 47% 48% 48% 48% 49% 49% 50% 50% 50% 51% 51% 51% 52% 52% 53% 53% 53% 54% 54% 55% 55% 55% 56% 56% 57% 57% 57% 58% 58% 58% 59% 59% 60% 60% 60% 61% 61% 62% 62% 62% 63% 63% 64% 64% 64% 65% 65% 66% 66% 66% 67% 67% 67% 68% 68% 69% 69% 69% 70% 70% 71% 71% 71% 72% 72% 73% 73% 73% 74% 74% 75% 75% 75% 76% 76% 76% 77% 77% 78% 78% 78% 79% 79% 80% 80% 80% 81% 81% 82% 82% 82% 83% 83% 83% 84% 84% 85% 85% 85% 86% 86% 87% 87% 87% 88% 88% 89% 89% 89% 90% 90% 91% 91% 91% 92% 92% 92% 93% 93% 94% 94% 94% 95% 95% 96% 96% 96% 97% 97% 98% 98% 98% 99% 99%passed 256 tests.
QED

2
tests/issues/issue098.icry.stdout
View File

@ -1,3 +1,3 @@
Loading module Cryptol
Assuming a = 4
[2, 4, 6, 8, 10, 12, 14, 0, 2, 4]
[0x2, 0x4, 0x6, 0x8, 0xa, 0xc, 0xe, 0x0, 0x2, 0x4]

8
tests/issues/issue108.icry.stdout
View File

@ -2,9 +2,9 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
Assuming a = 0
0
0x0
Assuming a = 2
2
0x2
Assuming a = 4
7
55
0x7
0x37

2
tests/issues/issue149.icry.stdout
View File

@ -1,3 +1,3 @@
Loading module Cryptol
Assuming a = 6
49
0x31

93
tests/issues/issue152.icry.stdout
View File

@ -1,39 +1,56 @@
Loading module Cryptol
108693264
[3, 23674312268953995, 105640702603489, 14, 15672, ...]
[[3, 1, 210, 22, 90, 1, 130, 13, 7, 90, 1, 7, 97, 0, 0, 8, 86, 252,
14, 210, 1, 3, 12, 6, 1, 5, 191, 8, 2, 5, 0, 9],
[1, 4, 0, 1, 1, 27, 4, 8, 0, 7, 0, 12, 109, 10, 25, 173, 243, 46,
2, 241, 215, 1, 63, 16, 1, 1, 17, 49, 3, 18, 190, 3],
[2, 1, 0, 1, 3, 5, 61, 145, 0, 1, 239, 250, 1, 2, 7, 251, 17, 1,
57, 1, 1, 5, 28, 29, 110, 15, 22, 125, 3, 7, 125, 3],
[0, 0, 133, 14, 33, 2, 29, 52, 137, 37, 9, 1, 1, 14, 30, 7, 29,
175, 6, 4, 9, 18, 17, 3, 1, 13, 0, 1, 49, 7, 178, 11],
[12, 4, 254, 85, 42, 0, 28, 163, 149, 201, 10, 1, 21, 126, 2, 1,
11, 7, 151, 1, 0, 2, 9, 19, 43, 28, 139, 0, 125, 12, 35, 113],
[61, 25, 48, 59, 99, 2, 1, 80, 0, 98, 1, 4, 3, 245, 39, 93, 58, 0,
93, 136, 1, 34, 205, 40, 4, 92, 5, 1, 160, 111, 123, 1],
[3, 0, 0, 0, 195, 95, 103, 143, 21, 20, 9, 18, 3, 3, 3, 0, 34, 52,
1, 238, 72, 1, 124, 6, 118, 165, 0, 29, 3, 31, 1, 12],
[1, 1, 11, 12, 2, 73, 55, 3, 1, 16, 1, 190, 86, 3, 27, 9, 112, 175,
155, 4, 0, 2, 6, 3, 103, 2, 155, 4, 7, 2, 29, 0],
[0, 1, 72, 84, 1, 219, 21, 1, 0, 3, 94, 0, 32, 7, 7, 54, 73, 94, 3,
15, 15, 28, 119, 9, 0, 0, 5, 3, 7, 18, 1, 15],
[5, 12, 96, 32, 57, 1, 6, 11, 6, 3, 14, 23, 2, 6, 22, 6, 14, 56, 5,
2, 41, 45, 225, 0, 211, 1, 1, 130, 2, 1, 4, 9],
[185, 24, 13, 59, 94, 30, 1, 26, 19, 42, 1, 55, 143, 1, 124, 61,
189, 0, 220, 0, 68, 199, 59, 3, 3, 50, 109, 28, 77, 128, 146, 0],
[1, 8, 6, 6, 6, 98, 5, 3, 169, 126, 1, 15, 6, 77, 1, 30, 3, 3, 30,
18, 3, 5, 5, 139, 22, 11, 42, 0, 19, 26, 71, 109],
[7, 15, 37, 0, 239, 47, 243, 5, 0, 92, 21, 1, 36, 28, 12, 16, 5,
151, 1, 6, 251, 1, 2, 114, 10, 5, 13, 1, 1, 214, 5, 2],
[242, 1, 5, 92, 27, 3, 1, 1, 3, 12, 97, 209, 0, 17, 88, 1, 134, 48,
7, 1, 101, 1, 24, 166, 17, 0, 6, 6, 0, 5, 1, 4],
[6, 227, 12, 89, 214, 48, 0, 164, 235, 5, 1, 10, 5, 12, 24, 23, 73,
1, 3, 53, 5, 96, 2, 26, 1, 54, 56, 14, 23, 0, 0, 43],
[1, 193, 5, 28, 26, 5, 41, 7, 97, 6, 7, 6, 167, 62, 0, 5, 0, 8,
109, 19, 4, 38, 8, 31, 3, 59, 64, 0, 3, 114, 34, 81]]
(108693264, 424)
{x = 15, y = 27}
0
28200025
0x1ff287ab
[0x7643183ef3572797, 0x761e5bad7e0d1e3a, 0x52b23ee35d4ff10b,
0xb2a146e17d6b1652, 0x1f114b663c2d71d8, ...]
[[0x6c, 0x56, 0xeb, 0x21, 0x81, 0x0c, 0xa2, 0x67, 0x62, 0x93, 0x88,
0x37, 0xe4, 0x06, 0xaa, 0x01, 0x71, 0x17, 0x7e, 0x6d, 0x81, 0x1a,
0x49, 0xae, 0x4b, 0x68, 0x73, 0xeb, 0x80, 0xbc, 0xcf, 0x00],
[0x35, 0x67, 0x45, 0xdc, 0x63, 0x10, 0x08, 0xde, 0x84, 0x16, 0xee,
0x56, 0xc7, 0x53, 0x10, 0x2d, 0x8e, 0x4e, 0xac, 0x24, 0x92, 0x3b,
0x73, 0xe0, 0xf8, 0x0e, 0x51, 0x0e, 0x78, 0x68, 0x03, 0x2e],
[0x2a, 0xfc, 0x06, 0x6f, 0xeb, 0x50, 0x81, 0x86, 0x86, 0x85, 0x10,
0x9e, 0x3e, 0x6a, 0x7c, 0x0d, 0xc8, 0x1a, 0x8c, 0x02, 0xfc, 0xc6,
0xd7, 0x58, 0x74, 0xdd, 0x53, 0x3a, 0xd9, 0xe6, 0x40, 0x4f],
[0xf8, 0xf8, 0xf6, 0x4b, 0xfb, 0xa2, 0x6f, 0x5a, 0x7c, 0x62, 0xb8,
0xd6, 0xd3, 0x28, 0xe1, 0xfa, 0x3a, 0xee, 0x2f, 0x8d, 0xd0, 0xe1,
0x2c, 0x4a, 0x6f, 0x27, 0x01, 0x1e, 0x64, 0xcb, 0xcd, 0xf5],
[0x2d, 0x23, 0x8a, 0x62, 0x73, 0xc8, 0x44, 0x71, 0xda, 0x13, 0x51,
0x2e, 0x66, 0x3d, 0xb0, 0x7c, 0xb4, 0x36, 0xdc, 0x35, 0x3b, 0xed,
0x9d, 0xbc, 0x8f, 0x1e, 0x67, 0x2a, 0xab, 0x01, 0xdf, 0x6c],
[0xee, 0xf2, 0xa8, 0x8b, 0xc6, 0x1a, 0x06, 0xfd, 0x6f, 0x68, 0x08,
0x83, 0xa4, 0x12, 0x0d, 0xa9, 0xf8, 0xd7, 0xa6, 0x10, 0x90, 0x15,
0xe3, 0xf5, 0x5c, 0x28, 0xa8, 0x9d, 0xf3, 0xba, 0xc2, 0x3d],
[0xf6, 0xa0, 0x8a, 0x88, 0x9b, 0xb6, 0x37, 0xb4, 0xee, 0x85, 0x67,
0xd9, 0xf9, 0x1f, 0x79, 0xfd, 0x8c, 0xe2, 0xaa, 0x86, 0x5e, 0x19,
0x55, 0x37, 0x92, 0xb9, 0x50, 0xb7, 0xb9, 0x9c, 0xff, 0xf6],
[0x87, 0x68, 0x8c, 0xb1, 0x5d, 0xc1, 0x3b, 0x5a, 0x35, 0xa0, 0x1d,
0x99, 0x85, 0xde, 0x52, 0xf7, 0x9a, 0x84, 0x98, 0xcb, 0x4e, 0x3b,
0x6d, 0xe4, 0x9c, 0x52, 0xf3, 0xa8, 0x50, 0x80, 0x24, 0x3b],
[0x80, 0xfb, 0x6f, 0x24, 0x37, 0xfc, 0xe3, 0x26, 0x2d, 0xbc, 0x94,
0xe7, 0xc2, 0xbd, 0x2e, 0x6b, 0xe2, 0x10, 0xff, 0x8f, 0xc0, 0x11,
0x98, 0x63, 0x0c, 0x3d, 0x19, 0x18, 0x41, 0x4d, 0x32, 0x3c],
[0x54, 0xc3, 0x3e, 0x5b, 0x43, 0x28, 0x53, 0xea, 0x73, 0x3c, 0x42,
0xe7, 0x21, 0x49, 0x84, 0x66, 0x14, 0x15, 0xe5, 0xce, 0xdf, 0xf3,
0x4a, 0x9f, 0xc5, 0xab, 0x0a, 0x35, 0x1a, 0xa6, 0x42, 0xf4],
[0x54, 0xcd, 0x25, 0xbb, 0xea, 0x6b, 0xc1, 0x58, 0xd7, 0x50, 0xa1,
0x07, 0x2c, 0xf2, 0xb7, 0xa8, 0x62, 0x99, 0xf0, 0xb1, 0x67, 0x5c,
0x05, 0x79, 0x09, 0xec, 0x5c, 0xed, 0xdc, 0x5e, 0x66, 0x9d],
[0x97, 0x45, 0x94, 0x13, 0xb7, 0xb3, 0xd3, 0x39, 0x6b, 0x15, 0x29,
0xd4, 0x53, 0xd5, 0x7e, 0x06, 0x8c, 0xe5, 0x52, 0xb0, 0x66, 0xce,
0x11, 0x33, 0x20, 0x86, 0x96, 0xd3, 0xa0, 0x2a, 0x7b, 0x68],
[0x49, 0x98, 0xf2, 0x34, 0xd0, 0xfc, 0x02, 0x9f, 0xb0, 0xfc, 0x56,
0xbe, 0xb6, 0x4c, 0xbe, 0x39, 0x31, 0x3b, 0x16, 0xd9, 0x7d, 0x90,
0xa7, 0x15, 0x90, 0x08, 0xb2, 0x19, 0x78, 0xe7, 0xb2, 0x90],
[0xd5, 0x88, 0x6f, 0xf7, 0x3f, 0x05, 0x69, 0x6a, 0x1e, 0x32, 0x9f,
0xe2, 0xab, 0x92, 0x30, 0x98, 0xd7, 0xa4, 0x61, 0x12, 0x90, 0xdd,
0x08, 0xfb, 0xe8, 0x73, 0x7a, 0x73, 0xeb, 0xc6, 0x46, 0x17],
[0x05, 0x40, 0x47, 0x17, 0x18, 0xe9, 0xd8, 0xf8, 0x31, 0x38, 0x24,
0x9a, 0x70, 0x57, 0x6a, 0x47, 0xdf, 0x8d, 0xbb, 0x95, 0x26, 0xf6,
0xc3, 0x1f, 0x22, 0xe0, 0xb3, 0xbe, 0xd6, 0x59, 0xe3, 0x53],
[0xf6, 0xf6, 0x6e, 0x4d, 0x7f, 0xdc, 0x5f, 0xdd, 0x60, 0x22, 0x3b,
0x21, 0xb5, 0x41, 0xfb, 0xbc, 0x6e, 0x7e, 0x67, 0xa2, 0xe5, 0xc5,
0xc3, 0x1c, 0x65, 0x61, 0x33, 0x2b, 0xd1, 0x9d, 0x3e, 0x8a]]
(0x1ff287ab, 0x79f0)
{x = 0x1c43a24d, y = 0x2785}
0x00000000
0x56058f47

2
tests/issues/issue184.icry.stdout
View File

@ -1,4 +1,4 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
[1, 2, 3, 4, 255, 0, 1, 2, 3, 4]
[0x01, 0x02, 0x03, 0x04, 0xff, 0x00, 0x01, 0x02, 0x03, 0x04]

2
tests/issues/issue289.icry.stdout
View File

@ -2,5 +2,5 @@ Loading module Cryptol
Loading module Cryptol
Loading module Main
Q.E.D.
av1 3701879183 3218045100 = False
av1 0xc00001c9 0xbfffffd5 = False
Q.E.D.

6
tests/issues/issue290.icry.stdout
View File

@ -3,6 +3,6 @@ Loading module Cryptol
Loading module issue290
Loading module issue290bar
Assuming a = 2
2
1
1
0x2
0x1
0x1

2
tests/issues/transpose0.icry.stdout
View File

@ -1,2 +1,2 @@
Loading module Cryptol
[0, 0, 0, 0, 0, 0, 0, 0]
[0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0]

2
tests/regression/check01.icry.stdout
View File

@ -6,5 +6,5 @@ Loading module Main
of expression (@@)
at check01.cry:2:17--2:19
to 5
[7, 20]
[0x00000007, 0x00000014]
True

2
tests/regression/check02.icry.stdout
View File

@ -12,5 +12,5 @@ Loading module Main
at <interactive>:1:6--1:8
to 4
Assuming a = 1
[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[0x1, 0x1, 0x1, 0x1, 0x1, 0x1, 0x1, 0x1, 0x1, 0x1, 0x1]
True

8
tests/regression/check03.icry.stdout
View File

@ -6,11 +6,15 @@ Loading module Main
of expression (@@)
at <interactive>:1:8--1:10
to 4
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
[0x00000000, 0x00000001, 0x00000002, 0x00000003, 0x00000004,
0x00000005, 0x00000006, 0x00000007, 0x00000008, 0x00000009,
0x0000000a]
[warning] at <interactive>:1:1--1:23:
Defaulting 4th type parameter
of expression (@@)
at <interactive>:1:9--1:11
to 4
[11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21]
[0x0000000b, 0x0000000c, 0x0000000d, 0x0000000e, 0x0000000f,
0x00000010, 0x00000011, 0x00000012, 0x00000013, 0x00000014,
0x00000015]
True

2
tests/regression/check04.icry.stdout
View File

@ -17,5 +17,5 @@ Loading module Main
at <interactive>:1:9--1:11
to 4
Assuming a = 2
[1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1]
[0x1, 0x2, 0x1, 0x2, 0x1, 0x2, 0x1, 0x2, 0x1, 0x2, 0x1]
True

2
tests/regression/check05.icry.stdout
View File

@ -17,5 +17,5 @@ Loading module Main
at <interactive>:1:9--1:11
to 4
Assuming a = 2
[2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2]
[0x2, 0x1, 0x2, 0x1, 0x2, 0x1, 0x2, 0x1, 0x2, 0x1, 0x2]
True

5
tests/regression/check06.icry.stdout
View File

@ -17,6 +17,7 @@ Loading module Main
at <interactive>:1:12--1:14
to 4
Assuming a = 2
[[1, 2], [2, 1], [1, 2], [2, 1], [1, 2], [2, 1], [1, 2], [2, 1],
[1, 2], [2, 1], [1, 2]]
[[0x1, 0x2], [0x2, 0x1], [0x1, 0x2], [0x2, 0x1], [0x1, 0x2],
[0x2, 0x1], [0x1, 0x2], [0x2, 0x1], [0x1, 0x2], [0x2, 0x1],
[0x1, 0x2]]
True

2
tests/regression/check08.icry.stdout
View File

@ -16,6 +16,6 @@ Loading module Main
of expression (@@)
at <interactive>:1:4--1:6
to 3
[1, 2, 5, 12, 27]
[0x00000001, 0x00000002, 0x00000005, 0x0000000c, 0x0000001b]
True
Q.E.D.

4
tests/regression/check10.icry.stdout
View File

@ -1,8 +1,8 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
0
0
0x00
0x00
True
True
True

3
tests/regression/check12.icry.stdout
View File

@ -1,5 +1,6 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
[0, 1, 3, 6, 10, 15, 21, 28, 36, 45]
[0x00000000, 0x00000001, 0x00000003, 0x00000006, 0x0000000a,
0x0000000f, 0x00000015, 0x0000001c, 0x00000024, 0x0000002d]
True

2
tests/regression/check14.icry.stdout
View File

@ -7,5 +7,5 @@ Loading module Main
at check14.cry:5:41--5:42
to 3
Assuming a = 3
[[3, 2, 1, 0], [7, 6, 5, 4]]
[[0x3, 0x2, 0x1, 0x0], [0x7, 0x6, 0x5, 0x4]]
True

2
tests/regression/check26.cry
View File

@ -1,7 +1,7 @@
fst (x, y) = x
snd (x, y) = y
xy = (13, 21)
check26a = (fst xy == xy.1) && (snd xy == xy.2) &&
check26a = (fst xy == xy.0) && (snd xy == xy.1) &&
(fst xy == 13) && (snd xy == 21)
xys = [ (x, y) | x <- [ 1 .. 10 ], y <- [ 2 .. 5 ] ]

5
tests/regression/layout01.icry Normal file
View File

@ -0,0 +1,5 @@
(x where x = 1)
[x where x = 1, x where x = 2]
{ x = x where x = 1, y = y where y = 2 }
x where (x,y) = (1,2)
x where { x = x, y = y } = { x = 10, y = 20 }

42
tests/regression/layout01.icry.stdout Normal file
View File

@ -0,0 +1,42 @@
Loading module Cryptol
Assuming a = 1
0x1
Assuming a = 2
[0x1, 0x2]
Assuming a = 1
Assuming b = 2
{x = 0x1, y = 0x2}
[warning] at <interactive>:1:1--1:22:
Defaulting 2nd type parameter
of expression __p0
at <interactive>:1:10--1:11
to 2
[warning] at <interactive>:1:1--1:22:
Defaulting 1st type parameter
of expression __p0
at <interactive>:1:12--1:13
to 1
[warning] at <interactive>:1:1--1:22:
Defaulting 2nd type parameter
of expression __p0
at <interactive>:1:12--1:13
to 2
Assuming a = 1
0x1
[warning] at <interactive>:1:1--1:46:
Defaulting 2nd type parameter
of expression __p0
at <interactive>:1:15--1:16
to 5
[warning] at <interactive>:1:1--1:46:
Defaulting 1st type parameter
of expression __p0
at <interactive>:1:22--1:23
to 4
[warning] at <interactive>:1:1--1:46:
Defaulting 2nd type parameter
of expression __p0
at <interactive>:1:22--1:23
to 5
Assuming a = 4
0xa

2
tests/regression/r02.icry.stdout
View File

@ -1,6 +1,6 @@
Loading module Cryptol
Assuming a = 4
[11, 11, 11, 11, 11, 11, 11, 11, 11, 11]
[0xb, 0xb, 0xb, 0xb, 0xb, 0xb, 0xb, 0xb, 0xb, 0xb]
[warning] at <interactive>:1:1--1:68:
Defaulting type parameter 'bits'
of finite enumeration

4
tests/regression/r03.icry.stdout
View File

@ -1,5 +1,5 @@
Loading module Cryptol
Loading module Cryptol
Loading module r03
(nQueens : Solution 5) [4, 2, 0, 3, 1] = True
(nQueensProve : Solution 4) [2, 0, 3, 1] = False
(nQueens : Solution 5) [0x4, 0x2, 0x0, 0x3, 0x1] = True
(nQueensProve : Solution 4) [0x2, 0x0, 0x3, 0x1] = False