def lt3

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/scalarops.bend:33

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
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 AR
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/proofs/crypto/secp256k1/ineq.bend as I

33# below 3 2^256 is below 2^512
34def lt3(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, Nat.add(C.shift(256n, one), Nat.add(C.shift(256n, one), C.shift(256n, one)))) == True{} : Bool}) -> {Nat.is_lt(x, Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}:
35  +t = C.shift(256n, one)
36  +e3 = Equal.trans(Nat, Nat.add(t, Nat.add(t, t)), Nat.add(t, Nat.add(t, Nat.add(t, 0n))), Nat.mul(3n, t), Equal.cong(Nat, Nat, z => Nat.add(t, Nat.add(t, z)), t, Nat.add(t, 0n), Equal.sym(Nat, Nat.add(t, 0n), t, NA.add_zero(t))), {==})
37  N.lt_le_trans(x, Nat.mul(3n, t), Nat.mul(t, t), I.lt_subst_r(x, Nat.add(t, Nat.add(t, t)), Nat.mul(3n, t), e3, hx), AR.mul_le(3n, t, t, three_le(one, h1)))