def vrs

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pver.bend:48
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend as Pver
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/ecdsa.bend as ES
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/ecdsa.bend as E
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/scalarpow.bend as SP
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/pmul.bend as PM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA

48def vrs(+one: Nat, +h1: {one == 1n : Nat}, +q: P.Point, +hq: {PT.pred(one, q) == True{} : Bool}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}) -> {E.verify_rs(q, z, r, s) == ES.verify_rs(one, PT.pv(one, q), FS.value(one, z), FS.value(one, r), FS.value(one, s)) : Bool}:
49  +hw = SP.inv_r(one, h1, s, hs)
50  +hu1 = SO.mul_r(one, h1, z, S.inv(s), hz, hw)
51  +hu2 = SO.mul_r(one, h1, r, S.inv(s), hr, hw)
52  +hg = PA.g_r(one, h1)
53  +hp1 = PM.mul_r(one, h1, S.mul(z, S.inv(s)), P.g(), SL.sl16(one, S.mul(z, S.inv(s)), hu1), hg)
54  +hp2 = PM.mul_r(one, h1, S.mul(r, S.inv(s)), q, SL.sl16(one, S.mul(r, S.inv(s)), hu2), hq)
55  +hrr = PT.padd_r(one, h1, P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q), hp1, hp2)
56  %Equal.sym(Bool, Bool.and(Bool.not(P.is_inf(P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q)))), S.eq(S.reduce(P.aff_x(P.to_affine(P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))))), r)), Bool.and(Bool.not(CV.is_inf(PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))), vfin(one, h1, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q)), hrr, r, hr)) : {_ == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
57  %Equal.sym(CV.SPoint, PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))), CV.padd(FS.prime(one), PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))), PT.padd_v(one, h1, P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q), hp1, hp2)) : {Bool.and(Bool.not(CV.is_inf(_)), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
58  %Equal.sym(CV.SPoint, PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))), CV.padd(FS.prime(one), PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))), PT.padd_v(one, h1, P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q), hp1, hp2)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), _)), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
59  %Equal.sym(CV.SPoint, PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), PM.mul_v(one, h1, S.mul(z, S.inv(s)), P.g(), SL.sl16(one, S.mul(z, S.inv(s)), hu1), hg)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), _, PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
60  %Equal.sym(CV.SPoint, PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), PM.mul_v(one, h1, S.mul(z, S.inv(s)), P.g(), SL.sl16(one, S.mul(z, S.inv(s)), hu1), hg)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), _, PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
61  %Equal.sym(CV.SPoint, PT.pv(one, P.mul(S.mul(r, S.inv(s)), q)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q)), PM.mul_v(one, h1, S.mul(r, S.inv(s)), q, SL.sl16(one, S.mul(r, S.inv(s)), hu2), hq)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), _))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
62  %Equal.sym(CV.SPoint, PT.pv(one, P.mul(S.mul(r, S.inv(s)), q)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q)), PM.mul_v(one, h1, S.mul(r, S.inv(s)), q, SL.sl16(one, S.mul(r, S.inv(s)), hu2), hq)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), _))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
63  %Equal.sym(CV.SPoint, PT.pv(one, P.g()), CV.g(one), PA.g_v(one, h1)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), _), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
64  %Equal.sym(CV.SPoint, PT.pv(one, P.g()), CV.g(one), PA.g_v(one, h1)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), _), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
65  %Equal.sym(Nat, FS.value(one, S.mul(z, S.inv(s))), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), SO.mul_v(one, h1, z, S.inv(s), hz, hw)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), _, CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
66  %Equal.sym(Nat, FS.value(one, S.mul(z, S.inv(s))), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), SO.mul_v(one, h1, z, S.inv(s), hz, hw)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), _, CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
67  %Equal.sym(Nat, FS.value(one, S.mul(r, S.inv(s))), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), SO.mul_v(one, h1, r, S.inv(s), hr, hw)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), _, PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
68  %Equal.sym(Nat, FS.value(one, S.mul(r, S.inv(s))), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), SO.mul_v(one, h1, r, S.inv(s), hr, hw)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), _, PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
69  %Equal.sym(Nat, FS.value(one, S.inv(s)), FS.minv(FS.order(one), FS.value(one, s)), SP.inv_v(one, h1, s, hs)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), _), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
70  %Equal.sym(Nat, FS.value(one, S.inv(s)), FS.minv(FS.order(one), FS.value(one, s)), SP.inv_v(one, h1, s, hs)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), _), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
71  %Equal.sym(Nat, FS.value(one, S.inv(s)), FS.minv(FS.order(one), FS.value(one, s)), SP.inv_v(one, h1, s, hs)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), _), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
72  %Equal.sym(Nat, FS.value(one, S.inv(s)), FS.minv(FS.order(one), FS.value(one, s)), SP.inv_v(one, h1, s, hs)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), _), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
73  {==}
Uses (48)

Used by (1)

bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver:vok