search

pirapira / eth-isabelle

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

Different nonce value in `recursiveCreateReturnValue`. #393

Closed pirapira closed 7 years ago

pirapira commented 7 years ago

recursiveCreateReturnValue address 97a3956189161fe3d52554c2a599bb619983be5d has nonce 1, but it should be 0!

pirapira commented 7 years ago

The difference seems to be:

when the global stack reaches the maximum depth and CREATE returns 0, the nonce of the current environment is incremented in the Lem model, but not in the test case.

pirapira commented 7 years ago

The Yellow Paper says non-increment.