def vr

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pschn.bend:116

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/spec/crypto/secp256k1/schnorr.bend as SS
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/src/crypto/secp256k1/schnorr.bend as SC
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/paff.bend as PA

116def vr(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hr: {FS.limbs16(one, 16n, r) == True{} : Bool}, +rr: P.Point, +hrr: {PT.pred(one, rr) == True{} : Bool}) -> {SC.verify_r(r, rr) == SS.check_r(FS.value(one, r), CV.is_inf(PT.pv(one, rr)), CV.to_affine(FS.prime(one), PT.pv(one, rr))) : Bool}:
117  %Equal.sym(Bool, P.is_inf(rr), CV.is_inf(PT.pv(one, rr)), PA.is_inf_v(one, h1, rr)) : {SC.verify_aff(r, _, P.to_affine(rr)) == SS.check_r(FS.value(one, r), CV.is_inf(PT.pv(one, rr)), CV.to_affine(FS.prime(one), PT.pv(one, rr))) : Bool}
118  %Equal.sym(CV.SAffine, CV.to_affine(FS.prime(one), PT.pv(one, rr)), PA.av(one, P.to_affine(rr)), 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))) : {SC.verify_aff(r, CV.is_inf(PT.pv(one, rr)), P.to_affine(rr)) == SS.check_r(FS.value(one, r), CV.is_inf(PT.pv(one, rr)), _) : Bool}
119  va(one, h1, r, hr, CV.is_inf(PT.pv(one, rr)), P.to_affine(rr), PA.aff_r(one, h1, rr, hrr))