Password.hp_go_ok: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend as Password
Lines 185-192 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend&start_line=185&end_line=192

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend as H
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as A2
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as PP

def hp_go_ok(+n: Nat, +v: List<&2, U32>, +last: Nat, +hv: {PP.ok(v) == True{} : Bool}) -> {PP.ok(A2.hp_go(n, v, last)) == True{} : Bool}:
  match n v:
    case _ Nil{}:
      {==}
    case 0n +x <> +r:
      ok_append(List.take(&2, U32, x <> r, 32n), H.hash(last, x <> r), ok_take(x <> r, 32n, hv), hash_ok(last, x <> r))
    case 1n+ +p +x <> +r:
      ok_append(List.take(&2, U32, x <> r, 32n), A2.hp_go(p, H.hash(64n, x <> r), last), ok_take(x <> r, 32n, hv), hp_go_ok(p, H.hash(64n, x <> r), last, hash_ok(64n, x <> r)))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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/password.bend&name=hash_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend&name=ok_append
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend&name=ok_take
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=ok
  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