proofs/crypto/secp256k1/prec.bend
bend-collections-laws-crypto@1.0.0.0 · 245 lines · 27 definitions
1
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend as F
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as S
9import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
10import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
11import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E
12import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
13import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend as K
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldops.bend as FO
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend as SO
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarpow.bend as SP
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as FW
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT
22import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as SL
23import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA
24import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as PE
25import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend as PV
26import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend as RC
27import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL
28import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend as SQ
29import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ptwo.bend as TW
30
31
32
33
34
35
36def 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
40def 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
46
47def 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
54def 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
58def 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
78
79def 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
90def 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
93def 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
96def 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
99def 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
102def 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
106def 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
111def 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
114def 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
124def lt4(c: Nat) -> {Nat.is_lt(4n+c, 4n) == False{} : Bool}:
125 match c:
126 case 0n:
127 {==}
128 case 1n+d:
129 {==}
130
131def 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
134def rfl_b(+b: Bool) -> {b == b : Bool}:
135 {==}
136
137def zmul(+x: Nat) -> {Nat.mul(0n, x) == 0n : Nat}:
138 {==}
139
140def 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
150def 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
160def 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
173def 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
186def 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
199def 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
210def 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
232def 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
242def 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))