def ix_lt

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA

163# The reference block is in the memory.
164def ix_lt(+r0: Bool, +s: Nat, +l: Nat, +idx: Nat, +p: Nat, +q: Nat, +sl: Nat, +pr: T.Lane, +hl: {Nat.is_lt(l, p) == True{} : Bool}, +hp: {Nat.is_le(1n, p) == True{} : Bool}, +hq1: {Nat.is_le(1n, q) == True{} : Bool}) -> {Nat.is_lt(ixs(r0, s, l, idx, p, q, sl, pr), Nat.mul(p, q)) == True{} : Bool}:
165  +rl = SA.ref_lane(Bool.and(r0, Nat.is_eq(s, 0n)), l, SA.hi(pr), p)
166  lt_mul_add(rl, p, Nat.mod(Nat.add(SA.start(r0, s, sl), SA.rel(SA.area(SA.area_base(r0, s, sl, q), idx, Nat.is_eq(rl, l)), SA.lo(pr))), q), q, ref_lane_lt(Bool.and(r0, Nat.is_eq(s, 0n)), l, SA.hi(pr), p, hl, hp), mod_lt(Nat.add(SA.start(r0, s, sl), SA.rel(SA.area(SA.area_base(r0, s, sl, q), idx, Nat.is_eq(rl, l)), SA.lo(pr))), q, hq1))