From 01d7a33949d8c3b0cd6c80c8a55f26f98abdf9b3 Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Mon, 20 May 2024 18:43:48 +0000 Subject: [PATCH 01/14] add `ToTy` and `ToValue` instances for lists/arrays --- CoqOfRust/core/simulations/array.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 CoqOfRust/core/simulations/array.v diff --git a/CoqOfRust/core/simulations/array.v b/CoqOfRust/core/simulations/array.v new file mode 100644 index 000000000..7971006bf --- /dev/null +++ b/CoqOfRust/core/simulations/array.v @@ -0,0 +1,14 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import simulations.M. +Require CoqOfRust.core.simulations.default. +Import simulations.M.Notations. + +Module Array. + Global Instance IsToTy (A : Set) (_ : ToTy A) : ToTy (list A) := { + Φ := Ty.apply (Ty.path "array") [Φ A]; + }. + + Global Instance IsToValue (A : Set) (_ : ToValue A) : ToValue (list A) := { + φ x := Value.Array (List.map φ x); + }. +End Array. From fa241b4c930fec698e5731d9ebd515d82b6d6401 Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Mon, 20 May 2024 18:45:40 +0000 Subject: [PATCH 02/14] add simulations the `Interpreter` type Somewhat incomplete and possibly incorrect simulations for the `Interpreter` type and all the types it depends on --- CoqOfRust/revm/simulations/arithmetic.v | 1031 +++++++++++++++++++++++ 1 file changed, 1031 insertions(+) create mode 100644 CoqOfRust/revm/simulations/arithmetic.v diff --git a/CoqOfRust/revm/simulations/arithmetic.v b/CoqOfRust/revm/simulations/arithmetic.v new file mode 100644 index 000000000..1574a2015 --- /dev/null +++ b/CoqOfRust/revm/simulations/arithmetic.v @@ -0,0 +1,1031 @@ +Require Import CoqOfRust.CoqOfRust. +Require CoqOfRust.core.simulations.default. +Require Import CoqOfRust.core.simulations.option. +Require Import CoqOfRust.core.simulations.result. +Require Import CoqOfRust.core.simulations.array. +Require Import CoqOfRust.core.simulations.bool. +Require CoqOfRust.examples.default.examples.ink_contracts.simulations.lib. +Require Import CoqOfRust.simulations.M. + +Import simulations.M.Notations. +Import simulations.bool.Notations. + +(** ** Primitives *) + + +(* + /// Represents the state of gas during execution. + #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct Gas { + /// The initial gas limit. This is constant throughout execution. + limit: u64, + /// The remaining gas. + remaining: u64, + /// Refunded gas. This is used only at the end of execution. + refunded: i64, + } +*) + +Module Gas. + Record t : Set := { + limit : Z; + remaining : Z; + refunded : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::gas::Gas"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::gas::Gas" [ + ("limit", φ x.(limit)); + ("remaining", φ x.(remaining)); + ("refunded", φ x.(refunded)) + ]; + }. +End Gas. + +(* + /// Wrapper type around [`bytes::Bytes`] to support "0x" prefixed hex strings. + #[derive(Clone, Default, Hash, PartialEq, Eq, PartialOrd, Ord)] + #[repr(transparent)] + pub struct Bytes(pub bytes::Bytes); +*) + +Module Bytes. + Parameter t : Set. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "bytes::bytes::Bytes"; + }. + + Global Instance IsToValue : ToValue t. + Admitted. +End Bytes. + +Module Bytecode. + Parameter t : Set. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_primitives::bytecode::Bytecode"; + }. + + Global Instance IsToValue : ToValue t. + Admitted. +End Bytecode. + +Module Address. + Parameter t : Set. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "alloy_primitives::bits::address::Address"; + }. + + Global Instance IsToValue : ToValue t. + Admitted. +End Address. + +Module FixedBytes. + Parameter t : Set. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "alloy_primitives::bits::fixed::FixedBytes"; + }. + + Global Instance IsToValue : ToValue t. + Admitted. +End FixedBytes. + +Definition B256 := FixedBytes.t. +Definition U256 := FixedBytes.t. + +(* + /// EVM contract information. + #[derive(Clone, Debug, Default)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct Contract { + /// Contracts data + pub input: Bytes, + /// Bytecode contains contract code, size of original code, analysis with gas block and jump table. + /// Note that current code is extended with push padding and STOP at end. + pub bytecode: Bytecode, + /// Bytecode hash for legacy. For EOF this would be None. + pub hash: Option, + /// Target address of the account. Storage of this address is going to be modified. + pub target_address: Address, + /// Caller of the EVM. + pub caller: Address, + /// Value send to contract from transaction or from CALL opcodes. + pub call_value: U256, + } +*) + +Module Contract. + Record t : Set := { + input : Bytes.t; + bytecode : Bytecode.t; + hash : option B256; + target_address : Address.t; + caller : Address.t; + call_value : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::contract::Contract"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::contract::Contract" [ + ("input", φ x.(input)); + ("bytecode", φ x.(bytecode)); + ("hash", φ x.(hash)); + ("target_address", φ x.(target_address)); + ("caller", φ x.(caller)); + ("call_value", φ x.(call_value)) + ]; + }. +End Contract. + +(* + #[repr(u8)] + #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub enum InstructionResult { + // success codes + #[default] + Continue = 0x00, + Stop, + Return, + SelfDestruct, + ReturnContract, + + // revert codes + Revert = 0x10, // revert opcode + CallTooDeep, + OutOfFunds, + + // Actions + CallOrCreate = 0x20, + + // error codes + OutOfGas = 0x50, + MemoryOOG, + MemoryLimitOOG, + PrecompileOOG, + InvalidOperandOOG, + OpcodeNotFound, + CallNotAllowedInsideStatic, + StateChangeDuringStaticCall, + InvalidFEOpcode, + InvalidJump, + NotActivated, + StackUnderflow, + StackOverflow, + OutOfOffset, + CreateCollision, + OverflowPayment, + PrecompileError, + NonceOverflow, + /// Create init code size exceeds limit (runtime). + CreateContractSizeLimit, + /// Error on created contract that begins with EF + CreateContractStartingWithEF, + /// EIP-3860: Limit and meter initcode. Initcode size limit exceeded. + CreateInitCodeSizeLimit, + /// Fatal external error. Returned by database. + FatalExternalError, + /// RETURNCONTRACT called in not init eof code. + ReturnContractInNotInitEOF, + /// Legacy contract is calling opcode that is enabled only in EOF. + EOFOpcodeDisabledInLegacy, + /// EOF function stack overflow + EOFFunctionStackOverflow, + } +*) + +Module InstructionResult. + Inductive t : Set := + (* success codes *) + | Continue + | Stop + | Return + | SelfDestruct + | ReturnContract + (* revert codes *) + | Revert + | CallTooDeep + | OutOfFunds + (* Actions *) + | CallOrCreate + (* error codes *) + | OutOfGas + | MemoryOOG + | MemoryLimitOOG + | PrecompileOOG + | InvalidOperandOOG + | OpcodeNotFound + | CallNotAllowedInsideStatic + | StateChangeDuringStaticCall + | InvalidFEOpcode + | InvalidJump + | NotActivated + | StackUnderflow + | StackOverflow + | OutOfOffset + | CreateCollision + | OverflowPayment + | PrecompileError + | NonceOverflow + | CreateContractSizeLimit + | CreateContractStartingWithEF + | CreateInitCodeSizeLimit + | FatalExternalError + | ReturnContractInNotInitEOF + | EOFOpcodeDisabledInLegacy + | EOFFunctionStackOverflow. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::instruction_result::InstructionResult"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + match x with + | Continue => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Continue" [] + | Stop => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Stop" [] + | Return => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Return" [] + | SelfDestruct => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::SelfDestruct" [] + | ReturnContract => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::ReturnContract" [] + | Revert => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Revert" [] + | CallTooDeep => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CallTooDeep" [] + | OutOfFunds => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OutOfFunds" [] + | CallOrCreate => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CallOrCreate" [] + | OutOfGas => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OutOfGas" [] + | MemoryOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::MemoryOOG" [] + | MemoryLimitOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::MemoryLimitOOG" [] + | PrecompileOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::PrecompileOOG" [] + | InvalidOperandOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG" [] + | OpcodeNotFound => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OpcodeNotFound" [] + | CallNotAllowedInsideStatic => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CallNotAllowedInsideStatic" [] + | StateChangeDuringStaticCall => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::StateChangeDuringStaticCall" [] + | InvalidFEOpcode => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::InvalidFEOpcode" [] + | InvalidJump => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::InvalidJump" [] + | NotActivated => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::NotActivated" [] + | StackUnderflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::StackUnderflow" [] + | StackOverflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::StackOverflow" [] + | OutOfOffset => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OutOfOffset" [] + | CreateCollision => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateCollision" [] + | OverflowPayment => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OverflowPayment" [] + | PrecompileError => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::PrecompileError" [] + | NonceOverflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::NonceOverflow" [] + | CreateContractSizeLimit => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateContractSizeLimit" [] + | CreateContractStartingWithEF => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateContractStartingWithEF" [] + | CreateInitCodeSizeLimit => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateInitCodeSizeLimit" [] + | FatalExternalError => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::FatalExternalError" [] + | ReturnContractInNotInitEOF => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::ReturnContractInNotInitEOF" [] + | EOFOpcodeDisabledInLegacy => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::EOFOpcodeDisabledInLegacy" [] + | EOFFunctionStackOverflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::EOFFunctionStackOverflow" [] + end; + }. +End InstructionResult. + +(* + /// A sequential memory shared between calls, which uses + /// a `Vec` for internal representation. + /// A [SharedMemory] instance should always be obtained using + /// the `new` static method to ensure memory safety. + #[derive(Clone, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct SharedMemory { + /// The underlying buffer. + buffer: Vec, + /// Memory checkpoints for each depth. + /// Invariant: these are always in bounds of `data`. + checkpoints: Vec, + /// Invariant: equals `self.checkpoints.last()` + last_checkpoint: usize, + /// Memory limit. See [`CfgEnv`](revm_primitives::CfgEnv). + #[cfg(feature = "memory_limit")] + memory_limit: u64, + } +*) + +Module SharedMemory. + Record t : Set := { + buffer : list Z; + checkpoints : list Z; + last_checkpoint : Z; + memory_limit : option Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::shared_memory::SharedMemory"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::shared_memory::SharedMemory" [ + ("buffer", φ x.(buffer)); + ("checkpoints", φ x.(checkpoints)); + ("last_checkpoint", φ x.(last_checkpoint)); + ("memory_limit", φ x.(memory_limit)) + ]; + }. +End SharedMemory. + +(* + /// EVM stack with [STACK_LIMIT] capacity of words. + #[derive(Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize))] + pub struct Stack { + /// The underlying data of the stack. + data: Vec, + } +*) + +Module Stack. + Record t : Set := { + data : list U256; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::stack::Stack"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::stack::Stack" [ + ("data", φ x.(data)) + ]; + }. +End Stack. + +(* + /// Function return frame. + /// Needed information for returning from a function. + #[derive(Debug, Default, Clone, Copy, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct FunctionReturnFrame { + /// The index of the code container that this frame is executing. + pub idx: usize, + /// The program counter where frame execution should continue. + pub pc: usize, + } +*) + +Module FunctionReturnFrame. + Record t : Set := { + idx : Z; + pc : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::function_return_frame::FunctionReturnFrame"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::function_return_frame::FunctionReturnFrame" [ + ("idx", φ x.(idx)); + ("pc", φ x.(pc)) + ]; + }. +End FunctionReturnFrame. + +(* + /// Function Stack + #[derive(Debug, Default)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct FunctionStack { + pub return_stack: Vec, + pub current_code_idx: usize, + } +*) + +(* TODO: Vectors? *) +Module FunctionStack. + Record t : Set := { + return_stack : list FunctionReturnFrame.t; + current_code_idx : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::function_stack::FunctionStack"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::function_stack::FunctionStack" [ + ("return_stack", φ x.(return_stack)); + ("current_code_idx", φ x.(current_code_idx)) + ]; + }. +End FunctionStack. + +(* + /// Call value. + #[derive(Clone, Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub enum CallValue { + /// Concrete value, transferred from caller to callee at the end of the transaction. + Transfer(U256), + /// Apparent value, that is **not** actually transferred. + /// + /// Set when in a `DELEGATECALL` call type, and used by the `CALLVALUE` opcode. + Apparent(U256), + } +*) + +Module CallValue. + Inductive t : Set := + | Transfer : Z -> t + | Apparent : Z -> t. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter_action::call_inputs::CallValue"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + match x with + | Transfer x => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallValue::Transfer" [φ x] + | Apparent x => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallValue::Approval" [φ x] + end; + }. +End CallValue. + +(* + /// Call scheme. + #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub enum CallScheme { + /// `CALL`. + Call, + /// `CALLCODE` + CallCode, + /// `DELEGATECALL` + DelegateCall, + /// `STATICCALL` + StaticCall, + } +*) + +Module CallScheme. + Inductive t : Set := + | Call + | CallCode + | DelegateCall + | StaticCall. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter_action::call_inputs::CallScheme"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + match x with + | Call => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::Call" [] + | CallCode => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::CallCode" [] + | DelegateCall => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::DelegateCall" [] + | StaticCall => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::StaticCall" [] + end; + }. +End CallScheme. + +(* + /// Inputs for a call. + #[derive(Clone, Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct CallInputs { + /// The call data of the call. + pub input: Bytes, + /// The return memory offset where the output of the call is written. + /// + /// In EOF, this range is invalid as EOF calls do not write output to memory. + pub return_memory_offset: Range, + /// The gas limit of the call. + pub gas_limit: u64, + /// The account address of bytecode that is going to be executed. + /// + /// Previously `context.code_address`. + pub bytecode_address: Address, + /// Target address, this account storage is going to be modified. + /// + /// Previously `context.address`. + pub target_address: Address, + /// This caller is invoking the call. + /// + /// Previously `context.caller`. + pub caller: Address, + /// Call value. + /// + /// NOTE: This value may not necessarily be transferred from caller to callee, see [`CallValue`]. + /// + /// Previously `transfer.value` or `context.apparent_value`. + pub value: CallValue, + /// The call scheme. + /// + /// Previously `context.scheme`. + pub scheme: CallScheme, + /// Whether the call is a static call, or is initiated inside a static call. + pub is_static: bool, + /// Whether the call is initiated from EOF bytecode. + pub is_eof: bool, + } +*) + +(* TODO: Ranges? *) +Module CallInputs. + Record t : Set := { + input : Bytes.t; + return_memory_offset : (Z * Z); + gas_limit : Z; + bytecode_address : Address.t; + target_address : Address.t; + caller : Address.t; + value : CallValue.t; + scheme : CallScheme.t; + is_static : bool; + is_eof : bool; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::call_inputs::CallInputs"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::call_inputs::CallInputs" [ + ("input", φ x.(input)); + ("return_memory_offset", φ x.(return_memory_offset)); + ("gas_limit", φ x.(gas_limit)); + ("bytecode_address", φ x.(bytecode_address)); + ("target_address", φ x.(target_address)); + ("caller", φ x.(caller)); + ("value", φ x.(value)); + ("scheme", φ x.(scheme)); + ("is_static", φ x.(is_static)); + ("is_eof", φ x.(is_eof)) + ]; + }. +End CallInputs. + +(* + /// Create scheme. + #[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub enum CreateScheme { + /// Legacy create scheme of `CREATE`. + Create, + /// Create scheme of `CREATE2`. + Create2 { + /// Salt. + salt: U256, + }, + } +*) + +Module CreateScheme. + Inductive t : Set := + | Create + | Create2 : Z -> t. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_primitives::env::CreateScheme"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + match x with + | Create => Value.StructTuple "revm_primitives::env::CreateScheme::Create" [] + | Create2 x => Value.StructTuple "revm_primitives::env::CreateScheme::Create2" [φ x] + end; + }. +End CreateScheme. + +(* + /// Inputs for a create call. + #[derive(Clone, Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct CreateInputs { + /// Caller address of the EVM. + pub caller: Address, + /// The create scheme. + pub scheme: CreateScheme, + /// The value to transfer. + pub value: U256, + /// The init code of the contract. + pub init_code: Bytes, + /// The gas limit of the call. + pub gas_limit: u64, + } +*) + +Module CreateInputs. + Record t : Set := { + caller : Address.t; + scheme : CreateScheme.t; + value : U256; + init_code : Bytes.t; + gas_limit : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::create_inputs::CreateInputs"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::create_inputs::CreateInputs" [ + ("caller", φ x.(caller)); + ("scheme", φ x.(scheme)); + ("value", φ x.(value)); + ("init_code", φ x.(init_code)); + ("gas_limit", φ x.(gas_limit)) + ]; + }. +End CreateInputs. + +(* + /// EOF Header containing + #[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct EofHeader { + /// Size of EOF types section. + /// types section includes num of input and outputs and max stack size. + pub types_size: u16, + /// Sizes of EOF code section. + /// Code size can't be zero. + pub code_sizes: Vec, + /// EOF Container size. + /// Container size can be zero. + pub container_sizes: Vec, + /// EOF data size. + pub data_size: u16, + /// sum code sizes + pub sum_code_sizes: usize, + /// sum container sizes + pub sum_container_sizes: usize, + } +*) + +Module EofHeader. + Record t : Set := { + types_size : Z; + code_sizes : list Z; + container_sizes : list Z; + data_size : Z; + sum_code_sizes : Z; + sum_container_sizes : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_primitives::bytecode::eof::header::EofHeader"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_primitives::bytecode::eof::header::EofHeader" [ + ("types_size", φ x.(types_size)); + ("code_sizes", φ x.(code_sizes)); + ("container_sizes", φ x.(container_sizes)); + ("data_size", φ x.(data_size)); + ("sum_code_sizes", φ x.(sum_code_sizes)); + ("sum_container_sizes", φ x.(sum_container_sizes)) + ]; + }. +End EofHeader. + +(* + /// Types section that contains stack information for matching code section. + #[derive(Debug, Clone, Default, Hash, PartialEq, Eq, Copy)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct TypesSection { + /// inputs - 1 byte - `0x00-0x7F` + /// number of stack elements the code section consumes + pub inputs: u8, + /// outputs - 1 byte - `0x00-0x80` + /// number of stack elements the code section returns or 0x80 for non-returning functions + pub outputs: u8, + /// max_stack_height - 2 bytes - `0x0000-0x03FF` + /// maximum number of elements ever placed onto the stack by the code section + pub max_stack_size: u16, + } +*) + +Module TypesSection. + Record t : Set := { + inputs : Z; + outputs : Z; + max_stack_size : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_primitives::bytecode::eof::types_section::TypesSection"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_primitives::bytecode::eof::types_section::TypesSection" [ + ("inputs", φ x.(inputs)); + ("outputs", φ x.(outputs)); + ("max_stack_size", φ x.(max_stack_size)) + ]; + }. +End TypesSection. + +(* + /// EOF Body, contains types, code, container and data sections. + /// + /// Can be used to create new EOF object. + #[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct EofBody { + pub types_section: Vec, + pub code_section: Vec, + pub container_section: Vec, + pub data_section: Bytes, + pub is_data_filled: bool, + } +*) + +Module EofBody. + Record t : Set := { + types_section : list TypesSection.t; + code_section : list Bytes.t; + container_section : list Bytes.t; + data_section : Bytes.t; + is_data_filled : bool; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_primitives::bytecode::eof::body::EofBody"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_primitives::bytecode::eof::body::EofBody" [ + ("types_section", φ x.(types_section)); + ("code_section", φ x.(code_section)); + ("container_section", φ x.(container_section)); + ("data_section", φ x.(data_section)); + ("is_data_filled", φ x.(is_data_filled)) + ]; + }. +End EofBody. + +(* + /// EOF - Ethereum Object Format. + /// + /// It consist of a header, body and raw original bytes Specified in EIP. + /// Most of body contain Bytes so it references to the raw bytes. + /// + /// If there is a need to create new EOF from scratch, it is recommended to use `EofBody` and + /// use `encode` function to create full [`Eof`] object. + #[derive(Clone, Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct Eof { + pub header: EofHeader, + pub body: EofBody, + pub raw: Bytes, + } +*) + +Module Eof. + Record t : Set := { + header : EofHeader.t; + body : EofBody.t; + raw : Bytes.t; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_primitives::bytecode::eof::Eof"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_primitives::bytecode::eof::Eof" [ + ("header", φ x.(header)); + ("body", φ x.(body)); + ("raw", φ x.(raw)) + ]; + }. +End Eof. + +(* + /// Inputs for EOF create call. + #[derive(Debug, Default, Clone, PartialEq, Eq)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct EOFCreateInput { + /// Caller of Eof Craate + pub caller: Address, + /// New contract address. + pub created_address: Address, + /// Values of ether transfered + pub value: U256, + /// Init eof code that is going to be executed. + pub eof_init_code: Eof, + /// Gas limit for the create call. + pub gas_limit: u64, + /// Return memory range. If EOF creation Reverts it can return the + /// the memory range. + pub return_memory_range: Range, + } +*) + +Module EOFCreateInput. + Record t : Set := { + caller : Address.t; + created_address : Address.t; + value : U256; + eof_init_code : Eof.t; + gas_limit : Z; + return_memory_range : (Z * Z); + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::eof_create_input::EOFCreateInput"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::eof_create_input::EOFCreateInput" [ + ("caller", φ x.(caller)); + ("created_address", φ x.(created_address)); + ("value", φ x.(value)); + ("eof_init_code", φ x.(eof_init_code)); + ("gas_limit", φ x.(gas_limit)); + ("return_memory_range", φ x.(return_memory_range)) + ]; + }. +End EOFCreateInput. + +(* + /// The result of an interpreter operation. + #[derive(Clone, Debug, PartialEq, Eq)] + #[cfg_attr(feature = "serde", derive(::serde::Serialize, ::serde::Deserialize))] + pub struct InterpreterResult { + /// The result of the instruction execution. + pub result: InstructionResult, + /// The output of the instruction execution. + pub output: Bytes, + /// The gas usage information. + pub gas: Gas, + } +*) + +Module InterpreterResult. + Record t : Set := { + result : InstructionResult.t; + output : Bytes.t; + gas : Gas.t; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::InterpreterResult"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::InterpreterResult" [ + ("result", φ x.(result)); + ("output", φ x.(output)); + ("gas", φ x.(gas)) + ]; + }. +End InterpreterResult. + +(* + #[derive(Clone, Debug, Default, PartialEq, Eq)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub enum InterpreterAction { + /// CALL, CALLCODE, DELEGATECALL, STATICCALL + /// or EOF EXT instuction called. + Call { inputs: Box }, + /// CREATE or CREATE2 instruction called. + Create { inputs: Box }, + /// EOF CREATE instruction called. + EOFCreate { inputs: Box }, + /// Interpreter finished execution. + Return { result: InterpreterResult }, + /// No action + #[default] + None, + } +*) + +(* TODO: Box? *) +Module InterpreterAction. + Inductive t : Set := + | Call : CallInputs.t -> t + | Create : CreateInputs.t -> t + | EOFCreate : EOFCreateInput.t -> t + | Return : InterpreterResult.t -> t + | None. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter_action::InterpreterAction"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + match x with + | Call x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::Call" [("inputs", φ x)] + | Create x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::Create" [("inputs", φ x)] + | EOFCreate x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::EOFCreate" [("inputs", φ x)] + | Return x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::Return" [("result", φ x)] + | None => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::None" [] + end; + }. +End InterpreterAction. + +(* + /// EVM bytecode interpreter. + #[derive(Debug)] + pub struct Interpreter { + /// The current instruction pointer. + pub instruction_pointer: *const u8, + /// The gas state. + pub gas: Gas, + /// Contract information and invoking data + pub contract: Contract, + /// The execution control flag. If this is not set to `Continue`, the interpreter will stop + /// execution. + pub instruction_result: InstructionResult, + /// Currently run Bytecode that instruction result will point to. + /// Bytecode is owned by the contract. + pub bytecode: Bytes, + /// Whether we are Interpreting the Ethereum Object Format (EOF) bytecode. + /// This is local field that is set from `contract.is_eof()`. + pub is_eof: bool, + /// Is init flag for eof create + pub is_eof_init: bool, + /// Shared memory. + /// + /// Note: This field is only set while running the interpreter loop. + /// Otherwise it is taken and replaced with empty shared memory. + pub shared_memory: SharedMemory, + /// Stack. + pub stack: Stack, + /// EOF function stack. + pub function_stack: FunctionStack, + /// The return data buffer for internal calls. + /// It has multi usage: + /// + /// * It contains the output bytes of call sub call. + /// * When this interpreter finishes execution it contains the output bytes of this contract. + pub return_data_buffer: Bytes, + /// Whether the interpreter is in "staticcall" mode, meaning no state changes can happen. + pub is_static: bool, + /// Actions that the EVM should do. + /// + /// Set inside CALL or CREATE instructions and RETURN or REVERT instructions. Additionally those instructions will set + /// InstructionResult to CallOrCreate/Return/Revert so we know the reason. + pub next_action: InterpreterAction, + } +*) + +Module Interpreter. + Record t : Set := { + instruction_pointer : list Z; + gas : Gas.t; + contract : Contract.t; + instruction_result : InstructionResult.t; + Bytecode : Bytes.t; + IsEof : bool; + IsEofInit : bool; + SharedMemory : SharedMemory.t; + stack : Stack.t; + function_stack : FunctionStack.t; + return_data_buffer : Bytes.t; + is_static : bool; + next_action : InterpreterAction.t; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::Interpreter"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::Interpreter" [ + ("instruction_pointer", φ x.(instruction_pointer)); + ("gas", φ x.(gas)); + ("contract", φ x.(contract)); + ("instruction_result", φ x.(instruction_result)); + ("Bytecode", φ x.(Bytecode)); + ("IsEof", φ x.(IsEof)); + ("IsEofInit", φ x.(IsEofInit)); + ("SharedMemory", φ x.(SharedMemory)); + ("stack", φ x.(stack)); + ("function_stack", φ x.(function_stack)); + ("return_data_buffer", φ x.(return_data_buffer)); + ("is_static", φ x.(is_static)); + ("next_action", φ x.(next_action)) + ]; + }. +End Interpreter. From 13c8b8a726f02dfa93eefae55ee6f39f45a54059 Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Mon, 20 May 2024 18:52:52 +0000 Subject: [PATCH 03/14] simulation for the `record_cost()` function Simulation for the `record_cost()` function that is used in the implementation of the `gas!` macro that is used in arithmetic --- CoqOfRust/revm/simulations/arithmetic.v | 28 +++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/CoqOfRust/revm/simulations/arithmetic.v b/CoqOfRust/revm/simulations/arithmetic.v index 1574a2015..6db61d7cc 100644 --- a/CoqOfRust/revm/simulations/arithmetic.v +++ b/CoqOfRust/revm/simulations/arithmetic.v @@ -46,6 +46,34 @@ Module Gas. ("refunded", φ x.(refunded)) ]; }. + + (* + /// Records an explicit cost. + /// + /// Returns `false` if the gas limit is exceeded. + #[inline] + #[must_use = "prefer using `gas!` instead to return an out-of-gas error on failure"] + pub fn record_cost(&mut self, cost: u64) -> bool { + let (remaining, overflow) = self.remaining.overflowing_sub(cost); + let success = !overflow; + if success { + self.remaining = remaining; + } + success + } + *) + Definition record_cost + (cost : Z) : + MS? t string bool := + letS? 'gas := readS? in + let remaining_sub_cost := gas.(remaining) - cost in + let success := remaining_sub_cost >=? 0 in + letS? _ := + if success + then writeS? (gas <| remaining := remaining_sub_cost |>) + else returnS? tt + in + returnS? success. End Gas. (* From ac3d15b007b9f6ebf8606835be1d17f4bb0cd29e Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Wed, 22 May 2024 20:20:49 +0000 Subject: [PATCH 04/14] simulation for the `gas!` macro --- CoqOfRust/revm/simulations/arithmetic.v | 47 +++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/CoqOfRust/revm/simulations/arithmetic.v b/CoqOfRust/revm/simulations/arithmetic.v index 6db61d7cc..d5866741a 100644 --- a/CoqOfRust/revm/simulations/arithmetic.v +++ b/CoqOfRust/revm/simulations/arithmetic.v @@ -1056,4 +1056,51 @@ Module Interpreter. ("next_action", φ x.(next_action)) ]; }. + + Definition update_gas + {A : Set} + (m : MS? Gas.t string A) : + MS? Interpreter.t string A := + letS? interp := readS? in + let gas := Interpreter.gas interp in + match m gas with + | (result, state) => + match result with + | inr e => panicS? e + | inl result => + letS? _ := writeS? (interp <| + Interpreter.gas := state + |>) in + returnS? result + end + end. End Interpreter. + +(* + /// Records a `gas` cost and fails the instruction if it would exceed the available gas. + #[macro_export] + macro_rules! gas { + ($interp:expr, $gas:expr) => { + $crate::gas!($interp, $gas, ()) + }; + ($interp:expr, $gas:expr, $ret:expr) => { + if !$interp.gas.record_cost($gas) { + $interp.instruction_result = $crate::InstructionResult::OutOfGas; + return $ret; + } + }; + } +*) + +Definition gas_macro (gas : Z) : + MS? Interpreter.t string unit := + letS? interp := readS? in + letS? success := Interpreter.update_gas (Gas.record_cost gas) in + if negb success + then + letS? _ := writeS? (interp <| + Interpreter.instruction_result := InstructionResult.OutOfGas + |>) in + returnS? tt + else + returnS? tt. From 19c07c39648039e0bcc3a26d64f166324fa29032 Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Wed, 22 May 2024 22:21:39 +0000 Subject: [PATCH 05/14] simulations for stack operations --- CoqOfRust/revm/simulations/arithmetic.v | 119 ++++++++++++++++++++++-- 1 file changed, 112 insertions(+), 7 deletions(-) diff --git a/CoqOfRust/revm/simulations/arithmetic.v b/CoqOfRust/revm/simulations/arithmetic.v index d5866741a..f926ad81e 100644 --- a/CoqOfRust/revm/simulations/arithmetic.v +++ b/CoqOfRust/revm/simulations/arithmetic.v @@ -376,20 +376,125 @@ End SharedMemory. *) Module Stack. - Record t : Set := { - data : list U256; - }. + Inductive t : Set := + | data : list U256 -> t. Global Instance IsToTy : ToTy t := { Φ := Ty.path "revm_interpreter::interpreter::stack::Stack"; }. Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_interpreter::interpreter::stack::Stack" [ - ("data", φ x.(data)) - ]; + φ '(data x) := + Value.StructRecord "revm_interpreter::interpreter::stack::Stack" [("data", φ x)] }. + + (* + /// Returns the length of the stack in words. + #[inline] + pub fn len(&self) -> usize { + self.data.len() + } + *) + Definition len '(data stack) : Z := + Z.of_nat (List.length stack). + + (* + /// Removes the topmost element from the stack and returns it, or `StackUnderflow` if it is + /// empty. + #[inline] + pub fn pop(&mut self) -> Result { + self.data.pop().ok_or(InstructionResult::StackUnderflow) + } + *) + Definition pop : + MS? t string (U256 + InstructionResult.t) := + letS? '(data stack) := readS? in + match stack with + | [] => returnS? (inr InstructionResult.StackUnderflow) + | x :: xs => + letS? _ := writeS? (data xs) in + returnS? (inl x) + end. + + (* + /// Removes the topmost element from the stack and returns it. + /// + /// # Safety + /// + /// The caller is responsible for checking the length of the stack. + #[inline] + pub unsafe fn pop_unsafe(&mut self) -> U256 { + self.data.pop().unwrap_unchecked() + } + *) + Definition pop_unsafe : + MS? t string U256 := + letS? result := pop in + match result with + | inl x => returnS? x + | inr _ => panicS? "Stack underflow" + end. + + (* + /// Peeks the top of the stack. + /// + /// # Safety + /// + /// The caller is responsible for checking the length of the stack. + #[inline] + pub unsafe fn top_unsafe(&mut self) -> &mut U256 { + let len = self.data.len(); + self.data.get_unchecked_mut(len - 1) + } + *) + Definition top_unsafe : + MS? t string U256 := + letS? '(data stack) := readS? in + match stack with + | [] => panicS? "Stack underflow" + | x :: _ => returnS? x + end. + + (* + /// Pop the topmost value, returning the value and the new topmost value. + /// + /// # Safety + /// + /// The caller is responsible for checking the length of the stack. + #[inline] + pub unsafe fn pop_top_unsafe(&mut self) -> (U256, &mut U256) { + let pop = self.pop_unsafe(); + let top = self.top_unsafe(); + (pop, top) + } + *) + Definition pop_top_unsafe : + MS? t string (U256 * U256) := + letS? pop := pop_unsafe in + letS? top := top_unsafe in + returnS? (pop, top). + + (* + /// Pops 2 values from the stack and returns them, in addition to the new topmost value. + /// + /// # Safety + /// + /// The caller is responsible for checking the length of the stack. + #[inline] + pub unsafe fn pop2_top_unsafe(&mut self) -> (U256, U256, &mut U256) { + let pop1 = self.pop_unsafe(); + let pop2 = self.pop_unsafe(); + let top = self.top_unsafe(); + + (pop1, pop2, top) + } + *) + Definition pop2_top_unsafe : + MS? t string (U256 * U256 * U256) := + letS? pop1 := pop_unsafe in + letS? pop2 := pop_unsafe in + letS? top := top_unsafe in + returnS? (pop1, pop2, top). End Stack. (* From c4b5d2c693bbc291831bb53d4cd8e5dc7d228daf Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Tue, 4 Jun 2024 10:00:55 +0000 Subject: [PATCH 06/14] split REVM simulations to multiple files Following REVM original project structure --- CoqOfRust/revm/simulations/arithmetic.v | 1211 ----------------- CoqOfRust/revm/simulations/dependencies.v | 45 + .../interpreter/instructions/macros.v | 35 + .../simulations/interpreter/interpreter.v | 116 ++ .../interpreter/interpreter/contract.v | 53 + .../interpreter/interpreter/function_stack.v | 65 + .../simulations/interpreter/interpreter/gas.v | 66 + .../interpreter/instruction_result.v | 145 ++ .../interpreter/interpreter/shared_memory.v | 48 + .../interpreter/interpreter/stack.v | 138 ++ .../interpreter/interpreter_action.v | 87 ++ .../interpreter_action/call_inputs.v | 153 +++ .../interpreter_action/create_inputs.v | 47 + .../interpreter_action/eof_create_inputs.v | 52 + .../revm/simulations/primitives/bytecode.v | 27 + .../simulations/primitives/bytecode/eof.v | 43 + .../primitives/bytecode/eof/body.v | 46 + .../primitives/bytecode/eof/header.v | 53 + .../primitives/bytecode/eof/type_section.v | 40 + CoqOfRust/revm/simulations/primitives/env.v | 35 + 20 files changed, 1294 insertions(+), 1211 deletions(-) delete mode 100644 CoqOfRust/revm/simulations/arithmetic.v create mode 100644 CoqOfRust/revm/simulations/dependencies.v create mode 100644 CoqOfRust/revm/simulations/interpreter/instructions/macros.v create mode 100644 CoqOfRust/revm/simulations/interpreter/interpreter.v create mode 100644 CoqOfRust/revm/simulations/interpreter/interpreter/contract.v create mode 100644 CoqOfRust/revm/simulations/interpreter/interpreter/function_stack.v create mode 100644 CoqOfRust/revm/simulations/interpreter/interpreter/gas.v create mode 100644 CoqOfRust/revm/simulations/interpreter/interpreter/instruction_result.v create mode 100644 CoqOfRust/revm/simulations/interpreter/interpreter/shared_memory.v create mode 100644 CoqOfRust/revm/simulations/interpreter/interpreter/stack.v create mode 100644 CoqOfRust/revm/simulations/interpreter/interpreter_action.v create mode 100644 CoqOfRust/revm/simulations/interpreter/interpreter_action/call_inputs.v create mode 100644 CoqOfRust/revm/simulations/interpreter/interpreter_action/create_inputs.v create mode 100644 CoqOfRust/revm/simulations/interpreter/interpreter_action/eof_create_inputs.v create mode 100644 CoqOfRust/revm/simulations/primitives/bytecode.v create mode 100644 CoqOfRust/revm/simulations/primitives/bytecode/eof.v create mode 100644 CoqOfRust/revm/simulations/primitives/bytecode/eof/body.v create mode 100644 CoqOfRust/revm/simulations/primitives/bytecode/eof/header.v create mode 100644 CoqOfRust/revm/simulations/primitives/bytecode/eof/type_section.v create mode 100644 CoqOfRust/revm/simulations/primitives/env.v diff --git a/CoqOfRust/revm/simulations/arithmetic.v b/CoqOfRust/revm/simulations/arithmetic.v deleted file mode 100644 index f926ad81e..000000000 --- a/CoqOfRust/revm/simulations/arithmetic.v +++ /dev/null @@ -1,1211 +0,0 @@ -Require Import CoqOfRust.CoqOfRust. -Require CoqOfRust.core.simulations.default. -Require Import CoqOfRust.core.simulations.option. -Require Import CoqOfRust.core.simulations.result. -Require Import CoqOfRust.core.simulations.array. -Require Import CoqOfRust.core.simulations.bool. -Require CoqOfRust.examples.default.examples.ink_contracts.simulations.lib. -Require Import CoqOfRust.simulations.M. - -Import simulations.M.Notations. -Import simulations.bool.Notations. - -(** ** Primitives *) - - -(* - /// Represents the state of gas during execution. - #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub struct Gas { - /// The initial gas limit. This is constant throughout execution. - limit: u64, - /// The remaining gas. - remaining: u64, - /// Refunded gas. This is used only at the end of execution. - refunded: i64, - } -*) - -Module Gas. - Record t : Set := { - limit : Z; - remaining : Z; - refunded : Z; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::gas::Gas"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_interpreter::gas::Gas" [ - ("limit", φ x.(limit)); - ("remaining", φ x.(remaining)); - ("refunded", φ x.(refunded)) - ]; - }. - - (* - /// Records an explicit cost. - /// - /// Returns `false` if the gas limit is exceeded. - #[inline] - #[must_use = "prefer using `gas!` instead to return an out-of-gas error on failure"] - pub fn record_cost(&mut self, cost: u64) -> bool { - let (remaining, overflow) = self.remaining.overflowing_sub(cost); - let success = !overflow; - if success { - self.remaining = remaining; - } - success - } - *) - Definition record_cost - (cost : Z) : - MS? t string bool := - letS? 'gas := readS? in - let remaining_sub_cost := gas.(remaining) - cost in - let success := remaining_sub_cost >=? 0 in - letS? _ := - if success - then writeS? (gas <| remaining := remaining_sub_cost |>) - else returnS? tt - in - returnS? success. -End Gas. - -(* - /// Wrapper type around [`bytes::Bytes`] to support "0x" prefixed hex strings. - #[derive(Clone, Default, Hash, PartialEq, Eq, PartialOrd, Ord)] - #[repr(transparent)] - pub struct Bytes(pub bytes::Bytes); -*) - -Module Bytes. - Parameter t : Set. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "bytes::bytes::Bytes"; - }. - - Global Instance IsToValue : ToValue t. - Admitted. -End Bytes. - -Module Bytecode. - Parameter t : Set. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_primitives::bytecode::Bytecode"; - }. - - Global Instance IsToValue : ToValue t. - Admitted. -End Bytecode. - -Module Address. - Parameter t : Set. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "alloy_primitives::bits::address::Address"; - }. - - Global Instance IsToValue : ToValue t. - Admitted. -End Address. - -Module FixedBytes. - Parameter t : Set. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "alloy_primitives::bits::fixed::FixedBytes"; - }. - - Global Instance IsToValue : ToValue t. - Admitted. -End FixedBytes. - -Definition B256 := FixedBytes.t. -Definition U256 := FixedBytes.t. - -(* - /// EVM contract information. - #[derive(Clone, Debug, Default)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub struct Contract { - /// Contracts data - pub input: Bytes, - /// Bytecode contains contract code, size of original code, analysis with gas block and jump table. - /// Note that current code is extended with push padding and STOP at end. - pub bytecode: Bytecode, - /// Bytecode hash for legacy. For EOF this would be None. - pub hash: Option, - /// Target address of the account. Storage of this address is going to be modified. - pub target_address: Address, - /// Caller of the EVM. - pub caller: Address, - /// Value send to contract from transaction or from CALL opcodes. - pub call_value: U256, - } -*) - -Module Contract. - Record t : Set := { - input : Bytes.t; - bytecode : Bytecode.t; - hash : option B256; - target_address : Address.t; - caller : Address.t; - call_value : Z; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter::contract::Contract"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_interpreter::interpreter::contract::Contract" [ - ("input", φ x.(input)); - ("bytecode", φ x.(bytecode)); - ("hash", φ x.(hash)); - ("target_address", φ x.(target_address)); - ("caller", φ x.(caller)); - ("call_value", φ x.(call_value)) - ]; - }. -End Contract. - -(* - #[repr(u8)] - #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub enum InstructionResult { - // success codes - #[default] - Continue = 0x00, - Stop, - Return, - SelfDestruct, - ReturnContract, - - // revert codes - Revert = 0x10, // revert opcode - CallTooDeep, - OutOfFunds, - - // Actions - CallOrCreate = 0x20, - - // error codes - OutOfGas = 0x50, - MemoryOOG, - MemoryLimitOOG, - PrecompileOOG, - InvalidOperandOOG, - OpcodeNotFound, - CallNotAllowedInsideStatic, - StateChangeDuringStaticCall, - InvalidFEOpcode, - InvalidJump, - NotActivated, - StackUnderflow, - StackOverflow, - OutOfOffset, - CreateCollision, - OverflowPayment, - PrecompileError, - NonceOverflow, - /// Create init code size exceeds limit (runtime). - CreateContractSizeLimit, - /// Error on created contract that begins with EF - CreateContractStartingWithEF, - /// EIP-3860: Limit and meter initcode. Initcode size limit exceeded. - CreateInitCodeSizeLimit, - /// Fatal external error. Returned by database. - FatalExternalError, - /// RETURNCONTRACT called in not init eof code. - ReturnContractInNotInitEOF, - /// Legacy contract is calling opcode that is enabled only in EOF. - EOFOpcodeDisabledInLegacy, - /// EOF function stack overflow - EOFFunctionStackOverflow, - } -*) - -Module InstructionResult. - Inductive t : Set := - (* success codes *) - | Continue - | Stop - | Return - | SelfDestruct - | ReturnContract - (* revert codes *) - | Revert - | CallTooDeep - | OutOfFunds - (* Actions *) - | CallOrCreate - (* error codes *) - | OutOfGas - | MemoryOOG - | MemoryLimitOOG - | PrecompileOOG - | InvalidOperandOOG - | OpcodeNotFound - | CallNotAllowedInsideStatic - | StateChangeDuringStaticCall - | InvalidFEOpcode - | InvalidJump - | NotActivated - | StackUnderflow - | StackOverflow - | OutOfOffset - | CreateCollision - | OverflowPayment - | PrecompileError - | NonceOverflow - | CreateContractSizeLimit - | CreateContractStartingWithEF - | CreateInitCodeSizeLimit - | FatalExternalError - | ReturnContractInNotInitEOF - | EOFOpcodeDisabledInLegacy - | EOFFunctionStackOverflow. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::instruction_result::InstructionResult"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - match x with - | Continue => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Continue" [] - | Stop => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Stop" [] - | Return => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Return" [] - | SelfDestruct => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::SelfDestruct" [] - | ReturnContract => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::ReturnContract" [] - | Revert => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Revert" [] - | CallTooDeep => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CallTooDeep" [] - | OutOfFunds => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OutOfFunds" [] - | CallOrCreate => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CallOrCreate" [] - | OutOfGas => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OutOfGas" [] - | MemoryOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::MemoryOOG" [] - | MemoryLimitOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::MemoryLimitOOG" [] - | PrecompileOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::PrecompileOOG" [] - | InvalidOperandOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG" [] - | OpcodeNotFound => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OpcodeNotFound" [] - | CallNotAllowedInsideStatic => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CallNotAllowedInsideStatic" [] - | StateChangeDuringStaticCall => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::StateChangeDuringStaticCall" [] - | InvalidFEOpcode => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::InvalidFEOpcode" [] - | InvalidJump => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::InvalidJump" [] - | NotActivated => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::NotActivated" [] - | StackUnderflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::StackUnderflow" [] - | StackOverflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::StackOverflow" [] - | OutOfOffset => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OutOfOffset" [] - | CreateCollision => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateCollision" [] - | OverflowPayment => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OverflowPayment" [] - | PrecompileError => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::PrecompileError" [] - | NonceOverflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::NonceOverflow" [] - | CreateContractSizeLimit => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateContractSizeLimit" [] - | CreateContractStartingWithEF => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateContractStartingWithEF" [] - | CreateInitCodeSizeLimit => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateInitCodeSizeLimit" [] - | FatalExternalError => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::FatalExternalError" [] - | ReturnContractInNotInitEOF => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::ReturnContractInNotInitEOF" [] - | EOFOpcodeDisabledInLegacy => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::EOFOpcodeDisabledInLegacy" [] - | EOFFunctionStackOverflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::EOFFunctionStackOverflow" [] - end; - }. -End InstructionResult. - -(* - /// A sequential memory shared between calls, which uses - /// a `Vec` for internal representation. - /// A [SharedMemory] instance should always be obtained using - /// the `new` static method to ensure memory safety. - #[derive(Clone, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub struct SharedMemory { - /// The underlying buffer. - buffer: Vec, - /// Memory checkpoints for each depth. - /// Invariant: these are always in bounds of `data`. - checkpoints: Vec, - /// Invariant: equals `self.checkpoints.last()` - last_checkpoint: usize, - /// Memory limit. See [`CfgEnv`](revm_primitives::CfgEnv). - #[cfg(feature = "memory_limit")] - memory_limit: u64, - } -*) - -Module SharedMemory. - Record t : Set := { - buffer : list Z; - checkpoints : list Z; - last_checkpoint : Z; - memory_limit : option Z; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter::shared_memory::SharedMemory"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_interpreter::interpreter::shared_memory::SharedMemory" [ - ("buffer", φ x.(buffer)); - ("checkpoints", φ x.(checkpoints)); - ("last_checkpoint", φ x.(last_checkpoint)); - ("memory_limit", φ x.(memory_limit)) - ]; - }. -End SharedMemory. - -(* - /// EVM stack with [STACK_LIMIT] capacity of words. - #[derive(Debug, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize))] - pub struct Stack { - /// The underlying data of the stack. - data: Vec, - } -*) - -Module Stack. - Inductive t : Set := - | data : list U256 -> t. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter::stack::Stack"; - }. - - Global Instance IsToValue : ToValue t := { - φ '(data x) := - Value.StructRecord "revm_interpreter::interpreter::stack::Stack" [("data", φ x)] - }. - - (* - /// Returns the length of the stack in words. - #[inline] - pub fn len(&self) -> usize { - self.data.len() - } - *) - Definition len '(data stack) : Z := - Z.of_nat (List.length stack). - - (* - /// Removes the topmost element from the stack and returns it, or `StackUnderflow` if it is - /// empty. - #[inline] - pub fn pop(&mut self) -> Result { - self.data.pop().ok_or(InstructionResult::StackUnderflow) - } - *) - Definition pop : - MS? t string (U256 + InstructionResult.t) := - letS? '(data stack) := readS? in - match stack with - | [] => returnS? (inr InstructionResult.StackUnderflow) - | x :: xs => - letS? _ := writeS? (data xs) in - returnS? (inl x) - end. - - (* - /// Removes the topmost element from the stack and returns it. - /// - /// # Safety - /// - /// The caller is responsible for checking the length of the stack. - #[inline] - pub unsafe fn pop_unsafe(&mut self) -> U256 { - self.data.pop().unwrap_unchecked() - } - *) - Definition pop_unsafe : - MS? t string U256 := - letS? result := pop in - match result with - | inl x => returnS? x - | inr _ => panicS? "Stack underflow" - end. - - (* - /// Peeks the top of the stack. - /// - /// # Safety - /// - /// The caller is responsible for checking the length of the stack. - #[inline] - pub unsafe fn top_unsafe(&mut self) -> &mut U256 { - let len = self.data.len(); - self.data.get_unchecked_mut(len - 1) - } - *) - Definition top_unsafe : - MS? t string U256 := - letS? '(data stack) := readS? in - match stack with - | [] => panicS? "Stack underflow" - | x :: _ => returnS? x - end. - - (* - /// Pop the topmost value, returning the value and the new topmost value. - /// - /// # Safety - /// - /// The caller is responsible for checking the length of the stack. - #[inline] - pub unsafe fn pop_top_unsafe(&mut self) -> (U256, &mut U256) { - let pop = self.pop_unsafe(); - let top = self.top_unsafe(); - (pop, top) - } - *) - Definition pop_top_unsafe : - MS? t string (U256 * U256) := - letS? pop := pop_unsafe in - letS? top := top_unsafe in - returnS? (pop, top). - - (* - /// Pops 2 values from the stack and returns them, in addition to the new topmost value. - /// - /// # Safety - /// - /// The caller is responsible for checking the length of the stack. - #[inline] - pub unsafe fn pop2_top_unsafe(&mut self) -> (U256, U256, &mut U256) { - let pop1 = self.pop_unsafe(); - let pop2 = self.pop_unsafe(); - let top = self.top_unsafe(); - - (pop1, pop2, top) - } - *) - Definition pop2_top_unsafe : - MS? t string (U256 * U256 * U256) := - letS? pop1 := pop_unsafe in - letS? pop2 := pop_unsafe in - letS? top := top_unsafe in - returnS? (pop1, pop2, top). -End Stack. - -(* - /// Function return frame. - /// Needed information for returning from a function. - #[derive(Debug, Default, Clone, Copy, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub struct FunctionReturnFrame { - /// The index of the code container that this frame is executing. - pub idx: usize, - /// The program counter where frame execution should continue. - pub pc: usize, - } -*) - -Module FunctionReturnFrame. - Record t : Set := { - idx : Z; - pc : Z; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter::function_return_frame::FunctionReturnFrame"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_interpreter::interpreter::function_return_frame::FunctionReturnFrame" [ - ("idx", φ x.(idx)); - ("pc", φ x.(pc)) - ]; - }. -End FunctionReturnFrame. - -(* - /// Function Stack - #[derive(Debug, Default)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub struct FunctionStack { - pub return_stack: Vec, - pub current_code_idx: usize, - } -*) - -(* TODO: Vectors? *) -Module FunctionStack. - Record t : Set := { - return_stack : list FunctionReturnFrame.t; - current_code_idx : Z; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter::function_stack::FunctionStack"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_interpreter::interpreter::function_stack::FunctionStack" [ - ("return_stack", φ x.(return_stack)); - ("current_code_idx", φ x.(current_code_idx)) - ]; - }. -End FunctionStack. - -(* - /// Call value. - #[derive(Clone, Debug, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub enum CallValue { - /// Concrete value, transferred from caller to callee at the end of the transaction. - Transfer(U256), - /// Apparent value, that is **not** actually transferred. - /// - /// Set when in a `DELEGATECALL` call type, and used by the `CALLVALUE` opcode. - Apparent(U256), - } -*) - -Module CallValue. - Inductive t : Set := - | Transfer : Z -> t - | Apparent : Z -> t. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter_action::call_inputs::CallValue"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - match x with - | Transfer x => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallValue::Transfer" [φ x] - | Apparent x => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallValue::Approval" [φ x] - end; - }. -End CallValue. - -(* - /// Call scheme. - #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub enum CallScheme { - /// `CALL`. - Call, - /// `CALLCODE` - CallCode, - /// `DELEGATECALL` - DelegateCall, - /// `STATICCALL` - StaticCall, - } -*) - -Module CallScheme. - Inductive t : Set := - | Call - | CallCode - | DelegateCall - | StaticCall. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter_action::call_inputs::CallScheme"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - match x with - | Call => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::Call" [] - | CallCode => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::CallCode" [] - | DelegateCall => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::DelegateCall" [] - | StaticCall => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::StaticCall" [] - end; - }. -End CallScheme. - -(* - /// Inputs for a call. - #[derive(Clone, Debug, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub struct CallInputs { - /// The call data of the call. - pub input: Bytes, - /// The return memory offset where the output of the call is written. - /// - /// In EOF, this range is invalid as EOF calls do not write output to memory. - pub return_memory_offset: Range, - /// The gas limit of the call. - pub gas_limit: u64, - /// The account address of bytecode that is going to be executed. - /// - /// Previously `context.code_address`. - pub bytecode_address: Address, - /// Target address, this account storage is going to be modified. - /// - /// Previously `context.address`. - pub target_address: Address, - /// This caller is invoking the call. - /// - /// Previously `context.caller`. - pub caller: Address, - /// Call value. - /// - /// NOTE: This value may not necessarily be transferred from caller to callee, see [`CallValue`]. - /// - /// Previously `transfer.value` or `context.apparent_value`. - pub value: CallValue, - /// The call scheme. - /// - /// Previously `context.scheme`. - pub scheme: CallScheme, - /// Whether the call is a static call, or is initiated inside a static call. - pub is_static: bool, - /// Whether the call is initiated from EOF bytecode. - pub is_eof: bool, - } -*) - -(* TODO: Ranges? *) -Module CallInputs. - Record t : Set := { - input : Bytes.t; - return_memory_offset : (Z * Z); - gas_limit : Z; - bytecode_address : Address.t; - target_address : Address.t; - caller : Address.t; - value : CallValue.t; - scheme : CallScheme.t; - is_static : bool; - is_eof : bool; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter::call_inputs::CallInputs"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_interpreter::interpreter::call_inputs::CallInputs" [ - ("input", φ x.(input)); - ("return_memory_offset", φ x.(return_memory_offset)); - ("gas_limit", φ x.(gas_limit)); - ("bytecode_address", φ x.(bytecode_address)); - ("target_address", φ x.(target_address)); - ("caller", φ x.(caller)); - ("value", φ x.(value)); - ("scheme", φ x.(scheme)); - ("is_static", φ x.(is_static)); - ("is_eof", φ x.(is_eof)) - ]; - }. -End CallInputs. - -(* - /// Create scheme. - #[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub enum CreateScheme { - /// Legacy create scheme of `CREATE`. - Create, - /// Create scheme of `CREATE2`. - Create2 { - /// Salt. - salt: U256, - }, - } -*) - -Module CreateScheme. - Inductive t : Set := - | Create - | Create2 : Z -> t. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_primitives::env::CreateScheme"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - match x with - | Create => Value.StructTuple "revm_primitives::env::CreateScheme::Create" [] - | Create2 x => Value.StructTuple "revm_primitives::env::CreateScheme::Create2" [φ x] - end; - }. -End CreateScheme. - -(* - /// Inputs for a create call. - #[derive(Clone, Debug, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub struct CreateInputs { - /// Caller address of the EVM. - pub caller: Address, - /// The create scheme. - pub scheme: CreateScheme, - /// The value to transfer. - pub value: U256, - /// The init code of the contract. - pub init_code: Bytes, - /// The gas limit of the call. - pub gas_limit: u64, - } -*) - -Module CreateInputs. - Record t : Set := { - caller : Address.t; - scheme : CreateScheme.t; - value : U256; - init_code : Bytes.t; - gas_limit : Z; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter::create_inputs::CreateInputs"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_interpreter::interpreter::create_inputs::CreateInputs" [ - ("caller", φ x.(caller)); - ("scheme", φ x.(scheme)); - ("value", φ x.(value)); - ("init_code", φ x.(init_code)); - ("gas_limit", φ x.(gas_limit)) - ]; - }. -End CreateInputs. - -(* - /// EOF Header containing - #[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub struct EofHeader { - /// Size of EOF types section. - /// types section includes num of input and outputs and max stack size. - pub types_size: u16, - /// Sizes of EOF code section. - /// Code size can't be zero. - pub code_sizes: Vec, - /// EOF Container size. - /// Container size can be zero. - pub container_sizes: Vec, - /// EOF data size. - pub data_size: u16, - /// sum code sizes - pub sum_code_sizes: usize, - /// sum container sizes - pub sum_container_sizes: usize, - } -*) - -Module EofHeader. - Record t : Set := { - types_size : Z; - code_sizes : list Z; - container_sizes : list Z; - data_size : Z; - sum_code_sizes : Z; - sum_container_sizes : Z; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_primitives::bytecode::eof::header::EofHeader"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_primitives::bytecode::eof::header::EofHeader" [ - ("types_size", φ x.(types_size)); - ("code_sizes", φ x.(code_sizes)); - ("container_sizes", φ x.(container_sizes)); - ("data_size", φ x.(data_size)); - ("sum_code_sizes", φ x.(sum_code_sizes)); - ("sum_container_sizes", φ x.(sum_container_sizes)) - ]; - }. -End EofHeader. - -(* - /// Types section that contains stack information for matching code section. - #[derive(Debug, Clone, Default, Hash, PartialEq, Eq, Copy)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub struct TypesSection { - /// inputs - 1 byte - `0x00-0x7F` - /// number of stack elements the code section consumes - pub inputs: u8, - /// outputs - 1 byte - `0x00-0x80` - /// number of stack elements the code section returns or 0x80 for non-returning functions - pub outputs: u8, - /// max_stack_height - 2 bytes - `0x0000-0x03FF` - /// maximum number of elements ever placed onto the stack by the code section - pub max_stack_size: u16, - } -*) - -Module TypesSection. - Record t : Set := { - inputs : Z; - outputs : Z; - max_stack_size : Z; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_primitives::bytecode::eof::types_section::TypesSection"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_primitives::bytecode::eof::types_section::TypesSection" [ - ("inputs", φ x.(inputs)); - ("outputs", φ x.(outputs)); - ("max_stack_size", φ x.(max_stack_size)) - ]; - }. -End TypesSection. - -(* - /// EOF Body, contains types, code, container and data sections. - /// - /// Can be used to create new EOF object. - #[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub struct EofBody { - pub types_section: Vec, - pub code_section: Vec, - pub container_section: Vec, - pub data_section: Bytes, - pub is_data_filled: bool, - } -*) - -Module EofBody. - Record t : Set := { - types_section : list TypesSection.t; - code_section : list Bytes.t; - container_section : list Bytes.t; - data_section : Bytes.t; - is_data_filled : bool; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_primitives::bytecode::eof::body::EofBody"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_primitives::bytecode::eof::body::EofBody" [ - ("types_section", φ x.(types_section)); - ("code_section", φ x.(code_section)); - ("container_section", φ x.(container_section)); - ("data_section", φ x.(data_section)); - ("is_data_filled", φ x.(is_data_filled)) - ]; - }. -End EofBody. - -(* - /// EOF - Ethereum Object Format. - /// - /// It consist of a header, body and raw original bytes Specified in EIP. - /// Most of body contain Bytes so it references to the raw bytes. - /// - /// If there is a need to create new EOF from scratch, it is recommended to use `EofBody` and - /// use `encode` function to create full [`Eof`] object. - #[derive(Clone, Debug, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub struct Eof { - pub header: EofHeader, - pub body: EofBody, - pub raw: Bytes, - } -*) - -Module Eof. - Record t : Set := { - header : EofHeader.t; - body : EofBody.t; - raw : Bytes.t; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_primitives::bytecode::eof::Eof"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_primitives::bytecode::eof::Eof" [ - ("header", φ x.(header)); - ("body", φ x.(body)); - ("raw", φ x.(raw)) - ]; - }. -End Eof. - -(* - /// Inputs for EOF create call. - #[derive(Debug, Default, Clone, PartialEq, Eq)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub struct EOFCreateInput { - /// Caller of Eof Craate - pub caller: Address, - /// New contract address. - pub created_address: Address, - /// Values of ether transfered - pub value: U256, - /// Init eof code that is going to be executed. - pub eof_init_code: Eof, - /// Gas limit for the create call. - pub gas_limit: u64, - /// Return memory range. If EOF creation Reverts it can return the - /// the memory range. - pub return_memory_range: Range, - } -*) - -Module EOFCreateInput. - Record t : Set := { - caller : Address.t; - created_address : Address.t; - value : U256; - eof_init_code : Eof.t; - gas_limit : Z; - return_memory_range : (Z * Z); - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter::eof_create_input::EOFCreateInput"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_interpreter::interpreter::eof_create_input::EOFCreateInput" [ - ("caller", φ x.(caller)); - ("created_address", φ x.(created_address)); - ("value", φ x.(value)); - ("eof_init_code", φ x.(eof_init_code)); - ("gas_limit", φ x.(gas_limit)); - ("return_memory_range", φ x.(return_memory_range)) - ]; - }. -End EOFCreateInput. - -(* - /// The result of an interpreter operation. - #[derive(Clone, Debug, PartialEq, Eq)] - #[cfg_attr(feature = "serde", derive(::serde::Serialize, ::serde::Deserialize))] - pub struct InterpreterResult { - /// The result of the instruction execution. - pub result: InstructionResult, - /// The output of the instruction execution. - pub output: Bytes, - /// The gas usage information. - pub gas: Gas, - } -*) - -Module InterpreterResult. - Record t : Set := { - result : InstructionResult.t; - output : Bytes.t; - gas : Gas.t; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter::InterpreterResult"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_interpreter::interpreter::InterpreterResult" [ - ("result", φ x.(result)); - ("output", φ x.(output)); - ("gas", φ x.(gas)) - ]; - }. -End InterpreterResult. - -(* - #[derive(Clone, Debug, Default, PartialEq, Eq)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub enum InterpreterAction { - /// CALL, CALLCODE, DELEGATECALL, STATICCALL - /// or EOF EXT instuction called. - Call { inputs: Box }, - /// CREATE or CREATE2 instruction called. - Create { inputs: Box }, - /// EOF CREATE instruction called. - EOFCreate { inputs: Box }, - /// Interpreter finished execution. - Return { result: InterpreterResult }, - /// No action - #[default] - None, - } -*) - -(* TODO: Box? *) -Module InterpreterAction. - Inductive t : Set := - | Call : CallInputs.t -> t - | Create : CreateInputs.t -> t - | EOFCreate : EOFCreateInput.t -> t - | Return : InterpreterResult.t -> t - | None. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter_action::InterpreterAction"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - match x with - | Call x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::Call" [("inputs", φ x)] - | Create x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::Create" [("inputs", φ x)] - | EOFCreate x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::EOFCreate" [("inputs", φ x)] - | Return x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::Return" [("result", φ x)] - | None => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::None" [] - end; - }. -End InterpreterAction. - -(* - /// EVM bytecode interpreter. - #[derive(Debug)] - pub struct Interpreter { - /// The current instruction pointer. - pub instruction_pointer: *const u8, - /// The gas state. - pub gas: Gas, - /// Contract information and invoking data - pub contract: Contract, - /// The execution control flag. If this is not set to `Continue`, the interpreter will stop - /// execution. - pub instruction_result: InstructionResult, - /// Currently run Bytecode that instruction result will point to. - /// Bytecode is owned by the contract. - pub bytecode: Bytes, - /// Whether we are Interpreting the Ethereum Object Format (EOF) bytecode. - /// This is local field that is set from `contract.is_eof()`. - pub is_eof: bool, - /// Is init flag for eof create - pub is_eof_init: bool, - /// Shared memory. - /// - /// Note: This field is only set while running the interpreter loop. - /// Otherwise it is taken and replaced with empty shared memory. - pub shared_memory: SharedMemory, - /// Stack. - pub stack: Stack, - /// EOF function stack. - pub function_stack: FunctionStack, - /// The return data buffer for internal calls. - /// It has multi usage: - /// - /// * It contains the output bytes of call sub call. - /// * When this interpreter finishes execution it contains the output bytes of this contract. - pub return_data_buffer: Bytes, - /// Whether the interpreter is in "staticcall" mode, meaning no state changes can happen. - pub is_static: bool, - /// Actions that the EVM should do. - /// - /// Set inside CALL or CREATE instructions and RETURN or REVERT instructions. Additionally those instructions will set - /// InstructionResult to CallOrCreate/Return/Revert so we know the reason. - pub next_action: InterpreterAction, - } -*) - -Module Interpreter. - Record t : Set := { - instruction_pointer : list Z; - gas : Gas.t; - contract : Contract.t; - instruction_result : InstructionResult.t; - Bytecode : Bytes.t; - IsEof : bool; - IsEofInit : bool; - SharedMemory : SharedMemory.t; - stack : Stack.t; - function_stack : FunctionStack.t; - return_data_buffer : Bytes.t; - is_static : bool; - next_action : InterpreterAction.t; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter::Interpreter"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_interpreter::interpreter::Interpreter" [ - ("instruction_pointer", φ x.(instruction_pointer)); - ("gas", φ x.(gas)); - ("contract", φ x.(contract)); - ("instruction_result", φ x.(instruction_result)); - ("Bytecode", φ x.(Bytecode)); - ("IsEof", φ x.(IsEof)); - ("IsEofInit", φ x.(IsEofInit)); - ("SharedMemory", φ x.(SharedMemory)); - ("stack", φ x.(stack)); - ("function_stack", φ x.(function_stack)); - ("return_data_buffer", φ x.(return_data_buffer)); - ("is_static", φ x.(is_static)); - ("next_action", φ x.(next_action)) - ]; - }. - - Definition update_gas - {A : Set} - (m : MS? Gas.t string A) : - MS? Interpreter.t string A := - letS? interp := readS? in - let gas := Interpreter.gas interp in - match m gas with - | (result, state) => - match result with - | inr e => panicS? e - | inl result => - letS? _ := writeS? (interp <| - Interpreter.gas := state - |>) in - returnS? result - end - end. -End Interpreter. - -(* - /// Records a `gas` cost and fails the instruction if it would exceed the available gas. - #[macro_export] - macro_rules! gas { - ($interp:expr, $gas:expr) => { - $crate::gas!($interp, $gas, ()) - }; - ($interp:expr, $gas:expr, $ret:expr) => { - if !$interp.gas.record_cost($gas) { - $interp.instruction_result = $crate::InstructionResult::OutOfGas; - return $ret; - } - }; - } -*) - -Definition gas_macro (gas : Z) : - MS? Interpreter.t string unit := - letS? interp := readS? in - letS? success := Interpreter.update_gas (Gas.record_cost gas) in - if negb success - then - letS? _ := writeS? (interp <| - Interpreter.instruction_result := InstructionResult.OutOfGas - |>) in - returnS? tt - else - returnS? tt. diff --git a/CoqOfRust/revm/simulations/dependencies.v b/CoqOfRust/revm/simulations/dependencies.v new file mode 100644 index 000000000..9101d7fa7 --- /dev/null +++ b/CoqOfRust/revm/simulations/dependencies.v @@ -0,0 +1,45 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. + +(* + /// Wrapper type around [`bytes::Bytes`] to support "0x" prefixed hex strings. + #[derive(Clone, Default, Hash, PartialEq, Eq, PartialOrd, Ord)] + #[repr(transparent)] + pub struct Bytes(pub bytes::Bytes); +*) + +Module Bytes. + Parameter t : Set. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "bytes::bytes::Bytes"; + }. + + Global Instance IsToValue : ToValue t. + Admitted. +End Bytes. + +Module Address. + Parameter t : Set. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "alloy_primitives::bits::address::Address"; + }. + + Global Instance IsToValue : ToValue t. + Admitted. +End Address. + +Module FixedBytes. + Parameter t : Set. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "alloy_primitives::bits::fixed::FixedBytes"; + }. + + Global Instance IsToValue : ToValue t. + Admitted. +End FixedBytes. + +Definition B256 := FixedBytes.t. +Definition U256 := FixedBytes.t. diff --git a/CoqOfRust/revm/simulations/interpreter/instructions/macros.v b/CoqOfRust/revm/simulations/interpreter/instructions/macros.v new file mode 100644 index 000000000..64149452c --- /dev/null +++ b/CoqOfRust/revm/simulations/interpreter/instructions/macros.v @@ -0,0 +1,35 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Import simulations.M.Notations. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter.gas. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter.instruction_result. + +(* + /// Records a `gas` cost and fails the instruction if it would exceed the available gas. + #[macro_export] + macro_rules! gas { + ($interp:expr, $gas:expr) => { + $crate::gas!($interp, $gas, ()) + }; + ($interp:expr, $gas:expr, $ret:expr) => { + if !$interp.gas.record_cost($gas) { + $interp.instruction_result = $crate::InstructionResult::OutOfGas; + return $ret; + } + }; + } +*) + +Definition gas_macro (gas : Z) : + MS? Interpreter.t string unit := + letS? interp := readS? in + letS? success := Interpreter.update_gas (Gas.record_cost gas) in + if negb success + then + letS? _ := writeS? (interp <| + Interpreter.instruction_result := InstructionResult.OutOfGas + |>) in + returnS? tt + else + returnS? tt. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter.v b/CoqOfRust/revm/simulations/interpreter/interpreter.v new file mode 100644 index 000000000..d0b06e61a --- /dev/null +++ b/CoqOfRust/revm/simulations/interpreter/interpreter.v @@ -0,0 +1,116 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Import simulations.M.Notations. +Require Import CoqOfRust.revm.simulations.dependencies. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter.instruction_result. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter.gas. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter.contract. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter.shared_memory. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter.stack. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter.function_stack. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter_action. + +(* + /// EVM bytecode interpreter. + #[derive(Debug)] + pub struct Interpreter { + /// The current instruction pointer. + pub instruction_pointer: *const u8, + /// The gas state. + pub gas: Gas, + /// Contract information and invoking data + pub contract: Contract, + /// The execution control flag. If this is not set to `Continue`, the interpreter will stop + /// execution. + pub instruction_result: InstructionResult, + /// Currently run Bytecode that instruction result will point to. + /// Bytecode is owned by the contract. + pub bytecode: Bytes, + /// Whether we are Interpreting the Ethereum Object Format (EOF) bytecode. + /// This is local field that is set from `contract.is_eof()`. + pub is_eof: bool, + /// Is init flag for eof create + pub is_eof_init: bool, + /// Shared memory. + /// + /// Note: This field is only set while running the interpreter loop. + /// Otherwise it is taken and replaced with empty shared memory. + pub shared_memory: SharedMemory, + /// Stack. + pub stack: Stack, + /// EOF function stack. + pub function_stack: FunctionStack, + /// The return data buffer for internal calls. + /// It has multi usage: + /// + /// * It contains the output bytes of call sub call. + /// * When this interpreter finishes execution it contains the output bytes of this contract. + pub return_data_buffer: Bytes, + /// Whether the interpreter is in "staticcall" mode, meaning no state changes can happen. + pub is_static: bool, + /// Actions that the EVM should do. + /// + /// Set inside CALL or CREATE instructions and RETURN or REVERT instructions. Additionally those instructions will set + /// InstructionResult to CallOrCreate/Return/Revert so we know the reason. + pub next_action: InterpreterAction, + } +*) + +Module Interpreter. + Record t : Set := { + instruction_pointer : list Z; + gas : Gas.t; + contract : Contract.t; + instruction_result : InstructionResult.t; + Bytecode : Bytes.t; + IsEof : bool; + IsEofInit : bool; + SharedMemory : SharedMemory.t; + stack : Stack.t; + function_stack : FunctionStack.t; + return_data_buffer : Bytes.t; + is_static : bool; + next_action : InterpreterAction.t; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::Interpreter"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::Interpreter" [ + ("instruction_pointer", φ x.(instruction_pointer)); + ("gas", φ x.(gas)); + ("contract", φ x.(contract)); + ("instruction_result", φ x.(instruction_result)); + ("Bytecode", φ x.(Bytecode)); + ("IsEof", φ x.(IsEof)); + ("IsEofInit", φ x.(IsEofInit)); + ("SharedMemory", φ x.(SharedMemory)); + ("stack", φ x.(stack)); + ("function_stack", φ x.(function_stack)); + ("return_data_buffer", φ x.(return_data_buffer)); + ("is_static", φ x.(is_static)); + ("next_action", φ x.(next_action)) + ]; + }. + + Definition update_gas + {A : Set} + (m : MS? Gas.t string A) : + MS? Interpreter.t string A := + letS? interp := readS? in + let gas := Interpreter.gas interp in + match m gas with + | (result, state) => + match result with + | inr e => panicS? e + | inl result => + letS? _ := writeS? (interp <| + Interpreter.gas := state + |>) in + returnS? result + end + end. +End Interpreter. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/contract.v b/CoqOfRust/revm/simulations/interpreter/interpreter/contract.v new file mode 100644 index 000000000..819e8f227 --- /dev/null +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/contract.v @@ -0,0 +1,53 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.core.simulations.option. +Require Import CoqOfRust.revm.simulations.dependencies. +Require Import CoqOfRust.revm.simulations.primitives.bytecode. + +(* + /// EVM contract information. + #[derive(Clone, Debug, Default)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct Contract { + /// Contracts data + pub input: Bytes, + /// Bytecode contains contract code, size of original code, analysis with gas block and jump table. + /// Note that current code is extended with push padding and STOP at end. + pub bytecode: Bytecode, + /// Bytecode hash for legacy. For EOF this would be None. + pub hash: Option, + /// Target address of the account. Storage of this address is going to be modified. + pub target_address: Address, + /// Caller of the EVM. + pub caller: Address, + /// Value send to contract from transaction or from CALL opcodes. + pub call_value: U256, + } +*) + +Module Contract. + Record t : Set := { + input : Bytes.t; + bytecode : Bytecode.t; + hash : option B256; + target_address : Address.t; + caller : Address.t; + call_value : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::contract::Contract"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::contract::Contract" [ + ("input", φ x.(input)); + ("bytecode", φ x.(bytecode)); + ("hash", φ x.(hash)); + ("target_address", φ x.(target_address)); + ("caller", φ x.(caller)); + ("call_value", φ x.(call_value)) + ]; + }. +End Contract. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/function_stack.v b/CoqOfRust/revm/simulations/interpreter/interpreter/function_stack.v new file mode 100644 index 000000000..d76dbc84e --- /dev/null +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/function_stack.v @@ -0,0 +1,65 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.core.simulations.array. + +(* + /// Function return frame. + /// Needed information for returning from a function. + #[derive(Debug, Default, Clone, Copy, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct FunctionReturnFrame { + /// The index of the code container that this frame is executing. + pub idx: usize, + /// The program counter where frame execution should continue. + pub pc: usize, + } +*) + +Module FunctionReturnFrame. + Record t : Set := { + idx : Z; + pc : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::function_return_frame::FunctionReturnFrame"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::function_return_frame::FunctionReturnFrame" [ + ("idx", φ x.(idx)); + ("pc", φ x.(pc)) + ]; + }. +End FunctionReturnFrame. + +(* + /// Function Stack + #[derive(Debug, Default)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct FunctionStack { + pub return_stack: Vec, + pub current_code_idx: usize, + } +*) + +(* TODO: Vectors? *) +Module FunctionStack. + Record t : Set := { + return_stack : list FunctionReturnFrame.t; + current_code_idx : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::function_stack::FunctionStack"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::function_stack::FunctionStack" [ + ("return_stack", φ x.(return_stack)); + ("current_code_idx", φ x.(current_code_idx)) + ]; + }. +End FunctionStack. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v b/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v new file mode 100644 index 000000000..fe8d9566c --- /dev/null +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v @@ -0,0 +1,66 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Import simulations.M.Notations. + +(* + /// Represents the state of gas during execution. + #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct Gas { + /// The initial gas limit. This is constant throughout execution. + limit: u64, + /// The remaining gas. + remaining: u64, + /// Refunded gas. This is used only at the end of execution. + refunded: i64, + } +*) + +Module Gas. + Record t : Set := { + limit : Z; + remaining : Z; + refunded : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::gas::Gas"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::gas::Gas" [ + ("limit", φ x.(limit)); + ("remaining", φ x.(remaining)); + ("refunded", φ x.(refunded)) + ]; + }. + + (* + /// Records an explicit cost. + /// + /// Returns `false` if the gas limit is exceeded. + #[inline] + #[must_use = "prefer using `gas!` instead to return an out-of-gas error on failure"] + pub fn record_cost(&mut self, cost: u64) -> bool { + let (remaining, overflow) = self.remaining.overflowing_sub(cost); + let success = !overflow; + if success { + self.remaining = remaining; + } + success + } + *) + Definition record_cost + (cost : Z) : + MS? t string bool := + letS? 'gas := readS? in + let remaining_sub_cost := gas.(remaining) - cost in + let success := remaining_sub_cost >=? 0 in + letS? _ := + if success + then writeS? (gas <| remaining := remaining_sub_cost |>) + else returnS? tt + in + returnS? success. +End Gas. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/instruction_result.v b/CoqOfRust/revm/simulations/interpreter/interpreter/instruction_result.v new file mode 100644 index 000000000..bb37deed0 --- /dev/null +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/instruction_result.v @@ -0,0 +1,145 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. + +(* + #[repr(u8)] + #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub enum InstructionResult { + // success codes + #[default] + Continue = 0x00, + Stop, + Return, + SelfDestruct, + ReturnContract, + + // revert codes + Revert = 0x10, // revert opcode + CallTooDeep, + OutOfFunds, + + // Actions + CallOrCreate = 0x20, + + // error codes + OutOfGas = 0x50, + MemoryOOG, + MemoryLimitOOG, + PrecompileOOG, + InvalidOperandOOG, + OpcodeNotFound, + CallNotAllowedInsideStatic, + StateChangeDuringStaticCall, + InvalidFEOpcode, + InvalidJump, + NotActivated, + StackUnderflow, + StackOverflow, + OutOfOffset, + CreateCollision, + OverflowPayment, + PrecompileError, + NonceOverflow, + /// Create init code size exceeds limit (runtime). + CreateContractSizeLimit, + /// Error on created contract that begins with EF + CreateContractStartingWithEF, + /// EIP-3860: Limit and meter initcode. Initcode size limit exceeded. + CreateInitCodeSizeLimit, + /// Fatal external error. Returned by database. + FatalExternalError, + /// RETURNCONTRACT called in not init eof code. + ReturnContractInNotInitEOF, + /// Legacy contract is calling opcode that is enabled only in EOF. + EOFOpcodeDisabledInLegacy, + /// EOF function stack overflow + EOFFunctionStackOverflow, + } +*) + +Module InstructionResult. + Inductive t : Set := + (* success codes *) + | Continue + | Stop + | Return + | SelfDestruct + | ReturnContract + (* revert codes *) + | Revert + | CallTooDeep + | OutOfFunds + (* Actions *) + | CallOrCreate + (* error codes *) + | OutOfGas + | MemoryOOG + | MemoryLimitOOG + | PrecompileOOG + | InvalidOperandOOG + | OpcodeNotFound + | CallNotAllowedInsideStatic + | StateChangeDuringStaticCall + | InvalidFEOpcode + | InvalidJump + | NotActivated + | StackUnderflow + | StackOverflow + | OutOfOffset + | CreateCollision + | OverflowPayment + | PrecompileError + | NonceOverflow + | CreateContractSizeLimit + | CreateContractStartingWithEF + | CreateInitCodeSizeLimit + | FatalExternalError + | ReturnContractInNotInitEOF + | EOFOpcodeDisabledInLegacy + | EOFFunctionStackOverflow. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::instruction_result::InstructionResult"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + match x with + | Continue => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Continue" [] + | Stop => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Stop" [] + | Return => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Return" [] + | SelfDestruct => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::SelfDestruct" [] + | ReturnContract => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::ReturnContract" [] + | Revert => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::Revert" [] + | CallTooDeep => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CallTooDeep" [] + | OutOfFunds => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OutOfFunds" [] + | CallOrCreate => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CallOrCreate" [] + | OutOfGas => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OutOfGas" [] + | MemoryOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::MemoryOOG" [] + | MemoryLimitOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::MemoryLimitOOG" [] + | PrecompileOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::PrecompileOOG" [] + | InvalidOperandOOG => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG" [] + | OpcodeNotFound => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OpcodeNotFound" [] + | CallNotAllowedInsideStatic => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CallNotAllowedInsideStatic" [] + | StateChangeDuringStaticCall => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::StateChangeDuringStaticCall" [] + | InvalidFEOpcode => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::InvalidFEOpcode" [] + | InvalidJump => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::InvalidJump" [] + | NotActivated => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::NotActivated" [] + | StackUnderflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::StackUnderflow" [] + | StackOverflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::StackOverflow" [] + | OutOfOffset => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OutOfOffset" [] + | CreateCollision => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateCollision" [] + | OverflowPayment => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::OverflowPayment" [] + | PrecompileError => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::PrecompileError" [] + | NonceOverflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::NonceOverflow" [] + | CreateContractSizeLimit => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateContractSizeLimit" [] + | CreateContractStartingWithEF => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateContractStartingWithEF" [] + | CreateInitCodeSizeLimit => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::CreateInitCodeSizeLimit" [] + | FatalExternalError => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::FatalExternalError" [] + | ReturnContractInNotInitEOF => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::ReturnContractInNotInitEOF" [] + | EOFOpcodeDisabledInLegacy => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::EOFOpcodeDisabledInLegacy" [] + | EOFFunctionStackOverflow => Value.StructTuple "revm_interpreter::instruction_result::InstructionResult::EOFFunctionStackOverflow" [] + end; + }. +End InstructionResult. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/shared_memory.v b/CoqOfRust/revm/simulations/interpreter/interpreter/shared_memory.v new file mode 100644 index 000000000..93379555b --- /dev/null +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/shared_memory.v @@ -0,0 +1,48 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.core.simulations.option. +Require Import CoqOfRust.core.simulations.array. + +(* + /// A sequential memory shared between calls, which uses + /// a `Vec` for internal representation. + /// A [SharedMemory] instance should always be obtained using + /// the `new` static method to ensure memory safety. + #[derive(Clone, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct SharedMemory { + /// The underlying buffer. + buffer: Vec, + /// Memory checkpoints for each depth. + /// Invariant: these are always in bounds of `data`. + checkpoints: Vec, + /// Invariant: equals `self.checkpoints.last()` + last_checkpoint: usize, + /// Memory limit. See [`CfgEnv`](revm_primitives::CfgEnv). + #[cfg(feature = "memory_limit")] + memory_limit: u64, + } +*) + +Module SharedMemory. + Record t : Set := { + buffer : list Z; + checkpoints : list Z; + last_checkpoint : Z; + memory_limit : option Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::shared_memory::SharedMemory"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::shared_memory::SharedMemory" [ + ("buffer", φ x.(buffer)); + ("checkpoints", φ x.(checkpoints)); + ("last_checkpoint", φ x.(last_checkpoint)); + ("memory_limit", φ x.(memory_limit)) + ]; + }. +End SharedMemory. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v b/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v new file mode 100644 index 000000000..3d9fdbee0 --- /dev/null +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v @@ -0,0 +1,138 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Import simulations.M.Notations. +Require Import CoqOfRust.core.simulations.array. +Require Import CoqOfRust.revm.simulations.dependencies. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter.instruction_result. + +(* + /// EVM stack with [STACK_LIMIT] capacity of words. + #[derive(Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize))] + pub struct Stack { + /// The underlying data of the stack. + data: Vec, + } +*) + +Module Stack. + Inductive t : Set := + | data : list U256 -> t. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::stack::Stack"; + }. + + Global Instance IsToValue : ToValue t := { + φ '(data x) := + Value.StructRecord "revm_interpreter::interpreter::stack::Stack" [("data", φ x)] + }. + + (* + /// Returns the length of the stack in words. + #[inline] + pub fn len(&self) -> usize { + self.data.len() + } + *) + Definition len '(data stack) : Z := + Z.of_nat (List.length stack). + + (* + /// Removes the topmost element from the stack and returns it, or `StackUnderflow` if it is + /// empty. + #[inline] + pub fn pop(&mut self) -> Result { + self.data.pop().ok_or(InstructionResult::StackUnderflow) + } + *) + Definition pop : + MS? t string (U256 + InstructionResult.t) := + letS? '(data stack) := readS? in + match stack with + | [] => returnS? (inr InstructionResult.StackUnderflow) + | x :: xs => + letS? _ := writeS? (data xs) in + returnS? (inl x) + end. + + (* + /// Removes the topmost element from the stack and returns it. + /// + /// # Safety + /// + /// The caller is responsible for checking the length of the stack. + #[inline] + pub unsafe fn pop_unsafe(&mut self) -> U256 { + self.data.pop().unwrap_unchecked() + } + *) + Definition pop_unsafe : + MS? t string U256 := + letS? result := pop in + match result with + | inl x => returnS? x + | inr _ => panicS? "Stack underflow" + end. + + (* + /// Peeks the top of the stack. + /// + /// # Safety + /// + /// The caller is responsible for checking the length of the stack. + #[inline] + pub unsafe fn top_unsafe(&mut self) -> &mut U256 { + let len = self.data.len(); + self.data.get_unchecked_mut(len - 1) + } + *) + Definition top_unsafe : + MS? t string U256 := + letS? '(data stack) := readS? in + match stack with + | [] => panicS? "Stack underflow" + | x :: _ => returnS? x + end. + + (* + /// Pop the topmost value, returning the value and the new topmost value. + /// + /// # Safety + /// + /// The caller is responsible for checking the length of the stack. + #[inline] + pub unsafe fn pop_top_unsafe(&mut self) -> (U256, &mut U256) { + let pop = self.pop_unsafe(); + let top = self.top_unsafe(); + (pop, top) + } + *) + Definition pop_top_unsafe : + MS? t string (U256 * U256) := + letS? pop := pop_unsafe in + letS? top := top_unsafe in + returnS? (pop, top). + + (* + /// Pops 2 values from the stack and returns them, in addition to the new topmost value. + /// + /// # Safety + /// + /// The caller is responsible for checking the length of the stack. + #[inline] + pub unsafe fn pop2_top_unsafe(&mut self) -> (U256, U256, &mut U256) { + let pop1 = self.pop_unsafe(); + let pop2 = self.pop_unsafe(); + let top = self.top_unsafe(); + + (pop1, pop2, top) + } + *) + Definition pop2_top_unsafe : + MS? t string (U256 * U256 * U256) := + letS? pop1 := pop_unsafe in + letS? pop2 := pop_unsafe in + letS? top := top_unsafe in + returnS? (pop1, pop2, top). +End Stack. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter_action.v b/CoqOfRust/revm/simulations/interpreter/interpreter_action.v new file mode 100644 index 000000000..0dfc5f872 --- /dev/null +++ b/CoqOfRust/revm/simulations/interpreter/interpreter_action.v @@ -0,0 +1,87 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.revm.simulations.dependencies. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter_action.call_inputs. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter_action.create_inputs. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter_action.eof_create_inputs. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter.instruction_result. +Require Import CoqOfRust.revm.simulations.interpreter.interpreter.gas. + +(* + /// The result of an interpreter operation. + #[derive(Clone, Debug, PartialEq, Eq)] + #[cfg_attr(feature = "serde", derive(::serde::Serialize, ::serde::Deserialize))] + pub struct InterpreterResult { + /// The result of the instruction execution. + pub result: InstructionResult, + /// The output of the instruction execution. + pub output: Bytes, + /// The gas usage information. + pub gas: Gas, + } +*) + +Module InterpreterResult. + Record t : Set := { + result : InstructionResult.t; + output : Bytes.t; + gas : Gas.t; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::InterpreterResult"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::InterpreterResult" [ + ("result", φ x.(result)); + ("output", φ x.(output)); + ("gas", φ x.(gas)) + ]; + }. +End InterpreterResult. + +(* + #[derive(Clone, Debug, Default, PartialEq, Eq)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub enum InterpreterAction { + /// CALL, CALLCODE, DELEGATECALL, STATICCALL + /// or EOF EXT instuction called. + Call { inputs: Box }, + /// CREATE or CREATE2 instruction called. + Create { inputs: Box }, + /// EOF CREATE instruction called. + EOFCreate { inputs: Box }, + /// Interpreter finished execution. + Return { result: InterpreterResult }, + /// No action + #[default] + None, + } +*) + +(* TODO: Box? *) +Module InterpreterAction. + Inductive t : Set := + | Call : CallInputs.t -> t + | Create : CreateInputs.t -> t + | EOFCreate : EOFCreateInput.t -> t + | Return : InterpreterResult.t -> t + | None. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter_action::InterpreterAction"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + match x with + | Call x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::Call" [("inputs", φ x)] + | Create x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::Create" [("inputs", φ x)] + | EOFCreate x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::EOFCreate" [("inputs", φ x)] + | Return x => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::Return" [("result", φ x)] + | None => Value.StructRecord "revm_interpreter::interpreter_action::InterpreterAction::None" [] + end; + }. +End InterpreterAction. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter_action/call_inputs.v b/CoqOfRust/revm/simulations/interpreter/interpreter_action/call_inputs.v new file mode 100644 index 000000000..eec530be5 --- /dev/null +++ b/CoqOfRust/revm/simulations/interpreter/interpreter_action/call_inputs.v @@ -0,0 +1,153 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.core.simulations.bool. +Require Import CoqOfRust.revm.simulations.dependencies. + +(* + /// Call value. + #[derive(Clone, Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub enum CallValue { + /// Concrete value, transferred from caller to callee at the end of the transaction. + Transfer(U256), + /// Apparent value, that is **not** actually transferred. + /// + /// Set when in a `DELEGATECALL` call type, and used by the `CALLVALUE` opcode. + Apparent(U256), + } +*) + +Module CallValue. + Inductive t : Set := + | Transfer : Z -> t + | Apparent : Z -> t. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter_action::call_inputs::CallValue"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + match x with + | Transfer x => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallValue::Transfer" [φ x] + | Apparent x => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallValue::Approval" [φ x] + end; + }. +End CallValue. + +(* + /// Call scheme. + #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub enum CallScheme { + /// `CALL`. + Call, + /// `CALLCODE` + CallCode, + /// `DELEGATECALL` + DelegateCall, + /// `STATICCALL` + StaticCall, + } +*) + +Module CallScheme. + Inductive t : Set := + | Call + | CallCode + | DelegateCall + | StaticCall. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter_action::call_inputs::CallScheme"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + match x with + | Call => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::Call" [] + | CallCode => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::CallCode" [] + | DelegateCall => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::DelegateCall" [] + | StaticCall => Value.StructTuple "revm_interpreter::interpreter_action::call_inputs::CallScheme::StaticCall" [] + end; + }. +End CallScheme. + + +(* + /// Inputs for a call. + #[derive(Clone, Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct CallInputs { + /// The call data of the call. + pub input: Bytes, + /// The return memory offset where the output of the call is written. + /// + /// In EOF, this range is invalid as EOF calls do not write output to memory. + pub return_memory_offset: Range, + /// The gas limit of the call. + pub gas_limit: u64, + /// The account address of bytecode that is going to be executed. + /// + /// Previously `context.code_address`. + pub bytecode_address: Address, + /// Target address, this account storage is going to be modified. + /// + /// Previously `context.address`. + pub target_address: Address, + /// This caller is invoking the call. + /// + /// Previously `context.caller`. + pub caller: Address, + /// Call value. + /// + /// NOTE: This value may not necessarily be transferred from caller to callee, see [`CallValue`]. + /// + /// Previously `transfer.value` or `context.apparent_value`. + pub value: CallValue, + /// The call scheme. + /// + /// Previously `context.scheme`. + pub scheme: CallScheme, + /// Whether the call is a static call, or is initiated inside a static call. + pub is_static: bool, + /// Whether the call is initiated from EOF bytecode. + pub is_eof: bool, + } +*) + +(* TODO: Ranges? *) +Module CallInputs. + Record t : Set := { + input : Bytes.t; + return_memory_offset : (Z * Z); + gas_limit : Z; + bytecode_address : Address.t; + target_address : Address.t; + caller : Address.t; + value : CallValue.t; + scheme : CallScheme.t; + is_static : bool; + is_eof : bool; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::call_inputs::CallInputs"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::call_inputs::CallInputs" [ + ("input", φ x.(input)); + ("return_memory_offset", φ x.(return_memory_offset)); + ("gas_limit", φ x.(gas_limit)); + ("bytecode_address", φ x.(bytecode_address)); + ("target_address", φ x.(target_address)); + ("caller", φ x.(caller)); + ("value", φ x.(value)); + ("scheme", φ x.(scheme)); + ("is_static", φ x.(is_static)); + ("is_eof", φ x.(is_eof)) + ]; + }. +End CallInputs. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter_action/create_inputs.v b/CoqOfRust/revm/simulations/interpreter/interpreter_action/create_inputs.v new file mode 100644 index 000000000..072328ae0 --- /dev/null +++ b/CoqOfRust/revm/simulations/interpreter/interpreter_action/create_inputs.v @@ -0,0 +1,47 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.revm.simulations.dependencies. +Require Import CoqOfRust.revm.simulations.primitives.env. + +(* + /// Inputs for a create call. + #[derive(Clone, Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct CreateInputs { + /// Caller address of the EVM. + pub caller: Address, + /// The create scheme. + pub scheme: CreateScheme, + /// The value to transfer. + pub value: U256, + /// The init code of the contract. + pub init_code: Bytes, + /// The gas limit of the call. + pub gas_limit: u64, + } +*) + +Module CreateInputs. + Record t : Set := { + caller : Address.t; + scheme : CreateScheme.t; + value : U256; + init_code : Bytes.t; + gas_limit : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::create_inputs::CreateInputs"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::create_inputs::CreateInputs" [ + ("caller", φ x.(caller)); + ("scheme", φ x.(scheme)); + ("value", φ x.(value)); + ("init_code", φ x.(init_code)); + ("gas_limit", φ x.(gas_limit)) + ]; + }. +End CreateInputs. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter_action/eof_create_inputs.v b/CoqOfRust/revm/simulations/interpreter/interpreter_action/eof_create_inputs.v new file mode 100644 index 000000000..186e3bb48 --- /dev/null +++ b/CoqOfRust/revm/simulations/interpreter/interpreter_action/eof_create_inputs.v @@ -0,0 +1,52 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.revm.simulations.dependencies. +Require Import CoqOfRust.revm.simulations.primitives.bytecode.eof. + +(* + /// Inputs for EOF create call. + #[derive(Debug, Default, Clone, PartialEq, Eq)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct EOFCreateInput { + /// Caller of Eof Craate + pub caller: Address, + /// New contract address. + pub created_address: Address, + /// Values of ether transfered + pub value: U256, + /// Init eof code that is going to be executed. + pub eof_init_code: Eof, + /// Gas limit for the create call. + pub gas_limit: u64, + /// Return memory range. If EOF creation Reverts it can return the + /// the memory range. + pub return_memory_range: Range, + } +*) + +Module EOFCreateInput. + Record t : Set := { + caller : Address.t; + created_address : Address.t; + value : U256; + eof_init_code : Eof.t; + gas_limit : Z; + return_memory_range : (Z * Z); + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::eof_create_input::EOFCreateInput"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::eof_create_input::EOFCreateInput" [ + ("caller", φ x.(caller)); + ("created_address", φ x.(created_address)); + ("value", φ x.(value)); + ("eof_init_code", φ x.(eof_init_code)); + ("gas_limit", φ x.(gas_limit)); + ("return_memory_range", φ x.(return_memory_range)) + ]; + }. +End EOFCreateInput. diff --git a/CoqOfRust/revm/simulations/primitives/bytecode.v b/CoqOfRust/revm/simulations/primitives/bytecode.v new file mode 100644 index 000000000..9dbbb75d2 --- /dev/null +++ b/CoqOfRust/revm/simulations/primitives/bytecode.v @@ -0,0 +1,27 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. + +(* + /// State of the [`Bytecode`] analysis. + #[derive(Clone, Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub enum Bytecode { + /// No analysis has been performed. + LegacyRaw(Bytes), + /// The bytecode has been analyzed for valid jump destinations. + LegacyAnalyzed(LegacyAnalyzedBytecode), + /// Ethereum Object Format + Eof(Eof), + } +*) + +Module Bytecode. + Parameter t : Set. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_primitives::bytecode::Bytecode"; + }. + + Global Instance IsToValue : ToValue t. + Admitted. +End Bytecode. diff --git a/CoqOfRust/revm/simulations/primitives/bytecode/eof.v b/CoqOfRust/revm/simulations/primitives/bytecode/eof.v new file mode 100644 index 000000000..e4b7d6a2b --- /dev/null +++ b/CoqOfRust/revm/simulations/primitives/bytecode/eof.v @@ -0,0 +1,43 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.revm.simulations.dependencies. +Require Import CoqOfRust.revm.simulations.primitives.bytecode.eof.header. +Require Import CoqOfRust.revm.simulations.primitives.bytecode.eof.body. + +(* + /// EOF - Ethereum Object Format. + /// + /// It consist of a header, body and raw original bytes Specified in EIP. + /// Most of body contain Bytes so it references to the raw bytes. + /// + /// If there is a need to create new EOF from scratch, it is recommended to use `EofBody` and + /// use `encode` function to create full [`Eof`] object. + #[derive(Clone, Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct Eof { + pub header: EofHeader, + pub body: EofBody, + pub raw: Bytes, + } +*) + +Module Eof. + Record t : Set := { + header : EofHeader.t; + body : EofBody.t; + raw : Bytes.t; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_primitives::bytecode::eof::Eof"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_primitives::bytecode::eof::Eof" [ + ("header", φ x.(header)); + ("body", φ x.(body)); + ("raw", φ x.(raw)) + ]; + }. +End Eof. diff --git a/CoqOfRust/revm/simulations/primitives/bytecode/eof/body.v b/CoqOfRust/revm/simulations/primitives/bytecode/eof/body.v new file mode 100644 index 000000000..f9276adad --- /dev/null +++ b/CoqOfRust/revm/simulations/primitives/bytecode/eof/body.v @@ -0,0 +1,46 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.core.simulations.bool. +Require Import CoqOfRust.core.simulations.array. +Require Import CoqOfRust.revm.simulations.dependencies. +Require Import CoqOfRust.revm.simulations.primitives.bytecode.eof.type_section. + +(* + /// EOF Body, contains types, code, container and data sections. + /// + /// Can be used to create new EOF object. + #[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct EofBody { + pub types_section: Vec, + pub code_section: Vec, + pub container_section: Vec, + pub data_section: Bytes, + pub is_data_filled: bool, + } +*) + +Module EofBody. + Record t : Set := { + types_section : list TypesSection.t; + code_section : list Bytes.t; + container_section : list Bytes.t; + data_section : Bytes.t; + is_data_filled : bool; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_primitives::bytecode::eof::body::EofBody"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_primitives::bytecode::eof::body::EofBody" [ + ("types_section", φ x.(types_section)); + ("code_section", φ x.(code_section)); + ("container_section", φ x.(container_section)); + ("data_section", φ x.(data_section)); + ("is_data_filled", φ x.(is_data_filled)) + ]; + }. +End EofBody. diff --git a/CoqOfRust/revm/simulations/primitives/bytecode/eof/header.v b/CoqOfRust/revm/simulations/primitives/bytecode/eof/header.v new file mode 100644 index 000000000..32c693c55 --- /dev/null +++ b/CoqOfRust/revm/simulations/primitives/bytecode/eof/header.v @@ -0,0 +1,53 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.core.simulations.array. + +(* + /// EOF Header containing + #[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct EofHeader { + /// Size of EOF types section. + /// types section includes num of input and outputs and max stack size. + pub types_size: u16, + /// Sizes of EOF code section. + /// Code size can't be zero. + pub code_sizes: Vec, + /// EOF Container size. + /// Container size can be zero. + pub container_sizes: Vec, + /// EOF data size. + pub data_size: u16, + /// sum code sizes + pub sum_code_sizes: usize, + /// sum container sizes + pub sum_container_sizes: usize, + } +*) + +Module EofHeader. + Record t : Set := { + types_size : Z; + code_sizes : list Z; + container_sizes : list Z; + data_size : Z; + sum_code_sizes : Z; + sum_container_sizes : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_primitives::bytecode::eof::header::EofHeader"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_primitives::bytecode::eof::header::EofHeader" [ + ("types_size", φ x.(types_size)); + ("code_sizes", φ x.(code_sizes)); + ("container_sizes", φ x.(container_sizes)); + ("data_size", φ x.(data_size)); + ("sum_code_sizes", φ x.(sum_code_sizes)); + ("sum_container_sizes", φ x.(sum_container_sizes)) + ]; + }. +End EofHeader. diff --git a/CoqOfRust/revm/simulations/primitives/bytecode/eof/type_section.v b/CoqOfRust/revm/simulations/primitives/bytecode/eof/type_section.v new file mode 100644 index 000000000..d07f7c346 --- /dev/null +++ b/CoqOfRust/revm/simulations/primitives/bytecode/eof/type_section.v @@ -0,0 +1,40 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. + +(* + /// Types section that contains stack information for matching code section. + #[derive(Debug, Clone, Default, Hash, PartialEq, Eq, Copy)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct TypesSection { + /// inputs - 1 byte - `0x00-0x7F` + /// number of stack elements the code section consumes + pub inputs: u8, + /// outputs - 1 byte - `0x00-0x80` + /// number of stack elements the code section returns or 0x80 for non-returning functions + pub outputs: u8, + /// max_stack_height - 2 bytes - `0x0000-0x03FF` + /// maximum number of elements ever placed onto the stack by the code section + pub max_stack_size: u16, + } +*) + +Module TypesSection. + Record t : Set := { + inputs : Z; + outputs : Z; + max_stack_size : Z; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_primitives::bytecode::eof::types_section::TypesSection"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_primitives::bytecode::eof::types_section::TypesSection" [ + ("inputs", φ x.(inputs)); + ("outputs", φ x.(outputs)); + ("max_stack_size", φ x.(max_stack_size)) + ]; + }. +End TypesSection. diff --git a/CoqOfRust/revm/simulations/primitives/env.v b/CoqOfRust/revm/simulations/primitives/env.v new file mode 100644 index 000000000..a5aa90429 --- /dev/null +++ b/CoqOfRust/revm/simulations/primitives/env.v @@ -0,0 +1,35 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.simulations.M. + +(* + /// Create scheme. + #[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub enum CreateScheme { + /// Legacy create scheme of `CREATE`. + Create, + /// Create scheme of `CREATE2`. + Create2 { + /// Salt. + salt: U256, + }, + } +*) + +Module CreateScheme. + Inductive t : Set := + | Create + | Create2 : Z -> t. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_primitives::env::CreateScheme"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + match x with + | Create => Value.StructTuple "revm_primitives::env::CreateScheme::Create" [] + | Create2 x => Value.StructTuple "revm_primitives::env::CreateScheme::Create2" [φ x] + end; + }. +End CreateScheme. From 87dc12f10d1a20b8325cd9b013d46e38663bf979 Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Tue, 4 Jun 2024 10:09:21 +0000 Subject: [PATCH 07/14] change the type of the `instruction_pointer` field --- CoqOfRust/revm/simulations/interpreter/interpreter.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter.v b/CoqOfRust/revm/simulations/interpreter/interpreter.v index d0b06e61a..be68a30b6 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter.v @@ -58,7 +58,7 @@ Require Import CoqOfRust.revm.simulations.interpreter.interpreter_action. Module Interpreter. Record t : Set := { - instruction_pointer : list Z; + instruction_pointer : Z; gas : Gas.t; contract : Contract.t; instruction_result : InstructionResult.t; From ff002f79cac8b8ad3c29be39936795517c89e281 Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Tue, 4 Jun 2024 14:41:05 +0000 Subject: [PATCH 08/14] core simulations - fix imports --- CoqOfRust/core/simulations/array.v | 4 +--- CoqOfRust/core/simulations/bool.v | 1 + CoqOfRust/core/simulations/option.v | 1 + CoqOfRust/core/simulations/result.v | 4 +--- 4 files changed, 4 insertions(+), 6 deletions(-) diff --git a/CoqOfRust/core/simulations/array.v b/CoqOfRust/core/simulations/array.v index 7971006bf..bacf9844d 100644 --- a/CoqOfRust/core/simulations/array.v +++ b/CoqOfRust/core/simulations/array.v @@ -1,7 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import simulations.M. -Require CoqOfRust.core.simulations.default. -Import simulations.M.Notations. +Require Import links.M. Module Array. Global Instance IsToTy (A : Set) (_ : ToTy A) : ToTy (list A) := { diff --git a/CoqOfRust/core/simulations/bool.v b/CoqOfRust/core/simulations/bool.v index 67bfb402b..0b5906148 100644 --- a/CoqOfRust/core/simulations/bool.v +++ b/CoqOfRust/core/simulations/bool.v @@ -1,4 +1,5 @@ Require Import Coq.Strings.String. +Require Import links.M. Require Import CoqOfRust.simulations.M. Require Import CoqOfRust.lib.lib. Import simulations.M.Notations. diff --git a/CoqOfRust/core/simulations/option.v b/CoqOfRust/core/simulations/option.v index f52f6644e..5b323449f 100644 --- a/CoqOfRust/core/simulations/option.v +++ b/CoqOfRust/core/simulations/option.v @@ -1,4 +1,5 @@ Require Import CoqOfRust.CoqOfRust. +Require Import links.M. Require Import simulations.M. Require CoqOfRust.core.simulations.default. Import simulations.M.Notations. diff --git a/CoqOfRust/core/simulations/result.v b/CoqOfRust/core/simulations/result.v index e0505baa1..5cc49360b 100644 --- a/CoqOfRust/core/simulations/result.v +++ b/CoqOfRust/core/simulations/result.v @@ -1,7 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import simulations.M. -Require CoqOfRust.core.simulations.default. -Import simulations.M.Notations. +Require Import links.M. Module Result. Global Instance IsToTy (A B : Set) (_ : ToTy A) (_ : ToTy B) : ToTy (A + B) := { From 86147fcab79568a98502d4f7bf40807adc3375fa Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Tue, 4 Jun 2024 14:41:31 +0000 Subject: [PATCH 09/14] REVM simulations - fix imports --- CoqOfRust/revm/simulations/dependencies.v | 2 +- CoqOfRust/revm/simulations/interpreter/instructions/macros.v | 1 + CoqOfRust/revm/simulations/interpreter/interpreter.v | 1 + CoqOfRust/revm/simulations/interpreter/interpreter/contract.v | 2 +- .../revm/simulations/interpreter/interpreter/function_stack.v | 2 +- CoqOfRust/revm/simulations/interpreter/interpreter/gas.v | 1 + .../simulations/interpreter/interpreter/instruction_result.v | 2 +- .../revm/simulations/interpreter/interpreter/shared_memory.v | 2 +- CoqOfRust/revm/simulations/interpreter/interpreter/stack.v | 1 + CoqOfRust/revm/simulations/interpreter/interpreter_action.v | 2 +- .../simulations/interpreter/interpreter_action/call_inputs.v | 2 +- .../simulations/interpreter/interpreter_action/create_inputs.v | 2 +- .../interpreter/interpreter_action/eof_create_inputs.v | 2 +- CoqOfRust/revm/simulations/primitives/bytecode.v | 2 +- CoqOfRust/revm/simulations/primitives/bytecode/eof.v | 2 +- CoqOfRust/revm/simulations/primitives/bytecode/eof/body.v | 2 +- CoqOfRust/revm/simulations/primitives/bytecode/eof/header.v | 2 +- .../revm/simulations/primitives/bytecode/eof/type_section.v | 3 ++- CoqOfRust/revm/simulations/primitives/env.v | 2 +- 19 files changed, 20 insertions(+), 15 deletions(-) diff --git a/CoqOfRust/revm/simulations/dependencies.v b/CoqOfRust/revm/simulations/dependencies.v index 9101d7fa7..fbcf48c70 100644 --- a/CoqOfRust/revm/simulations/dependencies.v +++ b/CoqOfRust/revm/simulations/dependencies.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. (* /// Wrapper type around [`bytes::Bytes`] to support "0x" prefixed hex strings. diff --git a/CoqOfRust/revm/simulations/interpreter/instructions/macros.v b/CoqOfRust/revm/simulations/interpreter/instructions/macros.v index 64149452c..e7dfce5a9 100644 --- a/CoqOfRust/revm/simulations/interpreter/instructions/macros.v +++ b/CoqOfRust/revm/simulations/interpreter/instructions/macros.v @@ -1,4 +1,5 @@ Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.simulations.M. Import simulations.M.Notations. Require Import CoqOfRust.revm.simulations.interpreter.interpreter. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter.v b/CoqOfRust/revm/simulations/interpreter/interpreter.v index be68a30b6..8e534f122 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter.v @@ -1,4 +1,5 @@ Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.simulations.M. Import simulations.M.Notations. Require Import CoqOfRust.revm.simulations.dependencies. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/contract.v b/CoqOfRust/revm/simulations/interpreter/interpreter/contract.v index 819e8f227..186156bbb 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter/contract.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/contract.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.core.simulations.option. Require Import CoqOfRust.revm.simulations.dependencies. Require Import CoqOfRust.revm.simulations.primitives.bytecode. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/function_stack.v b/CoqOfRust/revm/simulations/interpreter/interpreter/function_stack.v index d76dbc84e..fcf692c8f 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter/function_stack.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/function_stack.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.core.simulations.array. (* diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v b/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v index fe8d9566c..594797e10 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v @@ -1,4 +1,5 @@ Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.simulations.M. Import simulations.M.Notations. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/instruction_result.v b/CoqOfRust/revm/simulations/interpreter/interpreter/instruction_result.v index bb37deed0..60732ec68 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter/instruction_result.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/instruction_result.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. (* #[repr(u8)] diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/shared_memory.v b/CoqOfRust/revm/simulations/interpreter/interpreter/shared_memory.v index 93379555b..2dfd40741 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter/shared_memory.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/shared_memory.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.core.simulations.option. Require Import CoqOfRust.core.simulations.array. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v b/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v index 3d9fdbee0..4cf5b5830 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v @@ -1,4 +1,5 @@ Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.simulations.M. Import simulations.M.Notations. Require Import CoqOfRust.core.simulations.array. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter_action.v b/CoqOfRust/revm/simulations/interpreter/interpreter_action.v index 0dfc5f872..0bcf87eed 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter_action.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter_action.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.revm.simulations.dependencies. Require Import CoqOfRust.revm.simulations.interpreter.interpreter_action.call_inputs. Require Import CoqOfRust.revm.simulations.interpreter.interpreter_action.create_inputs. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter_action/call_inputs.v b/CoqOfRust/revm/simulations/interpreter/interpreter_action/call_inputs.v index eec530be5..9f886f5d1 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter_action/call_inputs.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter_action/call_inputs.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.core.simulations.bool. Require Import CoqOfRust.revm.simulations.dependencies. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter_action/create_inputs.v b/CoqOfRust/revm/simulations/interpreter/interpreter_action/create_inputs.v index 072328ae0..34e980b15 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter_action/create_inputs.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter_action/create_inputs.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.revm.simulations.dependencies. Require Import CoqOfRust.revm.simulations.primitives.env. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter_action/eof_create_inputs.v b/CoqOfRust/revm/simulations/interpreter/interpreter_action/eof_create_inputs.v index 186e3bb48..c7b7291ce 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter_action/eof_create_inputs.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter_action/eof_create_inputs.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.revm.simulations.dependencies. Require Import CoqOfRust.revm.simulations.primitives.bytecode.eof. diff --git a/CoqOfRust/revm/simulations/primitives/bytecode.v b/CoqOfRust/revm/simulations/primitives/bytecode.v index 9dbbb75d2..44c7335fe 100644 --- a/CoqOfRust/revm/simulations/primitives/bytecode.v +++ b/CoqOfRust/revm/simulations/primitives/bytecode.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. (* /// State of the [`Bytecode`] analysis. diff --git a/CoqOfRust/revm/simulations/primitives/bytecode/eof.v b/CoqOfRust/revm/simulations/primitives/bytecode/eof.v index e4b7d6a2b..f2c39990d 100644 --- a/CoqOfRust/revm/simulations/primitives/bytecode/eof.v +++ b/CoqOfRust/revm/simulations/primitives/bytecode/eof.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.revm.simulations.dependencies. Require Import CoqOfRust.revm.simulations.primitives.bytecode.eof.header. Require Import CoqOfRust.revm.simulations.primitives.bytecode.eof.body. diff --git a/CoqOfRust/revm/simulations/primitives/bytecode/eof/body.v b/CoqOfRust/revm/simulations/primitives/bytecode/eof/body.v index f9276adad..73476cb39 100644 --- a/CoqOfRust/revm/simulations/primitives/bytecode/eof/body.v +++ b/CoqOfRust/revm/simulations/primitives/bytecode/eof/body.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.core.simulations.bool. Require Import CoqOfRust.core.simulations.array. Require Import CoqOfRust.revm.simulations.dependencies. diff --git a/CoqOfRust/revm/simulations/primitives/bytecode/eof/header.v b/CoqOfRust/revm/simulations/primitives/bytecode/eof/header.v index 32c693c55..eb4958f44 100644 --- a/CoqOfRust/revm/simulations/primitives/bytecode/eof/header.v +++ b/CoqOfRust/revm/simulations/primitives/bytecode/eof/header.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. Require Import CoqOfRust.core.simulations.array. (* diff --git a/CoqOfRust/revm/simulations/primitives/bytecode/eof/type_section.v b/CoqOfRust/revm/simulations/primitives/bytecode/eof/type_section.v index d07f7c346..77468e67a 100644 --- a/CoqOfRust/revm/simulations/primitives/bytecode/eof/type_section.v +++ b/CoqOfRust/revm/simulations/primitives/bytecode/eof/type_section.v @@ -1,5 +1,6 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. + (* /// Types section that contains stack information for matching code section. diff --git a/CoqOfRust/revm/simulations/primitives/env.v b/CoqOfRust/revm/simulations/primitives/env.v index a5aa90429..0dd9cdd7e 100644 --- a/CoqOfRust/revm/simulations/primitives/env.v +++ b/CoqOfRust/revm/simulations/primitives/env.v @@ -1,5 +1,5 @@ Require Import CoqOfRust.CoqOfRust. -Require Import CoqOfRust.simulations.M. +Require Import CoqOfRust.links.M. (* /// Create scheme. From 8a968db05b9b1919753294fbad537a31d6502ff8 Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Thu, 6 Jun 2024 15:45:31 +0000 Subject: [PATCH 10/14] core - sepearate links and simulations --- CoqOfRust/core/{simulations => links}/array.v | 0 CoqOfRust/core/links/bool.v | 13 +++++++++++++ CoqOfRust/core/links/option.v | 16 ++++++++++++++++ CoqOfRust/core/{simulations => links}/result.v | 0 CoqOfRust/core/simulations/bool.v | 10 ---------- CoqOfRust/core/simulations/option.v | 15 --------------- 6 files changed, 29 insertions(+), 25 deletions(-) rename CoqOfRust/core/{simulations => links}/array.v (100%) create mode 100644 CoqOfRust/core/links/bool.v create mode 100644 CoqOfRust/core/links/option.v rename CoqOfRust/core/{simulations => links}/result.v (100%) diff --git a/CoqOfRust/core/simulations/array.v b/CoqOfRust/core/links/array.v similarity index 100% rename from CoqOfRust/core/simulations/array.v rename to CoqOfRust/core/links/array.v diff --git a/CoqOfRust/core/links/bool.v b/CoqOfRust/core/links/bool.v new file mode 100644 index 000000000..9dd256bda --- /dev/null +++ b/CoqOfRust/core/links/bool.v @@ -0,0 +1,13 @@ +Require Import Coq.Strings.String. +Require Import links.M. +Require Import CoqOfRust.lib.lib. + +Module Bool. + Global Instance IsToTy : ToTy bool := { + Φ := Ty.path "bool"; + }. + + Global Instance IsToValue : ToValue bool := { + φ := Value.Bool; + }. +End Bool. diff --git a/CoqOfRust/core/links/option.v b/CoqOfRust/core/links/option.v new file mode 100644 index 000000000..3e9c5b2a9 --- /dev/null +++ b/CoqOfRust/core/links/option.v @@ -0,0 +1,16 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import links.M. + +Module Option. + Global Instance IsToTy (A : Set) (_ : ToTy A) : ToTy (option A) := { + Φ := Ty.apply (Ty.path "core::option::Option") [Φ A]; + }. + + Global Instance IsToValue (A : Set) (_ : ToValue A) : ToValue (option A) := { + φ x := + match x with + | None => Value.StructTuple "core::option::Option::None" [] + | Some x => Value.StructTuple "core::option::Option::Some" [φ x] + end; + }. +End Option. diff --git a/CoqOfRust/core/simulations/result.v b/CoqOfRust/core/links/result.v similarity index 100% rename from CoqOfRust/core/simulations/result.v rename to CoqOfRust/core/links/result.v diff --git a/CoqOfRust/core/simulations/bool.v b/CoqOfRust/core/simulations/bool.v index 0b5906148..200feba74 100644 --- a/CoqOfRust/core/simulations/bool.v +++ b/CoqOfRust/core/simulations/bool.v @@ -1,18 +1,8 @@ Require Import Coq.Strings.String. -Require Import links.M. Require Import CoqOfRust.simulations.M. -Require Import CoqOfRust.lib.lib. Import simulations.M.Notations. Module Bool. - Global Instance IsToTy : ToTy bool := { - Φ := Ty.path "bool"; - }. - - Global Instance IsToValue : ToValue bool := { - φ := Value.Bool; - }. - Definition and {State Error} (x y : MS? State Error bool) : MS? State Error bool := letS? a := x in if negb a diff --git a/CoqOfRust/core/simulations/option.v b/CoqOfRust/core/simulations/option.v index 5b323449f..123753d72 100644 --- a/CoqOfRust/core/simulations/option.v +++ b/CoqOfRust/core/simulations/option.v @@ -1,23 +1,8 @@ Require Import CoqOfRust.CoqOfRust. -Require Import links.M. Require Import simulations.M. Require CoqOfRust.core.simulations.default. Import simulations.M.Notations. -Module Option. - Global Instance IsToTy (A : Set) (_ : ToTy A) : ToTy (option A) := { - Φ := Ty.apply (Ty.path "core::option::Option") [Φ A]; - }. - - Global Instance IsToValue (A : Set) (_ : ToValue A) : ToValue (option A) := { - φ x := - match x with - | None => Value.StructTuple "core::option::Option::None" [] - | Some x => Value.StructTuple "core::option::Option::Some" [φ x] - end; - }. -End Option. - Module Impl_Option_T. Definition Self (T : Set) : Set := option T. From d943126f978ec7158546d7f1ccf33f3983d124bf Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Thu, 6 Jun 2024 15:45:53 +0000 Subject: [PATCH 11/14] REVM - separate links and simulations --- .github/workflows/rust.yml | 8 +- CoqOfRust/blacklist.txt | 4 +- .../{simulations => links}/dependencies.v | 0 .../revm/links/interpreter/interpreter.v | 97 +++++++++++++++++ .../interpreter/interpreter/contract.v | 6 +- .../interpreter/interpreter/function_stack.v | 2 +- .../interpreter/interpreter}/gas.v | 15 ++- .../interpreter/instruction_result.v | 0 .../interpreter/interpreter/shared_memory.v | 4 +- .../links/interpreter/interpreter/stack.v | 28 +++++ .../interpreter/interpreter_action.v | 12 +-- .../interpreter_action/call_inputs.v | 4 +- .../interpreter_action/create_inputs.v | 4 +- .../interpreter_action/eof_create_inputs.v | 4 +- .../primitives/bytecode.v | 0 .../primitives/bytecode/eof.v | 6 +- .../primitives/bytecode/eof/body.v | 8 +- .../primitives/bytecode/eof/header.v | 2 +- .../primitives/bytecode/eof/type_section.v | 0 .../{simulations => links}/primitives/env.v | 0 .../interpreter/instructions/macros.v | 5 +- .../simulations/interpreter/interpreter.v | 101 ++---------------- .../simulations/interpreter/interpreter/gas.v | 40 +------ .../interpreter/interpreter/stack.v | 45 +++----- .../interpreter/function_stack.v | 0 .../revm/{ => translations}/interpreter/gas.v | 0 .../{ => translations}/interpreter/gas/calc.v | 0 .../interpreter/gas/constants.v | 0 .../{ => translations}/interpreter/host.v | 0 .../interpreter/host/dummy.v | 0 .../interpreter/instruction_result.v | 0 .../interpreter/instructions/arithmetic.v | 0 .../interpreter/instructions/bitwise.v | 0 .../interpreter/instructions/contract.v | 0 .../instructions/contract/call_helpers.v | 0 .../interpreter/instructions/control.v | 0 .../interpreter/instructions/data.v | 0 .../interpreter/instructions/host.v | 0 .../interpreter/instructions/host_env.v | 0 .../interpreter/instructions/i256.v | 0 .../interpreter/instructions/memory.v | 0 .../interpreter/instructions/stack.v | 0 .../interpreter/instructions/system.v | 0 .../interpreter/instructions/utility.v | 0 .../interpreter/interpreter.v | 0 .../interpreter/interpreter/analysis.v | 0 .../interpreter/interpreter/contract.v | 0 .../interpreter/interpreter/shared_memory.v | 0 .../interpreter/interpreter/stack.v | 0 .../interpreter/interpreter_action.v | 0 .../interpreter_action/call_inputs.v | 0 .../interpreter_action/call_outcome.v | 0 .../interpreter_action/create_inputs.v | 0 .../interpreter_action/create_outcome.v | 0 .../interpreter_action/eof_create_inputs.v | 0 .../interpreter_action/eof_create_outcome.v | 0 .../{ => translations}/interpreter/opcode.v | 0 .../interpreter/opcode/eof_printer.v | 0 .../{ => translations}/precompile/blake2.v | 0 .../{ => translations}/precompile/bn128.v | 0 .../revm/{ => translations}/precompile/hash.v | 0 .../{ => translations}/precompile/identity.v | 0 .../precompile/kzg_point_evaluation.v | 0 .../revm/{ => translations}/precompile/lib.v | 0 .../{ => translations}/precompile/modexp.v | 0 .../{ => translations}/precompile/secp256k1.v | 0 .../{ => translations}/precompile/utilities.v | 0 .../{ => translations}/primitives/bytecode.v | 0 .../primitives/bytecode/eof.v | 0 .../primitives/bytecode/eof/body.v | 0 .../primitives/bytecode/eof/decode_helpers.v | 0 .../primitives/bytecode/eof/header.v | 0 .../primitives/bytecode/eof/types_section.v | 0 .../primitives/bytecode/legacy.v | 0 .../primitives/bytecode/legacy/jump_map.v | 0 .../{ => translations}/primitives/constants.v | 0 .../revm/{ => translations}/primitives/db.v | 0 .../primitives/db/components.v | 0 .../primitives/db/components/block_hash.v | 0 .../primitives/db/components/state.v | 0 .../revm/{ => translations}/primitives/env.v | 0 .../primitives/env/handler_cfg.v | 0 .../primitives/kzg/env_settings.v | 0 .../primitives/kzg/trusted_setup_points.v | 0 .../primitives/precompile.v | 0 .../{ => translations}/primitives/result.v | 0 .../primitives/specification.v | 0 .../{ => translations}/primitives/state.v | 0 .../{ => translations}/primitives/utilities.v | 0 .../revm/{ => translations}/revm/builder.v | 0 .../revm/{ => translations}/revm/context.v | 0 .../revm/context/context_precompiles.v | 0 .../revm/context/evm_context.v | 0 .../revm/context/inner_evm_context.v | 0 .../revm/{ => translations}/revm/db/emptydb.v | 0 .../{ => translations}/revm/db/in_memory_db.v | 0 .../revm/db/states/account_status.v | 0 .../revm/db/states/bundle_account.v | 0 .../revm/db/states/bundle_state.v | 0 .../{ => translations}/revm/db/states/cache.v | 0 .../revm/db/states/cache_account.v | 0 .../revm/db/states/changes.v | 0 .../revm/db/states/plain_account.v | 0 .../revm/db/states/reverts.v | 0 .../{ => translations}/revm/db/states/state.v | 0 .../revm/db/states/state_builder.v | 0 .../revm/db/states/transition_account.v | 0 .../revm/db/states/transition_state.v | 0 CoqOfRust/revm/{ => translations}/revm/evm.v | 0 .../revm/{ => translations}/revm/frame.v | 0 .../revm/{ => translations}/revm/handler.v | 0 .../revm/handler/handle_types/execution.v | 0 .../handler/handle_types/post_execution.v | 0 .../revm/handler/handle_types/pre_execution.v | 0 .../revm/handler/handle_types/validation.v | 0 .../revm/handler/mainnet/execution.v | 0 .../revm/handler/mainnet/post_execution.v | 0 .../revm/handler/mainnet/pre_execution.v | 0 .../revm/handler/mainnet/validation.v | 0 .../revm/handler/register.v | 0 .../revm/{ => translations}/revm/inspector.v | 0 .../revm/inspector/customprinter.v | 0 .../{ => translations}/revm/inspector/gas.v | 0 .../revm/inspector/handler_register.v | 0 .../{ => translations}/revm/inspector/noop.v | 0 .../{ => translations}/revm/journaled_state.v | 0 126 files changed, 197 insertions(+), 198 deletions(-) rename CoqOfRust/revm/{simulations => links}/dependencies.v (100%) create mode 100644 CoqOfRust/revm/links/interpreter/interpreter.v rename CoqOfRust/revm/{simulations => links}/interpreter/interpreter/contract.v (90%) rename CoqOfRust/revm/{simulations => links}/interpreter/interpreter/function_stack.v (97%) rename CoqOfRust/revm/{interpreter/links => links/interpreter/interpreter}/gas.v (96%) rename CoqOfRust/revm/{simulations => links}/interpreter/interpreter/instruction_result.v (100%) rename CoqOfRust/revm/{simulations => links}/interpreter/interpreter/shared_memory.v (93%) create mode 100644 CoqOfRust/revm/links/interpreter/interpreter/stack.v rename CoqOfRust/revm/{simulations => links}/interpreter/interpreter_action.v (84%) rename CoqOfRust/revm/{simulations => links}/interpreter/interpreter_action/call_inputs.v (97%) rename CoqOfRust/revm/{simulations => links}/interpreter/interpreter_action/create_inputs.v (91%) rename CoqOfRust/revm/{simulations => links}/interpreter/interpreter_action/eof_create_inputs.v (92%) rename CoqOfRust/revm/{simulations => links}/primitives/bytecode.v (100%) rename CoqOfRust/revm/{simulations => links}/primitives/bytecode/eof.v (84%) rename CoqOfRust/revm/{simulations => links}/primitives/bytecode/eof/body.v (84%) rename CoqOfRust/revm/{simulations => links}/primitives/bytecode/eof/header.v (96%) rename CoqOfRust/revm/{simulations => links}/primitives/bytecode/eof/type_section.v (100%) rename CoqOfRust/revm/{simulations => links}/primitives/env.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/function_stack.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/gas.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/gas/calc.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/gas/constants.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/host.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/host/dummy.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instruction_result.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instructions/arithmetic.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instructions/bitwise.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instructions/contract.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instructions/contract/call_helpers.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instructions/control.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instructions/data.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instructions/host.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instructions/host_env.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instructions/i256.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instructions/memory.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instructions/stack.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instructions/system.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/instructions/utility.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/interpreter.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/interpreter/analysis.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/interpreter/contract.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/interpreter/shared_memory.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/interpreter/stack.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/interpreter_action.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/interpreter_action/call_inputs.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/interpreter_action/call_outcome.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/interpreter_action/create_inputs.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/interpreter_action/create_outcome.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/interpreter_action/eof_create_inputs.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/interpreter_action/eof_create_outcome.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/opcode.v (100%) rename CoqOfRust/revm/{ => translations}/interpreter/opcode/eof_printer.v (100%) rename CoqOfRust/revm/{ => translations}/precompile/blake2.v (100%) rename CoqOfRust/revm/{ => translations}/precompile/bn128.v (100%) rename CoqOfRust/revm/{ => translations}/precompile/hash.v (100%) rename CoqOfRust/revm/{ => translations}/precompile/identity.v (100%) rename CoqOfRust/revm/{ => translations}/precompile/kzg_point_evaluation.v (100%) rename CoqOfRust/revm/{ => translations}/precompile/lib.v (100%) rename CoqOfRust/revm/{ => translations}/precompile/modexp.v (100%) rename CoqOfRust/revm/{ => translations}/precompile/secp256k1.v (100%) rename CoqOfRust/revm/{ => translations}/precompile/utilities.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/bytecode.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/bytecode/eof.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/bytecode/eof/body.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/bytecode/eof/decode_helpers.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/bytecode/eof/header.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/bytecode/eof/types_section.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/bytecode/legacy.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/bytecode/legacy/jump_map.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/constants.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/db.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/db/components.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/db/components/block_hash.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/db/components/state.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/env.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/env/handler_cfg.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/kzg/env_settings.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/kzg/trusted_setup_points.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/precompile.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/result.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/specification.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/state.v (100%) rename CoqOfRust/revm/{ => translations}/primitives/utilities.v (100%) rename CoqOfRust/revm/{ => translations}/revm/builder.v (100%) rename CoqOfRust/revm/{ => translations}/revm/context.v (100%) rename CoqOfRust/revm/{ => translations}/revm/context/context_precompiles.v (100%) rename CoqOfRust/revm/{ => translations}/revm/context/evm_context.v (100%) rename CoqOfRust/revm/{ => translations}/revm/context/inner_evm_context.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/emptydb.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/in_memory_db.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/states/account_status.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/states/bundle_account.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/states/bundle_state.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/states/cache.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/states/cache_account.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/states/changes.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/states/plain_account.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/states/reverts.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/states/state.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/states/state_builder.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/states/transition_account.v (100%) rename CoqOfRust/revm/{ => translations}/revm/db/states/transition_state.v (100%) rename CoqOfRust/revm/{ => translations}/revm/evm.v (100%) rename CoqOfRust/revm/{ => translations}/revm/frame.v (100%) rename CoqOfRust/revm/{ => translations}/revm/handler.v (100%) rename CoqOfRust/revm/{ => translations}/revm/handler/handle_types/execution.v (100%) rename CoqOfRust/revm/{ => translations}/revm/handler/handle_types/post_execution.v (100%) rename CoqOfRust/revm/{ => translations}/revm/handler/handle_types/pre_execution.v (100%) rename CoqOfRust/revm/{ => translations}/revm/handler/handle_types/validation.v (100%) rename CoqOfRust/revm/{ => translations}/revm/handler/mainnet/execution.v (100%) rename CoqOfRust/revm/{ => translations}/revm/handler/mainnet/post_execution.v (100%) rename CoqOfRust/revm/{ => translations}/revm/handler/mainnet/pre_execution.v (100%) rename CoqOfRust/revm/{ => translations}/revm/handler/mainnet/validation.v (100%) rename CoqOfRust/revm/{ => translations}/revm/handler/register.v (100%) rename CoqOfRust/revm/{ => translations}/revm/inspector.v (100%) rename CoqOfRust/revm/{ => translations}/revm/inspector/customprinter.v (100%) rename CoqOfRust/revm/{ => translations}/revm/inspector/gas.v (100%) rename CoqOfRust/revm/{ => translations}/revm/inspector/handler_register.v (100%) rename CoqOfRust/revm/{ => translations}/revm/inspector/noop.v (100%) rename CoqOfRust/revm/{ => translations}/revm/journaled_state.v (100%) diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 82098ef96..c38a23411 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -86,28 +86,28 @@ jobs: cargo coq-of-rust touch src/lib.rs cargo coq-of-rust - rsync -av src/ ../../../../CoqOfRust/revm/interpreter/ --include='*/' --include='*.v' --exclude='*' + rsync -av src/ ../../../../CoqOfRust/revm/translations/interpreter/ --include='*/' --include='*.v' --exclude='*' cd .. # precompile cd precompile cargo coq-of-rust touch src/lib.rs cargo coq-of-rust - rsync -av src/ ../../../../CoqOfRust/revm/precompile/ --include='*/' --include='*.v' --exclude='*' + rsync -av src/ ../../../../CoqOfRust/revm/translations/precompile/ --include='*/' --include='*.v' --exclude='*' cd .. # primitives cd primitives cargo coq-of-rust touch src/lib.rs cargo coq-of-rust - rsync -av src/ ../../../../CoqOfRust/revm/primitives/ --include='*/' --include='*.v' --exclude='*' + rsync -av src/ ../../../../CoqOfRust/revm/translations/primitives/ --include='*/' --include='*.v' --exclude='*' cd .. # revm cd revm cargo coq-of-rust touch src/lib.rs cargo coq-of-rust - rsync -av src/ ../../../../CoqOfRust/revm/revm/ --include='*/' --include='*.v' --exclude='*' + rsync -av src/ ../../../../CoqOfRust/revm/translations/revm/ --include='*/' --include='*.v' --exclude='*' cd .. cd ../../.. endGroup diff --git a/CoqOfRust/blacklist.txt b/CoqOfRust/blacklist.txt index b0737bdab..a48700014 100644 --- a/CoqOfRust/blacklist.txt +++ b/CoqOfRust/blacklist.txt @@ -2,9 +2,9 @@ examples/default/examples/ink_contracts/proofs/erc20.v examples/default/examples/ink_contracts/proofs/lib.v examples/default/examples/ink_contracts/simulations/erc20.v examples/default/examples/ink_contracts/simulations/erc721.v -revm/precompile/utilities.v +revm/translations/precompile/utilities.v # This file works but is taking a very long time (ten minutes) -revm/interpreter/opcode.v +revm/translations/interpreter/opcode.v examples/default/examples/ink_contracts/proofs/erc721.v move/ core/any.v diff --git a/CoqOfRust/revm/simulations/dependencies.v b/CoqOfRust/revm/links/dependencies.v similarity index 100% rename from CoqOfRust/revm/simulations/dependencies.v rename to CoqOfRust/revm/links/dependencies.v diff --git a/CoqOfRust/revm/links/interpreter/interpreter.v b/CoqOfRust/revm/links/interpreter/interpreter.v new file mode 100644 index 000000000..d6d1726fe --- /dev/null +++ b/CoqOfRust/revm/links/interpreter/interpreter.v @@ -0,0 +1,97 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import CoqOfRust.revm.links.dependencies. +Require Import CoqOfRust.revm.links.interpreter.interpreter.instruction_result. +Require Import CoqOfRust.revm.links.interpreter.interpreter.gas. +Require Import CoqOfRust.revm.links.interpreter.interpreter.contract. +Require Import CoqOfRust.revm.links.interpreter.interpreter.shared_memory. +Require Import CoqOfRust.revm.links.interpreter.interpreter.stack. +Require Import CoqOfRust.revm.links.interpreter.interpreter.function_stack. +Require Import CoqOfRust.revm.links.interpreter.interpreter_action. + +(* + /// EVM bytecode interpreter. + #[derive(Debug)] + pub struct Interpreter { + /// The current instruction pointer. + pub instruction_pointer: *const u8, + /// The gas state. + pub gas: Gas, + /// Contract information and invoking data + pub contract: Contract, + /// The execution control flag. If this is not set to `Continue`, the interpreter will stop + /// execution. + pub instruction_result: InstructionResult, + /// Currently run Bytecode that instruction result will point to. + /// Bytecode is owned by the contract. + pub bytecode: Bytes, + /// Whether we are Interpreting the Ethereum Object Format (EOF) bytecode. + /// This is local field that is set from `contract.is_eof()`. + pub is_eof: bool, + /// Is init flag for eof create + pub is_eof_init: bool, + /// Shared memory. + /// + /// Note: This field is only set while running the interpreter loop. + /// Otherwise it is taken and replaced with empty shared memory. + pub shared_memory: SharedMemory, + /// Stack. + pub stack: Stack, + /// EOF function stack. + pub function_stack: FunctionStack, + /// The return data buffer for internal calls. + /// It has multi usage: + /// + /// * It contains the output bytes of call sub call. + /// * When this interpreter finishes execution it contains the output bytes of this contract. + pub return_data_buffer: Bytes, + /// Whether the interpreter is in "staticcall" mode, meaning no state changes can happen. + pub is_static: bool, + /// Actions that the EVM should do. + /// + /// Set inside CALL or CREATE instructions and RETURN or REVERT instructions. Additionally those instructions will set + /// InstructionResult to CallOrCreate/Return/Revert so we know the reason. + pub next_action: InterpreterAction, + } +*) + +Module Interpreter. + Record t : Set := { + instruction_pointer : Z; + gas : Gas.t; + contract : Contract.t; + instruction_result : InstructionResult.t; + Bytecode : Bytes.t; + IsEof : bool; + IsEofInit : bool; + SharedMemory : SharedMemory.t; + stack : Stack.t; + function_stack : FunctionStack.t; + return_data_buffer : Bytes.t; + is_static : bool; + next_action : InterpreterAction.t; + }. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::Interpreter"; + }. + + Global Instance IsToValue : ToValue t := { + φ x := + Value.StructRecord "revm_interpreter::interpreter::Interpreter" [ + ("instruction_pointer", φ x.(instruction_pointer)); + ("gas", φ x.(gas)); + ("contract", φ x.(contract)); + ("instruction_result", φ x.(instruction_result)); + ("Bytecode", φ x.(Bytecode)); + ("IsEof", φ x.(IsEof)); + ("IsEofInit", φ x.(IsEofInit)); + ("SharedMemory", φ x.(SharedMemory)); + ("stack", φ x.(stack)); + ("function_stack", φ x.(function_stack)); + ("return_data_buffer", φ x.(return_data_buffer)); + ("is_static", φ x.(is_static)); + ("next_action", φ x.(next_action)) + ]; + }. +End Interpreter. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/contract.v b/CoqOfRust/revm/links/interpreter/interpreter/contract.v similarity index 90% rename from CoqOfRust/revm/simulations/interpreter/interpreter/contract.v rename to CoqOfRust/revm/links/interpreter/interpreter/contract.v index 186156bbb..284d144d2 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter/contract.v +++ b/CoqOfRust/revm/links/interpreter/interpreter/contract.v @@ -1,8 +1,8 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. -Require Import CoqOfRust.core.simulations.option. -Require Import CoqOfRust.revm.simulations.dependencies. -Require Import CoqOfRust.revm.simulations.primitives.bytecode. +Require Import CoqOfRust.core.links.option. +Require Import CoqOfRust.revm.links.dependencies. +Require Import CoqOfRust.revm.links.primitives.bytecode. (* /// EVM contract information. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/function_stack.v b/CoqOfRust/revm/links/interpreter/interpreter/function_stack.v similarity index 97% rename from CoqOfRust/revm/simulations/interpreter/interpreter/function_stack.v rename to CoqOfRust/revm/links/interpreter/interpreter/function_stack.v index fcf692c8f..398d0a914 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter/function_stack.v +++ b/CoqOfRust/revm/links/interpreter/interpreter/function_stack.v @@ -1,6 +1,6 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. -Require Import CoqOfRust.core.simulations.array. +Require Import CoqOfRust.core.links.array. (* /// Function return frame. diff --git a/CoqOfRust/revm/interpreter/links/gas.v b/CoqOfRust/revm/links/interpreter/interpreter/gas.v similarity index 96% rename from CoqOfRust/revm/interpreter/links/gas.v rename to CoqOfRust/revm/links/interpreter/interpreter/gas.v index 18cd9d4bc..d0ebcee13 100644 --- a/CoqOfRust/revm/interpreter/links/gas.v +++ b/CoqOfRust/revm/links/interpreter/interpreter/gas.v @@ -1,19 +1,25 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. Require core.links.clone. -Require Import revm.interpreter.gas. +Require Import revm.translations.interpreter.gas. Import Run. -Module Gas. - (* pub struct Gas { +(* + /// Represents the state of gas during execution. + #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] + pub struct Gas { /// The initial gas limit. This is constant throughout execution. limit: u64, /// The remaining gas. remaining: u64, /// Refunded gas. This is used only at the end of execution. refunded: i64, - } *) + } +*) + +Module Gas. Record t : Set := { limit : Z; remaining : Z; @@ -33,6 +39,7 @@ Module Gas. ]; }. + Module SubPointer. Definition get_limit : SubPointer.Runner.t t Z := {| SubPointer.Runner.index := diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/instruction_result.v b/CoqOfRust/revm/links/interpreter/interpreter/instruction_result.v similarity index 100% rename from CoqOfRust/revm/simulations/interpreter/interpreter/instruction_result.v rename to CoqOfRust/revm/links/interpreter/interpreter/instruction_result.v diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/shared_memory.v b/CoqOfRust/revm/links/interpreter/interpreter/shared_memory.v similarity index 93% rename from CoqOfRust/revm/simulations/interpreter/interpreter/shared_memory.v rename to CoqOfRust/revm/links/interpreter/interpreter/shared_memory.v index 2dfd40741..77140c79d 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter/shared_memory.v +++ b/CoqOfRust/revm/links/interpreter/interpreter/shared_memory.v @@ -1,7 +1,7 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. -Require Import CoqOfRust.core.simulations.option. -Require Import CoqOfRust.core.simulations.array. +Require Import CoqOfRust.core.links.option. +Require Import CoqOfRust.core.links.array. (* /// A sequential memory shared between calls, which uses diff --git a/CoqOfRust/revm/links/interpreter/interpreter/stack.v b/CoqOfRust/revm/links/interpreter/interpreter/stack.v new file mode 100644 index 000000000..7725d9a97 --- /dev/null +++ b/CoqOfRust/revm/links/interpreter/interpreter/stack.v @@ -0,0 +1,28 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import CoqOfRust.core.links.array. +Require Import CoqOfRust.revm.links.dependencies. + +(* + /// EVM stack with [STACK_LIMIT] capacity of words. + #[derive(Debug, PartialEq, Eq, Hash)] + #[cfg_attr(feature = "serde", derive(serde::Serialize))] + pub struct Stack { + /// The underlying data of the stack. + data: Vec, + } +*) + +Module Stack. + Inductive t : Set := + | data : list U256 -> t. + + Global Instance IsToTy : ToTy t := { + Φ := Ty.path "revm_interpreter::interpreter::stack::Stack"; + }. + + Global Instance IsToValue : ToValue t := { + φ '(data x) := + Value.StructRecord "revm_interpreter::interpreter::stack::Stack" [("data", φ x)] + }. +End Stack. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter_action.v b/CoqOfRust/revm/links/interpreter/interpreter_action.v similarity index 84% rename from CoqOfRust/revm/simulations/interpreter/interpreter_action.v rename to CoqOfRust/revm/links/interpreter/interpreter_action.v index 0bcf87eed..4234a8bcd 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter_action.v +++ b/CoqOfRust/revm/links/interpreter/interpreter_action.v @@ -1,11 +1,11 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. -Require Import CoqOfRust.revm.simulations.dependencies. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter_action.call_inputs. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter_action.create_inputs. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter_action.eof_create_inputs. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter.instruction_result. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter.gas. +Require Import CoqOfRust.revm.links.dependencies. +Require Import CoqOfRust.revm.links.interpreter.interpreter_action.call_inputs. +Require Import CoqOfRust.revm.links.interpreter.interpreter_action.create_inputs. +Require Import CoqOfRust.revm.links.interpreter.interpreter_action.eof_create_inputs. +Require Import CoqOfRust.revm.links.interpreter.interpreter.instruction_result. +Require Import CoqOfRust.revm.links.interpreter.interpreter.gas. (* /// The result of an interpreter operation. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter_action/call_inputs.v b/CoqOfRust/revm/links/interpreter/interpreter_action/call_inputs.v similarity index 97% rename from CoqOfRust/revm/simulations/interpreter/interpreter_action/call_inputs.v rename to CoqOfRust/revm/links/interpreter/interpreter_action/call_inputs.v index 9f886f5d1..3b4bc8101 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter_action/call_inputs.v +++ b/CoqOfRust/revm/links/interpreter/interpreter_action/call_inputs.v @@ -1,7 +1,7 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. -Require Import CoqOfRust.core.simulations.bool. -Require Import CoqOfRust.revm.simulations.dependencies. +Require Import CoqOfRust.core.links.bool. +Require Import CoqOfRust.revm.links.dependencies. (* /// Call value. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter_action/create_inputs.v b/CoqOfRust/revm/links/interpreter/interpreter_action/create_inputs.v similarity index 91% rename from CoqOfRust/revm/simulations/interpreter/interpreter_action/create_inputs.v rename to CoqOfRust/revm/links/interpreter/interpreter_action/create_inputs.v index 34e980b15..2589647e6 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter_action/create_inputs.v +++ b/CoqOfRust/revm/links/interpreter/interpreter_action/create_inputs.v @@ -1,7 +1,7 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. -Require Import CoqOfRust.revm.simulations.dependencies. -Require Import CoqOfRust.revm.simulations.primitives.env. +Require Import CoqOfRust.revm.links.dependencies. +Require Import CoqOfRust.revm.links.primitives.env. (* /// Inputs for a create call. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter_action/eof_create_inputs.v b/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v similarity index 92% rename from CoqOfRust/revm/simulations/interpreter/interpreter_action/eof_create_inputs.v rename to CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v index c7b7291ce..7512bb822 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter_action/eof_create_inputs.v +++ b/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v @@ -1,7 +1,7 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. -Require Import CoqOfRust.revm.simulations.dependencies. -Require Import CoqOfRust.revm.simulations.primitives.bytecode.eof. +Require Import CoqOfRust.revm.links.dependencies. +Require Import CoqOfRust.revm.links.primitives.bytecode.eof. (* /// Inputs for EOF create call. diff --git a/CoqOfRust/revm/simulations/primitives/bytecode.v b/CoqOfRust/revm/links/primitives/bytecode.v similarity index 100% rename from CoqOfRust/revm/simulations/primitives/bytecode.v rename to CoqOfRust/revm/links/primitives/bytecode.v diff --git a/CoqOfRust/revm/simulations/primitives/bytecode/eof.v b/CoqOfRust/revm/links/primitives/bytecode/eof.v similarity index 84% rename from CoqOfRust/revm/simulations/primitives/bytecode/eof.v rename to CoqOfRust/revm/links/primitives/bytecode/eof.v index f2c39990d..19c363752 100644 --- a/CoqOfRust/revm/simulations/primitives/bytecode/eof.v +++ b/CoqOfRust/revm/links/primitives/bytecode/eof.v @@ -1,8 +1,8 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. -Require Import CoqOfRust.revm.simulations.dependencies. -Require Import CoqOfRust.revm.simulations.primitives.bytecode.eof.header. -Require Import CoqOfRust.revm.simulations.primitives.bytecode.eof.body. +Require Import CoqOfRust.revm.links.dependencies. +Require Import CoqOfRust.revm.links.primitives.bytecode.eof.header. +Require Import CoqOfRust.revm.links.primitives.bytecode.eof.body. (* /// EOF - Ethereum Object Format. diff --git a/CoqOfRust/revm/simulations/primitives/bytecode/eof/body.v b/CoqOfRust/revm/links/primitives/bytecode/eof/body.v similarity index 84% rename from CoqOfRust/revm/simulations/primitives/bytecode/eof/body.v rename to CoqOfRust/revm/links/primitives/bytecode/eof/body.v index 73476cb39..b54ddc0a1 100644 --- a/CoqOfRust/revm/simulations/primitives/bytecode/eof/body.v +++ b/CoqOfRust/revm/links/primitives/bytecode/eof/body.v @@ -1,9 +1,9 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. -Require Import CoqOfRust.core.simulations.bool. -Require Import CoqOfRust.core.simulations.array. -Require Import CoqOfRust.revm.simulations.dependencies. -Require Import CoqOfRust.revm.simulations.primitives.bytecode.eof.type_section. +Require Import CoqOfRust.core.links.bool. +Require Import CoqOfRust.core.links.array. +Require Import CoqOfRust.revm.links.dependencies. +Require Import CoqOfRust.revm.links.primitives.bytecode.eof.type_section. (* /// EOF Body, contains types, code, container and data sections. diff --git a/CoqOfRust/revm/simulations/primitives/bytecode/eof/header.v b/CoqOfRust/revm/links/primitives/bytecode/eof/header.v similarity index 96% rename from CoqOfRust/revm/simulations/primitives/bytecode/eof/header.v rename to CoqOfRust/revm/links/primitives/bytecode/eof/header.v index eb4958f44..a4a4b386b 100644 --- a/CoqOfRust/revm/simulations/primitives/bytecode/eof/header.v +++ b/CoqOfRust/revm/links/primitives/bytecode/eof/header.v @@ -1,6 +1,6 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. -Require Import CoqOfRust.core.simulations.array. +Require Import CoqOfRust.core.links.array. (* /// EOF Header containing diff --git a/CoqOfRust/revm/simulations/primitives/bytecode/eof/type_section.v b/CoqOfRust/revm/links/primitives/bytecode/eof/type_section.v similarity index 100% rename from CoqOfRust/revm/simulations/primitives/bytecode/eof/type_section.v rename to CoqOfRust/revm/links/primitives/bytecode/eof/type_section.v diff --git a/CoqOfRust/revm/simulations/primitives/env.v b/CoqOfRust/revm/links/primitives/env.v similarity index 100% rename from CoqOfRust/revm/simulations/primitives/env.v rename to CoqOfRust/revm/links/primitives/env.v diff --git a/CoqOfRust/revm/simulations/interpreter/instructions/macros.v b/CoqOfRust/revm/simulations/interpreter/instructions/macros.v index e7dfce5a9..62deb6603 100644 --- a/CoqOfRust/revm/simulations/interpreter/instructions/macros.v +++ b/CoqOfRust/revm/simulations/interpreter/instructions/macros.v @@ -2,9 +2,12 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. Require Import CoqOfRust.simulations.M. Import simulations.M.Notations. +Require Import CoqOfRust.revm.links.interpreter.interpreter. +Require Import CoqOfRust.revm.links.interpreter.interpreter.gas. +Require Import CoqOfRust.revm.links.interpreter.interpreter.instruction_result. Require Import CoqOfRust.revm.simulations.interpreter.interpreter. Require Import CoqOfRust.revm.simulations.interpreter.interpreter.gas. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter.instruction_result. + (* /// Records a `gas` cost and fails the instruction if it would exceed the available gas. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter.v b/CoqOfRust/revm/simulations/interpreter/interpreter.v index 8e534f122..9206c4f99 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter.v @@ -2,101 +2,18 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. Require Import CoqOfRust.simulations.M. Import simulations.M.Notations. -Require Import CoqOfRust.revm.simulations.dependencies. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter.instruction_result. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter.gas. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter.contract. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter.shared_memory. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter.stack. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter.function_stack. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter_action. +Require Import CoqOfRust.revm.links.dependencies. +Require Import CoqOfRust.revm.links.interpreter.interpreter.instruction_result. +Require Import CoqOfRust.revm.links.interpreter.interpreter.gas. +Require Import CoqOfRust.revm.links.interpreter.interpreter.contract. +Require Import CoqOfRust.revm.links.interpreter.interpreter.shared_memory. +Require Import CoqOfRust.revm.links.interpreter.interpreter.stack. +Require Import CoqOfRust.revm.links.interpreter.interpreter.function_stack. +Require Import CoqOfRust.revm.links.interpreter.interpreter_action. +Require Import CoqOfRust.revm.links.interpreter.interpreter. -(* - /// EVM bytecode interpreter. - #[derive(Debug)] - pub struct Interpreter { - /// The current instruction pointer. - pub instruction_pointer: *const u8, - /// The gas state. - pub gas: Gas, - /// Contract information and invoking data - pub contract: Contract, - /// The execution control flag. If this is not set to `Continue`, the interpreter will stop - /// execution. - pub instruction_result: InstructionResult, - /// Currently run Bytecode that instruction result will point to. - /// Bytecode is owned by the contract. - pub bytecode: Bytes, - /// Whether we are Interpreting the Ethereum Object Format (EOF) bytecode. - /// This is local field that is set from `contract.is_eof()`. - pub is_eof: bool, - /// Is init flag for eof create - pub is_eof_init: bool, - /// Shared memory. - /// - /// Note: This field is only set while running the interpreter loop. - /// Otherwise it is taken and replaced with empty shared memory. - pub shared_memory: SharedMemory, - /// Stack. - pub stack: Stack, - /// EOF function stack. - pub function_stack: FunctionStack, - /// The return data buffer for internal calls. - /// It has multi usage: - /// - /// * It contains the output bytes of call sub call. - /// * When this interpreter finishes execution it contains the output bytes of this contract. - pub return_data_buffer: Bytes, - /// Whether the interpreter is in "staticcall" mode, meaning no state changes can happen. - pub is_static: bool, - /// Actions that the EVM should do. - /// - /// Set inside CALL or CREATE instructions and RETURN or REVERT instructions. Additionally those instructions will set - /// InstructionResult to CallOrCreate/Return/Revert so we know the reason. - pub next_action: InterpreterAction, - } -*) Module Interpreter. - Record t : Set := { - instruction_pointer : Z; - gas : Gas.t; - contract : Contract.t; - instruction_result : InstructionResult.t; - Bytecode : Bytes.t; - IsEof : bool; - IsEofInit : bool; - SharedMemory : SharedMemory.t; - stack : Stack.t; - function_stack : FunctionStack.t; - return_data_buffer : Bytes.t; - is_static : bool; - next_action : InterpreterAction.t; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter::Interpreter"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_interpreter::interpreter::Interpreter" [ - ("instruction_pointer", φ x.(instruction_pointer)); - ("gas", φ x.(gas)); - ("contract", φ x.(contract)); - ("instruction_result", φ x.(instruction_result)); - ("Bytecode", φ x.(Bytecode)); - ("IsEof", φ x.(IsEof)); - ("IsEofInit", φ x.(IsEofInit)); - ("SharedMemory", φ x.(SharedMemory)); - ("stack", φ x.(stack)); - ("function_stack", φ x.(function_stack)); - ("return_data_buffer", φ x.(return_data_buffer)); - ("is_static", φ x.(is_static)); - ("next_action", φ x.(next_action)) - ]; - }. - Definition update_gas {A : Set} (m : MS? Gas.t string A) : diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v b/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v index 594797e10..ecc55e371 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/gas.v @@ -2,41 +2,9 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. Require Import CoqOfRust.simulations.M. Import simulations.M.Notations. - -(* - /// Represents the state of gas during execution. - #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] - pub struct Gas { - /// The initial gas limit. This is constant throughout execution. - limit: u64, - /// The remaining gas. - remaining: u64, - /// Refunded gas. This is used only at the end of execution. - refunded: i64, - } -*) +Require Import CoqOfRust.revm.links.interpreter.interpreter.gas. Module Gas. - Record t : Set := { - limit : Z; - remaining : Z; - refunded : Z; - }. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::gas::Gas"; - }. - - Global Instance IsToValue : ToValue t := { - φ x := - Value.StructRecord "revm_interpreter::gas::Gas" [ - ("limit", φ x.(limit)); - ("remaining", φ x.(remaining)); - ("refunded", φ x.(refunded)) - ]; - }. - (* /// Records an explicit cost. /// @@ -54,13 +22,13 @@ Module Gas. *) Definition record_cost (cost : Z) : - MS? t string bool := + MS? Gas.t string bool := letS? 'gas := readS? in - let remaining_sub_cost := gas.(remaining) - cost in + let remaining_sub_cost := gas.(Gas.remaining) - cost in let success := remaining_sub_cost >=? 0 in letS? _ := if success - then writeS? (gas <| remaining := remaining_sub_cost |>) + then writeS? (gas <| Gas.remaining := remaining_sub_cost |>) else returnS? tt in returnS? success. diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v b/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v index 4cf5b5830..e3cf85274 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v @@ -3,32 +3,11 @@ Require Import CoqOfRust.links.M. Require Import CoqOfRust.simulations.M. Import simulations.M.Notations. Require Import CoqOfRust.core.simulations.array. -Require Import CoqOfRust.revm.simulations.dependencies. -Require Import CoqOfRust.revm.simulations.interpreter.interpreter.instruction_result. - -(* - /// EVM stack with [STACK_LIMIT] capacity of words. - #[derive(Debug, PartialEq, Eq, Hash)] - #[cfg_attr(feature = "serde", derive(serde::Serialize))] - pub struct Stack { - /// The underlying data of the stack. - data: Vec, - } -*) +Require Import CoqOfRust.revm.links.dependencies. +Require Import CoqOfRust.revm.links.interpreter.interpreter.instruction_result. +Require Import CoqOfRust.revm.links.interpreter.interpreter.stack. Module Stack. - Inductive t : Set := - | data : list U256 -> t. - - Global Instance IsToTy : ToTy t := { - Φ := Ty.path "revm_interpreter::interpreter::stack::Stack"; - }. - - Global Instance IsToValue : ToValue t := { - φ '(data x) := - Value.StructRecord "revm_interpreter::interpreter::stack::Stack" [("data", φ x)] - }. - (* /// Returns the length of the stack in words. #[inline] @@ -36,7 +15,7 @@ Module Stack. self.data.len() } *) - Definition len '(data stack) : Z := + Definition len '(Stack.data stack) : Z := Z.of_nat (List.length stack). (* @@ -48,12 +27,12 @@ Module Stack. } *) Definition pop : - MS? t string (U256 + InstructionResult.t) := - letS? '(data stack) := readS? in + MS? Stack.t string (U256 + InstructionResult.t) := + letS? '(Stack.data stack) := readS? in match stack with | [] => returnS? (inr InstructionResult.StackUnderflow) | x :: xs => - letS? _ := writeS? (data xs) in + letS? _ := writeS? (Stack.data xs) in returnS? (inl x) end. @@ -69,7 +48,7 @@ Module Stack. } *) Definition pop_unsafe : - MS? t string U256 := + MS? Stack.t string U256 := letS? result := pop in match result with | inl x => returnS? x @@ -89,8 +68,8 @@ Module Stack. } *) Definition top_unsafe : - MS? t string U256 := - letS? '(data stack) := readS? in + MS? Stack.t string U256 := + letS? '(Stack.data stack) := readS? in match stack with | [] => panicS? "Stack underflow" | x :: _ => returnS? x @@ -110,7 +89,7 @@ Module Stack. } *) Definition pop_top_unsafe : - MS? t string (U256 * U256) := + MS? Stack.t string (U256 * U256) := letS? pop := pop_unsafe in letS? top := top_unsafe in returnS? (pop, top). @@ -131,7 +110,7 @@ Module Stack. } *) Definition pop2_top_unsafe : - MS? t string (U256 * U256 * U256) := + MS? Stack.t string (U256 * U256 * U256) := letS? pop1 := pop_unsafe in letS? pop2 := pop_unsafe in letS? top := top_unsafe in diff --git a/CoqOfRust/revm/interpreter/function_stack.v b/CoqOfRust/revm/translations/interpreter/function_stack.v similarity index 100% rename from CoqOfRust/revm/interpreter/function_stack.v rename to CoqOfRust/revm/translations/interpreter/function_stack.v diff --git a/CoqOfRust/revm/interpreter/gas.v b/CoqOfRust/revm/translations/interpreter/gas.v similarity index 100% rename from CoqOfRust/revm/interpreter/gas.v rename to CoqOfRust/revm/translations/interpreter/gas.v diff --git a/CoqOfRust/revm/interpreter/gas/calc.v b/CoqOfRust/revm/translations/interpreter/gas/calc.v similarity index 100% rename from CoqOfRust/revm/interpreter/gas/calc.v rename to CoqOfRust/revm/translations/interpreter/gas/calc.v diff --git a/CoqOfRust/revm/interpreter/gas/constants.v b/CoqOfRust/revm/translations/interpreter/gas/constants.v similarity index 100% rename from CoqOfRust/revm/interpreter/gas/constants.v rename to CoqOfRust/revm/translations/interpreter/gas/constants.v diff --git a/CoqOfRust/revm/interpreter/host.v b/CoqOfRust/revm/translations/interpreter/host.v similarity index 100% rename from CoqOfRust/revm/interpreter/host.v rename to CoqOfRust/revm/translations/interpreter/host.v diff --git a/CoqOfRust/revm/interpreter/host/dummy.v b/CoqOfRust/revm/translations/interpreter/host/dummy.v similarity index 100% rename from CoqOfRust/revm/interpreter/host/dummy.v rename to CoqOfRust/revm/translations/interpreter/host/dummy.v diff --git a/CoqOfRust/revm/interpreter/instruction_result.v b/CoqOfRust/revm/translations/interpreter/instruction_result.v similarity index 100% rename from CoqOfRust/revm/interpreter/instruction_result.v rename to CoqOfRust/revm/translations/interpreter/instruction_result.v diff --git a/CoqOfRust/revm/interpreter/instructions/arithmetic.v b/CoqOfRust/revm/translations/interpreter/instructions/arithmetic.v similarity index 100% rename from CoqOfRust/revm/interpreter/instructions/arithmetic.v rename to CoqOfRust/revm/translations/interpreter/instructions/arithmetic.v diff --git a/CoqOfRust/revm/interpreter/instructions/bitwise.v b/CoqOfRust/revm/translations/interpreter/instructions/bitwise.v similarity index 100% rename from CoqOfRust/revm/interpreter/instructions/bitwise.v rename to CoqOfRust/revm/translations/interpreter/instructions/bitwise.v diff --git a/CoqOfRust/revm/interpreter/instructions/contract.v b/CoqOfRust/revm/translations/interpreter/instructions/contract.v similarity index 100% rename from CoqOfRust/revm/interpreter/instructions/contract.v rename to CoqOfRust/revm/translations/interpreter/instructions/contract.v diff --git a/CoqOfRust/revm/interpreter/instructions/contract/call_helpers.v b/CoqOfRust/revm/translations/interpreter/instructions/contract/call_helpers.v similarity index 100% rename from CoqOfRust/revm/interpreter/instructions/contract/call_helpers.v rename to CoqOfRust/revm/translations/interpreter/instructions/contract/call_helpers.v diff --git a/CoqOfRust/revm/interpreter/instructions/control.v b/CoqOfRust/revm/translations/interpreter/instructions/control.v similarity index 100% rename from CoqOfRust/revm/interpreter/instructions/control.v rename to CoqOfRust/revm/translations/interpreter/instructions/control.v diff --git a/CoqOfRust/revm/interpreter/instructions/data.v b/CoqOfRust/revm/translations/interpreter/instructions/data.v similarity index 100% rename from CoqOfRust/revm/interpreter/instructions/data.v rename to CoqOfRust/revm/translations/interpreter/instructions/data.v diff --git a/CoqOfRust/revm/interpreter/instructions/host.v b/CoqOfRust/revm/translations/interpreter/instructions/host.v similarity index 100% rename from CoqOfRust/revm/interpreter/instructions/host.v rename to CoqOfRust/revm/translations/interpreter/instructions/host.v diff --git a/CoqOfRust/revm/interpreter/instructions/host_env.v b/CoqOfRust/revm/translations/interpreter/instructions/host_env.v similarity index 100% rename from CoqOfRust/revm/interpreter/instructions/host_env.v rename to CoqOfRust/revm/translations/interpreter/instructions/host_env.v diff --git a/CoqOfRust/revm/interpreter/instructions/i256.v b/CoqOfRust/revm/translations/interpreter/instructions/i256.v similarity index 100% rename from CoqOfRust/revm/interpreter/instructions/i256.v rename to CoqOfRust/revm/translations/interpreter/instructions/i256.v diff --git a/CoqOfRust/revm/interpreter/instructions/memory.v b/CoqOfRust/revm/translations/interpreter/instructions/memory.v similarity index 100% rename from CoqOfRust/revm/interpreter/instructions/memory.v rename to CoqOfRust/revm/translations/interpreter/instructions/memory.v diff --git a/CoqOfRust/revm/interpreter/instructions/stack.v b/CoqOfRust/revm/translations/interpreter/instructions/stack.v similarity index 100% rename from CoqOfRust/revm/interpreter/instructions/stack.v rename to CoqOfRust/revm/translations/interpreter/instructions/stack.v diff --git a/CoqOfRust/revm/interpreter/instructions/system.v b/CoqOfRust/revm/translations/interpreter/instructions/system.v similarity index 100% rename from CoqOfRust/revm/interpreter/instructions/system.v rename to CoqOfRust/revm/translations/interpreter/instructions/system.v diff --git a/CoqOfRust/revm/interpreter/instructions/utility.v b/CoqOfRust/revm/translations/interpreter/instructions/utility.v similarity index 100% rename from CoqOfRust/revm/interpreter/instructions/utility.v rename to CoqOfRust/revm/translations/interpreter/instructions/utility.v diff --git a/CoqOfRust/revm/interpreter/interpreter.v b/CoqOfRust/revm/translations/interpreter/interpreter.v similarity index 100% rename from CoqOfRust/revm/interpreter/interpreter.v rename to CoqOfRust/revm/translations/interpreter/interpreter.v diff --git a/CoqOfRust/revm/interpreter/interpreter/analysis.v b/CoqOfRust/revm/translations/interpreter/interpreter/analysis.v similarity index 100% rename from CoqOfRust/revm/interpreter/interpreter/analysis.v rename to CoqOfRust/revm/translations/interpreter/interpreter/analysis.v diff --git a/CoqOfRust/revm/interpreter/interpreter/contract.v b/CoqOfRust/revm/translations/interpreter/interpreter/contract.v similarity index 100% rename from CoqOfRust/revm/interpreter/interpreter/contract.v rename to CoqOfRust/revm/translations/interpreter/interpreter/contract.v diff --git a/CoqOfRust/revm/interpreter/interpreter/shared_memory.v b/CoqOfRust/revm/translations/interpreter/interpreter/shared_memory.v similarity index 100% rename from CoqOfRust/revm/interpreter/interpreter/shared_memory.v rename to CoqOfRust/revm/translations/interpreter/interpreter/shared_memory.v diff --git a/CoqOfRust/revm/interpreter/interpreter/stack.v b/CoqOfRust/revm/translations/interpreter/interpreter/stack.v similarity index 100% rename from CoqOfRust/revm/interpreter/interpreter/stack.v rename to CoqOfRust/revm/translations/interpreter/interpreter/stack.v diff --git a/CoqOfRust/revm/interpreter/interpreter_action.v b/CoqOfRust/revm/translations/interpreter/interpreter_action.v similarity index 100% rename from CoqOfRust/revm/interpreter/interpreter_action.v rename to CoqOfRust/revm/translations/interpreter/interpreter_action.v diff --git a/CoqOfRust/revm/interpreter/interpreter_action/call_inputs.v b/CoqOfRust/revm/translations/interpreter/interpreter_action/call_inputs.v similarity index 100% rename from CoqOfRust/revm/interpreter/interpreter_action/call_inputs.v rename to CoqOfRust/revm/translations/interpreter/interpreter_action/call_inputs.v diff --git a/CoqOfRust/revm/interpreter/interpreter_action/call_outcome.v b/CoqOfRust/revm/translations/interpreter/interpreter_action/call_outcome.v similarity index 100% rename from CoqOfRust/revm/interpreter/interpreter_action/call_outcome.v rename to CoqOfRust/revm/translations/interpreter/interpreter_action/call_outcome.v diff --git a/CoqOfRust/revm/interpreter/interpreter_action/create_inputs.v b/CoqOfRust/revm/translations/interpreter/interpreter_action/create_inputs.v similarity index 100% rename from CoqOfRust/revm/interpreter/interpreter_action/create_inputs.v rename to CoqOfRust/revm/translations/interpreter/interpreter_action/create_inputs.v diff --git a/CoqOfRust/revm/interpreter/interpreter_action/create_outcome.v b/CoqOfRust/revm/translations/interpreter/interpreter_action/create_outcome.v similarity index 100% rename from CoqOfRust/revm/interpreter/interpreter_action/create_outcome.v rename to CoqOfRust/revm/translations/interpreter/interpreter_action/create_outcome.v diff --git a/CoqOfRust/revm/interpreter/interpreter_action/eof_create_inputs.v b/CoqOfRust/revm/translations/interpreter/interpreter_action/eof_create_inputs.v similarity index 100% rename from CoqOfRust/revm/interpreter/interpreter_action/eof_create_inputs.v rename to CoqOfRust/revm/translations/interpreter/interpreter_action/eof_create_inputs.v diff --git a/CoqOfRust/revm/interpreter/interpreter_action/eof_create_outcome.v b/CoqOfRust/revm/translations/interpreter/interpreter_action/eof_create_outcome.v similarity index 100% rename from CoqOfRust/revm/interpreter/interpreter_action/eof_create_outcome.v rename to CoqOfRust/revm/translations/interpreter/interpreter_action/eof_create_outcome.v diff --git a/CoqOfRust/revm/interpreter/opcode.v b/CoqOfRust/revm/translations/interpreter/opcode.v similarity index 100% rename from CoqOfRust/revm/interpreter/opcode.v rename to CoqOfRust/revm/translations/interpreter/opcode.v diff --git a/CoqOfRust/revm/interpreter/opcode/eof_printer.v b/CoqOfRust/revm/translations/interpreter/opcode/eof_printer.v similarity index 100% rename from CoqOfRust/revm/interpreter/opcode/eof_printer.v rename to CoqOfRust/revm/translations/interpreter/opcode/eof_printer.v diff --git a/CoqOfRust/revm/precompile/blake2.v b/CoqOfRust/revm/translations/precompile/blake2.v similarity index 100% rename from CoqOfRust/revm/precompile/blake2.v rename to CoqOfRust/revm/translations/precompile/blake2.v diff --git a/CoqOfRust/revm/precompile/bn128.v b/CoqOfRust/revm/translations/precompile/bn128.v similarity index 100% rename from CoqOfRust/revm/precompile/bn128.v rename to CoqOfRust/revm/translations/precompile/bn128.v diff --git a/CoqOfRust/revm/precompile/hash.v b/CoqOfRust/revm/translations/precompile/hash.v similarity index 100% rename from CoqOfRust/revm/precompile/hash.v rename to CoqOfRust/revm/translations/precompile/hash.v diff --git a/CoqOfRust/revm/precompile/identity.v b/CoqOfRust/revm/translations/precompile/identity.v similarity index 100% rename from CoqOfRust/revm/precompile/identity.v rename to CoqOfRust/revm/translations/precompile/identity.v diff --git a/CoqOfRust/revm/precompile/kzg_point_evaluation.v b/CoqOfRust/revm/translations/precompile/kzg_point_evaluation.v similarity index 100% rename from CoqOfRust/revm/precompile/kzg_point_evaluation.v rename to CoqOfRust/revm/translations/precompile/kzg_point_evaluation.v diff --git a/CoqOfRust/revm/precompile/lib.v b/CoqOfRust/revm/translations/precompile/lib.v similarity index 100% rename from CoqOfRust/revm/precompile/lib.v rename to CoqOfRust/revm/translations/precompile/lib.v diff --git a/CoqOfRust/revm/precompile/modexp.v b/CoqOfRust/revm/translations/precompile/modexp.v similarity index 100% rename from CoqOfRust/revm/precompile/modexp.v rename to CoqOfRust/revm/translations/precompile/modexp.v diff --git a/CoqOfRust/revm/precompile/secp256k1.v b/CoqOfRust/revm/translations/precompile/secp256k1.v similarity index 100% rename from CoqOfRust/revm/precompile/secp256k1.v rename to CoqOfRust/revm/translations/precompile/secp256k1.v diff --git a/CoqOfRust/revm/precompile/utilities.v b/CoqOfRust/revm/translations/precompile/utilities.v similarity index 100% rename from CoqOfRust/revm/precompile/utilities.v rename to CoqOfRust/revm/translations/precompile/utilities.v diff --git a/CoqOfRust/revm/primitives/bytecode.v b/CoqOfRust/revm/translations/primitives/bytecode.v similarity index 100% rename from CoqOfRust/revm/primitives/bytecode.v rename to CoqOfRust/revm/translations/primitives/bytecode.v diff --git a/CoqOfRust/revm/primitives/bytecode/eof.v b/CoqOfRust/revm/translations/primitives/bytecode/eof.v similarity index 100% rename from CoqOfRust/revm/primitives/bytecode/eof.v rename to CoqOfRust/revm/translations/primitives/bytecode/eof.v diff --git a/CoqOfRust/revm/primitives/bytecode/eof/body.v b/CoqOfRust/revm/translations/primitives/bytecode/eof/body.v similarity index 100% rename from CoqOfRust/revm/primitives/bytecode/eof/body.v rename to CoqOfRust/revm/translations/primitives/bytecode/eof/body.v diff --git a/CoqOfRust/revm/primitives/bytecode/eof/decode_helpers.v b/CoqOfRust/revm/translations/primitives/bytecode/eof/decode_helpers.v similarity index 100% rename from CoqOfRust/revm/primitives/bytecode/eof/decode_helpers.v rename to CoqOfRust/revm/translations/primitives/bytecode/eof/decode_helpers.v diff --git a/CoqOfRust/revm/primitives/bytecode/eof/header.v b/CoqOfRust/revm/translations/primitives/bytecode/eof/header.v similarity index 100% rename from CoqOfRust/revm/primitives/bytecode/eof/header.v rename to CoqOfRust/revm/translations/primitives/bytecode/eof/header.v diff --git a/CoqOfRust/revm/primitives/bytecode/eof/types_section.v b/CoqOfRust/revm/translations/primitives/bytecode/eof/types_section.v similarity index 100% rename from CoqOfRust/revm/primitives/bytecode/eof/types_section.v rename to CoqOfRust/revm/translations/primitives/bytecode/eof/types_section.v diff --git a/CoqOfRust/revm/primitives/bytecode/legacy.v b/CoqOfRust/revm/translations/primitives/bytecode/legacy.v similarity index 100% rename from CoqOfRust/revm/primitives/bytecode/legacy.v rename to CoqOfRust/revm/translations/primitives/bytecode/legacy.v diff --git a/CoqOfRust/revm/primitives/bytecode/legacy/jump_map.v b/CoqOfRust/revm/translations/primitives/bytecode/legacy/jump_map.v similarity index 100% rename from CoqOfRust/revm/primitives/bytecode/legacy/jump_map.v rename to CoqOfRust/revm/translations/primitives/bytecode/legacy/jump_map.v diff --git a/CoqOfRust/revm/primitives/constants.v b/CoqOfRust/revm/translations/primitives/constants.v similarity index 100% rename from CoqOfRust/revm/primitives/constants.v rename to CoqOfRust/revm/translations/primitives/constants.v diff --git a/CoqOfRust/revm/primitives/db.v b/CoqOfRust/revm/translations/primitives/db.v similarity index 100% rename from CoqOfRust/revm/primitives/db.v rename to CoqOfRust/revm/translations/primitives/db.v diff --git a/CoqOfRust/revm/primitives/db/components.v b/CoqOfRust/revm/translations/primitives/db/components.v similarity index 100% rename from CoqOfRust/revm/primitives/db/components.v rename to CoqOfRust/revm/translations/primitives/db/components.v diff --git a/CoqOfRust/revm/primitives/db/components/block_hash.v b/CoqOfRust/revm/translations/primitives/db/components/block_hash.v similarity index 100% rename from CoqOfRust/revm/primitives/db/components/block_hash.v rename to CoqOfRust/revm/translations/primitives/db/components/block_hash.v diff --git a/CoqOfRust/revm/primitives/db/components/state.v b/CoqOfRust/revm/translations/primitives/db/components/state.v similarity index 100% rename from CoqOfRust/revm/primitives/db/components/state.v rename to CoqOfRust/revm/translations/primitives/db/components/state.v diff --git a/CoqOfRust/revm/primitives/env.v b/CoqOfRust/revm/translations/primitives/env.v similarity index 100% rename from CoqOfRust/revm/primitives/env.v rename to CoqOfRust/revm/translations/primitives/env.v diff --git a/CoqOfRust/revm/primitives/env/handler_cfg.v b/CoqOfRust/revm/translations/primitives/env/handler_cfg.v similarity index 100% rename from CoqOfRust/revm/primitives/env/handler_cfg.v rename to CoqOfRust/revm/translations/primitives/env/handler_cfg.v diff --git a/CoqOfRust/revm/primitives/kzg/env_settings.v b/CoqOfRust/revm/translations/primitives/kzg/env_settings.v similarity index 100% rename from CoqOfRust/revm/primitives/kzg/env_settings.v rename to CoqOfRust/revm/translations/primitives/kzg/env_settings.v diff --git a/CoqOfRust/revm/primitives/kzg/trusted_setup_points.v b/CoqOfRust/revm/translations/primitives/kzg/trusted_setup_points.v similarity index 100% rename from CoqOfRust/revm/primitives/kzg/trusted_setup_points.v rename to CoqOfRust/revm/translations/primitives/kzg/trusted_setup_points.v diff --git a/CoqOfRust/revm/primitives/precompile.v b/CoqOfRust/revm/translations/primitives/precompile.v similarity index 100% rename from CoqOfRust/revm/primitives/precompile.v rename to CoqOfRust/revm/translations/primitives/precompile.v diff --git a/CoqOfRust/revm/primitives/result.v b/CoqOfRust/revm/translations/primitives/result.v similarity index 100% rename from CoqOfRust/revm/primitives/result.v rename to CoqOfRust/revm/translations/primitives/result.v diff --git a/CoqOfRust/revm/primitives/specification.v b/CoqOfRust/revm/translations/primitives/specification.v similarity index 100% rename from CoqOfRust/revm/primitives/specification.v rename to CoqOfRust/revm/translations/primitives/specification.v diff --git a/CoqOfRust/revm/primitives/state.v b/CoqOfRust/revm/translations/primitives/state.v similarity index 100% rename from CoqOfRust/revm/primitives/state.v rename to CoqOfRust/revm/translations/primitives/state.v diff --git a/CoqOfRust/revm/primitives/utilities.v b/CoqOfRust/revm/translations/primitives/utilities.v similarity index 100% rename from CoqOfRust/revm/primitives/utilities.v rename to CoqOfRust/revm/translations/primitives/utilities.v diff --git a/CoqOfRust/revm/revm/builder.v b/CoqOfRust/revm/translations/revm/builder.v similarity index 100% rename from CoqOfRust/revm/revm/builder.v rename to CoqOfRust/revm/translations/revm/builder.v diff --git a/CoqOfRust/revm/revm/context.v b/CoqOfRust/revm/translations/revm/context.v similarity index 100% rename from CoqOfRust/revm/revm/context.v rename to CoqOfRust/revm/translations/revm/context.v diff --git a/CoqOfRust/revm/revm/context/context_precompiles.v b/CoqOfRust/revm/translations/revm/context/context_precompiles.v similarity index 100% rename from CoqOfRust/revm/revm/context/context_precompiles.v rename to CoqOfRust/revm/translations/revm/context/context_precompiles.v diff --git a/CoqOfRust/revm/revm/context/evm_context.v b/CoqOfRust/revm/translations/revm/context/evm_context.v similarity index 100% rename from CoqOfRust/revm/revm/context/evm_context.v rename to CoqOfRust/revm/translations/revm/context/evm_context.v diff --git a/CoqOfRust/revm/revm/context/inner_evm_context.v b/CoqOfRust/revm/translations/revm/context/inner_evm_context.v similarity index 100% rename from CoqOfRust/revm/revm/context/inner_evm_context.v rename to CoqOfRust/revm/translations/revm/context/inner_evm_context.v diff --git a/CoqOfRust/revm/revm/db/emptydb.v b/CoqOfRust/revm/translations/revm/db/emptydb.v similarity index 100% rename from CoqOfRust/revm/revm/db/emptydb.v rename to CoqOfRust/revm/translations/revm/db/emptydb.v diff --git a/CoqOfRust/revm/revm/db/in_memory_db.v b/CoqOfRust/revm/translations/revm/db/in_memory_db.v similarity index 100% rename from CoqOfRust/revm/revm/db/in_memory_db.v rename to CoqOfRust/revm/translations/revm/db/in_memory_db.v diff --git a/CoqOfRust/revm/revm/db/states/account_status.v b/CoqOfRust/revm/translations/revm/db/states/account_status.v similarity index 100% rename from CoqOfRust/revm/revm/db/states/account_status.v rename to CoqOfRust/revm/translations/revm/db/states/account_status.v diff --git a/CoqOfRust/revm/revm/db/states/bundle_account.v b/CoqOfRust/revm/translations/revm/db/states/bundle_account.v similarity index 100% rename from CoqOfRust/revm/revm/db/states/bundle_account.v rename to CoqOfRust/revm/translations/revm/db/states/bundle_account.v diff --git a/CoqOfRust/revm/revm/db/states/bundle_state.v b/CoqOfRust/revm/translations/revm/db/states/bundle_state.v similarity index 100% rename from CoqOfRust/revm/revm/db/states/bundle_state.v rename to CoqOfRust/revm/translations/revm/db/states/bundle_state.v diff --git a/CoqOfRust/revm/revm/db/states/cache.v b/CoqOfRust/revm/translations/revm/db/states/cache.v similarity index 100% rename from CoqOfRust/revm/revm/db/states/cache.v rename to CoqOfRust/revm/translations/revm/db/states/cache.v diff --git a/CoqOfRust/revm/revm/db/states/cache_account.v b/CoqOfRust/revm/translations/revm/db/states/cache_account.v similarity index 100% rename from CoqOfRust/revm/revm/db/states/cache_account.v rename to CoqOfRust/revm/translations/revm/db/states/cache_account.v diff --git a/CoqOfRust/revm/revm/db/states/changes.v b/CoqOfRust/revm/translations/revm/db/states/changes.v similarity index 100% rename from CoqOfRust/revm/revm/db/states/changes.v rename to CoqOfRust/revm/translations/revm/db/states/changes.v diff --git a/CoqOfRust/revm/revm/db/states/plain_account.v b/CoqOfRust/revm/translations/revm/db/states/plain_account.v similarity index 100% rename from CoqOfRust/revm/revm/db/states/plain_account.v rename to CoqOfRust/revm/translations/revm/db/states/plain_account.v diff --git a/CoqOfRust/revm/revm/db/states/reverts.v b/CoqOfRust/revm/translations/revm/db/states/reverts.v similarity index 100% rename from CoqOfRust/revm/revm/db/states/reverts.v rename to CoqOfRust/revm/translations/revm/db/states/reverts.v diff --git a/CoqOfRust/revm/revm/db/states/state.v b/CoqOfRust/revm/translations/revm/db/states/state.v similarity index 100% rename from CoqOfRust/revm/revm/db/states/state.v rename to CoqOfRust/revm/translations/revm/db/states/state.v diff --git a/CoqOfRust/revm/revm/db/states/state_builder.v b/CoqOfRust/revm/translations/revm/db/states/state_builder.v similarity index 100% rename from CoqOfRust/revm/revm/db/states/state_builder.v rename to CoqOfRust/revm/translations/revm/db/states/state_builder.v diff --git a/CoqOfRust/revm/revm/db/states/transition_account.v b/CoqOfRust/revm/translations/revm/db/states/transition_account.v similarity index 100% rename from CoqOfRust/revm/revm/db/states/transition_account.v rename to CoqOfRust/revm/translations/revm/db/states/transition_account.v diff --git a/CoqOfRust/revm/revm/db/states/transition_state.v b/CoqOfRust/revm/translations/revm/db/states/transition_state.v similarity index 100% rename from CoqOfRust/revm/revm/db/states/transition_state.v rename to CoqOfRust/revm/translations/revm/db/states/transition_state.v diff --git a/CoqOfRust/revm/revm/evm.v b/CoqOfRust/revm/translations/revm/evm.v similarity index 100% rename from CoqOfRust/revm/revm/evm.v rename to CoqOfRust/revm/translations/revm/evm.v diff --git a/CoqOfRust/revm/revm/frame.v b/CoqOfRust/revm/translations/revm/frame.v similarity index 100% rename from CoqOfRust/revm/revm/frame.v rename to CoqOfRust/revm/translations/revm/frame.v diff --git a/CoqOfRust/revm/revm/handler.v b/CoqOfRust/revm/translations/revm/handler.v similarity index 100% rename from CoqOfRust/revm/revm/handler.v rename to CoqOfRust/revm/translations/revm/handler.v diff --git a/CoqOfRust/revm/revm/handler/handle_types/execution.v b/CoqOfRust/revm/translations/revm/handler/handle_types/execution.v similarity index 100% rename from CoqOfRust/revm/revm/handler/handle_types/execution.v rename to CoqOfRust/revm/translations/revm/handler/handle_types/execution.v diff --git a/CoqOfRust/revm/revm/handler/handle_types/post_execution.v b/CoqOfRust/revm/translations/revm/handler/handle_types/post_execution.v similarity index 100% rename from CoqOfRust/revm/revm/handler/handle_types/post_execution.v rename to CoqOfRust/revm/translations/revm/handler/handle_types/post_execution.v diff --git a/CoqOfRust/revm/revm/handler/handle_types/pre_execution.v b/CoqOfRust/revm/translations/revm/handler/handle_types/pre_execution.v similarity index 100% rename from CoqOfRust/revm/revm/handler/handle_types/pre_execution.v rename to CoqOfRust/revm/translations/revm/handler/handle_types/pre_execution.v diff --git a/CoqOfRust/revm/revm/handler/handle_types/validation.v b/CoqOfRust/revm/translations/revm/handler/handle_types/validation.v similarity index 100% rename from CoqOfRust/revm/revm/handler/handle_types/validation.v rename to CoqOfRust/revm/translations/revm/handler/handle_types/validation.v diff --git a/CoqOfRust/revm/revm/handler/mainnet/execution.v b/CoqOfRust/revm/translations/revm/handler/mainnet/execution.v similarity index 100% rename from CoqOfRust/revm/revm/handler/mainnet/execution.v rename to CoqOfRust/revm/translations/revm/handler/mainnet/execution.v diff --git a/CoqOfRust/revm/revm/handler/mainnet/post_execution.v b/CoqOfRust/revm/translations/revm/handler/mainnet/post_execution.v similarity index 100% rename from CoqOfRust/revm/revm/handler/mainnet/post_execution.v rename to CoqOfRust/revm/translations/revm/handler/mainnet/post_execution.v diff --git a/CoqOfRust/revm/revm/handler/mainnet/pre_execution.v b/CoqOfRust/revm/translations/revm/handler/mainnet/pre_execution.v similarity index 100% rename from CoqOfRust/revm/revm/handler/mainnet/pre_execution.v rename to CoqOfRust/revm/translations/revm/handler/mainnet/pre_execution.v diff --git a/CoqOfRust/revm/revm/handler/mainnet/validation.v b/CoqOfRust/revm/translations/revm/handler/mainnet/validation.v similarity index 100% rename from CoqOfRust/revm/revm/handler/mainnet/validation.v rename to CoqOfRust/revm/translations/revm/handler/mainnet/validation.v diff --git a/CoqOfRust/revm/revm/handler/register.v b/CoqOfRust/revm/translations/revm/handler/register.v similarity index 100% rename from CoqOfRust/revm/revm/handler/register.v rename to CoqOfRust/revm/translations/revm/handler/register.v diff --git a/CoqOfRust/revm/revm/inspector.v b/CoqOfRust/revm/translations/revm/inspector.v similarity index 100% rename from CoqOfRust/revm/revm/inspector.v rename to CoqOfRust/revm/translations/revm/inspector.v diff --git a/CoqOfRust/revm/revm/inspector/customprinter.v b/CoqOfRust/revm/translations/revm/inspector/customprinter.v similarity index 100% rename from CoqOfRust/revm/revm/inspector/customprinter.v rename to CoqOfRust/revm/translations/revm/inspector/customprinter.v diff --git a/CoqOfRust/revm/revm/inspector/gas.v b/CoqOfRust/revm/translations/revm/inspector/gas.v similarity index 100% rename from CoqOfRust/revm/revm/inspector/gas.v rename to CoqOfRust/revm/translations/revm/inspector/gas.v diff --git a/CoqOfRust/revm/revm/inspector/handler_register.v b/CoqOfRust/revm/translations/revm/inspector/handler_register.v similarity index 100% rename from CoqOfRust/revm/revm/inspector/handler_register.v rename to CoqOfRust/revm/translations/revm/inspector/handler_register.v diff --git a/CoqOfRust/revm/revm/inspector/noop.v b/CoqOfRust/revm/translations/revm/inspector/noop.v similarity index 100% rename from CoqOfRust/revm/revm/inspector/noop.v rename to CoqOfRust/revm/translations/revm/inspector/noop.v diff --git a/CoqOfRust/revm/revm/journaled_state.v b/CoqOfRust/revm/translations/revm/journaled_state.v similarity index 100% rename from CoqOfRust/revm/revm/journaled_state.v rename to CoqOfRust/revm/translations/revm/journaled_state.v From 7f6a9bae7538f0e2d8d4b45f4879ac9dca265ea2 Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Thu, 6 Jun 2024 16:13:51 +0000 Subject: [PATCH 12/14] add lenses - to use in simulations --- CoqOfRust/simulations/M.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/CoqOfRust/simulations/M.v b/CoqOfRust/simulations/M.v index 70ff3f857..139af6cf1 100644 --- a/CoqOfRust/simulations/M.v +++ b/CoqOfRust/simulations/M.v @@ -1,5 +1,13 @@ Require Import CoqOfRust.CoqOfRust. +Module Lens. + Record t {Big_A A : Set} : Set := { + read : Big_A -> A; + write : Big_A -> A -> Big_A + }. + Arguments t : clear implicits. +End Lens. + (** ** Monads that are useful for the definition of simulations. *) Module Error. @@ -41,6 +49,14 @@ Module StateError. Definition lift_from_error {State Error A : Set} (value : Error.t Error A) : t State Error A := fun state => (value, state). + + Definition lift_lens {Big_State State Error A : Set} + (lens : Lens.t Big_State State) + (value : t State Error A) : + t Big_State Error A := + fun big_state => + let (value, state) := value (lens.(Lens.read) big_state) in + (value, lens.(Lens.write) big_state state). End StateError. Module Notations. @@ -75,4 +91,6 @@ Module Notations. Notation "panicS?" := StateError.panic. Notation "return?toS?" := StateError.lift_from_error. + + Notation "liftS?" := StateError.lift_lens. End Notations. From 116c02ed1fed4bfa543adb7d2289ddb7e111163e Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Thu, 6 Jun 2024 16:14:15 +0000 Subject: [PATCH 13/14] use lenses in REVM simulations --- .../interpreter/instructions/macros.v | 2 +- .../simulations/interpreter/interpreter.v | 24 +++++-------------- 2 files changed, 7 insertions(+), 19 deletions(-) diff --git a/CoqOfRust/revm/simulations/interpreter/instructions/macros.v b/CoqOfRust/revm/simulations/interpreter/instructions/macros.v index 62deb6603..17f456d3c 100644 --- a/CoqOfRust/revm/simulations/interpreter/instructions/macros.v +++ b/CoqOfRust/revm/simulations/interpreter/instructions/macros.v @@ -28,7 +28,7 @@ Require Import CoqOfRust.revm.simulations.interpreter.interpreter.gas. Definition gas_macro (gas : Z) : MS? Interpreter.t string unit := letS? interp := readS? in - letS? success := Interpreter.update_gas (Gas.record_cost gas) in + letS? success := liftS? Interpreter.Lens.gas (Gas.record_cost gas) in if negb success then letS? _ := writeS? (interp <| diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter.v b/CoqOfRust/revm/simulations/interpreter/interpreter.v index 9206c4f99..51162db2a 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter.v @@ -12,23 +12,11 @@ Require Import CoqOfRust.revm.links.interpreter.interpreter.function_stack. Require Import CoqOfRust.revm.links.interpreter.interpreter_action. Require Import CoqOfRust.revm.links.interpreter.interpreter. - Module Interpreter. - Definition update_gas - {A : Set} - (m : MS? Gas.t string A) : - MS? Interpreter.t string A := - letS? interp := readS? in - let gas := Interpreter.gas interp in - match m gas with - | (result, state) => - match result with - | inr e => panicS? e - | inl result => - letS? _ := writeS? (interp <| - Interpreter.gas := state - |>) in - returnS? result - end - end. + Module Lens. + Definition gas : Lens.t Interpreter.t Gas.t := {| + Lens.read interp := Interpreter.gas interp; + Lens.write interp gas := interp <| Interpreter.gas := gas |> + |}. + End Lens. End Interpreter. From 7458a352da55c6c6aa6d771d35edbc92224bdab7 Mon Sep 17 00:00:00 2001 From: Valerii Huhnin Date: Thu, 6 Jun 2024 18:57:42 +0000 Subject: [PATCH 14/14] fix import --- CoqOfRust/revm/simulations/interpreter/interpreter/stack.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v b/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v index e3cf85274..2192044d4 100644 --- a/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v +++ b/CoqOfRust/revm/simulations/interpreter/interpreter/stack.v @@ -2,7 +2,7 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. Require Import CoqOfRust.simulations.M. Import simulations.M.Notations. -Require Import CoqOfRust.core.simulations.array. +Require Import CoqOfRust.core.links.array. Require Import CoqOfRust.revm.links.dependencies. Require Import CoqOfRust.revm.links.interpreter.interpreter.instruction_result. Require Import CoqOfRust.revm.links.interpreter.interpreter.stack.