src/crypto/sha3/core.bend

bend-collections-laws-crypto@1.0.0.0 · 71 lines · 12 definitions

1# Generated by tools/generators/sha3_gen.py; do not edit by hand.
2import Base
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as T
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/lane.bend as L
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/permutation.bend as P
6
7# SHA3-256 (FIPS 202) on byte lists, on the Keccak-f[1600] of
8# src/crypto/keccak/permutation.bend (two rounds per step, proved equal to
9# FIPS 202's permutation in proofs/crypto/keccak/permutation.bend). The
10# message is padded (0x06 .. 0x80), read as little-endian lanes, and absorbed
11# 17 lanes (136 bytes) at a time; the digest is the first four lanes.
12# Proved equal to spec/crypto/sha3.bend in proofs/crypto/sha3/.
13
14def pack(a: U32, b: U32, c: U32, d: U32) -> U32:
15  U32.or(U32.or(U32.or(U32.and(a, 255), U32.shln(U32.and(b, 255), 8n)),
16    U32.shln(U32.and(c, 255), 16n)), U32.shln(U32.and(d, 255), 24n))
17
18def lanes(bytes: List<&2, U32>) -> List<&2, T.Lane>:
19  match bytes:
20    case a <> b <> c <> d <> e <> f <> g <> h <> rest:
21      T.W{pack(a, b, c, d), pack(e, f, g, h)} <> lanes(rest)
22    case _:
23      Nil{}
24
25# 0x06, zeros, 0x80 up to the end of the block (0x86 when one byte is left).
26def tail(q: Nat) -> List<&2, U32>:
27  match q:
28    case 0n:
29      Nil{}
30    case 1n:
31      [134]
32    case 2n+k:
33      6 <> List.append(&2, U32, List.replicate(U32, k, 0), [128])
34
35def suffix(+n: Nat) -> List<&2, U32>:
36  tail(Nat.sub(136n, Nat.mod(n, 136n)))
37
38def zero() -> T.State:
39  T.S{T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}, T.W{0, 0}}
40
41# XOR one block into the leading 17 lanes.
42def inject(s: T.State, l0: T.Lane, l1: T.Lane, l2: T.Lane, l3: T.Lane, l4: T.Lane, l5: T.Lane, l6: T.Lane, l7: T.Lane, l8: T.Lane, l9: T.Lane, l10: T.Lane, l11: T.Lane, l12: T.Lane, l13: T.Lane, l14: T.Lane, l15: T.Lane, l16: T.Lane) -> T.State:
43  match s:
44    case T.S{a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24}:
45      T.S{L.xor(a0, l0), L.xor(a1, l1), L.xor(a2, l2), L.xor(a3, l3), L.xor(a4, l4), L.xor(a5, l5), L.xor(a6, l6), L.xor(a7, l7), L.xor(a8, l8), L.xor(a9, l9), L.xor(a10, l10), L.xor(a11, l11), L.xor(a12, l12), L.xor(a13, l13), L.xor(a14, l14), L.xor(a15, l15), L.xor(a16, l16), a17, a18, a19, a20, a21, a22, a23, a24}
46
47# Absorb every whole block of 17 lanes with the given round count (24).
48def absorb(ls: List<&2, T.Lane>, +rounds: Nat, s: T.State) -> T.State:
49  match ls:
50    case l0 <> l1 <> l2 <> l3 <> l4 <> l5 <> l6 <> l7 <> l8 <> l9 <> l10 <> l11 <> l12 <> l13 <> l14 <> l15 <> l16 <> rest:
51      absorb(rest, rounds, P.rounds(rounds, 0n, inject(s, l0, l1, l2, l3, l4, l5, l6, l7, l8, l9, l10, l11, l12, l13, l14, l15, l16)))
52    case _:
53      s
54
55def le_bytes(+x: U32, tail: List<&2, U32>) -> List<&2, U32>:
56  U32.and(x, 255) <> U32.and(U32.shrn(x, 8n), 255) <> U32.and(U32.shrn(x, 16n), 255) <> U32.shrn(x, 24n) <> tail
57
58# The 32-byte digest: lanes 0..3, little-endian.
59def digest_bytes(s: T.State) -> List<&2, U32>:
60  match s:
61    case T.S{T.W{l0, h0}, T.W{l1, h1}, T.W{l2, h2}, T.W{l3, h3}, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24}:
62      le_bytes(l0, le_bytes(h0, le_bytes(l1, le_bytes(h1, le_bytes(l2, le_bytes(h2, le_bytes(l3, le_bytes(h3, Nil{}))))))))
63
64def hash_padded(bytes: List<&2, U32>, +rounds: Nat) -> List<&2, U32>:
65  digest_bytes(absorb(lanes(bytes), rounds, zero()))
66
67def keccak(+bytes: List<&2, U32>, +rounds: Nat) -> List<&2, U32>:
68  hash_padded(List.append(&2, U32, bytes, suffix(List.length(&2, U32, bytes))), rounds)
69
70def sha3_256(bytes: List<&2, U32>) -> List<&2, U32>:
71  keccak(bytes, 24n)