search

pirapira / eth-isabelle

A Lem formalization of EVM and some Isabelle/HOL proofs
Other
237 stars 42 forks source link

Figure out the sender of a transaction #422

Open pirapira opened 7 years ago

pirapira commented 7 years ago

In the blockchaintest format, a transaction is specified as

                   {
                        "data" : "0x7065cb48000000000000000000000000aaaf5374fce5edbc8e2a8697c15331677e6ebaaa",
                        "gasLimit" : "0x989680",
                        "gasPrice" : "0x01",
                        "nonce" : "0x01",
                        "r" : "0x81b347124f5a88c2e04509723f18984b91020bddbd74c982c651856727b5fa0d",
                        "s" : "0x41d1c0ef7309812cb795a5c86c462db176d8f782a8babbeb61ca715a49620504",
                        "to" : "0x6295ee1b4f6dd65047762f924ecd367c17eabf8f",
                        "v" : "0x1b",
                        "value" : "0x64"
                    }

The sender of the transaction needs to be computed from here.

This involves ECDSARECOVER operation.