~/jendhub

proofs/crypto/secp256k1/pecr.bend

bend-collections-laws-crypto@1.0.0.0 · 69 lines · 6 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pecr.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend as PR
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/peth.bend as PET
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL
10
11# Ethereum's ECRECOVER precompile of src/crypto/secp256k1/ecdsa.bend against
12# spec/crypto/secp256k1/ecdsa.bend.
13
14
15def zeros_v(bs: List<&2, U32>) -> {E.zeros_ok(bs) == ES.all_zero(bs) : Bool}:
16  match bs:
17    case Nil{}:
18      {==}
19    case +b <> t:
20      Equal.cong(Bool, Bool, x => Bool.and(U32.is_eq(b, 0), x), E.zeros_ok(t), ES.all_zero(t), zeros_v(t))
21
22def ew_v(m: Maybe<&2, List<&2, U32>>) -> {E.eth_word(m) == ES.word_of(m) : Maybe<&2, List<&2, U32>>}:
23  match m:
24    case None{}:
25      {==}
26    case Some{a}:
27      {==}
28
29def aw_v(m: Maybe<&2, List<&2, U32>>) -> {E.addr_word(m) == ES.addr_word(m) : Maybe<&2, List<&2, U32>>}:
30  match m:
31    case None{}:
32      {==}
33    case Some{+pk}:
34      %Equal.sym(Maybe<&2, List<&2, U32>>, E.eth_address(pk), ES.eth_address(pk), PET.eth_address_v(pk)) : {E.eth_word(_) == ES.word_of(ES.eth_address(pk)) : Maybe<&2, List<&2, U32>>}
35      ew_v(ES.eth_address(pk))
36
37def ecv(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +rs: List<&2, U32>, +v: U32, ok: Bool) -> {E.ecrecover_v(h, rs, v, ok) == ES.ecrecover_v(one, h, rs, v, ok) : Maybe<&2, List<&2, U32>>}:
38  match ok:
39    case True{}:
40      %Equal.sym(Maybe<&2, List<&2, U32>>, E.recover(h, List.append(&2, U32, rs, [U32.sub(v, 27)])), ES.recover(one, h, List.append(&2, U32, rs, [U32.sub(v, 27)])), PR.recover_v(one, h1, h, List.append(&2, U32, rs, [U32.sub(v, 27)]))) : {E.addr_word(_) == ES.addr_word(ES.recover(one, h, List.append(&2, U32, rs, [U32.sub(v, 27)]))) : Maybe<&2, List<&2, U32>>}
41      aw_v(ES.recover(one, h, List.append(&2, U32, rs, [U32.sub(v, 27)])))
42    case False{}:
43      {==}
44
45def ecin(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, U32>) -> {E.ecrecover_in(x) == ES.ecrecover_in(one, x) : Maybe<&2, List<&2, U32>>}:
46  %Equal.sym(List<&2, U32>, B.suffix(32n, x), CV.after(32n, x), BL.suffix_after(32n, x)) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), B.head(B.suffix(31n, B.prefix(32n, _))), Bool.and(E.zeros_ok(B.prefix(31n, B.prefix(32n, B.suffix(32n, x)))), Bool.or(U32.is_eq(B.head(B.suffix(31n, B.prefix(32n, B.suffix(32n, x)))), 27), U32.is_eq(B.head(B.suffix(31n, B.prefix(32n, B.suffix(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
47  %Equal.sym(List<&2, U32>, B.suffix(32n, x), CV.after(32n, x), BL.suffix_after(32n, x)) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), B.head(B.suffix(31n, B.prefix(32n, CV.after(32n, x)))), Bool.and(E.zeros_ok(B.prefix(31n, B.prefix(32n, _))), Bool.or(U32.is_eq(B.head(B.suffix(31n, B.prefix(32n, B.suffix(32n, x)))), 27), U32.is_eq(B.head(B.suffix(31n, B.prefix(32n, B.suffix(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
48  %Equal.sym(List<&2, U32>, B.suffix(32n, x), CV.after(32n, x), BL.suffix_after(32n, x)) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), B.head(B.suffix(31n, B.prefix(32n, CV.after(32n, x)))), Bool.and(E.zeros_ok(B.prefix(31n, B.prefix(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(B.head(B.suffix(31n, B.prefix(32n, _))), 27), U32.is_eq(B.head(B.suffix(31n, B.prefix(32n, B.suffix(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
49  %Equal.sym(List<&2, U32>, B.suffix(32n, x), CV.after(32n, x), BL.suffix_after(32n, x)) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), B.head(B.suffix(31n, B.prefix(32n, CV.after(32n, x)))), Bool.and(E.zeros_ok(B.prefix(31n, B.prefix(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(B.head(B.suffix(31n, B.prefix(32n, CV.after(32n, x)))), 27), U32.is_eq(B.head(B.suffix(31n, B.prefix(32n, _))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
50  %Equal.sym(List<&2, U32>, B.prefix(32n, CV.after(32n, x)), CV.first(32n, CV.after(32n, x)), BL.prefix_first(32n, CV.after(32n, x))) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), B.head(B.suffix(31n, _)), Bool.and(E.zeros_ok(B.prefix(31n, B.prefix(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(B.head(B.suffix(31n, B.prefix(32n, CV.after(32n, x)))), 27), U32.is_eq(B.head(B.suffix(31n, B.prefix(32n, CV.after(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
51  %Equal.sym(List<&2, U32>, B.prefix(32n, CV.after(32n, x)), CV.first(32n, CV.after(32n, x)), BL.prefix_first(32n, CV.after(32n, x))) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), B.head(B.suffix(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(E.zeros_ok(B.prefix(31n, _)), Bool.or(U32.is_eq(B.head(B.suffix(31n, B.prefix(32n, CV.after(32n, x)))), 27), U32.is_eq(B.head(B.suffix(31n, B.prefix(32n, CV.after(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
52  %Equal.sym(List<&2, U32>, B.prefix(32n, CV.after(32n, x)), CV.first(32n, CV.after(32n, x)), BL.prefix_first(32n, CV.after(32n, x))) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), B.head(B.suffix(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(E.zeros_ok(B.prefix(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(B.head(B.suffix(31n, _)), 27), U32.is_eq(B.head(B.suffix(31n, B.prefix(32n, CV.after(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
53  %Equal.sym(List<&2, U32>, B.prefix(32n, CV.after(32n, x)), CV.first(32n, CV.after(32n, x)), BL.prefix_first(32n, CV.after(32n, x))) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), B.head(B.suffix(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(E.zeros_ok(B.prefix(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(B.head(B.suffix(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(B.head(B.suffix(31n, _)), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
54  %Equal.sym(List<&2, U32>, B.suffix(31n, CV.first(32n, CV.after(32n, x))), CV.after(31n, CV.first(32n, CV.after(32n, x))), BL.suffix_after(31n, CV.first(32n, CV.after(32n, x)))) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), B.head(_), Bool.and(E.zeros_ok(B.prefix(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(B.head(B.suffix(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(B.head(B.suffix(31n, CV.first(32n, CV.after(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
55  %Equal.sym(List<&2, U32>, B.suffix(31n, CV.first(32n, CV.after(32n, x))), CV.after(31n, CV.first(32n, CV.after(32n, x))), BL.suffix_after(31n, CV.first(32n, CV.after(32n, x)))) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), B.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(E.zeros_ok(B.prefix(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(B.head(_), 27), U32.is_eq(B.head(B.suffix(31n, CV.first(32n, CV.after(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
56  %Equal.sym(List<&2, U32>, B.suffix(31n, CV.first(32n, CV.after(32n, x))), CV.after(31n, CV.first(32n, CV.after(32n, x))), BL.suffix_after(31n, CV.first(32n, CV.after(32n, x)))) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), B.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(E.zeros_ok(B.prefix(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(B.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(B.head(_), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
57  %Equal.sym(U32, B.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), BL.head_eq(CV.after(31n, CV.first(32n, CV.after(32n, x))))) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), _, Bool.and(E.zeros_ok(B.prefix(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(B.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(B.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
58  %Equal.sym(U32, B.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), BL.head_eq(CV.after(31n, CV.first(32n, CV.after(32n, x))))) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(E.zeros_ok(B.prefix(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(_, 27), U32.is_eq(B.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
59  %Equal.sym(U32, B.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), BL.head_eq(CV.after(31n, CV.first(32n, CV.after(32n, x))))) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(E.zeros_ok(B.prefix(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(_, 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
60  %Equal.sym(List<&2, U32>, B.prefix(31n, CV.first(32n, CV.after(32n, x))), CV.first(31n, CV.first(32n, CV.after(32n, x))), BL.prefix_first(31n, CV.first(32n, CV.after(32n, x)))) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(E.zeros_ok(_), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
61  %Equal.sym(Bool, E.zeros_ok(CV.first(31n, CV.first(32n, CV.after(32n, x)))), ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), zeros_v(CV.first(31n, CV.first(32n, CV.after(32n, x))))) : {E.ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(_, Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
62  %Equal.sym(List<&2, U32>, B.prefix(32n, x), CV.first(32n, x), BL.prefix_first(32n, x)) : {E.ecrecover_v(_, B.suffix(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
63  %Equal.sym(List<&2, U32>, B.suffix(64n, x), CV.after(64n, x), BL.suffix_after(64n, x)) : {E.ecrecover_v(CV.first(32n, x), _, CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) == ES.ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28)))) : Maybe<&2, List<&2, U32>>}
64  ecv(one, h1, CV.first(32n, x), CV.after(64n, x), CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), Bool.and(ES.all_zero(CV.first(31n, CV.first(32n, CV.after(32n, x)))), Bool.or(U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 27), U32.is_eq(CV.head(CV.after(31n, CV.first(32n, CV.after(32n, x)))), 28))))
65
66# the ECRECOVER precompile
67def ecrecover_v(+one: Nat, +h1: {one == 1n : Nat}, +input: List<&2, U32>) -> {E.ecrecover(input) == ES.ecrecover(one, input) : Maybe<&2, List<&2, U32>>}:
68  %Equal.sym(List<&2, U32>, B.prefix(128n, List.append(&2, U32, input, List.replicate(U32, 128n, 0))), CV.first(128n, List.append(&2, U32, input, List.replicate(U32, 128n, 0))), BL.prefix_first(128n, List.append(&2, U32, input, List.replicate(U32, 128n, 0)))) : {E.ecrecover_in(_) == ES.ecrecover_in(one, CV.first(128n, List.append(&2, U32, input, List.replicate(U32, 128n, 0)))) : Maybe<&2, List<&2, U32>>}
69  ecin(one, h1, CV.first(128n, List.append(&2, U32, input, List.replicate(U32, 128n, 0))))