1	import Base
2	import ../../lib/common.bend as C
3	import ../../../src/crypto/blake/blake2b/types.bend as T
4	import ../../../src/crypto/argon2/types.bend as A
5	import ../blake/blake2b.bend as B
6	import ./blamka.bend as G
7	
8	# Argon2id, version 0x13 (RFC 9106), as an executable specification.
9	#
10	# Bytes are U32 values below 256, byte strings lists of them. The memory is
11	# a list of m' blocks (spec/crypto/argon2/blamka.bend's 128-lane blocks),
12	# B[i][j] being element i * q + j; indices are natural numbers and the
13	# reference-index arithmetic of section 3.4.1.2 is done on Nat. BLAKE2b is
14	# the RFC 7693 specification of spec/crypto/blake/blake2b.bend with the
15	# digest length in the parameter block; G is spec/crypto/argon2/blamka.bend's.
16	# The lanes are computed one after the other within a slice (every segment
17	# only reads blocks of finished segments of other lanes, so this is the
18	# RFC's parallel schedule, sequentially, as in the reference implementation).
19	#
20	# It shares nothing with src/crypto/argon2 but the record types of a lane, a
21	# state and a block.
22	
23	def cat(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
24	  List.append(&2, U32, xs, ys)
25	
26	def len(xs: List<&2, U32>) -> Nat:
27	  List.length(&2, U32, xs)
28	
29	# ---------------------------------------------------------------- bytes
30	
31	# LE32(n): the four little-endian bytes of n < 2^32.
32	def le32(+n: Nat) -> List<&2, U32>:
33	  [U32.from_nat(Nat.mod(n, 256n)), U32.from_nat(Nat.mod(Nat.div(n, 256n), 256n)), U32.from_nat(Nat.mod(Nat.div(n, 65536n), 256n)), U32.from_nat(Nat.div(n, 16777216n))]
34	
35	# The little-endian word of four bytes.
36	def word(+b0: U32, +b1: U32, +b2: U32, +b3: U32) -> U32:
37	  U32.or(U32.or(b0, U32.shln(b1, 8n)), U32.or(U32.shln(b2, 16n), U32.shln(b3, 24n)))
38	
39	# Bytes as little-endian words, the last one zero-padded.
40	def words(bs: List<&2, U32>) -> List<&2, U32>:
41	  match bs:
42	    case Nil{}:
43	      Nil{}
44	    case b0 <> Nil{}:
45	      [word(b0, 0, 0, 0)]
46	    case b0 <> b1 <> Nil{}:
47	      [word(b0, b1, 0, 0)]
48	    case b0 <> b1 <> b2 <> Nil{}:
49	      [word(b0, b1, b2, 0)]
50	    case b0 <> b1 <> b2 <> b3 <> rest:
51	      word(b0, b1, b2, b3) <> words(rest)
52	
53	def le(+w: U32) -> List<&2, U32>:
54	  [U32.and(w, 255), U32.and(U32.shrn(w, 8n), 255), U32.and(U32.shrn(w, 16n), 255), U32.shrn(w, 24n)]
55	
56	def lane_bytes(l: T.Lane) -> List<&2, U32>:
57	  match l:
58	    case T.W{lo, hi}:
59	      List.append(&2, U32, le(lo), le(hi))
60	
61	# ---------------------------------------------------------------- BLAKE2b with digest length nn
62	
63	def fill(ws: List<&2, U32>, +i: U32, a: Array<U32>) -> Array<U32>:
64	  match ws:
65	    case Nil{}:
66	      a
67	    case w <> rest:
68	      fill(rest, U32.inc(i), Array.set(U32, a, i, w))
69	
70	def pw(k: Nat) -> Nat:
71	  match k:
72	    case 0n:
73	      1n
74	    case 1n+p:
75	      Nat.double(pw(p))
76	
77	def depth_go(fuel: Nat, +n: Nat, +d: Nat, done: Bool) -> Nat:
78	  match fuel done:
79	    case _ True{}:
80	      d
81	    case 0n False{}:
82	      d
83	    case 1n+f False{}:
84	      depth_go(f, n, 1n+d, Nat.is_le(n, pw(1n+d)))
85	
86	# The bytes packed in the BLAKE2b specification's input array.
87	def pack(bs: List<&2, U32>) -> Array<U32>:
88	  +ws = words(bs)
89	  +n = List.length(&2, U32, ws)
90	  fill(ws, 0, Array.new(U32, depth_go(32n, n, 0n, Nat.is_le(n, 1n)), 0))
91	
92	# RFC 7693 section 2.5: h[0] ^= 0x01010000 ^ (kk << 8) ^ nn with kk = 0.
93	def initial(+nn: U32) -> T.Chain:
94	  T.H{B.xor(B.iv(0n), T.W{U32.or(16842752, nn), 0}), B.iv(1n), B.iv(2n), B.iv(3n), B.iv(4n), B.iv(5n), B.iv(6n), B.iv(7n)}
95	
96	def chain_bytes(h: T.Chain) -> List<&2, U32>:
97	  match h:
98	    case T.H{h0, h1, h2, h3, h4, h5, h6, h7}:
99	      List.concat(&2, U32, [lane_bytes(h0), lane_bytes(h1), lane_bytes(h2), lane_bytes(h3), lane_bytes(h4), lane_bytes(h5), lane_bytes(h6), lane_bytes(h7)])
100	
101	# H^nn(bs): BLAKE2b with an nn-byte digest, 1 <= nn <= 64: the first nn bytes
102	# of h after the dd = max(1, ceil(ll / 128)) blocks.
103	def hash(+nn: Nat, +bs: List<&2, U32>) -> List<&2, U32>:
104	  +ll = List.length(&2, U32, bs)
105	  +n = Nat.div(Nat.sub(ll, 1n), 128n)
106	  List.take(&2, U32, chain_bytes(B.blocks(n, 0, Nat.sub(ll, Nat.mul(n, 128n)), T.C{0, 0, 0, 0}, (pack(bs), initial(U32.from_nat(nn))))), nn)
107	
108	# ---------------------------------------------------------------- H0 and H' (sections 3.2 and 3.3)
109	
110	# r = ceil(T / 32) - 2; V1 = H^64(LE32(T) || A), V_{i+1} = H^64(V_i),
111	# V_{r+1} = H^{T - 32r}(V_r); the output is W1 || .. || Wr || V_{r+1}, Wi
112	# the first 32 bytes of Vi.
113	# (V_i is a 64-byte digest, never empty; it is inspected first so that proofs
114	# keep the chain of hashes folded.)
115	def hp_go(n: Nat, v: List<&2, U32>, +last: Nat) -> List<&2, U32>:
116	  match n v:
117	    case _ Nil{}:
118	      Nil{}
119	    case 0n +x <> +r:
120	      cat(List.take(&2, U32, x <> r, 32n), hash(last, x <> r))
121	    case 1n+p +x <> +r:
122	      cat(List.take(&2, U32, x <> r, 32n), hp_go(p, hash(64n, x <> r), last))
123	
124	def hp_pick(+tl: Nat, +x: List<&2, U32>, short: Bool) -> List<&2, U32>:
125	  match short:
126	    case True{}:
127	      hash(tl, x)
128	    case False{}:
129	      +r = Nat.sub(Nat.div(Nat.add(tl, 31n), 32n), 2n)
130	      hp_go(Nat.sub(r, 1n), hash(64n, x), Nat.sub(tl, Nat.mul(32n, r)))
131	
132	# H'^T(a) = H^T(LE32(T) || a) if T <= 64, else as hp_go.
133	def hprime(+tl: Nat, a: List<&2, U32>) -> List<&2, U32>:
134	  hp_pick(tl, cat(le32(tl), a), Nat.is_le(tl, 64n))
135	
136	# H0 = H^64(LE32(p) || LE32(T) || LE32(m) || LE32(t) || LE32(v) || LE32(y) ||
137	# LE32(|P|) || P || LE32(|S|) || S || LE32(|K|) || K || LE32(|X|) || X), with
138	# v = 0x13 and y = 2 (Argon2id).
139	def h0(+p: Nat, +tl: Nat, +m: Nat, +t: Nat, +pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>) -> List<&2, U32>:
140	  hash(64n, cat(le32(p), cat(le32(tl), cat(le32(m), cat(le32(t), cat(le32(19n), cat(le32(2n), cat(le32(len(pw)), cat(pw, cat(le32(len(salt)), cat(salt, cat(le32(len(key)), cat(key, cat(le32(len(ad)), ad))))))))))))))
141	
142	# ---------------------------------------------------------------- blocks and bytes
143	
144	# 32 words (a row) as sixteen lanes, and the words left.
145	def row_of(ws: List<&2, U32>) -> T.State & List<&2, U32>:
146	  match ws:
147	    case w0 <> w1 <> w2 <> w3 <> w4 <> w5 <> w6 <> w7 <> w8 <> w9 <> w10 <> w11 <> w12 <> w13 <> w14 <> w15 <> w16 <> w17 <> w18 <> w19 <> w20 <> w21 <> w22 <> w23 <> w24 <> w25 <> w26 <> w27 <> w28 <> w29 <> w30 <> w31 <> rest:
148	      (T.V{T.W{w0, w1}, T.W{w2, w3}, T.W{w4, w5}, T.W{w6, w7}, T.W{w8, w9}, T.W{w10, w11}, T.W{w12, w13}, T.W{w14, w15}, T.W{w16, w17}, T.W{w18, w19}, T.W{w20, w21}, T.W{w22, w23}, T.W{w24, w25}, T.W{w26, w27}, T.W{w28, w29}, T.W{w30, w31}}, rest)
149	    case _:
150	      (G.zero_state(), Nil{})
151	
152	def rows_of7(r0: T.State, r1: T.State, r2: T.State, r3: T.State, r4: T.State, r5: T.State, r6: T.State, p: T.State & List<&2, U32>) -> A.Block:
153	  (r7, ws) = p
154	  A.B{r0, r1, r2, r3, r4, r5, r6, r7}
155	
156	def rows_of6(r0: T.State, r1: T.State, r2: T.State, r3: T.State, r4: T.State, r5: T.State, p: T.State & List<&2, U32>) -> A.Block:
157	  (r6, ws) = p
158	  rows_of7(r0, r1, r2, r3, r4, r5, r6, row_of(ws))
159	
160	def rows_of5(r0: T.State, r1: T.State, r2: T.State, r3: T.State, r4: T.State, p: T.State & List<&2, U32>) -> A.Block:
161	  (r5, ws) = p
162	  rows_of6(r0, r1, r2, r3, r4, r5, row_of(ws))
163	
164	def rows_of4(r0: T.State, r1: T.State, r2: T.State, r3: T.State, p: T.State & List<&2, U32>) -> A.Block:
165	  (r4, ws) = p
166	  rows_of5(r0, r1, r2, r3, r4, row_of(ws))
167	
168	def rows_of3(r0: T.State, r1: T.State, r2: T.State, p: T.State & List<&2, U32>) -> A.Block:
169	  (r3, ws) = p
170	  rows_of4(r0, r1, r2, r3, row_of(ws))
171	
172	def rows_of2(r0: T.State, r1: T.State, p: T.State & List<&2, U32>) -> A.Block:
173	  (r2, ws) = p
174	  rows_of3(r0, r1, r2, row_of(ws))
175	
176	def rows_of1(r0: T.State, p: T.State & List<&2, U32>) -> A.Block:
177	  (r1, ws) = p
178	  rows_of2(r0, r1, row_of(ws))
179	
180	def rows_of0(p: T.State & List<&2, U32>) -> A.Block:
181	  (r0, ws) = p
182	  rows_of1(r0, row_of(ws))
183	
184	# The block of 1024 bytes: lane n is the little-endian 64-bit word of bytes 8n .. 8n + 7.
185	def block_of(bs: List<&2, U32>) -> A.Block:
186	  rows_of0(row_of(words(bs)))
187	
188	def state_bytes(v: T.State) -> List<&2, U32>:
189	  match v:
190	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}:
191	      List.concat(&2, U32, [lane_bytes(x0), lane_bytes(x1), lane_bytes(x2), lane_bytes(x3), lane_bytes(x4), lane_bytes(x5), lane_bytes(x6), lane_bytes(x7), lane_bytes(x8), lane_bytes(x9), lane_bytes(x10), lane_bytes(x11), lane_bytes(x12), lane_bytes(x13), lane_bytes(x14), lane_bytes(x15)])
192	
193	# The 1024 bytes of a block.
194	def block_bytes(b: A.Block) -> List<&2, U32>:
195	  match b:
196	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7}:
197	      List.concat(&2, U32, [state_bytes(r0), state_bytes(r1), state_bytes(r2), state_bytes(r3), state_bytes(r4), state_bytes(r5), state_bytes(r6), state_bytes(r7)])
198	
199	# ---------------------------------------------------------------- memory
200	
201	# B[i][j] of the memory is element i * q + j; a block out of range reads as zero.
202	def get(mem: List<&2, A.Block>, +b: Nat) -> A.Block:
203	  Maybe.default(&2, A.Block, C.nth(A.Block, mem, b), G.zero())
204	
205	def set(mem: List<&2, A.Block>, +b: Nat, v: A.Block) -> List<&2, A.Block>:
206	  C.update(A.Block, mem, b, v)
207	
208	# ---------------------------------------------------------------- indexing (section 3.4)
209	
210	def small(+x: Nat) -> T.Lane:
211	  T.W{U32.from_nat(x), 0}
212	
213	# Z = (r, l, s, m', t, y, i) as the first seven 64-bit lanes of a zero block.
214	def input_of(+r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +ctr: Nat) -> A.Block:
215	  G.put_lanes([0n, 1n, 2n, 3n, 4n, 5n, 6n], [small(r), small(l), small(s), small(mm), small(t), small(2n), small(ctr)], G.zero())
216	
217	# (r is inspected first, so that proofs keep an input block with a symbolic
218	# pass number folded instead of evaluating G on it.)
219	def input_block(r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +ctr: Nat) -> A.Block:
220	  match r:
221	    case 0n:
222	      input_of(0n, l, s, mm, t, ctr)
223	    case 1n+x:
224	      input_of(1n+x, l, s, mm, t, ctr)
225	
226	# The address block with counter ctr: G(ZERO, G(ZERO, Z)).
227	def addresses(+r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +ctr: Nat) -> A.Block:
228	  G.G(G.zero(), G.G(G.zero(), input_block(r, l, s, mm, t, ctr)))
229	
230	# In a data-independent segment a new address block is computed for the
231	# segment's first position and at every multiple of 128, with counter
232	# idx / 128 + 1 (the i-th address block has counter i).
233	def regen(need: Bool, addr: A.Block, +r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +idx: Nat) -> A.Block:
234	  match need:
235	    case True{}:
236	      addresses(r, l, s, mm, t, Nat.add(Nat.div(idx, 128n), 1n))
237	    case False{}:
238	      addr
239	
240	# |W|: in the first pass, the blocks of finished segments of the lane (all
241	# previous blocks of the segment too, when the reference lane is the current
242	# one); in later passes the last three segments of the lane, plus the current
243	# segment's previous blocks for the same lane; never the block just before
244	# the current one ("minus one" when the current index is the first of its
245	# segment and the lane is another one).
246	def area_base(r0: Bool, +s: Nat, +sl: Nat, +q: Nat) -> Nat:
247	  match r0:
248	    case True{}:
249	      Nat.mul(s, sl)
250	    case False{}:
251	      Nat.sub(q, sl)
252	
253	def area_other(+base: Nat, zero: Bool) -> Nat:
254	  match zero:
255	    case True{}:
256	      Nat.sub(base, 1n)
257	    case False{}:
258	      base
259	
260	def area(+base: Nat, +idx: Nat, same: Bool) -> Nat:
261	  match same:
262	    case True{}:
263	      Nat.sub(Nat.add(base, idx), 1n)
264	    case False{}:
265	      area_other(base, Nat.is_eq(idx, 0n))
266	
267	# x = J1^2 / 2^32; y = (|W| * x) / 2^32; zz = |W| - 1 - y.
268	def rel(+w: Nat, +j1: U32) -> Nat:
269	  +x = C.high(32n, Nat.mul(U32.to_nat(j1), U32.to_nat(j1)))
270	  Nat.sub(Nat.sub(w, 1n), C.high(32n, Nat.mul(w, x)))
271	
272	def start_last(+s: Nat, +sl: Nat, last: Bool) -> Nat:
273	  match last:
274	    case True{}:
275	      0n
276	    case False{}:
277	      Nat.mul(Nat.add(s, 1n), sl)
278	
279	# The reference area starts at 0 in the first pass, else at the next segment.
280	def start(r0: Bool, +s: Nat, +sl: Nat) -> Nat:
281	  match r0:
282	    case True{}:
283	      0n
284	    case False{}:
285	      start_last(s, sl, Nat.is_eq(s, 3n))
286	
287	# l = J2 mod p, except in the first slice of the first pass (the current lane).
288	def ref_lane(forced: Bool, +l: Nat, +j2: U32, +p: Nat) -> Nat:
289	  match forced:
290	    case True{}:
291	      l
292	    case False{}:
293	      Nat.mod(U32.to_nat(j2), p)
294	
295	# The previous block: B[l][j - 1], or B[l][q - 1] for j = 0.
296	def prev_index(+l: Nat, +q: Nat, +j: Nat, first: Bool) -> Nat:
297	  match first:
298	    case True{}:
299	      Nat.add(Nat.mul(l, q), Nat.sub(q, 1n))
300	    case False{}:
301	      Nat.sub(Nat.add(Nat.mul(l, q), j), 1n)
302	
303	# J1 || J2: the address block's lane idx mod 128 (data-independent), or the
304	# first lane of the previous block (data-dependent).
305	def pick(indep: Bool, +addr: A.Block, +idx: Nat, +prev: A.Block) -> T.Lane:
306	  match indep:
307	    case True{}:
308	      G.lane(addr, Nat.mod(idx, 128n))
309	    case False{}:
310	      G.lane(prev, 0n)
311	
312	def lo(x: T.Lane) -> U32:
313	  match x:
314	    case T.W{l, h}:
315	      l
316	
317	def hi(x: T.Lane) -> U32:
318	  match x:
319	    case T.W{l, h}:
320	      h
321	
322	# ---------------------------------------------------------------- filling (section 3.2, steps 5 and 6)
323	
324	# B[l][j] = G(B[l][j-1], B[l'][z']) in the first pass; XORed into the old
325	# B[l][j] in later passes (version 0x13).
326	def store(r0: Bool, +cur: Nat, +prev: A.Block, +refb: A.Block, +mem: List<&2, A.Block>) -> List<&2, A.Block>:
327	  match r0:
328	    case True{}:
329	      set(mem, cur, G.G(prev, refb))
330	    case False{}:
331	      set(mem, cur, G.xor(G.G(prev, refb), get(mem, cur)))
332	
333	def step(+r: Nat, +l: Nat, +s: Nat, +idx: Nat, +p: Nat, +q: Nat, +sl: Nat, +cur: Nat, +indep: Bool, +addr: A.Block, +prev: A.Block, +mem: List<&2, A.Block>) -> List<&2, A.Block>:
334	  +r0 = Nat.is_eq(r, 0n)
335	  +pr = pick(indep, addr, idx, prev)
336	  +rl = ref_lane(Bool.and(r0, Nat.is_eq(s, 0n)), l, hi(pr), p)
337	  +w = area(area_base(r0, s, sl, q), idx, Nat.is_eq(rl, l))
338	  +ri = Nat.mod(Nat.add(start(r0, s, sl), rel(w, lo(pr))), q)
339	  store(r0, cur, prev, get(mem, Nat.add(Nat.mul(rl, q), ri)), mem)
340	
341	# Positions idx .. idx + n - 1 of segment (r, s) of lane l.
342	def seg_go(n: Nat, +idx: Nat, first: Bool, addr: A.Block, +mem: List<&2, A.Block>, +r: Nat, +l: Nat, +s: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +indep: Bool) -> List<&2, A.Block>:
343	  match n:
344	    case 0n:
345	      mem
346	    case 1n+rest:
347	      +addr2 = regen(Bool.and(indep, Bool.or(first, Nat.is_eq(Nat.mod(idx, 128n), 0n))), addr, r, l, s, mm, t, idx)
348	      +j = Nat.add(Nat.mul(s, sl), idx)
349	      +cur = Nat.add(Nat.mul(l, q), j)
350	      +prev = get(mem, prev_index(l, q, j, Nat.is_eq(j, 0n)))
351	      seg_go(rest, Nat.add(idx, 1n), False{}, addr2, step(r, l, s, idx, p, q, sl, cur, indep, addr2, prev, mem), r, l, s, p, q, sl, mm, t, indep)
352	
353	def start_index(first: Bool) -> Nat:
354	  match first:
355	    case True{}:
356	      2n
357	    case False{}:
358	      0n
359	
360	# Segment s of lane l in pass r; data-independent addressing (Argon2i) in the
361	# first two slices of the first pass, data-dependent (Argon2d) otherwise.
362	def segment(+r: Nat, +s: Nat, +l: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>) -> List<&2, A.Block>:
363	  +r0 = Nat.is_eq(r, 0n)
364	  +st = start_index(Bool.and(r0, Nat.is_eq(s, 0n)))
365	  seg_go(Nat.sub(sl, st), st, True{}, G.zero(), mem, r, l, s, p, q, sl, mm, t, Bool.and(r0, Nat.is_lt(s, 2n)))
366	
367	def lanes_go(n: Nat, +l: Nat, +r: Nat, +s: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>) -> List<&2, A.Block>:
368	  match n:
369	    case 0n:
370	      mem
371	    case 1n+rest:
372	      lanes_go(rest, Nat.add(l, 1n), r, s, p, q, sl, mm, t, segment(r, s, l, p, q, sl, mm, t, mem))
373	
374	def slices_go(n: Nat, +s: Nat, +r: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>) -> List<&2, A.Block>:
375	  match n:
376	    case 0n:
377	      mem
378	    case 1n+rest:
379	      slices_go(rest, Nat.add(s, 1n), r, p, q, sl, mm, t, lanes_go(p, 0n, r, s, p, q, sl, mm, t, mem))
380	
381	def passes_go(n: Nat, +r: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +mem: List<&2, A.Block>) -> List<&2, A.Block>:
382	  match n:
383	    case 0n:
384	      mem
385	    case 1n+rest:
386	      passes_go(rest, Nat.add(r, 1n), p, q, sl, mm, t, slices_go(4n, 0n, r, p, q, sl, mm, t, mem))
387	
388	# B[l][0] = H'^1024(H0 || LE32(0) || LE32(l)), B[l][1] = H'^1024(H0 || LE32(1) || LE32(l)).
389	def init_go(n: Nat, +l: Nat, +q: Nat, +hh: List<&2, U32>, +mem: List<&2, A.Block>) -> List<&2, A.Block>:
390	  match n:
391	    case 0n:
392	      mem
393	    case 1n+rest:
394	      +b0 = block_of(hprime(1024n, cat(hh, cat(le32(0n), le32(l)))))
395	      +b1 = block_of(hprime(1024n, cat(hh, cat(le32(1n), le32(l)))))
396	      init_go(rest, Nat.add(l, 1n), q, hh, set(set(mem, Nat.mul(l, q), b0), Nat.add(Nat.mul(l, q), 1n), b1))
397	
398	# C = B[0][q-1] XOR B[1][q-1] XOR .. XOR B[p-1][q-1]: b is B[l][q-1], n more
399	# lanes follow.
400	def final_go(n: Nat, +l: Nat, +q: Nat, c: A.Block, b: A.Block, +mem: List<&2, A.Block>) -> A.Block:
401	  match n:
402	    case 0n:
403	      G.xor(c, b)
404	    case 1n+rest:
405	      final_go(rest, Nat.add(l, 1n), q, G.xor(c, b), get(mem, Nat.add(Nat.mul(Nat.add(l, 1n), q), Nat.sub(q, 1n))), mem)
406	
407	# ---------------------------------------------------------------- Argon2id
408	
409	# RFC 9106 section 3.1: 1 <= p <= 2^24 - 1, 4 <= T <= 2^32 - 1,
410	# 8p <= m <= 2^32 - 1, 1 <= t <= 2^32 - 1, 8 <= |S| <= 2^32 - 1 and |P|, |K|,
411	# |X| <= 2^32 - 1.
412	def valid(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat) -> Bool:
413	  Bool.and(Bool.and(Bool.and(Nat.is_le(1n, p), Nat.is_le(p, 16777215n)), Bool.and(Nat.is_le(4n, tl), Nat.is_le(tl, 4294967295n))),
414	    Bool.and(Bool.and(Bool.and(Nat.is_le(Nat.mul(8n, p), m), Nat.is_le(m, 4294967295n)), Bool.and(Nat.is_le(1n, t), Nat.is_le(t, 4294967295n))),
415	      Bool.and(Bool.and(Nat.is_le(8n, len(salt)), Nat.is_le(len(salt), 4294967295n)), Bool.and(Nat.is_le(len(pw), 4294967295n), Bool.and(Nat.is_le(len(key), 4294967295n), Nat.is_le(len(ad), 4294967295n))))))
416	
417	# The tag: m' = 4p floor(m / 4p) blocks, q = m' / p columns, segments of q / 4.
418	def run(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat) -> List<&2, U32>:
419	  +mm = Nat.mul(Nat.mul(4n, p), Nat.div(m, Nat.mul(4n, p)))
420	  +q = Nat.div(mm, p)
421	  +sl = Nat.div(q, 4n)
422	  +hh = h0(p, tl, m, t, pw, salt, key, ad)
423	  +mem = passes_go(t, 0n, p, q, sl, mm, t, init_go(p, 0n, q, hh, C.replicate(A.Block, mm, G.zero())))
424	  hprime(tl, block_bytes(final_go(Nat.sub(p, 1n), 0n, q, G.zero(), get(mem, Nat.sub(q, 1n)), mem)))
425	
426	def checked(ok: Bool, +pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat) -> Maybe<&2, List<&2, U32>>:
427	  match ok:
428	    case True{}:
429	      Some{run(pw, salt, key, ad, t, m, p, tl)}
430	    case False{}:
431	      None{}
432	
433	# Argon2id(P, S, K, X; t passes, m KiB of memory, p lanes, T tag bytes), or
434	# None when a parameter is out of range.
435	def argon2id(+pw: List<&2, U32>, +salt: List<&2, U32>, +key: List<&2, U32>, +ad: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat) -> Maybe<&2, List<&2, U32>>:
436	  checked(valid(pw, salt, key, ad, t, m, p, tl), pw, salt, key, ad, t, m, p, tl)