GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-25 08:54:31 +03:00
Code Issues Projects Releases Wiki Activity

Remove all uses of [x..] syntax from examples and tests.

Browse Source
This commit is contained in:
Brian Huffman 2019-02-27 16:25:53 -08:00
parent 00b58277bb
commit c387dbe5fd
6 changed files with 11 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
examples/SIV-rfc5297.md
View File

@ -554,14 +554,14 @@ ctr32 : {n} (2^^39 - 128 >= n) => Key -> [128] -> [n] -> [n]
ctr32 k iv pt = pt ^ take stream ctr32 k iv pt = pt ^ take stream
where where
stream = join [E(k,v) | v <- ivs] stream = join [E(k,v) | v <- ivs]
ivs = [take `{96} iv # cnt + i | i <- [0,1..]] ivs = [take `{96} iv # cnt + i | i <- [0 ...]]
cnt = drop `{back=32} iv cnt = drop `{back=32} iv
ctr64 : {n} (2^^71 - 128 >= n) => Key -> [128] -> [n] -> [n] ctr64 : {n} (2^^71 - 128 >= n) => Key -> [128] -> [n] -> [n]
ctr64 k iv pt = pt ^ take stream ctr64 k iv pt = pt ^ take stream
where where
stream = join [E(k,v) | v <- ivs] stream = join [E(k,v) | v <- ivs]
ivs = [take `{64} iv # cnt + i | i <- [0,1..]] ivs = [take `{64} iv # cnt + i | i <- [0 ...]]
cnt = drop `{back=64} iv cnt = drop `{back=64} iv
``` ```

2
examples/funstuff/FoxChickenCorn.cry
View File

@ -91,7 +91,7 @@ ppArray = [farmerString, chickenString, cornString, foxString]
ppBits : [4] -> [4]StringRep ppBits : [4] -> [4]StringRep
ppBits s = [ if b then ppArray!i else noString ppBits s = [ if b then ppArray!i else noString
| b <- s | b <- s
| i <- [0 .. ]:[_][4] ] | i <- [0 ...]:[_][4] ]
// takes a sequence of states and derives what moved, and in which direction for each transition // takes a sequence of states and derives what moved, and in which direction for each transition
extractMoves : {a} [a+1]BankState -> [a](DirRep, [4]StringRep) extractMoves : {a} [a+1]BankState -> [a](DirRep, [4]StringRep)

8
examples/param_modules/AES/Round.cry
View File

@ -12,11 +12,11 @@ SubBytes : State -> State
SubBytes state = [ [ SubByte b | b <- row ] | row <- state ] SubBytes state = [ [ SubByte b | b <- row ] | row <- state ]
ShiftRows : State -> State ShiftRows : State -> State
ShiftRows state = [ row <<< i | row <- state | i : [2] <- [0 .. ] ] ShiftRows state = [ row <<< i | row <- state | i : [2] <- [0 .. 3] ]
MixColumns : State -> State MixColumns : State -> State
MixColumns state = gf28MatrixMult m state MixColumns state = gf28MatrixMult m state
where m = [ [2,3,1,1] >>> i | i <- [ 0 .. ] ] where m = [ [2,3,1,1] >>> i | i <- [0 .. 3] ]
/** The final AES round */ /** The final AES round */
AESFinalRound : RoundKey -> State -> State AESFinalRound : RoundKey -> State -> State
@ -33,12 +33,12 @@ InvSubBytes state = [ [ InvSubByte b | b <- row ] | row <- state ]
InvShiftRows : State -> State InvShiftRows : State -> State
InvShiftRows state = [ row >>> shiftAmount | row <- state InvShiftRows state = [ row >>> shiftAmount | row <- state
| shiftAmount : [2] <- [0 ..] | shiftAmount : [2] <- [0 .. 3]
] ]
InvMixColumns : State -> State InvMixColumns : State -> State
InvMixColumns state = gf28MatrixMult m state InvMixColumns state = gf28MatrixMult m state
where m = [[0x0e, 0x0b, 0x0d, 0x09] >>> i | i <- [ 0 .. ] ] where m = [[0x0e, 0x0b, 0x0d, 0x09] >>> i | i <- [0 .. 3] ]
/** The final inverted AES round */ /** The final inverted AES round */
AESFinalInvRound : RoundKey -> State -> State AESFinalInvRound : RoundKey -> State -> State

5
examples/param_modules/AES/SBox.cry
View File

@ -6,8 +6,7 @@ import AES::SubBytePlain
type SBox = [256] GF28 type SBox = [256] GF28
sbox : SBox sbox : SBox
sbox = [ SubByte x | x <- [ 0 .. ] ] sbox = [ SubByte x | x <- [0 .. 255] ]
sboxInv : SBox sboxInv : SBox
sboxInv = [ InvSubByte x | x <- [ 0 .. ] ] sboxInv = [ InvSubByte x | x <- [0 .. 255] ]

2
examples/param_modules/AES/TBox.cry
View File

@ -31,7 +31,7 @@ tboxInv : TBox
tboxInv = mkTBox [ 0x0e, 0x09, 0x0d, 0x0b ] sboxInv tboxInv = mkTBox [ 0x0e, 0x09, 0x0d, 0x0b ] sboxInv
mkTBox : [4]GF28 -> SBox -> TBox mkTBox : [4]GF28 -> SBox -> TBox
mkTBox seed box = [ [ a >>> i | a <- t0 ] | i <- [ 0 .. ] ] mkTBox seed box = [ [ a >>> i | a <- t0 ] | i <- [0 .. 3] ]
where where
t0 = [ [ gf28Mult c s | c <- seed ] | s <- box ] t0 = [ [ gf28Mult c s | c <- seed ] | s <- box ]

2
tests/regression/check11.cry
View File

@ -1,5 +1,5 @@
check11 = zz == ww check11 = zz == ww
where where
zz = [0 .. 99] zz = [0 .. 99]
qq = zz @@ ([0 ..] : [_][32]) qq = zz @@ ([0 .. 0xffffffff] : [_][32])
ww = qq @@ [0 .. 99] ww = qq @@ [0 .. 99]