def parse_format

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/phc.bend:1349

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend as PH

1349# parse(format(x)) == Some{x}, for byte lists of bytes below 256.
1350def parse_format(+m: Nat, +t: Nat, +p: Nat, +salt: List<&2, U32>, +hash: List<&2, U32>, +hs: {ok(salt) == True{} : Bool}, +hh: {ok(hash) == True{} : Bool}) -> {PH.parse(PH.format(PH.Phc{m, t, p, salt, hash})) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}:
1351  %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(m), SCon{Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))})), Some{PH.Got{m, SCon{Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))}}}, dec_rt(m, Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)])), {==})) : {PH.parse_m(_) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1352  %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(t), SCon{Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))})), Some{PH.Got{t, SCon{Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))}}}, dec_rt(t, Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)])), {==})) : {PH.parse_t(m, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1353  %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(p), SCon{Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)])})), Some{PH.Got{p, SCon{Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)])}}}, dec_rt(p, Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)]), {==})) : {PH.parse_p(m, t, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1354  %Equal.sym(Maybe<&2, PH.Cut>, PH.field(String.append(PH.b64(salt), SCon{Chr{36}, String.concat([PH.b64(hash)])})), Some{PH.Cut{PH.b64(salt), String.concat([PH.b64(hash)])}}, field_b64(salt, String.concat([PH.b64(hash)]), hs)) : {PH.parse_salt(m, t, p, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1355  %Equal.sym(String, String.append(PH.b64(hash), SNil{}), PH.b64(hash), append_nil(PH.b64(hash))) : {PH.parse_hash(m, t, p, PH.unb64(PH.b64(salt)), PH.unb64(_)) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1356  %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(salt)), Some{salt}, b64_rt(salt, hs)) : {PH.parse_hash(m, t, p, _, PH.unb64(PH.b64(hash))) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1357  %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(hash)), Some{hash}, b64_rt(hash, hh)) : {PH.parse_hash(m, t, p, Some{salt}, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1358  {==}