# Generated by tools/generators/blake2s_gen.py; do not edit.
# Block reads, the last block, the block loop and the public API.
# The implementation keeps its own copy of the counter carry; each lemma
# carries the spec-side high counter half u1 with a proof e : t1 == u1.
import Base
import ../../../../src/crypto/blake/blake2s/types.bend as T
import ../../../../src/crypto/blake/blake2s/compress.bend as C
import ../../../../src/crypto/blake/blake2s/blake2s.bend as K
import ../../../../spec/crypto/blake/blake2s.bend as R
import ./compress.bend as P
import ./bytes.bend as B
import ./array.bend as A

law carry_correct:
  for +c: Bool
  for +hi: U32
  {K.carry(c,hi) == R.carry(c,hi) : U32}

def carry_correct(c,hi):
  match c:
    case True{}: {==}
    case False{}: {==}

law count_correct:
  for +lo: U32
  for +hi: U32
  for +n: U32
  {K.count_hi(lo,hi,n) == R.count_hi(lo,hi,n) : U32}

def count_correct(lo,hi,n):
  carry_correct(U32.is_lt(U32.add(lo,n),n),hi)

law block_correct:
  for +h: T.State
  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 +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  {C.compress(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,False{}) == R.compress(10n,h,R.words(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15])),t0,u1,False{}) : T.State}

def block_correct(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,u1,e):
  %e : {C.compress(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,False{}) == R.compress(10n,h,R.words(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15])),t0,_,False{}) : T.State}
  Equal.trans(T.State,C.compress(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,False{}),R.compress(10n,h,[w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15],t0,t1,False{}),R.compress(10n,h,R.words(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15])),t0,t1,False{}),
    P.compress_correct(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,False{}),
    Equal.cong(List<&2,U32>,T.State,l => R.compress(10n,h,l,t0,t1,False{}),[w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15],R.words(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15])),Equal.sym(List<&2,U32>,R.words(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15])),[w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15],B.words_serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15]))))

law last_correct:
  for +remain: Nat
  for +h: T.State
  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 +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  {C.compress(h,K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),t0,t1,True{}) == R.compress(10n,h,R.words(R.pad(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15]),0n,remain)),t0,u1,True{}) : T.State}

def last_correct(remain,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,u1,e):
  %e : {C.compress(h,K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),t0,t1,True{}) == R.compress(10n,h,R.words(R.pad(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15]),0n,remain)),t0,_,True{}) : T.State}
  Equal.trans(T.State,C.compress(h,K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),t0,t1,True{}),R.compress(10n,h,[K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain)],t0,t1,True{}),R.compress(10n,h,R.words(R.pad(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15]),0n,remain)),t0,t1,True{}),
    P.compress_correct(h,K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain),t0,t1,True{}),
    Equal.cong(List<&2,U32>,T.State,l => R.compress(10n,h,l,t0,t1,True{}),[K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain)],R.words(R.pad(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15]),0n,remain)),Equal.sym(List<&2,U32>,R.words(R.pad(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15]),0n,remain)),[K.pad_word(w0,0n,remain),K.pad_word(w1,4n,remain),K.pad_word(w2,8n,remain),K.pad_word(w3,12n,remain),K.pad_word(w4,16n,remain),K.pad_word(w5,20n,remain),K.pad_word(w6,24n,remain),K.pad_word(w7,28n,remain),K.pad_word(w8,32n,remain),K.pad_word(w9,36n,remain),K.pad_word(w10,40n,remain),K.pad_word(w11,44n,remain),K.pad_word(w12,48n,remain),K.pad_word(w13,52n,remain),K.pad_word(w14,56n,remain),K.pad_word(w15,60n,remain)],B.words_pad([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15],0n,remain))))

law read15_correct:
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair) == R.full_block(10n,R.gather(0n,index,16,[w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read15_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair):
  (a,w15) = pair
  Equal.cong(T.State,Array<U32> & T.State,s => (a,s),C.compress(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,False{}),R.compress(10n,h,R.words(R.serialize([w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15])),t0,u1,False{}),block_correct(h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,u1,e))

law read14_correct:
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair) == R.full_block(10n,R.gather(1n,index,15,[w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read14_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair):
  (a,w14) = pair
  read15_correct(index,h,t0,t1,u1,e,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 +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair) == R.full_block(10n,R.gather(2n,index,14,[w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read13_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair):
  (a,w13) = pair
  read14_correct(index,h,t0,t1,u1,e,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 +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair) == R.full_block(10n,R.gather(3n,index,13,[w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read12_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair):
  (a,w12) = pair
  read13_correct(index,h,t0,t1,u1,e,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 +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair) == R.full_block(10n,R.gather(4n,index,12,[w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read11_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair):
  (a,w11) = pair
  read12_correct(index,h,t0,t1,u1,e,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 +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair) == R.full_block(10n,R.gather(5n,index,11,[w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read10_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair):
  (a,w10) = pair
  read11_correct(index,h,t0,t1,u1,e,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 +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair) == R.full_block(10n,R.gather(6n,index,10,[w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read9_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair):
  (a,w9) = pair
  read10_correct(index,h,t0,t1,u1,e,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 +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,pair) == R.full_block(10n,R.gather(7n,index,9,[w7,w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read8_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,pair):
  (a,w8) = pair
  read9_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))

law read7_correct:
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,pair) == R.full_block(10n,R.gather(8n,index,8,[w6,w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read7_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,pair):
  (a,w7) = pair
  read8_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))

law read6_correct:
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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,h,t0,t1,w0,w1,w2,w3,w4,w5,pair) == R.full_block(10n,R.gather(9n,index,7,[w5,w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read6_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,pair):
  (a,w6) = pair
  read7_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))

law read5_correct:
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  for +w0: U32
  for +w1: U32
  for +w2: U32
  for +w3: U32
  for +w4: U32
  for pair: Array<U32> & U32
  {K.read5(index,h,t0,t1,w0,w1,w2,w3,w4,pair) == R.full_block(10n,R.gather(10n,index,6,[w4,w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read5_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,pair):
  (a,w5) = pair
  read6_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))

law read4_correct:
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  for +w0: U32
  for +w1: U32
  for +w2: U32
  for +w3: U32
  for pair: Array<U32> & U32
  {K.read4(index,h,t0,t1,w0,w1,w2,w3,pair) == R.full_block(10n,R.gather(11n,index,5,[w3,w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read4_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,pair):
  (a,w4) = pair
  read5_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))

law read3_correct:
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  for +w0: U32
  for +w1: U32
  for +w2: U32
  for pair: Array<U32> & U32
  {K.read3(index,h,t0,t1,w0,w1,w2,pair) == R.full_block(10n,R.gather(12n,index,4,[w2,w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read3_correct(index,h,t0,t1,u1,e,w0,w1,w2,pair):
  (a,w3) = pair
  read4_correct(index,h,t0,t1,u1,e,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))

law read2_correct:
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  for +w0: U32
  for +w1: U32
  for pair: Array<U32> & U32
  {K.read2(index,h,t0,t1,w0,w1,pair) == R.full_block(10n,R.gather(13n,index,3,[w1,w0],pair),h,t0,u1) : Array<U32> & T.State}

def read2_correct(index,h,t0,t1,u1,e,w0,w1,pair):
  (a,w2) = pair
  read3_correct(index,h,t0,t1,u1,e,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))

law read1_correct:
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  for +w0: U32
  for pair: Array<U32> & U32
  {K.read1(index,h,t0,t1,w0,pair) == R.full_block(10n,R.gather(14n,index,2,[w0],pair),h,t0,u1) : Array<U32> & T.State}

def read1_correct(index,h,t0,t1,u1,e,w0,pair):
  (a,w1) = pair
  read2_correct(index,h,t0,t1,u1,e,w0,w1,Array.get(U32,a,U32.add(index,2)))

law read0_correct:
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  for pair: Array<U32> & U32
  {K.read0(index,h,t0,t1,pair) == R.full_block(10n,R.gather(15n,index,1,[],pair),h,t0,u1) : Array<U32> & T.State}

def read0_correct(index,h,t0,t1,u1,e,pair):
  (a,w0) = pair
  read1_correct(index,h,t0,t1,u1,e,w0,Array.get(U32,a,U32.add(index,1)))

law pad15_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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.pad15(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair) == R.last_block(10n,R.gather(0n,index,16,[w14,w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}

def pad15_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,pair):
  (a,w15) = pair
  last_correct(remain,h,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,t0,t1,u1,e)

law pad14_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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.pad14(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair) == R.last_block(10n,R.gather(1n,index,15,[w13,w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}

def pad14_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,pair):
  (a,w14) = pair
  pad15_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,Array.get(U32,a,U32.add(index,15)))

law pad13_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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.pad13(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair) == R.last_block(10n,R.gather(2n,index,14,[w12,w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}

def pad13_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,pair):
  (a,w13) = pair
  pad14_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,Array.get(U32,a,U32.add(index,14)))

law pad12_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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.pad12(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair) == R.last_block(10n,R.gather(3n,index,13,[w11,w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}

def pad12_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,pair):
  (a,w12) = pair
  pad13_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,Array.get(U32,a,U32.add(index,13)))

law pad11_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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.pad11(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair) == R.last_block(10n,R.gather(4n,index,12,[w10,w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}

def pad11_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,pair):
  (a,w11) = pair
  pad12_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,Array.get(U32,a,U32.add(index,12)))

law pad10_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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.pad10(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair) == R.last_block(10n,R.gather(5n,index,11,[w9,w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}

def pad10_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,pair):
  (a,w10) = pair
  pad11_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,Array.get(U32,a,U32.add(index,11)))

law pad9_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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.pad9(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair) == R.last_block(10n,R.gather(6n,index,10,[w8,w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}

def pad9_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,pair):
  (a,w9) = pair
  pad10_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,Array.get(U32,a,U32.add(index,10)))

law pad8_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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.pad8(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,w7,pair) == R.last_block(10n,R.gather(7n,index,9,[w7,w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}

def pad8_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,pair):
  (a,w8) = pair
  pad9_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,w8,Array.get(U32,a,U32.add(index,9)))

law pad7_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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.pad7(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,w6,pair) == R.last_block(10n,R.gather(8n,index,8,[w6,w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}

def pad7_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,pair):
  (a,w7) = pair
  pad8_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,w7,Array.get(U32,a,U32.add(index,8)))

law pad6_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : 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.pad6(remain,index,h,t0,t1,w0,w1,w2,w3,w4,w5,pair) == R.last_block(10n,R.gather(9n,index,7,[w5,w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}

def pad6_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,pair):
  (a,w6) = pair
  pad7_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,w6,Array.get(U32,a,U32.add(index,7)))

law pad5_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  for +w0: U32
  for +w1: U32
  for +w2: U32
  for +w3: U32
  for +w4: U32
  for pair: Array<U32> & U32
  {K.pad5(remain,index,h,t0,t1,w0,w1,w2,w3,w4,pair) == R.last_block(10n,R.gather(10n,index,6,[w4,w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}

def pad5_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,pair):
  (a,w5) = pair
  pad6_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,w5,Array.get(U32,a,U32.add(index,6)))

law pad4_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  for +w0: U32
  for +w1: U32
  for +w2: U32
  for +w3: U32
  for pair: Array<U32> & U32
  {K.pad4(remain,index,h,t0,t1,w0,w1,w2,w3,pair) == R.last_block(10n,R.gather(11n,index,5,[w3,w2,w1,w0],pair),remain,h,t0,u1) : T.State}

def pad4_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,pair):
  (a,w4) = pair
  pad5_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,w4,Array.get(U32,a,U32.add(index,5)))

law pad3_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  for +w0: U32
  for +w1: U32
  for +w2: U32
  for pair: Array<U32> & U32
  {K.pad3(remain,index,h,t0,t1,w0,w1,w2,pair) == R.last_block(10n,R.gather(12n,index,4,[w2,w1,w0],pair),remain,h,t0,u1) : T.State}

def pad3_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,pair):
  (a,w3) = pair
  pad4_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,w3,Array.get(U32,a,U32.add(index,4)))

law pad2_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  for +w0: U32
  for +w1: U32
  for pair: Array<U32> & U32
  {K.pad2(remain,index,h,t0,t1,w0,w1,pair) == R.last_block(10n,R.gather(13n,index,3,[w1,w0],pair),remain,h,t0,u1) : T.State}

def pad2_correct(remain,index,h,t0,t1,u1,e,w0,w1,pair):
  (a,w2) = pair
  pad3_correct(remain,index,h,t0,t1,u1,e,w0,w1,w2,Array.get(U32,a,U32.add(index,3)))

law pad1_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  for +w0: U32
  for pair: Array<U32> & U32
  {K.pad1(remain,index,h,t0,t1,w0,pair) == R.last_block(10n,R.gather(14n,index,2,[w0],pair),remain,h,t0,u1) : T.State}

def pad1_correct(remain,index,h,t0,t1,u1,e,w0,pair):
  (a,w1) = pair
  pad2_correct(remain,index,h,t0,t1,u1,e,w0,w1,Array.get(U32,a,U32.add(index,2)))

law pad0_correct:
  for +remain: Nat
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  for pair: Array<U32> & U32
  {K.pad0(remain,index,h,t0,t1,pair) == R.last_block(10n,R.gather(15n,index,1,[],pair),remain,h,t0,u1) : T.State}

def pad0_correct(remain,index,h,t0,t1,u1,e,pair):
  (a,w0) = pair
  pad1_correct(remain,index,h,t0,t1,u1,e,w0,Array.get(U32,a,U32.add(index,1)))

law absorb_correct:
  for a: Array<U32>
  for +index: U32
  for +h: T.State
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  {K.absorb(a,index,h,t0,t1) == R.absorb(10n,a,index,h,t0,u1) : Array<U32> & T.State}

def absorb_correct(a,index,h,t0,t1,u1,e):
  read0_correct(index,h,t0,t1,u1,e,Array.get(U32,a,index))

law finish_correct:
  for a: Array<U32>
  for +index: U32
  for +t0: U32
  for +t1: U32
  for +remain: Nat
  for +h: T.State
  {K.finish(a,index,t0,t1,remain,h) == R.finish(10n,a,index,t0,t1,remain,h) : T.State}

def finish_correct(a,index,t0,t1,remain,h):
  pad0_correct(remain,index,h,U32.add(t0,U32.from_nat(remain)),K.count_hi(t0,t1,U32.from_nat(remain)),R.count_hi(t0,t1,U32.from_nat(remain)),count_correct(t0,t1,U32.from_nat(remain)),Array.get(U32,a,index))

law blocks_step:
  for +n: Nat
  for +index: U32
  for +t0: U32
  for +t1: U32
  for +remain: Nat
  for -a: Array<U32>
  for +h: T.State
  for view: Sigma<&2,&1,A.Tree,t => {a == A.thaw(t) : Array<U32>}>
  for recurse: @pair: (Array<U32> & T.State) -> {K.blocks(n,U32.add(index,16),U32.add(t0,64),K.count_hi(t0,t1,64),remain,pair) == R.blocks(10n,n,U32.add(index,16),U32.add(t0,64),R.count_hi(t0,t1,64),remain,pair) : T.State}
  {K.blocks(1n+n,index,t0,t1,remain,(a,h)) == R.blocks(10n,1n+n,index,t0,t1,remain,(a,h)) : T.State}

def blocks_step(n,index,t0,t1,remain,a,h,view,recurse):
  match view:
    case Tuple{+tree,pf}:
      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.blocks(1n+n,index,t0,t1,remain,(_,h)) == R.blocks(10n,1n+n,index,t0,t1,remain,(_,h)) : T.State}
      Equal.trans(T.State,
        K.blocks(n,U32.add(index,16),U32.add(t0,64),K.count_hi(t0,t1,64),remain,K.absorb(A.thaw(tree),index,h,U32.add(t0,64),K.count_hi(t0,t1,64))),
        R.blocks(10n,n,U32.add(index,16),U32.add(t0,64),R.count_hi(t0,t1,64),remain,K.absorb(A.thaw(tree),index,h,U32.add(t0,64),K.count_hi(t0,t1,64))),
        R.blocks(10n,n,U32.add(index,16),U32.add(t0,64),R.count_hi(t0,t1,64),remain,R.absorb(10n,A.thaw(tree),index,h,U32.add(t0,64),R.count_hi(t0,t1,64))),
        recurse(K.absorb(A.thaw(tree),index,h,U32.add(t0,64),K.count_hi(t0,t1,64))),
        Equal.cong(Array<U32> & T.State,T.State,pair => R.blocks(10n,n,U32.add(index,16),U32.add(t0,64),R.count_hi(t0,t1,64),remain,pair),K.absorb(A.thaw(tree),index,h,U32.add(t0,64),K.count_hi(t0,t1,64)),R.absorb(10n,A.thaw(tree),index,h,U32.add(t0,64),R.count_hi(t0,t1,64)),absorb_correct(A.thaw(tree),index,h,U32.add(t0,64),K.count_hi(t0,t1,64),R.count_hi(t0,t1,64),count_correct(t0,t1,64))))

law blocks_correct:
  for +n: Nat
  for +index: U32
  for +t0: U32
  for +t1: U32
  for +u1: U32
  for e: {t1 == u1 : U32}
  for +remain: Nat
  for pair: Array<U32> & T.State
  {K.blocks(n,index,t0,t1,remain,pair) == R.blocks(10n,n,index,t0,u1,remain,pair) : T.State}

def blocks_correct(n,index,t0,t1,u1,e,remain,pair):
  match n pair:
    case 0n Tuple{a,h}:
      %e : {K.blocks(0n,index,t0,t1,remain,(a,h)) == R.blocks(10n,0n,index,t0,_,remain,(a,h)) : T.State}
      finish_correct(a,index,t0,t1,remain,h)
    case 1n+p Tuple{a,h}:
      %e : {K.blocks(1n+p,index,t0,t1,remain,(a,h)) == R.blocks(10n,1n+p,index,t0,_,remain,(a,h)) : T.State}
      blocks_step(p,index,t0,t1,remain,a,h,A.reify(a),pair => blocks_correct(p,U32.add(index,16),U32.add(t0,64),K.count_hi(t0,t1,64),R.count_hi(t0,t1,64),count_correct(t0,t1,64),remain,pair))

law leading_correct:
  for +length: Nat
  {K.leading(length) == Nat.sub(R.block_count(length),1n) : Nat}

def leading_correct(length):
  match length:
    case 0n: {==}
    case 1n+p: {==}

law hash_tail:
  for -a: Array<U32>
  for +length: Nat
  {R.blocks(10n,K.leading(length),0,0,0,Nat.sub(length,Nat.mul(64n,K.leading(length))),(a,K.initial())) == R.hash(10n,a,length) : T.State}

def hash_tail(a,length):
  %leading_correct(length) : {R.blocks(10n,K.leading(length),0,0,0,Nat.sub(length,Nat.mul(64n,K.leading(length))),(a,K.initial())) == R.blocks(10n,_,0,0,0,Nat.sub(length,Nat.mul(64n,_)),(a,R.initial())) : T.State}
  {==}

law unchecked_correct:
  for a: Array<U32>
  for +length: Nat
  {K.unchecked(a,length) == R.hash(10n,a,length) : T.State}

def unchecked_correct(a,length):
  Equal.trans(T.State,K.unchecked(a,length),R.blocks(10n,K.leading(length),0,0,0,Nat.sub(length,Nat.mul(64n,K.leading(length))),(a,K.initial())),R.hash(10n,a,length),
    blocks_correct(K.leading(length),0,0,0,0,{==},Nat.sub(length,Nat.mul(64n,K.leading(length))),(a,K.initial())),
    hash_tail(a,length))

law digest_correct:
  for +h: T.State
  {K.digest(h) == R.digest(h) : Array<U32>}

def digest_correct(h):
  match h:
    case T.H{h0,h1,h2,h3,h4,h5,h6,h7}: {==}

law checked_true:
  for -a: Array<U32>
  for +length: Nat
  for view: Sigma<&2,&1,A.Tree,t => {a == A.thaw(t) : Array<U32>}>
  {K.checked(True{},a,length) == R.checked(10n,True{},a,length) : Maybe<&1,Array<U32>>}

def checked_true(a,length,view):
  match view:
    case Tuple{+tree,pf}:
      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.checked(True{},_,length) == R.checked(10n,True{},_,length) : Maybe<&1,Array<U32>>}
      Equal.trans(Maybe<&1,Array<U32>>,
        Some{K.digest(K.unchecked(A.thaw(tree),length))},
        Some{K.digest(R.hash(10n,A.thaw(tree),length))},
        Some{R.digest(R.hash(10n,A.thaw(tree),length))},
        Equal.cong(T.State,Maybe<&1,Array<U32>>,s => Some{K.digest(s)},K.unchecked(A.thaw(tree),length),R.hash(10n,A.thaw(tree),length),unchecked_correct(A.thaw(tree),length)),
        Equal.cong(Array<U32>,Maybe<&1,Array<U32>>,d => Some{d},K.digest(R.hash(10n,A.thaw(tree),length)),R.digest(R.hash(10n,A.thaw(tree),length)),digest_correct(R.hash(10n,A.thaw(tree),length))))

law checked_correct:
  for +valid: Bool
  for a: Array<U32>
  for +length: Nat
  {K.checked(valid,a,length) == R.checked(10n,valid,a,length) : Maybe<&1,Array<U32>>}

def checked_correct(valid,a,length):
  match valid:
    case False{}: {==}
    case True{}: checked_true(a,length,A.reify(a))

law sized_correct:
  for +length: Nat
  for pair: Array<U32> & U32
  {K.sized(length,pair) == R.sized(10n,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 blake2s_correct:
  for a: Array<U32>
  for +length: Nat
  {K.blake2s(a,length) == R.blake2s(a,length) : Maybe<&1,Array<U32>>}

def blake2s_correct(a,length):
  sized_correct(length,Array.size(U32,a))