From c8b6285ec49ecb037cbba6f96f7122fd3bb2b3ac Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Tue, 17 Sep 2024 16:20:34 -0400 Subject: [PATCH 1/8] sha3: update theta step mapping #138 --- Primitive/Keyless/Hash/keccak.cry | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/Primitive/Keyless/Hash/keccak.cry b/Primitive/Keyless/Hash/keccak.cry index 6480504e..f0c6c1e4 100644 --- a/Primitive/Keyless/Hash/keccak.cry +++ b/Primitive/Keyless/Hash/keccak.cry @@ -129,22 +129,21 @@ private /** * One of the step mappings that's part of a round of Keccak-p. * + * The effect of this mapping is to XOR each bit in the state with the + * parity of two columns in the array. `C` computes the parities, `D` + * combines two of the parities for each column, and `A'` completes the + * transformation. * [FIPS-202] Section 3.2.1. */ θ : State -> State θ A = A' where - C = [ xor a | a <- A ] - D = [ C @ x ^ (C @ y <<< 1) - // In the spec, this is denoted `(x-1) mod 5` for 0 <= x < 5. - | (x:[8]) <- [4,0,1,2,3] - // In the spec, this is denoted `(x+1) mod 5` for 0 <= x < 5. - | (y:[8]) <- [1,2,3,4,0] - ] - A' = [ [ a ^ (D @ x) | a <- A @ x ] | (x:[8]) <- [0 .. 4] ] - - xor : {a, l} (fin a) => [a][l] -> [l] - xor xs = xors ! 0 - where xors = [zero] # [ x ^ z | x <- xs | z <- xors ] + C = [ A@x@0 ^ A@x@1 ^ A@x@2 ^ A@x@3 ^ A@x@4 + | x <- [0..4]] + D = [ C @ ((x - 1) % 5) ^ (C @ ((x + 1) % 5) <<< 1) + | x <- [0..4]] + A' = [[ A@x@y ^ D@x + | y <- [0..4]] + | x <- [0..4] ] /** From 7a0787cb7a84fb773d1c6814f35ed6364c7ed9d5 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Tue, 17 Sep 2024 16:28:39 -0400 Subject: [PATCH 2/8] sha3: update rho step mapping #138 --- Primitive/Keyless/Hash/keccak.cry | 30 +++++++++++++++++++++--------- 1 file changed, 21 insertions(+), 9 deletions(-) diff --git a/Primitive/Keyless/Hash/keccak.cry b/Primitive/Keyless/Hash/keccak.cry index f0c6c1e4..771fcf08 100644 --- a/Primitive/Keyless/Hash/keccak.cry +++ b/Primitive/Keyless/Hash/keccak.cry @@ -149,18 +149,30 @@ private /** * One of the step mappings that's part of a round of Keccak-p. * + * The effect of thuis mapping is to rotate the bits of each lane by a + * an _offset_ (computed in `set_lane`) that depends on the `x` and `y` + * coordinates of that lane. * [FIPS-202] Section 3.2.2. */ ρ : State -> State - ρ A = groupBy`{5} [ a <<< r | a <- join A | (r:[8]) <- R ] - where - R = [ - 00, 36, 03, 41, 18, - 01, 44, 10, 45, 02, - 62, 06, 43, 15, 61, - 28, 55, 25, 21, 56, - 27, 20, 39, 08, 14 - ] + ρ A = A' where + // Step 1. + A1 = [[ if (x == 0) && (y == 0) then A@0@0 else zero + | y <- [0..4]] + | x <- [0..4]] + // Step 2-3. + As = [((1,0), A1)] # + [ ((y, (2*x + 3*y) % 5), set_lane x y t Ai) + | ((x, y), Ai) <- As + | t <- [0..23]] + (_, A') = As ! 0 + + // Step 3a. Update the lane defined by x' and y'. + set_lane x' y' t Ai = [[ + if (x' == x) && (y' == y) then A@x@y <<< ((t+1)*(t+2)/2) + else Ai@x@y + | y <- [0..4]] + | x <- [0..4]] /** * One of the step mappings that's part of a round of Keccak-p. From c3418251e757da8be4471235d1495aef8c40df52 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Tue, 17 Sep 2024 16:30:50 -0400 Subject: [PATCH 3/8] sha3: update pi step mapping #138 --- Primitive/Keyless/Hash/keccak.cry | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Primitive/Keyless/Hash/keccak.cry b/Primitive/Keyless/Hash/keccak.cry index 771fcf08..2e5bde05 100644 --- a/Primitive/Keyless/Hash/keccak.cry +++ b/Primitive/Keyless/Hash/keccak.cry @@ -149,7 +149,7 @@ private /** * One of the step mappings that's part of a round of Keccak-p. * - * The effect of thuis mapping is to rotate the bits of each lane by a + * The effect of this mapping is to rotate the bits of each lane by a * an _offset_ (computed in `set_lane`) that depends on the `x` and `y` * coordinates of that lane. * [FIPS-202] Section 3.2.2. @@ -177,12 +177,14 @@ private /** * One of the step mappings that's part of a round of Keccak-p. * + * The effect of this mapping is to rearrange the position of the lanes, + * based on an offset of the `x` and `y` coordinates. * [FIPS-202] Section 3.2.3. */ π : State -> State - π A = groupBy`{5} [ A @ ((x + 3*y) % 5) @ x - | (x:[8]) <- [0..4], (y:[8]) <- [0..4] - ] + π A = [[ A @((x + 3 * y) % 5) @x + | y <- [0..4]] + | x <- [0..4]] /** * One of the step mappings that's part of a round of Keccak-p. From f0ed1995f8dacc1930e1d604978a6f1d71727b6e Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Wed, 18 Sep 2024 08:36:02 -0400 Subject: [PATCH 4/8] sha3: update chi step mapping #138 --- Primitive/Keyless/Hash/keccak.cry | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/Primitive/Keyless/Hash/keccak.cry b/Primitive/Keyless/Hash/keccak.cry index 2e5bde05..1fda880f 100644 --- a/Primitive/Keyless/Hash/keccak.cry +++ b/Primitive/Keyless/Hash/keccak.cry @@ -189,13 +189,18 @@ private /** * One of the step mappings that's part of a round of Keccak-p. * + * The effect of this mapping is to XOR each bit with a non-linear function + * of two other bits in its row. * [FIPS-202] Section 3.2.4. + * + * Note: in the first line, XOR 1 on a single bit is equivalent to bitwise + * NOT. Since we operate over the whole slice defined by each z-coordinate, + * it's nicer to use `~`. You can see the NOT gates in Figure 6. */ χ : State -> State - χ A = groupBy`{5} [ (A @ x @ y) ^ (~ A @ ((x + 1) % 5) @ y - && A @ ((x + 2) % 5) @ y) - | (x:[8]) <- [0..4], (y:[8]) <- [0..4] - ] + χ A = [[ A @x @y ^ (~A @((x + 1) % 5) @y && A @((x + 2) % 5) @y) + | y <- [0..4]] + | x <- [0..4]] /** * One of the step mappings that's part of a round of Keccak-p. From d20d32ff86cd09da0a3b8c261d2fa7d092c4c703 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Wed, 18 Sep 2024 08:51:16 -0400 Subject: [PATCH 5/8] sha3: update iota step mapping #138 This removes hard-coded round constants at a significant performance penalty. --- Primitive/Keyless/Hash/keccak.cry | 98 ++++++++++++++----------------- 1 file changed, 43 insertions(+), 55 deletions(-) diff --git a/Primitive/Keyless/Hash/keccak.cry b/Primitive/Keyless/Hash/keccak.cry index 1fda880f..1f6e766d 100644 --- a/Primitive/Keyless/Hash/keccak.cry +++ b/Primitive/Keyless/Hash/keccak.cry @@ -203,40 +203,52 @@ private | x <- [0..4]] /** - * One of the step mappings that's part of a round of Keccak-p. + * Compute the round constant for the `t`th lane. * - * [FIPS-202] Section 3.2.5, Algorithm 6 (kind of). + * [FIPS-202] Section 3.2.5, Algorithm 5. */ - ι : State -> State -> State - ι RC A = A ^ RC + rc : [8] -> Bit + rc t = if t % 255 == 0 then 1 // Step 1. + else Rs @ (t % 255) @0 // Step 4. + where + // Step 2 - 3. + Rs = [0b10000000] # [lfsr R | R <- Rs ] - /** - * Format the hard-coded round constant values. - * - * [FIPS-202] Section 3.2.5. - */ - RCs : {n} (fin n, 24 >= n, n == 12 + 2 * ell) => [n]State - RCs = take`{n} [ [[take`{w} RC] # zero] # zero | RC <- RCs64 ] + // Step 3. Linear feedback shift register. + // The truncation in step f is done manually in the return value. + lfsr : [8] -> [8] + lfsr Rin = [R0, R@1, R@2, R@3, R4, R5, R6, R@7] + where + R = 0b0 # Rin + R0 = R@0 ^ R@8 + R4 = R@4 ^ R@8 + R5 = R@5 ^ R@8 + R6 = R@6 ^ R@8 /** - * Hardcode the round constant values for b = 1600. - * [FIPS-202] Section 3.2.5. + * One of the step mappings that's part of a round of Keccak-p. + * + * The effect is to modify some of the bits of the Lane defined by + * `(0, 0)` according to the round index. + * [FIPS-202] Section 3.2.5, Algorithm 6. */ - RCs64 : [24][64] - RCs64 = join (transpose [ - [0x0000000000000001, 0x000000008000808B], - [0x0000000000008082, 0x800000000000008B], - [0x800000000000808A, 0x8000000000008089], - [0x8000000080008000, 0x8000000000008003], - [0x000000000000808B, 0x8000000000008002], - [0x0000000080000001, 0x8000000000000080], - [0x8000000080008081, 0x000000000000800A], - [0x8000000000008009, 0x800000008000000A], - [0x000000000000008A, 0x8000000080008081], - [0x0000000000000088, 0x8000000000008080], - [0x0000000080008009, 0x0000000080000001], - [0x000000008000000A, 0x8000000080008008] - ]) + ι : State -> [8] -> State + ι A ir = A'' where + // Step 1. + A' = A + // Step 2. + RC0 = zero : [w] + // Step 3. 0 is the identity for XOR, so we iteratively set the + // `2^j-1`th element by XORing the previously-set bits of RC with the + // correct value at the desired index. + RCs = [RC0] # [RC' ^ (zext`{w} [rc (j + 7 * ir)] << (2^^j - 1)) + | RC' <- RCs + | j <- [0..ell] ] + RC = (RCs ! 0) : [w] + // Step 4. + A'' = [[ if (x == 0) && (y == 0) then A'@0@0 ^ RC else A'@x@y + | y <- [0..4]] + | x <- [0..4]] /** * Padding rule `pad10*1`. @@ -268,7 +280,7 @@ private Keccak_f S = S' where A0 = unflatten S - rounds = [A0] # [ Round RC A | RC <- RCs | A <- rounds ] + rounds = [A0] # [ Round A ir | A <- rounds | ir <- [0..nr - 1]] S' = flatten (rounds ! 0) @@ -276,32 +288,8 @@ private * The round function for `Keccak-p`. Denoted `Rnd` in the spec. * [FIPS-202] Section 3.3. */ - Round : State -> State -> State - Round RC A = ι RC (χ (π (ρ (θ A)))) - - -/** - * Equivalence property showing that the hard-coded round constants - * match the description in the spec. - * [FIPS-202] Section 3.2.5. - * - * This takes about 6 seconds to prove. - * ```repl - * :prove RC_correct - * ``` - */ -RC_correct : [8] -> [8] -> Bool -property RC_correct i j = - // See Algorithm 6, Step 3. - i < 24 ==> j < `ell ==> RCs64@i!(2^^j - 1) == lfsr@(j + 7*i) - where - // Algorithm 5. - lfsr : [inf] - lfsr = [ p!0 | p <- ps ] - where - /* powers of x modulo m */ - ps = [0x01] # [ pmod (pmult p 0b10) m | p <- ps ] - m = <| x^^8 + x^^6 + x^^5 + x^^4 + 1 |> + Round : State -> [8] -> State + Round A ir = ι (χ (π (ρ (θ A)))) ir /** * See https://keccak.team/files/Keccak-reference-3.0.pdf, Section 1.2 From 01039acbac4d6d50933b1ea7bff4d08117cd382d Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Wed, 18 Sep 2024 08:58:07 -0400 Subject: [PATCH 6/8] sha3: clean up + docs on Keccak-f #138 --- Primitive/Keyless/Hash/keccak.cry | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/Primitive/Keyless/Hash/keccak.cry b/Primitive/Keyless/Hash/keccak.cry index 1f6e766d..f497f843 100644 --- a/Primitive/Keyless/Hash/keccak.cry +++ b/Primitive/Keyless/Hash/keccak.cry @@ -274,23 +274,28 @@ private /** * Keccak-f family of permutations. * + * This is implemented as defined in Section 3.4, but while `Keccak-p` isn't + * explicitly implemented, we "expanded" the `Keccak-p` implementation + * according to the parameters given in the definition of `Keccak-f`. + * Specifically, note the range of `ir`. + * + * The number of rounds is a parameter to this functor and not passed + * explicitly here. + * * [FIPS-202] Section 3.4. */ Keccak_f : [b] -> [b] Keccak_f S = S' where + // The round transformation is defined in [FIPS-202] Section 3.3. + Rnd A ir = ι (χ (π (ρ (θ A)))) ir + // Step 1. A0 = unflatten S - rounds = [A0] # [ Round A ir | A <- rounds | ir <- [0..nr - 1]] + // Step 2. + rounds = [A0] # [ Rnd A ir | A <- rounds | ir <- [0..nr - 1]] + // Step 3. S' = flatten (rounds ! 0) - - /** - * The round function for `Keccak-p`. Denoted `Rnd` in the spec. - * [FIPS-202] Section 3.3. - */ - Round : State -> [8] -> State - Round A ir = ι (χ (π (ρ (θ A)))) ir - /** * See https://keccak.team/files/Keccak-reference-3.0.pdf, Section 1.2 * ```repl From 2351749d32ff726b1735d2677b7bde2380792571 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Wed, 18 Sep 2024 09:30:37 -0400 Subject: [PATCH 7/8] sha3: add hardcoded round constants #138 --- Primitive/Keyless/Hash/keccak.cry | 58 ++++++++++++++++++++++--------- 1 file changed, 42 insertions(+), 16 deletions(-) diff --git a/Primitive/Keyless/Hash/keccak.cry b/Primitive/Keyless/Hash/keccak.cry index f497f843..dc9c1e77 100644 --- a/Primitive/Keyless/Hash/keccak.cry +++ b/Primitive/Keyless/Hash/keccak.cry @@ -208,22 +208,48 @@ private * [FIPS-202] Section 3.2.5, Algorithm 5. */ rc : [8] -> Bit - rc t = if t % 255 == 0 then 1 // Step 1. - else Rs @ (t % 255) @0 // Step 4. - where - // Step 2 - 3. - Rs = [0b10000000] # [lfsr R | R <- Rs ] + rc t = if (t % 255) == 0 then 1 // Step 1. + else Rs @ (t % 255) @0 // Step 4. + where + // Step 2 - 3. + Rs = [0b10000000] # [lfsr R | R <- Rs ] + // Step 3. Linear feedback shift register. + // The truncation in step f is done manually in the return value. + lfsr : [8] -> [8] + lfsr Rin = [R0, R@1, R@2, R@3, R4, R5, R6, R@7] + where + R = 0b0 # Rin + R0 = R@0 ^ R@8 + R4 = R@4 ^ R@8 + R5 = R@5 ^ R@8 + R6 = R@6 ^ R@8 + + /** + * Hardcode the round constant values. + * + * Since the `rc` function doesn't depend on any of the functor parameters, + * this hardcoded value is correct for all instantiations. + * We computed the value `constants` with: + * ``` + * [rc i | i <- [0..255]] + * ``` + * + * Equivalent to [FIPS-202] Section 3.2.5, Algorithm 5. + */ + rc_hardcoded : [8] -> Bit + rc_hardcoded t = constants @ t where + constants = join [ + 0x80b1e87f90a7d57062b32fde6ee54a25, + 0xa339e361175edf0d35b504ec9303a471 + ] - // Step 3. Linear feedback shift register. - // The truncation in step f is done manually in the return value. - lfsr : [8] -> [8] - lfsr Rin = [R0, R@1, R@2, R@3, R4, R5, R6, R@7] - where - R = 0b0 # Rin - R0 = R@0 ^ R@8 - R4 = R@4 ^ R@8 - R5 = R@5 ^ R@8 - R6 = R@6 ^ R@8 + /** + * Prove that the hardcoded round constants are correct. + * ```repl + * :prove round_constants_correctly_hardcoded + * ``` + */ + property round_constants_correctly_hardcoded t = rc_hardcoded t == rc t /** * One of the step mappings that's part of a round of Keccak-p. @@ -241,7 +267,7 @@ private // Step 3. 0 is the identity for XOR, so we iteratively set the // `2^j-1`th element by XORing the previously-set bits of RC with the // correct value at the desired index. - RCs = [RC0] # [RC' ^ (zext`{w} [rc (j + 7 * ir)] << (2^^j - 1)) + RCs = [RC0] # [RC' ^ (zext`{w} [rc_hardcoded (j + 7 * ir)] << (2^^j - 1)) | RC' <- RCs | j <- [0..ell] ] RC = (RCs ! 0) : [w] From a44273c00af7f47e6d7ab71886303a473fffd0d1 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Wed, 18 Sep 2024 10:28:51 -0400 Subject: [PATCH 8/8] sha3: add hardcoded rho function #138 --- Primitive/Keyless/Hash/keccak.cry | 47 +++++++++++++++++++++++++++++-- 1 file changed, 45 insertions(+), 2 deletions(-) diff --git a/Primitive/Keyless/Hash/keccak.cry b/Primitive/Keyless/Hash/keccak.cry index dc9c1e77..8163cd6a 100644 --- a/Primitive/Keyless/Hash/keccak.cry +++ b/Primitive/Keyless/Hash/keccak.cry @@ -174,6 +174,47 @@ private | y <- [0..4]] | x <- [0..4]] + /** + * Optimized and hard-coded version of `ρ`. + * + * This optimizes the hard-codable parts of `ρ` in the following ways: + * - Pre-computes the offsets `(t+1)*(t+2) / 2` + * - Pre-computes the corresponding sequence of lane indexes (e.g. the + * series defined by `(y, (2x + 3y) % 5))` + * - Re-orders the offsets and the lane indexes to be in the same order + * that we get if we iterate over the lanes generated by `join A` (e.g. + * (0,0), (0,1), (0,2), ...) + * - Maps directly over A, rotating each lane by the expected offset, + * instead of iteratively updating the lanes + * + * This provides a 2x speedup. + * + * Equivalent to [FIPS-202] Section 3.2.2, Algorithm 2. + */ + ρ_hardcoded : State -> State + ρ_hardcoded A = A' where + A' = groupBy [ a <<< offset | a <- join A | offset <- t_offsets] + + // This is technically equivalent to Table 2, but we index in the + // "normal" way e.g. the top-left corner is (0, 0) and the bottom-right + // is (4, 4), unlike the the table. + // We also write these in hex instead of base-10. + t_offsets = [ + 0x000, 0x024, 0x003, 0x069, 0x0d2, + 0x001, 0x12c, 0x00a, 0x02d, 0x042, + 0x0be, 0x006, 0x0ab, 0x00f, 0x0fd, + 0x01c, 0x037, 0x099, 0x015, 0x078, + 0x05b, 0x114, 0x0e7, 0x088, 0x04e + ] + + /** + * Prove that the hardcoded version of `ρ` is correct. + * ```repl + * :prove hardcoded_rho_is_correct + * ``` + */ + property hardcoded_rho_is_correct A = ρ A == ρ_hardcoded A + /** * One of the step mappings that's part of a round of Keccak-p. * @@ -230,10 +271,12 @@ private * Since the `rc` function doesn't depend on any of the functor parameters, * this hardcoded value is correct for all instantiations. * We computed the value `constants` with: - * ``` + * ```cryptol * [rc i | i <- [0..255]] * ``` * + * This provides a 4x speedup. + * * Equivalent to [FIPS-202] Section 3.2.5, Algorithm 5. */ rc_hardcoded : [8] -> Bit @@ -314,7 +357,7 @@ private Keccak_f S = S' where // The round transformation is defined in [FIPS-202] Section 3.3. - Rnd A ir = ι (χ (π (ρ (θ A)))) ir + Rnd A ir = ι (χ (π (ρ_hardcoded (θ A)))) ir // Step 1. A0 = unflatten S // Step 2.