proofs/crypto/secp256k1/prec.bend source
proofs/crypto/secp256k1/prec.bend on the hub · documented module
# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/prec.src; edit the .srcimport Baseimport ../../../spec/crypto/secp256k1/field.bend as FSimport ../../../spec/crypto/secp256k1/curve.bend as CVimport ../../../spec/crypto/secp256k1/ecdsa.bend as ESimport ../../../src/crypto/secp256k1/limbs.bend as Limport ../../../src/crypto/secp256k1/field.bend as Fimport ../../../src/crypto/secp256k1/scalar.bend as Simport ../../../src/crypto/secp256k1/bytes.bend as Bimport ../../../src/crypto/secp256k1/point.bend as Pimport ../../../src/crypto/secp256k1/ecdsa.bend as Eimport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Lgimport ./consts.bend as Kimport ./ineq.bend as Iimport ./fieldops.bend as FOimport ./scalarops.bend as SOimport ./scalarpow.bend as SPimport ./fwrap.bend as FWimport ./bytes.bend as BYimport ./point.bend as PTimport ./sel.bend as SLimport ./paff.bend as PAimport ./penc.bend as PEimport ./pver.bend as PVimport ./rconst.bend as RCimport ./blist.bend as BLimport ./pscal.bend as SQimport ./ptwo.bend as TW# ECDSA public key recovery of src/crypto/secp256k1/ecdsa.bend (recover)# against spec/crypto/secp256k1/ecdsa.bend.# ---- lengths of the fields of r || s || id ----def pl1(+sig: List<&2, U32>, +h: {B.has_len(65n, sig) == True{} : Bool}) -> {B.has_len(32n, B.prefix(32n, sig)) == True{} : Bool}: %Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig)) : {B.has_len(32n, _) == True{} : Bool} BL.pre_len(32n, 33n, sig, h)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}: %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} %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} BL.pre_len(32n, 1n, CV.after(32n, sig), BL.suf_len(32n, 33n, sig, h))# ---- Q, and its encoding ----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>>}: match b: case True{}: {==} case False{}: 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))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>>}: %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>>} rq_b(one, h1, q, hq, CV.is_inf(PT.pv(one, q)))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>>}: match m: case None{}: {==} case Some{+pr}: +hi = SP.inv_r(one, h1, r, hr) +hn = SO.neg_r(one, h1, z, hz) +hu1 = SO.mul_r(one, h1, S.neg(z), S.inv(r), hn, hi) +hu2 = SO.mul_r(one, h1, s, S.inv(r), hs, hi) +q = P.add(P.mul(S.mul(S.neg(z), S.inv(r)), P.g()), P.mul(S.mul(s, S.inv(r)), pr)) %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} {==}# ---- the point R of x-coordinate x ----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>>}: match c: case True{}: +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)) %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>>} %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>>} 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))) case False{}: {==}# r < n < pdef 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}: 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))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}: 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))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}: 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)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}: 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)))def cn_red(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.red(one, E.cn_fe()) == True{} : Bool}: +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)) 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))def cp_red(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.red(one, E.cp_fe()) == True{} : Bool}: +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)) 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))# x1 = (r - c_n + c_p) mod p = (r + n) mod pdef 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}: 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))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}: +hs = FO.sub_r(one, h1, r, E.cn_fe(), rp_red(one, h1, r, hr), cn_red(one, h1)) %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} %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} %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} %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} %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} %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} 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))def lt4(c: Nat) -> {Nat.is_lt(4n+c, 4n) == False{} : Bool}: match c: case 0n: {==} case 1n+d: {==}def not4(+c: Nat, +h: {Nat.is_lt(4n+c, 4n) == True{} : Bool}) -> Empty: 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))def rfl_b(+b: Bool) -> {b == b : Bool}: {==}def zmul(+x: Nat) -> {Nat.mul(0n, x) == 0n : Nat}: {==}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>>}: %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} 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))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>>}: %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} 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))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>>}: %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} 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)), {==})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>>}: %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} 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)), {==})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>>}: match id: case 0n: rc0(one, h1, z, hz, r, hr, s, hs) case 1n: rc1(one, h1, z, hz, r, hr, s, hs) case 2n: rc2(one, h1, z, hz, r, hr, s, hs) case 3n: rc3(one, h1, z, hz, r, hr, s, hs) case 4n+ +c: 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))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>>}: match a b c: case True{} True{} True{}: rid(one, h1, z, hz, r, PV.ok_red(one, r, hlr, ha), s, PV.ok_red(one, s, hls, hb), id, hc) case True{} True{} False{}: {==} case True{} False{} _: {==} case False{} _ _: {==}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>>}: +hlr = BY.of_be_limbs(one, h1, B.prefix(32n, sig), pl1(sig, hsig)) +hls = BY.of_be_limbs(one, h1, B.prefix(32n, B.suffix(32n, sig)), pl2(sig, hsig)) %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} %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>>} 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), {==}, {==}, {==})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>>}: match a b: case True{} True{}: rsig(one, h1, h, ha, sig, hb) case True{} False{}: {==} case False{} _: {==}# the key recovered from a 32-byte hash and a 65-byte r || s || iddef 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>>}: %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>>} %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>>} 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))