From eacac18b33f5d4f9b360487eff351c409bf7a7dd Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Fri, 21 Mar 2025 17:29:21 +0800 Subject: [PATCH 01/28] minor: small change to make PR visible --- CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v index 794431f42..36e073ac0 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v @@ -39,7 +39,7 @@ Proof. eapply Run.Rewrite. { progress repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. (* Seems like the code doesnt envolve proofs on `H` *) - (* progress repeat erewrite IsTraitAssociatedType_eq by apply run_Host_for_H. *) + (* progress repeat erewrite IsTraitAssociatedType_eq by apply run_Host_for_H. *) reflexivity. } destruct run_InterpreterTypes_for_WIRE. From c5a95c15abb01b44f0e650f783b81439d3d67ce2 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Fri, 21 Mar 2025 22:10:34 +0800 Subject: [PATCH 02/28] feat: Issue with `arithmetic` --- .../instructions/links/arithmetic.v | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v index 36e073ac0..773385430 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v @@ -4,6 +4,8 @@ Require Import revm.revm_context_interface.links.host. Require Import revm.revm_interpreter.links.gas. Require Import revm.revm_interpreter.links.interpreter. Require Import revm.revm_interpreter.links.interpreter_types. +(* NOTE: might be deleted *) +(* Require Import revm.revm_interpreter.instructions.i256. *) Require Import revm.revm_interpreter.instructions.arithmetic. Require Import ruint.links.add. Require Import ruint.links.cmp. @@ -39,7 +41,7 @@ Proof. eapply Run.Rewrite. { progress repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. (* Seems like the code doesnt envolve proofs on `H` *) - (* progress repeat erewrite IsTraitAssociatedType_eq by apply run_Host_for_H. *) + (* progress repeat erewrite IsTraitAssociatedType_eq by apply run_Host_for_H. *) reflexivity. } destruct run_InterpreterTypes_for_WIRE. @@ -162,6 +164,16 @@ Proof. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. (* TODO: revm_interpreter::instructions::i256::i256_div *) + (* NOTE: + Trait instructions.i256.i256_div [] [] + [lib.Uint.IsLink.(φ) value; lib.Uint.IsLink.(φ) value1] + (lib.Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}) + Here's an interesting result: the goal says we need to prove `i256_div` belongs to some trait, + in othr word, it's an associated function. + Two problems here: + 1. `i256_div` is not an associated function; + 2. I wonder how to link `i256_div`. My tried to generate an instance but it seems to be unrelated. + *) run_symbolic. (* Defined. *) Admitted. From 640c495e62b2ae9611bbf48a3927a1ca149a01eb Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Fri, 21 Mar 2025 22:12:38 +0800 Subject: [PATCH 03/28] feat: Add `i256.v` --- .../revm/revm_interpreter/instructions/links/i256.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v index 754b38126..2152af626 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v @@ -1 +1,11 @@ -(* Initial stub *) \ No newline at end of file +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import revm.revm_interpreter.instructions.i256. + +(* NOTE: This function isn't associated with a trait. I wonder if this is the correct way to translate it... *) +(* pub fn i256_div(mut first: U256, mut second: U256) -> U256 *) + +Global Instance Instance_IsFunction_i256_div : + M.IsFunction.Trait "revm::revm_interpreter::instructions::i256::i256_div" instructions.i256.i256_div. +Admitted. +Global Typeclasses Opaque instructions.i256.i256_div. \ No newline at end of file From b31bff4c35d8444af42ed2197ead7fcc5d68ed9c Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Sat, 22 Mar 2025 06:19:19 +0800 Subject: [PATCH 04/28] minor: comments --- .../instructions/links/arithmetic.v | 2 +- .../instructions/links/i256.v | 19 ++++++++++++++++++- 2 files changed, 19 insertions(+), 2 deletions(-) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v index 773385430..4a3026e17 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v @@ -172,7 +172,7 @@ Proof. in othr word, it's an associated function. Two problems here: 1. `i256_div` is not an associated function; - 2. I wonder how to link `i256_div`. My tried to generate an instance but it seems to be unrelated. + 2. `i256_div` seems to be unlinkable. My tried to generate an instance but it seems to be unrelated. *) run_symbolic. (* Defined. *) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v index 2152af626..5550bc465 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v @@ -8,4 +8,21 @@ Require Import revm.revm_interpreter.instructions.i256. Global Instance Instance_IsFunction_i256_div : M.IsFunction.Trait "revm::revm_interpreter::instructions::i256::i256_div" instructions.i256.i256_div. Admitted. -Global Typeclasses Opaque instructions.i256.i256_div. \ No newline at end of file +Global Typeclasses Opaque instructions.i256.i256_div. + +(* NOTE: 2nd failed attempt: + +Definition trait : TraitMethod.Header.t := + ("revm::revm_interpreter::instructions::i256", [], [], []). + +Definition Run_i256_div : Set := + TraitMethod.C trait "i256_div" (fun method => + forall (first : Ref.t Pointer.Kind.MutRef U256.t) + (second : Ref.t Pointer.Kind.MutRef U256.t), + Run.Trait method [] [] [ φ first; φ second; ] U256.t + ). + +Class Run : Set := { + i256_div : Run_i256_div; +}. +*) \ No newline at end of file From b407839d9a4c33e37ec4acc6eedc4363464d644a Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Sat, 22 Mar 2025 07:58:02 +0800 Subject: [PATCH 05/28] minor: comments --- .../revm/revm_interpreter/instructions/links/block_info.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index afebb154f..3da21d58b 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -60,9 +60,7 @@ Proof. destruct run_CfgGetter. destruct run_Cfg_for_Cfg. run_symbolic. - (* TODO: check `cfg::cfg` *) -Admitted. -(* Defined. *) +Defined. (* pub fn coinbase( @@ -94,6 +92,7 @@ Proof. destruct run_Host_for_H. destruct run_BlockGetter. destruct run_Block_for_Block. + (* TODO: core::convert::Into *) run_symbolic. Admitted. From 6188953bd7723d4192d02605779b13616db73b89 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Sat, 22 Mar 2025 09:29:27 +0800 Subject: [PATCH 06/28] minor: debugging `Into` --- CoqOfRust/core/convert/links/mod.v | 14 ++++++++------ .../instructions/links/block_info.v | 5 ++--- 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/CoqOfRust/core/convert/links/mod.v b/CoqOfRust/core/convert/links/mod.v index c6358f305..2d6fcba22 100644 --- a/CoqOfRust/core/convert/links/mod.v +++ b/CoqOfRust/core/convert/links/mod.v @@ -28,14 +28,16 @@ pub trait Into: Sized { } *) Module Into. + Definition trait (Self T : Set) `{Link Self} `{Link T} : TraitMethod.Header.t := + ("core::convert::Into", [], [Φ T], Φ Self). + Definition Run_into (Self T : Set) `{Link Self} `{Link T} : Set := - {into @ - IsTraitMethod.t "core::convert::Into" [] [Φ T] (Φ Self) "into" into * - forall (self : Self), - {{ into [] [] [φ self] 🔽 T }} - }. + TraitMethod.C (trait Self T) "into" (fun method => + forall (self : Ref.t Pointer.Kind.Ref Self), + Run.Trait method [] [] [ φ self ] T + ). - Record Run (Self : Set) (T : Set) `{Link Self} `{Link T} : Set := { + Class Run (Self : Set) (T : Set) `{Link Self} `{Link T} : Set := { into : Run_into Self T; }. End Into. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index 3da21d58b..ea507f0fd 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -15,8 +15,6 @@ Require Import core.convert.links.mod. Import Impl_SpecId. Import Impl_Gas. Import from.Impl_Uint. -(* TODO: check if we need to implement `into` function in `from` *) -(* Import into.Impl_Uint. *) (* TODO(progress): - finish link in `dependencies` and link to here @@ -92,7 +90,8 @@ Proof. destruct run_Host_for_H. destruct run_BlockGetter. destruct run_Block_for_Block. - (* TODO: core::convert::Into *) + (* TODO: why `core::convert::Into` still doesn't work? *) + (* assert ( forall (A : Set), A ) . *) run_symbolic. Admitted. From 41f15e0993f13c2747fbb06c89758abed42b86a4 Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Mon, 24 Mar 2025 10:44:34 +0100 Subject: [PATCH 07/28] suggestion commit as comment --- CoqOfRust/revm/links/dependencies.v | 33 ++++++++++++++----- .../instructions/links/arithmetic.v | 7 ++-- .../instructions/links/block_info.v | 3 +- .../instructions/links/i256.v | 15 +++++++-- 4 files changed, 40 insertions(+), 18 deletions(-) diff --git a/CoqOfRust/revm/links/dependencies.v b/CoqOfRust/revm/links/dependencies.v index ccf10969f..b3aef0be9 100644 --- a/CoqOfRust/revm/links/dependencies.v +++ b/CoqOfRust/revm/links/dependencies.v @@ -7,6 +7,11 @@ Require Import core.links.clone. Require Import core.links.default. Require Import ruint.links.lib. +Module U256. + Definition t : Set := + Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}. +End U256. + (* TODO: - Start link with beneficiary's Address return type @@ -60,11 +65,11 @@ Module alloy_primitives. forall (N : Usize.t), core.convert.links.mod.From.Run (Self N) (T := array.t U8.t N). End Impl_From_for_FixedBytes. - - Module Impl_Into_for_FixedBytes. + + Module Impl_Into_array_for_FixedBytes. Definition Self (N : Usize.t) : Set := FixedBytes.t N. - + (* fn into(self) -> Uint *) Parameter into : forall (N : Usize.t), PolymorphicFunction.t. @@ -77,7 +82,22 @@ Module alloy_primitives. Parameter run : forall (N : Usize.t), core.convert.links.mod.Into.Run (Self N) (array.t U8.t N). - End Impl_Into_for_FixedBytes. + End Impl_Into_array_for_FixedBytes. + + Module Impl_Into_U256_for_FixedBytes. + Definition Self : Set := + FixedBytes.t {| Integer.value := 32 |}. + + Parameter into : PolymorphicFunction.t. + + Axiom Implements : + M.IsTraitInstance + "core::convert::Into" [] [ Φ U256.t ] (Φ Self) + [ ("into", InstanceField.Method into) ]. + + Parameter run : + core.convert.links.mod.Into.Run Self U256.t. + End Impl_Into_U256_for_FixedBytes. End fixed. Module address. @@ -236,11 +256,6 @@ End FixedBytes. (** ** Here we define some aliases that are convenient *) -Module U256. - Definition t : Set := - Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}. -End U256. - Module B256. Definition t : Set := alloy_primitives.bits.links.fixed.FixedBytes.t {| Integer.value := 32 |}. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v index 4a3026e17..028eb8204 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v @@ -4,9 +4,9 @@ Require Import revm.revm_context_interface.links.host. Require Import revm.revm_interpreter.links.gas. Require Import revm.revm_interpreter.links.interpreter. Require Import revm.revm_interpreter.links.interpreter_types. -(* NOTE: might be deleted *) -(* Require Import revm.revm_interpreter.instructions.i256. *) +Require Import revm.revm_interpreter.instructions.links.i256. Require Import revm.revm_interpreter.instructions.arithmetic. +Require Import revm.revm_interpreter.instructions.i256. Require Import ruint.links.add. Require Import ruint.links.cmp. Require Import ruint.links.div. @@ -175,8 +175,7 @@ Proof. 2. `i256_div` seems to be unlinkable. My tried to generate an instance but it seems to be unrelated. *) run_symbolic. -(* Defined. *) -Admitted. +Defined. (* pub fn rem( diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index ea507f0fd..470470fe2 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -90,8 +90,7 @@ Proof. destruct run_Host_for_H. destruct run_BlockGetter. destruct run_Block_for_Block. - (* TODO: why `core::convert::Into` still doesn't work? *) - (* assert ( forall (A : Set), A ) . *) + destruct alloy_primitives.bits.links.fixed.Impl_Into_U256_for_FixedBytes.run. run_symbolic. Admitted. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v index 5550bc465..e926beb96 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v @@ -1,14 +1,15 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. +Require Import revm.links.dependencies. Require Import revm.revm_interpreter.instructions.i256. (* NOTE: This function isn't associated with a trait. I wonder if this is the correct way to translate it... *) (* pub fn i256_div(mut first: U256, mut second: U256) -> U256 *) -Global Instance Instance_IsFunction_i256_div : +(* Global Instance Instance_IsFunction_i256_div : M.IsFunction.Trait "revm::revm_interpreter::instructions::i256::i256_div" instructions.i256.i256_div. Admitted. -Global Typeclasses Opaque instructions.i256.i256_div. +Global Typeclasses Opaque instructions.i256.i256_div. *) (* NOTE: 2nd failed attempt: @@ -25,4 +26,12 @@ Definition Run_i256_div : Set := Class Run : Set := { i256_div : Run_i256_div; }. -*) \ No newline at end of file +*) + +(* pub fn i256_div(mut first: U256, mut second: U256) -> U256 *) +Instance run_i256_div (first second : U256.t) : + Run.Trait instructions.i256.i256_div [] [] [ φ first; φ second ] U256.t. +Proof. + constructor. + run_symbolic. +Admitted. From 06461e6f4cd0c6ac2a845f5bf50ee794babc1f4b Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Tue, 25 Mar 2025 20:41:53 +0800 Subject: [PATCH 08/28] minor: progress --- .../revm/revm_context_interface/links/block.v | 10 ++++++++ .../instructions/links/arithmetic.v | 11 -------- .../instructions/links/block_info.v | 11 +++++++- .../instructions/links/i256.v | 25 ------------------- 4 files changed, 20 insertions(+), 37 deletions(-) diff --git a/CoqOfRust/revm/revm_context_interface/links/block.v b/CoqOfRust/revm/revm_context_interface/links/block.v index b99fa597b..d8041afb1 100644 --- a/CoqOfRust/revm/revm_context_interface/links/block.v +++ b/CoqOfRust/revm/revm_context_interface/links/block.v @@ -120,6 +120,16 @@ Module BlockGetter. Run.Trait method [] [] [ φ self ] unit ). + (* NOTE: something to confirm is that, if `BlockGetter` "inherhits" several methods + from `Block` trait, do we still need to additionally write instances for these methods? *) + (* TODO: fill in timestamp *) + Definition Run_timestamp (Self : Set) `{Link Self} : Set := + (* TraitMethod.C (trait Self) "block" (fun method => + forall (self : Ref.t Pointer.Kind.Ref Self), + Run.Trait method [] [] [ φ self ] unit + ). *) + . + Class Run (Self : Set) `{Link Self} (types : Types.t) `{Types.AreLinks types} : Set := { Block_IsAssociated : IsTraitAssociatedType diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v index 028eb8204..e3b0b2944 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v @@ -163,17 +163,6 @@ Proof. destruct run_InterpreterTypes_for_WIRE. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. - (* TODO: revm_interpreter::instructions::i256::i256_div *) - (* NOTE: - Trait instructions.i256.i256_div [] [] - [lib.Uint.IsLink.(φ) value; lib.Uint.IsLink.(φ) value1] - (lib.Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}) - Here's an interesting result: the goal says we need to prove `i256_div` belongs to some trait, - in othr word, it's an associated function. - Two problems here: - 1. `i256_div` is not an associated function; - 2. `i256_div` seems to be unlinkable. My tried to generate an instance but it seems to be unrelated. - *) run_symbolic. Defined. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index 470470fe2..698381dd4 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -19,7 +19,7 @@ Import from.Impl_Uint. (* TODO(progress): - finish link in `dependencies` and link to here - Take a closer look at the syntax of M - *) +*) (* pub fn chainid( @@ -106,7 +106,9 @@ pub fn timestamp( Instance run_timestamp {WIRE H : Set} `{Link WIRE} `{Link H} {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (run_Host_for_H : Host.Run H H_types) (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) (_host : Ref.t Pointer.Kind.MutRef H) : Run.Trait @@ -122,6 +124,13 @@ Proof. destruct run_InterpreterTypes_for_WIRE. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. + destruct run_Host_for_H. + destruct run_BlockGetter. + destruct run_Block_for_Block. + (* TODO: + - check BlockGetter::timestamp + - check BlockGetter::block + *) run_symbolic. Admitted. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v index e926beb96..4748abcb5 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v @@ -3,31 +3,6 @@ Require Import CoqOfRust.links.M. Require Import revm.links.dependencies. Require Import revm.revm_interpreter.instructions.i256. -(* NOTE: This function isn't associated with a trait. I wonder if this is the correct way to translate it... *) -(* pub fn i256_div(mut first: U256, mut second: U256) -> U256 *) - -(* Global Instance Instance_IsFunction_i256_div : - M.IsFunction.Trait "revm::revm_interpreter::instructions::i256::i256_div" instructions.i256.i256_div. -Admitted. -Global Typeclasses Opaque instructions.i256.i256_div. *) - -(* NOTE: 2nd failed attempt: - -Definition trait : TraitMethod.Header.t := - ("revm::revm_interpreter::instructions::i256", [], [], []). - -Definition Run_i256_div : Set := - TraitMethod.C trait "i256_div" (fun method => - forall (first : Ref.t Pointer.Kind.MutRef U256.t) - (second : Ref.t Pointer.Kind.MutRef U256.t), - Run.Trait method [] [] [ φ first; φ second; ] U256.t - ). - -Class Run : Set := { - i256_div : Run_i256_div; -}. -*) - (* pub fn i256_div(mut first: U256, mut second: U256) -> U256 *) Instance run_i256_div (first second : U256.t) : Run.Trait instructions.i256.i256_div [] [] [ φ first; φ second ] U256.t. From b3f96bc1363ba1f769c43d0d03c4e7e4223cb9f0 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Tue, 25 Mar 2025 21:24:28 +0800 Subject: [PATCH 09/28] feat: Progress on `arithmetic` with `i256_mod` --- .../revm/revm_context_interface/links/block.v | 14 +++++++------- .../instructions/links/arithmetic.v | 4 +--- .../revm_interpreter/instructions/links/i256.v | 8 ++++++++ .../revm/revm_interpreter/links/instructions.v | 4 ++-- CoqOfRust/ruint/links/lib.v | 13 +++++++++++++ 5 files changed, 31 insertions(+), 12 deletions(-) diff --git a/CoqOfRust/revm/revm_context_interface/links/block.v b/CoqOfRust/revm/revm_context_interface/links/block.v index d8041afb1..15ec98027 100644 --- a/CoqOfRust/revm/revm_context_interface/links/block.v +++ b/CoqOfRust/revm/revm_context_interface/links/block.v @@ -120,15 +120,14 @@ Module BlockGetter. Run.Trait method [] [] [ φ self ] unit ). - (* NOTE: something to confirm is that, if `BlockGetter` "inherhits" several methods - from `Block` trait, do we still need to additionally write instances for these methods? *) - (* TODO: fill in timestamp *) + (* NOTE: Question: since `BlockGetter` "inherhits" several methods from `Block` trait, + do we still need to additionally write instances for these methods? *) + (* fn timestamp(&self) -> u64; *) Definition Run_timestamp (Self : Set) `{Link Self} : Set := - (* TraitMethod.C (trait Self) "block" (fun method => + TraitMethod.C (trait Self) "timestamp" (fun method => forall (self : Ref.t Pointer.Kind.Ref Self), - Run.Trait method [] [] [ φ self ] unit - ). *) - . + Run.Trait method [] [] [ φ self ] U64.t + ). Class Run (Self : Set) `{Link Self} (types : Types.t) `{Types.AreLinks types} : Set := { Block_IsAssociated : @@ -137,5 +136,6 @@ Module BlockGetter. "Block" (Φ types.(Types.Block)); run_Block_for_Block : Block.Run types.(Types.Block); block : Run_block Self; + timestamp : Run_timestamp Self; }. End BlockGetter. \ No newline at end of file diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v index e3b0b2944..5a7b63793 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v @@ -219,10 +219,8 @@ Proof. destruct run_InterpreterTypes_for_WIRE. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. - (* TODO: revm_interpreter::instructions::i256::i256_mod *) run_symbolic. - Admitted. -(* Defined. *) +Defined. (* pub fn addmod( diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v index 4748abcb5..470464ea2 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v @@ -10,3 +10,11 @@ Proof. constructor. run_symbolic. Admitted. + +(* pub fn i256_mod(mut first: U256, mut second: U256) -> U256 *) +Instance run_i256_mod (first second : U256.t) : + Run.Trait instructions.i256.i256_mod [] [] [ φ first; φ second ] U256.t. +Proof. + constructor. + run_symbolic. +Admitted. \ No newline at end of file diff --git a/CoqOfRust/revm/revm_interpreter/links/instructions.v b/CoqOfRust/revm/revm_interpreter/links/instructions.v index 9a64c45c4..f39a68435 100644 --- a/CoqOfRust/revm/revm_interpreter/links/instructions.v +++ b/CoqOfRust/revm/revm_interpreter/links/instructions.v @@ -74,5 +74,5 @@ Proof. (* TODO: resolve the incomplete run in future PRs In this file our major change results from adding `H` parameters in the `run_add` function *) -Admitted. -(* Defined. *) +(* Admitted. *) +Defined. diff --git a/CoqOfRust/ruint/links/lib.v b/CoqOfRust/ruint/links/lib.v index 7797c0353..b8b09080b 100644 --- a/CoqOfRust/ruint/links/lib.v +++ b/CoqOfRust/ruint/links/lib.v @@ -23,4 +23,17 @@ Module Uint. - mul_mod from ruint::modular - pow from ruint::modular *) + + (* + Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t := + ("revm_context_interface::block::Block", [], [], Φ Self). + + (* fn number(&self) -> u64; *) + Definition Run_number (Self : Set) `{Link Self} : Set := + TraitMethod.C (trait Self) "number" (fun method => + forall (self : Ref.t Pointer.Kind.Ref Self), + Run.Trait method [] [] [ φ self ] U64.t + ). + + *) End Uint. From 9425080c74e1b0b8ea3d06e29da25323ac80ffa5 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Wed, 26 Mar 2025 20:10:01 +0800 Subject: [PATCH 10/28] minor: progress --- CoqOfRust/revm/revm_context_interface/links/block.v | 6 +++--- .../revm/revm_interpreter/instructions/links/block_info.v | 4 ++-- CoqOfRust/ruint/links/lib.v | 2 ++ 3 files changed, 7 insertions(+), 5 deletions(-) diff --git a/CoqOfRust/revm/revm_context_interface/links/block.v b/CoqOfRust/revm/revm_context_interface/links/block.v index 15ec98027..f431f504e 100644 --- a/CoqOfRust/revm/revm_context_interface/links/block.v +++ b/CoqOfRust/revm/revm_context_interface/links/block.v @@ -120,14 +120,14 @@ Module BlockGetter. Run.Trait method [] [] [ φ self ] unit ). - (* NOTE: Question: since `BlockGetter` "inherhits" several methods from `Block` trait, + (* (* NOTE: Question: since `BlockGetter` "inherhits" several methods from `Block` trait, do we still need to additionally write instances for these methods? *) (* fn timestamp(&self) -> u64; *) Definition Run_timestamp (Self : Set) `{Link Self} : Set := TraitMethod.C (trait Self) "timestamp" (fun method => forall (self : Ref.t Pointer.Kind.Ref Self), Run.Trait method [] [] [ φ self ] U64.t - ). + ). *) Class Run (Self : Set) `{Link Self} (types : Types.t) `{Types.AreLinks types} : Set := { Block_IsAssociated : @@ -136,6 +136,6 @@ Module BlockGetter. "Block" (Φ types.(Types.Block)); run_Block_for_Block : Block.Run types.(Types.Block); block : Run_block Self; - timestamp : Run_timestamp Self; + (* timestamp : Run_timestamp Self; *) }. End BlockGetter. \ No newline at end of file diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index 698381dd4..1d440b725 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -128,8 +128,8 @@ Proof. destruct run_BlockGetter. destruct run_Block_for_Block. (* TODO: - - check BlockGetter::timestamp - - check BlockGetter::block + - check revm_interpreter::gas::Gas::record_cost + - check revm_interpreter::interpreter_types::LoopControl"::gas *) run_symbolic. Admitted. diff --git a/CoqOfRust/ruint/links/lib.v b/CoqOfRust/ruint/links/lib.v index b8b09080b..0ff9458de 100644 --- a/CoqOfRust/ruint/links/lib.v +++ b/CoqOfRust/ruint/links/lib.v @@ -19,6 +19,8 @@ Module Uint. Smpl Add eapply of_ty : of_ty. (* TODO: + - find source code + - Maybe refer to `i256` for implementing functions without traits? - add_mod from ruint::modular - mul_mod from ruint::modular - pow from ruint::modular From 77bb5f3160c9566d3a0e4c69ab393ae4b761a6fa Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Wed, 26 Mar 2025 20:49:29 +0800 Subject: [PATCH 11/28] minor: progress --- CoqOfRust/revm/links/dependencies.v | 12 --------- .../instructions/links/block_info.v | 5 ---- .../instructions/links/modular.v | 25 +++++++++++++++++++ CoqOfRust/ruint/links/lib.v | 21 ---------------- 4 files changed, 25 insertions(+), 38 deletions(-) create mode 100644 CoqOfRust/revm/revm_interpreter/instructions/links/modular.v diff --git a/CoqOfRust/revm/links/dependencies.v b/CoqOfRust/revm/links/dependencies.v index b3aef0be9..f86621596 100644 --- a/CoqOfRust/revm/links/dependencies.v +++ b/CoqOfRust/revm/links/dependencies.v @@ -12,14 +12,6 @@ Module U256. Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}. End U256. -(* -TODO: -- Start link with beneficiary's Address return type -- In `beneficiary`, link it to Address type(?) -- Link Addesss::into_word -- Link Uint::into -*) - Module alloy_primitives. Module bits. Module links. @@ -248,10 +240,6 @@ Module FixedBytes. Φ := Ty.path "alloy_primitives::bits::fixed::FixedBytes"; φ := to_value; }. - - (* TODO: - - (alloy_primitives::FixedBytes) fn into(self) -> Uint - *) End FixedBytes. (** ** Here we define some aliases that are convenient *) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index 1d440b725..e3954b382 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -16,11 +16,6 @@ Import Impl_SpecId. Import Impl_Gas. Import from.Impl_Uint. -(* TODO(progress): - - finish link in `dependencies` and link to here - - Take a closer look at the syntax of M -*) - (* pub fn chainid( interpreter: &mut Interpreter, diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/modular.v b/CoqOfRust/revm/revm_interpreter/instructions/links/modular.v new file mode 100644 index 000000000..92258d845 --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/modular.v @@ -0,0 +1,25 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import ruint.links.lib. +Require Import ruint.modular. + +(* +TODO: +- ruint::modular::add_mod +- ruint::modular::mul_mod +- ruint::modular::pow +- find source code +- Maybe refer to `i256` for implementing functions without traits? +*) + +(* + Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t := + ("revm_context_interface::block::Block", [], [], Φ Self). + +(* fn number(&self) -> u64; *) +Definition Run_number (Self : Set) `{Link Self} : Set := + TraitMethod.C (trait Self) "number" (fun method => + forall (self : Ref.t Pointer.Kind.Ref Self), + Run.Trait method [] [] [ φ self ] U64.t + ). +*) \ No newline at end of file diff --git a/CoqOfRust/ruint/links/lib.v b/CoqOfRust/ruint/links/lib.v index 0ff9458de..112e65f30 100644 --- a/CoqOfRust/ruint/links/lib.v +++ b/CoqOfRust/ruint/links/lib.v @@ -17,25 +17,4 @@ Module Uint. OfTy.t (Ty.apply (Ty.path "ruint::Uint") [ BITS' ; LIMBS' ] []). Proof. intros. eapply OfTy.Make with (A := t BITS LIMBS). now subst. Defined. Smpl Add eapply of_ty : of_ty. - - (* TODO: - - find source code - - Maybe refer to `i256` for implementing functions without traits? - - add_mod from ruint::modular - - mul_mod from ruint::modular - - pow from ruint::modular - *) - - (* - Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t := - ("revm_context_interface::block::Block", [], [], Φ Self). - - (* fn number(&self) -> u64; *) - Definition Run_number (Self : Set) `{Link Self} : Set := - TraitMethod.C (trait Self) "number" (fun method => - forall (self : Ref.t Pointer.Kind.Ref Self), - Run.Trait method [] [] [ φ self ] U64.t - ). - - *) End Uint. From cc6de0757e8cdc8b2349c26abb2edeb577c2320d Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Wed, 26 Mar 2025 20:51:08 +0800 Subject: [PATCH 12/28] minor: move file to correct directory --- .../{revm/revm_interpreter/instructions => ruint}/links/modular.v | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename CoqOfRust/{revm/revm_interpreter/instructions => ruint}/links/modular.v (100%) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/modular.v b/CoqOfRust/ruint/links/modular.v similarity index 100% rename from CoqOfRust/revm/revm_interpreter/instructions/links/modular.v rename to CoqOfRust/ruint/links/modular.v From c22f4ea0bd6b8a217b2fe3e485d2fbcb6de7916e Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Wed, 26 Mar 2025 22:02:22 +0800 Subject: [PATCH 13/28] feat: add `Uint` operation links --- CoqOfRust/ruint/links/modular.v | 48 ++++++++++++++++++++------------- 1 file changed, 30 insertions(+), 18 deletions(-) diff --git a/CoqOfRust/ruint/links/modular.v b/CoqOfRust/ruint/links/modular.v index 92258d845..fa1adceda 100644 --- a/CoqOfRust/ruint/links/modular.v +++ b/CoqOfRust/ruint/links/modular.v @@ -3,23 +3,35 @@ Require Import CoqOfRust.links.M. Require Import ruint.links.lib. Require Import ruint.modular. -(* -TODO: -- ruint::modular::add_mod -- ruint::modular::mul_mod -- ruint::modular::pow -- find source code -- Maybe refer to `i256` for implementing functions without traits? -*) +(* impl Uint *) +Module Impl_Uint. + Definition Self (BITS LIMBS : Usize.t) : Set := + Uint.t BITS LIMBS. -(* - Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t := - ("revm_context_interface::block::Block", [], [], Φ Self). + (* pub fn add_mod(self, rhs: Self, modulus: Self) -> Self *) + Instance run_add_mod + (BITS LIMBS : Usize.t) + (x1 x2 : Self BITS LIMBS) : + Run.Trait + (modular.Impl_ruint_Uint_BITS_LIMBS.add_mod (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ] + (Self BITS LIMBS). + Admitted. -(* fn number(&self) -> u64; *) -Definition Run_number (Self : Set) `{Link Self} : Set := - TraitMethod.C (trait Self) "number" (fun method => - forall (self : Ref.t Pointer.Kind.Ref Self), - Run.Trait method [] [] [ φ self ] U64.t - ). -*) \ No newline at end of file + (* pub fn mul_mod(self, rhs: Self, modulus: Self) -> Self *) + Instance run_mul_mod + (BITS LIMBS : Usize.t) + (x1 x2 : Self BITS LIMBS) : + Run.Trait + (modular.Impl_ruint_Uint_BITS_LIMBS.mul_mod (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ] + (Self BITS LIMBS). + Admitted. + + (* pub fn pow_mod(self, exp: Self, modulus: Self) -> Self *) + Instance run_pow_mod + (BITS LIMBS : Usize.t) + (x1 x2 : Self BITS LIMBS) : + Run.Trait + (modular.Impl_ruint_Uint_BITS_LIMBS.pow_mod (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ] + (Self BITS LIMBS). + Admitted. +End Impl_Uint. From 1d63421847b53da3cbc5c233399695fb399d47a3 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Wed, 26 Mar 2025 22:26:58 +0800 Subject: [PATCH 14/28] minor: progress --- .../revm/revm_interpreter/instructions/links/arithmetic.v | 2 ++ .../revm/revm_interpreter/instructions/links/block_info.v | 6 ++++++ 2 files changed, 8 insertions(+) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v index 5a7b63793..5fcbcabe4 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v @@ -11,12 +11,14 @@ Require Import ruint.links.add. Require Import ruint.links.cmp. Require Import ruint.links.div. Require Import ruint.links.mul. +Require Import ruint.links.modular. Import Impl_Gas. Import add.Impl_Uint. Import cmp.Impl_Uint. Import div.Impl_Uint. Import mul.Impl_Uint. +Import modular.Impl_Uint. (* pub fn add( diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index e3954b382..0d6faf9f5 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -16,6 +16,12 @@ Import Impl_SpecId. Import Impl_Gas. Import from.Impl_Uint. +(* TODO(progress): + - finish `ruint` related components + - check revm_interpreter::gas::Gas::record_cost + - check revm_interpreter::interpreter_types::LoopControl::gas + *) + (* pub fn chainid( interpreter: &mut Interpreter, From 3c359efe7d25ac3e8c72314b437098c6ad866c39 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Wed, 26 Mar 2025 22:34:55 +0800 Subject: [PATCH 15/28] minor: progress --- .../revm/revm_interpreter/instructions/links/arithmetic.v | 4 ++-- .../revm/revm_interpreter/instructions/links/block_info.v | 2 +- CoqOfRust/ruint/links/modular.v | 1 + 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v index 5fcbcabe4..0c839682f 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v @@ -251,8 +251,8 @@ Proof. destruct run_StackTrait_for_Stack. (* TODO: Uint::add_mod *) run_symbolic. - Admitted. -(* Defined. *) + (* Admitted. *) +Defined. (* pub fn mulmod( diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index 0d6faf9f5..c8a6ea06a 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -130,7 +130,7 @@ Proof. destruct run_Block_for_Block. (* TODO: - check revm_interpreter::gas::Gas::record_cost - - check revm_interpreter::interpreter_types::LoopControl"::gas + - check revm_interpreter::interpreter_types::LoopControl::gas *) run_symbolic. Admitted. diff --git a/CoqOfRust/ruint/links/modular.v b/CoqOfRust/ruint/links/modular.v index fa1adceda..530fe0b9e 100644 --- a/CoqOfRust/ruint/links/modular.v +++ b/CoqOfRust/ruint/links/modular.v @@ -5,6 +5,7 @@ Require Import ruint.modular. (* impl Uint *) Module Impl_Uint. + (* Uint *) Definition Self (BITS LIMBS : Usize.t) : Set := Uint.t BITS LIMBS. From 75bbf59d4fee9990b14533983427794edc6776f3 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Wed, 26 Mar 2025 22:54:20 +0800 Subject: [PATCH 16/28] minor: fix parameters in `modular` --- CoqOfRust/ruint/links/modular.v | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/CoqOfRust/ruint/links/modular.v b/CoqOfRust/ruint/links/modular.v index 530fe0b9e..a7a84102b 100644 --- a/CoqOfRust/ruint/links/modular.v +++ b/CoqOfRust/ruint/links/modular.v @@ -12,27 +12,27 @@ Module Impl_Uint. (* pub fn add_mod(self, rhs: Self, modulus: Self) -> Self *) Instance run_add_mod (BITS LIMBS : Usize.t) - (x1 x2 : Self BITS LIMBS) : + (x1 x2 x3 : Self BITS LIMBS) : Run.Trait - (modular.Impl_ruint_Uint_BITS_LIMBS.add_mod (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ] + (modular.Impl_ruint_Uint_BITS_LIMBS.add_mod (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2; φ x3 ] (Self BITS LIMBS). - Admitted. + Admitted. (* pub fn mul_mod(self, rhs: Self, modulus: Self) -> Self *) Instance run_mul_mod (BITS LIMBS : Usize.t) - (x1 x2 : Self BITS LIMBS) : - Run.Trait - (modular.Impl_ruint_Uint_BITS_LIMBS.mul_mod (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ] - (Self BITS LIMBS). + (x1 x2 x3 : Self BITS LIMBS) : + Run.Trait + (modular.Impl_ruint_Uint_BITS_LIMBS.mul_mod (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2; φ x3 ] + (Self BITS LIMBS). Admitted. (* pub fn pow_mod(self, exp: Self, modulus: Self) -> Self *) Instance run_pow_mod (BITS LIMBS : Usize.t) - (x1 x2 : Self BITS LIMBS) : - Run.Trait - (modular.Impl_ruint_Uint_BITS_LIMBS.pow_mod (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ] - (Self BITS LIMBS). + (x1 x2 x3 : Self BITS LIMBS) : + Run.Trait + (modular.Impl_ruint_Uint_BITS_LIMBS.pow_mod (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2; φ x3 ] + (Self BITS LIMBS). Admitted. End Impl_Uint. From 0dda6e334821bb9ebb5655b52fb06ca9884c9613 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Wed, 26 Mar 2025 22:54:35 +0800 Subject: [PATCH 17/28] minor: progress --- .../instructions/links/arithmetic.v | 25 ++++++++++++++----- .../instructions/links/block_info.v | 8 +++--- 2 files changed, 23 insertions(+), 10 deletions(-) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v index 0c839682f..147bf9b95 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v @@ -42,8 +42,6 @@ Proof. cbn. eapply Run.Rewrite. { progress repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. - (* Seems like the code doesnt envolve proofs on `H` *) - (* progress repeat erewrite IsTraitAssociatedType_eq by apply run_Host_for_H. *) reflexivity. } destruct run_InterpreterTypes_for_WIRE. @@ -250,8 +248,23 @@ Proof. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. (* TODO: Uint::add_mod *) + (* + Trait + (add.add.Impl_ruint_Uint_BITS_LIMBS.wrapping_add + (Integer.IsLink.(φ) {| Integer.value := 256 |}) + (Integer.IsLink.(φ) {| Integer.value := 4 |})) [] [] + [lib.Uint.IsLink.(φ) value; lib.Uint.IsLink.(φ) value1] + (lib.Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}) + -------- + Trait + (modular.modular.Impl_ruint_Uint_BITS_LIMBS.add_mod + (Integer.IsLink.(φ) {| Integer.value := 256 |}) + (Integer.IsLink.(φ) {| Integer.value := 4 |})) [] [] + [lib.Uint.IsLink.(φ) value; lib.Uint.IsLink.(φ) value0; + lib.Uint.IsLink.(φ) value2] + (lib.Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}) + *) run_symbolic. - (* Admitted. *) Defined. (* @@ -281,8 +294,7 @@ Proof. destruct run_StackTrait_for_Stack. (* TODO: Uint::mul_mod *) run_symbolic. - Admitted. -(* Defined. *) +Defined. (* pub fn exp( @@ -312,7 +324,8 @@ Proof. destruct run_RuntimeFlag_for_RuntimeFlag. (* TODO: - calc.gas.calc.exp_cost - - Uint::pow*) + - Uint::pow + *) run_symbolic. Admitted. (* Defined. *) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index c8a6ea06a..3e2e44a5e 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -17,10 +17,10 @@ Import Impl_Gas. Import from.Impl_Uint. (* TODO(progress): - - finish `ruint` related components + - (PRIORITY) refer to `interpreter_types` on `block.v` to see anything missing - check revm_interpreter::gas::Gas::record_cost - check revm_interpreter::interpreter_types::LoopControl::gas - *) +*) (* pub fn chainid( @@ -191,8 +191,8 @@ Proof. destruct run_InterpreterTypes_for_WIRE. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. + destruct run_RuntimeFlag_for_RuntimeFlag. (* TODO: - - revm_interpreter::interpreter_types::RuntimeFlag::spec_id - BlockGetter::difficulty *) run_symbolic. @@ -251,8 +251,8 @@ Proof. destruct run_InterpreterTypes_for_WIRE. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. + destruct run_RuntimeFlag_for_RuntimeFlag. (* TODO: - - RuntimeFlag::spec_id - BlockGetter::base_fee *) run_symbolic. From 15f084290c993ddd2f9e43814ff045c030cefbcc Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Wed, 26 Mar 2025 23:04:57 +0800 Subject: [PATCH 18/28] feat: add `pow` links --- CoqOfRust/ruint/links/pow.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 CoqOfRust/ruint/links/pow.v diff --git a/CoqOfRust/ruint/links/pow.v b/CoqOfRust/ruint/links/pow.v new file mode 100644 index 000000000..efc396c43 --- /dev/null +++ b/CoqOfRust/ruint/links/pow.v @@ -0,0 +1,28 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import ruint.links.lib. +Require Import ruint.pow. + +Module Impl_Uint. + (* Uint *) + Definition Self (BITS LIMBS : Usize.t) : Set := + Uint.t BITS LIMBS. + + (* pub fn pow(self, exp: Self) -> Self *) + Instance run_pow + (BITS LIMBS : Usize.t) + (x1 x2 : Self BITS LIMBS) : + Run.Trait + (pow.Impl_ruint_Uint_BITS_LIMBS.pow (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ] + (Self BITS LIMBS). + Admitted. + + (* pub fn wrapping_pow(mut self, mut exp: Self) -> Self *) + Instance run_wrapping_pow + (BITS LIMBS : Usize.t) + (x1 x2 : Self BITS LIMBS) : + Run.Trait + (pow.Impl_ruint_Uint_BITS_LIMBS.wrapping_pow (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ] + (Self BITS LIMBS). + Admitted. +End Impl_Uint. \ No newline at end of file From 6a13bb330c239bdf1cd120cdebc9908db1c7cee8 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Thu, 27 Mar 2025 08:04:27 +0800 Subject: [PATCH 19/28] minor: progress on `arithmetic` --- .../revm/revm_interpreter/gas/links/calc.v | 17 +++++++++++- .../instructions/links/arithmetic.v | 27 +++++-------------- .../instructions/links/block_info.v | 1 + 3 files changed, 23 insertions(+), 22 deletions(-) diff --git a/CoqOfRust/revm/revm_interpreter/gas/links/calc.v b/CoqOfRust/revm/revm_interpreter/gas/links/calc.v index d62f3978c..616ad08bf 100644 --- a/CoqOfRust/revm/revm_interpreter/gas/links/calc.v +++ b/CoqOfRust/revm/revm_interpreter/gas/links/calc.v @@ -2,8 +2,10 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. Require Import core.num.mod. Require Import core.num.links.mod. -Require Import revm_interpreter.gas.calc. +Require Import revm_specification.links.hardfork. +Require Import CoqOfRust.revm.links.dependencies. Require revm_interpreter.gas.links.constants. +Require Import revm_interpreter.gas.calc. Import Impl_u64. @@ -23,3 +25,16 @@ Proof. constructor. run_symbolic. Defined. + +(* NOTE: since we don't have U256 for now, we use Usize instead *) +(* pub fn exp_cost(spec_id: SpecId, power: U256) -> Option *) +Instance run_exp_cost (spec_id : SpecId.t) (power : U256.t) : + Run.Trait + gas.calc.exp_cost [] [] [ φ spec_id; φ power ] + (option U64.t). +Proof. + constructor. + run_symbolic. + (* NOTE: Should I finish the proof? *) +Admitted. +(* Defined. *) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v index 147bf9b95..377df0056 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v @@ -1,17 +1,20 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. +Require Import revm.revm_interpreter.instructions.arithmetic. Require Import revm.revm_context_interface.links.host. Require Import revm.revm_interpreter.links.gas. Require Import revm.revm_interpreter.links.interpreter. Require Import revm.revm_interpreter.links.interpreter_types. Require Import revm.revm_interpreter.instructions.links.i256. -Require Import revm.revm_interpreter.instructions.arithmetic. -Require Import revm.revm_interpreter.instructions.i256. +(* TODO: see if its necessary to import `option` *) +(* Require Import core.links.option. *) Require Import ruint.links.add. Require Import ruint.links.cmp. Require Import ruint.links.div. Require Import ruint.links.mul. Require Import ruint.links.modular. +Require Import ruint.links.pow. +Require Import core.links.cmp. Import Impl_Gas. Import add.Impl_Uint. @@ -19,6 +22,7 @@ Import cmp.Impl_Uint. Import div.Impl_Uint. Import mul.Impl_Uint. Import modular.Impl_Uint. +Import pow.Impl_Uint. (* pub fn add( @@ -247,23 +251,6 @@ Proof. destruct run_InterpreterTypes_for_WIRE. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. - (* TODO: Uint::add_mod *) - (* - Trait - (add.add.Impl_ruint_Uint_BITS_LIMBS.wrapping_add - (Integer.IsLink.(φ) {| Integer.value := 256 |}) - (Integer.IsLink.(φ) {| Integer.value := 4 |})) [] [] - [lib.Uint.IsLink.(φ) value; lib.Uint.IsLink.(φ) value1] - (lib.Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}) - -------- - Trait - (modular.modular.Impl_ruint_Uint_BITS_LIMBS.add_mod - (Integer.IsLink.(φ) {| Integer.value := 256 |}) - (Integer.IsLink.(φ) {| Integer.value := 4 |})) [] [] - [lib.Uint.IsLink.(φ) value; lib.Uint.IsLink.(φ) value0; - lib.Uint.IsLink.(φ) value2] - (lib.Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}) - *) run_symbolic. Defined. @@ -292,7 +279,6 @@ Proof. destruct run_InterpreterTypes_for_WIRE. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. - (* TODO: Uint::mul_mod *) run_symbolic. Defined. @@ -324,7 +310,6 @@ Proof. destruct run_RuntimeFlag_for_RuntimeFlag. (* TODO: - calc.gas.calc.exp_cost - - Uint::pow *) run_symbolic. Admitted. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index 3e2e44a5e..780a06d5a 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -285,6 +285,7 @@ Proof. destruct run_StackTrait_for_Stack. (* TODO: - Runtimeflag::spec_id + NOTE: is there an issue with translation of blob_gasprice's `option`? - BlockGetter::blob_gasprice *) run_symbolic. From a99ed9cf1338f80be84c394392c8d1de0bbd9aff Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Thu, 27 Mar 2025 08:28:02 +0800 Subject: [PATCH 20/28] minor: reduce issues in `block_info` to `block` --- .../revm/revm_context_interface/links/block.v | 12 +++--- .../instructions/links/block_info.v | 40 +++++++++++++++---- 2 files changed, 39 insertions(+), 13 deletions(-) diff --git a/CoqOfRust/revm/revm_context_interface/links/block.v b/CoqOfRust/revm/revm_context_interface/links/block.v index f431f504e..11822efc5 100644 --- a/CoqOfRust/revm/revm_context_interface/links/block.v +++ b/CoqOfRust/revm/revm_context_interface/links/block.v @@ -120,14 +120,14 @@ Module BlockGetter. Run.Trait method [] [] [ φ self ] unit ). - (* (* NOTE: Question: since `BlockGetter` "inherhits" several methods from `Block` trait, + (* NOTE: Question: since `BlockGetter` "inherhits" several methods from `Block` trait, do we still need to additionally write instances for these methods? *) - (* fn timestamp(&self) -> u64; *) - Definition Run_timestamp (Self : Set) `{Link Self} : Set := - TraitMethod.C (trait Self) "timestamp" (fun method => + (* NOTE: to test on `block_info::block_number` *) + Definition Run_number (Self : Set) `{Link Self} : Set := + TraitMethod.C (trait Self) "number" (fun method => forall (self : Ref.t Pointer.Kind.Ref Self), Run.Trait method [] [] [ φ self ] U64.t - ). *) + ). Class Run (Self : Set) `{Link Self} (types : Types.t) `{Types.AreLinks types} : Set := { Block_IsAssociated : @@ -136,6 +136,6 @@ Module BlockGetter. "Block" (Φ types.(Types.Block)); run_Block_for_Block : Block.Run types.(Types.Block); block : Run_block Self; - (* timestamp : Run_timestamp Self; *) + (* number : Run_number Self; *) }. End BlockGetter. \ No newline at end of file diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index 780a06d5a..cc4a9b0fa 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -18,8 +18,6 @@ Import from.Impl_Uint. (* TODO(progress): - (PRIORITY) refer to `interpreter_types` on `block.v` to see anything missing - - check revm_interpreter::gas::Gas::record_cost - - check revm_interpreter::interpreter_types::LoopControl::gas *) (* @@ -129,8 +127,8 @@ Proof. destruct run_BlockGetter. destruct run_Block_for_Block. (* TODO: - - check revm_interpreter::gas::Gas::record_cost - - check revm_interpreter::interpreter_types::LoopControl::gas + - BlockGetter::timestamp + - BlockGetter::block *) run_symbolic. Admitted. @@ -148,6 +146,8 @@ Instance block_number {WIRE H : Set} `{Link WIRE} `{Link H} {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} + (run_Host_for_H : Host.Run H H_types) (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) (_host : Ref.t Pointer.Kind.MutRef H) : Run.Trait @@ -163,6 +163,13 @@ Proof. destruct run_InterpreterTypes_for_WIRE. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. + destruct run_Host_for_H. + destruct run_BlockGetter. + destruct run_Block_for_Block. + (* TODO: + - BlockGetter::number (what's still missing here?) + - BlockGetter::block + *) run_symbolic. Admitted. @@ -175,6 +182,8 @@ pub fn difficulty( Instance difficulty {WIRE H : Set} `{Link WIRE} `{Link H} {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} + (run_Host_for_H : Host.Run H H_types) (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) (_host : Ref.t Pointer.Kind.MutRef H) : @@ -192,8 +201,11 @@ Proof. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. destruct run_RuntimeFlag_for_RuntimeFlag. + destruct run_Host_for_H. + destruct run_BlockGetter. + destruct run_Block_for_Block. (* TODO: - - BlockGetter::difficulty + - revm_interpreter::instructions::utility::IntoU256::into_u256 *) run_symbolic. Admitted. @@ -207,7 +219,9 @@ pub fn gaslimit( Instance gaslimit {WIRE H : Set} `{Link WIRE} `{Link H} {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (run_Host_for_H : Host.Run H H_types) (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) (_host : Ref.t Pointer.Kind.MutRef H) : Run.Trait @@ -223,6 +237,13 @@ Proof. destruct run_InterpreterTypes_for_WIRE. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. + destruct run_Host_for_H. + destruct run_BlockGetter. + destruct run_Block_for_Block. + (* TODO: + - BlockGetter::gas_limit + - BlockGetter::block + *) run_symbolic. Admitted. @@ -267,7 +288,9 @@ pub fn blob_basefee( Instance blob_basefee {WIRE H : Set} `{Link WIRE} `{Link H} {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (run_Host_for_H : Host.Run H H_types) (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) (_host : Ref.t Pointer.Kind.MutRef H) : Run.Trait @@ -283,9 +306,12 @@ Proof. destruct run_InterpreterTypes_for_WIRE. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. + destruct run_RuntimeFlag_for_RuntimeFlag. + destruct run_Host_for_H. + destruct run_BlockGetter. + destruct run_Block_for_Block. (* TODO: - - Runtimeflag::spec_id - NOTE: is there an issue with translation of blob_gasprice's `option`? + - BlockGetter::block - BlockGetter::blob_gasprice *) run_symbolic. From fcc17f92e70ccfe325d5a65c7fc5d7821960aeb0 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Thu, 27 Mar 2025 08:51:05 +0800 Subject: [PATCH 21/28] minor: progress on `block` --- .../revm/revm_context_interface/links/block.v | 19 +++++-------------- .../instructions/links/block_info.v | 8 ++++++++ 2 files changed, 13 insertions(+), 14 deletions(-) diff --git a/CoqOfRust/revm/revm_context_interface/links/block.v b/CoqOfRust/revm/revm_context_interface/links/block.v index 11822efc5..5c4b7a262 100644 --- a/CoqOfRust/revm/revm_context_interface/links/block.v +++ b/CoqOfRust/revm/revm_context_interface/links/block.v @@ -114,28 +114,19 @@ Module BlockGetter. Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t := ("revm_context_interface::block::BlockGetter", [], [], Φ Self). - Definition Run_block (Self : Set) `{Link Self} : Set := + Definition Run_block (Self : Set) `{Link Self} (types : Types.t) `{Types.AreLinks types} : Set := TraitMethod.C (trait Self) "block" (fun method => forall (self : Ref.t Pointer.Kind.Ref Self), - Run.Trait method [] [] [ φ self ] unit + Run.Trait method [] [] [ φ self ] (types.(Types.Block)) ). - (* NOTE: Question: since `BlockGetter` "inherhits" several methods from `Block` trait, - do we still need to additionally write instances for these methods? *) - (* NOTE: to test on `block_info::block_number` *) - Definition Run_number (Self : Set) `{Link Self} : Set := - TraitMethod.C (trait Self) "number" (fun method => - forall (self : Ref.t Pointer.Kind.Ref Self), - Run.Trait method [] [] [ φ self ] U64.t - ). - - Class Run (Self : Set) `{Link Self} (types : Types.t) `{Types.AreLinks types} : Set := { + Class Run (Self : Set) `{Link Self} (types : Types.t) `{Types.AreLinks types} : Set := { Block_IsAssociated : IsTraitAssociatedType "revm_context_interface::block::BlockGetter" [] [] (Φ Self) "Block" (Φ types.(Types.Block)); run_Block_for_Block : Block.Run types.(Types.Block); - block : Run_block Self; - (* number : Run_number Self; *) + (* TODO: fix this *) + block : Run_block Self types.(Types.Block); }. End BlockGetter. \ No newline at end of file diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index cc4a9b0fa..cd6d10c2c 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -56,6 +56,10 @@ Proof. destruct run_Host_for_H. destruct run_CfgGetter. destruct run_Cfg_for_Cfg. + (* TODO: + - BlockGetter::beneficiary + - BlockGetter::block + *) run_symbolic. Defined. @@ -90,6 +94,10 @@ Proof. destruct run_BlockGetter. destruct run_Block_for_Block. destruct alloy_primitives.bits.links.fixed.Impl_Into_U256_for_FixedBytes.run. + (* TODO: + - BlockGetter::beneficiary + - BlockGetter::block + *) run_symbolic. Admitted. From f85919492b47c485860c7eabb5f2b38f2b9bbb21 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Thu, 27 Mar 2025 09:12:23 +0800 Subject: [PATCH 22/28] minor: progress --- CoqOfRust/revm/revm_context_interface/links/block.v | 3 +-- .../revm/revm_interpreter/instructions/links/block_info.v | 6 +----- 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/CoqOfRust/revm/revm_context_interface/links/block.v b/CoqOfRust/revm/revm_context_interface/links/block.v index 5c4b7a262..46232ce44 100644 --- a/CoqOfRust/revm/revm_context_interface/links/block.v +++ b/CoqOfRust/revm/revm_context_interface/links/block.v @@ -126,7 +126,6 @@ Module BlockGetter. "revm_context_interface::block::BlockGetter" [] [] (Φ Self) "Block" (Φ types.(Types.Block)); run_Block_for_Block : Block.Run types.(Types.Block); - (* TODO: fix this *) - block : Run_block Self types.(Types.Block); + block : Run_block Self types; }. End BlockGetter. \ No newline at end of file diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index cd6d10c2c..8d4c34247 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -56,10 +56,6 @@ Proof. destruct run_Host_for_H. destruct run_CfgGetter. destruct run_Cfg_for_Cfg. - (* TODO: - - BlockGetter::beneficiary - - BlockGetter::block - *) run_symbolic. Defined. @@ -175,7 +171,7 @@ Proof. destruct run_BlockGetter. destruct run_Block_for_Block. (* TODO: - - BlockGetter::number (what's still missing here?) + - BlockGetter::number - BlockGetter::block *) run_symbolic. From 0998589b32dc81002dfe9e5a80046f96057cb2c4 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Thu, 27 Mar 2025 12:27:21 +0800 Subject: [PATCH 23/28] minor: comment --- CoqOfRust/revm/revm_context_interface/links/block.v | 1 + 1 file changed, 1 insertion(+) diff --git a/CoqOfRust/revm/revm_context_interface/links/block.v b/CoqOfRust/revm/revm_context_interface/links/block.v index 46232ce44..a2223514e 100644 --- a/CoqOfRust/revm/revm_context_interface/links/block.v +++ b/CoqOfRust/revm/revm_context_interface/links/block.v @@ -117,6 +117,7 @@ Module BlockGetter. Definition Run_block (Self : Set) `{Link Self} (types : Types.t) `{Types.AreLinks types} : Set := TraitMethod.C (trait Self) "block" (fun method => forall (self : Ref.t Pointer.Kind.Ref Self), + (* Is there something wrong with `Self.Block` here? *) Run.Trait method [] [] [ φ self ] (types.(Types.Block)) ). From 8f32e0640bb2e7c14d959a6974949f98a80e9833 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Thu, 27 Mar 2025 18:19:28 +0800 Subject: [PATCH 24/28] minor: deleted Host parameter that is never used --- CoqOfRust/revm/revm_interpreter/links/instructions.v | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/CoqOfRust/revm/revm_interpreter/links/instructions.v b/CoqOfRust/revm/revm_interpreter/links/instructions.v index f39a68435..6afdaac76 100644 --- a/CoqOfRust/revm/revm_interpreter/links/instructions.v +++ b/CoqOfRust/revm/revm_interpreter/links/instructions.v @@ -21,7 +21,6 @@ Instance run_instruction_table {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (run_Host_for_H : Host.Run H H_types) : Run.Trait instructions.instruction_table [] [ Φ WIRE; Φ H ] [] @@ -42,7 +41,7 @@ Proof. run_symbolic. } { (* add *) - set (f := Function2.of_run (run_add run_InterpreterTypes_for_WIRE run_Host_for_H)). + set (f := Function2.of_run (run_add run_InterpreterTypes_for_WIRE)). change (Value.Closure _) with (φ f). run_symbolic. } @@ -53,6 +52,13 @@ Proof. } Defined. +(* ++ {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} +. (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) ++ (run_Host_for_H : Host.Run H H_types) ++ : +*) + (* pub const fn instruction( opcode: u8, From 5138fdf6719e03bb63275460de1ac2b53a37b75a Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Thu, 27 Mar 2025 18:21:55 +0800 Subject: [PATCH 25/28] minor: resetted `instructions` --- CoqOfRust/revm/revm_interpreter/links/instructions.v | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/CoqOfRust/revm/revm_interpreter/links/instructions.v b/CoqOfRust/revm/revm_interpreter/links/instructions.v index 6afdaac76..ef31f448e 100644 --- a/CoqOfRust/revm/revm_interpreter/links/instructions.v +++ b/CoqOfRust/revm/revm_interpreter/links/instructions.v @@ -52,13 +52,6 @@ Proof. } Defined. -(* -+ {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} -. (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) -+ (run_Host_for_H : Host.Run H H_types) -+ : -*) - (* pub const fn instruction( opcode: u8, @@ -77,8 +70,4 @@ Instance run_instruction Proof. constructor. run_symbolic. -(* TODO: resolve the incomplete run in future PRs - In this file our major change results from adding `H` parameters in the `run_add` function -*) -(* Admitted. *) Defined. From fbef042c1e482f3d902d7458afead4233a88eb27 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Thu, 27 Mar 2025 18:22:01 +0800 Subject: [PATCH 26/28] minor: comment --- .../revm/revm_interpreter/instructions/links/arithmetic.v | 3 --- 1 file changed, 3 deletions(-) diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v index 377df0056..9523ccb0a 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v @@ -6,8 +6,6 @@ Require Import revm.revm_interpreter.links.gas. Require Import revm.revm_interpreter.links.interpreter. Require Import revm.revm_interpreter.links.interpreter_types. Require Import revm.revm_interpreter.instructions.links.i256. -(* TODO: see if its necessary to import `option` *) -(* Require Import core.links.option. *) Require Import ruint.links.add. Require Import ruint.links.cmp. Require Import ruint.links.div. @@ -35,7 +33,6 @@ Instance run_add {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (run_Host_for_H : Host.Run H H_types) (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) (_host : Ref.t Pointer.Kind.MutRef H) : Run.Trait From 3af7b5d2fe2107b91dd0103a214785217cc0bebc Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Thu, 27 Mar 2025 18:50:09 +0800 Subject: [PATCH 27/28] minor: progress --- .../revm/revm_interpreter/gas/links/calc.v | 1 - .../instructions/links/arithmetic.v | 2 +- .../instructions/links/block_info.v | 27 +++++++++++-------- 3 files changed, 17 insertions(+), 13 deletions(-) diff --git a/CoqOfRust/revm/revm_interpreter/gas/links/calc.v b/CoqOfRust/revm/revm_interpreter/gas/links/calc.v index 616ad08bf..ccf6f22fe 100644 --- a/CoqOfRust/revm/revm_interpreter/gas/links/calc.v +++ b/CoqOfRust/revm/revm_interpreter/gas/links/calc.v @@ -26,7 +26,6 @@ Proof. run_symbolic. Defined. -(* NOTE: since we don't have U256 for now, we use Usize instead *) (* pub fn exp_cost(spec_id: SpecId, power: U256) -> Option *) Instance run_exp_cost (spec_id : SpecId.t) (power : U256.t) : Run.Trait diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v index 9523ccb0a..edb5bf56d 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v @@ -309,7 +309,7 @@ Proof. - calc.gas.calc.exp_cost *) run_symbolic. - Admitted. +Admitted. (* Defined. *) (* diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index 8d4c34247..454329f07 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -16,10 +16,6 @@ Import Impl_SpecId. Import Impl_Gas. Import from.Impl_Uint. -(* TODO(progress): - - (PRIORITY) refer to `interpreter_types` on `block.v` to see anything missing -*) - (* pub fn chainid( interpreter: &mut Interpreter, @@ -80,7 +76,8 @@ Proof. constructor. cbn. eapply Run.Rewrite. { - repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_Host_for_H. reflexivity. } destruct run_InterpreterTypes_for_WIRE. @@ -121,7 +118,8 @@ Proof. constructor. cbn. eapply Run.Rewrite. { - repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_Host_for_H. reflexivity. } destruct run_InterpreterTypes_for_WIRE. @@ -161,7 +159,8 @@ Proof. constructor. cbn. eapply Run.Rewrite. { - repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_Host_for_H. reflexivity. } destruct run_InterpreterTypes_for_WIRE. @@ -198,7 +197,8 @@ Proof. constructor. cbn. eapply Run.Rewrite. { - repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_Host_for_H. reflexivity. } destruct run_InterpreterTypes_for_WIRE. @@ -235,7 +235,8 @@ Proof. constructor. cbn. eapply Run.Rewrite. { - repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_Host_for_H. reflexivity. } destruct run_InterpreterTypes_for_WIRE. @@ -260,8 +261,10 @@ pub fn basefee( Instance basefee {WIRE H : Set} `{Link WIRE} `{Link H} {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (run_Host_for_H : Host.Run H H_types) (_host : Ref.t Pointer.Kind.MutRef H) : Run.Trait instructions.block_info.basefee [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] @@ -270,7 +273,8 @@ Proof. constructor. cbn. eapply Run.Rewrite. { - repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_Host_for_H. reflexivity. } destruct run_InterpreterTypes_for_WIRE. @@ -304,7 +308,8 @@ Proof. constructor. cbn. eapply Run.Rewrite. { - repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE. + progress repeat erewrite IsTraitAssociatedType_eq by apply run_Host_for_H. reflexivity. } destruct run_InterpreterTypes_for_WIRE. From 0c2f5b4dec85f0ce1eb97358e576e17c292ddb40 Mon Sep 17 00:00:00 2001 From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com> Date: Thu, 27 Mar 2025 20:22:39 +0800 Subject: [PATCH 28/28] feat: Resolved most dependencies for `block_info` --- CoqOfRust/core/links/option.v | 8 +++ .../revm/revm_context_interface/links/block.v | 3 +- .../instructions/links/block_info.v | 53 +++++++++---------- 3 files changed, 35 insertions(+), 29 deletions(-) diff --git a/CoqOfRust/core/links/option.v b/CoqOfRust/core/links/option.v index 6a2f5dd1a..7c96540fe 100644 --- a/CoqOfRust/core/links/option.v +++ b/CoqOfRust/core/links/option.v @@ -100,4 +100,12 @@ Module Impl_Option. (option.Impl_core_option_Option_T.unwrap_unchecked (Φ T)) [] [] [ φ self ] T. Admitted. + + (* pub fn unwrap_or_default(self) -> T *) + Instance run_unwrap_or_default {T : Set} `{Link T} + (self : Self T) : + Run.Trait + (option.Impl_core_option_Option_T.unwrap_or_default (Φ T)) [] [] [ φ self ] + T. + Admitted. End Impl_Option. diff --git a/CoqOfRust/revm/revm_context_interface/links/block.v b/CoqOfRust/revm/revm_context_interface/links/block.v index a2223514e..b090dfff7 100644 --- a/CoqOfRust/revm/revm_context_interface/links/block.v +++ b/CoqOfRust/revm/revm_context_interface/links/block.v @@ -117,8 +117,7 @@ Module BlockGetter. Definition Run_block (Self : Set) `{Link Self} (types : Types.t) `{Types.AreLinks types} : Set := TraitMethod.C (trait Self) "block" (fun method => forall (self : Ref.t Pointer.Kind.Ref Self), - (* Is there something wrong with `Self.Block` here? *) - Run.Trait method [] [] [ φ self ] (types.(Types.Block)) + Run.Trait method [] [] [ φ self ] (Ref.t Pointer.Kind.Ref types.(Types.Block)) ). Class Run (Self : Set) `{Link Self} (types : Types.t) `{Types.AreLinks types} : Set := { diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v index 454329f07..57a9bac98 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v @@ -11,10 +11,12 @@ Require Import revm.revm_specification.links.hardfork. Require Import revm.revm_context_interface.links.cfg. Require Import ruint.links.from. Require Import core.convert.links.mod. +Require Import core.links.option. Import Impl_SpecId. Import Impl_Gas. Import from.Impl_Uint. +Import Impl_Option. (* pub fn chainid( @@ -55,6 +57,18 @@ Proof. run_symbolic. Defined. +(* Instance run_coinbase + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (run_Host_for_H : Host.Run H H_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Trait block.(TraitMethod.method) [] [] + [Ref.IsLink.(φ) (Ref.cast_to Pointer.Kind.Ref _host)] + (Ref.t Pointer.Kind.Ref H_types.(Host.Types.Block)). *) + (* pub fn coinbase( interpreter: &mut Interpreter, @@ -87,9 +101,9 @@ Proof. destruct run_BlockGetter. destruct run_Block_for_Block. destruct alloy_primitives.bits.links.fixed.Impl_Into_U256_for_FixedBytes.run. - (* TODO: - - BlockGetter::beneficiary - - BlockGetter::block + (* TODO: resolve axiomatization for: + - Impl_Address::into_word(?) + - FixedBytes::into() *) run_symbolic. Admitted. @@ -128,12 +142,8 @@ Proof. destruct run_Host_for_H. destruct run_BlockGetter. destruct run_Block_for_Block. - (* TODO: - - BlockGetter::timestamp - - BlockGetter::block - *) run_symbolic. -Admitted. +Defined. (* pub fn block_number( @@ -169,12 +179,8 @@ Proof. destruct run_Host_for_H. destruct run_BlockGetter. destruct run_Block_for_Block. - (* TODO: - - BlockGetter::number - - BlockGetter::block - *) run_symbolic. -Admitted. +Defined. (* pub fn difficulty( @@ -208,6 +214,7 @@ Proof. destruct run_Host_for_H. destruct run_BlockGetter. destruct run_Block_for_Block. + destruct alloy_primitives.bits.links.fixed.Impl_Into_U256_for_FixedBytes.run. (* TODO: - revm_interpreter::instructions::utility::IntoU256::into_u256 *) @@ -245,12 +252,8 @@ Proof. destruct run_Host_for_H. destruct run_BlockGetter. destruct run_Block_for_Block. - (* TODO: - - BlockGetter::gas_limit - - BlockGetter::block - *) run_symbolic. -Admitted. +Defined. (* pub fn basefee( @@ -281,11 +284,11 @@ Proof. destruct run_LoopControl_for_Control. destruct run_StackTrait_for_Stack. destruct run_RuntimeFlag_for_RuntimeFlag. - (* TODO: - - BlockGetter::base_fee - *) + destruct run_Host_for_H. + destruct run_BlockGetter. + destruct run_Block_for_Block. run_symbolic. -Admitted. +Defined. (* pub fn blob_basefee( @@ -319,9 +322,5 @@ Proof. destruct run_Host_for_H. destruct run_BlockGetter. destruct run_Block_for_Block. - (* TODO: - - BlockGetter::block - - BlockGetter::blob_gasprice - *) run_symbolic. -Admitted. \ No newline at end of file +Defined. \ No newline at end of file