proofs/crypto/secp256k1/pschn.bend

bend-collections-laws-crypto@1.0.0.0 · 365 lines · 41 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pschn.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha.bend as FIPS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
6import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend as SS
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/sha256.bend as SHA
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
9import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend as F
10import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as S
11import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
12import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
13import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend as SC
14import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/laws.bend as SHL
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/correctness.bend as SHC
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend as SO
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as FW
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY
22import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT
23import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as SL
24import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pmul.bend as PM
25import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA
26import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as PE
27import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL
28import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend as SQ
29import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ptwo.bend as TW
30
31# BIP-340 Schnorr signatures of src/crypto/secp256k1/schnorr.bend against
32# spec/crypto/secp256k1/schnorr.bend: tagged hashes, verification, signing
33# and x-only public keys.
34
35# ---- bytes and hashes ----
36
37def fips_len(+bytes: List<&2, U32>) -> {List.length(&2, U32, FIPS.sha256_bytes(bytes)) == 32n : Nat}:
38  SHC.digest_octets_length(FIPS.blocks(FIPS.prepare(bytes, 48n), FIPS.constants())(FIPS.initial()))
39
40def 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>}:
41  %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>}
42  %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>}
43  {==}
44
45def xor_v(xs: List<&2, U32>, ys: List<&2, U32>) -> {SC.xor_bytes(xs, ys) == SS.xor_bytes(xs, ys) : List<&2, U32>}:
46  match xs ys:
47    case +x <> xt +y <> yt:
48      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))
49    case Nil{} _:
50      {==}
51    case _ Nil{}:
52      {==}
53
54def tagged_v(+tag: List<&2, U32>, +x: List<&2, U32>) -> {SC.tagged(tag, x) == SS.tagged(tag, x) : List<&2, U32>}:
55  %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>}
56  %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>}
57  %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>}
58  {==}
59
60def tagged_len(+tag: List<&2, U32>, +x: List<&2, U32>) -> {B.has_len(32n, SS.tagged(tag, x)) == True{} : Bool}:
61  %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}
62  %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}
63  {==}
64
65# int(hash) mod n
66def 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}:
67  %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}
68  SQ.hash_v(one, h1, SS.tagged(tag, x), tagged_len(tag, x))
69
70def 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}:
71  %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}
72  SQ.hash_r(one, h1, SS.tagged(tag, x), tagged_len(tag, x))
73
74# ---- the even-y key or nonce: x or n - x ----
75
76def 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}:
77  match q:
78    case 0n:
79      %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}
80      {==}
81    case 1n:
82      %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}
83      SO.neg_v(one, h1, x, hx)
84    case 2n+ +c:
85      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))
86
87def 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}:
88  match q:
89    case 0n:
90      %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}
91      hx
92    case 1n:
93      %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}
94      SO.neg_r(one, h1, x, hx)
95    case 2n+ +c:
96      Empty.absurd({FS.reduced(one, FS.order(one), S.select(2n+c, S.neg(x), x)) == True{} : Bool}, SL.not01(c, hq))
97
98def 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}:
99  %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}
100  ev_q(one, h1, Nat.mod(FS.value(one, y), 2n), x, hx, PE.mod2_lt(FS.value(one, y)))
101
102def 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}:
103  %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}
104  ev_qr(one, h1, Nat.mod(FS.value(one, y), 2n), x, hx, PE.mod2_lt(FS.value(one, y)))
105
106# ---- verification ----
107
108def 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}:
109  match a:
110    case P.Affine{+x, +y}:
111      +hx = SL.l16(one, x, Lg.and_left(PT.red(one, x), PT.red(one, y), ha))
112      %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}
113      %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}
114      {==}
115
116def 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}:
117  %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}
118  %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}
119  va(one, h1, r, hr, CV.is_inf(PT.pv(one, rr)), P.to_affine(rr), PA.aff_r(one, h1, rr, hrr))
120
121def vrs(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hr: {FS.limbs16(one, 16n, r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}, +e: List<&2, Nat>, +he: {FS.reduced(one, FS.order(one), e) == True{} : Bool}, +pp: P.Point, +hp: {PT.pred(one, pp) == True{} : Bool}) -> {SC.verify_r(r, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))) == SS.verify_rs(one, FS.value(one, r), FS.value(one, s), FS.value(one, e), PT.pv(one, pp)) : Bool}:
122  +hn = SO.neg_r(one, h1, e, he)
123  +hq = TW.two_r(one, h1, s, hs, S.neg(e), hn, pp, hp)
124  %Equal.sym(Bool, SC.verify_r(r, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))), SS.check_r(FS.value(one, r), CV.is_inf(PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp)))), CV.to_affine(FS.prime(one), PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))))), vr(one, h1, r, hr, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp)), hq)) : {_ == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
125  %Equal.sym(CV.SPoint, PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.neg(e)), PT.pv(one, pp))), TW.two_v(one, h1, s, hs, S.neg(e), hn, pp, hp)) : {SS.check_r(FS.value(one, r), CV.is_inf(_), CV.to_affine(FS.prime(one), PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))))) == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
126  %Equal.sym(CV.SPoint, PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.neg(e)), PT.pv(one, pp))), TW.two_v(one, h1, s, hs, S.neg(e), hn, pp, hp)) : {SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.neg(e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), _)) == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
127  %Equal.sym(Nat, FS.value(one, S.neg(e)), FS.mneg(FS.order(one), FS.value(one, e)), SO.neg_v(one, h1, e, he)) : {SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), _, PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.neg(e)), PT.pv(one, pp))))) == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
128  %Equal.sym(Nat, FS.value(one, S.neg(e)), FS.mneg(FS.order(one), FS.value(one, e)), SO.neg_v(one, h1, e, he)) : {SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), _, PT.pv(one, pp))))) == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
129  {==}
130
131def tc() -> {SC.tag_challenge() == SS.tag_challenge() : List<&2, U32>}:
132  {==}
133
134def ta() -> {SC.tag_aux() == SS.tag_aux() : List<&2, U32>}:
135  {==}
136
137def tn() -> {SC.tag_nonce() == SS.tag_nonce() : List<&2, U32>}:
138  {==}
139
140def 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}:
141  Lg.and_intro(FS.limbs16(one, 16n, x), Nat.is_lt(FS.value(one, x), FS.order(one)), hl, h)
142
143def 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}:
144  match a b:
145    case True{} True{}:
146      vrs(one, h1, r, hlr, s, red_n(one, s, hls, hb), e, he, pp, hp)
147    case True{} False{}:
148      {==}
149    case False{} _:
150      {==}
151
152def 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}:
153  match mp:
154    case None{}:
155      {==}
156    case Some{+pp}:
157      +hlr = BY.of_be_limbs(one, h1, CV.first(32n, sig), BL.pre_len(32n, 32n, sig, hsig))
158      +hls = BY.of_be_limbs(one, h1, CV.after(32n, sig), BL.suf_len(32n, 32n, sig, hsig))
159      %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}
160      %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}
161      %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}
162      %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}
163      %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}
164      %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}
165      %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}
166      %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}
167      %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}
168      %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}
169      %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}
170      %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}
171      %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}
172      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)), {==}, {==})
173
174def 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>}:
175  match b:
176    case True{}:
177      PE.decompress_v(one, h1, x, 0n, SL.red_of(one, x, hl, hb), {==})
178    case False{}:
179      {==}
180
181def 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}:
182  match b:
183    case True{}:
184      PE.decompress_r(one, h1, x, 0n, SL.red_of(one, x, hl, hb), {==})
185    case False{}:
186      {==}
187
188def 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>}:
189  %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>}
190  lxb(one, h1, x, hl, Nat.is_lt(FS.value(one, x), FS.prime(one)), {==})
191
192def 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}:
193  %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}
194  lxr(one, h1, x, hl, Nat.is_lt(FS.value(one, x), FS.prime(one)), {==})
195
196def 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}:
197  match a b:
198    case True{} True{}:
199      +hl = BY.of_be_limbs(one, h1, pk, ha)
200      %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}
201      %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}
202      vp(one, h1, pk, m, sig, hb, SC.lift_x(B.of_be(pk)), lx_r(one, h1, B.of_be(pk), hl))
203    case True{} False{}:
204      {==}
205    case False{} _:
206      {==}
207
208# BIP-340 verification
209def 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}:
210  %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}
211  %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}
212  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))
213
214# ---- signing ----
215
216def sok(+sig: List<&2, U32>, b: Bool) -> {SC.sign_ok(sig, b) == SS.sign_if(sig, b) : Maybe<&2, List<&2, U32>>}:
217  match b:
218    case True{}:
219      {==}
220    case False{}:
221      {==}
222
223def 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>>}:
224  %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>>}
225  sok(sig, SS.verify(one, pb, m, sig))
226
227def 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}:
228  SL.l16(one, x, Lg.and_left(PT.red(one, x), PT.red(one, y), ha))
229
230def 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>>}:
231  match a:
232    case P.Affine{+rx, +ry}:
233      +hrx = ax_l(one, rx, ry, ha)
234      +hk = even_r(one, h1, ry, k0, hk0)
235      +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)))
236      +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)
237      +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)
238      %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>>}
239      %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>>}
240      %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>>}
241      %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>>}
242      %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>>}
243      %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>>}
244      %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>>}
245      %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>>}
246      %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>>}
247      {==}
248
249def 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>>}:
250  match z:
251    case True{}:
252      {==}
253    case False{}:
254      +hg = PA.g_r(one, h1)
255      +hm = PM.mul_r(one, h1, k0, P.g(), SL.sl16(one, k0, hk0), hg)
256      %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>>}
257      %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>>}
258      %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>>}
259      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))
260
261def 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>>}:
262  %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>>}
263  snz(one, h1, d, hd, pb, m, k0, hk0, Nat.is_eq(FS.value(one, k0), 0n))
264
265def spk(+one: Nat, +h1: {one == 1n : Nat}, +d0: List<&2, Nat>, +hd0: {FS.reduced(one, FS.order(one), d0) == True{} : Bool}, +m: List<&2, U32>, +aux: List<&2, U32>, a: P.Affine, +ha: {PA.ared(one, a) == True{} : Bool}) -> {SC.sign_p(d0, m, aux, a) == SS.sign_p(one, FS.value(one, d0), m, aux, PA.av(one, a)) : Maybe<&2, List<&2, U32>>}:
266  match a:
267    case P.Affine{+px, +py}:
268      +hpx = ax_l(one, px, py, ha)
269      +hd = even_r(one, h1, py, d0, hd0)
270      %Equal.sym(List<&2, U32>, B.to_be(px), CV.i2osp(32n, FS.value(one, px)), tbv(one, h1, px, hpx)) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), _, m, S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, B.to_be(px), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, B.to_be(px), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
271      %Equal.sym(List<&2, U32>, B.to_be(px), CV.i2osp(32n, FS.value(one, px)), tbv(one, h1, px, hpx)) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, _, m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, B.to_be(px), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
272      %Equal.sym(List<&2, U32>, B.to_be(px), CV.i2osp(32n, FS.value(one, px)), tbv(one, h1, px, hpx)) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, _, m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
273      %Equal.sym(List<&2, U32>, B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), tbv(one, h1, S.select(SC.is_odd(py), S.neg(d0), d0), SL.sl16(one, S.select(SC.is_odd(py), S.neg(d0), d0), hd))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(_, SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
274      %Equal.sym(List<&2, U32>, B.to_be(S.select(SC.is_odd(py), S.neg(d0), d0)), CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), tbv(one, h1, S.select(SC.is_odd(py), S.neg(d0), d0), SL.sl16(one, S.select(SC.is_odd(py), S.neg(d0), d0), hd))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(_, SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
275      %Equal.sym(List<&2, U32>, SC.tag_nonce(), SS.tag_nonce(), tn()) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(_, List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SC.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
276      %Equal.sym(List<&2, U32>, SC.tag_nonce(), SS.tag_nonce(), tn()) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(_, List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
277      %Equal.sym(List<&2, U32>, SC.tag_aux(), SS.tag_aux(), ta()) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(_, aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SC.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
278      %Equal.sym(List<&2, U32>, SC.tag_aux(), SS.tag_aux(), ta()) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(_, aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
279      %Equal.sym(List<&2, U32>, SC.tagged(SS.tag_aux(), aux), SS.tagged(SS.tag_aux(), aux), tagged_v(SS.tag_aux(), aux)) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), _), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SC.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
280      %Equal.sym(List<&2, U32>, SC.tagged(SS.tag_aux(), aux), SS.tagged(SS.tag_aux(), aux), tagged_v(SS.tag_aux(), aux)) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), _), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
281      %Equal.sym(List<&2, U32>, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), xor_v(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, _, List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
282      %Equal.sym(List<&2, U32>, SC.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), xor_v(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, _, List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
283      %Equal.sym(Nat, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0)), Equal.sym(Nat, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0)), SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), even_v(one, h1, py, d0, hd0))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, _, CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
284      %Equal.sym(Nat, SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0)), Equal.sym(Nat, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0)), SS.even(FS.order(one), FS.value(one, py), FS.value(one, d0)), even_v(one, h1, py, d0, hd0))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0)), CV.i2osp(32n, FS.value(one, px)), m, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, _), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one))) : Maybe<&2, List<&2, U32>>}
285      %Equal.sym(Nat, Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one)), FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))), Equal.sym(Nat, FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))), Nat.mod(CV.os2ip(SS.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))), FS.order(one)), th_v(one, h1, SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))) : {SC.sign_nz(S.select(SC.is_odd(py), S.neg(d0), d0), CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), Bool.not(S.is_zero(S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m)))))))) == SS.sign_k(one, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0)), CV.i2osp(32n, FS.value(one, px)), m, _) : Maybe<&2, List<&2, U32>>}
286      sk2(one, h1, S.select(SC.is_odd(py), S.neg(d0), d0), hd, CV.i2osp(32n, FS.value(one, px)), m, S.reduce(B.of_be(SC.tagged(SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))), th_r(one, h1, SS.tag_nonce(), List.append(&2, U32, SS.xor_bytes(CV.i2osp(32n, FS.value(one, S.select(SC.is_odd(py), S.neg(d0), d0))), SS.tagged(SS.tag_aux(), aux)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, px)), m))))
287
288def 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>>}:
289  match c:
290    case True{}:
291      +hdl = BY.of_be_limbs(one, h1, sk, hl)
292      +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))
293      +hd0 = red_n(one, B.of_be(sk), hdl, hlt)
294      +hg = PA.g_r(one, h1)
295      +hm = PM.mul_r(one, h1, B.of_be(sk), P.g(), hdl, hg)
296      %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>>}
297      %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>>}
298      %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>>}
299      %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>>}
300      %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>>}
301      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))
302    case False{}:
303      {==}
304
305def 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>>}:
306  match b:
307    case True{}:
308      %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>>}
309      %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>>}
310      %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>>}
311      %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>>}
312      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))), {==})
313    case False{}:
314      {==}
315
316def 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>>}:
317  match a:
318    case True{}:
319      %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>>}
320      s2(one, h1, sk, m, aux, CV.length_is(32n, sk), BL.hl_is(32n, sk))
321    case False{}:
322      {==}
323
324# BIP-340 signing
325def 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>>}:
326  %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>>}
327  s1(one, h1, sk, m, aux, CV.length_is(32n, aux), BL.hl_is(32n, aux))
328
329# ---- x-only public keys ----
330
331def 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>}:
332  match a:
333    case P.Affine{+x, +y}:
334      tbv(one, h1, x, ax_l(one, x, y, ha))
335
336def 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>>}:
337  match c:
338    case True{}:
339      +hdl = BY.of_be_limbs(one, h1, sk, hl)
340      +hg = PA.g_r(one, h1)
341      +hm = PM.mul_r(one, h1, B.of_be(sk), P.g(), hdl, hg)
342      %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>>}
343      %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>>}
344      %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>>}
345      %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>>}
346      %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>>}
347      {==}
348    case False{}:
349      {==}
350
351def 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>>}:
352  match b:
353    case True{}:
354      %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>>}
355      %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>>}
356      %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>>}
357      %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>>}
358      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))))
359    case False{}:
360      {==}
361
362# the x-only public key of a secret key
363def pubkey_v(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>) -> {SC.pubkey(sk) == SS.pubkey(one, sk) : Maybe<&2, List<&2, U32>>}:
364  %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>>}
365  pk2(one, h1, sk, CV.length_is(32n, sk), BL.hl_is(32n, sk))