1	import Base
2	import ../../../../src/crypto/blake/blake3/types.bend as T
3	import ../../../../src/crypto/blake/blake3/blake3.bend as K
4	import ../../../../spec/crypto/blake/blake3.bend as S
5	
6	# Generated by tools/generators/blake3/proofs.py.
7	#
8	# The implementation's unrolled block read (read0..read15) equals the
9	# specification's word-gathering loop, step by step, for every array and index;
10	# the implementation's final-block mask equals the specification's zero
11	# padding, for every block and length.
12	
13	law read15_correct:
14	  for +index: U32
15	  for +w0: U32
16	  for +w1: U32
17	  for +w2: U32
18	  for +w3: U32
19	  for +w4: U32
20	  for +w5: U32
21	  for +w6: U32
22	  for +w7: U32
23	  for +w8: U32
24	  for +w9: U32
25	  for +w10: U32
26	  for +w11: U32
27	  for +w12: U32
28	  for +w13: U32
29	  for +w14: U32
30	  for pair: Array<U32> & U32
31	  {K.read15(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair) == S.as_block(S.gather(0n,index,16,[w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : Array<U32> & T.Block}
32	
33	def read15_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair):
34	  (a,w15) = pair
35	  {==}
36	
37	law read14_correct:
38	  for +index: U32
39	  for +w0: U32
40	  for +w1: U32
41	  for +w2: U32
42	  for +w3: U32
43	  for +w4: U32
44	  for +w5: U32
45	  for +w6: U32
46	  for +w7: U32
47	  for +w8: U32
48	  for +w9: U32
49	  for +w10: U32
50	  for +w11: U32
51	  for +w12: U32
52	  for +w13: U32
53	  for pair: Array<U32> & U32
54	  {K.read14(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair) == S.as_block(S.gather(1n,index,15,[w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : Array<U32> & T.Block}
55	
56	def read14_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair):
57	  (a,w14) = pair
58	  read15_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))
59	
60	law read13_correct:
61	  for +index: U32
62	  for +w0: U32
63	  for +w1: U32
64	  for +w2: U32
65	  for +w3: U32
66	  for +w4: U32
67	  for +w5: U32
68	  for +w6: U32
69	  for +w7: U32
70	  for +w8: U32
71	  for +w9: U32
72	  for +w10: U32
73	  for +w11: U32
74	  for +w12: U32
75	  for pair: Array<U32> & U32
76	  {K.read13(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair) == S.as_block(S.gather(2n,index,14,[w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : Array<U32> & T.Block}
77	
78	def read13_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair):
79	  (a,w13) = pair
80	  read14_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))
81	
82	law read12_correct:
83	  for +index: U32
84	  for +w0: U32
85	  for +w1: U32
86	  for +w2: U32
87	  for +w3: U32
88	  for +w4: U32
89	  for +w5: U32
90	  for +w6: U32
91	  for +w7: U32
92	  for +w8: U32
93	  for +w9: U32
94	  for +w10: U32
95	  for +w11: U32
96	  for pair: Array<U32> & U32
97	  {K.read12(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair) == S.as_block(S.gather(3n,index,13,[w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : Array<U32> & T.Block}
98	
99	def read12_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair):
100	  (a,w12) = pair
101	  read13_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))
102	
103	law read11_correct:
104	  for +index: U32
105	  for +w0: U32
106	  for +w1: U32
107	  for +w2: U32
108	  for +w3: U32
109	  for +w4: U32
110	  for +w5: U32
111	  for +w6: U32
112	  for +w7: U32
113	  for +w8: U32
114	  for +w9: U32
115	  for +w10: U32
116	  for pair: Array<U32> & U32
117	  {K.read11(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair) == S.as_block(S.gather(4n,index,12,[w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : Array<U32> & T.Block}
118	
119	def read11_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair):
120	  (a,w11) = pair
121	  read12_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))
122	
123	law read10_correct:
124	  for +index: U32
125	  for +w0: U32
126	  for +w1: U32
127	  for +w2: U32
128	  for +w3: U32
129	  for +w4: U32
130	  for +w5: U32
131	  for +w6: U32
132	  for +w7: U32
133	  for +w8: U32
134	  for +w9: U32
135	  for pair: Array<U32> & U32
136	  {K.read10(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair) == S.as_block(S.gather(5n,index,11,[w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : Array<U32> & T.Block}
137	
138	def read10_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair):
139	  (a,w10) = pair
140	  read11_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))
141	
142	law read9_correct:
143	  for +index: U32
144	  for +w0: U32
145	  for +w1: U32
146	  for +w2: U32
147	  for +w3: U32
148	  for +w4: U32
149	  for +w5: U32
150	  for +w6: U32
151	  for +w7: U32
152	  for +w8: U32
153	  for pair: Array<U32> & U32
154	  {K.read9(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair) == S.as_block(S.gather(6n,index,10,[w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : Array<U32> & T.Block}
155	
156	def read9_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair):
157	  (a,w9) = pair
158	  read10_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))
159	
160	law read8_correct:
161	  for +index: U32
162	  for +w0: U32
163	  for +w1: U32
164	  for +w2: U32
165	  for +w3: U32
166	  for +w4: U32
167	  for +w5: U32
168	  for +w6: U32
169	  for +w7: U32
170	  for pair: Array<U32> & U32
171	  {K.read8(index,w0,w1,w2,w3,w4,w5,w6,w7,pair) == S.as_block(S.gather(7n,index,9,[w7,w6,w5,w4,w3,w2,w1,w0],pair)) : Array<U32> & T.Block}
172	
173	def read8_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,pair):
174	  (a,w8) = pair
175	  read9_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))
176	
177	law read7_correct:
178	  for +index: U32
179	  for +w0: U32
180	  for +w1: U32
181	  for +w2: U32
182	  for +w3: U32
183	  for +w4: U32
184	  for +w5: U32
185	  for +w6: U32
186	  for pair: Array<U32> & U32
187	  {K.read7(index,w0,w1,w2,w3,w4,w5,w6,pair) == S.as_block(S.gather(8n,index,8,[w6,w5,w4,w3,w2,w1,w0],pair)) : Array<U32> & T.Block}
188	
189	def read7_correct(index,w0,w1,w2,w3,w4,w5,w6,pair):
190	  (a,w7) = pair
191	  read8_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))
192	
193	law read6_correct:
194	  for +index: U32
195	  for +w0: U32
196	  for +w1: U32
197	  for +w2: U32
198	  for +w3: U32
199	  for +w4: U32
200	  for +w5: U32
201	  for pair: Array<U32> & U32
202	  {K.read6(index,w0,w1,w2,w3,w4,w5,pair) == S.as_block(S.gather(9n,index,7,[w5,w4,w3,w2,w1,w0],pair)) : Array<U32> & T.Block}
203	
204	def read6_correct(index,w0,w1,w2,w3,w4,w5,pair):
205	  (a,w6) = pair
206	  read7_correct(index,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))
207	
208	law read5_correct:
209	  for +index: U32
210	  for +w0: U32
211	  for +w1: U32
212	  for +w2: U32
213	  for +w3: U32
214	  for +w4: U32
215	  for pair: Array<U32> & U32
216	  {K.read5(index,w0,w1,w2,w3,w4,pair) == S.as_block(S.gather(10n,index,6,[w4,w3,w2,w1,w0],pair)) : Array<U32> & T.Block}
217	
218	def read5_correct(index,w0,w1,w2,w3,w4,pair):
219	  (a,w5) = pair
220	  read6_correct(index,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))
221	
222	law read4_correct:
223	  for +index: U32
224	  for +w0: U32
225	  for +w1: U32
226	  for +w2: U32
227	  for +w3: U32
228	  for pair: Array<U32> & U32
229	  {K.read4(index,w0,w1,w2,w3,pair) == S.as_block(S.gather(11n,index,5,[w3,w2,w1,w0],pair)) : Array<U32> & T.Block}
230	
231	def read4_correct(index,w0,w1,w2,w3,pair):
232	  (a,w4) = pair
233	  read5_correct(index,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))
234	
235	law read3_correct:
236	  for +index: U32
237	  for +w0: U32
238	  for +w1: U32
239	  for +w2: U32
240	  for pair: Array<U32> & U32
241	  {K.read3(index,w0,w1,w2,pair) == S.as_block(S.gather(12n,index,4,[w2,w1,w0],pair)) : Array<U32> & T.Block}
242	
243	def read3_correct(index,w0,w1,w2,pair):
244	  (a,w3) = pair
245	  read4_correct(index,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))
246	
247	law read2_correct:
248	  for +index: U32
249	  for +w0: U32
250	  for +w1: U32
251	  for pair: Array<U32> & U32
252	  {K.read2(index,w0,w1,pair) == S.as_block(S.gather(13n,index,3,[w1,w0],pair)) : Array<U32> & T.Block}
253	
254	def read2_correct(index,w0,w1,pair):
255	  (a,w2) = pair
256	  read3_correct(index,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))
257	
258	law read1_correct:
259	  for +index: U32
260	  for +w0: U32
261	  for pair: Array<U32> & U32
262	  {K.read1(index,w0,pair) == S.as_block(S.gather(14n,index,2,[w0],pair)) : Array<U32> & T.Block}
263	
264	def read1_correct(index,w0,pair):
265	  (a,w1) = pair
266	  read2_correct(index,w0,w1,Array.get(U32,a,U32.add(index,2)))
267	
268	law read0_correct:
269	  for +index: U32
270	  for pair: Array<U32> & U32
271	  {K.read0(index,pair) == S.as_block(S.gather(15n,index,1,Nil{},pair)) : Array<U32> & T.Block}
272	
273	def read0_correct(index,pair):
274	  (a,w0) = pair
275	  read1_correct(index,w0,Array.get(U32,a,U32.add(index,1)))
276	
277	law read_block_correct:
278	  for a: Array<U32>
279	  for +index: U32
280	  {K.read_block(a,index) == S.read_block(a,index) : Array<U32> & T.Block}
281	
282	def read_block_correct(a,index):
283	  read0_correct(index,Array.get(U32,a,index))
284	
285	law partial_low:
286	  for +w: U32
287	  for +d: Nat
288	  {K.partial(w,d) == S.low_bytes(w,Nat.min(4n,d)) : U32}
289	
290	def partial_low(w,d):
291	  match d:
292	    case 0n: {==}
293	    case 1n: {==}
294	    case 2n: {==}
295	    case 3n: {==}
296	    case 4n+q: {==}
297	
298	law mask_keep:
299	  for +w: U32
300	  for +pos: Nat
301	  for +len: Nat
302	  {K.mask(w,pos,len) == S.keep(w,pos,len) : U32}
303	
304	def mask_keep(w,pos,len):
305	  partial_low(w,Nat.sub(len,pos))
306	
307	law mask_block_correct:
308	  for +b: T.Block
309	  for +len: Nat
310	  {K.mask_block(b,len) == S.zero_tail(b,len) : T.Block}
311	
312	def mask_block_correct(b,len):
313	  match b:
314	    case T.B{m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15}:
315	      %mask_keep(m0,0n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{_,S.keep(m1,4n,len),S.keep(m2,8n,len),S.keep(m3,12n,len),S.keep(m4,16n,len),S.keep(m5,20n,len),S.keep(m6,24n,len),S.keep(m7,28n,len),S.keep(m8,32n,len),S.keep(m9,36n,len),S.keep(m10,40n,len),S.keep(m11,44n,len),S.keep(m12,48n,len),S.keep(m13,52n,len),S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
316	      %mask_keep(m1,4n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),_,S.keep(m2,8n,len),S.keep(m3,12n,len),S.keep(m4,16n,len),S.keep(m5,20n,len),S.keep(m6,24n,len),S.keep(m7,28n,len),S.keep(m8,32n,len),S.keep(m9,36n,len),S.keep(m10,40n,len),S.keep(m11,44n,len),S.keep(m12,48n,len),S.keep(m13,52n,len),S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
317	      %mask_keep(m2,8n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),_,S.keep(m3,12n,len),S.keep(m4,16n,len),S.keep(m5,20n,len),S.keep(m6,24n,len),S.keep(m7,28n,len),S.keep(m8,32n,len),S.keep(m9,36n,len),S.keep(m10,40n,len),S.keep(m11,44n,len),S.keep(m12,48n,len),S.keep(m13,52n,len),S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
318	      %mask_keep(m3,12n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),_,S.keep(m4,16n,len),S.keep(m5,20n,len),S.keep(m6,24n,len),S.keep(m7,28n,len),S.keep(m8,32n,len),S.keep(m9,36n,len),S.keep(m10,40n,len),S.keep(m11,44n,len),S.keep(m12,48n,len),S.keep(m13,52n,len),S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
319	      %mask_keep(m4,16n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),_,S.keep(m5,20n,len),S.keep(m6,24n,len),S.keep(m7,28n,len),S.keep(m8,32n,len),S.keep(m9,36n,len),S.keep(m10,40n,len),S.keep(m11,44n,len),S.keep(m12,48n,len),S.keep(m13,52n,len),S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
320	      %mask_keep(m5,20n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),_,S.keep(m6,24n,len),S.keep(m7,28n,len),S.keep(m8,32n,len),S.keep(m9,36n,len),S.keep(m10,40n,len),S.keep(m11,44n,len),S.keep(m12,48n,len),S.keep(m13,52n,len),S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
321	      %mask_keep(m6,24n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),_,S.keep(m7,28n,len),S.keep(m8,32n,len),S.keep(m9,36n,len),S.keep(m10,40n,len),S.keep(m11,44n,len),S.keep(m12,48n,len),S.keep(m13,52n,len),S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
322	      %mask_keep(m7,28n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),_,S.keep(m8,32n,len),S.keep(m9,36n,len),S.keep(m10,40n,len),S.keep(m11,44n,len),S.keep(m12,48n,len),S.keep(m13,52n,len),S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
323	      %mask_keep(m8,32n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),_,S.keep(m9,36n,len),S.keep(m10,40n,len),S.keep(m11,44n,len),S.keep(m12,48n,len),S.keep(m13,52n,len),S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
324	      %mask_keep(m9,36n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),_,S.keep(m10,40n,len),S.keep(m11,44n,len),S.keep(m12,48n,len),S.keep(m13,52n,len),S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
325	      %mask_keep(m10,40n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),_,S.keep(m11,44n,len),S.keep(m12,48n,len),S.keep(m13,52n,len),S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
326	      %mask_keep(m11,44n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),_,S.keep(m12,48n,len),S.keep(m13,52n,len),S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
327	      %mask_keep(m12,48n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),_,S.keep(m13,52n,len),S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
328	      %mask_keep(m13,52n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),_,S.keep(m14,56n,len),S.keep(m15,60n,len)} : T.Block}
329	      %mask_keep(m14,56n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),_,S.keep(m15,60n,len)} : T.Block}
330	      %mask_keep(m15,60n,len) : {T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),K.mask(m15,60n,len)} == T.B{K.mask(m0,0n,len),K.mask(m1,4n,len),K.mask(m2,8n,len),K.mask(m3,12n,len),K.mask(m4,16n,len),K.mask(m5,20n,len),K.mask(m6,24n,len),K.mask(m7,28n,len),K.mask(m8,32n,len),K.mask(m9,36n,len),K.mask(m10,40n,len),K.mask(m11,44n,len),K.mask(m12,48n,len),K.mask(m13,52n,len),K.mask(m14,56n,len),_} : T.Block}
331	      {==}
332	
333	# A full block keeps all 64 bytes.
334	law zero_tail_full:
335	  for +b: T.Block
336	  {S.zero_tail(b,64n) == b : T.Block}
337	
338	def zero_tail_full(b):
339	  match b:
340	    case T.B{m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15}: {==}