1 # GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/prec.src; edit the .src 2 import Base 3 import ../../../spec/crypto/secp256k1/field.bend as FS 4 import ../../../spec/crypto/secp256k1/curve.bend as CV 5 import ../../../spec/crypto/secp256k1/ecdsa.bend as ES 6 import ../../../src/crypto/secp256k1/limbs.bend as L 7 import ../../../src/crypto/secp256k1/field.bend as F 8 import ../../../src/crypto/secp256k1/scalar.bend as S 9 import ../../../src/crypto/secp256k1/bytes.bend as B 10 import ../../../src/crypto/secp256k1/point.bend as P 11 import ../../../src/crypto/secp256k1/ecdsa.bend as E 12 import ../../lib/nat.bend as N 13 import ../../lib/logic.bend as Lg 14 import ./consts.bend as K 15 import ./ineq.bend as I 16 import ./fieldops.bend as FO 17 import ./scalarops.bend as SO 18 import ./scalarpow.bend as SP 19 import ./fwrap.bend as FW 20 import ./bytes.bend as BY 21 import ./point.bend as PT 22 import ./sel.bend as SL 23 import ./paff.bend as PA 24 import ./penc.bend as PE 25 import ./pver.bend as PV 26 import ./rconst.bend as RC 27 import ./blist.bend as BL 28 import ./pscal.bend as SQ 29 import ./ptwo.bend as TW 30 31 # ECDSA public key recovery of src/crypto/secp256k1/ecdsa.bend (recover) 32 # against spec/crypto/secp256k1/ecdsa.bend. 33 34 # ---- lengths of the fields of r || s || id ---- 35 36 def pl1(+sig: List<&2, U32>, +h: {B.has_len(65n, sig) == True{} : Bool}) -> {B.has_len(32n, B.prefix(32n, sig)) == True{} : Bool}: 37 %Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig)) : {B.has_len(32n, _) == True{} : Bool} 38 BL.pre_len(32n, 33n, sig, h) 39 40 def pl2(+sig: List<&2, U32>, +h: {B.has_len(65n, sig) == True{} : Bool}) -> {B.has_len(32n, B.prefix(32n, B.suffix(32n, sig))) == True{} : Bool}: 41 %Equal.sym(List<&2, U32>, B.prefix(32n, B.suffix(32n, sig)), CV.first(32n, B.suffix(32n, sig)), BL.prefix_first(32n, B.suffix(32n, sig))) : {B.has_len(32n, _) == True{} : Bool} 42 %Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig)) : {B.has_len(32n, CV.first(32n, _)) == True{} : Bool} 43 BL.pre_len(32n, 1n, CV.after(32n, sig), BL.suf_len(32n, 33n, sig, h)) 44 45 # ---- Q, and its encoding ---- 46 47 def rq_b(+one: Nat, +h1: {one == 1n : Nat}, +q: P.Point, +hq: {PT.pred(one, q) == True{} : Bool}, b: Bool) -> {E.recover_q(q, b) == ES.recover_q_if(one, PT.pv(one, q), b) : Maybe<&2, List<&2, U32>>}: 48 match b: 49 case True{}: 50 {==} 51 case False{}: 52 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, P.encode_uncompressed(q), CV.encode_uncompressed(FS.prime(one), PT.pv(one, q)), PE.encode_uncompressed_v(one, h1, q, hq)) 53 54 def rq_v(+one: Nat, +h1: {one == 1n : Nat}, +q: P.Point, +hq: {PT.pred(one, q) == True{} : Bool}) -> {E.recover_q(q, P.is_inf(q)) == ES.recover_q(one, PT.pv(one, q)) : Maybe<&2, List<&2, U32>>}: 55 %Equal.sym(Bool, P.is_inf(q), CV.is_inf(PT.pv(one, q)), PA.is_inf_v(one, h1, q)) : {E.recover_q(q, _) == ES.recover_q(one, PT.pv(one, q)) : Maybe<&2, List<&2, U32>>} 56 rq_b(one, h1, q, hq, CV.is_inf(PT.pv(one, q))) 57 58 def rr(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}, m: Maybe<&2, P.Point>, +hm: {PE.mpred(one, m) == True{} : Bool}) -> {E.recover_r(z, r, s, m) == ES.recover_r(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), PE.mpv(one, m)) : Maybe<&2, List<&2, U32>>}: 59 match m: 60 case None{}: 61 {==} 62 case Some{+pr}: 63 +hi = SP.inv_r(one, h1, r, hr) 64 +hn = SO.neg_r(one, h1, z, hz) 65 +hu1 = SO.mul_r(one, h1, S.neg(z), S.inv(r), hn, hi) 66 +hu2 = SO.mul_r(one, h1, s, S.inv(r), hs, hi) 67 +q = P.add(P.mul(S.mul(S.neg(z), S.inv(r)), P.g()), P.mul(S.mul(s, S.inv(r)), pr)) 68 %Equal.sym(Maybe<&2, List<&2, U32>>, E.recover_q(P.add(P.mul(S.mul(S.neg(z), S.inv(r)), P.g()), P.mul(S.mul(s, S.inv(r)), pr)), P.is_inf(P.add(P.mul(S.mul(S.neg(z), S.inv(r)), P.g()), P.mul(S.mul(s, S.inv(r)), pr)))), ES.recover_q(one, PT.pv(one, P.add(P.mul(S.mul(S.neg(z), S.inv(r)), P.g()), P.mul(S.mul(s, S.inv(r)), pr)))), rq_v(one, h1, P.add(P.mul(S.mul(S.neg(z), S.inv(r)), P.g()), P.mul(S.mul(s, S.inv(r)), pr)), TW.two_r(one, h1, S.mul(S.neg(z), S.inv(r)), hu1, S.mul(s, S.inv(r)), hu2, pr, hm))) : {_ == ES.recover_q(one, CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.mneg(FS.order(one), FS.value(one, z)), FS.minv(FS.order(one), FS.value(one, r))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, s), FS.minv(FS.order(one), FS.value(one, r))), PT.pv(one, pr)))) : Maybe<&2, List<&2, U32>>} 69 %Equal.sym(CV.SPoint, PT.pv(one, P.add(P.mul(S.mul(S.neg(z), S.inv(r)), P.g()), P.mul(S.mul(s, S.inv(r)), pr))), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(S.neg(z), S.inv(r))), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(s, S.inv(r))), PT.pv(one, pr))), TW.two_v(one, h1, S.mul(S.neg(z), S.inv(r)), hu1, S.mul(s, S.inv(r)), hu2, pr, hm)) : {ES.recover_q(one, _) == ES.recover_q(one, CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.mneg(FS.order(one), FS.value(one, z)), FS.minv(FS.order(one), FS.value(one, r))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, s), FS.minv(FS.order(one), FS.value(one, r))), PT.pv(one, pr)))) : Maybe<&2, List<&2, U32>>} 70 %Equal.sym(Nat, FS.value(one, S.mul(S.neg(z), S.inv(r))), FS.mmul(FS.order(one), FS.value(one, S.neg(z)), FS.value(one, S.inv(r))), SO.mul_v(one, h1, S.neg(z), S.inv(r), hn, hi)) : {ES.recover_q(one, CV.padd(FS.prime(one), CV.pmul(FS.prime(one), _, CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(s, S.inv(r))), PT.pv(one, pr)))) == ES.recover_q(one, CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.mneg(FS.order(one), FS.value(one, z)), FS.minv(FS.order(one), FS.value(one, r))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, s), FS.minv(FS.order(one), FS.value(one, r))), PT.pv(one, pr)))) : Maybe<&2, List<&2, U32>>} 71 %Equal.sym(Nat, FS.value(one, S.mul(s, S.inv(r))), FS.mmul(FS.order(one), FS.value(one, s), FS.value(one, S.inv(r))), SO.mul_v(one, h1, s, S.inv(r), hs, hi)) : {ES.recover_q(one, CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, S.neg(z)), FS.value(one, S.inv(r))), CV.g(one)), CV.pmul(FS.prime(one), _, PT.pv(one, pr)))) == ES.recover_q(one, CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.mneg(FS.order(one), FS.value(one, z)), FS.minv(FS.order(one), FS.value(one, r))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, s), FS.minv(FS.order(one), FS.value(one, r))), PT.pv(one, pr)))) : Maybe<&2, List<&2, U32>>} 72 %Equal.sym(Nat, FS.value(one, S.neg(z)), FS.mneg(FS.order(one), FS.value(one, z)), SO.neg_v(one, h1, z, hz)) : {ES.recover_q(one, CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), _, FS.value(one, S.inv(r))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, s), FS.value(one, S.inv(r))), PT.pv(one, pr)))) == ES.recover_q(one, CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.mneg(FS.order(one), FS.value(one, z)), FS.minv(FS.order(one), FS.value(one, r))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, s), FS.minv(FS.order(one), FS.value(one, r))), PT.pv(one, pr)))) : Maybe<&2, List<&2, U32>>} 73 %Equal.sym(Nat, FS.value(one, S.inv(r)), FS.minv(FS.order(one), FS.value(one, r)), SP.inv_v(one, h1, r, hr)) : {ES.recover_q(one, CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.mneg(FS.order(one), FS.value(one, z)), _), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, s), FS.value(one, S.inv(r))), PT.pv(one, pr)))) == ES.recover_q(one, CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.mneg(FS.order(one), FS.value(one, z)), FS.minv(FS.order(one), FS.value(one, r))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, s), FS.minv(FS.order(one), FS.value(one, r))), PT.pv(one, pr)))) : Maybe<&2, List<&2, U32>>} 74 %Equal.sym(Nat, FS.value(one, S.inv(r)), FS.minv(FS.order(one), FS.value(one, r)), SP.inv_v(one, h1, r, hr)) : {ES.recover_q(one, CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.mneg(FS.order(one), FS.value(one, z)), FS.minv(FS.order(one), FS.value(one, r))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, s), _), PT.pv(one, pr)))) == ES.recover_q(one, CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.mneg(FS.order(one), FS.value(one, z)), FS.minv(FS.order(one), FS.value(one, r))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, s), FS.minv(FS.order(one), FS.value(one, r))), PT.pv(one, pr)))) : Maybe<&2, List<&2, U32>>} 75 {==} 76 77 # ---- the point R of x-coordinate x ---- 78 79 def rxg(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}, +id: Nat, +x: List<&2, Nat>, +hx: {PT.red(one, x) == True{} : Bool}, +xv: Nat, +hxv: {FS.value(one, x) == Nat.mod(xv, 1n+K.pp(one)) : Nat}, c: Bool, +hc: {Nat.is_lt(xv, 1n+K.pp(one)) == c : Bool}) -> {E.recover_x(z, r, s, id, x, c) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), id, xv, c) : Maybe<&2, List<&2, U32>>}: 80 match c: 81 case True{}: 82 +e = Equal.trans(Nat, FS.value(one, x), Nat.mod(xv, 1n+K.pp(one)), xv, hxv, RC.mod_small(K.pp(one), xv, hc)) 83 %Equal.sym(Nat, xv, FS.value(one, x), Equal.sym(Nat, FS.value(one, x), xv, e)) : {E.recover_r(z, r, s, P.decompress(x, Nat.mod(id, 2n))) == ES.recover_r(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), CV.decompress(FS.prime(one), _, Nat.mod(id, 2n))) : Maybe<&2, List<&2, U32>>} 84 %Equal.sym(Maybe<&2, CV.SPoint>, CV.decompress(FS.prime(one), FS.value(one, x), Nat.mod(id, 2n)), PE.mpv(one, P.decompress(x, Nat.mod(id, 2n))), Equal.sym(Maybe<&2, CV.SPoint>, PE.mpv(one, P.decompress(x, Nat.mod(id, 2n))), CV.decompress(FS.prime(one), FS.value(one, x), Nat.mod(id, 2n)), PE.decompress_v(one, h1, x, Nat.mod(id, 2n), hx, PE.mod2_lt(id)))) : {E.recover_r(z, r, s, P.decompress(x, Nat.mod(id, 2n))) == ES.recover_r(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), _) : Maybe<&2, List<&2, U32>>} 85 rr(one, h1, z, hz, r, hr, s, hs, P.decompress(x, Nat.mod(id, 2n)), PE.decompress_r(one, h1, x, Nat.mod(id, 2n), hx, PE.mod2_lt(id))) 86 case False{}: 87 {==} 88 89 # r < n < p 90 def r_lt_n(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}) -> {Nat.is_lt(FS.value(one, r), 1n+K.np(one)) == True{} : Bool}: 91 I.lt_subst_r(FS.value(one, r), FS.order(one), 1n+K.np(one), K.order_eq(one, h1), Lg.and_right(FS.limbs16(one, 16n, r), Nat.is_lt(FS.value(one, r), FS.order(one)), hr)) 92 93 def r_lt_pp(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}) -> {Nat.is_lt(FS.value(one, r), 1n+K.pp(one)) == True{} : Bool}: 94 N.lt_trans(FS.value(one, r), 1n+K.np(one), 1n+K.pp(one), r_lt_n(one, h1, r, hr), RC.n_lt_p(one, h1)) 95 96 def to_p(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +h: {Nat.is_lt(x, 1n+K.pp(one)) == True{} : Bool}) -> {Nat.is_lt(x, FS.prime(one)) == True{} : Bool}: 97 I.lt_subst_r(x, 1n+K.pp(one), FS.prime(one), Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)), h) 98 99 def rp_red(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}) -> {PT.red(one, r) == True{} : Bool}: 100 Lg.and_intro(FS.limbs16(one, 16n, r), Nat.is_lt(FS.value(one, r), FS.prime(one)), SL.sl16(one, r, hr), to_p(one, h1, FS.value(one, r), r_lt_pp(one, h1, r, hr))) 101 102 def cn_red(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.red(one, E.cn_fe()) == True{} : Bool}: 103 +h = I.lt_subst_l(FS.cn(one), FS.value(one, E.cn_fe()), 1n+K.pp(one), Equal.sym(Nat, FS.value(one, E.cn_fe()), FS.cn(one), RC.cn_fe_v(one)), RC.cn_lt_p(one, h1)) 104 Lg.and_intro(FS.limbs16(one, 16n, E.cn_fe()), Nat.is_lt(FS.value(one, E.cn_fe()), FS.prime(one)), RC.cn_fe_l(one, h1), to_p(one, h1, FS.value(one, E.cn_fe()), h)) 105 106 def cp_red(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.red(one, E.cp_fe()) == True{} : Bool}: 107 +h = I.lt_subst_l(FS.cp(one), FS.value(one, E.cp_fe()), 1n+K.pp(one), Equal.sym(Nat, FS.value(one, E.cp_fe()), FS.cp(one), RC.cp_fe_v(one)), RC.cp_lt_p(one, h1)) 108 Lg.and_intro(FS.limbs16(one, 16n, E.cp_fe()), Nat.is_lt(FS.value(one, E.cp_fe()), FS.prime(one)), RC.cp_fe_l(one, h1), to_p(one, h1, FS.value(one, E.cp_fe()), h)) 109 110 # x1 = (r - c_n + c_p) mod p = (r + n) mod p 111 def x1_r(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}) -> {PT.red(one, E.rn_fe(r)) == True{} : Bool}: 112 FO.add_r(one, h1, F.sub(r, E.cn_fe()), E.cp_fe(), FO.sub_r(one, h1, r, E.cn_fe(), rp_red(one, h1, r, hr), cn_red(one, h1)), cp_red(one, h1)) 113 114 def x1_v(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}) -> {FS.value(one, E.rn_fe(r)) == Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)) : Nat}: 115 +hs = FO.sub_r(one, h1, r, E.cn_fe(), rp_red(one, h1, r, hr), cn_red(one, h1)) 116 %Equal.sym(Nat, FS.value(one, F.add(F.sub(r, E.cn_fe()), E.cp_fe())), FS.madd(FS.prime(one), FS.value(one, F.sub(r, E.cn_fe())), FS.value(one, E.cp_fe())), FO.add_v(one, h1, F.sub(r, E.cn_fe()), E.cp_fe(), hs, cp_red(one, h1))) : {_ == Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)) : Nat} 117 %Equal.sym(Nat, FS.value(one, F.sub(r, E.cn_fe())), FS.msub(FS.prime(one), FS.value(one, r), FS.value(one, E.cn_fe())), FO.sub_v(one, h1, r, E.cn_fe(), rp_red(one, h1, r, hr), cn_red(one, h1))) : {FS.madd(FS.prime(one), _, FS.value(one, E.cp_fe())) == Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)) : Nat} 118 %Equal.sym(Nat, FS.value(one, E.cn_fe()), FS.cn(one), RC.cn_fe_v(one)) : {FS.madd(FS.prime(one), FS.msub(FS.prime(one), FS.value(one, r), _), FS.value(one, E.cp_fe())) == Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)) : Nat} 119 %Equal.sym(Nat, FS.value(one, E.cp_fe()), FS.cp(one), RC.cp_fe_v(one)) : {FS.madd(FS.prime(one), FS.msub(FS.prime(one), FS.value(one, r), FS.cn(one)), _) == Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)) : Nat} 120 %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {FS.madd(_, FS.msub(FS.prime(one), FS.value(one, r), FS.cn(one)), FS.cp(one)) == Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)) : Nat} 121 %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {FS.madd(1n+K.pp(one), FS.msub(_, FS.value(one, r), FS.cn(one)), FS.cp(one)) == Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)) : Nat} 122 RC.rn_val(FS.value(one, r), 1n+K.np(one), K.pp(one), FS.cn(one), FS.cp(one), RC.pn_sum(one, h1), RC.cn_lt_p(one, h1)) 123 124 def lt4(c: Nat) -> {Nat.is_lt(4n+c, 4n) == False{} : Bool}: 125 match c: 126 case 0n: 127 {==} 128 case 1n+d: 129 {==} 130 131 def not4(+c: Nat, +h: {Nat.is_lt(4n+c, 4n) == True{} : Bool}) -> Empty: 132 Lg.false_true(Equal.trans(Bool, False{}, Nat.is_lt(4n+c, 4n), True{}, Equal.sym(Bool, Nat.is_lt(4n+c, 4n), False{}, lt4(c)), h)) 133 134 def rfl_b(+b: Bool) -> {b == b : Bool}: 135 {==} 136 137 def zmul(+x: Nat) -> {Nat.mul(0n, x) == 0n : Nat}: 138 {==} 139 140 def rc0(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}) -> {E.recover_ok(z, r, s, 0n, True{}) == ES.recover_ok(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, True{}) : Maybe<&2, List<&2, U32>>}: 141 %Equal.sym(List<&2, Nat>, L.select(0n, E.rn_fe(r), r), r, SL.sel0(one, 16n, E.rn_fe(r), r, SL.l16(one, E.rn_fe(r), x1_r(one, h1, r, hr)), SL.sl16(one, r, hr))) : {E.recover_x(z, r, s, 0n, _, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, Nat.add(FS.value(one, r), Nat.mul(0n, FS.order(one))), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(0n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 142 %Equal.sym(Nat, Nat.mul(0n, FS.order(one)), 0n, zmul(FS.order(one))) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, Nat.add(FS.value(one, r), _), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(0n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 143 %Equal.sym(Nat, Nat.mul(0n, FS.order(one)), 0n, zmul(FS.order(one))) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, Nat.add(FS.value(one, r), 0n), Nat.is_lt(Nat.add(FS.value(one, r), _), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 144 %Equal.sym(Nat, Nat.add(FS.value(one, r), 0n), FS.value(one, r), N.add_zero(FS.value(one, r))) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, _, Nat.is_lt(Nat.add(FS.value(one, r), 0n), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 145 %Equal.sym(Nat, Nat.add(FS.value(one, r), 0n), FS.value(one, r), N.add_zero(FS.value(one, r))) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, FS.value(one, r), Nat.is_lt(_, FS.prime(one))) : Maybe<&2, List<&2, U32>>} 146 %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, FS.value(one, r), Nat.is_lt(FS.value(one, r), _)) : Maybe<&2, List<&2, U32>>} 147 %Equal.sym(Bool, Nat.is_lt(FS.value(one, r), 1n+K.pp(one)), True{}, r_lt_pp(one, h1, r, hr)) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, FS.value(one, r), _) : Maybe<&2, List<&2, U32>>} 148 rxg(one, h1, z, hz, r, hr, s, hs, 0n, r, rp_red(one, h1, r, hr), FS.value(one, r), Equal.sym(Nat, Nat.mod(FS.value(one, r), 1n+K.pp(one)), FS.value(one, r), RC.mod_small(K.pp(one), FS.value(one, r), r_lt_pp(one, h1, r, hr))), True{}, r_lt_pp(one, h1, r, hr)) 149 150 def rc1(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}) -> {E.recover_ok(z, r, s, 1n, True{}) == ES.recover_ok(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 1n, True{}) : Maybe<&2, List<&2, U32>>}: 151 %Equal.sym(List<&2, Nat>, L.select(0n, E.rn_fe(r), r), r, SL.sel0(one, 16n, E.rn_fe(r), r, SL.l16(one, E.rn_fe(r), x1_r(one, h1, r, hr)), SL.sl16(one, r, hr))) : {E.recover_x(z, r, s, 1n, _, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 1n, Nat.add(FS.value(one, r), Nat.mul(0n, FS.order(one))), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(0n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 152 %Equal.sym(Nat, Nat.mul(0n, FS.order(one)), 0n, zmul(FS.order(one))) : {E.recover_x(z, r, s, 1n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 1n, Nat.add(FS.value(one, r), _), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(0n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 153 %Equal.sym(Nat, Nat.mul(0n, FS.order(one)), 0n, zmul(FS.order(one))) : {E.recover_x(z, r, s, 1n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 1n, Nat.add(FS.value(one, r), 0n), Nat.is_lt(Nat.add(FS.value(one, r), _), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 154 %Equal.sym(Nat, Nat.add(FS.value(one, r), 0n), FS.value(one, r), N.add_zero(FS.value(one, r))) : {E.recover_x(z, r, s, 1n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 1n, _, Nat.is_lt(Nat.add(FS.value(one, r), 0n), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 155 %Equal.sym(Nat, Nat.add(FS.value(one, r), 0n), FS.value(one, r), N.add_zero(FS.value(one, r))) : {E.recover_x(z, r, s, 1n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 1n, FS.value(one, r), Nat.is_lt(_, FS.prime(one))) : Maybe<&2, List<&2, U32>>} 156 %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {E.recover_x(z, r, s, 1n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 1n, FS.value(one, r), Nat.is_lt(FS.value(one, r), _)) : Maybe<&2, List<&2, U32>>} 157 %Equal.sym(Bool, Nat.is_lt(FS.value(one, r), 1n+K.pp(one)), True{}, r_lt_pp(one, h1, r, hr)) : {E.recover_x(z, r, s, 1n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 1n, FS.value(one, r), _) : Maybe<&2, List<&2, U32>>} 158 rxg(one, h1, z, hz, r, hr, s, hs, 1n, r, rp_red(one, h1, r, hr), FS.value(one, r), Equal.sym(Nat, Nat.mod(FS.value(one, r), 1n+K.pp(one)), FS.value(one, r), RC.mod_small(K.pp(one), FS.value(one, r), r_lt_pp(one, h1, r, hr))), True{}, r_lt_pp(one, h1, r, hr)) 159 160 def rc2(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}) -> {E.recover_ok(z, r, s, 2n, True{}) == ES.recover_ok(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 2n, True{}) : Maybe<&2, List<&2, U32>>}: 161 %Equal.sym(List<&2, Nat>, L.select(1n, E.rn_fe(r), r), E.rn_fe(r), SL.sel1(one, 16n, E.rn_fe(r), r, SL.l16(one, E.rn_fe(r), x1_r(one, h1, r, hr)), SL.sl16(one, r, hr))) : {E.recover_x(z, r, s, 2n, _, Bool.not(S.lt_n(E.rn_fe(r)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 2n, Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 162 %Equal.sym(Bool, S.lt_n(E.rn_fe(r)), Nat.is_lt(FS.value(one, E.rn_fe(r)), FS.order(one)), FW.lt_n_s(one, h1, E.rn_fe(r))) : {E.recover_x(z, r, s, 2n, E.rn_fe(r), Bool.not(_)) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 2n, Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 163 %Equal.sym(Nat, FS.value(one, E.rn_fe(r)), Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), x1_v(one, h1, r, hr)) : {E.recover_x(z, r, s, 2n, E.rn_fe(r), Bool.not(Nat.is_lt(_, FS.order(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 2n, Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 164 %Equal.sym(Nat, Nat.mul(1n, FS.order(one)), FS.order(one), RC.m1(FS.order(one))) : {E.recover_x(z, r, s, 2n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), FS.order(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 2n, Nat.add(FS.value(one, r), _), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 165 %Equal.sym(Nat, Nat.mul(1n, FS.order(one)), FS.order(one), RC.m1(FS.order(one))) : {E.recover_x(z, r, s, 2n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), FS.order(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 2n, Nat.add(FS.value(one, r), FS.order(one)), Nat.is_lt(Nat.add(FS.value(one, r), _), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 166 %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {E.recover_x(z, r, s, 2n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), _))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 2n, Nat.add(FS.value(one, r), FS.order(one)), Nat.is_lt(Nat.add(FS.value(one, r), FS.order(one)), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 167 %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {E.recover_x(z, r, s, 2n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), 1n+K.np(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 2n, Nat.add(FS.value(one, r), _), Nat.is_lt(Nat.add(FS.value(one, r), FS.order(one)), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 168 %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {E.recover_x(z, r, s, 2n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), 1n+K.np(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 2n, Nat.add(FS.value(one, r), 1n+K.np(one)), Nat.is_lt(Nat.add(FS.value(one, r), _), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 169 %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {E.recover_x(z, r, s, 2n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), 1n+K.np(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 2n, Nat.add(FS.value(one, r), 1n+K.np(one)), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), _)) : Maybe<&2, List<&2, U32>>} 170 %Equal.sym(Bool, Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), 1n+K.np(one))), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), RC.rn_cond(FS.value(one, r), 1n+K.np(one), K.pp(one), r_lt_n(one, h1, r, hr), RC.n_lt_p(one, h1), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), rfl_b(Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one))))) : {E.recover_x(z, r, s, 2n, E.rn_fe(r), _) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 2n, Nat.add(FS.value(one, r), 1n+K.np(one)), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one))) : Maybe<&2, List<&2, U32>>} 171 rxg(one, h1, z, hz, r, hr, s, hs, 2n, E.rn_fe(r), x1_r(one, h1, r, hr), Nat.add(FS.value(one, r), 1n+K.np(one)), x1_v(one, h1, r, hr), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), {==}) 172 173 def rc3(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}) -> {E.recover_ok(z, r, s, 3n, True{}) == ES.recover_ok(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, True{}) : Maybe<&2, List<&2, U32>>}: 174 %Equal.sym(List<&2, Nat>, L.select(1n, E.rn_fe(r), r), E.rn_fe(r), SL.sel1(one, 16n, E.rn_fe(r), r, SL.l16(one, E.rn_fe(r), x1_r(one, h1, r, hr)), SL.sl16(one, r, hr))) : {E.recover_x(z, r, s, 3n, _, Bool.not(S.lt_n(E.rn_fe(r)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 175 %Equal.sym(Bool, S.lt_n(E.rn_fe(r)), Nat.is_lt(FS.value(one, E.rn_fe(r)), FS.order(one)), FW.lt_n_s(one, h1, E.rn_fe(r))) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(_)) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 176 %Equal.sym(Nat, FS.value(one, E.rn_fe(r)), Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), x1_v(one, h1, r, hr)) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(_, FS.order(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 177 %Equal.sym(Nat, Nat.mul(1n, FS.order(one)), FS.order(one), RC.m1(FS.order(one))) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), FS.order(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), _), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(1n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 178 %Equal.sym(Nat, Nat.mul(1n, FS.order(one)), FS.order(one), RC.m1(FS.order(one))) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), FS.order(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), FS.order(one)), Nat.is_lt(Nat.add(FS.value(one, r), _), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 179 %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), _))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), FS.order(one)), Nat.is_lt(Nat.add(FS.value(one, r), FS.order(one)), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 180 %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), 1n+K.np(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), _), Nat.is_lt(Nat.add(FS.value(one, r), FS.order(one)), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 181 %Equal.sym(Nat, FS.order(one), 1n+K.np(one), K.order_eq(one, h1)) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), 1n+K.np(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), 1n+K.np(one)), Nat.is_lt(Nat.add(FS.value(one, r), _), FS.prime(one))) : Maybe<&2, List<&2, U32>>} 182 %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), 1n+K.np(one)))) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), 1n+K.np(one)), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), _)) : Maybe<&2, List<&2, U32>>} 183 %Equal.sym(Bool, Bool.not(Nat.is_lt(Nat.mod(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), 1n+K.np(one))), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), RC.rn_cond(FS.value(one, r), 1n+K.np(one), K.pp(one), r_lt_n(one, h1, r, hr), RC.n_lt_p(one, h1), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), rfl_b(Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one))))) : {E.recover_x(z, r, s, 3n, E.rn_fe(r), _) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 3n, Nat.add(FS.value(one, r), 1n+K.np(one)), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one))) : Maybe<&2, List<&2, U32>>} 184 rxg(one, h1, z, hz, r, hr, s, hs, 3n, E.rn_fe(r), x1_r(one, h1, r, hr), Nat.add(FS.value(one, r), 1n+K.np(one)), x1_v(one, h1, r, hr), Nat.is_lt(Nat.add(FS.value(one, r), 1n+K.np(one)), 1n+K.pp(one)), {==}) 185 186 def rid(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}, id: Nat, +hid: {Nat.is_lt(id, 4n) == True{} : Bool}) -> {E.recover_ok(z, r, s, id, True{}) == ES.recover_ok(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), id, True{}) : Maybe<&2, List<&2, U32>>}: 187 match id: 188 case 0n: 189 rc0(one, h1, z, hz, r, hr, s, hs) 190 case 1n: 191 rc1(one, h1, z, hz, r, hr, s, hs) 192 case 2n: 193 rc2(one, h1, z, hz, r, hr, s, hs) 194 case 3n: 195 rc3(one, h1, z, hz, r, hr, s, hs) 196 case 4n+ +c: 197 Empty.absurd({E.recover_ok(z, r, s, 4n+c, True{}) == ES.recover_ok(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 4n+c, True{}) : Maybe<&2, List<&2, U32>>}, not4(c, hid)) 198 199 def rok(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hlr: {FS.limbs16(one, 16n, r) == True{} : Bool}, +s: List<&2, Nat>, +hls: {FS.limbs16(one, 16n, s) == True{} : Bool}, +id: Nat, a: Bool, b: Bool, c: Bool, +ha: {ES.scalar_ok(one, FS.value(one, r)) == a : Bool}, +hb: {ES.scalar_ok(one, FS.value(one, s)) == b : Bool}, +hc: {Nat.is_lt(id, 4n) == c : Bool}) -> {E.recover_ok(z, r, s, id, Bool.and(Bool.and(a, b), c)) == ES.recover_ok(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), id, Bool.and(Bool.and(a, b), c)) : Maybe<&2, List<&2, U32>>}: 200 match a b c: 201 case True{} True{} True{}: 202 rid(one, h1, z, hz, r, PV.ok_red(one, r, hlr, ha), s, PV.ok_red(one, s, hls, hb), id, hc) 203 case True{} True{} False{}: 204 {==} 205 case True{} False{} _: 206 {==} 207 case False{} _ _: 208 {==} 209 210 def rsig(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {B.has_len(32n, h) == True{} : Bool}, +sig: List<&2, U32>, +hsig: {B.has_len(65n, sig) == True{} : Bool}) -> {E.recover_sig(h, sig) == ES.recover_len(one, h, sig, True{}) : Maybe<&2, List<&2, U32>>}: 211 +hlr = BY.of_be_limbs(one, h1, B.prefix(32n, sig), pl1(sig, hsig)) 212 +hls = BY.of_be_limbs(one, h1, B.prefix(32n, B.suffix(32n, sig)), pl2(sig, hsig)) 213 %Equal.sym(Bool, E.scalar_ok(B.of_be(B.prefix(32n, sig))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), SQ.scalar_ok_v(one, h1, B.of_be(B.prefix(32n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(_, E.scalar_ok(B.of_be(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, ES.hash_scalar(one, h), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.first(32n, CV.after(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, CV.after(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 214 %Equal.sym(Bool, E.scalar_ok(B.of_be(B.prefix(32n, B.suffix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig))))), SQ.scalar_ok_v(one, h1, B.of_be(B.prefix(32n, B.suffix(32n, sig))))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), _), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, ES.hash_scalar(one, h), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.first(32n, CV.after(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, CV.after(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 215 %Equal.sym(Nat, ES.hash_scalar(one, h), FS.value(one, E.hash_scalar(h)), Equal.sym(Nat, FS.value(one, E.hash_scalar(h)), ES.hash_scalar(one, h), SQ.hash_v(one, h1, h, hh))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, _, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.first(32n, CV.after(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, CV.after(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 216 %Equal.sym(List<&2, U32>, CV.after(32n, sig), B.suffix(32n, sig), Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.first(32n, _)), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, CV.after(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 217 %Equal.sym(List<&2, U32>, CV.after(32n, sig), B.suffix(32n, sig), Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.first(32n, B.suffix(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, _)))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 218 %Equal.sym(List<&2, U32>, CV.first(32n, sig), B.prefix(32n, sig), Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(_), CV.os2ip(CV.first(32n, B.suffix(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 219 %Equal.sym(List<&2, U32>, CV.first(32n, sig), B.prefix(32n, sig), Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(CV.first(32n, B.suffix(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(_)), ES.scalar_ok(one, CV.os2ip(CV.first(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 220 %Equal.sym(List<&2, U32>, CV.first(32n, B.suffix(32n, sig)), B.prefix(32n, B.suffix(32n, sig)), Equal.sym(List<&2, U32>, B.prefix(32n, B.suffix(32n, sig)), CV.first(32n, B.suffix(32n, sig)), BL.prefix_first(32n, B.suffix(32n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(_), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.first(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 221 %Equal.sym(List<&2, U32>, CV.first(32n, B.suffix(32n, sig)), B.prefix(32n, B.suffix(32n, sig)), Equal.sym(List<&2, U32>, B.prefix(32n, B.suffix(32n, sig)), CV.first(32n, B.suffix(32n, sig)), BL.prefix_first(32n, B.suffix(32n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(CV.head(CV.after(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(_))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 222 %Equal.sym(List<&2, U32>, CV.after(64n, sig), B.suffix(64n, sig), Equal.sym(List<&2, U32>, B.suffix(64n, sig), CV.after(64n, sig), BL.suffix_after(64n, sig))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(CV.head(_)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(CV.after(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 223 %Equal.sym(List<&2, U32>, CV.after(64n, sig), B.suffix(64n, sig), Equal.sym(List<&2, U32>, B.suffix(64n, sig), CV.after(64n, sig), BL.suffix_after(64n, sig))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(CV.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(_)), 4n))) : Maybe<&2, List<&2, U32>>} 224 %Equal.sym(U32, CV.head(B.suffix(64n, sig)), B.head(B.suffix(64n, sig)), Equal.sym(U32, B.head(B.suffix(64n, sig)), CV.head(B.suffix(64n, sig)), BL.head_eq(B.suffix(64n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(_), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(CV.head(B.suffix(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 225 %Equal.sym(U32, CV.head(B.suffix(64n, sig)), B.head(B.suffix(64n, sig)), Equal.sym(U32, B.head(B.suffix(64n, sig)), CV.head(B.suffix(64n, sig)), BL.head_eq(B.suffix(64n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(_), 4n))) : Maybe<&2, List<&2, U32>>} 226 %Equal.sym(Nat, CV.os2ip(B.prefix(32n, sig)), FS.value(one, B.of_be(B.prefix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, sig))), CV.os2ip(B.prefix(32n, sig)), BY.of_be_value(one, h1, B.prefix(32n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), _, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 227 %Equal.sym(Nat, CV.os2ip(B.prefix(32n, sig)), FS.value(one, B.of_be(B.prefix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, sig))), CV.os2ip(B.prefix(32n, sig)), BY.of_be_value(one, h1, B.prefix(32n, sig)))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, _), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 228 %Equal.sym(Nat, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), BY.of_be_value(one, h1, B.prefix(32n, B.suffix(32n, sig))))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), _, U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 229 %Equal.sym(Nat, CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))), CV.os2ip(B.prefix(32n, B.suffix(32n, sig))), BY.of_be_value(one, h1, B.prefix(32n, B.suffix(32n, sig))))) : {E.recover_ok(E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.prefix(32n, B.suffix(32n, sig))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) == ES.recover_ok(one, FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig)))), U32.to_nat(B.head(B.suffix(64n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, _)), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n))) : Maybe<&2, List<&2, U32>>} 230 rok(one, h1, E.hash_scalar(h), SQ.hash_r(one, h1, h, hh), B.of_be(B.prefix(32n, sig)), hlr, B.of_be(B.prefix(32n, B.suffix(32n, sig))), hls, U32.to_nat(B.head(B.suffix(64n, sig))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, B.suffix(32n, sig))))), Nat.is_lt(U32.to_nat(B.head(B.suffix(64n, sig))), 4n), {==}, {==}, {==}) 231 232 def rlen(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +sig: List<&2, U32>, a: Bool, b: Bool, +ha: {B.has_len(32n, h) == a : Bool}, +hb: {B.has_len(65n, sig) == b : Bool}) -> {E.recover_len(h, sig, Bool.and(a, b)) == ES.recover_len(one, h, sig, Bool.and(a, b)) : Maybe<&2, List<&2, U32>>}: 233 match a b: 234 case True{} True{}: 235 rsig(one, h1, h, ha, sig, hb) 236 case True{} False{}: 237 {==} 238 case False{} _: 239 {==} 240 241 # the key recovered from a 32-byte hash and a 65-byte r || s || id 242 def recover_v(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +sig: List<&2, U32>) -> {E.recover(h, sig) == ES.recover(one, h, sig) : Maybe<&2, List<&2, U32>>}: 243 %Equal.sym(Bool, B.has_len(32n, h), CV.length_is(32n, h), BL.hl_is(32n, h)) : {E.recover_len(h, sig, Bool.and(_, B.has_len(65n, sig))) == ES.recover_len(one, h, sig, Bool.and(CV.length_is(32n, h), CV.length_is(65n, sig))) : Maybe<&2, List<&2, U32>>} 244 %Equal.sym(Bool, B.has_len(65n, sig), CV.length_is(65n, sig), BL.hl_is(65n, sig)) : {E.recover_len(h, sig, Bool.and(CV.length_is(32n, h), _)) == ES.recover_len(one, h, sig, Bool.and(CV.length_is(32n, h), CV.length_is(65n, sig))) : Maybe<&2, List<&2, U32>>} 245 rlen(one, h1, h, sig, CV.length_is(32n, h), CV.length_is(65n, sig), BL.hl_is(32n, h), BL.hl_is(65n, sig))