Hash.hash_eq: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend as Hash
Lines 79-90 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend&start_line=79&end_line=90

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/blake2b.bend as IB
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend as IH
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend as SBL
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/blocks.bend as BB

def hash_eq(+nn: Nat, +bs: List<&2, U32>) -> {IH.hash(nn, bs) == SA.hash(nn, bs) : List<&2, U32>}:
  +ll = List.length(&2, U32, bs)
  +n = Nat.div(Nat.sub(ll, 1n), 128n)
  +rem = Nat.sub(ll, Nat.mul(n, 128n))
  +f = U32.from_nat(nn)
  Equal.trans(List<&2, U32>, List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (IH.pack(bs), IH.initial(f)))), nn), List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))), nn), SA.hash(nn, bs),
    Equal.trans(List<&2, U32>, List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (IH.pack(bs), IH.initial(f)))), nn), List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), IH.initial(f)))), nn), List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))), nn),
      Equal.cong(Array<U32>, List<&2, U32>, z => List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (z, IH.initial(f)))), nn), IH.pack(bs), SA.pack(bs), pack_eq(bs)),
      Equal.cong(T.Chain, List<&2, U32>, z => List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), z))), nn), IH.initial(f), SA.initial(f), initial_eq(f))),
    Equal.trans(List<&2, U32>, List.take(&2, U32, IH.chain_bytes(IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))), nn), List.take(&2, U32, IH.chain_bytes(SBL.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))), nn), SA.hash(nn, bs),
      Equal.cong(T.Chain, List<&2, U32>, z => List.take(&2, U32, IH.chain_bytes(z), nn), IB.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f))), SBL.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f))), BB.blocks_correct(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))),
      Equal.cong(List<&2, U32>, List<&2, U32>, z => List.take(&2, U32, z, nn), IH.chain_bytes(SBL.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))), SA.chain_bytes(SBL.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))), chain_bytes_eq(SBL.blocks(n, 0, rem, T.C{0, 0, 0, 0}, (SA.pack(bs), SA.initial(f)))))))

Uses (29):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.take
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend&name=chain_bytes_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend&name=initial_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend&name=pack_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/blocks.bend&name=blocks_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=chain_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=hash
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=initial
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend&name=blocks
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/blake2b.bend&name=blocks
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend&name=chain_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend&name=hash
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend&name=initial
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend&name=Chain
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend&name=Counter