proofs/crypto/blake/blake3/read.bend

bend-collections-laws-crypto@1.0.0.0 · 340 lines · 21 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as K
4import bend-collections-laws-crypto@1.0.0.0/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
13law 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
33def 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
37law 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
56def 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
60law 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
78def 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
82law 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
99def 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
103law 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
119def 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
123law 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
138def 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
142law 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
156def 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
160law 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
173def 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
177law 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
189def 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
193law 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
204def 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
208law 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
218def 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
222law 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
231def 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
235law 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
243def 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
247law 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
254def 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
258law 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
264def read1_correct(index,w0,pair):
265  (a,w1) = pair
266  read2_correct(index,w0,w1,Array.get(U32,a,U32.add(index,2)))
267
268law 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
273def read0_correct(index,pair):
274  (a,w0) = pair
275  read1_correct(index,w0,Array.get(U32,a,U32.add(index,1)))
276
277law 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
282def read_block_correct(a,index):
283  read0_correct(index,Array.get(U32,a,index))
284
285law 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
290def partial_low(w,d):
291  match d:
292    case 0n: {==}
293    case 1n: {==}
294    case 2n: {==}
295    case 3n: {==}
296    case 4n+q: {==}
297
298law 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
304def mask_keep(w,pos,len):
305  partial_low(w,Nat.sub(len,pos))
306
307law 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
312def 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.
334law zero_tail_full:
335  for +b: T.Block
336  {S.zero_tail(b,64n) == b : T.Block}
337
338def 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}: {==}