proofs/crypto/secp256k1/pschn.bend source

proofs/crypto/secp256k1/pschn.bend on the hub · documented module

# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pschn.src; edit the .srcimport Baseimport ../../../spec/crypto/sha.bend as FIPSimport ../../../spec/crypto/secp256k1/field.bend as FSimport ../../../spec/crypto/secp256k1/curve.bend as CVimport ../../../spec/crypto/secp256k1/schnorr.bend as SSimport ../../../src/crypto/sha/sha256.bend as SHAimport ../../../src/crypto/secp256k1/limbs.bend as Limport ../../../src/crypto/secp256k1/field.bend as Fimport ../../../src/crypto/secp256k1/scalar.bend as Simport ../../../src/crypto/secp256k1/bytes.bend as Bimport ../../../src/crypto/secp256k1/point.bend as Pimport ../../../src/crypto/secp256k1/schnorr.bend as SCimport ../../lib/logic.bend as Lgimport ../sha/laws.bend as SHLimport ../sha/correctness.bend as SHCimport ./limbs.bend as LVimport ./ineq.bend as Iimport ./scalarops.bend as SOimport ./fwrap.bend as FWimport ./bytes.bend as BYimport ./point.bend as PTimport ./sel.bend as SLimport ./pmul.bend as PMimport ./paff.bend as PAimport ./penc.bend as PEimport ./blist.bend as BLimport ./pscal.bend as SQimport ./ptwo.bend as TW# BIP-340 Schnorr signatures of src/crypto/secp256k1/schnorr.bend against# spec/crypto/secp256k1/schnorr.bend: tagged hashes, verification, signing# and x-only public keys.# ---- bytes and hashes ----def fips_len(+bytes: List<&2, U32>) -> {List.length(&2, U32, FIPS.sha256_bytes(bytes)) == 32n : Nat}:  SHC.digest_octets_length(FIPS.blocks(FIPS.prepare(bytes, 48n), FIPS.constants())(FIPS.initial()))def tbv(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {FS.limbs16(one, 16n, x) == True{} : Bool}) -> {B.to_be(x) == CV.i2osp(32n, FS.value(one, x)) : List<&2, U32>}:  %Equal.sym(List<&2, U32>, B.to_be(x), CV.i2osp(32n, LV.ev(x)), BY.to_be_v(one, h1, x, hx)) : {_ == CV.i2osp(32n, FS.value(one, x)) : List<&2, U32>}  %Equal.sym(Nat, FS.value(one, x), LV.ev(x), LV.ev_value(one, h1, x)) : {CV.i2osp(32n, LV.ev(x)) == CV.i2osp(32n, _) : List<&2, U32>}  {==}def xor_v(xs: List<&2, U32>, ys: List<&2, U32>) -> {SC.xor_bytes(xs, ys) == SS.xor_bytes(xs, ys) : List<&2, U32>}:  match xs ys:    case +x <> xt +y <> yt:      Equal.cong(List<&2, U32>, List<&2, U32>, l => U32.xor(x, y) <> l, SC.xor_bytes(xt, yt), SS.xor_bytes(xt, yt), xor_v(xt, yt))    case Nil{} _:      {==}    case _ Nil{}:      {==}def tagged_v(+tag: List<&2, U32>, +x: List<&2, U32>) -> {SC.tagged(tag, x) == SS.tagged(tag, x) : List<&2, U32>}:  %Equal.sym(List<&2, U32>, SHA.sha256_bytes(tag), FIPS.sha256_bytes(tag), SHL.sha256_bytes_correct(tag)) : {SHA.sha256_bytes(List.append(&2, U32, _, List.append(&2, U32, SHA.sha256_bytes(tag), x))) == FIPS.sha256_bytes(List.append(&2, U32, FIPS.sha256_bytes(tag), List.append(&2, U32, FIPS.sha256_bytes(tag), x))) : List<&2, U32>}  %Equal.sym(List<&2, U32>, SHA.sha256_bytes(tag), FIPS.sha256_bytes(tag), SHL.sha256_bytes_correct(tag)) : {SHA.sha256_bytes(List.append(&2, U32, FIPS.sha256_bytes(tag), List.append(&2, U32, _, x))) == FIPS.sha256_bytes(List.append(&2, U32, FIPS.sha256_bytes(tag), List.append(&2, U32, FIPS.sha256_bytes(tag), x))) : List<&2, U32>}  %Equal.sym(List<&2, U32>, SHA.sha256_bytes(List.append(&2, U32, FIPS.sha256_bytes(tag), List.append(&2, U32, FIPS.sha256_bytes(tag), x))), FIPS.sha256_bytes(List.append(&2, U32, FIPS.sha256_bytes(tag), List.append(&2, U32, FIPS.sha256_bytes(tag), x))), SHL.sha256_bytes_correct(List.append(&2, U32, FIPS.sha256_bytes(tag), List.append(&2, U32, FIPS.sha256_bytes(tag), x)))) : {_ == FIPS.sha256_bytes(List.append(&2, U32, FIPS.sha256_bytes(tag), List.append(&2, U32, FIPS.sha256_bytes(tag), x))) : List<&2, U32>}  {==}def tagged_len(+tag: List<&2, U32>, +x: List<&2, U32>) -> {B.has_len(32n, SS.tagged(tag, x)) == True{} : Bool}:  %Equal.sym(Bool, B.has_len(32n, SS.tagged(tag, x)), Nat.is_eq(List.length(&2, U32, SS.tagged(tag, x)), 32n), BY.has_len_v(32n, SS.tagged(tag, x))) : {_ == True{} : Bool}  %Equal.sym(Nat, List.length(&2, U32, SS.tagged(tag, x)), 32n, fips_len(List.append(&2, U32, FIPS.sha256_bytes(tag), List.append(&2, U32, FIPS.sha256_bytes(tag), x)))) : {Nat.is_eq(_, 32n) == True{} : Bool}  {==}# int(hash) mod ndef th_v(+one: Nat, +h1: {one == 1n : Nat}, +tag: List<&2, U32>, +x: List<&2, U32>) -> {FS.value(one, S.reduce(B.of_be(SC.tagged(tag, x)))) == Nat.mod(CV.os2ip(SS.tagged(tag, x)), FS.order(one)) : Nat}:  %Equal.sym(List<&2, U32>, SC.tagged(tag, x), SS.tagged(tag, x), tagged_v(tag, x)) : {FS.value(one, S.reduce(B.of_be(_))) == Nat.mod(CV.os2ip(SS.tagged(tag, x)), FS.order(one)) : Nat}  SQ.hash_v(one, h1, SS.tagged(tag, x), tagged_len(tag, x))def th_r(+one: Nat, +h1: {one == 1n : Nat}, +tag: List<&2, U32>, +x: List<&2, U32>) -> {FS.reduced(one, FS.order(one), S.reduce(B.of_be(SC.tagged(tag, x)))) == True{} : Bool}:  %Equal.sym(List<&2, U32>, SC.tagged(tag, x), SS.tagged(tag, x), tagged_v(tag, x)) : {FS.reduced(one, FS.order(one), S.reduce(B.of_be(_))) == True{} : Bool}  SQ.hash_r(one, h1, SS.tagged(tag, x), tagged_len(tag, x))# ---- the even-y key or nonce: x or n - x ----def ev_q(+one: Nat, +h1: {one == 1n : Nat}, q: Nat, +x: List<&2, Nat>, +hx: {FS.reduced(one, FS.order(one), x) == True{} : Bool}, +hq: {Nat.is_lt(q, 2n) == True{} : Bool}) -> {FS.value(one, S.select(q, S.neg(x), x)) == SS.even_b(FS.order(one), q, FS.value(one, x)) : Nat}:  match q:    case 0n:      %Equal.sym(List<&2, Nat>, L.select(0n, S.neg(x), x), x, SL.sel0(one, 16n, S.neg(x), x, SL.sl16(one, S.neg(x), SO.neg_r(one, h1, x, hx)), SL.sl16(one, x, hx))) : {FS.value(one, _) == FS.value(one, x) : Nat}      {==}    case 1n:      %Equal.sym(List<&2, Nat>, L.select(1n, S.neg(x), x), S.neg(x), SL.sel1(one, 16n, S.neg(x), x, SL.sl16(one, S.neg(x), SO.neg_r(one, h1, x, hx)), SL.sl16(one, x, hx))) : {FS.value(one, _) == FS.mneg(FS.order(one), FS.value(one, x)) : Nat}      SO.neg_v(one, h1, x, hx)    case 2n+ +c:      Empty.absurd({FS.value(one, S.select(2n+c, S.neg(x), x)) == SS.even_b(FS.order(one), 2n+c, FS.value(one, x)) : Nat}, SL.not01(c, hq))def ev_qr(+one: Nat, +h1: {one == 1n : Nat}, q: Nat, +x: List<&2, Nat>, +hx: {FS.reduced(one, FS.order(one), x) == True{} : Bool}, +hq: {Nat.is_lt(q, 2n) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.select(q, S.neg(x), x)) == True{} : Bool}:  match q:    case 0n:      %Equal.sym(List<&2, Nat>, L.select(0n, S.neg(x), x), x, SL.sel0(one, 16n, S.neg(x), x, SL.sl16(one, S.neg(x), SO.neg_r(one, h1, x, hx)), SL.sl16(one, x, hx))) : {FS.reduced(one, FS.order(one), _) == True{} : Bool}      hx    case 1n:      %Equal.sym(List<&2, Nat>, L.select(1n, S.neg(x), x), S.neg(x), SL.sel1(one, 16n, S.neg(x), x, SL.sl16(one, S.neg(x), SO.neg_r(one, h1, x, hx)), SL.sl16(one, x, hx))) : {FS.reduced(one, FS.order(one), _) == True{} : Bool}      SO.neg_r(one, h1, x, hx)    case 2n+ +c:      Empty.absurd({FS.reduced(one, FS.order(one), S.select(2n+c, S.neg(x), x)) == True{} : Bool}, SL.not01(c, hq))def even_v(+one: Nat, +h1: {one == 1n : Nat}, +y: List<&2, Nat>, +x: List<&2, Nat>, +hx: {FS.reduced(one, FS.order(one), x) == True{} : Bool}) -> {FS.value(one, S.select(SC.is_odd(y), S.neg(x), x)) == SS.even(FS.order(one), FS.value(one, y), FS.value(one, x)) : Nat}:  %Equal.sym(Nat, F.parity(y), Nat.mod(FS.value(one, y), 2n), FW.parity_f(one, h1, y)) : {FS.value(one, S.select(_, S.neg(x), x)) == SS.even_b(FS.order(one), Nat.mod(FS.value(one, y), 2n), FS.value(one, x)) : Nat}  ev_q(one, h1, Nat.mod(FS.value(one, y), 2n), x, hx, PE.mod2_lt(FS.value(one, y)))def even_r(+one: Nat, +h1: {one == 1n : Nat}, +y: List<&2, Nat>, +x: List<&2, Nat>, +hx: {FS.reduced(one, FS.order(one), x) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.select(SC.is_odd(y), S.neg(x), x)) == True{} : Bool}:  %Equal.sym(Nat, F.parity(y), Nat.mod(FS.value(one, y), 2n), FW.parity_f(one, h1, y)) : {FS.reduced(one, FS.order(one), S.select(_, S.neg(x), x)) == True{} : Bool}  ev_qr(one, h1, Nat.mod(FS.value(one, y), 2n), x, hx, PE.mod2_lt(FS.value(one, y)))# ---- verification ----def va(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hr: {FS.limbs16(one, 16n, r) == True{} : Bool}, +inf: Bool, a: P.Affine, +ha: {PA.ared(one, a) == True{} : Bool}) -> {SC.verify_aff(r, inf, a) == SS.check_r(FS.value(one, r), inf, PA.av(one, a)) : Bool}:  match a:    case P.Affine{+x, +y}:      +hx = SL.l16(one, x, Lg.and_left(PT.red(one, x), PT.red(one, y), ha))      %Equal.sym(Nat, F.parity(y), Nat.mod(FS.value(one, y), 2n), FW.parity_f(one, h1, y)) : {Bool.and(Bool.not(inf), Bool.and(Nat.is_eq(_, 0n), F.eq(x, r))) == Bool.and(Bool.not(inf), Bool.and(Nat.is_eq(Nat.mod(FS.value(one, y), 2n), 0n), Nat.is_eq(FS.value(one, x), FS.value(one, r)))) : Bool}      %Equal.sym(Bool, F.eq(x, r), Nat.is_eq(FS.value(one, x), FS.value(one, r)), FW.eq_f(one, h1, x, r, hx, hr)) : {Bool.and(Bool.not(inf), Bool.and(Nat.is_eq(Nat.mod(FS.value(one, y), 2n), 0n), _)) == Bool.and(Bool.not(inf), Bool.and(Nat.is_eq(Nat.mod(FS.value(one, y), 2n), 0n), Nat.is_eq(FS.value(one, x), FS.value(one, r)))) : Bool}      {==}def 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}:  %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}  %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}  va(one, h1, r, hr, CV.is_inf(PT.pv(one, rr)), P.to_affine(rr), PA.aff_r(one, h1, rr, hrr))def 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}:  +hn = SO.neg_r(one, h1, e, he)  +hq = TW.two_r(one, h1, s, hs, S.neg(e), hn, pp, hp)  %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}  %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}  %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}  %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}  %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}  {==}def tc() -> {SC.tag_challenge() == SS.tag_challenge() : List<&2, U32>}:  {==}def ta() -> {SC.tag_aux() == SS.tag_aux() : List<&2, U32>}:  {==}def tn() -> {SC.tag_nonce() == SS.tag_nonce() : List<&2, U32>}:  {==}def red_n(+one: Nat, +x: List<&2, Nat>, +hl: {FS.limbs16(one, 16n, x) == True{} : Bool}, +h: {Nat.is_lt(FS.value(one, x), FS.order(one)) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), x) == True{} : Bool}:  Lg.and_intro(FS.limbs16(one, 16n, x), Nat.is_lt(FS.value(one, x), FS.order(one)), hl, h)def vok(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hlr: {FS.limbs16(one, 16n, r) == True{} : Bool}, +s: List<&2, Nat>, +hls: {FS.limbs16(one, 16n, 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}, a: Bool, b: Bool, +ha: {Nat.is_lt(FS.value(one, r), FS.prime(one)) == a : Bool}, +hb: {Nat.is_lt(FS.value(one, s), FS.order(one)) == b : Bool}) -> {SC.verify_ok(r, s, e, pp, Bool.and(a, b)) == SS.verify_ok(one, FS.value(one, r), FS.value(one, s), FS.value(one, e), PT.pv(one, pp), Bool.and(a, b)) : Bool}:  match a b:    case True{} True{}:      vrs(one, h1, r, hlr, s, red_n(one, s, hls, hb), e, he, pp, hp)    case True{} False{}:      {==}    case False{} _:      {==}def vp(+one: Nat, +h1: {one == 1n : Nat}, +pk: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>, +hsig: {B.has_len(64n, sig) == True{} : Bool}, mp: Maybe<&2, P.Point>, +hmp: {PE.mpred(one, mp) == True{} : Bool}) -> {SC.verify_p(pk, m, sig, mp) == SS.verify_p(one, pk, m, sig, PE.mpv(one, mp)) : Bool}:  match mp:    case None{}:      {==}    case Some{+pp}:      +hlr = BY.of_be_limbs(one, h1, CV.first(32n, sig), BL.pre_len(32n, 32n, sig, hsig))      +hls = BY.of_be_limbs(one, h1, CV.after(32n, sig), BL.suf_len(32n, 32n, sig, hsig))      %Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig)) : {SC.verify_ok(B.of_be(_), B.of_be(B.suffix(32n, sig)), S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, B.prefix(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(F.lt_p(B.of_be(B.prefix(32n, sig))), S.lt_n(B.of_be(B.suffix(32n, sig))))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool}      %Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig)) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(B.suffix(32n, sig)), S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, _, List.append(&2, U32, pk, m))))), pp, Bool.and(F.lt_p(B.of_be(B.prefix(32n, sig))), S.lt_n(B.of_be(B.suffix(32n, sig))))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool}      %Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig)) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(B.suffix(32n, sig)), S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(F.lt_p(B.of_be(_)), S.lt_n(B.of_be(B.suffix(32n, sig))))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool}      %Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig)) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(_), S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(F.lt_p(B.of_be(CV.first(32n, sig))), S.lt_n(B.of_be(B.suffix(32n, sig))))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool}      %Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig)) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(F.lt_p(B.of_be(CV.first(32n, sig))), S.lt_n(B.of_be(_)))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool}      %Equal.sym(List<&2, U32>, SC.tag_challenge(), SS.tag_challenge(), tc()) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(_, List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(F.lt_p(B.of_be(CV.first(32n, sig))), S.lt_n(B.of_be(CV.after(32n, sig))))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool}      %Equal.sym(Bool, F.lt_p(B.of_be(CV.first(32n, sig))), Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), FW.lt_p_f(one, h1, B.of_be(CV.first(32n, sig)))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(_, S.lt_n(B.of_be(CV.after(32n, sig))))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool}      %Equal.sym(Bool, S.lt_n(B.of_be(CV.after(32n, sig))), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)), FW.lt_n_s(one, h1, B.of_be(CV.after(32n, sig)))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), _)) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool}      %Equal.sym(Nat, Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))))), Equal.sym(Nat, FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))))), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), th_v(one, h1, SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), _, PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool}      %Equal.sym(Nat, CV.os2ip(CV.first(32n, sig)), FS.value(one, B.of_be(CV.first(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(CV.first(32n, sig))), CV.os2ip(CV.first(32n, sig)), BY.of_be_value(one, h1, CV.first(32n, sig)))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)))) == SS.verify_ok(one, _, CV.os2ip(CV.after(32n, sig)), FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))))), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool}      %Equal.sym(Nat, CV.os2ip(CV.first(32n, sig)), FS.value(one, B.of_be(CV.first(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(CV.first(32n, sig))), CV.os2ip(CV.first(32n, sig)), BY.of_be_value(one, h1, CV.first(32n, sig)))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)))) == SS.verify_ok(one, FS.value(one, B.of_be(CV.first(32n, sig))), CV.os2ip(CV.after(32n, sig)), FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))))), PT.pv(one, pp), Bool.and(Nat.is_lt(_, FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool}      %Equal.sym(Nat, CV.os2ip(CV.after(32n, sig)), FS.value(one, B.of_be(CV.after(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(CV.after(32n, sig))), CV.os2ip(CV.after(32n, sig)), BY.of_be_value(one, h1, CV.after(32n, sig)))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)))) == SS.verify_ok(one, FS.value(one, B.of_be(CV.first(32n, sig))), _, FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))))), PT.pv(one, pp), Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool}      %Equal.sym(Nat, CV.os2ip(CV.after(32n, sig)), FS.value(one, B.of_be(CV.after(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(CV.after(32n, sig))), CV.os2ip(CV.after(32n, sig)), BY.of_be_value(one, h1, CV.after(32n, sig)))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)))) == SS.verify_ok(one, FS.value(one, B.of_be(CV.first(32n, sig))), FS.value(one, B.of_be(CV.after(32n, sig))), FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))))), PT.pv(one, pp), Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(_, FS.order(one)))) : Bool}      vok(one, h1, B.of_be(CV.first(32n, sig)), hlr, B.of_be(CV.after(32n, sig)), hls, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), th_r(one, h1, SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))), pp, hmp, Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)), {==}, {==})def lxb(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hl: {FS.limbs16(one, 16n, x) == True{} : Bool}, b: Bool, +hb: {Nat.is_lt(FS.value(one, x), FS.prime(one)) == b : Bool}) -> {PE.mpv(one, SC.lift_if(x, b)) == SS.lift_if(one, FS.value(one, x), b) : Maybe<&2, CV.SPoint>}:  match b:    case True{}:      PE.decompress_v(one, h1, x, 0n, SL.red_of(one, x, hl, hb), {==})    case False{}:      {==}def lxr(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hl: {FS.limbs16(one, 16n, x) == True{} : Bool}, b: Bool, +hb: {Nat.is_lt(FS.value(one, x), FS.prime(one)) == b : Bool}) -> {PE.mpred(one, SC.lift_if(x, b)) == True{} : Bool}:  match b:    case True{}:      PE.decompress_r(one, h1, x, 0n, SL.red_of(one, x, hl, hb), {==})    case False{}:      {==}def lx(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hl: {FS.limbs16(one, 16n, x) == True{} : Bool}) -> {PE.mpv(one, SC.lift_x(x)) == SS.lift_x(one, FS.value(one, x)) : Maybe<&2, CV.SPoint>}:  %Equal.sym(Bool, F.lt_p(x), Nat.is_lt(FS.value(one, x), FS.prime(one)), FW.lt_p_f(one, h1, x)) : {PE.mpv(one, SC.lift_if(x, _)) == SS.lift_if(one, FS.value(one, x), Nat.is_lt(FS.value(one, x), FS.prime(one))) : Maybe<&2, CV.SPoint>}  lxb(one, h1, x, hl, Nat.is_lt(FS.value(one, x), FS.prime(one)), {==})def lx_r(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hl: {FS.limbs16(one, 16n, x) == True{} : Bool}) -> {PE.mpred(one, SC.lift_x(x)) == True{} : Bool}:  %Equal.sym(Bool, F.lt_p(x), Nat.is_lt(FS.value(one, x), FS.prime(one)), FW.lt_p_f(one, h1, x)) : {PE.mpred(one, SC.lift_if(x, _)) == True{} : Bool}  lxr(one, h1, x, hl, Nat.is_lt(FS.value(one, x), FS.prime(one)), {==})def vlen(+one: Nat, +h1: {one == 1n : Nat}, +pk: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>, a: Bool, b: Bool, +ha: {B.has_len(32n, pk) == a : Bool}, +hb: {B.has_len(64n, sig) == b : Bool}) -> {SC.verify_len(pk, m, sig, Bool.and(a, b)) == SS.verify_len(one, pk, m, sig, Bool.and(a, b)) : Bool}:  match a b:    case True{} True{}:      +hl = BY.of_be_limbs(one, h1, pk, ha)      %Equal.sym(Nat, CV.os2ip(pk), FS.value(one, B.of_be(pk)), Equal.sym(Nat, FS.value(one, B.of_be(pk)), CV.os2ip(pk), BY.of_be_value(one, h1, pk))) : {SC.verify_p(pk, m, sig, SC.lift_x(B.of_be(pk))) == SS.verify_p(one, pk, m, sig, SS.lift_x(one, _)) : Bool}      %Equal.sym(Maybe<&2, CV.SPoint>, SS.lift_x(one, FS.value(one, B.of_be(pk))), PE.mpv(one, SC.lift_x(B.of_be(pk))), Equal.sym(Maybe<&2, CV.SPoint>, PE.mpv(one, SC.lift_x(B.of_be(pk))), SS.lift_x(one, FS.value(one, B.of_be(pk))), lx(one, h1, B.of_be(pk), hl))) : {SC.verify_p(pk, m, sig, SC.lift_x(B.of_be(pk))) == SS.verify_p(one, pk, m, sig, _) : Bool}      vp(one, h1, pk, m, sig, hb, SC.lift_x(B.of_be(pk)), lx_r(one, h1, B.of_be(pk), hl))    case True{} False{}:      {==}    case False{} _:      {==}# BIP-340 verificationdef verify_v(+one: Nat, +h1: {one == 1n : Nat}, +pk: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>) -> {SC.verify(pk, m, sig) == SS.verify(one, pk, m, sig) : Bool}:  %Equal.sym(Bool, B.has_len(32n, pk), CV.length_is(32n, pk), BL.hl_is(32n, pk)) : {SC.verify_len(pk, m, sig, Bool.and(_, B.has_len(64n, sig))) == SS.verify_len(one, pk, m, sig, Bool.and(CV.length_is(32n, pk), CV.length_is(64n, sig))) : Bool}  %Equal.sym(Bool, B.has_len(64n, sig), CV.length_is(64n, sig), BL.hl_is(64n, sig)) : {SC.verify_len(pk, m, sig, Bool.and(CV.length_is(32n, pk), _)) == SS.verify_len(one, pk, m, sig, Bool.and(CV.length_is(32n, pk), CV.length_is(64n, sig))) : Bool}  vlen(one, h1, pk, m, sig, CV.length_is(32n, pk), CV.length_is(64n, sig), BL.hl_is(32n, pk), BL.hl_is(64n, sig))# ---- signing ----def sok(+sig: List<&2, U32>, b: Bool) -> {SC.sign_ok(sig, b) == SS.sign_if(sig, b) : Maybe<&2, List<&2, U32>>}:  match b:    case True{}:      {==}    case False{}:      {==}def sfin(+one: Nat, +h1: {one == 1n : Nat}, +pb: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>) -> {SC.sign_fin(pb, m, sig) == SS.sign_fin(one, pb, m, sig) : Maybe<&2, List<&2, U32>>}:  %Equal.sym(Bool, SC.verify(pb, m, sig), SS.verify(one, pb, m, sig), verify_v(one, h1, pb, m, sig)) : {SC.sign_ok(sig, _) == SS.sign_if(sig, SS.verify(one, pb, m, sig)) : Maybe<&2, List<&2, U32>>}  sok(sig, SS.verify(one, pb, m, sig))def ax_l(+one: Nat, +x: List<&2, Nat>, +y: List<&2, Nat>, +ha: {PA.ared(one, P.Affine{x, y}) == True{} : Bool}) -> {FS.limbs16(one, 16n, x) == True{} : Bool}:  SL.l16(one, x, Lg.and_left(PT.red(one, x), PT.red(one, y), ha))def sk_v(+one: Nat, +h1: {one == 1n : Nat}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}, +pb: List<&2, U32>, +m: List<&2, U32>, +k0: List<&2, Nat>, +hk0: {FS.reduced(one, FS.order(one), k0) == True{} : Bool}, a: P.Affine, +ha: {PA.ared(one, a) == True{} : Bool}) -> {SC.sign_k(d, pb, m, k0, a) == SS.sign_r(one, FS.value(one, d), pb, m, FS.value(one, k0), PA.av(one, a)) : Maybe<&2, List<&2, U32>>}:  match a:    case P.Affine{+rx, +ry}:      +hrx = ax_l(one, rx, ry, ha)      +hk = even_r(one, h1, ry, k0, hk0)      +he = th_r(one, h1, SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))      +hm = SO.mul_r(one, h1, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d, he, hd)      +hs = SO.add_r(one, h1, S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d), hk, hm)      %Equal.sym(List<&2, U32>, B.to_be(rx), CV.i2osp(32n, FS.value(one, rx)), tbv(one, h1, rx, hrx)) : {SC.sign_fin(pb, m, List.append(&2, U32, _, B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, B.to_be(rx), List.append(&2, U32, pb, m))))), d))))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(List<&2, U32>, B.to_be(rx), CV.i2osp(32n, FS.value(one, rx)), tbv(one, h1, rx, hrx)) : {SC.sign_fin(pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, _, List.append(&2, U32, pb, m))))), d))))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(List<&2, U32>, SC.tag_challenge(), SS.tag_challenge(), tc()) : {SC.sign_fin(pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(_, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d))))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(Maybe<&2, List<&2, U32>>, SC.sign_fin(pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d))))), SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d))))), sfin(one, h1, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d)))))) : {_ == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(List<&2, U32>, B.to_be(S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d))), CV.i2osp(32n, FS.value(one, S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d)))), tbv(one, h1, S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d)), SL.sl16(one, S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d)), hs))) : {SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), _)) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(Nat, FS.value(one, S.add(S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d))), FS.madd(FS.order(one), FS.value(one, S.select(SC.is_odd(ry), S.neg(k0), k0)), FS.value(one, S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d))), SO.add_v(one, h1, S.select(SC.is_odd(ry), S.neg(k0), k0), S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d), hk, hm)) : {SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, _))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(Nat, FS.value(one, S.mul(S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d)), FS.mmul(FS.order(one), FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))))), FS.value(one, d)), SO.mul_v(one, h1, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m))))), d, he, hd)) : {SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), FS.value(one, S.select(SC.is_odd(ry), S.neg(k0), k0)), _)))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(Nat, FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))))), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), th_v(one, h1, SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))) : {SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), FS.value(one, S.select(SC.is_odd(ry), S.neg(k0), k0)), FS.mmul(FS.order(one), _, FS.value(one, d)))))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(Nat, FS.value(one, S.select(SC.is_odd(ry), S.neg(k0), k0)), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), even_v(one, h1, ry, k0, hk0)) : {SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), _, FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) == SS.sign_fin(one, pb, m, List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), CV.i2osp(32n, FS.madd(FS.order(one), SS.even(FS.order(one), FS.value(one, ry), FS.value(one, k0)), FS.mmul(FS.order(one), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.i2osp(32n, FS.value(one, rx)), List.append(&2, U32, pb, m)))), FS.order(one)), FS.value(one, d)))))) : Maybe<&2, List<&2, U32>>}      {==}def snz(+one: Nat, +h1: {one == 1n : Nat}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}, +pb: List<&2, U32>, +m: List<&2, U32>, +k0: List<&2, Nat>, +hk0: {FS.reduced(one, FS.order(one), k0) == True{} : Bool}, z: Bool) -> {SC.sign_nz(d, pb, m, k0, Bool.not(z)) == SS.sign_kz(one, FS.value(one, d), pb, m, FS.value(one, k0), z) : Maybe<&2, List<&2, U32>>}:  match z:    case True{}:      {==}    case False{}:      +hg = PA.g_r(one, h1)      +hm = PM.mul_r(one, h1, k0, P.g(), SL.sl16(one, k0, hk0), hg)      %Equal.sym(CV.SPoint, CV.g(one), PT.pv(one, P.g()), Equal.sym(CV.SPoint, PT.pv(one, P.g()), CV.g(one), PA.g_v(one, h1))) : {SC.sign_k(d, pb, m, k0, P.to_affine(P.mul(k0, P.g()))) == SS.sign_r(one, FS.value(one, d), pb, m, FS.value(one, k0), CV.to_affine(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, k0), _))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(CV.SPoint, CV.pmul(FS.prime(one), FS.value(one, k0), PT.pv(one, P.g())), PT.pv(one, P.mul(k0, P.g())), Equal.sym(CV.SPoint, PT.pv(one, P.mul(k0, P.g())), CV.pmul(FS.prime(one), FS.value(one, k0), PT.pv(one, P.g())), PM.mul_v(one, h1, k0, P.g(), SL.sl16(one, k0, hk0), hg))) : {SC.sign_k(d, pb, m, k0, P.to_affine(P.mul(k0, P.g()))) == SS.sign_r(one, FS.value(one, d), pb, m, FS.value(one, k0), CV.to_affine(FS.prime(one), _)) : Maybe<&2, List<&2, U32>>}      %Equal.sym(CV.SAffine, CV.to_affine(FS.prime(one), PT.pv(one, P.mul(k0, P.g()))), PA.av(one, P.to_affine(P.mul(k0, P.g()))), Equal.sym(CV.SAffine, PA.av(one, P.to_affine(P.mul(k0, P.g()))), CV.to_affine(FS.prime(one), PT.pv(one, P.mul(k0, P.g()))), PA.aff_v(one, h1, P.mul(k0, P.g()), hm))) : {SC.sign_k(d, pb, m, k0, P.to_affine(P.mul(k0, P.g()))) == SS.sign_r(one, FS.value(one, d), pb, m, FS.value(one, k0), _) : Maybe<&2, List<&2, U32>>}      sk_v(one, h1, d, hd, pb, m, k0, hk0, P.to_affine(P.mul(k0, P.g())), PA.aff_r(one, h1, P.mul(k0, P.g()), hm))def sk2(+one: Nat, +h1: {one == 1n : Nat}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}, +pb: List<&2, U32>, +m: List<&2, U32>, +k0: List<&2, Nat>, +hk0: {FS.reduced(one, FS.order(one), k0) == True{} : Bool}) -> {SC.sign_nz(d, pb, m, k0, Bool.not(S.is_zero(k0))) == SS.sign_k(one, FS.value(one, d), pb, m, FS.value(one, k0)) : Maybe<&2, List<&2, U32>>}:  %Equal.sym(Bool, S.is_zero(k0), Nat.is_eq(FS.value(one, k0), 0n), FW.is_zero_s(one, h1, k0)) : {SC.sign_nz(d, pb, m, k0, Bool.not(_)) == SS.sign_kz(one, FS.value(one, d), pb, m, FS.value(one, k0), Nat.is_eq(FS.value(one, k0), 0n)) : Maybe<&2, List<&2, U32>>}  snz(one, h1, d, hd, pb, m, k0, hk0, Nat.is_eq(FS.value(one, k0), 0n))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))))def s3(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +hl: {B.has_len(32n, sk) == True{} : Bool}, +m: List<&2, U32>, +aux: List<&2, U32>, c: Bool, +hc: {Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))) == c : Bool}) -> {SC.sign_d(m, aux, SC.secret_if(B.of_be(sk), c)) == SS.sign_ok(one, sk, m, aux, c) : Maybe<&2, List<&2, U32>>}:  match c:    case True{}:      +hdl = BY.of_be_limbs(one, h1, sk, hl)      +hlt = I.lt_subst_l(CV.os2ip(sk), FS.value(one, B.of_be(sk)), FS.order(one), Equal.sym(Nat, FS.value(one, B.of_be(sk)), CV.os2ip(sk), BY.of_be_value(one, h1, sk)), Lg.and_right(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one)), hc))      +hd0 = red_n(one, B.of_be(sk), hdl, hlt)      +hg = PA.g_r(one, h1)      +hm = PM.mul_r(one, h1, B.of_be(sk), P.g(), hdl, hg)      %Equal.sym(Nat, CV.os2ip(sk), FS.value(one, B.of_be(sk)), Equal.sym(Nat, FS.value(one, B.of_be(sk)), CV.os2ip(sk), BY.of_be_value(one, h1, sk))) : {SC.sign_p(B.of_be(sk), m, aux, P.to_affine(P.mul(B.of_be(sk), P.g()))) == SS.sign_p(one, _, m, aux, CV.to_affine(FS.prime(one), CV.pmul(FS.prime(one), CV.os2ip(sk), CV.g(one)))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(Nat, CV.os2ip(sk), FS.value(one, B.of_be(sk)), Equal.sym(Nat, FS.value(one, B.of_be(sk)), CV.os2ip(sk), BY.of_be_value(one, h1, sk))) : {SC.sign_p(B.of_be(sk), m, aux, P.to_affine(P.mul(B.of_be(sk), P.g()))) == SS.sign_p(one, FS.value(one, B.of_be(sk)), m, aux, CV.to_affine(FS.prime(one), CV.pmul(FS.prime(one), _, CV.g(one)))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(CV.SPoint, CV.g(one), PT.pv(one, P.g()), Equal.sym(CV.SPoint, PT.pv(one, P.g()), CV.g(one), PA.g_v(one, h1))) : {SC.sign_p(B.of_be(sk), m, aux, P.to_affine(P.mul(B.of_be(sk), P.g()))) == SS.sign_p(one, FS.value(one, B.of_be(sk)), m, aux, CV.to_affine(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, B.of_be(sk)), _))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(CV.SPoint, CV.pmul(FS.prime(one), FS.value(one, B.of_be(sk)), PT.pv(one, P.g())), PT.pv(one, P.mul(B.of_be(sk), P.g())), Equal.sym(CV.SPoint, PT.pv(one, P.mul(B.of_be(sk), P.g())), CV.pmul(FS.prime(one), FS.value(one, B.of_be(sk)), PT.pv(one, P.g())), PM.mul_v(one, h1, B.of_be(sk), P.g(), hdl, hg))) : {SC.sign_p(B.of_be(sk), m, aux, P.to_affine(P.mul(B.of_be(sk), P.g()))) == SS.sign_p(one, FS.value(one, B.of_be(sk)), m, aux, CV.to_affine(FS.prime(one), _)) : Maybe<&2, List<&2, U32>>}      %Equal.sym(CV.SAffine, CV.to_affine(FS.prime(one), PT.pv(one, P.mul(B.of_be(sk), P.g()))), PA.av(one, P.to_affine(P.mul(B.of_be(sk), P.g()))), Equal.sym(CV.SAffine, PA.av(one, P.to_affine(P.mul(B.of_be(sk), P.g()))), CV.to_affine(FS.prime(one), PT.pv(one, P.mul(B.of_be(sk), P.g()))), PA.aff_v(one, h1, P.mul(B.of_be(sk), P.g()), hm))) : {SC.sign_p(B.of_be(sk), m, aux, P.to_affine(P.mul(B.of_be(sk), P.g()))) == SS.sign_p(one, FS.value(one, B.of_be(sk)), m, aux, _) : Maybe<&2, List<&2, U32>>}      spk(one, h1, B.of_be(sk), hd0, m, aux, P.to_affine(P.mul(B.of_be(sk), P.g())), PA.aff_r(one, h1, P.mul(B.of_be(sk), P.g()), hm))    case False{}:      {==}def s2(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +m: List<&2, U32>, +aux: List<&2, U32>, b: Bool, +hb: {B.has_len(32n, sk) == b : Bool}) -> {SC.sign_d(m, aux, SC.secret_if(B.of_be(sk), Bool.and(b, Bool.and(Bool.not(S.is_zero(B.of_be(sk))), S.lt_n(B.of_be(sk)))))) == SS.sign_ok(one, sk, m, aux, Bool.and(b, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))) : Maybe<&2, List<&2, U32>>}:  match b:    case True{}:      %Equal.sym(Bool, S.is_zero(B.of_be(sk)), Nat.is_eq(FS.value(one, B.of_be(sk)), 0n), FW.is_zero_s(one, h1, B.of_be(sk))) : {SC.sign_d(m, aux, SC.secret_if(B.of_be(sk), Bool.and(b, Bool.and(Bool.not(_), S.lt_n(B.of_be(sk)))))) == SS.sign_ok(one, sk, m, aux, Bool.and(b, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(Bool, S.lt_n(B.of_be(sk)), Nat.is_lt(FS.value(one, B.of_be(sk)), FS.order(one)), FW.lt_n_s(one, h1, B.of_be(sk))) : {SC.sign_d(m, aux, SC.secret_if(B.of_be(sk), Bool.and(b, Bool.and(Bool.not(Nat.is_eq(FS.value(one, B.of_be(sk)), 0n)), _)))) == SS.sign_ok(one, sk, m, aux, Bool.and(b, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(Nat, FS.value(one, B.of_be(sk)), CV.os2ip(sk), BY.of_be_value(one, h1, sk)) : {SC.sign_d(m, aux, SC.secret_if(B.of_be(sk), Bool.and(b, Bool.and(Bool.not(Nat.is_eq(_, 0n)), Nat.is_lt(FS.value(one, B.of_be(sk)), FS.order(one)))))) == SS.sign_ok(one, sk, m, aux, Bool.and(b, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(Nat, FS.value(one, B.of_be(sk)), CV.os2ip(sk), BY.of_be_value(one, h1, sk)) : {SC.sign_d(m, aux, SC.secret_if(B.of_be(sk), Bool.and(b, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(_, FS.order(one)))))) == SS.sign_ok(one, sk, m, aux, Bool.and(b, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))) : Maybe<&2, List<&2, U32>>}      s3(one, h1, sk, hb, m, aux, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))), {==})    case False{}:      {==}def s1(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +m: List<&2, U32>, +aux: List<&2, U32>, a: Bool, +ha: {B.has_len(32n, aux) == a : Bool}) -> {SC.sign_len(sk, m, aux, a) == SS.sign_ok(one, sk, m, aux, Bool.and(a, SS.secret_ok(one, sk))) : Maybe<&2, List<&2, U32>>}:  match a:    case True{}:      %Equal.sym(Bool, B.has_len(32n, sk), CV.length_is(32n, sk), BL.hl_is(32n, sk)) : {SC.sign_d(m, aux, SC.secret_if(B.of_be(sk), Bool.and(_, Bool.and(Bool.not(S.is_zero(B.of_be(sk))), S.lt_n(B.of_be(sk)))))) == SS.sign_ok(one, sk, m, aux, Bool.and(CV.length_is(32n, sk), Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))) : Maybe<&2, List<&2, U32>>}      s2(one, h1, sk, m, aux, CV.length_is(32n, sk), BL.hl_is(32n, sk))    case False{}:      {==}# BIP-340 signingdef sign_v(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +m: List<&2, U32>, +aux: List<&2, U32>) -> {SC.sign(sk, m, aux) == SS.sign(one, sk, m, aux) : Maybe<&2, List<&2, U32>>}:  %Equal.sym(Bool, B.has_len(32n, aux), CV.length_is(32n, aux), BL.hl_is(32n, aux)) : {SC.sign_len(sk, m, aux, _) == SS.sign_ok(one, sk, m, aux, Bool.and(CV.length_is(32n, aux), SS.secret_ok(one, sk))) : Maybe<&2, List<&2, U32>>}  s1(one, h1, sk, m, aux, CV.length_is(32n, aux), BL.hl_is(32n, aux))# ---- x-only public keys ----def paff(+one: Nat, +h1: {one == 1n : Nat}, a: P.Affine, +ha: {PA.ared(one, a) == True{} : Bool}) -> {SC.pubkey_aff(a) == SS.pub_of(PA.av(one, a)) : List<&2, U32>}:  match a:    case P.Affine{+x, +y}:      tbv(one, h1, x, ax_l(one, x, y, ha))def pk3(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +hl: {B.has_len(32n, sk) == True{} : Bool}, c: Bool) -> {SC.pubkey_d(SC.secret_if(B.of_be(sk), c)) == SS.pubkey_ok(one, sk, c) : Maybe<&2, List<&2, U32>>}:  match c:    case True{}:      +hdl = BY.of_be_limbs(one, h1, sk, hl)      +hg = PA.g_r(one, h1)      +hm = PM.mul_r(one, h1, B.of_be(sk), P.g(), hdl, hg)      %Equal.sym(Nat, CV.os2ip(sk), FS.value(one, B.of_be(sk)), Equal.sym(Nat, FS.value(one, B.of_be(sk)), CV.os2ip(sk), BY.of_be_value(one, h1, sk))) : {Some{SC.pubkey_aff(P.to_affine(P.mul(B.of_be(sk), P.g())))} == Some{SS.pub_of(CV.to_affine(FS.prime(one), CV.pmul(FS.prime(one), _, CV.g(one))))} : Maybe<&2, List<&2, U32>>}      %Equal.sym(CV.SPoint, CV.g(one), PT.pv(one, P.g()), Equal.sym(CV.SPoint, PT.pv(one, P.g()), CV.g(one), PA.g_v(one, h1))) : {Some{SC.pubkey_aff(P.to_affine(P.mul(B.of_be(sk), P.g())))} == Some{SS.pub_of(CV.to_affine(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, B.of_be(sk)), _)))} : Maybe<&2, List<&2, U32>>}      %Equal.sym(CV.SPoint, CV.pmul(FS.prime(one), FS.value(one, B.of_be(sk)), PT.pv(one, P.g())), PT.pv(one, P.mul(B.of_be(sk), P.g())), Equal.sym(CV.SPoint, PT.pv(one, P.mul(B.of_be(sk), P.g())), CV.pmul(FS.prime(one), FS.value(one, B.of_be(sk)), PT.pv(one, P.g())), PM.mul_v(one, h1, B.of_be(sk), P.g(), hdl, hg))) : {Some{SC.pubkey_aff(P.to_affine(P.mul(B.of_be(sk), P.g())))} == Some{SS.pub_of(CV.to_affine(FS.prime(one), _))} : Maybe<&2, List<&2, U32>>}      %Equal.sym(CV.SAffine, CV.to_affine(FS.prime(one), PT.pv(one, P.mul(B.of_be(sk), P.g()))), PA.av(one, P.to_affine(P.mul(B.of_be(sk), P.g()))), Equal.sym(CV.SAffine, PA.av(one, P.to_affine(P.mul(B.of_be(sk), P.g()))), CV.to_affine(FS.prime(one), PT.pv(one, P.mul(B.of_be(sk), P.g()))), PA.aff_v(one, h1, P.mul(B.of_be(sk), P.g()), hm))) : {Some{SC.pubkey_aff(P.to_affine(P.mul(B.of_be(sk), P.g())))} == Some{SS.pub_of(_)} : Maybe<&2, List<&2, U32>>}      %Equal.sym(List<&2, U32>, SC.pubkey_aff(P.to_affine(P.mul(B.of_be(sk), P.g()))), SS.pub_of(PA.av(one, P.to_affine(P.mul(B.of_be(sk), P.g())))), paff(one, h1, P.to_affine(P.mul(B.of_be(sk), P.g())), PA.aff_r(one, h1, P.mul(B.of_be(sk), P.g()), hm))) : {Some{_} == Some{SS.pub_of(PA.av(one, P.to_affine(P.mul(B.of_be(sk), P.g()))))} : Maybe<&2, List<&2, U32>>}      {==}    case False{}:      {==}def pk2(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, b: Bool, +hb: {B.has_len(32n, sk) == b : Bool}) -> {SC.pubkey_d(SC.secret_if(B.of_be(sk), Bool.and(b, Bool.and(Bool.not(S.is_zero(B.of_be(sk))), S.lt_n(B.of_be(sk)))))) == SS.pubkey_ok(one, sk, Bool.and(b, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))) : Maybe<&2, List<&2, U32>>}:  match b:    case True{}:      %Equal.sym(Bool, S.is_zero(B.of_be(sk)), Nat.is_eq(FS.value(one, B.of_be(sk)), 0n), FW.is_zero_s(one, h1, B.of_be(sk))) : {SC.pubkey_d(SC.secret_if(B.of_be(sk), Bool.and(b, Bool.and(Bool.not(_), S.lt_n(B.of_be(sk)))))) == SS.pubkey_ok(one, sk, Bool.and(b, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(Bool, S.lt_n(B.of_be(sk)), Nat.is_lt(FS.value(one, B.of_be(sk)), FS.order(one)), FW.lt_n_s(one, h1, B.of_be(sk))) : {SC.pubkey_d(SC.secret_if(B.of_be(sk), Bool.and(b, Bool.and(Bool.not(Nat.is_eq(FS.value(one, B.of_be(sk)), 0n)), _)))) == SS.pubkey_ok(one, sk, Bool.and(b, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(Nat, FS.value(one, B.of_be(sk)), CV.os2ip(sk), BY.of_be_value(one, h1, sk)) : {SC.pubkey_d(SC.secret_if(B.of_be(sk), Bool.and(b, Bool.and(Bool.not(Nat.is_eq(_, 0n)), Nat.is_lt(FS.value(one, B.of_be(sk)), FS.order(one)))))) == SS.pubkey_ok(one, sk, Bool.and(b, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))) : Maybe<&2, List<&2, U32>>}      %Equal.sym(Nat, FS.value(one, B.of_be(sk)), CV.os2ip(sk), BY.of_be_value(one, h1, sk)) : {SC.pubkey_d(SC.secret_if(B.of_be(sk), Bool.and(b, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(_, FS.order(one)))))) == SS.pubkey_ok(one, sk, Bool.and(b, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))) : Maybe<&2, List<&2, U32>>}      pk3(one, h1, sk, hb, Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))    case False{}:      {==}# the x-only public key of a secret keydef pubkey_v(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>) -> {SC.pubkey(sk) == SS.pubkey(one, sk) : Maybe<&2, List<&2, U32>>}:  %Equal.sym(Bool, B.has_len(32n, sk), CV.length_is(32n, sk), BL.hl_is(32n, sk)) : {SC.pubkey_d(SC.secret_if(B.of_be(sk), Bool.and(_, Bool.and(Bool.not(S.is_zero(B.of_be(sk))), S.lt_n(B.of_be(sk)))))) == SS.pubkey_ok(one, sk, Bool.and(CV.length_is(32n, sk), Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), FS.order(one))))) : Maybe<&2, List<&2, U32>>}  pk2(one, h1, sk, CV.length_is(32n, sk), BL.hl_is(32n, sk))