def prev_lt

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

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/arith.bend as AR2
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA

206# The previous block is in the memory.
207def prev_lt(+l: Nat, +p: Nat, +q: Nat, +j: Nat, +b: Bool, +hl: {Nat.is_lt(l, p) == True{} : Bool}, +hj: {Nat.is_lt(j, q) == True{} : Bool}, +hq1: {Nat.is_le(1n, q) == True{} : Bool}) -> {Nat.is_lt(SA.prev_index(l, q, j, b), Nat.mul(p, q)) == True{} : Bool}:
208  match b:
209    case True{}:
210      lt_mul_add(l, p, Nat.sub(q, 1n), q, hl, sub1_lt(q, hq1))
211    case False{}:
212      N.le_lt_trans(Nat.sub(Nat.add(Nat.mul(l, q), j), 1n), Nat.add(Nat.mul(l, q), j), Nat.mul(p, q), AR2.sub_le2(Nat.add(Nat.mul(l, q), j), 1n), lt_mul_add(l, p, j, q, hl, hj))