def vrs

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

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/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/src/crypto/secp256k1/schnorr.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend as SO
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/ptwo.bend as TW

121def vrs(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hr: {FS.limbs16(one, 16n, r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}, +e: List<&2, Nat>, +he: {FS.reduced(one, FS.order(one), e) == True{} : Bool}, +pp: P.Point, +hp: {PT.pred(one, pp) == True{} : Bool}) -> {SC.verify_r(r, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))) == SS.verify_rs(one, FS.value(one, r), FS.value(one, s), FS.value(one, e), PT.pv(one, pp)) : Bool}:
122  +hn = SO.neg_r(one, h1, e, he)
123  +hq = TW.two_r(one, h1, s, hs, S.neg(e), hn, pp, hp)
124  %Equal.sym(Bool, SC.verify_r(r, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))), SS.check_r(FS.value(one, r), CV.is_inf(PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp)))), CV.to_affine(FS.prime(one), PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))))), vr(one, h1, r, hr, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp)), hq)) : {_ == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
125  %Equal.sym(CV.SPoint, PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.neg(e)), PT.pv(one, pp))), TW.two_v(one, h1, s, hs, S.neg(e), hn, pp, hp)) : {SS.check_r(FS.value(one, r), CV.is_inf(_), CV.to_affine(FS.prime(one), PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))))) == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
126  %Equal.sym(CV.SPoint, PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.neg(e)), PT.pv(one, pp))), TW.two_v(one, h1, s, hs, S.neg(e), hn, pp, hp)) : {SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.neg(e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), _)) == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
127  %Equal.sym(Nat, FS.value(one, S.neg(e)), FS.mneg(FS.order(one), FS.value(one, e)), SO.neg_v(one, h1, e, he)) : {SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), _, PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.neg(e)), PT.pv(one, pp))))) == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
128  %Equal.sym(Nat, FS.value(one, S.neg(e)), FS.mneg(FS.order(one), FS.value(one, e)), SO.neg_v(one, h1, e, he)) : {SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), _, PT.pv(one, pp))))) == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
129  {==}