Password.verify_hash: 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 279-284 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=279&end_line=284

import Base
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/src/crypto/password.bend as PW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as PP

# verify_password(pw, hash_password(pw, salt, params)) == True whenever
# hash_password returns a string, for every salt of bytes below 256.
def verify_hash(+pw: List<&2, U32>, +salt: List<&2, U32>, +params: PW.Params, +hs: {PP.ok(salt) == True{} : Bool}) -> {verified(pw, PW.hash_password(pw, salt, params)) == True{} : Bool}:
  match params:
    case PW.Params{+m, +t, +p, +tl, +sl}:
      enc_ver(pw, salt, m, t, p, tl, A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, tl), {==}, hs)

Uses (9):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend&name=enc_ver
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend&name=verified
  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=argon2id
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/password.bend&name=Params
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/password.bend&name=hash_password