import Base
import ../../../../src/crypto/blake/blake3/types.bend as T
import ../../../../src/crypto/blake/blake3/blake3.bend as K
import ../../../../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}: {==}