Look at `#mkCall` and `#mkCreate` in KEVM for doing calls

makerdao / mkr-mcd-spec

High level KSpecification for the MCD System by Runtime Verification and Maker Foundation

GNU General Public License v3.0

28 stars 9 forks source link

Look at `#mkCall` and `#mkCreate` in KEVM for doing calls #247

Open ehildenb opened 3 years ago

ehildenb commented 3 years ago

Both call #initVM.

Start with directly placing the state you need on the RHS of #serializeTx. Then start looking at the call-chains for #mkCall and #mkCreate to see if some of that can be re-used for initializing state (which makes your rule for #serializeTx smaller).