proofs/crypto/blake/blake3/read.bend source
proofs/crypto/blake/blake3/read.bend on the hub · documented module
import Baseimport ../../../../src/crypto/blake/blake3/types.bend as Timport ../../../../src/crypto/blake/blake3/blake3.bend as Kimport ../../../../spec/crypto/blake/blake3.bend as S# Generated by tools/generators/blake3/proofs.py.## The implementation's unrolled block read (read0..read15) equals the# specification's word-gathering loop, step by step, for every array and index;# the implementation's final-block mask equals the specification's zero# padding, for every block and length.law read15_correct: for +index: U32 for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for +w5: U32 for +w6: U32 for +w7: U32 for +w8: U32 for +w9: U32 for +w10: U32 for +w11: U32 for +w12: U32 for +w13: U32 for +w14: U32 for pair: Array<U32> & U32 {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}def read15_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair): (a,w15) = pair {==}law read14_correct: for +index: U32 for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for +w5: U32 for +w6: U32 for +w7: U32 for +w8: U32 for +w9: U32 for +w10: U32 for +w11: U32 for +w12: U32 for +w13: U32 for pair: Array<U32> & U32 {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}def read14_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair): (a,w14) = pair 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)))law read13_correct: for +index: U32 for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for +w5: U32 for +w6: U32 for +w7: U32 for +w8: U32 for +w9: U32 for +w10: U32 for +w11: U32 for +w12: U32 for pair: Array<U32> & U32 {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}def read13_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair): (a,w13) = pair 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)))law read12_correct: for +index: U32 for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for +w5: U32 for +w6: U32 for +w7: U32 for +w8: U32 for +w9: U32 for +w10: U32 for +w11: U32 for pair: Array<U32> & U32 {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}def read12_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair): (a,w12) = pair read13_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))law read11_correct: for +index: U32 for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for +w5: U32 for +w6: U32 for +w7: U32 for +w8: U32 for +w9: U32 for +w10: U32 for pair: Array<U32> & U32 {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}def read11_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair): (a,w11) = pair read12_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))law read10_correct: for +index: U32 for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for +w5: U32 for +w6: U32 for +w7: U32 for +w8: U32 for +w9: U32 for pair: Array<U32> & U32 {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}def read10_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair): (a,w10) = pair read11_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))law read9_correct: for +index: U32 for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for +w5: U32 for +w6: U32 for +w7: U32 for +w8: U32 for pair: Array<U32> & U32 {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}def read9_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair): (a,w9) = pair read10_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))law read8_correct: for +index: U32 for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for +w5: U32 for +w6: U32 for +w7: U32 for pair: Array<U32> & U32 {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}def read8_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,pair): (a,w8) = pair read9_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))law read7_correct: for +index: U32 for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for +w5: U32 for +w6: U32 for pair: Array<U32> & U32 {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}def read7_correct(index,w0,w1,w2,w3,w4,w5,w6,pair): (a,w7) = pair read8_correct(index,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))law read6_correct: for +index: U32 for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for +w5: U32 for pair: Array<U32> & U32 {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}def read6_correct(index,w0,w1,w2,w3,w4,w5,pair): (a,w6) = pair read7_correct(index,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))law read5_correct: for +index: U32 for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for pair: Array<U32> & U32 {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}def read5_correct(index,w0,w1,w2,w3,w4,pair): (a,w5) = pair read6_correct(index,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))law read4_correct: for +index: U32 for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for pair: Array<U32> & U32 {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}def read4_correct(index,w0,w1,w2,w3,pair): (a,w4) = pair read5_correct(index,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))law read3_correct: for +index: U32 for +w0: U32 for +w1: U32 for +w2: U32 for pair: Array<U32> & U32 {K.read3(index,w0,w1,w2,pair) == S.as_block(S.gather(12n,index,4,[w2,w1,w0],pair)) : Array<U32> & T.Block}def read3_correct(index,w0,w1,w2,pair): (a,w3) = pair read4_correct(index,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))law read2_correct: for +index: U32 for +w0: U32 for +w1: U32 for pair: Array<U32> & U32 {K.read2(index,w0,w1,pair) == S.as_block(S.gather(13n,index,3,[w1,w0],pair)) : Array<U32> & T.Block}def read2_correct(index,w0,w1,pair): (a,w2) = pair read3_correct(index,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))law read1_correct: for +index: U32 for +w0: U32 for pair: Array<U32> & U32 {K.read1(index,w0,pair) == S.as_block(S.gather(14n,index,2,[w0],pair)) : Array<U32> & T.Block}def read1_correct(index,w0,pair): (a,w1) = pair read2_correct(index,w0,w1,Array.get(U32,a,U32.add(index,2)))law read0_correct: for +index: U32 for pair: Array<U32> & U32 {K.read0(index,pair) == S.as_block(S.gather(15n,index,1,Nil{},pair)) : Array<U32> & T.Block}def read0_correct(index,pair): (a,w0) = pair read1_correct(index,w0,Array.get(U32,a,U32.add(index,1)))law read_block_correct: for a: Array<U32> for +index: U32 {K.read_block(a,index) == S.read_block(a,index) : Array<U32> & T.Block}def read_block_correct(a,index): read0_correct(index,Array.get(U32,a,index))law partial_low: for +w: U32 for +d: Nat {K.partial(w,d) == S.low_bytes(w,Nat.min(4n,d)) : U32}def partial_low(w,d): match d: case 0n: {==} case 1n: {==} case 2n: {==} case 3n: {==} case 4n+q: {==}law mask_keep: for +w: U32 for +pos: Nat for +len: Nat {K.mask(w,pos,len) == S.keep(w,pos,len) : U32}def mask_keep(w,pos,len): partial_low(w,Nat.sub(len,pos))law mask_block_correct: for +b: T.Block for +len: Nat {K.mask_block(b,len) == S.zero_tail(b,len) : T.Block}def mask_block_correct(b,len): match b: case T.B{m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15}: %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} {==}# A full block keeps all 64 bytes.law zero_tail_full: for +b: T.Block {S.zero_tail(b,64n) == b : T.Block}def zero_tail_full(b): match b: case T.B{m0,m1,m2,m3,m4,m5,m6,m7,m8,m9,m10,m11,m12,m13,m14,m15}: {==}