Hash.pack_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 64-67 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=64&end_line=67

import Base
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/argon2/argon2.bend as SA

def pack_eq(+bs: List<&2, U32>) -> {IH.pack(bs) == SA.pack(bs) : Array<U32>}:
  Equal.trans(Array<U32>, IH.fill(IH.words(bs), 0, Array.new(U32, IH.depth_go(32n, List.length(&2, U32, IH.words(bs)), 0n, Nat.is_le(List.length(&2, U32, IH.words(bs)), 1n)), 0)), IH.fill(SA.words(bs), 0, Array.new(U32, IH.depth_go(32n, List.length(&2, U32, SA.words(bs)), 0n, Nat.is_le(List.length(&2, U32, SA.words(bs)), 1n)), 0)), SA.pack(bs),
    Equal.cong(List<&2, U32>, Array<U32>, +z => IH.fill(z, 0, Array.new(U32, IH.depth_go(32n, List.length(&2, U32, z), 0n, Nat.is_le(List.length(&2, U32, z), 1n)), 0)), IH.words(bs), SA.words(bs), words_eq(bs)),
    pack_fin(SA.words(bs)))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new
  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=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend&name=pack_fin
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend&name=words_eq
  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/argon2/argon2.bend&name=words
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend&name=depth_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend&name=fill
  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/sized.bend&name=words