def rlt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/fieldops.bend:79

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/proofs/lib/logic.bend as Lg
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/consts.bend as K

79def rlt(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +h: {FS.reduced(one, FS.prime(one), x) == True{} : Bool}) -> {Nat.is_lt(LV.ev(x), 1n+K.pp(one)) == True{} : Bool}:
80  +l = Lg.and_right(FS.limbs16(one, 16n, x), Nat.is_lt(FS.value(one, x), FS.prime(one)), h)
81  +l2 = I.lt_subst_l(FS.value(one, x), LV.ev(x), FS.prime(one), LV.ev_value(one, h1, x), l)
82  I.lt_subst_r(LV.ev(x), FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1), l2)