1 # GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pschn.src; edit the .src 2 import Base 3 import ../../../spec/crypto/sha.bend as FIPS 4 import ../../../spec/crypto/secp256k1/field.bend as FS 5 import ../../../spec/crypto/secp256k1/curve.bend as CV 6 import ../../../spec/crypto/secp256k1/schnorr.bend as SS 7 import ../../../src/crypto/sha/sha256.bend as SHA 8 import ../../../src/crypto/secp256k1/limbs.bend as L 9 import ../../../src/crypto/secp256k1/field.bend as F 10 import ../../../src/crypto/secp256k1/scalar.bend as S 11 import ../../../src/crypto/secp256k1/bytes.bend as B 12 import ../../../src/crypto/secp256k1/point.bend as P 13 import ../../../src/crypto/secp256k1/schnorr.bend as SC 14 import ../../lib/logic.bend as Lg 15 import ../sha/laws.bend as SHL 16 import ../sha/correctness.bend as SHC 17 import ./limbs.bend as LV 18 import ./ineq.bend as I 19 import ./scalarops.bend as SO 20 import ./fwrap.bend as FW 21 import ./bytes.bend as BY 22 import ./point.bend as PT 23 import ./sel.bend as SL 24 import ./pmul.bend as PM 25 import ./paff.bend as PA 26 import ./penc.bend as PE 27 import ./blist.bend as BL 28 import ./pscal.bend as SQ 29 import ./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 37 def 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 40 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>}: 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 45 def 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 54 def 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 60 def 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 66 def 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 70 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}: 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 76 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}: 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 87 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}: 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 98 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}: 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 102 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}: 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 108 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}: 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 116 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}: 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 121 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}: 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 131 def tc() -> {SC.tag_challenge() == SS.tag_challenge() : List<&2, U32>}: 132 {==} 133 134 def ta() -> {SC.tag_aux() == SS.tag_aux() : List<&2, U32>}: 135 {==} 136 137 def tn() -> {SC.tag_nonce() == SS.tag_nonce() : List<&2, U32>}: 138 {==} 139 140 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}: 141 Lg.and_intro(FS.limbs16(one, 16n, x), Nat.is_lt(FS.value(one, x), FS.order(one)), hl, h) 142 143 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}: 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 152 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}: 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 174 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>}: 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 181 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}: 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 188 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>}: 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 192 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}: 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 196 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}: 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 209 def 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 216 def 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 223 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>>}: 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 227 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}: 228 SL.l16(one, x, Lg.and_left(PT.red(one, x), PT.red(one, y), ha)) 229 230 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>>}: 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 249 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>>}: 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 261 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>>}: 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 265 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>>}: 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, _) : May 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 288 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>>}: 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 305 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>>}: 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 316 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>>}: 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 325 def 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 331 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>}: 332 match a: 333 case P.Affine{+x, +y}: 334 tbv(one, h1, x, ax_l(one, x, y, ha)) 335 336 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>>}: 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 351 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>>}: 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 363 def 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))