src/crypto/blake/blake2b/compress.bend

bend-collections-laws-crypto@1.0.0.0 · 728 lines · 140 definitions

1# Generated by tools/generators/blake2b_gen.py; do not edit by hand.
2import Base
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/lane.bend as L
5
6# G (RFC 7693 section 3.1) on four words and two message words.
7def 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
18def 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
23def 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
28def 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
33def 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).
39def 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
44def 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
49def 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
54def 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
59def 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).
65def 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.
71def 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
74def 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
79def 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
84def 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
89def 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).
95def 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
100def 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
105def 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
110def 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
115def 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).
121def 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.
127def 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
130def 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
135def 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
140def 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
145def 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).
151def 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
156def 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
161def 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
166def 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
171def 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).
177def 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.
183def 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
186def 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
191def 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
196def 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
201def 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).
207def 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
212def 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
217def 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
222def 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
227def 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).
233def 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.
239def 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
242def 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
247def 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
252def 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
257def 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).
263def 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
268def 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
273def 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
278def 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
283def 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).
289def 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.
295def 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
298def 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
303def 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
308def 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
313def 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).
319def 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
324def 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
329def 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
334def 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
339def 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).
345def 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.
351def 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
354def 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
359def 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
364def 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
369def 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).
375def 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
380def 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
385def 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
390def 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
395def 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).
401def 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.
407def 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
410def 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
415def 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
420def 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
425def 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).
431def 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
436def 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
441def 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
446def 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
451def 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).
457def 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.
463def 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
466def 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
471def 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
476def 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
481def 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).
487def 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
492def 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
497def 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
502def 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
507def 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).
513def 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.
519def 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
522def 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
527def 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
532def 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
537def 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).
543def 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
548def 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
553def 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
558def 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
563def 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).
569def 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.
575def 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
578def 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
583def 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
588def 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
593def 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).
599def 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
604def 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
609def 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
614def 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
619def 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).
625def 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.
631def 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
634def 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
639def 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
644def 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
649def 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).
655def 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
660def 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
665def 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
670def 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
675def 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).
681def 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.
687def 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
690def 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.
694def 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).
700def 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].
706def 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.
712def 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.
716def 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.
720def 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)))}