def cp_red

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/prec.bend:106

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend as K
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/point.bend as PT
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend as RC

106def cp_red(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.red(one, E.cp_fe()) == True{} : Bool}:
107  +h = I.lt_subst_l(FS.cp(one), FS.value(one, E.cp_fe()), 1n+K.pp(one), Equal.sym(Nat, FS.value(one, E.cp_fe()), FS.cp(one), RC.cp_fe_v(one)), RC.cp_lt_p(one, h1))
108  Lg.and_intro(FS.limbs16(one, 16n, E.cp_fe()), Nat.is_lt(FS.value(one, E.cp_fe()), FS.prime(one)), RC.cp_fe_l(one, h1), to_p(one, h1, FS.value(one, E.cp_fe()), h))