~/bend-docscommunity

proofs/crypto/secp256k1/pecr.bend source

proofs/crypto/secp256k1/pecr.bend on the hub · documented module

# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pecr.src; edit the .srcimport Baseimport ../../../spec/crypto/secp256k1/curve.bend as CVimport ../../../spec/crypto/secp256k1/ecdsa.bend as ESimport ../../../src/crypto/secp256k1/bytes.bend as Bimport ../../../src/crypto/secp256k1/ecdsa.bend as Eimport ./prec.bend as PRimport ./peth.bend as PETimport ./blist.bend as BL# Ethereum's ECRECOVER precompile of src/crypto/secp256k1/ecdsa.bend against# spec/crypto/secp256k1/ecdsa.bend.def zeros_v(bs: List<&2, U32>) -> {E.zeros_ok(bs) == ES.all_zero(bs) : Bool}:  match bs:    case Nil{}:      {==}    case +b <> t:      Equal.cong(Bool, Bool, x => Bool.and(U32.is_eq(b, 0), x), E.zeros_ok(t), ES.all_zero(t), zeros_v(t))def ew_v(m: Maybe<&2, List<&2, U32>>) -> {E.eth_word(m) == ES.word_of(m) : Maybe<&2, List<&2, U32>>}:  match m:    case None{}:      {==}    case Some{a}:      {==}def aw_v(m: Maybe<&2, List<&2, U32>>) -> {E.addr_word(m) == ES.addr_word(m) : Maybe<&2, List<&2, U32>>}:  match m:    case None{}:      {==}    case Some{+pk}:      %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>>}      ew_v(ES.eth_address(pk))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>>}:  match ok:    case True{}:      %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>>}      aw_v(ES.recover(one, h, List.append(&2, U32, rs, [U32.sub(v, 27)])))    case False{}:      {==}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>>}:  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  %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>>}  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))))# the ECRECOVER precompiledef ecrecover_v(+one: Nat, +h1: {one == 1n : Nat}, +input: List<&2, U32>) -> {E.ecrecover(input) == ES.ecrecover(one, input) : Maybe<&2, List<&2, U32>>}:  %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>>}  ecin(one, h1, CV.first(128n, List.append(&2, U32, input, List.replicate(U32, 128n, 0))))