Hash.hp_go_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 94-103 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=94&end_line=103

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/src/crypto/argon2/argon2.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA

def hp_go_eq(+n: Nat, +v: List<&2, U32>, +last: Nat) -> {I.hp_go(n, v, last) == SA.hp_go(n, v, last) : List<&2, U32>}:
  match n v:
    case _ Nil{}:
      {==}
    case 0n +x <> +r:
      Equal.cong(List<&2, U32>, List<&2, U32>, z => List.append(&2, U32, List.take(&2, U32, x <> r, 32n), z), IH.hash(last, x <> r), SA.hash(last, x <> r), hash_eq(last, x <> r))
    case 1n+ +p +x <> +r:
      Equal.trans(List<&2, U32>, List.append(&2, U32, List.take(&2, U32, x <> r, 32n), I.hp_go(p, IH.hash(64n, x <> r), last)), List.append(&2, U32, List.take(&2, U32, x <> r, 32n), I.hp_go(p, SA.hash(64n, x <> r), last)), List.append(&2, U32, List.take(&2, U32, x <> r, 32n), SA.hp_go(p, SA.hash(64n, x <> r), last)),
        Equal.cong(List<&2, U32>, List<&2, U32>, z => List.append(&2, U32, List.take(&2, U32, x <> r, 32n), I.hp_go(p, z, last)), IH.hash(64n, x <> r), SA.hash(64n, x <> r), hash_eq(64n, x <> r)),
        Equal.cong(List<&2, U32>, List<&2, U32>, z => List.append(&2, U32, List.take(&2, U32, x <> r, 32n), z), I.hp_go(p, SA.hash(64n, x <> r), last), SA.hp_go(p, SA.hash(64n, x <> r), last), hp_go_eq(p, SA.hash(64n, x <> r), last)))

Uses (12):
  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.append
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend&name=hash_eq
  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=hp_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=hp_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend&name=hash