def base_lt

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

import Base
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/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA

63# The base of the reference area plus the index stays below q = 4 sl.
64def base_lt(+r0: Bool, +s: Nat, +sl: Nat, +idx: Nat, +hs: {Nat.is_lt(s, 4n) == True{} : Bool}, +hi: {Nat.is_lt(idx, sl) == True{} : Bool}) -> {Nat.is_lt(Nat.add(SA.area_base(r0, s, sl, Nat.mul(4n, sl)), idx), Nat.mul(4n, sl)) == True{} : Bool}:
65  match r0:
66    case True{}:
67      seg_lt(s, sl, idx, hs, hi)
68    case False{}:
69      +q = Nat.mul(4n, sl)
70      +hsq = N.le_trans(sl, Nat.add(sl, Nat.mul(3n, sl)), q, N.le_add_right(sl, Nat.mul(3n, sl)), N.le_refl(q))
71      +e = N.sub_add(q, sl, hsq)
72      +h1 = N.lt_add_left(idx, sl, Nat.sub(q, sl), hi)
73      L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.sub(q, sl), idx), z) == True{} : Bool}, Nat.add(Nat.sub(q, sl), sl), q,
74        Equal.trans(Nat, Nat.add(Nat.sub(q, sl), sl), Nat.add(sl, Nat.sub(q, sl)), q, NA.add_comm(Nat.sub(q, sl), sl), e), h1)