WIP: Link file for block_info.v

CoqOfRust/revm/revm_context_interface/links/block.v

@@ -0,0 +1 @@
+(* Initial stub *)

CoqOfRust/revm/revm_context_interface/links/cfg.v

@@ -31,3 +31,67 @@ Module CreateScheme.
       end;
   }.
 End CreateScheme.
+
+(* 
+#[auto_impl(&, &mut, Box, Arc)]
+pub trait Cfg {
+    type Spec: Into<SpecId> + Clone;
+
+    fn chain_id(&self) -> u64;
+
+    // Specification id that is set.
+    fn spec(&self) -> Self::Spec;
+
+    /// Returns the blob target and max count for the given spec id.
+    ///
+    /// EIP-7840: Add blob schedule to execution client configuration files
+    fn blob_max_count(&self, spec_id: SpecId) -> u8;
+
+    fn max_code_size(&self) -> usize;
+
+    fn is_eip3607_disabled(&self) -> bool;
+
+    fn is_balance_check_disabled(&self) -> bool;
+
+    fn is_block_gas_limit_disabled(&self) -> bool;
+
+    fn is_nonce_check_disabled(&self) -> bool;
+
+    fn is_base_fee_check_disabled(&self) -> bool;
+}
+*)
+Module Cfg.
+  (* type Spec: Into<SpecId> + Clone; *)
+  Module Types.
+    Record t : Type := {
+      Spec : Set;
+    }.
+
+
+    Class AreLinks (types : t) : Set := {
+      H_Spec : Link types.(Spec);
+    }.
+
+    Global Instance IsLinkSpec (types : t) (H : AreLinks types) : Link types.(Spec) :=
+      H.(H_Spec _).
+  End Types.
+
+  Definition Run_chain_id (Self : Set) `{Link Self} : Set :=
+    {chain_id @
+      IsTraitMethod.t "revm_context_interface::cfg::Cfg" [] [] (Φ Self) "chain_id" chain_id *
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+        {{ chain_id [] [] [ φ self ] 🔽 U64.t }}
+    }.
+
+  (* NOTE: Is this the right design for `Run`'s parameters? *)
+  Record Run (Self : Set) `{Link Self} (types : Types.t) 
+    `{Types.AreLinks types} : Set := 
+  {
+    Spec_IsAssociated :
+      IsTraitAssociatedType
+        "revm_context_interface::cfg::Cfg" [] [] (Φ Self)
+        "Spec" (Φ types.(Types.Spec));
+    (* run_StackTrait_for_Stack : StackTrait.Run types.(Types.Stack); *) (* TODO: Do we need to implement `Into` for Spec? *)
+    chain_id : Run_chain_id Self;
+  }.
+End Cfg.

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

@@ -6,9 +6,11 @@ Require Import revm.revm_interpreter.links.interpreter.
 Require Import revm.revm_interpreter.links.interpreter_types.
 Require Import revm.revm_interpreter.instructions.arithmetic.
 Require Import ruint.links.add.
+Require Import ruint.links.mul.
 
 Import Impl_Gas.
-Import Impl_Uint.
+Import add.Impl_Uint.
+Import mul.Impl_Uint.
 
 (*
 pub fn add<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -33,10 +35,158 @@ Proof.
     reflexivity.
   }
   destruct run_InterpreterTypes_for_WIRE.
-  destruct run_StackTrait_for_Stack.
-  destruct popn_top as [popn_top [H_popn_top run_popn_top]].
   destruct run_LoopControl_for_Control.
   destruct gas as [gas [H_gas run_gas]].
   destruct set_instruction_result as [set_instruction_result [H_set_instruction_result run_set_instruction_result]].
-  run_symbolic.
+  destruct run_StackTrait_for_Stack.
+  destruct popn_top as [popn_top [H_popn_top run_popn_top]].
+  run_symbolic. 
 Defined.
+
+(*
+pub fn mul<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    _host: &mut H,
+) {
+    gas!(interpreter, gas::LOW);
+    popn_top!([op1], op2, interpreter);
+    *op2 = op1.wrapping_mul( *op2);
+}
+*)
+Instance run_mul
+    {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)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.arithmetic.mul [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+  Proof.
+    constructor.
+    cbn.
+    eapply Run.Rewrite. {
+      repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE.
+      reflexivity.
+    }
+    destruct run_InterpreterTypes_for_WIRE.
+    destruct run_LoopControl_for_Control.
+    destruct gas as [gas [H_gas run_gas]].
+    destruct set_instruction_result as [set_instruction_result [H_set_instruction_result run_set_instruction_result]].
+    destruct run_StackTrait_for_Stack.
+    destruct popn_top as [popn_top [H_popn_top run_popn_top]].
+    run_symbolic. 
+  Defined.
+
+(*
+pub fn sub<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    _host: &mut H,
+) 
+*)
+Instance run_sub
+    {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)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.arithmetic.sub [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+  Proof.
+    constructor.
+    cbn.
+    eapply Run.Rewrite. {
+      repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE.
+      reflexivity.
+    }
+    destruct run_InterpreterTypes_for_WIRE.
+    destruct run_LoopControl_for_Control.
+    destruct gas as [gas [H_gas run_gas]].
+    destruct set_instruction_result as [set_instruction_result [H_set_instruction_result run_set_instruction_result]].
+    destruct run_StackTrait_for_Stack.
+    destruct popn_top as [popn_top [H_popn_top run_popn_top]].
+    run_symbolic. 
+  Defined.
+
+(*
+pub fn div<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    _host: &mut H,
+) 
+*)
+Instance run_div
+    {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)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.arithmetic.div [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+  Proof.
+    constructor.
+    cbn.
+    eapply Run.Rewrite. {
+      repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE.
+      reflexivity.
+    }
+    destruct run_InterpreterTypes_for_WIRE.
+    destruct run_LoopControl_for_Control.
+    destruct gas as [gas [H_gas run_gas]].
+    destruct set_instruction_result as [set_instruction_result [H_set_instruction_result run_set_instruction_result]].
+    destruct run_StackTrait_for_Stack.
+    destruct popn_top as [popn_top [H_popn_top run_popn_top]].
+    (* TODO: figure out the rest *)
+    run_symbolic. 
+    Admitted.
+  (* Defined. *)
+
+(*
+pub fn sdiv<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    _host: &mut H,
+) 
+*)
+
+(*
+pub fn rem<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    _host: &mut H,
+) 
+*)
+
+(*
+pub fn smod<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    _host: &mut H,
+) 
+*)
+
+(*
+pub fn addmod<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    _host: &mut H,
+) 
+*)
+
+(*
+pub fn mulmod<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    _host: &mut H,
+) 
+*)
+
+(*
+pub fn exp<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    _host: &mut H,
+) 
+*)
+
+(*
+pub fn signextend<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    _host: &mut H,
+) 
+*)

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

@@ -0,0 +1,111 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+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.block_info.
+Require Import revm.revm_specification.links.hardfork.
+Require Import revm.revm_context_interface.links.cfg.
+Require Import ruint.links.from.
+
+Import Impl_SpecId.
+Import Impl_Gas.
+Import from.Impl_Uint.
+
+(*
+pub fn chainid<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    host: &mut H,
+) {
+    check!(interpreter, ISTANBUL);
+    gas!(interpreter, gas::BASE);
+    push!(interpreter, U256::from(host.cfg().chain_id()));
+  }
+*)
+Instance run_chainid
+  {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)
+  (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+  (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.block_info.chainid [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+  Proof.
+    constructor.
+    cbn.
+    eapply Run.Rewrite. {
+      repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE.
+      reflexivity.
+    }
+    destruct run_InterpreterTypes_for_WIRE.
+    destruct run_RuntimeFlag_for_RuntimeFlag.
+    destruct spec_id as [spec_id [H_spec_id  run_spec_id]].
+    destruct run_LoopControl_for_Control.
+    destruct set_instruction_result as [set_instruction_result [H_set_instruction_result run_set_instruction_result]].
+    destruct gas as [gas [H_gas run_gas]].
+    destruct run_StackTrait_for_Stack.
+    destruct push as [push [H_push run_push]].
+    (* TODO: 
+    - Finish link for "revm_context_interface::cfg::Cfg" trait to `run_chain_id`
+    *)
+    (* 
+    CoqOfRust.M.LowM.CallPrimitive
+      (Primitive.GetTraitMethod
+        "revm_context_interface::cfg::Cfg"
+        (Ty.associated_in_trait
+            "revm_context_interface::cfg::CfgGetter"
+            [] [] H1.(Φ _) "Cfg") [] []
+        "chain_id" [] [])
+      (fun v : Value.t =>
+      CoqOfRust.M.LowM.CallPrimitive
+        (Primitive.GetTraitMethod
+            "revm_context_interface::cfg::CfgGetter"
+            H1.(Φ _) [] [] "cfg" [] [])
+        (fun v0 : Value.t =>
+          CoqOfRust.M.LowM.CallPrimitive
+            (CoqOfRust.M.Primitive.StateRead
+              (Ref.IsLink.(φ)
+                  (Ref.immediate
+                    Pointer.Kind.Raw
+                    _host)))
+            (fun v1 : Value.t =>
+    *)
+    run_symbolic.
+  Admitted.
+  (* Defined. *)
+
+(*
+pub fn coinbase<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    host: &mut H,
+)
+*)
+Instance run_coinbase
+  {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)
+  (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+  (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.block_info.coinbase [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+  Proof. 
+    constructor.
+    cbn.
+    eapply Run.Rewrite. {
+      repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE.
+      reflexivity.
+    }
+    destruct run_InterpreterTypes_for_WIRE.
+    destruct run_LoopControl_for_Control.
+    destruct gas as [gas [H_gas run_gas]].
+    destruct set_instruction_result as [set_instruction_result [H_set_instruction_result run_set_instruction_result]].
+    destruct run_StackTrait_for_Stack.
+    destruct push as [push [H_push run_push]].
+    (* TODO: fill in links for
+    - core::convert::Into::into 
+    - revm_context_interface::block::Block::beneficiary 
+    - revm_context_interface::block::Block::block *)
+    run_symbolic.
+  Admitted.

CoqOfRust/revm/types.v

@@ -7481,3 +7481,5 @@ Module RecoveredAuthorization.
       ]
   }.
 End RecoveredAuthorization.
+
+(* TODO: Should I create `Cfg` type here? *)

CoqOfRust/ruint/links/add.v

@@ -16,4 +16,13 @@ Module Impl_Uint.
       (add.Impl_ruint_Uint_BITS_LIMBS.wrapping_add (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ]
       (Self BITS LIMBS).
   Admitted.
+
+  (* pub const fn wrapping_add(self, rhs: Self) -> Self *)
+  Instance run_wrapping_sub
+    (BITS LIMBS : Usize.t)
+    (x1 x2 : Self BITS LIMBS) :
+  Run.Trait
+    (add.Impl_ruint_Uint_BITS_LIMBS.wrapping_sub (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ]
+    (Self BITS LIMBS).
+  Admitted.
 End Impl_Uint.