def s_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/limbs.bend:217

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/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M

217# carry-in at most 2^21 and a limb at most 2^28: their sum is below 2^29
218def s_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +c: U32, +hx: {Nat.is_le(v(x), WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(v(x), v(c)), WD.sc(29n, one)) == True{} : Bool}:
219  +c28 = N.lt_le(v(c), WD.sc(28n, one), N.le_lt_trans(v(c), WD.sc(21n, one), WD.sc(28n, one), hc, sc_lt(6n, 21n, one, h1)))
220  +lt = N.le_lt_trans(Nat.add(v(x), v(c)), Nat.add(WD.sc(28n, one), WD.sc(21n, one)), Nat.add(WD.sc(28n, one), WD.sc(28n, one)), M.le_add2(v(x), v(c), WD.sc(28n, one), WD.sc(21n, one), hx, hc), N.lt_add_left(WD.sc(21n, one), WD.sc(28n, one), WD.sc(28n, one), sc_lt(6n, 21n, one, h1)))
221  %M.sc_dbl(28n, one) : {Nat.is_lt(Nat.add(v(x), v(c)), _) == True{} : Bool}
222  lt