Password.rehash_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 301-307 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=301&end_line=307

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

# needs_rehash(hash_password(pw, salt, params), params) == False whenever
# hash_password returns a string, for every salt of bytes below 256 with the
# parameters' salt length.
def rehash_hash(+pw: List<&2, U32>, +salt: List<&2, U32>, +params: PW.Params, +hs: {PP.ok(salt) == True{} : Bool}, +hl: {len(salt) == PW.salt_len(params) : Nat}) -> {fresh(PW.hash_password(pw, salt, params), params) == False{} : Bool}:
  match params:
    case PW.Params{+m, +t, +p, +tl, +sl}:
      enc_fresh(pw, salt, m, t, p, tl, sl, A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, tl), {==}, hs, hl)

Uses (12):
  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=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=enc_fresh
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend&name=fresh
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend&name=len
  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
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/password.bend&name=salt_len