proofs/crypto/argon2/top.bend checks
raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend as Top
21 imports
import Base import ../../../spec/lib/common.bend as SC import ../../lib/array.bend as AR import ../../lib/list.bend as LL import ../../lib/nat.bend as N import ../../lib/logic.bend as L import ../../lib/arith.bend as AR2 import ../../lib/lemmas/proofs/nat_algebra.bend as NA import ../../math/natural/arith.bend as NR import ../../../src/crypto/blake/blake2b/types.bend as T import ../../../src/crypto/argon2/types.bend as A import ../../../src/crypto/argon2/blamka.bend as G import ../../../src/crypto/argon2/memory.bend as M import ../../../src/crypto/argon2/argon2.bend as I import ../../../spec/crypto/argon2/blamka.bend as SG import ../../../spec/crypto/argon2/argon2.bend as SA import ./blamka.bend as BL import ./memory.bend as MEM import ./hash.bend as HS import ./fill.bend as F import ./run.bend as R
Definitions
def X source · line 28 · raw
@+m:Nat -> @+p:Nat -> Nat
def mm_swap source · line 31 · raw
@+p:Nat -> @+x:Nat -> {Nat.mul(Nat.mul(4n, p), x) == Nat.mul(Nat.mul(4n, x), p) : Nat}
def div_exact source · line 39 · raw
@+y:Nat -> @+d:Nat -> @+hd:{Nat.is_le(1n, d) == True{} : Bool} -> {Nat.div(Nat.mul(y, d), d) == y : Nat}Exact division: y * d / d = y for d >= 1.
def q_eq source · line 48 · raw
@+m:Nat -> @+p:Nat -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> {Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.blocks(m, p), p) == Nat.mul(4n, X(m, p)) : Nat}q = m' / p = 4 X.
def div4 source · line 53 · raw
@+x:Nat -> {Nat.div(Nat.mul(4n, x), 4n) == x : Nat}sl = q / 4 = X.
def sl_eq source · line 57 · raw
@+m:Nat -> @+p:Nat -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> {Nat.div(Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.blocks(m, p), p), 4n) == X(m, p) : Nat}
def hq source · line 62 · raw
@+m:Nat -> @+p:Nat -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> {Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.blocks(m, p), p) == Nat.mul(4n, Nat.div(Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.blocks(m, p), p), 4n)) : Nat}q = 4 sl
def hlen source · line 67 · raw
@+m:Nat -> @+p:Nat -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.blocks(m, p) == Nat.mul(p, Nat.div(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.blocks(m, p), p)) : Nat}m' = p q
def x_ge2 source · line 74 · raw
@+m:Nat -> @+p:Nat -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> @+h8:{Nat.is_le(Nat.mul(8n, p), m) == True{} : Bool} -> {Nat.is_le(2n, X(m, p)) == True{} : Bool}8p <= m gives X >= 2.
def pw_eq source · line 85 · raw
@+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.pw(k) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(k) : Nat}
def d8 source · line 92 · raw
@+b:Nat -> {Nat.mul(b, 256n) == Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(Nat.double(b)))))))) : Nat}
def levels_go_ok source · line 101 · raw
@+f:Nat -> @+n:Nat -> @+k:Nat -> @+done:Bool -> @+hd:{done == Nat.is_le(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.pw(k)) : Bool} -> @+hr:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.levels_go(f, n, k, done), Nat.add(k, f)) == True{} : Bool} -> {Nat.is_le(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.pw(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.levels_go(f, n, k, done))) == True{} : Bool}levels(n) = k with k <= 23 gives n <= 2^k.
def levels_ok source · line 111 · raw
@+n:Nat -> @+h:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.levels(n), 23n) == True{} : Bool} -> {Nat.is_le(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.levels(n))) == True{} : Bool}
def cap source · line 116 · raw
@+n:Nat -> @+h:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.levels(n), 23n) == True{} : Bool} -> {Nat.is_le(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.replicate(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.zero)), 256n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(Nat.add(8n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.levels(n)))) == True{} : Bool}256 m' <= 2^(8 + k).
def depth_lt source · line 122 · raw
@+n:Nat -> @+h:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.levels(n), 23n) == True{} : Bool} -> {Nat.is_lt(Nat.add(8n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.levels(n)), 32n) == True{} : Bool}
def q2 source · line 127 · raw
@+q:Nat -> @+sl:Nat -> @+hq:{q == Nat.mul(4n, sl) : Nat} -> @+hsl:{Nat.is_le(2n, sl) == True{} : Bool} -> {Nat.is_le(2n, q) == True{} : Bool}
def fill_eq source · line 130 · raw
@+d:Nat -> @+t:Nat -> @+p:Nat -> @+q:Nat -> @+sl:Nat -> @+mm:Nat -> @+hh:List<&2, U32> -> @+z:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hc:{Nat.is_le(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, z), 256n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hlen:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, z) == Nat.mul(p, q) : Nat} -> @+hq:{q == Nat.mul(4n, sl) : Nat} -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> @+hsl:{Nat.is_le(2n, sl) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.passes_go(t, 0n, p, q, sl, mm, t, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.init_go(p, 0n, q, hh, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/memory.mt(d, z)))) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/memory.mt(d, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.passes_go(t, 0n, p, q, sl, mm, t, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.init_go(p, 0n, q, hh, z)))) : Array<U32>}
def tail_i source · line 138 · raw
@+tl:Nat -> @+p:Nat -> @+q:Nat -> @a:Array<U32> -> List<&2, U32>
def tail_s source · line 141 · raw
@+tl:Nat -> @+p:Nat -> @+q:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> List<&2, U32>
def tail_eq source · line 144 · raw
@+d:Nat -> @+tl:Nat -> @+p:Nat -> @+q:Nat -> @+mem:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block> -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hc:{Nat.is_le(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem), 256n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hlen:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.Block, mem) == Nat.mul(p, q) : Nat} -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> @+hq1:{Nat.is_le(1n, q) == True{} : Bool} -> {tail_i(tl, p, q, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.thaw(U32, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/memory.mt(d, mem))) == tail_s(tl, p, q, mem) : List<&2, U32>}
def valid_p1 source · line 158 · raw
@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.valid(pw, salt, key, ad, t, m, p, tl) == True{} : Bool} -> {Nat.is_le(1n, p) == True{} : Bool}
def valid_p8 source · line 168 · raw
@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.valid(pw, salt, key, ad, t, m, p, tl) == True{} : Bool} -> {Nat.is_le(Nat.mul(8n, p), m) == True{} : Bool}
def run_body source · line 178 · raw
@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> @+hp:{Nat.is_le(1n, p) == True{} : Bool} -> @+h8:{Nat.is_le(Nat.mul(8n, p), m) == True{} : Bool} -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.fits(m, p) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.run(pw, salt, key, ad, t, m, p, tl) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.run(pw, salt, key, ad, t, m, p, tl) : List<&2, U32>}
def run_eq source · line 203 · raw
@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.valid(pw, salt, key, ad, t, m, p, tl) == True{} : Bool} -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.fits(m, p) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.run(pw, salt, key, ad, t, m, p, tl) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.run(pw, salt, key, ad, t, m, p, tl) : List<&2, U32>}
def checked_eq source · line 206 · raw
@+ok:Bool -> @+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.valid(pw, salt, key, ad, t, m, p, tl) == ok : Bool} -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.fits(m, p) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.checked(ok, pw, salt, key, ad, t, m, p, tl) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.checked(ok, pw, salt, key, ad, t, m, p, tl) : Maybe<&2, List<&2, U32>>}
def valid_eq source · line 213 · raw
@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.valid(pw, salt, key, ad, t, m, p, tl) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.valid(pw, salt, key, ad, t, m, p, tl) : Bool}
def and_true source · line 216 · raw
@+b:Bool -> {Bool.and(b, True{}) == b : Bool}
def argon2id_correct source · line 226 · raw
@+pw:List<&2, U32> -> @+salt:List<&2, U32> -> @+key:List<&2, U32> -> @+ad:List<&2, U32> -> @+t:Nat -> @+m:Nat -> @+p:Nat -> @+tl:Nat -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.fits(m, p) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.argon2id(pw, salt, key, ad, t, m, p, tl) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.argon2id(pw, salt, key, ad, t, m, p, tl) : Maybe<&2, List<&2, U32>>}Argon2id: for every password, salt, secret, associated data and parameters whose memory fits this implementation (m' <= 2^23 blocks), the implementation's tag (or None) is the specification's.