def hi_byte_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/negate.bend:54

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/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend as R

54# x < 2^16: x div 256 < 256
55def hi_byte_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.div(x, 256n), 256n) == True{} : Bool}:
56  +bq = C.shift(8n, one)
57  +hi = Nat.div(x, 256n)
58  +le = I.le_subst_r(Nat.mul(hi, 256n), Nat.add(Nat.mul(hi, 256n), Nat.mod(x, 256n)), x, Equal.sym(Nat, x, Nat.add(Nat.mul(hi, 256n), Nat.mod(x, 256n)), NR.dm_eq(255n, x)), N.le_add_right(Nat.mul(hi, 256n), Nat.mod(x, 256n)))
59  +le2 = I.le_subst_l(Nat.mul(hi, 256n), Nat.mul(hi, bq), x, Equal.cong(Nat, Nat, z => Nat.mul(hi, z), 256n, bq, Equal.sym(Nat, bq, 256n, LV.b8(one, h1))), le)
60  +s1 = N.le_lt_trans(Nat.mul(hi, bq), x, C.shift(16n, one), le2, hx)
61  +s2 = I.lt_subst_r(Nat.mul(hi, bq), C.shift(16n, one), Nat.mul(bq, bq), Equal.sym(Nat, Nat.mul(bq, bq), C.shift(16n, one), bb_sq(one, h1)), s1)
62  +s3 = R.mul_lt_cancel(bq, hi, bq, s2, Nat.is_lt(hi, bq), {==})
63  I.lt_subst_r(hi, bq, 256n, LV.b8(one, h1), s3)