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/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.
@@ -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. `i256_div` seems to be unlinkable. My tried to generate an instance but it seems to be unrelated.
+  *)
   run_symbolic.
 (* Defined. *)
 Admitted.

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
@@ -60,9 +58,7 @@ Proof.
   destruct run_CfgGetter.
   destruct run_Cfg_for_Cfg.
   run_symbolic.
-  (* TODO: check `cfg::cfg` *)
-Admitted.
-(* Defined. *)
+Defined.
 
 (*
 pub fn coinbase<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -94,6 +90,8 @@ 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 )  . *)
   run_symbolic.
 Admitted.
 

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

@@ -1 +1,28 @@
-(* Initial stub *)
+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.
+
+(* 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;
+}.
+*)