1	# Generated by tools/generators/hash_gen.py; do not edit by hand.
2	import Base
3	import ./sha/state.bend as S256
4	import ./sha/core.bend as C256
5	import ./sha/sha256.bend as SHA256
6	import ./sha512/types.bend as T512
7	import ./sha512/core.bend as C512
8	import ./keccak/types.bend as TK
9	import ./keccak/permutation.bend as P
10	import ./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.
29	type Sha256State is Data:
30	  St256{s: S256.State, buf: List<&2, U32>}
31	
32	type Sha512State is Data:
33	  St512{s: T512.State, buf: List<&2, U32>}
34	
35	type Sha3State is Data:
36	  St3{s: TK.State, buf: List<&2, U32>}
37	
38	type 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.
46	def sha256(bytes: List<&2, U32>) -> List<&2, U32>:
47	  SHA256.sha256_bytes(bytes)
48	
49	# SHA-512 (FIPS 180-4), 64 bytes.
50	def sha512(bytes: List<&2, U32>) -> List<&2, U32>:
51	  C512.sha512(bytes)
52	
53	# SHA3-256 (FIPS 202), 32 bytes.
54	def 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.
61	type 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	
65	def 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	
68	def 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	
75	def 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	
82	def 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	
89	def 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	
96	def 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	
103	def 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	
110	def 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	
117	def 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	
124	def 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	
131	def 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	
138	def 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	
145	def 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	
152	def 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	
159	def 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	
166	def 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	
173	def 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.
184	def 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	
193	def 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	
199	def 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.
208	type 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	
212	def 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	
215	def 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	
222	def 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	
229	def 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	
236	def 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	
243	def 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	
250	def 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	
257	def 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	
264	def 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	
271	def 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	
278	def 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	
285	def 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	
292	def 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	
299	def 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	
306	def 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	
313	def 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	
320	def 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.
331	def 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	
340	def 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	
346	def 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.
355	type 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	
359	def 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	
362	def 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	
369	def 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	
376	def 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	
383	def 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	
390	def 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	
397	def 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	
404	def 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	
411	def 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	
418	def 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	
425	def 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	
432	def 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	
439	def 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	
446	def 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	
453	def 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	
460	def 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	
467	def 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	
474	def 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.
485	def 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	
494	def 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	
500	def 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	
507	def new_sha256() -> Hasher:
508	  Sha256H{St256{C256.initial(), Nil{}}, 0n}
509	
510	def new_sha512() -> Hasher:
511	  Sha512H{St512{C512.initial(), Nil{}}, 0n}
512	
513	def new_sha3_256() -> Hasher:
514	  Sha3H{St3{C3.zero(), Nil{}}, 0n}
515	
516	def 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	
525	def 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	
532	def update_all(h: Hasher, chunks: List<&2, List<&2, U32>>) -> Hasher:
533	  fold(chunks, h)
534	
535	def 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)