diff options
Diffstat (limited to 'automation/saw/chacha20.cry')
| -rw-r--r-- | automation/saw/chacha20.cry | 357 |
1 files changed, 0 insertions, 357 deletions
diff --git a/automation/saw/chacha20.cry b/automation/saw/chacha20.cry deleted file mode 100644 index 0b52d51ad..000000000 --- a/automation/saw/chacha20.cry +++ /dev/null @@ -1,357 +0,0 @@ -/* -** ChaCha20 specification -** Author: Austin Seipp <aseipp@pobox.com>. Released in the Public Domain. -** -** Based on RFC 7539 - "ChaCha20 and Poly1305 for IETF Protocols" -** https://tools.ietf.org/html/rfc7539 -*/ -module chacha20 where - -/* -------------------------------------------------------------------------- */ -/* -- Implementation -------------------------------------------------------- */ - -type Round = [16][32] // An input to the ChaCha20 core function -type Block = [64][8] // An output block from the ChaCha20 core function. -type Key = [32][8] // A 32-byte input key -type Nonce = [12][8] // A 12-byte nonce -type Counter = [32] // Starting block counter. Usually 1 or 0. - -/* ---------------------------------- */ -/* -- Quarter Round ----------------- */ - -// The quarter round. This takes 4 32-bit integers and diffuses them -// appropriately, and is the core of the column and diagonal round. -qround : [4][32] -> [4][32] -qround [ a0, b0, c0, d0 ] = [ a2, b4, c2, d4 ] - where - a1 = a0 + b0 /* a += b; d ^= a; d <<<= 16 */ - d1 = d0 ^ a1 - d2 = d1 <<< 16 - - c1 = c0 + d2 /* c += d; b ^= c; b <<<= 12 */ - b1 = b0 ^ c1 - b2 = b1 <<< 12 - - a2 = a1 + b2 /* a += b; d ^= a; d <<<= 8 */ - d3 = d2 ^ a2 - d4 = d3 <<< 8 - - c2 = c1 + d4 /* c += d; b ^= c; b <<<= 7 */ - b3 = b2 ^ c2 - b4 = b3 <<< 7 - - -/* ---------------------------------- */ -/* -- Column and diagonal rounds ---- */ - -// Perform the column round, followed by the diagonal round on the -// input state, which are both defined in terms of the quarter -// round. ChaCha20 requires 20 total rounds of interleaving -// column/diagonal passes on the state, and therefore `cdround` actually -// does two passes at once (mostly for simplicity). -cdround : Round -> Round -cdround [ x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15 ] - = [ z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15 ] - where - // Column round - [ y0, y4, y8, y12 ] = qround [ x0, x4, x8, x12 ] - [ y1, y5, y9, y13 ] = qround [ x1, x5, x9, x13 ] - [ y2, y6, y10, y14 ] = qround [ x2, x6, x10, x14 ] - [ y3, y7, y11, y15 ] = qround [ x3, x7, x11, x15 ] - - // Diagonal round - [ z0, z5, z10, z15 ] = qround [ y0, y5, y10, y15 ] - [ z1, z6, z11, z12 ] = qround [ y1, y6, y11, y12 ] - [ z2, z7, z8, z13 ] = qround [ y2, y7, y8, y13 ] - [ z3, z4, z9, z14 ] = qround [ y3, y4, y9, y14 ] - - -/* ---------------------------------- */ -/* -- Block encryption -------------- */ - -// Given an input round, calculate the core ChaCha20 algorithm over -// the round and return an output block. These output blocks form the -// stream which you XOR your plaintext with, and successive iterations of -// the core algorithm result in an infinite stream you can use as a -// cipher. -core : Round -> Block -core x = block - where - rounds = iterate cdround x // Do a bunch of column/diagonal passes... - result = rounds @ 10 // And grab the 10th result (20 total passes) - block = blocked (x + result) // Add to input, convert to output block - - -/* ---------------------------------- */ -/* -- Key Expansion ----------------- */ - -// Key expansion. Given a nonce and a key, compute a round (which is -// fed to the core algorithm above) by taking the initial round state and -// mixing in the key and nonce appropriately. -kexp : Key -> Counter -> Nonce -> Round -kexp k c n = [ c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15 ] - where - // The following describes the layout of the output round, which - // is fed into the core algorithm successively. - - // Bytes 0-3: Constants - [ c0, c1, c2, c3 ] = [ 0x61707865, 0x3320646e, 0x79622d32, 0x6b206574 ] - - // Bytes 4-11: Key - [ c4, c5, c6, c7 ] = map rjoin (groupBy`{4} kslice1 : [4][4][8]) : [4][32] - [ c8, c9, c10, c11 ] = map rjoin (groupBy`{4} kslice2 : [4][4][8]) : [4][32] - kslice1 = k @@ ([ 0 .. 15 ] : [16][32]) // Top half - kslice2 = k @@ ([ 16 .. 31 ] : [16][32]) // Bottom half - - // Bytes 12: Counter, starts off with whatever the user specified - // (usually 0 or 1) - [ c12 ] = [ c ] - - // Bytes 14-15: Nonce - [ c13, c14, c15 ] = map rjoin (groupBy`{4} n) - - -/* ---------------------------------- */ -/* -- Round increments -------------- */ - -// Take a given number of iterations and the input round (after key -// expansion!), and calculate the input round for the core algorithm -// function. This allows you to index into a particular Round which -// can be passed to the 'core' function. -iround : [64] -> Round -> Round -iround n r = (iterate once r) @ n where - // Given a round, increment the counter inside (index no 12) - once [ x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15 ] - = [ x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12+1, x13, x14, x15 ] - -/* ---------------------------------- */ -/* -- ChaCha20 encryption ----------- */ - -// Produce a psuedo-random stream given a nonce and a key, which can -// be XOR'd with your data to encrypt it. -stream : {n} (fin n) => Key -> Counter -> Nonce -> [n][8] -stream k c n = take`{n} (join rounds) // Take n bytes from the final result - where - // Expand key - key = kexp k c n - - // Produce the stream by successively incrementing the input round - // by `i`, and running the core algorithm to get the resulting - // stream for the `i`th input. Once these are concatenated, you have - // an infinite list representing the ChaCha20 stream. - rounds = [ core (iround i key) | i <- [ 0, 1 ... ] ] - - -// Given an message, a nonce, and a key, produce an encrypted -// message. This is simply defined as the XOR of the message and the -// corresponding encryption stream. -encrypt : {n} (fin n) => Key -> Counter -> Nonce -> [n][8] -> [n][8] -encrypt k c n m = m ^ (stream k c n) - -/* -------------------------------------------------------------------------- */ -/* -- Theorems, tests ------------------------------------------------------- */ - -// Tests are private -private - qround01 = qround in == out - where - in = [ 0x11111111, 0x01020304, 0x9b8d6f43, 0x01234567 ] - out = [ 0xea2a92f4, 0xcb1cf8ce, 0x4581472e, 0x5881c4bb ] - - core01 = kexp k 1 n == out - where - n = [ 0x00, 0x00, 0x00, 0x09, 0x00, 0x00, 0x00, 0x4a, - 0x00, 0x00, 0x00, 0x00 ] - k = [ 0x00, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, - 0x08, 0x09, 0x0a, 0x0b, 0x0c, 0x0d, 0x0e, 0x0f, - 0x10, 0x11, 0x12, 0x13, 0x14, 0x15, 0x16, 0x17, - 0x18, 0x19, 0x1a, 0x1b, 0x1c, 0x1d, 0x1e, 0x1f ] - out = [ 0x61707865, 0x3320646e, 0x79622d32, 0x6b206574, - 0x03020100, 0x07060504, 0x0b0a0908, 0x0f0e0d0c, - 0x13121110, 0x17161514, 0x1b1a1918, 0x1f1e1d1c, - 0x00000001, 0x09000000, 0x4a000000, 0x00000000 ] - - core02 = core (kexp k 1 n) == out - where - n = [ 0x00, 0x00, 0x00, 0x09, 0x00, 0x00, 0x00, 0x4a, - 0x00, 0x00, 0x00, 0x00 ] - k = [ 0x00, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, - 0x08, 0x09, 0x0a, 0x0b, 0x0c, 0x0d, 0x0e, 0x0f, - 0x10, 0x11, 0x12, 0x13, 0x14, 0x15, 0x16, 0x17, - 0x18, 0x19, 0x1a, 0x1b, 0x1c, 0x1d, 0x1e, 0x1f ] - out = [ 0x10, 0xf1, 0xe7, 0xe4, 0xd1, 0x3b, 0x59, 0x15, - 0x50, 0x0f, 0xdd, 0x1f, 0xa3, 0x20, 0x71, 0xc4, - 0xc7, 0xd1, 0xf4, 0xc7, 0x33, 0xc0, 0x68, 0x03, - 0x04, 0x22, 0xaa, 0x9a, 0xc3, 0xd4, 0x6c, 0x4e, - 0xd2, 0x82, 0x64, 0x46, 0x07, 0x9f, 0xaa, 0x09, - 0x14, 0xc2, 0xd7, 0x05, 0xd9, 0x8b, 0x02, 0xa2, - 0xb5, 0x12, 0x9c, 0xd1, 0xde, 0x16, 0x4e, 0xb9, - 0xcb, 0xd0, 0x83, 0xe8, 0xa2, 0x50, 0x3c, 0x4e ] - - rfctest01 = encrypt zero zero zero zero - == [ 0x76, 0xb8, 0xe0, 0xad, 0xa0, 0xf1, 0x3d, 0x90, 0x40, 0x5d, - 0x6a, 0xe5, 0x53, 0x86, 0xbd, 0x28, 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 ] - - rfctest02 = encrypt (zero # [1]) 1 (zero # [2]) msg == out - where - out = [ 0xa3, 0xfb, 0xf0, 0x7d, 0xf3, 0xfa, 0x2f, 0xde, 0x4f, 0x37, - 0x6c, 0xa2, 0x3e, 0x82, 0x73, 0x70, 0x41, 0x60, 0x5d, 0x9f, - 0x4f, 0x4f, 0x57, 0xbd, 0x8c, 0xff, 0x2c, 0x1d, 0x4b, 0x79, - 0x55, 0xec, 0x2a, 0x97, 0x94, 0x8b, 0xd3, 0x72, 0x29, 0x15, - 0xc8, 0xf3, 0xd3, 0x37, 0xf7, 0xd3, 0x70, 0x05, 0x0e, 0x9e, - 0x96, 0xd6, 0x47, 0xb7, 0xc3, 0x9f, 0x56, 0xe0, 0x31, 0xca, - 0x5e, 0xb6, 0x25, 0x0d, 0x40, 0x42, 0xe0, 0x27, 0x85, 0xec, - 0xec, 0xfa, 0x4b, 0x4b, 0xb5, 0xe8, 0xea, 0xd0, 0x44, 0x0e, - 0x20, 0xb6, 0xe8, 0xdb, 0x09, 0xd8, 0x81, 0xa7, 0xc6, 0x13, - 0x2f, 0x42, 0x0e, 0x52, 0x79, 0x50, 0x42, 0xbd, 0xfa, 0x77, - 0x73, 0xd8, 0xa9, 0x05, 0x14, 0x47, 0xb3, 0x29, 0x1c, 0xe1, - 0x41, 0x1c, 0x68, 0x04, 0x65, 0x55, 0x2a, 0xa6, 0xc4, 0x05, - 0xb7, 0x76, 0x4d, 0x5e, 0x87, 0xbe, 0xa8, 0x5a, 0xd0, 0x0f, - 0x84, 0x49, 0xed, 0x8f, 0x72, 0xd0, 0xd6, 0x62, 0xab, 0x05, - 0x26, 0x91, 0xca, 0x66, 0x42, 0x4b, 0xc8, 0x6d, 0x2d, 0xf8, - 0x0e, 0xa4, 0x1f, 0x43, 0xab, 0xf9, 0x37, 0xd3, 0x25, 0x9d, - 0xc4, 0xb2, 0xd0, 0xdf, 0xb4, 0x8a, 0x6c, 0x91, 0x39, 0xdd, - 0xd7, 0xf7, 0x69, 0x66, 0xe9, 0x28, 0xe6, 0x35, 0x55, 0x3b, - 0xa7, 0x6c, 0x5c, 0x87, 0x9d, 0x7b, 0x35, 0xd4, 0x9e, 0xb2, - 0xe6, 0x2b, 0x08, 0x71, 0xcd, 0xac, 0x63, 0x89, 0x39, 0xe2, - 0x5e, 0x8a, 0x1e, 0x0e, 0xf9, 0xd5, 0x28, 0x0f, 0xa8, 0xca, - 0x32, 0x8b, 0x35, 0x1c, 0x3c, 0x76, 0x59, 0x89, 0xcb, 0xcf, - 0x3d, 0xaa, 0x8b, 0x6c, 0xcc, 0x3a, 0xaf, 0x9f, 0x39, 0x79, - 0xc9, 0x2b, 0x37, 0x20, 0xfc, 0x88, 0xdc, 0x95, 0xed, 0x84, - 0xa1, 0xbe, 0x05, 0x9c, 0x64, 0x99, 0xb9, 0xfd, 0xa2, 0x36, - 0xe7, 0xe8, 0x18, 0xb0, 0x4b, 0x0b, 0xc3, 0x9c, 0x1e, 0x87, - 0x6b, 0x19, 0x3b, 0xfe, 0x55, 0x69, 0x75, 0x3f, 0x88, 0x12, - 0x8c, 0xc0, 0x8a, 0xaa, 0x9b, 0x63, 0xd1, 0xa1, 0x6f, 0x80, - 0xef, 0x25, 0x54, 0xd7, 0x18, 0x9c, 0x41, 0x1f, 0x58, 0x69, - 0xca, 0x52, 0xc5, 0xb8, 0x3f, 0xa3, 0x6f, 0xf2, 0x16, 0xb9, - 0xc1, 0xd3, 0x00, 0x62, 0xbe, 0xbc, 0xfd, 0x2d, 0xc5, 0xbc, - 0xe0, 0x91, 0x19, 0x34, 0xfd, 0xa7, 0x9a, 0x86, 0xf6, 0xe6, - 0x98, 0xce, 0xd7, 0x59, 0xc3, 0xff, 0x9b, 0x64, 0x77, 0x33, - 0x8f, 0x3d, 0xa4, 0xf9, 0xcd, 0x85, 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 ] - - msg = [ 0x41, 0x6e, 0x79, 0x20, 0x73, 0x75, 0x62, 0x6d, 0x69, 0x73, - 0x73, 0x69, 0x6f, 0x6e, 0x20, 0x74, 0x6f, 0x20, 0x74, 0x68, - 0x65, 0x20, 0x49, 0x45, 0x54, 0x46, 0x20, 0x69, 0x6e, 0x74, - 0x65, 0x6e, 0x64, 0x65, 0x64, 0x20, 0x62, 0x79, 0x20, 0x74, - 0x68, 0x65, 0x20, 0x43, 0x6f, 0x6e, 0x74, 0x72, 0x69, 0x62, - 0x75, 0x74, 0x6f, 0x72, 0x20, 0x66, 0x6f, 0x72, 0x20, 0x70, - 0x75, 0x62, 0x6c, 0x69, 0x63, 0x61, 0x74, 0x69, 0x6f, 0x6e, - 0x20, 0x61, 0x73, 0x20, 0x61, 0x6c, 0x6c, 0x20, 0x6f, 0x72, - 0x20, 0x70, 0x61, 0x72, 0x74, 0x20, 0x6f, 0x66, 0x20, 0x61, - 0x6e, 0x20, 0x49, 0x45, 0x54, 0x46, 0x20, 0x49, 0x6e, 0x74, - 0x65, 0x72, 0x6e, 0x65, 0x74, 0x2d, 0x44, 0x72, 0x61, 0x66, - 0x74, 0x20, 0x6f, 0x72, 0x20, 0x52, 0x46, 0x43, 0x20, 0x61, - 0x6e, 0x64, 0x20, 0x61, 0x6e, 0x79, 0x20, 0x73, 0x74, 0x61, - 0x74, 0x65, 0x6d, 0x65, 0x6e, 0x74, 0x20, 0x6d, 0x61, 0x64, - 0x65, 0x20, 0x77, 0x69, 0x74, 0x68, 0x69, 0x6e, 0x20, 0x74, - 0x68, 0x65, 0x20, 0x63, 0x6f, 0x6e, 0x74, 0x65, 0x78, 0x74, - 0x20, 0x6f, 0x66, 0x20, 0x61, 0x6e, 0x20, 0x49, 0x45, 0x54, - 0x46, 0x20, 0x61, 0x63, 0x74, 0x69, 0x76, 0x69, 0x74, 0x79, - 0x20, 0x69, 0x73, 0x20, 0x63, 0x6f, 0x6e, 0x73, 0x69, 0x64, - 0x65, 0x72, 0x65, 0x64, 0x20, 0x61, 0x6e, 0x20, 0x22, 0x49, - 0x45, 0x54, 0x46, 0x20, 0x43, 0x6f, 0x6e, 0x74, 0x72, 0x69, - 0x62, 0x75, 0x74, 0x69, 0x6f, 0x6e, 0x22, 0x2e, 0x20, 0x53, - 0x75, 0x63, 0x68, 0x20, 0x73, 0x74, 0x61, 0x74, 0x65, 0x6d, - 0x65, 0x6e, 0x74, 0x73, 0x20, 0x69, 0x6e, 0x63, 0x6c, 0x75, - 0x64, 0x65, 0x20, 0x6f, 0x72, 0x61, 0x6c, 0x20, 0x73, 0x74, - 0x61, 0x74, 0x65, 0x6d, 0x65, 0x6e, 0x74, 0x73, 0x20, 0x69, - 0x6e, 0x20, 0x49, 0x45, 0x54, 0x46, 0x20, 0x73, 0x65, 0x73, - 0x73, 0x69, 0x6f, 0x6e, 0x73, 0x2c, 0x20, 0x61, 0x73, 0x20, - 0x77, 0x65, 0x6c, 0x6c, 0x20, 0x61, 0x73, 0x20, 0x77, 0x72, - 0x69, 0x74, 0x74, 0x65, 0x6e, 0x20, 0x61, 0x6e, 0x64, 0x20, - 0x65, 0x6c, 0x65, 0x63, 0x74, 0x72, 0x6f, 0x6e, 0x69, 0x63, - 0x20, 0x63, 0x6f, 0x6d, 0x6d, 0x75, 0x6e, 0x69, 0x63, 0x61, - 0x74, 0x69, 0x6f, 0x6e, 0x73, 0x20, 0x6d, 0x61, 0x64, 0x65, - 0x20, 0x61, 0x74, 0x20, 0x61, 0x6e, 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 ] - - rfctest03 = encrypt key 42 (zero # [2]) msg == out - where - key = [ 0x1c, 0x92, 0x40, 0xa5, 0xeb, 0x55, 0xd3, 0x8a, 0xf3, 0x33, - 0x88, 0x86, 0x04, 0xf6, 0xb5, 0xf0, 0x47, 0x39, 0x17, 0xc1, - 0x40, 0x2b, 0x80, 0x09, 0x9d, 0xca, 0x5c, 0xbc, 0x20, 0x70, - 0x75, 0xc0 ] - out = [ 0x27, 0x54, 0x77, 0x61, 0x73, 0x20, 0x62, 0x72, 0x69, 0x6c, - 0x6c, 0x69, 0x67, 0x2c, 0x20, 0x61, 0x6e, 0x64, 0x20, 0x74, - 0x68, 0x65, 0x20, 0x73, 0x6c, 0x69, 0x74, 0x68, 0x79, 0x20, - 0x74, 0x6f, 0x76, 0x65, 0x73, 0x0a, 0x44, 0x69, 0x64, 0x20, - 0x67, 0x79, 0x72, 0x65, 0x20, 0x61, 0x6e, 0x64, 0x20, 0x67, - 0x69, 0x6d, 0x62, 0x6c, 0x65, 0x20, 0x69, 0x6e, 0x20, 0x74, - 0x68, 0x65, 0x20, 0x77, 0x61, 0x62, 0x65, 0x3a, 0x0a, 0x41, - 0x6c, 0x6c, 0x20, 0x6d, 0x69, 0x6d, 0x73, 0x79, 0x20, 0x77, - 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 ] - - msg = [ 0x62, 0xe6, 0x34, 0x7f, 0x95, 0xed, 0x87, 0xa4, 0x5f, 0xfa, - 0xe7, 0x42, 0x6f, 0x27, 0xa1, 0xdf, 0x5f, 0xb6, 0x91, 0x10, - 0x04, 0x4c, 0x0d, 0x73, 0x11, 0x8e, 0xff, 0xa9, 0x5b, 0x01, - 0xe5, 0xcf, 0x16, 0x6d, 0x3d, 0xf2, 0xd7, 0x21, 0xca, 0xf9, - 0xb2, 0x1e, 0x5f, 0xb1, 0x4c, 0x61, 0x68, 0x71, 0xfd, 0x84, - 0xc5, 0x4f, 0x9d, 0x65, 0xb2, 0x83, 0x19, 0x6c, 0x7f, 0xe4, - 0xf6, 0x05, 0x53, 0xeb, 0xf3, 0x9c, 0x64, 0x02, 0xc4, 0x22, - 0x34, 0xe3, 0x2a, 0x35, 0x6b, 0x3e, 0x76, 0x43, 0x12, 0xa6, - 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 allTestsPass = - ([ // Basic tests - qround01, core01, core02 - // Full RFC test vectors - , rfctest01, rfctest02, rfctest03 - ] : [_]Bit) == ~zero // All test bits should equal one - -/* -------------------------------------------------------------------------- */ -/* -- Private utilities ----------------------------------------------------- */ - -private - // Convert a round into a block, by splitting every 32-bit round entry - // into 4 bytes, and then serialize those values into a full block. - blocked : Round -> Block - blocked x = join (map toBytes x) - where - // This essentially splits a 32-bit number into 4-byte - // little-endian form, where 'rjoin' is the inverse and would merge - // 4 bytes as a 32-bit little endian number. - toBytes : [32] -> [4][8] - toBytes v = reverse (groupBy`{8} v) - - // Map a function over a finite list. - map : { a, b, c } - (a -> b) -> [c]a -> [c]b - map f xs = [ f x | x <- xs ] - - // Map a function iteratively over a seed value, producing an infinite - // list of successive function applications: - // - // iterate f 0 == [ 0, f 0, f (f 0), f (f (f 0)), ... ] - iterate : { a } (a -> a) -> a -> [inf]a - iterate f x = [x] # [ f v | v <- iterate f x ] - where - // NB: Needs a binded name in order to tie the recursive knot. - xs = [x] # [ f v | v <- xs ] - - // rjoin = join . reverse - // This encodes a sequence of values as a little endian number - // e.g. [ 0xaa, 0xbb, 0xcc, 0xdd ] is serialized as \xdd\xcc\xbb\xaa - rjoin : {a, b, c} - ( fin a, fin c - ) => [c][a]b -> [a * c]b - rjoin x = join (reverse x) |