1	# Generated by tools/generators/argon2_gen.py; do not edit by hand.
2	import Base
3	import ../blake/blake2b/types.bend as T
4	import ./types.bend as A
5	
6	# The 32 words of a row: lane n is words 2n (low) and 2n+1 (high).
7	def row_words(v: T.State) -> List<&2,U32>:
8	  match v:
9	    case T.V{T.W{l0,h0},T.W{l1,h1},T.W{l2,h2},T.W{l3,h3},T.W{l4,h4},T.W{l5,h5},T.W{l6,h6},T.W{l7,h7},T.W{l8,h8},T.W{l9,h9},T.W{l10,h10},T.W{l11,h11},T.W{l12,h12},T.W{l13,h13},T.W{l14,h14},T.W{l15,h15}}:
10	      [l0,h0,l1,h1,l2,h2,l3,h3,l4,h4,l5,h5,l6,h6,l7,h7,l8,h8,l9,h9,l10,h10,l11,h11,l12,h12,l13,h13,l14,h14,l15,h15]
11	
12	def app(xs: List<&2,U32>, ys: List<&2,U32>) -> List<&2,U32>:
13	  List.append(&2, U32, xs, ys)
14	
15	# The 256 words of a block, row after row.
16	def words(b: A.Block) -> List<&2,U32>:
17	  match b:
18	    case A.B{r0,r1,r2,r3,r4,r5,r6,r7}:
19	      app(row_words(r0),app(row_words(r1),app(row_words(r2),app(row_words(r3),app(row_words(r4),app(row_words(r5),app(row_words(r6),app(row_words(r7),Nil{}))))))))
20	
21	# Sixteen lanes from 32 words, and the words left over.
22	def row(ws: List<&2,U32>) -> T.State & List<&2,U32>:
23	  match ws:
24	    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:
25	      (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)
26	    case _: (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}},Nil{})
27	
28	def rows8_7(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:
29	  (r7,ws) = p
30	  A.B{r0,r1,r2,r3,r4,r5,r6,r7}
31	
32	def rows8_6(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:
33	  (r6,ws) = p
34	  rows8_7(r0,r1,r2,r3,r4,r5,r6,row(ws))
35	
36	def rows8_5(r0: T.State, r1: T.State, r2: T.State, r3: T.State, r4: T.State, p: T.State & List<&2,U32>) -> A.Block:
37	  (r5,ws) = p
38	  rows8_6(r0,r1,r2,r3,r4,r5,row(ws))
39	
40	def rows8_4(r0: T.State, r1: T.State, r2: T.State, r3: T.State, p: T.State & List<&2,U32>) -> A.Block:
41	  (r4,ws) = p
42	  rows8_5(r0,r1,r2,r3,r4,row(ws))
43	
44	def rows8_3(r0: T.State, r1: T.State, r2: T.State, p: T.State & List<&2,U32>) -> A.Block:
45	  (r3,ws) = p
46	  rows8_4(r0,r1,r2,r3,row(ws))
47	
48	def rows8_2(r0: T.State, r1: T.State, p: T.State & List<&2,U32>) -> A.Block:
49	  (r2,ws) = p
50	  rows8_3(r0,r1,r2,row(ws))
51	
52	def rows8_1(r0: T.State, p: T.State & List<&2,U32>) -> A.Block:
53	  (r1,ws) = p
54	  rows8_2(r0,r1,row(ws))
55	
56	def rows8_0(p: T.State & List<&2,U32>) -> A.Block:
57	  (r0,ws) = p
58	  rows8_1(r0,row(ws))
59	
60	# The block of 256 words (the inverse of words).
61	def rows8(ws: List<&2,U32>) -> A.Block:
62	  rows8_0(row(ws))