def area_bound

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/fill.bend:118

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA

118# |W| < 2^d.
119def area_bound(+d: Nat, +n: Nat, +r0: Bool, +s: Nat, +sl: Nat, +q: Nat, +idx: Nat, +same: Bool, +hq: {q == Nat.mul(4n, sl) : Nat}, +hs: {Nat.is_lt(s, 4n) == True{} : Bool}, +hi: {Nat.is_lt(idx, sl) == True{} : Bool}, +hqn: {Nat.is_le(q, n) == True{} : Bool}, +hn: {Nat.is_le(Nat.mul(n, 256n), SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(SA.area(SA.area_base(r0, s, sl, q), idx, same), SC.pow2(d)) == True{} : Bool}:
120  +base = SA.area_base(r0, s, sl, q)
121  +h1 = area_le(base, idx, same)
122  +h2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(SA.area_base(r0, s, sl, z), idx), z) == True{} : Bool}, Nat.mul(4n, sl), q, Equal.sym(Nat, q, Nat.mul(4n, sl), hq), base_lt(r0, s, sl, idx, hs, hi))
123  +h3 = N.le_trans(n, Nat.mul(n, 256n), SC.pow2(d), le_mul256(n), hn)
124  N.le_lt_trans(SA.area(base, idx, same), Nat.add(base, idx), SC.pow2(d), h1, N.lt_le_trans(Nat.add(base, idx), q, SC.pow2(d), h2, N.le_trans(q, n, SC.pow2(d), hqn, h3)))