1	import Base
2	import ../../math/w64.bend as X
3	import ../blake/blake2b/types.bend as T
4	import ../blake/blake2b/sized.bend as H
5	import ./types.bend as A
6	import ./blamka.bend as G
7	import ./sub.bend as SB
8	import ./memory.bend as M
9	
10	# Argon2id, version 0x13 (RFC 9106). Bytes are U32 values below 256; every
11	# size is a Nat. The memory is the packed Array<U32> of memory.bend; the
12	# blocks are compressed by blamka.bend. The lanes are filled one after the
13	# other within a slice (a sequential schedule of the RFC's parallel one).
14	
15	def cat(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
16	  List.append(&2, U32, xs, ys)
17	
18	def len(xs: List<&2, U32>) -> Nat:
19	  List.length(&2, U32, xs)
20	
21	# LE32(n) for n < 2^32.
22	def le32(+n: Nat) -> List<&2, U32>:
23	  [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))]
24	
25	# ---------------------------------------------------------------- H0 and H'
26	
27	# H' for T > 64 (RFC 9106 section 3.3): W1 || .. || Wr || V_{r+1}, where
28	# Wi is the first 32 bytes of Vi, V_{i+1} = H^64(Vi) and V_{r+1} = H^{T-32r}(Vr).
29	# (V_i is a 64-byte digest, never empty; it is inspected first so that proofs
30	# keep the chain of hashes folded.)
31	def hp_go(n: Nat, v: List<&2, U32>, +last: Nat) -> List<&2, U32>:
32	  match n v:
33	    case _ Nil{}:
34	      Nil{}
35	    case 0n +x <> +r:
36	      cat(List.take(&2, U32, x <> r, 32n), H.hash(last, x <> r))
37	    case 1n+p +x <> +r:
38	      cat(List.take(&2, U32, x <> r, 32n), hp_go(p, H.hash(64n, x <> r), last))
39	
40	def hp_pick(+tl: Nat, +x: List<&2, U32>, short: Bool) -> List<&2, U32>:
41	  match short:
42	    case True{}:
43	      H.hash(tl, x)
44	    case False{}:
45	      +r = Nat.sub(Nat.div(Nat.add(tl, 31n), 32n), 2n)
46	      hp_go(Nat.sub(r, 1n), H.hash(64n, x), Nat.sub(tl, Nat.mul(32n, r)))
47	
48	# H'^T(a): the variable-length hash, over LE32(T) || a.
49	def hprime(+tl: Nat, a: List<&2, U32>) -> List<&2, U32>:
50	  hp_pick(tl, cat(le32(tl), a), Nat.is_le(tl, 64n))
51	
52	# H0 (RFC 9106 section 3.2, step 1), version 0x13 and type 2 (Argon2id).
53	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>:
54	  H.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))))))))))))))
55	
56	# ---------------------------------------------------------------- blocks and bytes
57	
58	# A block from its 1024 little-endian bytes.
59	def block_of(bs: List<&2, U32>) -> A.Block:
60	  SB.rows8(H.words(bs))
61	
62	def state_bytes(v: T.State) -> List<&2, U32>:
63	  match v:
64	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15}:
65	      List.concat(&2, U32, [H.lane_bytes(x0), H.lane_bytes(x1), H.lane_bytes(x2), H.lane_bytes(x3), H.lane_bytes(x4), H.lane_bytes(x5), H.lane_bytes(x6), H.lane_bytes(x7), H.lane_bytes(x8), H.lane_bytes(x9), H.lane_bytes(x10), H.lane_bytes(x11), H.lane_bytes(x12), H.lane_bytes(x13), H.lane_bytes(x14), H.lane_bytes(x15)])
66	
67	# The 1024 little-endian bytes of a block.
68	def block_bytes(b: A.Block) -> List<&2, U32>:
69	  match b:
70	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7}:
71	      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)])
72	
73	def row_at(b: A.Block, +i: Nat) -> T.State:
74	  match b i:
75	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 0n:
76	      r0
77	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 1n:
78	      r1
79	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 2n:
80	      r2
81	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 3n:
82	      r3
83	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 4n:
84	      r4
85	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 5n:
86	      r5
87	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} 6n:
88	      r6
89	    case A.B{r0, r1, r2, r3, r4, r5, r6, r7} _:
90	      r7
91	
92	def at(v: T.State, +j: Nat) -> T.Lane:
93	  match v j:
94	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 0n:
95	      x0
96	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 1n:
97	      x1
98	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 2n:
99	      x2
100	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 3n:
101	      x3
102	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 4n:
103	      x4
104	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 5n:
105	      x5
106	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 6n:
107	      x6
108	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 7n:
109	      x7
110	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 8n:
111	      x8
112	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 9n:
113	      x9
114	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 10n:
115	      x10
116	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 11n:
117	      x11
118	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 12n:
119	      x12
120	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 13n:
121	      x13
122	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 14n:
123	      x14
124	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} 15n:
125	      x15
126	    case T.V{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} _:
127	      T.W{0, 0}
128	
129	# Lane n (0 <= n < 128) of a block.
130	def lane(+b: A.Block, +n: Nat) -> T.Lane:
131	  at(row_at(b, Nat.div(n, 16n)), Nat.mod(n, 16n))
132	
133	# ---------------------------------------------------------------- indexing (RFC 9106 section 3.4)
134	
135	def hi(x: T.Lane) -> U32:
136	  match x:
137	    case T.W{l, h}:
138	      h
139	
140	def small(+x: Nat) -> T.Lane:
141	  T.W{U32.from_nat(x), 0}
142	
143	# Z = (r, l, s, m', t, y, i), zero-padded to a block.
144	def input_of(+r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +ctr: Nat) -> A.Block:
145	  A.B{T.V{small(r), small(l), small(s), small(mm), small(t), small(2n), small(ctr), 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.V{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.V{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.V{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.V{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.V{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.V{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.V{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}}}
146	
147	# (r is inspected first, so the proofs keep an input block with a symbolic
148	# pass folded instead of compressing it symbolically.)
149	def input_block(r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +ctr: Nat) -> A.Block:
150	  match r:
151	    case 0n:
152	      input_of(0n, l, s, mm, t, ctr)
153	    case 1n+x:
154	      input_of(1n+x, l, s, mm, t, ctr)
155	
156	# The address block of counter ctr: G(0, G(0, Z)).
157	def addresses(+r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +ctr: Nat) -> A.Block:
158	  G.compress(G.zero(), G.compress(G.zero(), input_block(r, l, s, mm, t, ctr)))
159	
160	# The address block for position idx: a new one at the segment's first
161	# position and at every multiple of 128 (data-independent segments only).
162	def regen(need: Bool, addr: A.Block, +r: Nat, +l: Nat, +s: Nat, +mm: Nat, +t: Nat, +idx: Nat) -> A.Block:
163	  match need:
164	    case True{}:
165	      addresses(r, l, s, mm, t, Nat.add(Nat.div(idx, 128n), 1n))
166	    case False{}:
167	      addr
168	
169	# |W|, the number of blocks the reference may be drawn from.
170	def area_base(r0: Bool, +s: Nat, +sl: Nat, +q: Nat) -> Nat:
171	  match r0:
172	    case True{}:
173	      Nat.mul(s, sl)
174	    case False{}:
175	      Nat.sub(q, sl)
176	
177	def area_other(+base: Nat, zero: Bool) -> Nat:
178	  match zero:
179	    case True{}:
180	      Nat.sub(base, 1n)
181	    case False{}:
182	      base
183	
184	def area(+base: Nat, +idx: Nat, same: Bool) -> Nat:
185	  match same:
186	    case True{}:
187	      Nat.sub(Nat.add(base, idx), 1n)
188	    case False{}:
189	      area_other(base, Nat.is_eq(idx, 0n))
190	
191	# |W| - 1 - (|W| * (J1^2 / 2^32)) / 2^32
192	def rel(+w: Nat, +j1: U32) -> Nat:
193	  +x = X.hi(X.mul32(j1, j1))
194	  Nat.sub(Nat.sub(w, 1n), U32.to_nat(X.hi(X.mul32(U32.from_nat(w), x))))
195	
196	def start_last(+s: Nat, +sl: Nat, last: Bool) -> Nat:
197	  match last:
198	    case True{}:
199	      0n
200	    case False{}:
201	      Nat.mul(Nat.add(s, 1n), sl)
202	
203	# The first block of the reference area: 0 in the first pass, else the start
204	# of the next segment (wrapping).
205	def start(r0: Bool, +s: Nat, +sl: Nat) -> Nat:
206	  match r0:
207	    case True{}:
208	      0n
209	    case False{}:
210	      start_last(s, sl, Nat.is_eq(s, 3n))
211	
212	def ref_lane(forced: Bool, +l: Nat, +j2: U32, +p: Nat) -> Nat:
213	  match forced:
214	    case True{}:
215	      l
216	    case False{}:
217	      Nat.mod(U32.to_nat(j2), p)
218	
219	def prev_index(+l: Nat, +q: Nat, +j: Nat, first: Bool) -> Nat:
220	  match first:
221	    case True{}:
222	      Nat.add(Nat.mul(l, q), Nat.sub(q, 1n))
223	    case False{}:
224	      Nat.sub(Nat.add(Nat.mul(l, q), j), 1n)
225	
226	def pick(indep: Bool, +addr: A.Block, +idx: Nat, +prev: A.Block) -> T.Lane:
227	  match indep:
228	    case True{}:
229	      lane(addr, Nat.mod(idx, 128n))
230	    case False{}:
231	      lane(prev, 0n)
232	
233	# ---------------------------------------------------------------- filling (RFC 9106 section 3.2, steps 5-6)
234	
235	def store_xor(+cur: Nat, +prev: A.Block, +refb: A.Block, pair: Array<U32> & A.Block) -> Array<U32>:
236	  (a, old) = pair
237	  M.set(cur, G.compress_xor(prev, refb, old), a)
238	
239	# B[l][j] = G(B[l][j-1], B[l'][z']), XORed into the old block after the first pass.
240	def store(r0: Bool, +cur: Nat, +prev: A.Block, +refb: A.Block, a: Array<U32>) -> Array<U32>:
241	  match r0:
242	    case True{}:
243	      M.set(cur, G.compress(prev, refb), a)
244	    case False{}:
245	      store_xor(cur, prev, refb, M.get(cur, a))
246	
247	def with_ref(r0: Bool, +cur: Nat, +prev: A.Block, pair: Array<U32> & A.Block) -> Array<U32>:
248	  (a, +refb) = pair
249	  store(r0, cur, prev, refb, a)
250	
251	# One block: pair holds the memory and the previous block.
252	def step(+r: Nat, +l: Nat, +s: Nat, +idx: Nat, +p: Nat, +q: Nat, +sl: Nat, +cur: Nat, +indep: Bool, +addr: A.Block, pair: Array<U32> & A.Block) -> Array<U32>:
253	  (a, +prev) = pair
254	  +r0 = Nat.is_eq(r, 0n)
255	  +pr = pick(indep, addr, idx, prev)
256	  +rl = ref_lane(Bool.and(r0, Nat.is_eq(s, 0n)), l, hi(pr), p)
257	  +w = area(area_base(r0, s, sl, q), idx, Nat.is_eq(rl, l))
258	  +ri = Nat.mod(Nat.add(start(r0, s, sl), rel(w, G.lo(pr))), q)
259	  with_ref(r0, cur, prev, M.get(Nat.add(Nat.mul(rl, q), ri), a))
260	
261	# Positions idx .. idx + n - 1 of segment (r, s) of lane l.
262	def seg_go(n: Nat, +idx: Nat, first: Bool, addr: A.Block, a: Array<U32>, +r: Nat, +l: Nat, +s: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, +indep: Bool) -> Array<U32>:
263	  match n:
264	    case 0n:
265	      a
266	    case 1n+rest:
267	      +addr2 = regen(Bool.and(indep, Bool.or(first, Nat.is_eq(Nat.mod(idx, 128n), 0n))), addr, r, l, s, mm, t, idx)
268	      +j = Nat.add(Nat.mul(s, sl), idx)
269	      +cur = Nat.add(Nat.mul(l, q), j)
270	      seg_go(rest, Nat.add(idx, 1n), False{}, addr2, step(r, l, s, idx, p, q, sl, cur, indep, addr2, M.get(prev_index(l, q, j, Nat.is_eq(j, 0n)), a)), r, l, s, p, q, sl, mm, t, indep)
271	
272	def start_index(first: Bool) -> Nat:
273	  match first:
274	    case True{}:
275	      2n
276	    case False{}:
277	      0n
278	
279	# Segment s of lane l in pass r; data-independent addressing in the first two
280	# slices of the first pass. The first two blocks of each lane are already set.
281	def segment(+r: Nat, +s: Nat, +l: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, a: Array<U32>) -> Array<U32>:
282	  +r0 = Nat.is_eq(r, 0n)
283	  +st = start_index(Bool.and(r0, Nat.is_eq(s, 0n)))
284	  seg_go(Nat.sub(sl, st), st, True{}, G.zero(), a, r, l, s, p, q, sl, mm, t, Bool.and(r0, Nat.is_lt(s, 2n)))
285	
286	def lanes_go(n: Nat, +l: Nat, +r: Nat, +s: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, a: Array<U32>) -> Array<U32>:
287	  match n:
288	    case 0n:
289	      a
290	    case 1n+rest:
291	      lanes_go(rest, Nat.add(l, 1n), r, s, p, q, sl, mm, t, segment(r, s, l, p, q, sl, mm, t, a))
292	
293	def slices_go(n: Nat, +s: Nat, +r: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, a: Array<U32>) -> Array<U32>:
294	  match n:
295	    case 0n:
296	      a
297	    case 1n+rest:
298	      slices_go(rest, Nat.add(s, 1n), r, p, q, sl, mm, t, lanes_go(p, 0n, r, s, p, q, sl, mm, t, a))
299	
300	def passes_go(n: Nat, +r: Nat, +p: Nat, +q: Nat, +sl: Nat, +mm: Nat, +t: Nat, a: Array<U32>) -> Array<U32>:
301	  match n:
302	    case 0n:
303	      a
304	    case 1n+rest:
305	      passes_go(rest, Nat.add(r, 1n), p, q, sl, mm, t, slices_go(4n, 0n, r, p, q, sl, mm, t, a))
306	
307	# B[l][0] = H'^1024(H0 || LE32(0) || LE32(l)), B[l][1] = H'^1024(H0 || LE32(1) || LE32(l)).
308	def init_go(n: Nat, +l: Nat, +q: Nat, +hh: List<&2, U32>, a: Array<U32>) -> Array<U32>:
309	  match n:
310	    case 0n:
311	      a
312	    case 1n+rest:
313	      +b0 = block_of(hprime(1024n, cat(hh, cat(le32(0n), le32(l)))))
314	      +b1 = block_of(hprime(1024n, cat(hh, cat(le32(1n), le32(l)))))
315	      init_go(rest, Nat.add(l, 1n), q, hh, M.set(Nat.add(Nat.mul(l, q), 1n), b1, M.set(Nat.mul(l, q), b0, a)))
316	
317	# C = B[0][q-1] XOR .. XOR B[p-1][q-1]: pair holds the memory and B[l][q-1],
318	# n more lanes follow.
319	def final_go(n: Nat, +l: Nat, +q: Nat, c: A.Block, pair: Array<U32> & A.Block) -> A.Block:
320	  match n pair:
321	    case 0n Tuple{a, b}:
322	      G.xor(c, b)
323	    case 1n+rest Tuple{a, b}:
324	      final_go(rest, Nat.add(l, 1n), q, G.xor(c, b), M.get(Nat.add(Nat.mul(Nat.add(l, 1n), q), Nat.sub(q, 1n)), a))
325	
326	# ---------------------------------------------------------------- Argon2id
327	
328	# RFC 9106 section 3.1 ranges: 1 <= p <= 2^24 - 1, 4 <= T <= 2^32 - 1,
329	# 8p <= m <= 2^32 - 1, 1 <= t <= 2^32 - 1, 8 <= |S| <= 2^32 - 1 and |P|,
330	# |K|, |X| <= 2^32 - 1.
331	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:
332	  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))),
333	    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))),
334	      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))))))
335	
336	# m' = 4p floor(m / 4p), the number of blocks.
337	def blocks(+m: Nat, +p: Nat) -> Nat:
338	  Nat.mul(Nat.mul(4n, p), Nat.div(m, Nat.mul(4n, p)))
339	
340	# This implementation's limit: the memory of m' blocks is an array of at most
341	# 2^31 words, so m' <= 2^23 (8 GiB), the RFC allowing up to 2^32 - 1 KiB.
342	def fits(+m: Nat, +p: Nat) -> Bool:
343	  Nat.is_le(M.levels(blocks(m, p)), 23n)
344	
345	# The tag for valid parameters.
346	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>:
347	  +mm = blocks(m, p)
348	  +q = Nat.div(mm, p)
349	  +sl = Nat.div(q, 4n)
350	  +k = M.levels(mm)
351	  +hh = h0(p, tl, m, t, pw, salt, key, ad)
352	  a = passes_go(t, 0n, p, q, sl, mm, t, init_go(p, 0n, q, hh, M.new(k)))
353	  hprime(tl, block_bytes(final_go(Nat.sub(p, 1n), 0n, q, G.zero(), M.get(Nat.sub(q, 1n), a))))
354	
355	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>>:
356	  match ok:
357	    case True{}:
358	      Some{run(pw, salt, key, ad, t, m, p, tl)}
359	    case False{}:
360	      None{}
361	
362	# Argon2id(P, S, K, X; t passes, m KiB, p lanes, T tag bytes): the T-byte tag,
363	# or None when a parameter is out of the RFC 9106 ranges or the memory does
364	# not fit (fits).
365	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>>:
366	  checked(Bool.and(valid(pw, salt, key, ad, t, m, p, tl), fits(m, p)), pw, salt, key, ad, t, m, p, tl)