proofs/crypto/argon2/proof.bend
bend-collections-laws-crypto@1.0.0.0 · 33 lines · 0 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend as GB
3import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend as BL
4import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend as HS
5import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as MEM
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/index.bend as IX
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend as FL
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/run.bend as RN
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend as TOP
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as PP
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend as PWP
12import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
13import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
14import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/laws.bend as Laws
16
17
18
19def Laws.gb_correct(a, b, c, d): GB.gb_correct(a, b, c, d)
20def Laws.p_correct(v): BL.p_correct(v)
21def Laws.compress_correct(x, y): BL.compress_correct(x, y)
22def Laws.compress_xor_correct(x, y, old): BL.compress_xor_correct(x, y, old)
23def Laws.hash_correct(nn, bs): HS.hash_eq(nn, bs)
24def Laws.hprime_correct(tl, x): HS.hprime_eq(tl, x)
25def Laws.h0_correct(p, tl, m, t, pw, salt, key, ad): HS.h0_eq(p, tl, m, t, pw, salt, key, ad)
26def Laws.rel_correct(w, j1, k, hk, hw): IX.rel_eq(w, j1, k, hk, L.subst(Nat, z => {Nat.is_lt(w, z) == True{} : Bool}, Nat.pow(2n, k), SC.pow2(k), Equal.sym(Nat, SC.pow2(k), Nat.pow(2n, k), U.pow2_pow(k)), hw))
27def Laws.addresses_correct(r, l, s, mm, t, ctr): IX.addresses_eq(r, l, s, mm, t, ctr)
28def Laws.argon2id_correct(pw, salt, key, ad, t, m, p, tl, hf): TOP.argon2id_correct(pw, salt, key, ad, t, m, p, tl, hf)
29def Laws.parse_format(m, t, p, salt, hash, hs, hh): PP.parse_format(m, t, p, salt, hash, hs, hh)
30def Laws.verify_hash(pw, salt, params, hs): PWP.verify_hash(pw, salt, params, hs)
31def Laws.rehash_hash(pw, salt, params, hs, hl): PWP.rehash_hash(pw, salt, params, hs, hl)
32def Laws.tag_length(tl, x): PWP.hprime_len(tl, x)
33def Laws.tag_bytes(tl, x): PWP.hprime_ok(tl, x)