From 1322156d28b7ab4466f05570e492bd6dbaf95c9c Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Fri, 19 Feb 2016 10:08:20 -0800 Subject: [PATCH] Remove trailing whitespace --- bench/data/AES.cry | 4 +- cryptol-server/Cryptol/Aeson.hs | 2 +- docs/ProgrammingCryptol/aes/AES.cry | 4 +- examples/ChaChaPolyCryptolIETF.md | 114 +++++++++--------- examples/DES.cry | 5 +- examples/MiniLock/prim/Base64.cry | 2 +- examples/MiniLock/prim/Blake2s.cry | 3 +- examples/MiniLock/prim/Poly1305.md | 18 +-- examples/MiniLock/prim/mod_arith.cry | 2 +- examples/SHA1.cry | 6 +- examples/SIV-rfc5297.md | 4 +- examples/TripleDES.cry | 2 +- examples/contrib/A51.cry | 14 +-- examples/contrib/bivium.cry | 9 +- examples/contrib/trivium.cry | 7 +- examples/funstuff/NQueens.cry | 3 +- examples/funstuff/marble.cry | 7 +- examples/maliciousSHA/malicious_SHA1.cry | 15 ++- lib/Cryptol.cry | 2 +- src/Cryptol/ModuleSystem/Monad.hs | 4 +- src/Cryptol/ModuleSystem/NamingEnv.hs | 2 +- src/Cryptol/Parser/Lexer.x | 5 +- src/Cryptol/Prims/Eval.hs | 2 +- src/Cryptol/REPL/Monad.hs | 5 +- src/Cryptol/TypeCheck/Infer.hs | 2 +- src/Cryptol/TypeCheck/InferTypes.hs | 3 +- src/Cryptol/TypeCheck/Sanity.hs | 4 +- src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs | 4 +- .../TypeCheck/Solver/Numeric/ImportExport.hs | 3 +- .../TypeCheck/Solver/Numeric/Interval.hs | 7 +- .../TypeCheck/Solver/Numeric/NonLin.hs | 12 +- src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs | 4 +- .../TypeCheck/Solver/Numeric/Simplify.hs | 5 +- .../TypeCheck/Solver/Numeric/Simplify1.hs | 10 +- .../TypeCheck/Solver/Numeric/SimplifyExpr.hs | 7 +- tests/issues/issue187.cry | 2 +- tests/issues/issue212.cry | 4 +- tests/issues/issue225.cry | 3 +- tests/issues/issue289.cry | 2 +- tests/issues/simon.cry2 | 4 +- tests/parser/nested-where.cry | 2 +- tests/parser/pat1.cry | 2 +- tests/regression/AES.cry | 4 +- tests/regression/check09.cry | 4 +- tests/regression/check23.cry | 2 +- 45 files changed, 143 insertions(+), 188 deletions(-) diff --git a/bench/data/AES.cry b/bench/data/AES.cry index 665d82af..3b95fc87 100644 --- a/bench/data/AES.cry +++ b/bench/data/AES.cry @@ -32,7 +32,7 @@ type AESKeySize = (Nk*32) type GF28 = [8] type State = [4][Nb]GF28 type RoundKey = State -type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey) +type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey) // GF28 operations gf28Add : {n} (fin n) => [n]GF28 -> GF28 gf28Add ps = sums ! 0 @@ -196,7 +196,7 @@ aesDecrypt : ([128], [AESKeySize]) -> [128] aesDecrypt (ct, key) = stateToMsg (AESFinalInvRound (kFinal, rounds ! 0)) where (kFinal, ks, kInit) = ExpandKey key state0 = AddRoundKey(kInit, msgToState ct) - rounds = [state0] # [ AESInvRound (rk, s) + rounds = [state0] # [ AESInvRound (rk, s) | rk <- reverse ks | s <- rounds ] diff --git a/cryptol-server/Cryptol/Aeson.hs b/cryptol-server/Cryptol/Aeson.hs index 90b05b27..97c6f084 100644 --- a/cryptol-server/Cryptol/Aeson.hs +++ b/cryptol-server/Cryptol/Aeson.hs @@ -5,7 +5,7 @@ -- Maintainer : cryptol@galois.com -- Stability : provisional -- Portability : portable --- +-- -- Orphan 'FromJSON' and 'ToJSON' instances for certain Cryptol -- types. Since these are meant to be consumed over a wire, they are -- mostly focused on base values and interfaces rather than a full diff --git a/docs/ProgrammingCryptol/aes/AES.cry b/docs/ProgrammingCryptol/aes/AES.cry index f71e6505..c266c9b3 100644 --- a/docs/ProgrammingCryptol/aes/AES.cry +++ b/docs/ProgrammingCryptol/aes/AES.cry @@ -32,7 +32,7 @@ type AESKeySize = (Nk*32) type GF28 = [8] type State = [4][Nb]GF28 type RoundKey = State -type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey) +type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey) // GF28 operations gf28Add : {n} (fin n) => [n]GF28 -> GF28 gf28Add ps = sums ! 0 @@ -196,7 +196,7 @@ aesDecrypt : ([128], [AESKeySize]) -> [128] aesDecrypt (ct, key) = stateToMsg (AESFinalInvRound (kFinal, rounds ! 0)) where (kFinal, ks, kInit) = ExpandKey key state0 = AddRoundKey(kInit, msgToState ct) - rounds = [state0] # [ AESInvRound (rk, s) + rounds = [state0] # [ AESInvRound (rk, s) | rk <- reverse ks | s <- rounds ] diff --git a/examples/ChaChaPolyCryptolIETF.md b/examples/ChaChaPolyCryptolIETF.md index f3eda726..6357b17f 100755 --- a/examples/ChaChaPolyCryptolIETF.md +++ b/examples/ChaChaPolyCryptolIETF.md @@ -1,4 +1,4 @@ -% ChaCha20 and Poly1305 for IETF protocols +% ChaCha20 and Poly1305 for IETF protocols % Y. Nir (Check Point), A. Langley (Google Inc), D. McNamee (Galois, Inc) % July 28, 2014 @@ -178,7 +178,7 @@ leaving the others alone: ``` Note that this run of quarter round is part of what is called a -"column round". +"column round". ### Test Vector for the Quarter Round on the ChaCha state @@ -208,8 +208,8 @@ After applying QUARTERROUND(2,7,8,13) Note that only the numbers in positions 2, 7, 8, and 13 changed. -In the Cryptol implementation of ChaCha20, the ChaChaQuarterround is called on four elements at a time, -and there is no destructive state modification, so it would be artificial to reproduce the +In the Cryptol implementation of ChaCha20, the ChaChaQuarterround is called on four elements at a time, +and there is no destructive state modification, so it would be artificial to reproduce the above example of the partially-destructively modified matrix. Instead, we show the output of calling ChaChaQuarterround on the diagonal elements identified above: @@ -726,7 +726,7 @@ Next, divide the message into 16-byte blocks. The last block might be shorter: * Add the current block to the accumulator. * Multiply by "r" - * Set the accumulator to the result modulo p. To summarize: + * Set the accumulator to the result modulo p. To summarize: ``accum[i+1] = ((accum[i]+block)*r) % p``. ```cryptol @@ -773,7 +773,7 @@ using AES, and assume that we got the following keying material: 03:80:8a:fb:0d:b2:fd:4a:bf:f6:af:41:49:f5:1b ```cryptol -Poly1305TestKey = join (parseHexString +Poly1305TestKey = join (parseHexString ( "85:d6:be:78:57:55:6d:33:7f:44:52:fe:42:d5:06:a8:01:" # "03:80:8a:fb:0d:b2:fd:4a:bf:f6:af:41:49:f5:1b." ) ) @@ -808,7 +808,7 @@ values of the accumulator: ```cryptol // TODO: refactor the Poly function in terms of this AccumBlocks // challenge: doing so while maintaining the clean literate correspondence with the spec -AccumBlocks : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16) +AccumBlocks : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16) => [256] -> [m][8] -> ([_][136], [136]) AccumBlocks key msg = (accum, lastAccum) where @@ -864,7 +864,7 @@ Acc + block = 2d8adaf23b0337fa7cccfb4ea344ca153 ``` ```cryptol -property polyBlocksOK = +property polyBlocksOK = (blocks @ 1 == 0x02c88c77849d64ae9147ddeb88e69c83fc) && (blocks @ 2 == 0x02d8adaf23b0337fa7cccfb4ea344b30de) && (lastBlock == 0x028d31b7caff946c77c8844335369d03a7) where @@ -876,7 +876,7 @@ Adding s we get this number, and serialize if to get the tag: Acc + s = 2a927010caf8b2bc2c6365130c11d06a8 Tag: a8:06:1d:c1:30:51:36:c6:c2:2b:8b:af:0c:01:27:a9 - + ```cryptol // Putting it all together and testing: @@ -904,7 +904,7 @@ SK_a* or *_write_MAC_key is only for stand-alone Poly1305. The method is to call the block function with the following parameters: - + * The 256-bit session integrity key is used as the ChaCha20 key. * The block counter is set to zero. * The protocol will specify a 96-bit or 64-bit nonce. This MUST be @@ -929,7 +929,7 @@ encryption algorithms (often called Initialization Vectors, or IVs), they usually don't have such a provision for the MAC function. In that case the per-invocation nonce will have to come from somewhere else, such as a message counter. - + ### Poly1305 Key Generation Test Vector For this example, we'll set: @@ -966,7 +966,7 @@ PolyChaChaState_testVector = [ 0x37b633a8, 0xa50dfde3, 0xe2b8db08, 0x46a6d1fd, 0x7da03782, 0x9183a233, 0x148ad271, 0xb46773d1, 0x3cc1875a, 0x8607def1, 0xca5c3086, 0x7085eb87 ] - + property PolyChaCha_correct = ChaCha20Block PolyKeyTest PolyNonceTest 0 == PolyChaChaState_testVector ``` @@ -978,7 +978,7 @@ PolyOutput = join (parseHexString ( "8a d5 a0 8b 90 5f 81 cc 81 50 40 27 4a b2 94 71 " # "a8 33 b6 37 e3 fd 0d a5 08 db b8 e2 fd d1 a6 46 ")) -GeneratePolyKeyUsingChaCha k n i = join [littleendian (groupBy`{8}b) +GeneratePolyKeyUsingChaCha k n i = join [littleendian (groupBy`{8}b) | b <- take `{8}(ChaCha20Block k n i) ] property Poly_passes_test = GeneratePolyKeyUsingChaCha PolyKeyTest PolyNonceTest 0 == PolyOutput @@ -1048,7 +1048,7 @@ takes a 256-bit key and 96-bit nonce as follows: counter set to 1. ```cryptol - ct = ChaCha20EncryptBytes p k nonce 1 + ct = ChaCha20EncryptBytes p k nonce 1 ``` * Finally, the Poly1305 function is called with the Poly1305 key @@ -1071,12 +1071,12 @@ takes a 256-bit key and 96-bit nonce as follows: ```cryptol ptlen : [8][8] - ptlen = groupBy`{8}(littleendian (groupBy`{8}(`m:[64]))) + ptlen = groupBy`{8}(littleendian (groupBy`{8}(`m:[64]))) adlen : [8][8] adlen = groupBy`{8}(littleendian (groupBy`{8}(`n:[64]))) // compute padding tag = Poly1305 PolyKey (AeadConstruction aad ct) - + //ct in this function has tag removed AeadConstruction (AAD : [n][8]) (CT : [m][8]) = (AAD # padding1 # CT # padding2 # adlen # ptlen) where padding1 = (zero:[(16-n%16)%16][8]) @@ -1100,7 +1100,7 @@ AEAD_CHACHA20_POLY1305_DECRYPT : {m, n} (fin m, fin n ,64 >= width m, 64 >= width n) => [256] -> [96] -> [m+16][8] -> [n][8] - -> ([m][8], Bit) + -> ([m][8], Bit) AEAD_CHACHA20_POLY1305_DECRYPT k nonce ct ad = (pt, valid) where inTag = drop`{m}ct inCt = take`{m}ct @@ -1185,7 +1185,7 @@ AeadPolyOneTimeKey_testVector = [ 0x93929190, 0x97969594, 0x9b9a9998, 0x9f9e9d9c, 0x00000000, 0x00000007, 0x43424140, 0x47464544 ] -property AeadPolyKeyBuildState_correct = +property AeadPolyKeyBuildState_correct = BuildState AeadKey AeadNonce 0 == AeadPolyOneTimeKey_testVector ``` @@ -1198,7 +1198,7 @@ AeadPolyOneTimeKeyState = [ 0xdecc7ea2, 0xb44ddbad, 0xe49c17d1, 0xd8430bc9, 0x8c94b7bc, 0x8b7d4b4b, 0x3927f67d, 0x1669a432] -property AeadPolyChaCha_correct = +property AeadPolyChaCha_correct = ChaCha20Block AeadKey AeadNonce 0 == AeadPolyOneTimeKeyState ``` @@ -1262,7 +1262,7 @@ AeadTagTestVector = parseHexString "1a:e1:0b:59:4f:09:e2:6a:7e:90:2e:cb:d0:60:06 ``` ```cryptol -property AeadTag_correct = AeadTag == AeadTagTestVector +property AeadTag_correct = AeadTag == AeadTagTestVector property AeadConstruction_correct = (AeadConstruction AeadAAD AeadCT) == AeadConstructionTestVector @@ -1458,12 +1458,12 @@ Email: dylan@galois.com ```cryptol // helper macros for higher-up properties TV_block_correct key nonce blockcounter result = ChaCha20Block key nonce blockcounter == result - + TV_block_Keystream_correct key nonce blockcounter keystream = take`{0x40} (groupBy`{8} (join (join (ChaCha20ExpandKey key nonce blockcounter)))) == keystream -ChaCha20_block_correct key nonce blockcounter result keystream = - TV_block_correct key nonce blockcounter result && +ChaCha20_block_correct key nonce blockcounter result keystream = + TV_block_correct key nonce blockcounter result && TV_block_Keystream_correct key nonce blockcounter keystream ``` @@ -1489,7 +1489,7 @@ TV1_block_KeyStream = [ property TV1_block_correct = ChaCha20_block_correct TV1_block_Key TV1_block_Nonce TV1_block_BlockCounter TV1_block_After20 TV1_block_KeyStream ``` - + ### Test Vector #2 ```cryptol @@ -1511,7 +1511,7 @@ TV2_block_KeyStream = [ property TV2_block_correct = ChaCha20_block_correct TV2_block_Key TV2_block_Nonce TV2_block_BlockCounter TV2_block_After20 TV2_block_KeyStream - + ``` ### Test Vector #3 @@ -1526,11 +1526,11 @@ TV3_block_After20 = [ 0xe8252083, 0x60818b01, 0xf38422b8, 0x5aaa49c9, 0xbb00ca8e, 0xda3ba7b4, 0xc4b592d1, 0xfdf2732f, 0x4436274e, 0x2561b3c8, 0xebdd4aa6, 0xa0136c00] - + TV3_block_KeyStream = [ - 0x3a, 0xeb, 0x52, 0x24, 0xec, 0xf8, 0x49, 0x92, 0x9b, 0x9d, 0x82, 0x8d, 0xb1, 0xce, 0xd4, 0xdd, - 0x83, 0x20, 0x25, 0xe8, 0x01, 0x8b, 0x81, 0x60, 0xb8, 0x22, 0x84, 0xf3, 0xc9, 0x49, 0xaa, 0x5a, - 0x8e, 0xca, 0x00, 0xbb, 0xb4, 0xa7, 0x3b, 0xda, 0xd1, 0x92, 0xb5, 0xc4, 0x2f, 0x73, 0xf2, 0xfd, + 0x3a, 0xeb, 0x52, 0x24, 0xec, 0xf8, 0x49, 0x92, 0x9b, 0x9d, 0x82, 0x8d, 0xb1, 0xce, 0xd4, 0xdd, + 0x83, 0x20, 0x25, 0xe8, 0x01, 0x8b, 0x81, 0x60, 0xb8, 0x22, 0x84, 0xf3, 0xc9, 0x49, 0xaa, 0x5a, + 0x8e, 0xca, 0x00, 0xbb, 0xb4, 0xa7, 0x3b, 0xda, 0xd1, 0x92, 0xb5, 0xc4, 0x2f, 0x73, 0xf2, 0xfd, 0x4e, 0x27, 0x36, 0x44, 0xc8, 0xb3, 0x61, 0x25, 0xa6, 0x4a, 0xdd, 0xeb, 0x00, 0x6c, 0x13, 0xa0] property TV3_block_correct = ChaCha20_block_correct TV3_block_Key TV3_block_Nonce TV3_block_BlockCounter TV3_block_After20 TV3_block_KeyStream @@ -1549,11 +1549,11 @@ TV4_block_After20 = [ 0xa78dea8f, 0x5e269039, 0xa1bebbc1, 0xcaf09aae, 0xa25ab213, 0x48a6b46c, 0x1b9d9bcb, 0x092c5be6, 0x546ca624, 0x1bec45d5, 0x87f47473, 0x96f0992e] - + TV4_block_KeyStream = [ - 0x72, 0xd5, 0x4d, 0xfb, 0xf1, 0x2e, 0xc4, 0x4b, 0x36, 0x26, 0x92, 0xdf, 0x94, 0x13, 0x7f, 0x32, - 0x8f, 0xea, 0x8d, 0xa7, 0x39, 0x90, 0x26, 0x5e, 0xc1, 0xbb, 0xbe, 0xa1, 0xae, 0x9a, 0xf0, 0xca, - 0x13, 0xb2, 0x5a, 0xa2, 0x6c, 0xb4, 0xa6, 0x48, 0xcb, 0x9b, 0x9d, 0x1b, 0xe6, 0x5b, 0x2c, 0x09, + 0x72, 0xd5, 0x4d, 0xfb, 0xf1, 0x2e, 0xc4, 0x4b, 0x36, 0x26, 0x92, 0xdf, 0x94, 0x13, 0x7f, 0x32, + 0x8f, 0xea, 0x8d, 0xa7, 0x39, 0x90, 0x26, 0x5e, 0xc1, 0xbb, 0xbe, 0xa1, 0xae, 0x9a, 0xf0, 0xca, + 0x13, 0xb2, 0x5a, 0xa2, 0x6c, 0xb4, 0xa6, 0x48, 0xcb, 0x9b, 0x9d, 0x1b, 0xe6, 0x5b, 0x2c, 0x09, 0x24, 0xa6, 0x6c, 0x54, 0xd5, 0x45, 0xec, 0x1b, 0x73, 0x74, 0xf4, 0x87, 0x2e, 0x99, 0xf0, 0x96] property TV4_block_correct = ChaCha20_block_correct TV4_block_Key TV4_block_Nonce TV4_block_BlockCounter TV4_block_After20 TV4_block_KeyStream @@ -1572,7 +1572,7 @@ TV5_block_After20 = [ 0x88228b1a, 0x96a4dfb3, 0x5b76ab72, 0xc727ee54, 0x0e0e978a, 0xf3145c95, 0x1b748ea8, 0xf786c297, 0x99c28f5f, 0x628314e8, 0x398a19fa, 0x6ded1b53] - + TV5_block_KeyStream = [ 0xc2, 0xc6, 0x4d, 0x37, 0x8c, 0xd5, 0x36, 0x37, 0x4a, 0xe2, 0x04, 0xb9, 0xef, 0x93, 0x3f, 0xcd, 0x1a, 0x8b, 0x22, 0x88, 0xb3, 0xdf, 0xa4, 0x96, 0x72, 0xab, 0x76, 0x5b, 0x54, 0xee, 0x27, 0xc7, @@ -1586,8 +1586,8 @@ property all_block_tests_correct = TV2_block_correct && TV3_block_correct && TV4_block_correct && - TV5_block_correct - + TV5_block_correct + ``` ## ChaCha20 Encryption @@ -1610,7 +1610,7 @@ TV1_enc_cyphertext = [ 0xbd, 0xd2, 0x19, 0xb8, 0xa0, 0x8d, 0xed, 0x1a, 0xa8, 0x36, 0xef, 0xcc, 0x8b, 0x77, 0x0d, 0xc7, 0xda, 0x41, 0x59, 0x7c, 0x51, 0x57, 0x48, 0x8d, 0x77, 0x24, 0xe0, 0x3f, 0xb8, 0xd8, 0x4a, 0x37, 0x6a, 0x43, 0xb8, 0xf4, 0x15, 0x18, 0xa1, 0x1c, 0xc3, 0x87, 0xb6, 0x69, 0xb2, 0xee, 0x65, 0x86] - + property TV1_enc_correct = ChaCha20_enc_correct TV1_enc_Key TV1_enc_Nonce TV1_enc_BlockCounter TV1_enc_plaintext TV1_enc_cyphertext ``` @@ -1647,7 +1647,7 @@ IETF_submission_text = [ 0x79, 0x20, 0x74, 0x69, 0x6d, 0x65, 0x20, 0x6f, 0x72, 0x20, 0x70, 0x6c, 0x61, 0x63, 0x65, 0x2c, 0x20, 0x77, 0x68, 0x69, 0x63, 0x68, 0x20, 0x61, 0x72, 0x65, 0x20, 0x61, 0x64, 0x64, 0x72, 0x65, 0x73, 0x73, 0x65, 0x64, 0x20, 0x74, 0x6f ] - + TV2_enc_plaintext = IETF_submission_text @@ -1676,7 +1676,7 @@ TV2_enc_cyphertext = [ 0x14, 0xea, 0x99, 0x82, 0xcc, 0xaf, 0xb3, 0x41, 0xb2, 0x38, 0x4d, 0xd9, 0x02, 0xf3, 0xd1, 0xab, 0x7a, 0xc6, 0x1d, 0xd2, 0x9c, 0x6f, 0x21, 0xba, 0x5b, 0x86, 0x2f, 0x37, 0x30, 0xe3, 0x7c, 0xfd, 0xc4, 0xfd, 0x80, 0x6c, 0x22, 0xf2, 0x21] - + property TV2_enc_correct = ChaCha20_enc_correct TV2_enc_Key TV2_enc_Nonce TV2_enc_BlockCounter TV2_enc_plaintext TV2_enc_cyphertext ``` @@ -1699,7 +1699,7 @@ jabberwock_text = [ 0x65, 0x72, 0x65, 0x20, 0x74, 0x68, 0x65, 0x20, 0x62, 0x6f, 0x72, 0x6f, 0x67, 0x6f, 0x76, 0x65, 0x73, 0x2c, 0x0a, 0x41, 0x6e, 0x64, 0x20, 0x74, 0x68, 0x65, 0x20, 0x6d, 0x6f, 0x6d, 0x65, 0x20, 0x72, 0x61, 0x74, 0x68, 0x73, 0x20, 0x6f, 0x75, 0x74, 0x67, 0x72, 0x61, 0x62, 0x65, 0x2e] - + TV3_enc_plaintext = jabberwock_text @@ -1712,13 +1712,13 @@ TV3_enc_cyphertext = [ 0x1a, 0x55, 0x32, 0x05, 0x57, 0x16, 0xea, 0xd6, 0x96, 0x25, 0x68, 0xf8, 0x7d, 0x3f, 0x3f, 0x77, 0x04, 0xc6, 0xa8, 0xd1, 0xbc, 0xd1, 0xbf, 0x4d, 0x50, 0xd6, 0x15, 0x4b, 0x6d, 0xa7, 0x31, 0xb1, 0x87, 0xb5, 0x8d, 0xfd, 0x72, 0x8a, 0xfa, 0x36, 0x75, 0x7a, 0x79, 0x7a, 0xc1, 0x88, 0xd1] - + property TV3_enc_correct = ChaCha20_enc_correct TV3_enc_Key TV3_enc_Nonce TV3_enc_BlockCounter TV3_enc_plaintext TV3_enc_cyphertext property all_enc_tests_correct = TV1_enc_correct && TV2_enc_correct && - TV3_enc_correct + TV3_enc_correct ``` ## Poly1305 Message Authentication Code @@ -1857,7 +1857,7 @@ exactly 2^130-6? TV9_MAC_Key = 0x02 # zero:[256] -TV9_MAC_text = +TV9_MAC_text = [0xFD, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF] TV9_MAC_tag = [0xFA, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF]: [16][8] @@ -1898,7 +1898,7 @@ TV11_MAC_text = [ 0xE3, 0x35, 0x94, 0xD7, 0x50, 0x5E, 0x43, 0xB9, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x33, 0x94, 0xD7, 0x50, 0x5E, 0x43, 0x79, 0xCD, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] - + TV11_MAC_tag = split(0x13 # 0): [16][8] property TV11_MAC_correct = poly1305_MAC_correct TV11_MAC_Key TV11_MAC_text TV11_MAC_tag @@ -1914,7 +1914,7 @@ property all_MAC_tests_correct = TV8_MAC_correct && TV9_MAC_correct && TV10_MAC_correct && - TV11_MAC_correct + TV11_MAC_correct ``` @@ -1967,7 +1967,7 @@ property TV3_key_correct = Poly1305_key_correct TV3_key_Key TV3_key_Nonce TV3_ke property all_key_tests_correct = TV1_key_correct && TV2_key_correct && - TV3_key_correct + TV3_key_correct ``` ## ChaCha20-Poly1305 AEAD Decryption @@ -2004,7 +2004,7 @@ TV1_AEAD_known_otk = join([ //sent TV1_AEAD_tag = [0xee, 0xad, 0x9d, 0x67, 0x89, 0x0c, 0xbb, 0x22, 0x39, 0x23, 0x36, 0xfe, 0xa1, 0x85, 0x1f, 0x38] - + TV1_AEAD_cypherText = [ 0x64, 0xa0, 0x86, 0x15, 0x75, 0x86, 0x1a, 0xf4, 0x60, 0xf0, 0x62, 0xc7, 0x9b, 0xe6, 0x43, 0xbd, 0x5e, 0x80, 0x5c, 0xfd, 0x34, 0x5c, 0xf3, 0x89, 0xf1, 0x08, 0x67, 0x0a, 0xc7, 0x6c, 0x8c, 0xb2, @@ -2049,7 +2049,7 @@ TV1_AEAD_Poly_input = [ First, we calculate the one-time Poly1305 key ```cryptol - + //generate and check the one time key (leaving out the given states from the document, they will be correct if this is correct) property TV1_otk_correct = Poly1305_key_correct TV1_AEAD_key TV1_AEAD_nonce TV1_AEAD_known_otk @@ -2069,7 +2069,7 @@ We calculate the Poly1305 tag and find that it matches ```cryptol property TV1_tag_correct = poly1305_MAC_correct TV1_AEAD_known_otk (AeadConstruction TV1_AEAD_AAD TV1_AEAD_cypherText) TV1_AEAD_tag ``` - + ```cryptol TV1_plaintext = [ 0x49, 0x6e, 0x74, 0x65, 0x72, 0x6e, 0x65, 0x74, 0x2d, 0x44, 0x72, 0x61, 0x66, 0x74, 0x73, 0x20, @@ -2089,14 +2089,14 @@ TV1_plaintext = [ 0x6d, 0x20, 0x6f, 0x74, 0x68, 0x65, 0x72, 0x20, 0x74, 0x68, 0x61, 0x6e, 0x20, 0x61, 0x73, 0x20, 0x2f, 0xe2, 0x80, 0x9c, 0x77, 0x6f, 0x72, 0x6b, 0x20, 0x69, 0x6e, 0x20, 0x70, 0x72, 0x6f, 0x67, 0x72, 0x65, 0x73, 0x73, 0x2e, 0x2f, 0xe2, 0x80, 0x9d] - + TV1_calculate_plaintext = AEAD_CHACHA20_POLY1305_DECRYPT TV1_AEAD_key TV1_AEAD_nonce (TV1_AEAD_cypherText # TV1_AEAD_tag) TV1_AEAD_AAD - + property TV1_plaintext_correct = isValid && pt == TV1_plaintext where (pt,isValid) = TV1_calculate_plaintext - -property decryption_vector_correct = + +property decryption_vector_correct = TV1_plaintext_correct && TV1_tag_correct && TV1_otk_correct @@ -2146,7 +2146,7 @@ property parseHexString_check = "14:15:16:17:18:19:1a:1b:1c:1d:1e:1f.")) == 0x000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f -property AllPropertiesPass = +property AllPropertiesPass = ChaChaQuarterround_passes_test && ChaChaQuarterround_passes_column_test && FirstRow_correct && @@ -2182,7 +2182,7 @@ by loading it into a Cryptol interpreter, and running the AllPropertiesPass function, like this: ```example -$ cryptol ChaChaPolyCryptolIETF.md +$ cryptol ChaChaPolyCryptolIETF.md _ _ ___ _ __ _ _ _ __ | |_ ___ | | / __| '__| | | | '_ \| __/ _ \| | @@ -2193,10 +2193,8 @@ $ cryptol ChaChaPolyCryptolIETF.md Loading module Cryptol Loading module ChaCha20 ... a bunch of warnings about the use of ambiguous-width constants -ChaCha20> AllPropertiesPass +ChaCha20> AllPropertiesPass True ``` This check verifies the implementation of `ChaCha`, `Poly1305` and the `AEAD` construction all work with the provided test vectors. - - diff --git a/examples/DES.cry b/examples/DES.cry index 905ddf07..c2061b0c 100644 --- a/examples/DES.cry +++ b/examples/DES.cry @@ -9,12 +9,12 @@ import Cipher // DES API DES : Cipher 64 64 -DES = +DES = { encrypt key pt = des pt (expandKey key) , decrypt key ct = des ct (reverse (expandKey key)) } -// Encryption +// Encryption des pt keys = (swap (split last)) @@ FPz where @@ -169,4 +169,3 @@ sbox8 = [[13, 2, 8, 4, 6, 15, 11, 1, 10, 9, 3, 14, 5, 0, 12, 7], [7, 11, 4, 1, 9, 12, 14, 2, 0, 6, 10, 13, 15, 3, 5, 8], [2, 1, 14, 7, 4, 10, 8, 13, 15, 12, 9, 0, 3, 5, 6, 11] ] - diff --git a/examples/MiniLock/prim/Base64.cry b/examples/MiniLock/prim/Base64.cry index 6f29478a..a825da25 100644 --- a/examples/MiniLock/prim/Base64.cry +++ b/examples/MiniLock/prim/Base64.cry @@ -6,7 +6,7 @@ module Base64 where import Cryptol::Extras -type Enc64 n = 4*(((3-(n%3))%3) + n)/3 +type Enc64 n = 4*(((3-(n%3))%3) + n)/3 base64enc : {n,m,padZ} (4*(padZ + n)/3 == m, fin n, fin m, padZ == (3-(n%3))%3, 2>=padZ) => [n][8] -> [Enc64 n][8] diff --git a/examples/MiniLock/prim/Blake2s.cry b/examples/MiniLock/prim/Blake2s.cry index 30c710a1..b3724a4d 100644 --- a/examples/MiniLock/prim/Blake2s.cry +++ b/examples/MiniLock/prim/Blake2s.cry @@ -162,7 +162,7 @@ updateVector orig idxNew = vs vs = [if i == idx then new else orig@i | i <- [0..a-1]] -property katsPass = ~zero == +property katsPass = ~zero == [ nthKat `{0} , nthKat `{1} , nthKat `{2} @@ -685,4 +685,3 @@ kats = [ 0x69217a3079908094e11121d042354a7c1f55b6482ca1a51e1b250dfd1ed0eef9 , 0xc08aa1c286d709fdc7473744977188c895ba011014247e4efa8d07e78fec695c , 0xf03f5789d3336b80d002d59fdf918bdb775b00956ed5528e86aa994acb38fe2d ] - diff --git a/examples/MiniLock/prim/Poly1305.md b/examples/MiniLock/prim/Poly1305.md index 1a0176dd..069f62df 100644 --- a/examples/MiniLock/prim/Poly1305.md +++ b/examples/MiniLock/prim/Poly1305.md @@ -1,4 +1,4 @@ -% Poly1305 for IETF protocols +% Poly1305 for IETF protocols % Y. Nir (Check Point), A. Langley (Google Inc), D. McNamee (Galois, Inc) % July 28, 2014 % @@ -70,7 +70,7 @@ The inputs to Poly1305 are: The output is a 128-bit tag. ```cryptol -Poly1305 : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16) +Poly1305 : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16) => [256] -> [m][8] -> [16][8] ``` @@ -114,7 +114,7 @@ Next, divide the message into 16-byte blocks. The last block might be shorter: * Add the current block to the accumulator. * Multiply by "r" - * Set the accumulator to the result modulo p. To summarize: + * Set the accumulator to the result modulo p. To summarize: ``accum[i+1] = ((accum[i]+block)*r) % p``. ```cryptol @@ -161,7 +161,7 @@ using AES, and assume that we got the following keying material: 03:80:8a:fb:0d:b2:fd:4a:bf:f6:af:41:49:f5:1b ```cryptol -Poly1305TestKey = join (parseHexString +Poly1305TestKey = join (parseHexString ( "85:d6:be:78:57:55:6d:33:7f:44:52:fe:42:d5:06:a8:01:" # "03:80:8a:fb:0d:b2:fd:4a:bf:f6:af:41:49:f5:1b." ) ) @@ -196,7 +196,7 @@ values of the accumulator: ```cryptol // TODO: refactor the Poly function in terms of this AccumBlocks // challenge: doing so while maintaining the clean literate correspondence with the spec -AccumBlocks : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16) +AccumBlocks : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16) => [256] -> [m][8] -> ([_][136], [136]) AccumBlocks key msg = (accum, lastAccum) where @@ -252,7 +252,7 @@ Acc + block = 2d8adaf23b0337fa7cccfb4ea344ca153 ``` ```cryptol -property polyBlocksOK = +property polyBlocksOK = (blocks @ 1 == 0x02c88c77849d64ae9147ddeb88e69c83fc) && (blocks @ 2 == 0x02d8adaf23b0337fa7cccfb4ea344b30de) && (lastBlock == 0x028d31b7caff946c77c8844335369d03a7) where @@ -264,7 +264,7 @@ Adding s we get this number, and serialize if to get the tag: Acc + s = 2a927010caf8b2bc2c6365130c11d06a8 Tag: a8:06:1d:c1:30:51:36:c6:c2:2b:8b:af:0c:01:27:a9 - + ```cryptol // Putting it all together and testing: @@ -292,7 +292,7 @@ SK_a* or *_write_MAC_key is only for stand-alone Poly1305. The method is to call the block function with the following parameters: - + * The 256-bit session integrity key is used as the ChaCha20 key. * The block counter is set to zero. * The protocol will specify a 96-bit or 64-bit nonce. This MUST be @@ -317,7 +317,7 @@ encryption algorithms (often called Initialization Vectors, or IVs), they usually don't have such a provision for the MAC function. In that case the per-invocation nonce will have to come from somewhere else, such as a message counter. - + ### Poly1305 Key Generation Test Vector For this example, we'll set: diff --git a/examples/MiniLock/prim/mod_arith.cry b/examples/MiniLock/prim/mod_arith.cry index fd2173ac..2604af47 100644 --- a/examples/MiniLock/prim/mod_arith.cry +++ b/examples/MiniLock/prim/mod_arith.cry @@ -45,7 +45,7 @@ mod_div(p,x,y) = egcd(p,0,y,x) egcd(a, ra, b >> 1, mod_half(p, rb)) else if a < b then egcd(a, ra, (b - a) >> 1, mod_half(p, mod_sub(p, rb, ra))) - else + else egcd(b, rb, (a - b) >> 1, mod_half(p, mod_sub(p, ra, rb))) mod_pow : {a} (fin a, a >= 1) => ([a] , [a] , [a]) -> [a] diff --git a/examples/SHA1.cry b/examples/SHA1.cry index 9e10f578..19e05f9f 100644 --- a/examples/SHA1.cry +++ b/examples/SHA1.cry @@ -12,7 +12,7 @@ sha1 msg = sha1' pmsg sha1' : {chunks} (fin chunks) => [chunks][512] -> [160] sha1' pmsg = join (Hs!0) - where + where Hs = [[0x67452301, 0xefcdab89, 0x98badcfe, 0x10325476, 0xc3d2e1f0]] # [ block(H, split(M)) | H <- Hs @@ -38,7 +38,7 @@ pad msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64])) type padding = (512 - contentLen % 512) % 512 // prettier if type #'s could be < 0 f : ([8], [32], [32], [32]) -> [32] -f (t, x, y, z) = +f (t, x, y, z) = if (0 <= t) && (t <= 19) then (x && y) ^ (~x && z) | (20 <= t) && (t <= 39) then x ^ y ^ z | (40 <= t) && (t <= 59) then (x && y) ^ (x && z) ^ (y && z) @@ -54,7 +54,7 @@ Ks = [ 0x5a827999 | t <- [0..19] ] block : ([5][32], [16][32]) -> [5][32] block ([H0, H1, H2, H3, H4], M) = [(H0+As@80), (H1+Bs@80), (H2+Cs@80), (H3+Ds@80), (H4+Es@80)] - where + where Ws : [80][32] Ws = M # [ (W3 ^ W8 ^ W14 ^ W16) <<< 1 | W16 <- drop`{16 - 16} Ws diff --git a/examples/SIV-rfc5297.md b/examples/SIV-rfc5297.md index ab0471f6..3add90ec 100644 --- a/examples/SIV-rfc5297.md +++ b/examples/SIV-rfc5297.md @@ -321,7 +321,7 @@ E(K,X) = aesEncrypt (X,K) // 8. Return T. aesCMAC : {m} (fin m) => Key -> [m] -> [128] -aesCMAC K m = +aesCMAC K m = cmacBlocks K ((`m%128) == 0 && `m > 0) (split `{each=128,parts=blocks} full) where pd = [True] # zero : [128] @@ -501,7 +501,7 @@ S2V K S1 S2 = res else aesCMAC K (dbl D1 ^ pad S2) private - // The length of 'p' is >= 128, but Cryptol lacks + // The length of 'p' is >= 128, but Cryptol lacks // dependent types and can not infer this fact. We // Provide a no-op computation that results in a // new type for 'p' that is at least 128 bits diff --git a/examples/TripleDES.cry b/examples/TripleDES.cry index 5d745ee7..80e169bf 100644 --- a/examples/TripleDES.cry +++ b/examples/TripleDES.cry @@ -8,7 +8,7 @@ module TripleDES where import DES blockEncrypt : ([64],[64],[64],[64]) -> [64] -blockEncrypt (k1,k2,k3,data) = result where +blockEncrypt (k1,k2,k3,data) = result where ex = DES.encrypt k1 data dx = DES.decrypt k2 ex result = DES.encrypt k3 dx diff --git a/examples/contrib/A51.cry b/examples/contrib/A51.cry index 8008889f..072f15ca 100644 --- a/examples/contrib/A51.cry +++ b/examples/contrib/A51.cry @@ -11,13 +11,13 @@ A51_stream R1 R2 R3 = R1s ^ R2s ^ R3s (R2s, R2f) = lfsrki <| x^^22 + x^^21 + 1 |> R2c R2 (R3s, R3f) = lfsrki <| x^^23 + x^^22 + x^^21 + x^^8 + 1 |> R3c R3 majvs = [ majv (r1@8) (r2@10) (r3@10) | r1 <- R1f | r2 <- R2f | r3 <- R3f ] - R1c = [ r1@8 == m | r1 <- R1f | m <- majvs ] + R1c = [ r1@8 == m | r1 <- R1f | m <- majvs ] R2c = [ r2@10 == m | r2 <- R2f | m <- majvs ] - R3c = [ r3@10 == m | r3 <- R3f | m <- majvs ] + R3c = [ r3@10 == m | r3 <- R3f | m <- majvs ] type N = 128 A51 : ([19], [22], [23]) -> [N]Bit -A51(reg1, reg2, reg3) = keystream +A51(reg1, reg2, reg3) = keystream where keystream = take`{N} (A51_stream reg1 reg2 reg3) @@ -38,14 +38,14 @@ lfsrki poly conds init = (stream, fills) prefix f xs = ys!0 where ys = [xs@0] # [ f y x | y <- ys | x <- tail xs ] - + majv a b c = (a && b) || (a && c) || (b && c) /***********************************************************************/ -iv1 = 0b1010111011101011101 -iv2 = 0b1010111011101010101110 -iv3 = 0b10100000111100110011011 +iv1 = 0b1010111011101011101 +iv2 = 0b1010111011101010101110 +iv3 = 0b10100000111100110011011 test_keystream = 0b00100100111010001110101110101100010100110111110101000101110000011101000111110101010000010011001111110101110001011010100000010001 diff --git a/examples/contrib/bivium.cry b/examples/contrib/bivium.cry index dac47621..b1c1d28e 100644 --- a/examples/contrib/bivium.cry +++ b/examples/contrib/bivium.cry @@ -7,11 +7,11 @@ Russian Academy of Sciences Bivium_stream : [93] -> [84] -> [inf] Bivium_stream R1 R2 = stream where - (stream, ra, rb) = shift_regs R1 R2 + (stream, ra, rb) = shift_regs R1 R2 type N = 200 Bivium : ([93], [84]) -> [N]Bit -Bivium (reg1, reg2) = keystream +Bivium (reg1, reg2) = keystream where keystream = take`{N} (Bivium_stream reg1 reg2) @@ -29,10 +29,10 @@ shift_regs r1 r2 = (stream, regA, regB) s2 = [(f2 @ 68) ^ (f2 @ 83) | f2 <- regB] stream = s1 ^ s2 - t1 = [(f1 @ 65) ^ ((f1 @ 90) && (f1 @ 91)) ^ (f1 @ 92) ^ (f2 @ 77) | + t1 = [(f1 @ 65) ^ ((f1 @ 90) && (f1 @ 91)) ^ (f1 @ 92) ^ (f2 @ 77) | f2 <- regB | f1 <- regA ] - t2 = [(f2 @ 68) ^ ((f2 @ 81) && (f2 @ 82)) ^ (f2 @ 83) ^ (f1 @ 68) | + t2 = [(f2 @ 68) ^ ((f2 @ 81) && (f2 @ 82)) ^ (f2 @ 83) ^ (f1 @ 68) | f1 <- regA | f2 <- regB ] @@ -51,4 +51,3 @@ suffix = 0b000000001000000000000000000001 property Bivium_correct = (Bivium(iv1, iv2)) == test_keystream property Bivium_search (x, y) = (Bivium(x, y)) == test_keystream property Bivium_search_with_suffix (x, y) = (Bivium(x, y#suffix)) == test_keystream - diff --git a/examples/contrib/trivium.cry b/examples/contrib/trivium.cry index b19bc4fd..6637f033 100644 --- a/examples/contrib/trivium.cry +++ b/examples/contrib/trivium.cry @@ -24,16 +24,16 @@ shift fill bit = fills shift_regs : {d,e,f} (fin d, fin e, fin f, d >=1, e >=1, f>=1) => [d] -> [e] -> [f] -> ([inf],[inf][d],[inf][e],[inf][f]) shift_regs r1 r2 r3 = (stream, regA, regB, regC) where - + s1 = [(f1 @ 65) ^ (f1 @ 92) | f1 <- regA] s2 = [(f2 @ 68) ^ (f2 @ 83) | f2 <- regB] s3 = [(f3 @ 65) ^ (f3 @ 110) | f3 <- regC] stream = s1 ^ s2 ^ s3 - t1 = [(f1 @ 65) ^ ((f1 @ 90) && (f1 @ 91)) ^ (f1 @ 92) ^ (f2 @ 77) | + t1 = [(f1 @ 65) ^ ((f1 @ 90) && (f1 @ 91)) ^ (f1 @ 92) ^ (f2 @ 77) | f2 <- regB | f1 <- regA ] - t2 = [(f2 @ 68) ^ ((f2 @ 81) && (f2 @ 82)) ^ (f2 @ 83) ^ (f3 @ 86) | + t2 = [(f2 @ 68) ^ ((f2 @ 81) && (f2 @ 82)) ^ (f2 @ 83) ^ (f3 @ 86) | f2 <- regB | f3 <- regC ] t3 = [(f3 @ 65) ^ ((f3 @ 108) && (f3 @ 109)) ^ (f3 @ 110) ^ (f1 @ 68)| @@ -54,4 +54,3 @@ test_keystream = 0b0111111101111011111101000011100000000000001000100000000000000 property Trivium_correct = (Trivium(iv1, iv2, iv3)) == test_keystream property Trivium_search (x, y, z) = (Trivium(x, y, z)) == test_keystream - diff --git a/examples/funstuff/NQueens.cry b/examples/funstuff/NQueens.cry index 6cd24a1a..e1716699 100644 --- a/examples/funstuff/NQueens.cry +++ b/examples/funstuff/NQueens.cry @@ -9,7 +9,7 @@ where n is the board-size You may find that cvc4 takes a long time for solutions bigger than 5. - For those sizes, we have had good luck with both Yices and Z3. + For those sizes, we have had good luck with both Yices and Z3. To do that, @@ -54,4 +54,3 @@ inRange : {n} (fin n, n >= 1) => Board n -> Position n -> Bit inRange qs x = x <= `(n - 1) property nQueensProve x = (nQueens x) == False - diff --git a/examples/funstuff/marble.cry b/examples/funstuff/marble.cry index d5f5ece8..c3eef58a 100644 --- a/examples/funstuff/marble.cry +++ b/examples/funstuff/marble.cry @@ -66,8 +66,8 @@ validBoard : Board -> Bit validBoard b = join (b && ~posns) == zero validRowJump : Board -> Board -> Bit -validRowJump a a' = validBoard a - && validBoard a' +validRowJump a a' = validBoard a + && validBoard a' && validRowMove (differentRow a a') differentRow : Board -> Board -> ([7], [7]) @@ -83,7 +83,7 @@ validRowMove (r, r') = (xors == 0b0000111 || xors == 0b0001110 || xors == 0b0011100 || xors == 0b0111000 || - xors == 0b1110000) + xors == 0b1110000) && ( rxors == 0b0000011 || rxors == 0b0000110 || @@ -105,4 +105,3 @@ validMoveSequence moves = all [validMove a b | a <- moves | b <- drop`{1} moves] solutionInNmoves : {n} (fin n) => [n] Board -> Bit property solutionInNmoves ms = validMoveSequence ([start] # ms # [second]) - diff --git a/examples/maliciousSHA/malicious_SHA1.cry b/examples/maliciousSHA/malicious_SHA1.cry index faf122eb..b3c75ef9 100755 --- a/examples/maliciousSHA/malicious_SHA1.cry +++ b/examples/maliciousSHA/malicious_SHA1.cry @@ -24,7 +24,7 @@ malicious_sha1 msg k = malicious_sha1' rmsg k malicious_sha1' : {chunks} (fin chunks) => [chunks][512] -> [4][32] -> [160] malicious_sha1' pmsg k = join (Hs!0) - where + where Hs = [[0x67452301, 0xefcdab89, 0x98badcfe, 0x10325476, 0xc3d2e1f0]] # [ malicious_block (H, split(M)) k | H <- Hs @@ -53,7 +53,7 @@ eve1 = [ //hexdump of file available at http://malicioussha1.github.io/pocs/eve2.sh //when executed will print "hello world" -//The ascii cow and hello world can be switched out in both files +//The ascii cow and hello world can be switched out in both files //and the hashes will still collide. The next example shows this eve2 = [ 0x1d23, 0x921b, 0x4014, 0xac09, 0x4d98, 0xd3a6, 0xe1bc, 0x4910, @@ -94,7 +94,7 @@ eve1_galois = [ 0x6365, 0x6f68, 0x2220, 0x6147, 0x6f6c, 0x7369, 0x3b22, 0x660a, 0x0a69] -//hexdump malicious/eve1.sh +//hexdump malicious/eve1.sh eve2_galois = [ 0x1d23, 0x921b, 0x4014, 0xac09, 0x4d98, 0xd3a6, 0xe1bc, 0x4910, 0x8570, 0x1812, 0x786f, 0xb926, 0x37bd, 0xac2b, 0x50ae, 0x6a08, @@ -135,15 +135,15 @@ pad : {msgLen,contentLen,chunks,padding} pad msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64])) f : ([8], [32], [32], [32]) -> [32] -f (t, x, y, z) = +f (t, x, y, z) = if (0 <= t) && (t <= 19) then (x && y) ^ (~x && z) | (20 <= t) && (t <= 39) then x ^ y ^ z | (40 <= t) && (t <= 59) then (x && y) ^ (x && z) ^ (y && z) | (60 <= t) && (t <= 79) then x ^ y ^ z else error "f: t out of range" - -Ks : [4][32] -> [80][32] + +Ks : [4][32] -> [80][32] Ks k = [ k@0 | t <- [0..19] ] # [ k@1 | t <- [20..39] ] # [ k@2 | t <- [40..59] ] @@ -152,7 +152,7 @@ Ks k = [ k@0 | t <- [0..19] ] malicious_block : ([5][32], [16][32]) -> [4][32]-> [5][32] malicious_block ([H0, H1, H2, H3, H4], M) k = [(H0+As@80), (H1+Bs@80), (H2+Cs@80), (H3+Ds@80), (H4+Es@80)] - where + where Ws : [80][32] Ws = M # [ (W3 ^ W8 ^ W14 ^ W16) <<< 1 | W16 <- drop`{16 - 16} Ws @@ -172,4 +172,3 @@ malicious_block ([H0, H1, H2, H3, H4], M) k = | W <- Ws | K <- (Ks k) | t <- [0..79] ] - diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index e6f407b3..e756bef3 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -67,7 +67,7 @@ primitive (^^) : {a} (Arith a) => a -> a -> a /** * Log base two. - * + * * For words, computes the ceiling of log, base 2, of a number. * Over structured values, operates element-wise. */ diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index dcb62c1c..4ce60496 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -280,7 +280,7 @@ runModuleT :: Monad m => ModuleEnv -> ModuleT m a -> m (Either ModuleError (a, ModuleEnv), [ModuleWarning]) -runModuleT env m = +runModuleT env m = runWriterT $ runExceptionT $ runStateT env @@ -444,5 +444,3 @@ getSolverConfig :: ModuleM T.SolverConfig getSolverConfig = ModuleT $ do me <- get return (meSolverConfig me) - - diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index 86684ea5..ef4837ec 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -243,7 +243,7 @@ instance BindsNames ImportIface where namingEnv (ImportIface imp Iface { .. }) = return (interpImport imp ifPublic) --- | Introduce the name +-- | Introduce the name instance BindsNames (InModule (Bind PName)) where namingEnv (InModule ns b) = do let Located { .. } = bName b diff --git a/src/Cryptol/Parser/Lexer.x b/src/Cryptol/Parser/Lexer.x index 6a5722cd..b9df04e9 100644 --- a/src/Cryptol/Parser/Lexer.x +++ b/src/Cryptol/Parser/Lexer.x @@ -6,7 +6,7 @@ -- Maintainer : cryptol@galois.com -- Stability : provisional -- Portability : portable --- +-- -- At present Alex generates code with too many warnings. {-# LANGUAGE Trustworthy #-} {-# LANGUAGE OverloadedStrings #-} @@ -246,6 +246,3 @@ primLexer cfg cs = run inp Normal -- vim: ft=haskell } - - - diff --git a/src/Cryptol/Prims/Eval.hs b/src/Cryptol/Prims/Eval.hs index 1648ae83..8c77fb86 100644 --- a/src/Cryptol/Prims/Eval.hs +++ b/src/Cryptol/Prims/Eval.hs @@ -192,7 +192,7 @@ divModPoly xs xsLen ys ysLen todoBits = map (testBit xs) (downIxes (xsLen - degree)) --- | Create a packed word +-- | Create a packed word modExp :: Integer -- ^ bit size of the resulting word -> Integer -- ^ base -> Integer -- ^ exponent diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index ebe8a567..50945926 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -343,7 +343,7 @@ getPutStr = fmap ePutStr getRW rPutStr :: String -> REPL () rPutStr str = do rw <- getRW - io $ ePutStr rw str + io $ ePutStr rw str -- | Use the configured output action to print a string with a trailing newline rPutStrLn :: String -> REPL () @@ -730,6 +730,3 @@ z3exists = do case mPath of Nothing -> return (Just Z3NotFound) Just _ -> return Nothing - - - diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index b5ca5825..687d063c 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -569,7 +569,7 @@ inferBinds :: Bool -> Bool -> [P.Bind Name] -> InferM [Decl] inferBinds isTopLevel isRec binds = mdo let dExpr (DExpr e) = e dExpr DPrim = panic "[TypeCheck]" [ "primitive in a recursive group" ] - + exprMap = Map.fromList [ (x,inst (EVar x) (dExpr (dDefinition b))) | b <- genBs, let x = dName b ] -- REC. diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs index 2d579f9e..1ce1b9f7 100644 --- a/src/Cryptol/TypeCheck/InferTypes.hs +++ b/src/Cryptol/TypeCheck/InferTypes.hs @@ -486,7 +486,7 @@ instance PP (WithNames Error) where AmbiguousType xs -> text "The inferred type for" <+> commaSep (map pp xs) - <+> text "is ambiguous." + <+> text "is ambiguous." where nested x y = x $$ nest 2 y @@ -564,4 +564,3 @@ instance PP Solved where where suDoc = maybe empty pp mb Unsolved -> text "unsolved" Unsolvable -> text "unsolvable" - diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs index 40dbb755..3e0993e7 100644 --- a/src/Cryptol/TypeCheck/Sanity.hs +++ b/src/Cryptol/TypeCheck/Sanity.hs @@ -326,7 +326,7 @@ convertible t1 t2 convertible t1 t2 = go t1 t2 where go ty1 ty2 = - let err = reportError $ TypeMismatch (tMono ty1) (tMono ty2) + let err = reportError $ TypeMismatch (tMono ty1) (tMono ty2) other = tNoUser ty2 goMany [] [] = return () @@ -533,5 +533,3 @@ lookupVar x = case Map.lookup x (roVars ro) of Just s -> return s Nothing -> reportError $ UndefinedVariable x - - diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs index 5492cf77..3db84537 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs @@ -5,7 +5,7 @@ -- Maintainer : cryptol@galois.com -- Stability : provisional -- Portability : portable --- +-- -- Simplification of `fin` constraints. {-# LANGUAGE PatternGuards #-} @@ -89,5 +89,3 @@ cryIsFinType varInfo g ty = where solved ps = Solved Nothing [ g { goal = p } | p <- ps ] - - diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs b/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs index 230a1169..3fb86cb1 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs @@ -125,7 +125,7 @@ importProp prop = _ :>= _ -> Nothing a :> b -> Just (b :>= a) _ :==: _ -> Nothing - a :>: b -> Just (b :>= a) + a :>: b -> Just (b :>= a) -- XXX: Do we need to add Fin on `a` and 'b'? @@ -168,4 +168,3 @@ importType = go t2 <- go y t3 <- go z return (app f [t1,t2,t3]) - diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs index f7be0da8..30016880 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs @@ -5,7 +5,7 @@ -- Maintainer : cryptol@galois.com -- Stability : provisional -- Portability : portable --- +-- -- An interval interpretation of types. {-# LANGUAGE PatternGuards #-} @@ -337,8 +337,3 @@ iLenFromThenTo i j k | Just x <- iIsExact i, Just y <- iIsExact j, Just z <- iIsExact k , Just r <- nLenFromThenTo x y z = iConst r | otherwise = iAnyFin - - - - - diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs b/src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs index 5e399240..7fa4c351 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs @@ -5,12 +5,12 @@ -- Maintainer : cryptol@galois.com -- Stability : provisional -- Portability : portable --- +-- -- Separate Non-Linear Constraints -- When we spot a non-linear expression, we name it and add it to a map. --- +-- -- If we see the same expression multiple times, then we give it the same name. --- +-- -- The body of the non-linear expression is not processed further, -- so the resulting map should not contain any of the newly minted names. @@ -78,7 +78,7 @@ lookupNL x NonLinS { .. } = Map.lookup x nonLinExprs runNL :: NonLinS -> NonLinM a -> ((a, [Prop]), NonLinS) runNL s m = runId - $ runStateT s + $ runStateT s $ do a <- m ps <- finishTodos return (a,ps) @@ -279,7 +279,3 @@ finishTodos = p' <- nonLinPropM p ps' <- finishTodos return (p' : ps') - - - - diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs b/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs index 99be2f37..e273ef08 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs @@ -173,7 +173,7 @@ smtName a = case a of name p n = case divMod n 26 of (q,r) -> p ++ toEnum (fromEnum 'a' + r) : (if q == 0 then "" else show q) - + -- | The name of a boolean variable, representing `fin x`. smtFinName :: Name -> String @@ -515,5 +515,3 @@ linRel (x1,y1) (x2,y2) = let b = y1 - a * x1 guard $ not $ a < 0 && b < 0 -- No way this will give a natural number. return (a,b) - - diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs index f9d054fe..1ceca925 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs @@ -5,7 +5,7 @@ -- Maintainer : cryptol@galois.com -- Stability : provisional -- Portability : portable --- +-- -- TODO: -- - Putting in a normal form to spot "prove by assumption" -- - Additional simplification rules, namely various cancelation. @@ -841,6 +841,3 @@ cryNatOp op x y = Impossible -> PFalse -- It doesn't matter, but @false@ might anihilate. Return p -> p If p t e -> p :&& toProp t :|| Not p :&& toProp e - - - diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify1.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify1.hs index 1e0775d1..bf8968e2 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify1.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify1.hs @@ -5,16 +5,16 @@ -- Maintainer : cryptol@galois.com -- Stability : provisional -- Portability : portable --- +-- -- Simplification. -- The rules in this module are all conditional on the expressions being -- well-defined. --- +-- -- So, for example, consider the formula `P`, which corresponds to `fin e`. -- `P` says the following: --- +-- -- if e is well-formed, then will evaluate to a finite natural number. --- +-- -- More concretely, consider `fin (3 - 5)`. This will be simplified to `True`, -- which does not mean that `3 - 5` is actually finite. @@ -509,5 +509,3 @@ eNoInf expr = (_, K Inf, _) -> Impossible (_, _, K Inf) -> Impossible _ -> return (f x' y' z') - - diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/SimplifyExpr.hs b/src/Cryptol/TypeCheck/Solver/Numeric/SimplifyExpr.hs index 15c2bca5..2501bce3 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/SimplifyExpr.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/SimplifyExpr.hs @@ -9,9 +9,9 @@ -- Simplification of expressions. -- The result of simplifying an expression `e`, is a new expression `e'`, -- which satisfies the property: --- +-- -- if e is well-defined then e and e' will evaluate to the same type. --- +-- {-# LANGUAGE Safe, BangPatterns #-} module Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr where @@ -211,6 +211,3 @@ crySimpExprStep1 expr = case (x,y,z) of (K a, K b, K c) -> K `fmap` IN.nLenFromThenTo a b c _ -> Nothing - - - diff --git a/tests/issues/issue187.cry b/tests/issues/issue187.cry index e72582e3..c2ecf5c7 100644 --- a/tests/issues/issue187.cry +++ b/tests/issues/issue187.cry @@ -8,7 +8,7 @@ enigmaLoop = undefined // Encryption/Decryption enigma : {n, m} (fin n, fin m) => ([n], [m]) -> [m] enigma (m, pt) = tail [ True | _ <- rcs ] - where rcs = [ (m, True)] # + where rcs = [ (m, True)] # [ (enigmaLoop, True) | _ <- pt | (_,_) <- rcs diff --git a/tests/issues/issue212.cry b/tests/issues/issue212.cry index 09835e05..5f505242 100644 --- a/tests/issues/issue212.cry +++ b/tests/issues/issue212.cry @@ -7,7 +7,7 @@ width_eq_geq : {n} (32 == width n, n >= 1) => [n]Bit width_eq_geq = [True | _ <- [1..n] : [_][32] ] -// Want: const >= width (x+1) ==> const > width x +// Want: const >= width (x+1) ==> const > width x // or any monotonic function, not just addition. // // Also Want: const >= width n ==> fin n @@ -19,7 +19,7 @@ can_not_width = zero # (`n : [width n]) // Want: Honestly, I don't know what's going on here. It seems to relate to some of our regressions though. // Tell me if there should be another ticket - probably one that already exists. -TMD -// Issue: Cryptol 2.3 wants 'n == 4 + (?a3 - n % 4)' +// Issue: Cryptol 2.3 wants 'n == 4 + (?a3 - n % 4)' take_knows_no_bounds : {n} (fin n, n >= 4) => [n][8] -> [4 - (n%4)][8] take_knows_no_bounds ns = foo where diff --git a/tests/issues/issue225.cry b/tests/issues/issue225.cry index 44a543b8..ca479e34 100644 --- a/tests/issues/issue225.cry +++ b/tests/issues/issue225.cry @@ -1,4 +1,4 @@ -module EnigmaBroke where +module EnigmaBroke where type Rotor = [26](Char, Bit) @@ -20,4 +20,3 @@ joinRotors (rotors, inputChar) = (rotors', outputChar) ] rotors' = tail [ r | (_, _, r) <- ncrs ] (_, outputChar, _) = ncrs ! 0 - diff --git a/tests/issues/issue289.cry b/tests/issues/issue289.cry index 71aa24d0..2d08ca4f 100644 --- a/tests/issues/issue289.cry +++ b/tests/issues/issue289.cry @@ -1,6 +1,6 @@ average33 : [32] -> [32] -> [32] average33 x y = drop`{1}(z'/2) - where + where z' : [33] z' = (0b0 # x) + (0b0 # y) diff --git a/tests/issues/simon.cry2 b/tests/issues/simon.cry2 index fe9c2589..fc631a4d 100644 --- a/tests/issues/simon.cry2 +++ b/tests/issues/simon.cry2 @@ -52,7 +52,7 @@ f x = ((x <<< 1) && (x <<< 8)) ^ (x <<< 2) // encryption / decryption /////////////////////////////////////////////////////////////////////// -encrypt : {n, m, T, j} +encrypt : {n, m, T, j} ( fin n, fin m, fin T, fin j , n >= 2, T - 1 >= m, T >= 1 ) => [m][n] -> ([n], [n]) -> ([n], [n]) @@ -62,7 +62,7 @@ encrypt k0 p0 = ps ! 0 ks = expandKey `{n=n,m=m,T=T,j=j} (reverse k0) -decrypt : {n, m, T, j} +decrypt : {n, m, T, j} ( fin n, fin m, fin T, fin j , n >= 2, T - 1 >= m, T >= 1 ) => [m][n] -> ([n], [n]) -> ([n], [n]) diff --git a/tests/parser/nested-where.cry b/tests/parser/nested-where.cry index e01960da..ecd7db64 100644 --- a/tests/parser/nested-where.cry +++ b/tests/parser/nested-where.cry @@ -1,4 +1,4 @@ -/* This is +/* This is a block comment */ test1 = 1 where x = 2 diff --git a/tests/parser/pat1.cry b/tests/parser/pat1.cry index 63933449..854c5e07 100644 --- a/tests/parser/pat1.cry +++ b/tests/parser/pat1.cry @@ -14,7 +14,7 @@ let {} in a : [10] case a : [10] of { } -// f (a :# b :: Int) = +// f (a :# b :: Int) = (fa,fb) = f6 diff --git a/tests/regression/AES.cry b/tests/regression/AES.cry index 2cc9a19a..4282cd22 100644 --- a/tests/regression/AES.cry +++ b/tests/regression/AES.cry @@ -23,7 +23,7 @@ type AESKeySize = (Nk*32) type GF28 = [8] type State = [4][Nb]GF28 type RoundKey = State -type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey) +type KeySchedule = (RoundKey, [Nr-1]RoundKey, RoundKey) // GF28 operations gf28Add : {n} (fin n) => [n]GF28 -> GF28 gf28Add ps = sums ! 0 @@ -213,5 +213,3 @@ sbox = [ 0xe1, 0xf8, 0x98, 0x11, 0x69, 0xd9, 0x8e, 0x94, 0x9b, 0x1e, 0x87, 0xe9, 0xce, 0x55, 0x28, 0xdf, 0x8c, 0xa1, 0x89, 0x0d, 0xbf, 0xe6, 0x42, 0x68, 0x41, 0x99, 0x2d, 0x0f, 0xb0, 0x54, 0xbb, 0x16 ] - - diff --git a/tests/regression/check09.cry b/tests/regression/check09.cry index 46d9c770..3b032129 100644 --- a/tests/regression/check09.cry +++ b/tests/regression/check09.cry @@ -5,7 +5,7 @@ initL = [0] ss = [ (s + a + b) <<< 3 | s <- initS # ss | a <- [1] # ss | b <- [0] # ls ] -ls = [ (l + a + b) <<< (a + b) +ls = [ (l + a + b) <<< (a + b) | l <- initL # ls | a <- ss | b <- [0] # ls ] @@ -30,7 +30,7 @@ keyX key = ss @@ [ 0 .. 6 ] | b <- [0] # ls ] // NOTE different endianness from Cryptol 1 test -check9b = keyX (reverse "abcd") == +check9b = keyX (reverse "abcd") == [0x00000008, 0x1b134ba3, 0x11ae69b1, 0xb7b3f42f, 0xc9eb1fdc, 0x008b5f36, 0x8991bc8c] diff --git a/tests/regression/check23.cry b/tests/regression/check23.cry index 47614fec..c9108b42 100644 --- a/tests/regression/check23.cry +++ b/tests/regression/check23.cry @@ -1,4 +1,4 @@ -pad : {msgLen, padding, contentLen, chunks} +pad : {msgLen, padding, contentLen, chunks} ( fin msgLen , fin padding , contentLen == msgLen + 65