~/bend-docscommunity

proofs/crypto/secp256k1/laws_recover.bend open laws/TODOs

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/laws_recover.bend as Laws_recover

4 imports
import Base
import ../../../src/crypto/secp256k1.bend as K
import ../../../spec/crypto/secp256k1/ecdsa.bend as ES
import ../../../spec/crypto/secp256k1/schnorr.bend as SS

Laws

law Recover.correct openits proof in laws_crypto.bend does not pass the checker (fails)source · line 21 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+sig:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1.recover(h, sig) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.recover(one, h, sig) : Maybe<&2, List<&2, U32>>}

public key recovery (SEC 1 4.1.6)

law Ecrecover.correct openits proof in laws_crypto.bend does not pass the checker (fails)source · line 29 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+input:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1.ecrecover(input) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.ecrecover(one, input) : Maybe<&2, List<&2, U32>>}

Ethereum's ECRECOVER precompile