def spk

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pschn.bend:265
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend as Pschn
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/bytes.bend as B
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/sel.bend as SL
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA

265def spk(+one: Nat, +h1: {one == 1n : Nat}, +d0: List<&2, Nat>, +hd0: {FS.reduced(one, FS.order(one), d0) == True{} : Bool}, +m: List<&2, U32>, +aux: List<&2, U32>, a: P.Affine, +ha: {PA.ared(one, a) == True{} : Bool}) -> {SC.sign_p(d0, m, aux, a) == SS.sign_p(one, FS.value(one, d0), m, aux, PA.av(one, a)) : Maybe<&2, List<&2, U32>>}:
266  match a:
267    case P.Affine{+px, +py}:
268      +hpx = ax_l(one, px, py, ha)
269      +hd = even_r(one, h1, py, d0, hd0)
270      %Equal.sym(List<&2, U32>, B.to_be(px), CV.i2osp(32n, FS.value(one, px)), tbv(one, h1, px, hpx)) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), _, m, S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, B.to_be(px), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, B.to_be(px), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
271      %Equal.sym(List<&2, U32>, B.to_be(px), CV.i2osp(32n, FS.value(one, px)), tbv(one, h1, px, hpx)) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, _, m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, B.to_be(px), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
272      %Equal.sym(List<&2, U32>, B.to_be(px), CV.i2osp(32n, FS.value(one, px)), tbv(one, h1, px, hpx)) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, _, m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
273      %Equal.sym(List<&2, U32>, B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), tbv(one, h1, S.select(SC.is_odd(py), S.neg(d0), d0), SL.sl16(one, S.select(SC.is_odd(py), S.neg(d0), d0), hd))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(_, SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
274      %Equal.sym(List<&2, U32>, B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), tbv(one, h1, S.select(SC.is_odd(py), S.neg(d0), d0), SL.sl16(one, S.select(SC.is_odd(py), S.neg(d0), d0), hd))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(_, SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
275      %Equal.sym(List<&2, U32>, SC.tag_nonce(), SS.tag_nonce(), tn()) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(_, List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
276      %Equal.sym(List<&2, U32>, SC.tag_nonce(), SS.tag_nonce(), tn()) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(_, List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
277      %Equal.sym(List<&2, U32>, SC.tag_aux(), SS.tag_aux(), ta()) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(_, aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
278      %Equal.sym(List<&2, U32>, SC.tag_aux(), SS.tag_aux(), ta()) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(_, aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
279      %Equal.sym(List<&2, U32>, SC.tagged(SS.tag_aux(), aux), SS.tagged(SS.tag_aux(), aux), tagged_v(SS.tag_aux(), aux)) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), _), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
280      %Equal.sym(List<&2, U32>, SC.tagged(SS.tag_aux(), aux), SS.tagged(SS.tag_aux(), aux), tagged_v(SS.tag_aux(), aux)) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), _), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
281      %Equal.sym(List<&2, U32>, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), xor_v(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, _, List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
282      %Equal.sym(List<&2, U32>, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), xor_v(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, _, List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
283      %Equal.sym(Nat, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0)), Equal.sym(Nat, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0)), SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), even_v(one, h1, py, d0, hd0))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, _, CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
284      %Equal.sym(Nat, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0)), Equal.sym(Nat, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0)), SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), even_v(one, h1, py, d0, hd0))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, _), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
285      %Equal.sym(Nat, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one)), FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))), Equal.sym(Nat, FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))), Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one)), th_v(one, h1, SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0)), CV.i2osp(32n, FS.value(one, px)), m, _) : Maybe<&2, List<&2, U32>>}
286      sk2(one, h1, S.select(SC.is_odd(py), S.neg(d0), d0), hd, CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), th_r(one, h1, SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))
Uses (49)

Used by (1)

bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn:s3