law Ecrecover.correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/laws_recover.bend:28

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1.bend as K
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES

28# Ethereum's ECRECOVER precompile
29law Ecrecover.correct:
30  for +one: Nat
31  for +h1: {one == 1n : Nat}
32  for +input: List<&2, U32>
33  {K.ecrecover(input) == ES.ecrecover(one, input) : Maybe<&2, List<&2, U32>>}