1	# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pecr.src; edit the .src
2	import Base
3	import ../../../spec/crypto/secp256k1/curve.bend as CV
4	import ../../../spec/crypto/secp256k1/ecdsa.bend as ES
5	import ../../../src/crypto/secp256k1/bytes.bend as B
6	import ../../../src/crypto/secp256k1/ecdsa.bend as E
7	import ./prec.bend as PR
8	import ./peth.bend as PET
9	import ./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	
15	def 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	
22	def 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	
29	def 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	
37	def 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	
45	def 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
67	def 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))))