Pver.vfin: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend as Pver
Lines 37-46 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend&start_line=37&end_line=46

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

# R not the point at infinity and x(R) mod n = r
def 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}:
  +ha = PA.aff_r(one, h1, rr, hrr)
  +hx = aff_x_l(one, P.to_affine(rr), ha)
  %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}
  %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}
  %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}
  %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}
  %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}
  {==}

Uses (34):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend&name=eq_s
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=aff_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=aff_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=av
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=is_inf_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=pred
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=pv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend&name=sred_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend&name=sred_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend&name=aff_x_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend&name=aff_x_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&name=sl16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=SAffine
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=aff_x
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=is_inf
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=to_affine
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=order
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=prime
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=reduced
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=Point
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=aff_x
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=is_inf
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=to_affine
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=reduce