Link file for block_info.v, Part 2

CoqOfRust/core/convert/links/mod.v

@@ -28,14 +28,16 @@ pub trait Into<T>: 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.

CoqOfRust/revm/links/dependencies.v

@@ -7,13 +7,10 @@ Require Import core.links.clone.
 Require Import core.links.default.
 Require Import ruint.links.lib.
 
-(* 
-TODO: 
-- Start link with beneficiary's Address return type
-- In `beneficiary`, link it to Address type(?)
-- Link Addesss::into_word
-- Link Uint::into
-*)
+Module U256.
+  Definition t : Set :=
+    Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}.
+End U256.
 
 Module alloy_primitives.
   Module bits.
@@ -60,11 +57,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 +74,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.
@@ -228,19 +240,10 @@ 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 *)
 
-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 |}.

CoqOfRust/revm/revm_context_interface/links/block.v

@@ -114,18 +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
+      (* Is there something wrong with `Self.Block` here? *)
+        Run.Trait method [] [] [ φ self ] (types.(Types.Block))
     ).
 
-  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;
+    block : Run_block Self types;
   }.
 End BlockGetter.

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<u64> *)
+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. *)

CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v

@@ -1,20 +1,28 @@
 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.arithmetic.
+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.
 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.
 Import cmp.Impl_Uint.
 Import div.Impl_Uint.
 Import mul.Impl_Uint.
+Import modular.Impl_Uint.
+Import pow.Impl_Uint.
 
 (*
 pub fn add<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -38,8 +46,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.
@@ -161,10 +167,8 @@ Proof.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
-  (* TODO: revm_interpreter::instructions::i256::i256_div *)
   run_symbolic.
-(* Defined. *)
-Admitted.
+Defined.
 
 (*
 pub fn rem<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -219,10 +223,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<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -249,10 +251,8 @@ Proof.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
-  (* TODO: Uint::add_mod *)
   run_symbolic.
-  Admitted.
-(* Defined. *)
+Defined.
 
 (*
 pub fn mulmod<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -279,10 +279,8 @@ Proof.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
-  (* TODO: Uint::mul_mod *)
   run_symbolic.
-  Admitted.
-(* Defined. *)
+Defined.
 
 (*
 pub fn exp<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -312,7 +310,7 @@ Proof.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   (* TODO:
   - calc.gas.calc.exp_cost
-  - Uint::pow*)
+  *)
   run_symbolic.
   Admitted.
 (* Defined. *)