def vfin

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pver.bend:37

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/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as S
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as FW
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/sel.bend as SL
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend as SQ

37# R not the point at infinity and x(R) mod n = r
38def vfin(+one: Nat, +h1: {one == 1n : Nat}, +rr: P.Point, +hrr: {PT.pred(one, rr) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}) -> {Bool.and(Bool.not(P.is_inf(rr)), S.eq(S.reduce(P.aff_x(P.to_affine(rr))), r)) == Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, rr))), FS.order(one)), FS.value(one, r))) : Bool}:
39  +ha = PA.aff_r(one, h1, rr, hrr)
40  +hx = aff_x_l(one, P.to_affine(rr), ha)
41  %Equal.sym(Bool, P.is_inf(rr), CV.is_inf(PT.pv(one, rr)), PA.is_inf_v(one, h1, rr)) : {Bool.and(Bool.not(_), S.eq(S.reduce(P.aff_x(P.to_affine(rr))), r)) == Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, rr))), FS.order(one)), FS.value(one, r))) : Bool}
42  %Equal.sym(Bool, S.eq(S.reduce(P.aff_x(P.to_affine(rr))), r), Nat.is_eq(FS.value(one, S.reduce(P.aff_x(P.to_affine(rr)))), FS.value(one, r)), FW.eq_s(one, h1, S.reduce(P.aff_x(P.to_affine(rr))), r, SL.sl16(one, S.reduce(P.aff_x(P.to_affine(rr))), SQ.sred_r(one, h1, P.aff_x(P.to_affine(rr)), hx)), SL.sl16(one, r, hr))) : {Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), _) == Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, rr))), FS.order(one)), FS.value(one, r))) : Bool}
43  %Equal.sym(Nat, FS.value(one, S.reduce(P.aff_x(P.to_affine(rr)))), Nat.mod(FS.value(one, P.aff_x(P.to_affine(rr))), FS.order(one)), SQ.sred_v(one, h1, P.aff_x(P.to_affine(rr)), hx)) : {Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(_, FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, rr))), FS.order(one)), FS.value(one, r))) : Bool}
44  %Equal.sym(Nat, FS.value(one, P.aff_x(P.to_affine(rr))), CV.aff_x(PA.av(one, P.to_affine(rr))), aff_x_v(one, P.to_affine(rr))) : {Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(_, FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, rr))), FS.order(one)), FS.value(one, r))) : Bool}
45  %Equal.sym(CV.SAffine, PA.av(one, P.to_affine(rr)), CV.to_affine(FS.prime(one), PT.pv(one, rr)), PA.aff_v(one, h1, rr, hrr)) : {Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(_), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, rr))), FS.order(one)), FS.value(one, r))) : Bool}
46  {==}