Simulations for the REVM arithmetic #547
Conversation
olympichek
changed the title
| pub struct Bytes(pub bytes::Bytes); | ||
| *) | ||
|
|
||
| Module Bytes. |
There was a problem hiding this comment.
It seems there are many crates on which we depend, like bytes here or alloy_primitives later. To keep things simple, instead of translating all these crates, you can create a CoqOfRust/revm/simulations/dependencies.v where we put all the simulations that are about the dependencies (except for alloc and core that we have translated).
| Admitted. | ||
| End Bytes. | ||
|
|
||
| Module Bytecode. |
There was a problem hiding this comment.
In a CoqOfRust/revm/primitives folder, so that we follow the folder name that they are using. We should move also what we have put into CoqOfRust/revm/ to CoqOfRust/revm/interpreter/ as there is only the translation of the interpreter folder.
|
|
||
| Module Interpreter. | ||
| Record t : Set := { | ||
| instruction_pointer : list Z; |
There was a problem hiding this comment.
| instruction_pointer : list Z; | |
| instruction_pointer : Z; |
I think the best way here is to interpret that as an index in the bytecode. We will write specifically how it relates to the Rust's translation.
Somewhat incomplete and possibly incorrect simulations for the `Interpreter` type and all the types it depends on
Simulation for the `record_cost()` function that is used in the implementation of the `gas!` macro that is used in arithmetic
Following REVM original project structure
olympichek
force-pushed
the
valerii-huhnin@revm-arithmetic-simulations
branch
from
23b16e2 to
87dc12f
Compare
olympichek
changed the title
Simulations for the REVM arithmetic operations and functions they depend on.
Work in progress on #545
This pull request also separates simulations from things related to links in core library and REVM.
For REVM, the following structure is used:
Additionally, it adds definition of
Lensstructure andlift_lensmonadic operation to use in REVM and other simulations to represent modifications of the substate.