From 8f69fc938ef8502485a8b6a766a3dcb6af17baef Mon Sep 17 00:00:00 2001 From: Antoine James Date: Fri, 24 Jan 2025 15:11:07 +0100 Subject: [PATCH 1/3] draft: implement eof_create_inputs definitions --- .../interpreter_action/eof_create_inputs.v | 127 +++++++++++++++++- 1 file changed, 123 insertions(+), 4 deletions(-) diff --git a/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v b/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v index 02d7fbddf..058234bc4 100644 --- a/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v +++ b/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v @@ -3,6 +3,61 @@ Require Import CoqOfRust.links.M. Require Import CoqOfRust.revm.links.dependencies. Require Import CoqOfRust.revm.links.primitives.bytecode.eof. +(* +#[derive(Debug, Clone, PartialEq, Eq)] +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +pub enum EOFCreateKind { + Tx { + initdata: Bytes, + }, + Opcode { + initcode: Eof, + input: Bytes, + created_address: Address, + }, +} +*) + +Module EOFCreateKind. + Inductive t : Type := + | Tx (initdata : Bytes.t) + | Opcode (initcode : Eof.t) (input : Bytes.t) (created_address : Address.t). + + Global Instance IsLink : Link t := { + Φ := Ty.path "revm_interpreter::interpreter::eof_create_input::EOFCreateKind"; + φ k := + match k with + | Tx initdata => + Value.StructRecord "revm_interpreter::interpreter::eof_create_input::EOFCreateKind::Tx" [ + ("initdata", φ initdata) + ] + | Opcode initcode input created_address => + Value.StructRecord "revm_interpreter::interpreter::eof_create_input::EOFCreateKind::Opcode" [ + ("initcode", φ initcode); + ("input", φ input); + ("created_address", φ created_address) + ] + end; + }. +End EOFCreateKind. + +(* +impl EOFCreateKind { + /// Returns created address + pub fn created_address(&self) -> Option<&Address> { + match self { + EOFCreateKind::Opcode { + created_address, .. + } => Some(created_address), + EOFCreateKind::Tx { .. } => None, + } + } +} +*) + + + + (* /// Inputs for EOF create call. #[derive(Debug, Default, Clone, PartialEq, Eq)] @@ -21,7 +76,7 @@ Require Import CoqOfRust.revm.links.primitives.bytecode.eof. } *) -Module EOFCreateInput. +Module EOFCreateInputs. Record t : Set := { caller : Address.t; created_address : Address.t; @@ -31,9 +86,9 @@ Module EOFCreateInput. }. Global Instance IsLink : Link t := { - Φ := Ty.path "revm_interpreter::interpreter::eof_create_input::EOFCreateInput"; + Φ := Ty.path "revm_interpreter::interpreter::eof_create_input::EOFCreateInputs"; φ x := - Value.StructRecord "revm_interpreter::interpreter::eof_create_input::EOFCreateInput" [ + Value.StructRecord "revm_interpreter::interpreter::eof_create_input::EOFCreateInputs" [ ("caller", φ x.(caller)); ("created_address", φ x.(created_address)); ("value", φ x.(value)); @@ -41,4 +96,68 @@ Module EOFCreateInput. ("gas_limit", φ x.(gas_limit)) ]; }. -End EOFCreateInput. +End EOFCreateInputs. + +Module Impl_EOFCreateInputs. + Definition Self := EOFCreateInputs.t. + + (* + pub fn new(caller: Address, value: U256, gas_limit: u64, kind: EOFCreateKind) -> Self { + //let (eof_init_code, input) = Eof::decode_dangling(tx.data.clone())?; + EOFCreateInputs { + caller, + value, + gas_limit, + kind, + } + } + *) + + Parameter address_default : Address.t. + Parameter eof_decode : Bytes.t -> Eof.t. + + Definition new (caller : Address.t) (value : U256.t) + (gas_limit : U64.t) (kind : EOFCreateKind.t) : Self := + {| EOFCreateInputs.caller := caller; + EOFCreateInputs.created_address := + match kind with + | EOFCreateKind.Opcode _ _ addr => addr + | EOFCreateKind.Tx _ => address_default + end; + EOFCreateInputs.value := value; + EOFCreateInputs.eof_init_code := + match kind with + | EOFCreateKind.Opcode code _ _ => code + | EOFCreateKind.Tx data => eof_decode data + end; + EOFCreateInputs.gas_limit := gas_limit |}. + + (* + pub fn new_opcode( + caller: Address, + created_address: Address, + value: U256, + eof_init_code: Eof, + gas_limit: u64, + input: Bytes, + ) -> EOFCreateInputs { + EOFCreateInputs::new( + caller, + value, + gas_limit, + EOFCreateKind::Opcode { + initcode: eof_init_code, + input, + created_address, + }, + ) + } + *) + + Definition new_opcode (caller : Address.t) (created_address : Address.t) + (value : U256.t) (eof_init_code : Eof.t) + (gas_limit : U64.t) (input : Bytes.t) : Self := + new caller value gas_limit (EOFCreateKind.Opcode eof_init_code input created_address). + +End Impl_EOFCreateInputs. + From 6bf7f682050f4cb044fffe640b96c0f3cdcd8be1 Mon Sep 17 00:00:00 2001 From: Antoine James Date: Fri, 24 Jan 2025 16:08:29 +0100 Subject: [PATCH 2/3] feat: implement links notation and added imports --- .../interpreter_action/eof_create_inputs.v | 44 +++++++++---------- 1 file changed, 21 insertions(+), 23 deletions(-) diff --git a/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v b/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v index 058234bc4..8c5270152 100644 --- a/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v +++ b/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v @@ -2,6 +2,8 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. Require Import CoqOfRust.revm.links.dependencies. Require Import CoqOfRust.revm.links.primitives.bytecode.eof. +Require Import CoqOfRust.revm.translations.interpreter.interpreter_action.eof_create_inputs. +Import Run. (* #[derive(Debug, Clone, PartialEq, Eq)] @@ -113,24 +115,14 @@ Module Impl_EOFCreateInputs. } *) - Parameter address_default : Address.t. - Parameter eof_decode : Bytes.t -> Eof.t. - - Definition new (caller : Address.t) (value : U256.t) - (gas_limit : U64.t) (kind : EOFCreateKind.t) : Self := - {| EOFCreateInputs.caller := caller; - EOFCreateInputs.created_address := - match kind with - | EOFCreateKind.Opcode _ _ addr => addr - | EOFCreateKind.Tx _ => address_default - end; - EOFCreateInputs.value := value; - EOFCreateInputs.eof_init_code := - match kind with - | EOFCreateKind.Opcode code _ _ => code - | EOFCreateKind.Tx data => eof_decode data - end; - EOFCreateInputs.gas_limit := gas_limit |}. + Definition run_new (caller : Address.t) (value : U256.t) (gas_limit : U64.t) (kind : EOFCreateKind.t) : + {{ + interpreter_action.eof_create_inputs.Impl_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInputs.new + [] [] [φ caller; φ value; φ gas_limit; φ kind] ⇓ + fun (v : Self) => inl (φ v) + }}. + Proof. + Admitted. (* pub fn new_opcode( @@ -153,11 +145,17 @@ Module Impl_EOFCreateInputs. ) } *) - - Definition new_opcode (caller : Address.t) (created_address : Address.t) - (value : U256.t) (eof_init_code : Eof.t) - (gas_limit : U64.t) (input : Bytes.t) : Self := - new caller value gas_limit (EOFCreateKind.Opcode eof_init_code input created_address). + (* Main run_new_opcode specification *) + (* Main run_new_opcode specification *) + Definition run_new_opcode (caller : Address.t) (created_address : Address.t) (value : U256.t) + (eof_init_code : Eof.t) (gas_limit : U64.t) (input : Bytes.t) : + {{ + interpreter_action.eof_create_inputs.Impl_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInputs.new + [] [] [φ caller; φ value; φ gas_limit; φ (EOFCreateKind.Opcode eof_init_code input created_address)] ⇓ + fun (v : EOFCreateInputs.t) => inl (φ v) + }}. + Proof. + Admitted. End Impl_EOFCreateInputs. From 97746b772201607f0d05fd9f1e7e527da6379ba2 Mon Sep 17 00:00:00 2001 From: Antoine James Date: Fri, 24 Jan 2025 17:04:46 +0100 Subject: [PATCH 3/3] draft: implement Impl_EOFCreateKind --- .../interpreter_action/eof_create_inputs.v | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v b/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v index 8c5270152..b7d4b6d0d 100644 --- a/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v +++ b/CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v @@ -57,8 +57,21 @@ impl EOFCreateKind { } *) +Module Impl_EOFCreateKind. + Definition created_address (k : EOFCreateKind.t) : option Address.t := + match k with + | EOFCreateKind.Tx _ => None + | EOFCreateKind.Opcode _ _ addr => Some addr + end. - + (* NOT WORKING as Value.Function doesn't exists in 'M.v' *) + (* + Global Instance IsLink : Link (EOFCreateKind.t -> option Address.t) := { + Φ := Ty.path "revm_interpreter::interpreter::eof_create_input::EOFCreateKind::created_address"; + φ f := Value.Function (fun k => φ (f k)); + }. + *) +End Impl_EOFCreateKind. (* /// Inputs for EOF create call.