def tag_ok

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
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

227def tag_ok(+pw: List<&2, U32>, +salt: List<&2, U32>, +t: Nat, +m: Nat, +p: Nat, +tl: Nat, +tag: List<&2, U32>, +er: {A2.argon2id(pw, salt, Nil{}, Nil{}, t, m, p, tl) == Some{tag} : Maybe<&2, List<&2, U32>>}) -> {PP.ok(tag) == True{} : Bool}:
228  +ok = Bool.and(A2.valid(pw, salt, Nil{}, Nil{}, t, m, p, tl), A2.fits(m, p))
229  L.subst(List<&2, U32>, z => {PP.ok(z) == True{} : Bool}, A2.run(pw, salt, Nil{}, Nil{}, t, m, p, tl), tag, tag_of(ok, pw, salt, t, m, p, tl, tag, er), run_ok(pw, salt, t, m, p, tl))