src/crypto/hash.bend

bend-collections-laws-crypto@1.0.0.0 · 542 lines · 78 definitions

1# Generated by tools/generators/hash_gen.py; do not edit by hand.
2import Base
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as S256
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend as C256
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/sha256.bend as SHA256
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T512
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend as C512
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as TK
9import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/permutation.bend as P
10import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha3/core.bend as C3
11
12# Hash functions: one-shot and incremental.
13#
14#   sha256(bytes), sha512(bytes), sha3_256(bytes)       the digest (32, 64, 32 bytes)
15#   new_sha256(), new_sha512(), new_sha3_256()          an empty Hasher
16#   update(h, bytes)                                    h with bytes appended
17#   update_all(h, chunks)                               update with each chunk in turn
18#   digest(h)                                           the digest of everything appended
19#
20# Bytes are U32 values, each < 256 (List<&2, U32>). A Hasher keeps the chaining
21# state, the bytes of the unfinished block (fewer than one block) and the total
22# length; update compresses every block it completes, and digest pads the
23# buffered tail with the total length. Proved (proofs/crypto/hash/laws.bend):
24# each one-shot function equals its executable specification, and for every
25# list of chunks, digest(update_all(new_X(), chunks)) == X(concat(chunks)).
26# Hashers are values: update returns a new one, the old one is unchanged.
27
28# A chaining state and the buffered bytes of the unfinished block.
29type Sha256State is Data:
30  St256{s: S256.State, buf: List<&2, U32>}
31
32type Sha512State is Data:
33  St512{s: T512.State, buf: List<&2, U32>}
34
35type Sha3State is Data:
36  St3{s: TK.State, buf: List<&2, U32>}
37
38type Hasher is Data:
39  Sha256H{st: Sha256State, len: Nat}
40  Sha512H{st: Sha512State, len: Nat}
41  Sha3H{st: Sha3State, len: Nat}
42
43# ---------------------------------------------------------------- one-shot
44
45# SHA-256 (FIPS 180-4), 32 bytes.
46def sha256(bytes: List<&2, U32>) -> List<&2, U32>:
47  SHA256.sha256_bytes(bytes)
48
49# SHA-512 (FIPS 180-4), 64 bytes.
50def sha512(bytes: List<&2, U32>) -> List<&2, U32>:
51  C512.sha512(bytes)
52
53# SHA3-256 (FIPS 202), 32 bytes.
54def sha3_256(bytes: List<&2, U32>) -> List<&2, U32>:
55  C3.sha3_256(bytes)
56
57# ---------------------------------------------------------------- SHA-256 (FIPS 180-4)
58
59# One block read 4 bytes at a time into its 16 words, or Short when
60# fewer than 64 bytes are left.
61type Read256 is Data:
62  Blk256{w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, rest: List<&2, U32>}
63  Short256{}
64
65def read256_16(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32) -> Read256:
66  Blk256{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, bytes}
67
68def read256_15(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32) -> Read256:
69  match bytes:
70    case b0 <> b1 <> b2 <> b3 <> rest:
71      read256_16(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, C256.pack(b0, b1, b2, b3))
72    case _:
73      Short256{}
74
75def read256_14(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32) -> Read256:
76  match bytes:
77    case b0 <> b1 <> b2 <> b3 <> rest:
78      read256_15(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, C256.pack(b0, b1, b2, b3))
79    case _:
80      Short256{}
81
82def read256_13(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32) -> Read256:
83  match bytes:
84    case b0 <> b1 <> b2 <> b3 <> rest:
85      read256_14(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, C256.pack(b0, b1, b2, b3))
86    case _:
87      Short256{}
88
89def read256_12(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32) -> Read256:
90  match bytes:
91    case b0 <> b1 <> b2 <> b3 <> rest:
92      read256_13(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, C256.pack(b0, b1, b2, b3))
93    case _:
94      Short256{}
95
96def read256_11(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32) -> Read256:
97  match bytes:
98    case b0 <> b1 <> b2 <> b3 <> rest:
99      read256_12(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, C256.pack(b0, b1, b2, b3))
100    case _:
101      Short256{}
102
103def read256_10(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32) -> Read256:
104  match bytes:
105    case b0 <> b1 <> b2 <> b3 <> rest:
106      read256_11(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, C256.pack(b0, b1, b2, b3))
107    case _:
108      Short256{}
109
110def read256_9(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32) -> Read256:
111  match bytes:
112    case b0 <> b1 <> b2 <> b3 <> rest:
113      read256_10(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, C256.pack(b0, b1, b2, b3))
114    case _:
115      Short256{}
116
117def read256_8(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32) -> Read256:
118  match bytes:
119    case b0 <> b1 <> b2 <> b3 <> rest:
120      read256_9(rest, w0, w1, w2, w3, w4, w5, w6, w7, C256.pack(b0, b1, b2, b3))
121    case _:
122      Short256{}
123
124def read256_7(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32) -> Read256:
125  match bytes:
126    case b0 <> b1 <> b2 <> b3 <> rest:
127      read256_8(rest, w0, w1, w2, w3, w4, w5, w6, C256.pack(b0, b1, b2, b3))
128    case _:
129      Short256{}
130
131def read256_6(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32) -> Read256:
132  match bytes:
133    case b0 <> b1 <> b2 <> b3 <> rest:
134      read256_7(rest, w0, w1, w2, w3, w4, w5, C256.pack(b0, b1, b2, b3))
135    case _:
136      Short256{}
137
138def read256_5(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32) -> Read256:
139  match bytes:
140    case b0 <> b1 <> b2 <> b3 <> rest:
141      read256_6(rest, w0, w1, w2, w3, w4, C256.pack(b0, b1, b2, b3))
142    case _:
143      Short256{}
144
145def read256_4(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32) -> Read256:
146  match bytes:
147    case b0 <> b1 <> b2 <> b3 <> rest:
148      read256_5(rest, w0, w1, w2, w3, C256.pack(b0, b1, b2, b3))
149    case _:
150      Short256{}
151
152def read256_3(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32) -> Read256:
153  match bytes:
154    case b0 <> b1 <> b2 <> b3 <> rest:
155      read256_4(rest, w0, w1, w2, C256.pack(b0, b1, b2, b3))
156    case _:
157      Short256{}
158
159def read256_2(bytes: List<&2, U32>, w0: U32, w1: U32) -> Read256:
160  match bytes:
161    case b0 <> b1 <> b2 <> b3 <> rest:
162      read256_3(rest, w0, w1, C256.pack(b0, b1, b2, b3))
163    case _:
164      Short256{}
165
166def read256_1(bytes: List<&2, U32>, w0: U32) -> Read256:
167  match bytes:
168    case b0 <> b1 <> b2 <> b3 <> rest:
169      read256_2(rest, w0, C256.pack(b0, b1, b2, b3))
170    case _:
171      Short256{}
172
173def read256_0(bytes: List<&2, U32>) -> Read256:
174  match bytes:
175    case b0 <> b1 <> b2 <> b3 <> rest:
176      read256_1(rest, C256.pack(b0, b1, b2, b3))
177    case _:
178      Short256{}
179
180# Compress every whole block (fuel bounds the count: any fuel >= the number of
181# blocks reads them all; fewer leaves the rest buffered, still correct). The
182# chaining state and the unread bytes; orig is the list the read r started at.
183# q is the algorithm's round parameter (48n), kept a variable for the proofs.
184def absorb256(fuel: Nat, r: Read256, orig: List<&2, U32>, +q: Nat, s: S256.State) -> Sha256State:
185  match fuel r:
186    case 0n _:
187      St256{s, orig}
188    case 1n+p Short256{}:
189      St256{s, orig}
190    case 1n+p Blk256{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, +rest}:
191      absorb256(p, read256_0(rest), rest, q, C256.fips_compress16(w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, q, s))
192
193def step256(st: Sha256State, xs: List<&2, U32>, +q: Nat) -> Sha256State:
194  match st:
195    case St256{s, buf}:
196      +bytes = List.append(&2, U32, buf, xs)
197      absorb256(List.length(&2, U32, bytes), read256_0(bytes), bytes, q, s)
198
199def finish256(st: Sha256State, +len: Nat, +q: Nat) -> List<&2, U32>:
200  match st:
201    case St256{s, buf}:
202      SHA256.digest_bytes(C256.digest(C256.block_bytes(List.append(&2, U32, buf, C256.suffix(len)), q, C256.round_constants(), s)))
203
204# ---------------------------------------------------------------- SHA-512 (FIPS 180-4)
205
206# One block read 8 bytes at a time into its 16 words, or Short when
207# fewer than 128 bytes are left.
208type Read512 is Data:
209  Blk512{w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane, w13: T512.Lane, w14: T512.Lane, w15: T512.Lane, rest: List<&2, U32>}
210  Short512{}
211
212def read512_16(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane, w13: T512.Lane, w14: T512.Lane, w15: T512.Lane) -> Read512:
213  Blk512{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, bytes}
214
215def read512_15(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane, w13: T512.Lane, w14: T512.Lane) -> Read512:
216  match bytes:
217    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
218      read512_16(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
219    case _:
220      Short512{}
221
222def read512_14(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane, w13: T512.Lane) -> Read512:
223  match bytes:
224    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
225      read512_15(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
226    case _:
227      Short512{}
228
229def read512_13(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane) -> Read512:
230  match bytes:
231    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
232      read512_14(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
233    case _:
234      Short512{}
235
236def read512_12(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane) -> Read512:
237  match bytes:
238    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
239      read512_13(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
240    case _:
241      Short512{}
242
243def read512_11(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane) -> Read512:
244  match bytes:
245    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
246      read512_12(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
247    case _:
248      Short512{}
249
250def read512_10(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane) -> Read512:
251  match bytes:
252    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
253      read512_11(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
254    case _:
255      Short512{}
256
257def read512_9(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane) -> Read512:
258  match bytes:
259    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
260      read512_10(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
261    case _:
262      Short512{}
263
264def read512_8(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane) -> Read512:
265  match bytes:
266    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
267      read512_9(rest, w0, w1, w2, w3, w4, w5, w6, w7, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
268    case _:
269      Short512{}
270
271def read512_7(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane) -> Read512:
272  match bytes:
273    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
274      read512_8(rest, w0, w1, w2, w3, w4, w5, w6, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
275    case _:
276      Short512{}
277
278def read512_6(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane) -> Read512:
279  match bytes:
280    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
281      read512_7(rest, w0, w1, w2, w3, w4, w5, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
282    case _:
283      Short512{}
284
285def read512_5(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane) -> Read512:
286  match bytes:
287    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
288      read512_6(rest, w0, w1, w2, w3, w4, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
289    case _:
290      Short512{}
291
292def read512_4(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane) -> Read512:
293  match bytes:
294    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
295      read512_5(rest, w0, w1, w2, w3, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
296    case _:
297      Short512{}
298
299def read512_3(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane) -> Read512:
300  match bytes:
301    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
302      read512_4(rest, w0, w1, w2, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
303    case _:
304      Short512{}
305
306def read512_2(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane) -> Read512:
307  match bytes:
308    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
309      read512_3(rest, w0, w1, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
310    case _:
311      Short512{}
312
313def read512_1(bytes: List<&2, U32>, w0: T512.Lane) -> Read512:
314  match bytes:
315    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
316      read512_2(rest, w0, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
317    case _:
318      Short512{}
319
320def read512_0(bytes: List<&2, U32>) -> Read512:
321  match bytes:
322    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
323      read512_1(rest, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})
324    case _:
325      Short512{}
326
327# Compress every whole block (fuel bounds the count: any fuel >= the number of
328# blocks reads them all; fewer leaves the rest buffered, still correct). The
329# chaining state and the unread bytes; orig is the list the read r started at.
330# q is the algorithm's round parameter (64n), kept a variable for the proofs.
331def absorb512(fuel: Nat, r: Read512, orig: List<&2, U32>, +q: Nat, s: T512.State) -> Sha512State:
332  match fuel r:
333    case 0n _:
334      St512{s, orig}
335    case 1n+p Short512{}:
336      St512{s, orig}
337    case 1n+p Blk512{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, +rest}:
338      absorb512(p, read512_0(rest), rest, q, C512.compress16(w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, q, C512.round_constants(), s))
339
340def step512(st: Sha512State, xs: List<&2, U32>, +q: Nat) -> Sha512State:
341  match st:
342    case St512{s, buf}:
343      +bytes = List.append(&2, U32, buf, xs)
344      absorb512(List.length(&2, U32, bytes), read512_0(bytes), bytes, q, s)
345
346def finish512(st: Sha512State, +len: Nat, +q: Nat) -> List<&2, U32>:
347  match st:
348    case St512{s, buf}:
349      C512.digest_bytes(C512.blocks(C512.lanes(List.append(&2, U32, buf, C512.suffix(len))), q, C512.round_constants(), s))
350
351# ---------------------------------------------------------------- SHA3-256 (FIPS 202)
352
353# One block read 8 bytes at a time into its 17 words, or Short when
354# fewer than 136 bytes are left.
355type Read3 is Data:
356  Blk3{w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane, w14: TK.Lane, w15: TK.Lane, w16: TK.Lane, rest: List<&2, U32>}
357  Short3{}
358
359def read3_17(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane, w14: TK.Lane, w15: TK.Lane, w16: TK.Lane) -> Read3:
360  Blk3{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, bytes}
361
362def read3_16(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane, w14: TK.Lane, w15: TK.Lane) -> Read3:
363  match bytes:
364    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
365      read3_17(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
366    case _:
367      Short3{}
368
369def read3_15(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane, w14: TK.Lane) -> Read3:
370  match bytes:
371    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
372      read3_16(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
373    case _:
374      Short3{}
375
376def read3_14(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane) -> Read3:
377  match bytes:
378    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
379      read3_15(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
380    case _:
381      Short3{}
382
383def read3_13(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane) -> Read3:
384  match bytes:
385    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
386      read3_14(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
387    case _:
388      Short3{}
389
390def read3_12(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane) -> Read3:
391  match bytes:
392    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
393      read3_13(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
394    case _:
395      Short3{}
396
397def read3_11(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane) -> Read3:
398  match bytes:
399    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
400      read3_12(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
401    case _:
402      Short3{}
403
404def read3_10(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane) -> Read3:
405  match bytes:
406    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
407      read3_11(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
408    case _:
409      Short3{}
410
411def read3_9(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane) -> Read3:
412  match bytes:
413    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
414      read3_10(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
415    case _:
416      Short3{}
417
418def read3_8(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane) -> Read3:
419  match bytes:
420    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
421      read3_9(rest, w0, w1, w2, w3, w4, w5, w6, w7, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
422    case _:
423      Short3{}
424
425def read3_7(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane) -> Read3:
426  match bytes:
427    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
428      read3_8(rest, w0, w1, w2, w3, w4, w5, w6, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
429    case _:
430      Short3{}
431
432def read3_6(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane) -> Read3:
433  match bytes:
434    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
435      read3_7(rest, w0, w1, w2, w3, w4, w5, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
436    case _:
437      Short3{}
438
439def read3_5(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane) -> Read3:
440  match bytes:
441    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
442      read3_6(rest, w0, w1, w2, w3, w4, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
443    case _:
444      Short3{}
445
446def read3_4(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane) -> Read3:
447  match bytes:
448    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
449      read3_5(rest, w0, w1, w2, w3, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
450    case _:
451      Short3{}
452
453def read3_3(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane) -> Read3:
454  match bytes:
455    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
456      read3_4(rest, w0, w1, w2, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
457    case _:
458      Short3{}
459
460def read3_2(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane) -> Read3:
461  match bytes:
462    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
463      read3_3(rest, w0, w1, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
464    case _:
465      Short3{}
466
467def read3_1(bytes: List<&2, U32>, w0: TK.Lane) -> Read3:
468  match bytes:
469    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
470      read3_2(rest, w0, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
471    case _:
472      Short3{}
473
474def read3_0(bytes: List<&2, U32>) -> Read3:
475  match bytes:
476    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
477      read3_1(rest, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})
478    case _:
479      Short3{}
480
481# Compress every whole block (fuel bounds the count: any fuel >= the number of
482# blocks reads them all; fewer leaves the rest buffered, still correct). The
483# chaining state and the unread bytes; orig is the list the read r started at.
484# q is the algorithm's round parameter (24n), kept a variable for the proofs.
485def absorb3(fuel: Nat, r: Read3, orig: List<&2, U32>, +q: Nat, s: TK.State) -> Sha3State:
486  match fuel r:
487    case 0n _:
488      St3{s, orig}
489    case 1n+p Short3{}:
490      St3{s, orig}
491    case 1n+p Blk3{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, +rest}:
492      absorb3(p, read3_0(rest), rest, q, P.rounds(q, 0n, C3.inject(s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16)))
493
494def step3(st: Sha3State, xs: List<&2, U32>, +q: Nat) -> Sha3State:
495  match st:
496    case St3{s, buf}:
497      +bytes = List.append(&2, U32, buf, xs)
498      absorb3(List.length(&2, U32, bytes), read3_0(bytes), bytes, q, s)
499
500def finish3(st: Sha3State, +len: Nat, +q: Nat) -> List<&2, U32>:
501  match st:
502    case St3{s, buf}:
503      C3.digest_bytes(C3.absorb(C3.lanes(List.append(&2, U32, buf, C3.suffix(len))), q, s))
504
505# ---------------------------------------------------------------- the Hasher
506
507def new_sha256() -> Hasher:
508  Sha256H{St256{C256.initial(), Nil{}}, 0n}
509
510def new_sha512() -> Hasher:
511  Sha512H{St512{C512.initial(), Nil{}}, 0n}
512
513def new_sha3_256() -> Hasher:
514  Sha3H{St3{C3.zero(), Nil{}}, 0n}
515
516def update(h: Hasher, +bytes: List<&2, U32>) -> Hasher:
517  match h:
518    case Sha256H{st, len}:
519      Sha256H{step256(st, bytes, 48n), Nat.add(len, List.length(&2, U32, bytes))}
520    case Sha512H{st, len}:
521      Sha512H{step512(st, bytes, 64n), Nat.add(len, List.length(&2, U32, bytes))}
522    case Sha3H{st, len}:
523      Sha3H{step3(st, bytes, 24n), Nat.add(len, List.length(&2, U32, bytes))}
524
525def fold(chunks: List<&2, List<&2, U32>>, h: Hasher) -> Hasher:
526  match chunks:
527    case Nil{}:
528      h
529    case c <> rest:
530      fold(rest, update(h, c))
531
532def update_all(h: Hasher, chunks: List<&2, List<&2, U32>>) -> Hasher:
533  fold(chunks, h)
534
535def digest(h: Hasher) -> List<&2, U32>:
536  match h:
537    case Sha256H{st, len}:
538      finish256(st, len, 48n)
539    case Sha512H{st, len}:
540      finish512(st, len, 64n)
541    case Sha3H{st, len}:
542      finish3(st, len, 24n)