def rehash_hash

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/password.bend:301

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

301# needs_rehash(hash_password(pw, salt, params), params) == False whenever
302# hash_password returns a string, for every salt of bytes below 256 with the
303# parameters' salt length.
304def 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}:
305  match params:
306    case PW.Params{+m, +t, +p, +tl, +sl}:
307      enc_fresh(pw, salt, m, t, p, tl, sl, A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, tl), {==}, hs, hl)