def ltm_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/listops.bend:187

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/src/crypto/secp256k1/limbs.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
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/bounds.bend as B
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend as R

187def ltm_v(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +x: List<&2, Nat>) -> {L.ltm(c, x) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}:
188  +u = L.carry(32n, L.add(x, c), 0n)
189  +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(x, c), 0n, {==})
190  +ll = I.lt_subst_r(LV.ev(L.take(16n, u)), LV.pos(16n, one), C.shift(256n, one), B.pos16(one), B.limbs_lt(one, h1, 16n, L.take(16n, u), hu16))
191  %Equal.sym(Nat, L.horner(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), LV.horner_v(L.drop(16n, L.carry(32n, L.add(x, c), 0n)))) : {Nat.is_eq(_, 0n) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
192  %Equal.sym(Bool, Nat.is_eq(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), 0n), Nat.is_lt(Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), C.shift(256n, one)), hz(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one), ll)) : {_ == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
193  %Equal.sym(Nat, Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), LV.ev(L.carry(32n, L.add(x, c), 0n)), Equal.sym(Nat, LV.ev(L.carry(32n, L.add(x, c), 0n)), Nat.add(LV.ev(L.take(16n, L.carry(32n, L.add(x, c), 0n))), Nat.mul(LV.ev(L.drop(16n, L.carry(32n, L.add(x, c), 0n))), C.shift(256n, one))), R.split256(one, h1, L.carry(32n, L.add(x, c), 0n)))) : {Nat.is_lt(_, C.shift(256n, one)) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
194  %Equal.sym(Nat, LV.ev(L.carry(32n, L.add(x, c), 0n)), Nat.add(LV.ev(x), LV.ev(c)), R.u_val(c, x)) : {Nat.is_lt(_, C.shift(256n, one)) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
195  %Equal.sym(Nat, C.shift(256n, one), Nat.add(1n+mp, LV.ev(c)), Equal.sym(Nat, Nat.add(1n+mp, LV.ev(c)), C.shift(256n, one), hm)) : {Nat.is_lt(Nat.add(LV.ev(x), LV.ev(c)), _) == Nat.is_lt(LV.ev(x), 1n+mp) : Bool}
196  WW.lt_cancel_r(LV.ev(x), 1n+mp, LV.ev(c))