Pschn.spk: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend as Pschn
Lines 265-286 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&start_line=265&end_line=286

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

def 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>>}:
  match a:
    case P.Affine{+px, +py}:
      +hpx = ax_l(one, px, py, ha)
      +hd = even_r(one, h1, py, d0, hd0)
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      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):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend&name=ared
  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/pschn.bend&name=ax_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=even_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=even_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=sk2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=ta
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=tagged_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=tbv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=th_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=th_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=tn
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=xor_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=i2osp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=os2ip
  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=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/spec/crypto/secp256k1/schnorr.bend&name=even
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=sign_k
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=sign_p
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=tag_aux
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=tag_nonce
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=tagged
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=xor_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=of_be
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=to_be
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=Affine
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=neg
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=reduce
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=select
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=is_odd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=sign_nz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=sign_p
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=tag_aux
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=tag_nonce
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=tagged
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=xor_bytes