def ecin
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pecr.bend:45
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pecr.bend as Pecr
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL
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))))