proofs/crypto/blake/blake2b/blocks.bend source
proofs/crypto/blake/blake2b/blocks.bend on the hub · documented module
# Generated by tools/generators/blake2b_gen.py; do not edit by hand.import Baseimport ../../../../src/crypto/blake/blake2b/types.bend as Timport ../../../../src/crypto/blake/blake2b/compress.bend as Fimport ../../../../src/crypto/blake/blake2b/blake2b.bend as Iimport ../../../../spec/crypto/blake/blake2b.bend as Simport ./compress.bend as Cimport ./array.bend as Alaw read31_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for +w25: U32 for +w26: U32 for +w27: U32 for +w28: U32 for +w29: U32 for +w30: U32 for pair: Array<U32> & U32 {I.read31(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,pair) == S.gather(0n,index,32,False{},0n,t,h,[w30,w29,w28,w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read31_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,pair): (a,w31) = pair Equal.cong(T.Chain,Array<U32> & T.Chain,x => (a,x),F.compress(h,t,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31),S.compress(h,[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}],t,False{}),C.compress_correct(h,t,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31))law read30_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for +w25: U32 for +w26: U32 for +w27: U32 for +w28: U32 for +w29: U32 for pair: Array<U32> & U32 {I.read30(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,pair) == S.gather(1n,index,31,False{},0n,t,h,[w29,w28,w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read30_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,pair): (a,w30) = pair read31_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,Array.get(U32,a,U32.add(index,31)))law read29_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for +w25: U32 for +w26: U32 for +w27: U32 for +w28: U32 for pair: Array<U32> & U32 {I.read29(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,pair) == S.gather(2n,index,30,False{},0n,t,h,[w28,w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read29_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,pair): (a,w29) = pair read30_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,Array.get(U32,a,U32.add(index,30)))law read28_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for +w25: U32 for +w26: U32 for +w27: U32 for pair: Array<U32> & U32 {I.read28(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,pair) == S.gather(3n,index,29,False{},0n,t,h,[w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read28_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,pair): (a,w28) = pair read29_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,Array.get(U32,a,U32.add(index,29)))law read27_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for +w25: U32 for +w26: U32 for pair: Array<U32> & U32 {I.read27(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,pair) == S.gather(4n,index,28,False{},0n,t,h,[w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read27_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,pair): (a,w27) = pair read28_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,Array.get(U32,a,U32.add(index,28)))law read26_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for +w25: U32 for pair: Array<U32> & U32 {I.read26(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,pair) == S.gather(5n,index,27,False{},0n,t,h,[w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read26_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,pair): (a,w26) = pair read27_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,Array.get(U32,a,U32.add(index,27)))law read25_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for pair: Array<U32> & U32 {I.read25(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,pair) == S.gather(6n,index,26,False{},0n,t,h,[w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read25_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,pair): (a,w25) = pair read26_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,Array.get(U32,a,U32.add(index,26)))law read24_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for pair: Array<U32> & U32 {I.read24(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,pair) == S.gather(7n,index,25,False{},0n,t,h,[w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read24_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,pair): (a,w24) = pair read25_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,Array.get(U32,a,U32.add(index,25)))law read23_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for pair: Array<U32> & U32 {I.read23(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,pair) == S.gather(8n,index,24,False{},0n,t,h,[w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read23_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,pair): (a,w23) = pair read24_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,Array.get(U32,a,U32.add(index,24)))law read22_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for pair: Array<U32> & U32 {I.read22(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,pair) == S.gather(9n,index,23,False{},0n,t,h,[w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read22_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,pair): (a,w22) = pair read23_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,Array.get(U32,a,U32.add(index,23)))law read21_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for pair: Array<U32> & U32 {I.read21(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,pair) == S.gather(10n,index,22,False{},0n,t,h,[w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read21_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,pair): (a,w21) = pair read22_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,Array.get(U32,a,U32.add(index,22)))law read20_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for pair: Array<U32> & U32 {I.read20(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,pair) == S.gather(11n,index,21,False{},0n,t,h,[w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read20_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,pair): (a,w20) = pair read21_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,Array.get(U32,a,U32.add(index,21)))law read19_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for pair: Array<U32> & U32 {I.read19(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,pair) == S.gather(12n,index,20,False{},0n,t,h,[w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read19_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,pair): (a,w19) = pair read20_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,Array.get(U32,a,U32.add(index,20)))law read18_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for pair: Array<U32> & U32 {I.read18(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,pair) == S.gather(13n,index,19,False{},0n,t,h,[w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read18_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,pair): (a,w18) = pair read19_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,Array.get(U32,a,U32.add(index,19)))law read17_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for pair: Array<U32> & U32 {I.read17(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,pair) == S.gather(14n,index,18,False{},0n,t,h,[w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read17_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,pair): (a,w17) = pair read18_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,Array.get(U32,a,U32.add(index,18)))law read16_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for pair: Array<U32> & U32 {I.read16(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,pair) == S.gather(15n,index,17,False{},0n,t,h,[w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read16_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,pair): (a,w16) = pair read17_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,Array.get(U32,a,U32.add(index,17)))law read15_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 {I.read15(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair) == S.gather(16n,index,16,False{},0n,t,h,[w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read15_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair): (a,w15) = pair read16_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,Array.get(U32,a,U32.add(index,16)))law read14_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 {I.read14(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair) == S.gather(17n,index,15,False{},0n,t,h,[w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read14_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair): (a,w14) = pair read15_correct(index,t,h,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 +t: T.Counter for +h: T.Chain 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 {I.read13(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair) == S.gather(18n,index,14,False{},0n,t,h,[w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read13_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair): (a,w13) = pair read14_correct(index,t,h,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 +t: T.Counter for +h: T.Chain 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 {I.read12(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair) == S.gather(19n,index,13,False{},0n,t,h,[w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read12_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair): (a,w12) = pair read13_correct(index,t,h,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 +t: T.Counter for +h: T.Chain 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 {I.read11(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair) == S.gather(20n,index,12,False{},0n,t,h,[w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read11_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair): (a,w11) = pair read12_correct(index,t,h,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 +t: T.Counter for +h: T.Chain 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 {I.read10(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair) == S.gather(21n,index,11,False{},0n,t,h,[w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read10_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair): (a,w10) = pair read11_correct(index,t,h,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 +t: T.Counter for +h: T.Chain 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 {I.read9(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair) == S.gather(22n,index,10,False{},0n,t,h,[w8,w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read9_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair): (a,w9) = pair read10_correct(index,t,h,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 +t: T.Counter for +h: T.Chain 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 {I.read8(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,pair) == S.gather(23n,index,9,False{},0n,t,h,[w7,w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read8_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,pair): (a,w8) = pair read9_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))law read7_correct: for +index: U32 for +t: T.Counter for +h: T.Chain 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 {I.read7(index,t,h,w0,w1,w2,w3,w4,w5,w6,pair) == S.gather(24n,index,8,False{},0n,t,h,[w6,w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read7_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,pair): (a,w7) = pair read8_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))law read6_correct: for +index: U32 for +t: T.Counter for +h: T.Chain for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for +w5: U32 for pair: Array<U32> & U32 {I.read6(index,t,h,w0,w1,w2,w3,w4,w5,pair) == S.gather(25n,index,7,False{},0n,t,h,[w5,w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read6_correct(index,t,h,w0,w1,w2,w3,w4,w5,pair): (a,w6) = pair read7_correct(index,t,h,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))law read5_correct: for +index: U32 for +t: T.Counter for +h: T.Chain for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for pair: Array<U32> & U32 {I.read5(index,t,h,w0,w1,w2,w3,w4,pair) == S.gather(26n,index,6,False{},0n,t,h,[w4,w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read5_correct(index,t,h,w0,w1,w2,w3,w4,pair): (a,w5) = pair read6_correct(index,t,h,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))law read4_correct: for +index: U32 for +t: T.Counter for +h: T.Chain for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for pair: Array<U32> & U32 {I.read4(index,t,h,w0,w1,w2,w3,pair) == S.gather(27n,index,5,False{},0n,t,h,[w3,w2,w1,w0],pair) : Array<U32> & T.Chain}def read4_correct(index,t,h,w0,w1,w2,w3,pair): (a,w4) = pair read5_correct(index,t,h,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))law read3_correct: for +index: U32 for +t: T.Counter for +h: T.Chain for +w0: U32 for +w1: U32 for +w2: U32 for pair: Array<U32> & U32 {I.read3(index,t,h,w0,w1,w2,pair) == S.gather(28n,index,4,False{},0n,t,h,[w2,w1,w0],pair) : Array<U32> & T.Chain}def read3_correct(index,t,h,w0,w1,w2,pair): (a,w3) = pair read4_correct(index,t,h,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))law read2_correct: for +index: U32 for +t: T.Counter for +h: T.Chain for +w0: U32 for +w1: U32 for pair: Array<U32> & U32 {I.read2(index,t,h,w0,w1,pair) == S.gather(29n,index,3,False{},0n,t,h,[w1,w0],pair) : Array<U32> & T.Chain}def read2_correct(index,t,h,w0,w1,pair): (a,w2) = pair read3_correct(index,t,h,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))law read1_correct: for +index: U32 for +t: T.Counter for +h: T.Chain for +w0: U32 for pair: Array<U32> & U32 {I.read1(index,t,h,w0,pair) == S.gather(30n,index,2,False{},0n,t,h,[w0],pair) : Array<U32> & T.Chain}def read1_correct(index,t,h,w0,pair): (a,w1) = pair read2_correct(index,t,h,w0,w1,Array.get(U32,a,U32.add(index,2)))law read0_correct: for +index: U32 for +t: T.Counter for +h: T.Chain for pair: Array<U32> & U32 {I.read0(index,t,h,pair) == S.gather(31n,index,1,False{},0n,t,h,[],pair) : Array<U32> & T.Chain}def read0_correct(index,t,h,pair): (a,w0) = pair read1_correct(index,t,h,w0,Array.get(U32,a,U32.add(index,1)))law absorb_correct: for a: Array<U32> for +index: U32 for +t: T.Counter for +h: T.Chain {I.absorb(a,index,t,h) == S.absorb(a,index,t,h) : Array<U32> & T.Chain}def absorb_correct(a,index,t,h): read0_correct(index,t,h,Array.get(U32,a,index))law keep_correct: for +w: U32 for +n: Nat {I.keep(w,n) == S.keep(w,n) : U32}def keep_correct(w,n): match n: case 0n: {==} case 1n: {==} case 2n: {==} case 3n: {==} case 4n+p: {==}law masks_correct: for +remain: Nat 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for +w25: U32 for +w26: U32 for +w27: U32 for +w28: U32 for +w29: U32 for +w30: U32 for +w31: U32 {[I.mask(w0,0n,remain),I.mask(w1,4n,remain),I.mask(w2,8n,remain),I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>}def masks_correct(remain,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31): %Equal.sym(U32,I.mask(w0,0n,remain),S.mask(w0,0n,remain),keep_correct(w0,Nat.sub(remain,0n))) : {[_,I.mask(w1,4n,remain),I.mask(w2,8n,remain),I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w1,4n,remain),S.mask(w1,4n,remain),keep_correct(w1,Nat.sub(remain,4n))) : {[S.mask(w0,0n,remain),_,I.mask(w2,8n,remain),I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w2,8n,remain),S.mask(w2,8n,remain),keep_correct(w2,Nat.sub(remain,8n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),_,I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w3,12n,remain),S.mask(w3,12n,remain),keep_correct(w3,Nat.sub(remain,12n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),_,I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w4,16n,remain),S.mask(w4,16n,remain),keep_correct(w4,Nat.sub(remain,16n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),_,I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w5,20n,remain),S.mask(w5,20n,remain),keep_correct(w5,Nat.sub(remain,20n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),_,I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w6,24n,remain),S.mask(w6,24n,remain),keep_correct(w6,Nat.sub(remain,24n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),_,I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w7,28n,remain),S.mask(w7,28n,remain),keep_correct(w7,Nat.sub(remain,28n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),_,I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w8,32n,remain),S.mask(w8,32n,remain),keep_correct(w8,Nat.sub(remain,32n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),_,I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w9,36n,remain),S.mask(w9,36n,remain),keep_correct(w9,Nat.sub(remain,36n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),_,I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w10,40n,remain),S.mask(w10,40n,remain),keep_correct(w10,Nat.sub(remain,40n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),_,I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w11,44n,remain),S.mask(w11,44n,remain),keep_correct(w11,Nat.sub(remain,44n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),_,I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w12,48n,remain),S.mask(w12,48n,remain),keep_correct(w12,Nat.sub(remain,48n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),_,I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w13,52n,remain),S.mask(w13,52n,remain),keep_correct(w13,Nat.sub(remain,52n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),_,I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w14,56n,remain),S.mask(w14,56n,remain),keep_correct(w14,Nat.sub(remain,56n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),_,I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w15,60n,remain),S.mask(w15,60n,remain),keep_correct(w15,Nat.sub(remain,60n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),_,I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w16,64n,remain),S.mask(w16,64n,remain),keep_correct(w16,Nat.sub(remain,64n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),_,I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w17,68n,remain),S.mask(w17,68n,remain),keep_correct(w17,Nat.sub(remain,68n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),_,I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w18,72n,remain),S.mask(w18,72n,remain),keep_correct(w18,Nat.sub(remain,72n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),_,I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w19,76n,remain),S.mask(w19,76n,remain),keep_correct(w19,Nat.sub(remain,76n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),_,I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w20,80n,remain),S.mask(w20,80n,remain),keep_correct(w20,Nat.sub(remain,80n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),_,I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w21,84n,remain),S.mask(w21,84n,remain),keep_correct(w21,Nat.sub(remain,84n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),_,I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w22,88n,remain),S.mask(w22,88n,remain),keep_correct(w22,Nat.sub(remain,88n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),_,I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w23,92n,remain),S.mask(w23,92n,remain),keep_correct(w23,Nat.sub(remain,92n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),_,I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w24,96n,remain),S.mask(w24,96n,remain),keep_correct(w24,Nat.sub(remain,96n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),_,I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w25,100n,remain),S.mask(w25,100n,remain),keep_correct(w25,Nat.sub(remain,100n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),_,I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w26,104n,remain),S.mask(w26,104n,remain),keep_correct(w26,Nat.sub(remain,104n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),S.mask(w25,100n,remain),_,I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w27,108n,remain),S.mask(w27,108n,remain),keep_correct(w27,Nat.sub(remain,108n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),S.mask(w25,100n,remain),S.mask(w26,104n,remain),_,I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w28,112n,remain),S.mask(w28,112n,remain),keep_correct(w28,Nat.sub(remain,112n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),S.mask(w25,100n,remain),S.mask(w26,104n,remain),S.mask(w27,108n,remain),_,I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w29,116n,remain),S.mask(w29,116n,remain),keep_correct(w29,Nat.sub(remain,116n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),S.mask(w25,100n,remain),S.mask(w26,104n,remain),S.mask(w27,108n,remain),S.mask(w28,112n,remain),_,I.mask(w30,120n,remain),I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w30,120n,remain),S.mask(w30,120n,remain),keep_correct(w30,Nat.sub(remain,120n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),S.mask(w25,100n,remain),S.mask(w26,104n,remain),S.mask(w27,108n,remain),S.mask(w28,112n,remain),S.mask(w29,116n,remain),_,I.mask(w31,124n,remain)] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} %Equal.sym(U32,I.mask(w31,124n,remain),S.mask(w31,124n,remain),keep_correct(w31,Nat.sub(remain,124n))) : {[S.mask(w0,0n,remain),S.mask(w1,4n,remain),S.mask(w2,8n,remain),S.mask(w3,12n,remain),S.mask(w4,16n,remain),S.mask(w5,20n,remain),S.mask(w6,24n,remain),S.mask(w7,28n,remain),S.mask(w8,32n,remain),S.mask(w9,36n,remain),S.mask(w10,40n,remain),S.mask(w11,44n,remain),S.mask(w12,48n,remain),S.mask(w13,52n,remain),S.mask(w14,56n,remain),S.mask(w15,60n,remain),S.mask(w16,64n,remain),S.mask(w17,68n,remain),S.mask(w18,72n,remain),S.mask(w19,76n,remain),S.mask(w20,80n,remain),S.mask(w21,84n,remain),S.mask(w22,88n,remain),S.mask(w23,92n,remain),S.mask(w24,96n,remain),S.mask(w25,100n,remain),S.mask(w26,104n,remain),S.mask(w27,108n,remain),S.mask(w28,112n,remain),S.mask(w29,116n,remain),S.mask(w30,120n,remain),_] == S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain) : List<&2,U32>} {==}law last31_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for +w25: U32 for +w26: U32 for +w27: U32 for +w28: U32 for +w29: U32 for +w30: U32 for pair: Array<U32> & U32 {I.last31(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(0n,index,32,True{},remain,t,h,[w30,w29,w28,w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last31_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,pair): (a,+w31) = pair Equal.trans(T.Chain,F.compress_last(h,t,I.mask(w0,0n,remain),I.mask(w1,4n,remain),I.mask(w2,8n,remain),I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)),S.compress(h,[T.W{I.mask(w0,0n,remain),I.mask(w1,4n,remain)},T.W{I.mask(w2,8n,remain),I.mask(w3,12n,remain)},T.W{I.mask(w4,16n,remain),I.mask(w5,20n,remain)},T.W{I.mask(w6,24n,remain),I.mask(w7,28n,remain)},T.W{I.mask(w8,32n,remain),I.mask(w9,36n,remain)},T.W{I.mask(w10,40n,remain),I.mask(w11,44n,remain)},T.W{I.mask(w12,48n,remain),I.mask(w13,52n,remain)},T.W{I.mask(w14,56n,remain),I.mask(w15,60n,remain)},T.W{I.mask(w16,64n,remain),I.mask(w17,68n,remain)},T.W{I.mask(w18,72n,remain),I.mask(w19,76n,remain)},T.W{I.mask(w20,80n,remain),I.mask(w21,84n,remain)},T.W{I.mask(w22,88n,remain),I.mask(w23,92n,remain)},T.W{I.mask(w24,96n,remain),I.mask(w25,100n,remain)},T.W{I.mask(w26,104n,remain),I.mask(w27,108n,remain)},T.W{I.mask(w28,112n,remain),I.mask(w29,116n,remain)},T.W{I.mask(w30,120n,remain),I.mask(w31,124n,remain)}],t,True{}),S.compress(h,S.lanes(S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain)),t,True{}), C.compress_last_correct(h,t,I.mask(w0,0n,remain),I.mask(w1,4n,remain),I.mask(w2,8n,remain),I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)), Equal.cong(List<&2,U32>,T.Chain,x => S.compress(h,S.lanes(x),t,True{}),[I.mask(w0,0n,remain),I.mask(w1,4n,remain),I.mask(w2,8n,remain),I.mask(w3,12n,remain),I.mask(w4,16n,remain),I.mask(w5,20n,remain),I.mask(w6,24n,remain),I.mask(w7,28n,remain),I.mask(w8,32n,remain),I.mask(w9,36n,remain),I.mask(w10,40n,remain),I.mask(w11,44n,remain),I.mask(w12,48n,remain),I.mask(w13,52n,remain),I.mask(w14,56n,remain),I.mask(w15,60n,remain),I.mask(w16,64n,remain),I.mask(w17,68n,remain),I.mask(w18,72n,remain),I.mask(w19,76n,remain),I.mask(w20,80n,remain),I.mask(w21,84n,remain),I.mask(w22,88n,remain),I.mask(w23,92n,remain),I.mask(w24,96n,remain),I.mask(w25,100n,remain),I.mask(w26,104n,remain),I.mask(w27,108n,remain),I.mask(w28,112n,remain),I.mask(w29,116n,remain),I.mask(w30,120n,remain),I.mask(w31,124n,remain)],S.trim([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31],0n,remain),masks_correct(remain,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,w31)))law last30_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for +w25: U32 for +w26: U32 for +w27: U32 for +w28: U32 for +w29: U32 for pair: Array<U32> & U32 {I.last30(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(1n,index,31,True{},remain,t,h,[w29,w28,w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last30_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,pair): (a,+w30) = pair last31_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,w30,Array.get(U32,a,U32.add(index,31)))law last29_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for +w25: U32 for +w26: U32 for +w27: U32 for +w28: U32 for pair: Array<U32> & U32 {I.last29(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(2n,index,30,True{},remain,t,h,[w28,w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last29_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,pair): (a,+w29) = pair last30_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,w29,Array.get(U32,a,U32.add(index,30)))law last28_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for +w25: U32 for +w26: U32 for +w27: U32 for pair: Array<U32> & U32 {I.last28(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(3n,index,29,True{},remain,t,h,[w27,w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last28_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,pair): (a,+w28) = pair last29_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,w28,Array.get(U32,a,U32.add(index,29)))law last27_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for +w25: U32 for +w26: U32 for pair: Array<U32> & U32 {I.last27(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(4n,index,28,True{},remain,t,h,[w26,w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last27_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,pair): (a,+w27) = pair last28_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,w27,Array.get(U32,a,U32.add(index,28)))law last26_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for +w25: U32 for pair: Array<U32> & U32 {I.last26(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(5n,index,27,True{},remain,t,h,[w25,w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last26_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,pair): (a,+w26) = pair last27_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,w26,Array.get(U32,a,U32.add(index,27)))law last25_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for +w24: U32 for pair: Array<U32> & U32 {I.last25(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(6n,index,26,True{},remain,t,h,[w24,w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last25_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,pair): (a,+w25) = pair last26_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,w25,Array.get(U32,a,U32.add(index,26)))law last24_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for +w23: U32 for pair: Array<U32> & U32 {I.last24(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(7n,index,25,True{},remain,t,h,[w23,w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last24_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,pair): (a,+w24) = pair last25_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,w24,Array.get(U32,a,U32.add(index,25)))law last23_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for +w22: U32 for pair: Array<U32> & U32 {I.last23(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(8n,index,24,True{},remain,t,h,[w22,w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last23_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,pair): (a,+w23) = pair last24_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,w23,Array.get(U32,a,U32.add(index,24)))law last22_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for +w21: U32 for pair: Array<U32> & U32 {I.last22(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(9n,index,23,True{},remain,t,h,[w21,w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last22_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,pair): (a,+w22) = pair last23_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,w22,Array.get(U32,a,U32.add(index,23)))law last21_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for +w20: U32 for pair: Array<U32> & U32 {I.last21(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(10n,index,22,True{},remain,t,h,[w20,w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last21_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,pair): (a,+w21) = pair last22_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,w21,Array.get(U32,a,U32.add(index,22)))law last20_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for +w19: U32 for pair: Array<U32> & U32 {I.last20(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(11n,index,21,True{},remain,t,h,[w19,w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last20_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,pair): (a,+w20) = pair last21_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,w20,Array.get(U32,a,U32.add(index,21)))law last19_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for +w18: U32 for pair: Array<U32> & U32 {I.last19(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(12n,index,20,True{},remain,t,h,[w18,w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last19_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,pair): (a,+w19) = pair last20_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,w19,Array.get(U32,a,U32.add(index,20)))law last18_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for +w17: U32 for pair: Array<U32> & U32 {I.last18(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(13n,index,19,True{},remain,t,h,[w17,w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last18_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,pair): (a,+w18) = pair last19_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,w18,Array.get(U32,a,U32.add(index,19)))law last17_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for +w16: U32 for pair: Array<U32> & U32 {I.last17(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(14n,index,18,True{},remain,t,h,[w16,w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last17_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,pair): (a,+w17) = pair last18_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,w17,Array.get(U32,a,U32.add(index,18)))law last16_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 +w15: U32 for pair: Array<U32> & U32 {I.last16(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(15n,index,17,True{},remain,t,h,[w15,w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last16_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,pair): (a,+w16) = pair last17_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16,Array.get(U32,a,U32.add(index,17)))law last15_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 {I.last15(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(16n,index,16,True{},remain,t,h,[w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last15_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair): (a,+w15) = pair last16_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,Array.get(U32,a,U32.add(index,16)))law last14_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 {I.last14(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(17n,index,15,True{},remain,t,h,[w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last14_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair): (a,+w14) = pair last15_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))law last13_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 {I.last13(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(18n,index,14,True{},remain,t,h,[w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last13_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair): (a,+w13) = pair last14_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))law last12_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 {I.last12(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(19n,index,13,True{},remain,t,h,[w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last12_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair): (a,+w12) = pair last13_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))law last11_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 {I.last11(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(20n,index,12,True{},remain,t,h,[w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last11_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair): (a,+w11) = pair last12_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))law last10_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 {I.last10(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(21n,index,11,True{},remain,t,h,[w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last10_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair): (a,+w10) = pair last11_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))law last9_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 {I.last9(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(22n,index,10,True{},remain,t,h,[w8,w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last9_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair): (a,+w9) = pair last10_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))law last8_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 {I.last8(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(23n,index,9,True{},remain,t,h,[w7,w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last8_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,pair): (a,+w8) = pair last9_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))law last7_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain 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 {I.last7(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(24n,index,8,True{},remain,t,h,[w6,w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last7_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,pair): (a,+w7) = pair last8_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))law last6_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for +w5: U32 for pair: Array<U32> & U32 {I.last6(remain,index,t,h,w0,w1,w2,w3,w4,w5,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(25n,index,7,True{},remain,t,h,[w5,w4,w3,w2,w1,w0],pair)) : T.Chain}def last6_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,pair): (a,+w6) = pair last7_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))law last5_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for +w4: U32 for pair: Array<U32> & U32 {I.last5(remain,index,t,h,w0,w1,w2,w3,w4,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(26n,index,6,True{},remain,t,h,[w4,w3,w2,w1,w0],pair)) : T.Chain}def last5_correct(remain,index,t,h,w0,w1,w2,w3,w4,pair): (a,+w5) = pair last6_correct(remain,index,t,h,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))law last4_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain for +w0: U32 for +w1: U32 for +w2: U32 for +w3: U32 for pair: Array<U32> & U32 {I.last4(remain,index,t,h,w0,w1,w2,w3,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(27n,index,5,True{},remain,t,h,[w3,w2,w1,w0],pair)) : T.Chain}def last4_correct(remain,index,t,h,w0,w1,w2,w3,pair): (a,+w4) = pair last5_correct(remain,index,t,h,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))law last3_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain for +w0: U32 for +w1: U32 for +w2: U32 for pair: Array<U32> & U32 {I.last3(remain,index,t,h,w0,w1,w2,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(28n,index,4,True{},remain,t,h,[w2,w1,w0],pair)) : T.Chain}def last3_correct(remain,index,t,h,w0,w1,w2,pair): (a,+w3) = pair last4_correct(remain,index,t,h,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))law last2_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain for +w0: U32 for +w1: U32 for pair: Array<U32> & U32 {I.last2(remain,index,t,h,w0,w1,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(29n,index,3,True{},remain,t,h,[w1,w0],pair)) : T.Chain}def last2_correct(remain,index,t,h,w0,w1,pair): (a,+w2) = pair last3_correct(remain,index,t,h,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))law last1_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain for +w0: U32 for pair: Array<U32> & U32 {I.last1(remain,index,t,h,w0,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(30n,index,2,True{},remain,t,h,[w0],pair)) : T.Chain}def last1_correct(remain,index,t,h,w0,pair): (a,+w1) = pair last2_correct(remain,index,t,h,w0,w1,Array.get(U32,a,U32.add(index,2)))law last0_correct: for +remain: Nat for +index: U32 for +t: T.Counter for +h: T.Chain for pair: Array<U32> & U32 {I.last0(remain,index,t,h,pair) == Pair.snd(Array<U32>,T.Chain,S.gather(31n,index,1,True{},remain,t,h,[],pair)) : T.Chain}def last0_correct(remain,index,t,h,pair): (a,+w0) = pair last1_correct(remain,index,t,h,w0,Array.get(U32,a,U32.add(index,1)))law final_correct: for a: Array<U32> for +index: U32 for +remain: Nat for +t: T.Counter for +h: T.Chain {I.final(a,index,remain,t,h) == S.final(a,index,remain,t,h) : T.Chain}def final_correct(a,index,remain,t,h): %Equal.sym(T.Counter,F.bump(t,U32.from_nat(remain)),S.advance(t,U32.from_nat(remain)),C.bump_correct(t,U32.from_nat(remain))) : {I.last0(remain,index,_,h,Array.get(U32,a,index)) == S.final(a,index,remain,t,h) : T.Chain} last0_correct(remain,index,S.advance(t,U32.from_nat(remain)),h,Array.get(U32,a,index))law blocks_step: for +n: Nat for +index: U32 for +remain: Nat for +t: T.Counter for -a: Array<U32> for +h: T.Chain for view: Sigma<&2,&1,A.Tree,z => {a == A.thaw(z) : Array<U32>}> for recurse: @pair: (Array<U32> & T.Chain) -> {I.blocks(n,U32.add(index,32),remain,S.advance(t,128),pair) == S.blocks(n,U32.add(index,32),remain,S.advance(t,128),pair) : T.Chain} {I.blocks(1n+n,index,remain,t,(a,h)) == S.blocks(1n+n,index,remain,t,(a,h)) : T.Chain}def blocks_step(n,index,remain,t,a,h,view,recurse): match view: case Tuple{+tree,pf}: %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {I.blocks(1n+n,index,remain,t,(_,h)) == S.blocks(1n+n,index,remain,t,(_,h)) : T.Chain} %Equal.sym(T.Counter,F.bump(t,128),S.advance(t,128),C.bump_correct(t,128)) : {I.blocks(n,U32.add(index,32),remain,_,I.absorb(A.thaw(tree),index,_,h)) == S.blocks(1n+n,index,remain,t,(A.thaw(tree),h)) : T.Chain} Equal.trans(T.Chain, I.blocks(n,U32.add(index,32),remain,S.advance(t,128),I.absorb(A.thaw(tree),index,S.advance(t,128),h)), S.blocks(n,U32.add(index,32),remain,S.advance(t,128),I.absorb(A.thaw(tree),index,S.advance(t,128),h)), S.blocks(n,U32.add(index,32),remain,S.advance(t,128),S.absorb(A.thaw(tree),index,S.advance(t,128),h)), recurse(I.absorb(A.thaw(tree),index,S.advance(t,128),h)), Equal.cong(Array<U32> & T.Chain,T.Chain,pair => S.blocks(n,U32.add(index,32),remain,S.advance(t,128),pair), I.absorb(A.thaw(tree),index,S.advance(t,128),h),S.absorb(A.thaw(tree),index,S.advance(t,128),h),absorb_correct(A.thaw(tree),index,S.advance(t,128),h)))law blocks_correct: for +n: Nat for +index: U32 for +remain: Nat for +t: T.Counter for pair: Array<U32> & T.Chain {I.blocks(n,index,remain,t,pair) == S.blocks(n,index,remain,t,pair) : T.Chain}def blocks_correct(n,index,remain,t,pair): match n pair: case 0n Tuple{a,h}: final_correct(a,index,remain,t,h) case 1n+p Tuple{a,h}: blocks_step(p,index,remain,t,a,h,A.reify(a),pair => blocks_correct(p,U32.add(index,32),remain,S.advance(t,128),pair))law unchecked_correct: for a: Array<U32> for +length: Nat {I.unchecked(a,length) == S.unchecked(a,length) : T.Chain}def unchecked_correct(a,length): blocks_correct(Nat.div(Nat.sub(length,1n),128n),0,Nat.sub(length,Nat.mul(Nat.div(Nat.sub(length,1n),128n),128n)),T.C{0,0,0,0},(a,I.initial()))law digest_correct: for +h: T.Chain {I.digest(h) == S.digest(h) : Array<U32>}def digest_correct(h): match h: case T.H{T.W{l0,u0},T.W{l1,u1},T.W{l2,u2},T.W{l3,u3},T.W{l4,u4},T.W{l5,u5},T.W{l6,u6},T.W{l7,u7}}: {==}law checked_true_reified: for -a: Array<U32> for +length: Nat for view: Sigma<&2,&1,A.Tree,z => {a == A.thaw(z) : Array<U32>}> {I.checked(True{},a,length) == S.checked(True{},a,length) : Maybe<&1,Array<U32>>}def checked_true_reified(a,length,view): match view: case Tuple{+tree,pf}: %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {I.checked(True{},_,length) == S.checked(True{},_,length) : Maybe<&1,Array<U32>>} Equal.trans(Maybe<&1,Array<U32>>, Some{I.digest(I.unchecked(A.thaw(tree),length))}, Some{I.digest(S.unchecked(A.thaw(tree),length))}, Some{S.digest(S.unchecked(A.thaw(tree),length))}, Equal.cong(T.Chain,Maybe<&1,Array<U32>>,x => Some{I.digest(x)},I.unchecked(A.thaw(tree),length),S.unchecked(A.thaw(tree),length),unchecked_correct(A.thaw(tree),length)), Equal.cong(Array<U32>,Maybe<&1,Array<U32>>,x => Some{x},I.digest(S.unchecked(A.thaw(tree),length)),S.digest(S.unchecked(A.thaw(tree),length)),digest_correct(S.unchecked(A.thaw(tree),length))))law checked_correct: for +valid: Bool for a: Array<U32> for +length: Nat {I.checked(valid,a,length) == S.checked(valid,a,length) : Maybe<&1,Array<U32>>}def checked_correct(valid,a,length): match valid: case False{}: {==} case True{}: checked_true_reified(a,length,A.reify(a))law sized_correct: for +length: Nat for pair: Array<U32> & U32 {I.sized(length,pair) == S.sized(length,pair) : Maybe<&1,Array<U32>>}def sized_correct(length,pair): (a,capacity) = pair checked_correct(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)law blake2b_correct: for words: Array<U32> for +byte_length: Nat {I.blake2b(words,byte_length) == S.blake2b(words,byte_length) : Maybe<&1,Array<U32>>}def blake2b_correct(words,byte_length): sized_correct(byte_length,Array.size(U32,words))