Skip to content

draft: implement eof_create_inputs definitions #648

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open

draft: implement eof_create_inputs definitions #648

Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8f69fc9
draft: implement eof_create_inputs definitions
0xMushow Jan 24, 2025
6bf7f68
feat: implement links notation and added imports
0xMushow Jan 24, 2025
97746b7
draft: implement Impl_EOFCreateKind
0xMushow Jan 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
127 changes: 123 additions & 4 deletions CoqOfRust/revm/links/interpreter/interpreter_action/eof_create_inputs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand All @@ -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;
Expand All @@ -31,14 +86,78 @@ 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));
("eof_init_code", φ x.(eof_init_code));
("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 :=
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We do not create any definitions in the links mode and only write run_new. This is one advantage of the links approach. Here the statement would be something like:

Definition run_new (caller : Address.t) (value : U256.t) (gas_limit : U64.t) (kind : EOFCreateKind.t) :
  {{
    (* the name is in the translation file and might be longer with more module prefixes *)
    Impl_revm_interpreter_interpreter_action_eof_create_inputs_EOFCreateInputs.new
      [] [] [φ caller; φ value; φ gas_limit; φ kind] ⇓
    fun (v : Self) => inl (φ v)
  }}.
Proof.

Then for an example of proof there is the file https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/revm/links/interpreter/interpreter/gas.v , although it is still quite experimental.

{| 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).
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same as with the new function!


End Impl_EOFCreateInputs.

Loading