1	# Generated by tools/generators/blake2b_gen.py; do not edit by hand.
2	import Base
3	import ./types.bend as T
4	import ./lane.bend as L
5	
6	# G (RFC 7693 section 3.1) on four words and two message words.
7	def g(a: T.Lane, +b: T.Lane, c: T.Lane, d: T.Lane, x: T.Lane, y: T.Lane) -> T.Quad:
8	  +a1 = L.add(L.add(a,b),x)
9	  +d1 = L.rot32(L.xor(d,a1))
10	  +c1 = L.add(c,d1)
11	  +b1 = L.rot24(L.xor(b,c1))
12	  +a2 = L.add(L.add(a1,b1),y)
13	  +d2 = L.rot16(L.xor(d1,a2))
14	  +c2 = L.add(c1,d2)
15	  +b2 = L.rot63(L.xor(b1,c2))
16	  T.Q{a2,b2,c2,d2}
17	
18	def column0_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
19	  match q:
20	    case T.Q{t4_3,t4_7,t4_11,t4_15}:
21	      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}
22	
23	def column0_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
24	  match q:
25	    case T.Q{t3_2,t3_6,t3_10,t3_14}:
26	      column0_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)
27	
28	def column0_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
29	  match q:
30	    case T.Q{t2_1,t2_5,t2_9,t2_13}:
31	      column0_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)
32	
33	def column0_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
34	  match q:
35	    case T.Q{t1_0,t1_4,t1_8,t1_12}:
36	      column0_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)
37	
38	# Round 0, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
39	def column0(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
40	  match v:
41	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
42	      column0_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)
43	
44	def diagonal0_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
45	  match q:
46	    case T.Q{t4_3,t4_4,t4_9,t4_14}:
47	      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}
48	
49	def diagonal0_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
50	  match q:
51	    case T.Q{t3_2,t3_7,t3_8,t3_13}:
52	      diagonal0_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)
53	
54	def diagonal0_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
55	  match q:
56	    case T.Q{t2_1,t2_6,t2_11,t2_12}:
57	      diagonal0_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)
58	
59	def diagonal0_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
60	  match q:
61	    case T.Q{t1_0,t1_5,t1_10,t1_15}:
62	      diagonal0_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)
63	
64	# Round 0, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
65	def diagonal0(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
66	  match v:
67	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
68	      diagonal0_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)
69	
70	# Round 0 uses the message schedule SIGMA[0], fixed at compile time.
71	def round0(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
72	  diagonal0(column0(v,m0,m1,m2,m3,m4,m5,m6,m7),m8,m9,m10,m11,m12,m13,m14,m15)
73	
74	def column1_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
75	  match q:
76	    case T.Q{t4_3,t4_7,t4_11,t4_15}:
77	      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}
78	
79	def column1_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
80	  match q:
81	    case T.Q{t3_2,t3_6,t3_10,t3_14}:
82	      column1_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)
83	
84	def column1_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
85	  match q:
86	    case T.Q{t2_1,t2_5,t2_9,t2_13}:
87	      column1_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)
88	
89	def column1_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
90	  match q:
91	    case T.Q{t1_0,t1_4,t1_8,t1_12}:
92	      column1_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)
93	
94	# Round 1, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
95	def column1(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
96	  match v:
97	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
98	      column1_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)
99	
100	def diagonal1_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
101	  match q:
102	    case T.Q{t4_3,t4_4,t4_9,t4_14}:
103	      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}
104	
105	def diagonal1_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
106	  match q:
107	    case T.Q{t3_2,t3_7,t3_8,t3_13}:
108	      diagonal1_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)
109	
110	def diagonal1_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
111	  match q:
112	    case T.Q{t2_1,t2_6,t2_11,t2_12}:
113	      diagonal1_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)
114	
115	def diagonal1_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
116	  match q:
117	    case T.Q{t1_0,t1_5,t1_10,t1_15}:
118	      diagonal1_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)
119	
120	# Round 1, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
121	def diagonal1(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
122	  match v:
123	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
124	      diagonal1_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)
125	
126	# Round 1 uses the message schedule SIGMA[1], fixed at compile time.
127	def round1(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
128	  diagonal1(column1(v,m14,m10,m4,m8,m9,m15,m13,m6),m1,m12,m0,m2,m11,m7,m5,m3)
129	
130	def column2_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
131	  match q:
132	    case T.Q{t4_3,t4_7,t4_11,t4_15}:
133	      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}
134	
135	def column2_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
136	  match q:
137	    case T.Q{t3_2,t3_6,t3_10,t3_14}:
138	      column2_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)
139	
140	def column2_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
141	  match q:
142	    case T.Q{t2_1,t2_5,t2_9,t2_13}:
143	      column2_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)
144	
145	def column2_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
146	  match q:
147	    case T.Q{t1_0,t1_4,t1_8,t1_12}:
148	      column2_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)
149	
150	# Round 2, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
151	def column2(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
152	  match v:
153	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
154	      column2_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)
155	
156	def diagonal2_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
157	  match q:
158	    case T.Q{t4_3,t4_4,t4_9,t4_14}:
159	      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}
160	
161	def diagonal2_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
162	  match q:
163	    case T.Q{t3_2,t3_7,t3_8,t3_13}:
164	      diagonal2_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)
165	
166	def diagonal2_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
167	  match q:
168	    case T.Q{t2_1,t2_6,t2_11,t2_12}:
169	      diagonal2_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)
170	
171	def diagonal2_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
172	  match q:
173	    case T.Q{t1_0,t1_5,t1_10,t1_15}:
174	      diagonal2_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)
175	
176	# Round 2, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
177	def diagonal2(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
178	  match v:
179	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
180	      diagonal2_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)
181	
182	# Round 2 uses the message schedule SIGMA[2], fixed at compile time.
183	def round2(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
184	  diagonal2(column2(v,m11,m8,m12,m0,m5,m2,m15,m13),m10,m14,m3,m6,m7,m1,m9,m4)
185	
186	def column3_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
187	  match q:
188	    case T.Q{t4_3,t4_7,t4_11,t4_15}:
189	      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}
190	
191	def column3_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
192	  match q:
193	    case T.Q{t3_2,t3_6,t3_10,t3_14}:
194	      column3_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)
195	
196	def column3_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
197	  match q:
198	    case T.Q{t2_1,t2_5,t2_9,t2_13}:
199	      column3_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)
200	
201	def column3_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
202	  match q:
203	    case T.Q{t1_0,t1_4,t1_8,t1_12}:
204	      column3_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)
205	
206	# Round 3, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
207	def column3(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
208	  match v:
209	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
210	      column3_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)
211	
212	def diagonal3_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
213	  match q:
214	    case T.Q{t4_3,t4_4,t4_9,t4_14}:
215	      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}
216	
217	def diagonal3_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
218	  match q:
219	    case T.Q{t3_2,t3_7,t3_8,t3_13}:
220	      diagonal3_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)
221	
222	def diagonal3_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
223	  match q:
224	    case T.Q{t2_1,t2_6,t2_11,t2_12}:
225	      diagonal3_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)
226	
227	def diagonal3_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
228	  match q:
229	    case T.Q{t1_0,t1_5,t1_10,t1_15}:
230	      diagonal3_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)
231	
232	# Round 3, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
233	def diagonal3(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
234	  match v:
235	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
236	      diagonal3_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)
237	
238	# Round 3 uses the message schedule SIGMA[3], fixed at compile time.
239	def round3(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
240	  diagonal3(column3(v,m7,m9,m3,m1,m13,m12,m11,m14),m2,m6,m5,m10,m4,m0,m15,m8)
241	
242	def column4_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
243	  match q:
244	    case T.Q{t4_3,t4_7,t4_11,t4_15}:
245	      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}
246	
247	def column4_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
248	  match q:
249	    case T.Q{t3_2,t3_6,t3_10,t3_14}:
250	      column4_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)
251	
252	def column4_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
253	  match q:
254	    case T.Q{t2_1,t2_5,t2_9,t2_13}:
255	      column4_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)
256	
257	def column4_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
258	  match q:
259	    case T.Q{t1_0,t1_4,t1_8,t1_12}:
260	      column4_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)
261	
262	# Round 4, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
263	def column4(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
264	  match v:
265	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
266	      column4_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)
267	
268	def diagonal4_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
269	  match q:
270	    case T.Q{t4_3,t4_4,t4_9,t4_14}:
271	      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}
272	
273	def diagonal4_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
274	  match q:
275	    case T.Q{t3_2,t3_7,t3_8,t3_13}:
276	      diagonal4_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)
277	
278	def diagonal4_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
279	  match q:
280	    case T.Q{t2_1,t2_6,t2_11,t2_12}:
281	      diagonal4_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)
282	
283	def diagonal4_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
284	  match q:
285	    case T.Q{t1_0,t1_5,t1_10,t1_15}:
286	      diagonal4_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)
287	
288	# Round 4, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
289	def diagonal4(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
290	  match v:
291	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
292	      diagonal4_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)
293	
294	# Round 4 uses the message schedule SIGMA[4], fixed at compile time.
295	def round4(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
296	  diagonal4(column4(v,m9,m0,m5,m7,m2,m4,m10,m15),m14,m1,m11,m12,m6,m8,m3,m13)
297	
298	def column5_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
299	  match q:
300	    case T.Q{t4_3,t4_7,t4_11,t4_15}:
301	      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}
302	
303	def column5_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
304	  match q:
305	    case T.Q{t3_2,t3_6,t3_10,t3_14}:
306	      column5_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)
307	
308	def column5_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
309	  match q:
310	    case T.Q{t2_1,t2_5,t2_9,t2_13}:
311	      column5_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)
312	
313	def column5_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
314	  match q:
315	    case T.Q{t1_0,t1_4,t1_8,t1_12}:
316	      column5_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)
317	
318	# Round 5, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
319	def column5(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
320	  match v:
321	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
322	      column5_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)
323	
324	def diagonal5_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
325	  match q:
326	    case T.Q{t4_3,t4_4,t4_9,t4_14}:
327	      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}
328	
329	def diagonal5_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
330	  match q:
331	    case T.Q{t3_2,t3_7,t3_8,t3_13}:
332	      diagonal5_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)
333	
334	def diagonal5_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
335	  match q:
336	    case T.Q{t2_1,t2_6,t2_11,t2_12}:
337	      diagonal5_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)
338	
339	def diagonal5_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
340	  match q:
341	    case T.Q{t1_0,t1_5,t1_10,t1_15}:
342	      diagonal5_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)
343	
344	# Round 5, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
345	def diagonal5(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
346	  match v:
347	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
348	      diagonal5_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)
349	
350	# Round 5 uses the message schedule SIGMA[5], fixed at compile time.
351	def round5(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
352	  diagonal5(column5(v,m2,m12,m6,m10,m0,m11,m8,m3),m4,m13,m7,m5,m15,m14,m1,m9)
353	
354	def column6_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
355	  match q:
356	    case T.Q{t4_3,t4_7,t4_11,t4_15}:
357	      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}
358	
359	def column6_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
360	  match q:
361	    case T.Q{t3_2,t3_6,t3_10,t3_14}:
362	      column6_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)
363	
364	def column6_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
365	  match q:
366	    case T.Q{t2_1,t2_5,t2_9,t2_13}:
367	      column6_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)
368	
369	def column6_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
370	  match q:
371	    case T.Q{t1_0,t1_4,t1_8,t1_12}:
372	      column6_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)
373	
374	# Round 6, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
375	def column6(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
376	  match v:
377	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
378	      column6_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)
379	
380	def diagonal6_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
381	  match q:
382	    case T.Q{t4_3,t4_4,t4_9,t4_14}:
383	      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}
384	
385	def diagonal6_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
386	  match q:
387	    case T.Q{t3_2,t3_7,t3_8,t3_13}:
388	      diagonal6_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)
389	
390	def diagonal6_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
391	  match q:
392	    case T.Q{t2_1,t2_6,t2_11,t2_12}:
393	      diagonal6_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)
394	
395	def diagonal6_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
396	  match q:
397	    case T.Q{t1_0,t1_5,t1_10,t1_15}:
398	      diagonal6_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)
399	
400	# Round 6, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
401	def diagonal6(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
402	  match v:
403	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
404	      diagonal6_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)
405	
406	# Round 6 uses the message schedule SIGMA[6], fixed at compile time.
407	def round6(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
408	  diagonal6(column6(v,m12,m5,m1,m15,m14,m13,m4,m10),m0,m7,m6,m3,m9,m2,m8,m11)
409	
410	def column7_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
411	  match q:
412	    case T.Q{t4_3,t4_7,t4_11,t4_15}:
413	      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}
414	
415	def column7_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
416	  match q:
417	    case T.Q{t3_2,t3_6,t3_10,t3_14}:
418	      column7_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)
419	
420	def column7_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
421	  match q:
422	    case T.Q{t2_1,t2_5,t2_9,t2_13}:
423	      column7_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)
424	
425	def column7_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
426	  match q:
427	    case T.Q{t1_0,t1_4,t1_8,t1_12}:
428	      column7_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)
429	
430	# Round 7, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
431	def column7(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
432	  match v:
433	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
434	      column7_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)
435	
436	def diagonal7_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
437	  match q:
438	    case T.Q{t4_3,t4_4,t4_9,t4_14}:
439	      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}
440	
441	def diagonal7_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
442	  match q:
443	    case T.Q{t3_2,t3_7,t3_8,t3_13}:
444	      diagonal7_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)
445	
446	def diagonal7_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
447	  match q:
448	    case T.Q{t2_1,t2_6,t2_11,t2_12}:
449	      diagonal7_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)
450	
451	def diagonal7_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
452	  match q:
453	    case T.Q{t1_0,t1_5,t1_10,t1_15}:
454	      diagonal7_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)
455	
456	# Round 7, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
457	def diagonal7(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
458	  match v:
459	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
460	      diagonal7_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)
461	
462	# Round 7 uses the message schedule SIGMA[7], fixed at compile time.
463	def round7(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
464	  diagonal7(column7(v,m13,m11,m7,m14,m12,m1,m3,m9),m5,m0,m15,m4,m8,m6,m2,m10)
465	
466	def column8_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
467	  match q:
468	    case T.Q{t4_3,t4_7,t4_11,t4_15}:
469	      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}
470	
471	def column8_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
472	  match q:
473	    case T.Q{t3_2,t3_6,t3_10,t3_14}:
474	      column8_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)
475	
476	def column8_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
477	  match q:
478	    case T.Q{t2_1,t2_5,t2_9,t2_13}:
479	      column8_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)
480	
481	def column8_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
482	  match q:
483	    case T.Q{t1_0,t1_4,t1_8,t1_12}:
484	      column8_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)
485	
486	# Round 8, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
487	def column8(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
488	  match v:
489	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
490	      column8_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)
491	
492	def diagonal8_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
493	  match q:
494	    case T.Q{t4_3,t4_4,t4_9,t4_14}:
495	      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}
496	
497	def diagonal8_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
498	  match q:
499	    case T.Q{t3_2,t3_7,t3_8,t3_13}:
500	      diagonal8_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)
501	
502	def diagonal8_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
503	  match q:
504	    case T.Q{t2_1,t2_6,t2_11,t2_12}:
505	      diagonal8_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)
506	
507	def diagonal8_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
508	  match q:
509	    case T.Q{t1_0,t1_5,t1_10,t1_15}:
510	      diagonal8_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)
511	
512	# Round 8, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
513	def diagonal8(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
514	  match v:
515	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
516	      diagonal8_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)
517	
518	# Round 8 uses the message schedule SIGMA[8], fixed at compile time.
519	def round8(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
520	  diagonal8(column8(v,m6,m15,m14,m9,m11,m3,m0,m8),m12,m2,m13,m7,m1,m4,m10,m5)
521	
522	def column9_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
523	  match q:
524	    case T.Q{t4_3,t4_7,t4_11,t4_15}:
525	      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}
526	
527	def column9_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
528	  match q:
529	    case T.Q{t3_2,t3_6,t3_10,t3_14}:
530	      column9_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)
531	
532	def column9_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
533	  match q:
534	    case T.Q{t2_1,t2_5,t2_9,t2_13}:
535	      column9_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)
536	
537	def column9_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
538	  match q:
539	    case T.Q{t1_0,t1_4,t1_8,t1_12}:
540	      column9_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)
541	
542	# Round 9, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
543	def column9(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
544	  match v:
545	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
546	      column9_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)
547	
548	def diagonal9_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
549	  match q:
550	    case T.Q{t4_3,t4_4,t4_9,t4_14}:
551	      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}
552	
553	def diagonal9_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
554	  match q:
555	    case T.Q{t3_2,t3_7,t3_8,t3_13}:
556	      diagonal9_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)
557	
558	def diagonal9_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
559	  match q:
560	    case T.Q{t2_1,t2_6,t2_11,t2_12}:
561	      diagonal9_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)
562	
563	def diagonal9_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
564	  match q:
565	    case T.Q{t1_0,t1_5,t1_10,t1_15}:
566	      diagonal9_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)
567	
568	# Round 9, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
569	def diagonal9(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
570	  match v:
571	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
572	      diagonal9_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)
573	
574	# Round 9 uses the message schedule SIGMA[9], fixed at compile time.
575	def round9(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
576	  diagonal9(column9(v,m10,m2,m8,m4,m7,m6,m1,m5),m15,m11,m9,m14,m3,m12,m13,m0)
577	
578	def column10_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
579	  match q:
580	    case T.Q{t4_3,t4_7,t4_11,t4_15}:
581	      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}
582	
583	def column10_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
584	  match q:
585	    case T.Q{t3_2,t3_6,t3_10,t3_14}:
586	      column10_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)
587	
588	def column10_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
589	  match q:
590	    case T.Q{t2_1,t2_5,t2_9,t2_13}:
591	      column10_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)
592	
593	def column10_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
594	  match q:
595	    case T.Q{t1_0,t1_4,t1_8,t1_12}:
596	      column10_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)
597	
598	# Round 10, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
599	def column10(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
600	  match v:
601	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
602	      column10_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)
603	
604	def diagonal10_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
605	  match q:
606	    case T.Q{t4_3,t4_4,t4_9,t4_14}:
607	      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}
608	
609	def diagonal10_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
610	  match q:
611	    case T.Q{t3_2,t3_7,t3_8,t3_13}:
612	      diagonal10_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)
613	
614	def diagonal10_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
615	  match q:
616	    case T.Q{t2_1,t2_6,t2_11,t2_12}:
617	      diagonal10_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)
618	
619	def diagonal10_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
620	  match q:
621	    case T.Q{t1_0,t1_5,t1_10,t1_15}:
622	      diagonal10_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)
623	
624	# Round 10, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
625	def diagonal10(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
626	  match v:
627	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
628	      diagonal10_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)
629	
630	# Round 10 uses the message schedule SIGMA[0], fixed at compile time.
631	def round10(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
632	  diagonal10(column10(v,m0,m1,m2,m3,m4,m5,m6,m7),m8,m9,m10,m11,m12,m13,m14,m15)
633	
634	def column11_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_4: T.Lane, t2_5: T.Lane, t3_6: T.Lane, t1_8: T.Lane, t2_9: T.Lane, t3_10: T.Lane, t1_12: T.Lane, t2_13: T.Lane, t3_14: T.Lane) -> T.State:
635	  match q:
636	    case T.Q{t4_3,t4_7,t4_11,t4_15}:
637	      T.V{t1_0,t2_1,t3_2,t4_3,t1_4,t2_5,t3_6,t4_7,t1_8,t2_9,t3_10,t4_11,t1_12,t2_13,t3_14,t4_15}
638	
639	def column11_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, t1_4: T.Lane, t2_5: T.Lane, s7: T.Lane, t1_8: T.Lane, t2_9: T.Lane, s11: T.Lane, t1_12: T.Lane, t2_13: T.Lane, s15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
640	  match q:
641	    case T.Q{t3_2,t3_6,t3_10,t3_14}:
642	      column11_4(g(s3,s7,s11,s15,x6,x7),t1_0,t2_1,t3_2,t1_4,t2_5,t3_6,t1_8,t2_9,t3_10,t1_12,t2_13,t3_14)
643	
644	def column11_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, t1_4: T.Lane, s6: T.Lane, s7: T.Lane, t1_8: T.Lane, s10: T.Lane, s11: T.Lane, t1_12: T.Lane, s14: T.Lane, s15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
645	  match q:
646	    case T.Q{t2_1,t2_5,t2_9,t2_13}:
647	      column11_3(g(s2,s6,s10,s14,x4,x5),t1_0,t2_1,s3,t1_4,t2_5,s7,t1_8,t2_9,s11,t1_12,t2_13,s15,x6,x7)
648	
649	def column11_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s5: T.Lane, s6: T.Lane, s7: T.Lane, s9: T.Lane, s10: T.Lane, s11: T.Lane, s13: T.Lane, s14: T.Lane, s15: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
650	  match q:
651	    case T.Q{t1_0,t1_4,t1_8,t1_12}:
652	      column11_2(g(s1,s5,s9,s13,x2,x3),t1_0,s2,s3,t1_4,s6,s7,t1_8,s10,s11,t1_12,s14,s15,x4,x5,x6,x7)
653	
654	# Round 11, G on the four columns: (0,4,8,12), (1,5,9,13), (2,6,10,14), (3,7,11,15).
655	def column11(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
656	  match v:
657	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
658	      column11_1(g(s0,s4,s8,s12,x0,x1),s1,s2,s3,s5,s6,s7,s9,s10,s11,s13,s14,s15,x2,x3,x4,x5,x6,x7)
659	
660	def diagonal11_4(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, t3_2: T.Lane, t1_5: T.Lane, t2_6: T.Lane, t3_7: T.Lane, t3_8: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, t3_13: T.Lane, t1_15: T.Lane) -> T.State:
661	  match q:
662	    case T.Q{t4_3,t4_4,t4_9,t4_14}:
663	      T.V{t1_0,t2_1,t3_2,t4_3,t4_4,t1_5,t2_6,t3_7,t3_8,t4_9,t1_10,t2_11,t2_12,t3_13,t4_14,t1_15}
664	
665	def diagonal11_3(q: T.Quad, t1_0: T.Lane, t2_1: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, t2_6: T.Lane, s9: T.Lane, t1_10: T.Lane, t2_11: T.Lane, t2_12: T.Lane, s14: T.Lane, t1_15: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
666	  match q:
667	    case T.Q{t3_2,t3_7,t3_8,t3_13}:
668	      diagonal11_4(g(s3,s4,s9,s14,x6,x7),t1_0,t2_1,t3_2,t1_5,t2_6,t3_7,t3_8,t1_10,t2_11,t2_12,t3_13,t1_15)
669	
670	def diagonal11_2(q: T.Quad, t1_0: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, t1_5: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, t1_10: T.Lane, s13: T.Lane, s14: T.Lane, t1_15: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
671	  match q:
672	    case T.Q{t2_1,t2_6,t2_11,t2_12}:
673	      diagonal11_3(g(s2,s7,s8,s13,x4,x5),t1_0,t2_1,s3,s4,t1_5,t2_6,s9,t1_10,t2_11,t2_12,s14,t1_15,x6,x7)
674	
675	def diagonal11_1(q: T.Quad, s1: T.Lane, s2: T.Lane, s3: T.Lane, s4: T.Lane, s6: T.Lane, s7: T.Lane, s8: T.Lane, s9: T.Lane, s11: T.Lane, s12: T.Lane, s13: T.Lane, s14: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
676	  match q:
677	    case T.Q{t1_0,t1_5,t1_10,t1_15}:
678	      diagonal11_2(g(s1,s6,s11,s12,x2,x3),t1_0,s2,s3,s4,t1_5,s7,s8,s9,t1_10,s13,s14,t1_15,x4,x5,x6,x7)
679	
680	# Round 11, G on the four diagonals: (0,5,10,15), (1,6,11,12), (2,7,8,13), (3,4,9,14).
681	def diagonal11(v: T.State, x0: T.Lane, x1: T.Lane, x2: T.Lane, x3: T.Lane, x4: T.Lane, x5: T.Lane, x6: T.Lane, x7: T.Lane) -> T.State:
682	  match v:
683	    case T.V{s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15}:
684	      diagonal11_1(g(s0,s5,s10,s15,x0,x1),s1,s2,s3,s4,s6,s7,s8,s9,s11,s12,s13,s14,x2,x3,x4,x5,x6,x7)
685	
686	# Round 11 uses the message schedule SIGMA[1], fixed at compile time.
687	def round11(v: T.State, m0: T.Lane, m1: T.Lane, m2: T.Lane, m3: T.Lane, m4: T.Lane, m5: T.Lane, m6: T.Lane, m7: T.Lane, m8: T.Lane, m9: T.Lane, m10: T.Lane, m11: T.Lane, m12: T.Lane, m13: T.Lane, m14: T.Lane, m15: T.Lane) -> T.State:
688	  diagonal11(column11(v,m14,m10,m4,m8,m9,m15,m13,m6),m1,m12,m0,m2,m11,m7,m5,m3)
689	
690	def rounds(v: T.State, +m0: T.Lane, +m1: T.Lane, +m2: T.Lane, +m3: T.Lane, +m4: T.Lane, +m5: T.Lane, +m6: T.Lane, +m7: T.Lane, +m8: T.Lane, +m9: T.Lane, +m10: T.Lane, +m11: T.Lane, +m12: T.Lane, +m13: T.Lane, +m14: T.Lane, +m15: T.Lane) -> T.State:
691	  round11(round10(round9(round8(round7(round6(round5(round4(round3(round2(round1(round0(v,m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15),m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15)
692	
693	# v = h[0..7] || IV[0..7], v12 ^= t low 64 bits, v13 ^= t high 64 bits; a block that is not the last.
694	def start(h: T.Chain, t: T.Counter) -> T.State:
695	  match h t:
696	    case T.H{h0,h1,h2,h3,h4,h5,h6,h7} T.C{t0,t1,t2,t3}:
697	      T.V{h0,h1,h2,h3,h4,h5,h6,h7,T.W{4089235720,1779033703},T.W{2227873595,3144134277},T.W{4271175723,1013904242},T.W{1595750129,2773480762},L.xor(T.W{2917565137,1359893119},T.W{t0,t1}),L.xor(T.W{725511199,2600822924},T.W{t2,t3}),T.W{4215389547,528734635},T.W{327033209,1541459225}}
698	
699	# v = h[0..7] || IV[0..7], v12 ^= t low 64 bits, v13 ^= t high 64 bits; the last block (v14 inverted).
700	def start_last(h: T.Chain, t: T.Counter) -> T.State:
701	  match h t:
702	    case T.H{h0,h1,h2,h3,h4,h5,h6,h7} T.C{t0,t1,t2,t3}:
703	      T.V{h0,h1,h2,h3,h4,h5,h6,h7,T.W{4089235720,1779033703},T.W{2227873595,3144134277},T.W{4271175723,1013904242},T.W{1595750129,2773480762},L.xor(T.W{2917565137,1359893119},T.W{t0,t1}),L.xor(T.W{725511199,2600822924},T.W{t2,t3}),L.xor(T.W{4215389547,528734635},T.W{4294967295,4294967295}),T.W{327033209,1541459225}}
704	
705	# h[i] ^= v[i] ^ v[i+8].
706	def finish(h: T.Chain, v: T.State) -> T.Chain:
707	  match h v:
708	    case T.H{h0,h1,h2,h3,h4,h5,h6,h7} T.V{v0,v1,v2,v3,v4,v5,v6,v7,v8,v9,v10,v11,v12,v13,v14,v15}:
709	      T.H{L.xor(L.xor(h0,v0),v8),L.xor(L.xor(h1,v1),v9),L.xor(L.xor(h2,v2),v10),L.xor(L.xor(h3,v3),v11),L.xor(L.xor(h4,v4),v12),L.xor(L.xor(h5,v5),v13),L.xor(L.xor(h6,v6),v14),L.xor(L.xor(h7,v7),v15)}
710	
711	# The compression function F on one block of 32 little-endian words.
712	def compress(+h: T.Chain, t: T.Counter, 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, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, w27: U32, w28: U32, w29: U32, w30: U32, w31: U32) -> T.Chain:
713	  finish(h,rounds(start(h,t),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}))
714	
715	# The compression function F on one block of 32 little-endian words.
716	def compress_last(+h: T.Chain, t: T.Counter, 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, w16: U32, w17: U32, w18: U32, w19: U32, w20: U32, w21: U32, w22: U32, w23: U32, w24: U32, w25: U32, w26: U32, w27: U32, w28: U32, w29: U32, w30: U32, w31: U32) -> T.Chain:
717	  finish(h,rounds(start_last(h,t),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}))
718	
719	# t += x on the 128-bit counter.
720	def bump(c: T.Counter, +x: U32) -> T.Counter:
721	  match c:
722	    case T.C{c0,c1,c2,c3}:
723	      +s0 = U32.add(c0,x)
724	      +k0 = Bool.to_u32(U32.is_lt(s0,x))
725	      +s1 = U32.add(c1,k0)
726	      +k1 = Bool.to_u32(U32.is_lt(s1,k0))
727	      +s2 = U32.add(c2,k1)
728	      T.C{s0,s1,s2,U32.add(c3,Bool.to_u32(U32.is_lt(s2,k1)))}