def seg_lt

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

import Base

41# s < 4 and idx < sl give s * sl + idx < 4 sl.
42def seg_lt(+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(Nat.mul(s, sl), idx), Nat.mul(4n, sl)) == True{} : Bool}:
43  lt_mul_add(s, 4n, idx, sl, hs, hi)