diff --git a/CoqOfRust/alloy_primitives/links/common.v b/CoqOfRust/alloy_primitives/links/common.v
new file mode 100644
index 000000000..f3a650e97
--- /dev/null
+++ b/CoqOfRust/alloy_primitives/links/common.v
@@ -0,0 +1,29 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.bits.links.address.
+Require Import alloy_primitives.common.
+
+(*
+pub enum TxKind {
+    Create,
+    Call(Address),
+}
+*)
+Module TxKind.
+  Inductive t : Set :=
+  | Create
+  | Call (address : Address.t).
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "alloy_primitives::common::TxKind";
+    φ x :=
+      match x with
+      | Create => Value.StructTuple "alloy_primitives::common::TxKind::Create" []
+      | Call address => Value.StructTuple "alloy_primitives::common::TxKind::Call" [φ address]
+      end;
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "alloy_primitives::common::TxKind").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add apply of_ty : of_ty.
+End TxKind.
diff --git a/CoqOfRust/alloy_primitives/links/lib.v b/CoqOfRust/alloy_primitives/links/lib.v
deleted file mode 100644
index e69de29bb..000000000
diff --git a/CoqOfRust/alloy_primitives/log/links/mod.v b/CoqOfRust/alloy_primitives/log/links/mod.v
new file mode 100644
index 000000000..b1fee1561
--- /dev/null
+++ b/CoqOfRust/alloy_primitives/log/links/mod.v
@@ -0,0 +1,24 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.log.mod.
+
+(*
+pub struct Log<T = LogData> {
+    pub address: Address,
+    pub data: T,
+}
+*)
+Module Log.
+  Parameter t : Set.
+
+  Parameter to_value : t -> Value.t.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "alloy_primitives::log::Log";
+    φ := to_value;
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "alloy_primitives::log::Log").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add apply of_ty : of_ty.
+End Log.
diff --git a/CoqOfRust/core/convert/links/mod.v b/CoqOfRust/core/convert/links/mod.v
index 9a752870d..6079097bc 100644
--- a/CoqOfRust/core/convert/links/mod.v
+++ b/CoqOfRust/core/convert/links/mod.v
@@ -137,3 +137,25 @@ Module TryFrom.
     try_from : Run_try_from Self T Error;
   }.
 End TryFrom.
+
+(*
+pub trait TryInto<T>: Sized {
+    type Error;
+
+    fn try_into(self) -> Result<T, Self::Error>;
+}
+*)
+Module TryInto.
+  Definition trait (Self T : Set) `{Link Self} `{Link T} : TraitMethod.Header.t :=
+    ("core::convert::TryInto", [], [Φ T], Φ Self).
+
+  Definition Run_try_into (Self T Error : Set) `{Link Self} `{Link T} `{Link Error} : Set :=
+    TraitMethod.C (trait Self T) "try_into" (fun method =>
+      forall (self : Self),
+        Run.Trait method [] [] [ φ self ] (Result.t T Error)
+    ).
+
+  Class Run (Self : Set) (T : Set) (Error : Set) `{Link Self} `{Link T} `{Link Error} : Set := {
+    try_into : Run_try_into Self T Error;
+  }.
+End TryInto.
diff --git a/CoqOfRust/core/convert/links/num.v b/CoqOfRust/core/convert/links/num.v
index 3ac76fed6..32b267ec5 100644
--- a/CoqOfRust/core/convert/links/num.v
+++ b/CoqOfRust/core/convert/links/num.v
@@ -27,3 +27,25 @@ Module Impl_TryFrom_u64_for_usize.
     TryFrom.try_from := run_try_from;
   }.
 End Impl_TryFrom_u64_for_usize.
+
+Module Impl_TryFrom_u64_for_isize.
+  Definition Self : Set :=
+    Isize.t.
+
+  Definition run_try_from : TryFrom.Run_try_from Self U64.t TryFromIntError.t.
+  Proof.
+    eexists.
+    { eapply IsTraitMethod.Defined.
+      { apply convert.num.ptr_try_from_impls.Impl_core_convert_TryFrom_u64_for_isize.Implements. }
+      { reflexivity. }
+    }
+    { constructor.
+      run_symbolic.
+      all: admit.
+    }
+  Admitted.
+
+  Instance run : TryFrom.Run Self U64.t TryFromIntError.t := {
+    TryFrom.try_from := run_try_from;
+  }.
+End Impl_TryFrom_u64_for_isize.
diff --git a/CoqOfRust/core/fmt/links/mod.v b/CoqOfRust/core/fmt/links/mod.v
index a6a39ddd0..c8d8592e4 100644
--- a/CoqOfRust/core/fmt/links/mod.v
+++ b/CoqOfRust/core/fmt/links/mod.v
@@ -3,6 +3,7 @@ Require Import CoqOfRust.links.M.
 Require Import core.fmt.links.rt.
 Require Import core.fmt.mod.
 Require Import core.links.array.
+
 (*
 pub struct Arguments<'a> {
     pieces: &'a [&'static str],
@@ -28,6 +29,16 @@ End Arguments.
 Module Impl_Arguments.
   Definition Self : Set := Arguments.t.
 
+  (* pub const fn new_const<const N: usize>(pieces: &'a [&'static str; N]) -> Self *)
+  Instance run_new_const
+      (N : Usize.t)
+      (pieces : Ref.t Pointer.Kind.Ref (array.t (Ref.t Pointer.Kind.Ref string) N)) :
+    Run.Trait fmt.Impl_core_fmt_Arguments.new_const [φ N] [] [φ pieces] Self.
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
   (*
     pub fn new_v1<const P: usize, const A: usize>(
         pieces: &'a [&'static str; P],
diff --git a/CoqOfRust/core/iter/traits/links/iterator.v b/CoqOfRust/core/iter/traits/links/iterator.v
index ea96119f4..a5d52e564 100644
--- a/CoqOfRust/core/iter/traits/links/iterator.v
+++ b/CoqOfRust/core/iter/traits/links/iterator.v
@@ -259,7 +259,7 @@ Module Iterator.
       Set :=
     TraitMethod.C (trait Self) "next" (fun method =>
       forall (self : Ref.t Pointer.Kind.MutRef Self),
-      Run.Trait method [] [] [φ self] Item
+      Run.Trait method [] [] [φ self] (option Item)
     ).
 
   Definition Run_next_chunk
diff --git a/CoqOfRust/core/links/cmp.v b/CoqOfRust/core/links/cmp.v
index 706619977..9b84543d0 100644
--- a/CoqOfRust/core/links/cmp.v
+++ b/CoqOfRust/core/links/cmp.v
@@ -6,6 +6,34 @@ Require Import core.links.option.
 Require Import core.ops.links.function.
 Require Export core.links.cmpOrdering.
 
+(*
+pub trait PartialEq<Rhs: ?Sized = Self> {
+    fn eq(&self, other: &Rhs) -> bool;
+    fn ne(&self, other: &Rhs) -> bool;
+}
+*)
+Module PartialEq.
+  Definition trait (Self Rhs : Set) `{Link Self} `{Link Rhs} : TraitMethod.Header.t :=
+    ("core::cmp::PartialEq", [], [ Φ Rhs ], Φ Self).
+    
+  Definition Run_eq (Self Rhs : Set) `{Link Self} `{Link Rhs} : Set :=
+    TraitMethod.C (trait Self Rhs) "eq" (fun method =>
+      forall (self other : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self; φ other ] bool
+    ).
+    
+  Definition Run_ne (Self Rhs : Set) `{Link Self} `{Link Rhs} : Set :=
+    TraitMethod.C (trait Self Rhs) "ne" (fun method =>
+      forall (self other : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self; φ other ] bool
+    ).
+
+  Class Run (Self Rhs : Set) `{Link Self} `{Link Rhs} : Set := {
+    eq : Run_eq Self Rhs;
+    ne : Run_ne Self Rhs;
+  }.
+End PartialEq.
+
 (*
     pub fn max_by<T, F: FnOnce(&T, &T) -> Ordering>(v1: T, v2: T, compare: F) -> T {
         match compare(&v1, &v2) {
diff --git a/CoqOfRust/core/links/error.v b/CoqOfRust/core/links/error.v
new file mode 100644
index 000000000..9dddd70f4
--- /dev/null
+++ b/CoqOfRust/core/links/error.v
@@ -0,0 +1,53 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+
+(* pub struct Request<'a>(Tagged<dyn Erased<'a> + 'a>); *)
+Module Request.
+  Parameter t : Set.
+
+  Parameter to_value : t -> Value.t.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "core::error::Request";
+    φ := to_value;
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "core::error::Request").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add apply of_ty : of_ty.
+End Request.
+
+(*
+pub trait Error: Debug + Display {
+    // Provided methods
+    fn source(&self) -> Option<&(dyn Error + 'static)> { ... }
+    fn description(&self) -> &str { ... }
+    fn cause(&self) -> Option<&dyn Error> { ... }
+    fn provide<'a>(&'a self, request: &mut Request<'a>) { ... }
+}
+*)
+Module Error.
+  Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
+    ("core::error::Error", [], [], Φ Self).
+
+  Definition Run_description (Self : Set) `{Link Self} : Set :=
+    TraitMethod.C (trait Self) "description" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] (Ref.t Pointer.Kind.Ref string)
+    ).
+
+  Definition Run_provide (Self : Set) `{Link Self} : Set :=
+    TraitMethod.C (trait Self) "provide" (fun method =>
+      forall
+        (self : Ref.t Pointer.Kind.Ref Self)
+        (request : Ref.t Pointer.Kind.MutRef Request.t),
+      Run.Trait method [] [] [ φ self; φ request ] unit
+    ).
+
+  Class Run (Self : Set) `{Link Self} : Set := {
+    (* TODO: Add source *)
+    description : Run_description Self;
+    (* TODO: Add cause *)
+    provide : Run_provide Self;
+  }.
+End Error.
diff --git a/CoqOfRust/core/links/option.v b/CoqOfRust/core/links/option.v
index 7c96540fe..b289e461d 100644
--- a/CoqOfRust/core/links/option.v
+++ b/CoqOfRust/core/links/option.v
@@ -93,6 +93,14 @@ Module Impl_Option.
       (Result.t T E).
   Admitted.
 
+  (* pub const fn unwrap(self) -> T *)
+  Instance run_unwrap {T : Set} `{Link T}
+      (self : Self T) :
+    Run.Trait
+      (option.Impl_core_option_Option_T.unwrap (Φ T)) [] [] [ φ self ]
+      T.
+  Admitted.
+
   (* pub const unsafe fn unwrap_unchecked(self) -> T *)
   Instance run_unwrap_unchecked {T : Set} `{Link T}
       (self : Self T) :
@@ -108,4 +116,20 @@ Module Impl_Option.
       (option.Impl_core_option_Option_T.unwrap_or_default (Φ T)) [] [] [ φ self ]
       T.
   Admitted.
+
+  (* pub fn unwrap_or(self, default: T) -> T *)
+  Instance run_unwrap_or {T : Set} `{Link T}
+      (self : Self T) (default : T) :
+    Run.Trait
+      (option.Impl_core_option_Option_T.unwrap_or (Φ T)) [] [] [ φ self; φ default ]
+      T.
+  Admitted.
+
+  (* pub const fn expect(self, msg: &str) -> T *)
+  Instance run_expect {T : Set} `{Link T}
+      (self : Self T) (msg : Ref.t Pointer.Kind.Ref string) :
+    Run.Trait
+      (option.Impl_core_option_Option_T.expect (Φ T)) [] [] [ φ self; φ msg ]
+      T.
+  Admitted.
 End Impl_Option.
diff --git a/CoqOfRust/core/links/panicking.v b/CoqOfRust/core/links/panicking.v
index 0d988a4e1..fa1505ece 100644
--- a/CoqOfRust/core/links/panicking.v
+++ b/CoqOfRust/core/links/panicking.v
@@ -1,6 +1,7 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import core.fmt.links.mod.
+Require Import core.links.option.
 Require Import core.panicking.
 
 (* pub const fn panic_fmt(fmt: fmt::Arguments<'_>) -> ! *)
@@ -18,3 +19,84 @@ Proof.
   constructor.
   run_symbolic.
 Admitted.
+
+(*
+pub enum AssertKind {
+    Eq,
+    Ne,
+    Match,
+}
+*)
+Module AssertKind.
+  Inductive t : Set :=
+  | Eq
+  | Ne
+  | Match.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "core::panicking::AssertKind";
+    φ x :=
+      match x with
+      | Eq => Value.StructTuple "core::panicking::AssertKind::Eq" []
+      | Ne => Value.StructTuple "core::panicking::AssertKind::Ne" []
+      | Match => Value.StructTuple "core::panicking::AssertKind::Match" []
+      end;
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "core::panicking::AssertKind").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add apply of_ty : of_ty.
+
+  Lemma of_value_with_Eq :
+    Value.StructTuple "core::panicking::AssertKind::Eq" [] = φ Eq.
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_Eq : of_value.
+
+  Lemma of_value_with_Ne :
+    Value.StructTuple "core::panicking::AssertKind::Ne" [] = φ Ne.
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_Ne : of_value.
+
+  Lemma of_value_with_Match :
+    Value.StructTuple "core::panicking::AssertKind::Match" [] = φ Match.
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_Match : of_value.
+
+  Definition of_value_Eq :
+    OfValue.t (Value.StructTuple "core::panicking::AssertKind::Eq" []).
+  Proof. econstructor; apply of_value_with_Eq. Defined.
+  Smpl Add apply of_value_Eq : of_value.
+
+  Definition of_value_Ne :
+    OfValue.t (Value.StructTuple "core::panicking::AssertKind::Ne" []).
+  Proof. econstructor; apply of_value_with_Ne. Defined.
+  Smpl Add apply of_value_Ne : of_value.
+
+  Definition of_value_Match :
+    OfValue.t (Value.StructTuple "core::panicking::AssertKind::Match" []).
+  Proof. econstructor; apply of_value_with_Match. Defined.
+  Smpl Add apply of_value_Match : of_value.
+End AssertKind.
+
+(*
+pub fn assert_failed<T, U>(
+    kind: AssertKind,
+    left: &T,
+    right: &U,
+    args: Option<fmt::Arguments<'_>>,
+) -> !
+*)
+Instance run_assert_failed
+  (T : Set) `{Link T}
+  (U : Set) `{Link U}
+  (kind : AssertKind.t)
+  (left : Ref.t Pointer.Kind.Ref T)
+  (right : Ref.t Pointer.Kind.Ref U)
+  (args : option Arguments.t) :
+  Run.Trait
+    panicking.assert_failed [] [ Φ T; Φ U ] [φ kind; φ left; φ right; φ args]
+    Empty_set.
+Proof.
+  constructor.
+  run_symbolic.
+Admitted.
diff --git a/CoqOfRust/core/num/links/mod.v b/CoqOfRust/core/num/links/mod.v
index d565e30f6..8812a0aac 100644
--- a/CoqOfRust/core/num/links/mod.v
+++ b/CoqOfRust/core/num/links/mod.v
@@ -1,6 +1,7 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import core.intrinsics.links.mod.
+Require Import core.links.array.
 Require Import core.num.mod.
 
 Module Impl_u64.
@@ -40,6 +41,14 @@ Module Impl_u64.
     Run.Trait num.Impl_u64.overflowing_sub [] [] [ φ self; φ rhs ] (Self * bool).
   Proof.
   Admitted.
+
+  (* pub const fn from_be_bytes(bytes: [u8; 8]) -> Self *)
+  Instance run_from_be_bytes (bytes: array.t U8.t {| Integer.value := 8 |}) :
+    Run.Trait num.Impl_u64.from_be_bytes [] [] [ φ bytes ] Self.
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
 End Impl_u64.
 
 Module Impl_usize.
@@ -80,3 +89,44 @@ Module Impl_usize.
   Proof.
   Admitted.
 End Impl_usize.
+
+Module Impl_isize.
+  Import Impl_usize.
+
+  Definition Self : Set := Isize.t.
+
+  (* pub const MAX: Self *)
+  Instance run_max :
+    Run.Trait num.Impl_isize.value_MAX [] [] [] (Ref.t Pointer.Kind.Raw Self).
+  Proof.
+    constructor.
+    run_symbolic.
+  Defined.
+
+  (* pub const MIN: Self *)
+  Instance run_min :
+    Run.Trait num.Impl_isize.value_MIN [] [] [] (Ref.t Pointer.Kind.Raw Self).
+  Proof.
+    constructor.
+    run_symbolic.
+  Defined.
+
+  (* pub const fn saturating_add(self, rhs: Self) -> Self *)
+  Instance run_saturating_add (self rhs: Self) :
+    Run.Trait num.Impl_isize.saturating_add [] [] [ φ self; φ rhs ] Self.
+  Proof.
+    constructor.
+    run_symbolic.
+  Defined.
+
+  Instance run_saturating_mul (self rhs: Self) :
+    Run.Trait num.Impl_isize.saturating_mul [] [] [ φ self; φ rhs ] Self.
+  Proof.
+  Admitted.
+
+  (* pub const fn overflowing_sub(self, rhs: Self) -> (Self, bool) *)
+  Instance run_overflowing_sub (self rhs: Self) :
+    Run.Trait num.Impl_isize.overflowing_sub [] [] [ φ self; φ rhs ] (Self * bool).
+  Proof.
+  Admitted.
+End Impl_isize.
diff --git a/CoqOfRust/core/ptr/links/mut_ptr.v b/CoqOfRust/core/ptr/links/mut_ptr.v
new file mode 100644
index 000000000..a4bc7bc52
--- /dev/null
+++ b/CoqOfRust/core/ptr/links/mut_ptr.v
@@ -0,0 +1,245 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import links.M.
+Require Import core.ptr.mut_ptr.
+Require Import core.links.option.
+Require Import core.mem.links.maybe_uninit.
+
+Module Impl_pointer_mut_T.
+  Definition Self (T : Set) `{Link T} : Set := Ref.t Pointer.Kind.MutPointer T.
+
+  (* pub const fn is_null(self) -> bool *)
+  Instance run_is_null
+      (T : Set) `{Link T}
+      (self : Self T) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.is_null (Φ T)) [] [] [ φ self ] bool.
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const fn cast<U>(self) -> *mut U *)
+  Instance run_cast
+      (T : Set) `{Link T}
+      (U : Set) `{Link U}
+      (self : Self T) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.cast (Φ T)) [] [Φ U] [ φ self ] (Self U).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const fn with_addr(self, addr: usize) -> Self *)
+  Instance run_with_addr
+      (T : Set) `{Link T}
+      (self : Self T)
+      (addr : Usize.t) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.with_addr (Φ T)) [] [] [ φ self; φ addr ] (Self T).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const unsafe fn as_mut<'a>(self) -> Option<&'a mut T> *)
+  Instance run_as_mut
+      (T : Set) `{Link T}
+      (self : Self T) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.as_mut (Φ T)) [] [] [ φ self ]
+      (option (Ref.t Pointer.Kind.MutRef T)).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const unsafe fn as_uninit_mut<'a>(self) -> Option<&'a mut MaybeUninit<T>> *)
+  Instance run_as_uninit_mut
+      (T : Set) `{Link T}
+      (self : Self T) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.as_uninit_mut (Φ T)) [] [] [ φ self ]
+      (option (Ref.t Pointer.Kind.MutRef (maybe_uninit.MaybeUninit.t T))).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const fn guaranteed_eq(self, other: *mut T) -> Option<bool> *)
+  Instance run_guaranteed_eq
+      (T : Set) `{Link T}
+      (self : Self T)
+      (other : Self T) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.guaranteed_eq (Φ T)) [] [] [ φ self; φ other ]
+      (option bool).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const fn guaranteed_ne(self, other: *mut T) -> Option<bool> *)
+  Instance run_guaranteed_ne
+      (T : Set) `{Link T}
+      (self : Self T)
+      (other : Self T) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.guaranteed_ne (Φ T)) [] [] [ φ self; φ other ]
+      (option bool).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const unsafe fn offset(self, count: isize) -> *mut T *)
+  Instance run_offset
+      (T : Set) `{Link T}
+      (self : Self T)
+      (count : Isize.t) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.offset (Φ T)) [] [] [ φ self; φ count ] (Self T).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const fn wrapping_offset(self, count: isize) -> *mut T *)
+  Instance run_wrapping_offset
+      (T : Set) `{Link T}
+      (self : Self T)
+      (count : Isize.t) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.wrapping_offset (Φ T)) [] [] [ φ self; φ count ] (Self T).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const fn wrapping_byte_offset(self, count: isize) -> *mut T *)
+  Instance run_wrapping_byte_offset
+      (T : Set) `{Link T}
+      (self : Self T)
+      (count : Isize.t) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.wrapping_byte_offset (Φ T)) [] [] [ φ self; φ count ] (Self T).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub fn mask(self, mask: usize) -> *mut T *)
+  Instance run_mask
+      (T : Set) `{Link T}
+      (self : Self T)
+      (mask : Usize.t) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.mask (Φ T)) [] [] [ φ self; φ mask ] (Self T).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const unsafe fn as_mut_unchecked<'a>(self) -> &'a mut T *)
+  Instance run_as_mut_unchecked
+      (T : Set) `{Link T}
+      (self : Self T) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.as_mut_unchecked (Φ T)) [] [] [ φ self ]
+      (Ref.t Pointer.Kind.MutRef T).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const unsafe fn add(self, count: usize) -> Self *)
+  Instance run_add
+      (T : Set) `{Link T}
+      (self : Self T)
+      (count : Usize.t) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.add (Φ T)) [] [] [ φ self; φ count ] (Self T).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const fn wrapping_add(self, count: usize) -> Self *)
+  Instance run_wrapping_add
+      (T : Set) `{Link T}
+      (self : Self T)
+      (count : Usize.t) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.wrapping_add (Φ T)) [] [] [ φ self; φ count ] (Self T).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const unsafe fn sub(self, count: usize) -> Self *)
+  Instance run_sub
+      (T : Set) `{Link T}
+      (self : Self T)
+      (count : Usize.t) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.sub (Φ T)) [] [] [ φ self; φ count ] (Self T).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const fn wrapping_sub(self, count: usize) -> Self *)
+  Instance run_wrapping_sub
+      (T : Set) `{Link T}
+      (self : Self T)
+      (count : Usize.t) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.wrapping_sub (Φ T)) [] [] [ φ self; φ count ] (Self T).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const fn addr(self) -> usize *)
+  Instance run_addr
+      (T : Set) `{Link T}
+      (self : Self T) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.addr (Φ T)) [] [] [ φ self ] Usize.t.
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const fn cast_const(self) -> *const T *)
+  Instance run_cast_const
+      (T : Set) `{Link T}
+      (self : Self T) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.cast_const (Φ T)) [] [] [ φ self ]
+      (Ref.t Pointer.Kind.ConstPointer T).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const fn with_metadata_of<U>(self, val: *mut U) -> *mut U *)
+  Instance run_with_metadata_of
+      (T : Set) `{Link T}
+      (U : Set) `{Link U}
+      (self : Self T)
+      (val : Ref.t Pointer.Kind.MutPointer U) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.with_metadata_of (Φ T)) [] [Φ U] [ φ self; φ val ]
+      (Ref.t Pointer.Kind.MutPointer U).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const unsafe fn write(self, val: T) *)
+  Instance run_write
+      (T : Set) `{Link T}
+      (self : Self T)
+      (val : T) :
+    Run.Trait (ptr.mut_ptr.Impl_pointer_mut_T.write (Φ T)) [] [] [ φ self; φ val ] unit.
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* pub const unsafe fn write_bytes(self, val: u8, count: usize) *)
+  Instance run_write_bytes
+      (T : Set) `{Link T}
+      (self : Self T)
+      (val : U8.t)
+      (count : Usize.t) :
+    Run.Trait
+      (ptr.mut_ptr.Impl_pointer_mut_T.write_bytes (Φ T)) [] [] [ φ self; φ val; φ count ]
+      unit.
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+End Impl_pointer_mut_T.
diff --git a/CoqOfRust/core/slice/links/iter.v b/CoqOfRust/core/slice/links/iter.v
index 0d8a1642b..3a35a4277 100644
--- a/CoqOfRust/core/slice/links/iter.v
+++ b/CoqOfRust/core/slice/links/iter.v
@@ -1,5 +1,6 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
+Require Import core.iter.traits.links.iterator.
 Require Import core.slice.iter.
 
 (* pub struct IterMut<'a, T: 'a> { /* private fields */ } *)
@@ -24,3 +25,115 @@ Module IterMut.
   Defined.
   Smpl Add apply of_ty : of_ty.
 End IterMut.
+
+(*
+pub struct ChunksExact<'a, T: 'a> {
+    v: &'a [T],
+    rem: &'a [T],
+    chunk_size: usize,
+}
+*)
+Module ChunksExact.
+  Parameter t : forall (T : Set), Set.
+
+  Parameter to_value : forall {T : Set}, t T -> Value.t.
+
+  Global Instance IsLink (T : Set) `{Link T} : Link (t T) := {
+    Φ := Ty.apply (Ty.path "core::slice::iter::ChunksExact") [] [Φ T];
+    φ := to_value;
+  }.
+
+  Definition of_ty T_ty :
+    OfTy.t T_ty ->
+    OfTy.t (Ty.apply (Ty.path "core::slice::iter::ChunksExact") [] [T_ty]).
+  Proof.
+    intros [T].
+    eapply OfTy.Make with (A := t T).
+    subst.
+    reflexivity.
+  Defined.
+  Smpl Add apply of_ty : of_ty.
+End ChunksExact.
+
+Module Impl_ChunksExact.
+  Definition Self (T : Set) `{Link T} : Set :=
+    ChunksExact.t T.
+    
+  (* pub fn remainder(&self) -> &'a [T] *)
+  Instance run_remainder
+    (T : Set) `{Link T}
+    (self : Ref.t Pointer.Kind.Ref (Self T)) :
+    Run.Trait (slice.iter.Impl_core_slice_iter_ChunksExact_T.remainder (Φ T)) [] [] [φ self]
+      (Ref.t Pointer.Kind.Ref (list T)).
+  Admitted.
+End Impl_ChunksExact.
+
+(* impl<'a, T> Iterator for ChunksExact<'a, T> *)
+Module Impl_Iterator_for_ChunksExact.
+  Definition Self (T : Set) `{Link T} : Set :=
+    ChunksExact.t T.
+
+    (* type Item = &'a [T]; *)
+    Definition Item (T : Set) `{Link T} : Set :=
+      Ref.t Pointer.Kind.Ref (list T).
+
+    Instance run (T : Set) `{Link T} : Iterator.Run (Self T) (Item T).
+    Admitted.
+End Impl_Iterator_for_ChunksExact.
+
+(*
+pub struct RChunksExact<'a, T: 'a> {
+    v: &'a [T],
+    rem: &'a [T],
+    chunk_size: usize,
+}
+*)
+Module RChunksExact.
+  Parameter t : forall (T : Set), Set.
+
+  Parameter to_value : forall {T : Set}, t T -> Value.t.
+
+  Global Instance IsLink (T : Set) `{Link T} : Link (t T) := {
+    Φ := Ty.apply (Ty.path "core::slice::iter::RChunksExact") [] [Φ T];
+    φ := to_value;
+  }.
+
+  Definition of_ty T_ty :
+    OfTy.t T_ty ->
+    OfTy.t (Ty.apply (Ty.path "core::slice::iter::RChunksExact") [] [T_ty]).
+  Proof.
+    intros [T].
+    eapply OfTy.Make with (A := t T).
+    subst.
+    reflexivity.
+  Defined.
+  Smpl Add apply of_ty : of_ty.
+End RChunksExact.
+
+(* impl<'a, T> RChunksExact<'a, T> *)
+Module Impl_RChunksExact.
+  Definition Self (T : Set) : Set :=
+    RChunksExact.t T.
+
+  (* pub fn remainder(&self) -> &'a [T] *)
+  Instance run_remainder
+    (T : Set) `{Link T}
+    (self : Ref.t Pointer.Kind.Ref (Self T)) :
+    Run.Trait
+      (slice.iter.Impl_core_slice_iter_RChunksExact_T.remainder (Φ T)) [] [] [φ self]
+      (Ref.t Pointer.Kind.Ref (list T)).
+  Admitted.
+End Impl_RChunksExact.
+
+(* impl<'a, T> Iterator for RChunksExact<'a, T> *)
+Module Impl_Iterator_for_RChunksExact.
+  Definition Self (T : Set) `{Link T} : Set :=
+    RChunksExact.t T.
+
+    (* type Item = &'a [T]; *)
+    Definition Item (T : Set) `{Link T} : Set :=
+      Ref.t Pointer.Kind.Ref (list T).
+
+    Instance run (T : Set) `{Link T} : Iterator.Run (Self T) (Item T).
+    Admitted.
+End Impl_Iterator_for_RChunksExact.
diff --git a/CoqOfRust/core/slice/links/mod.v b/CoqOfRust/core/slice/links/mod.v
index 4bf32f231..84e69d2d0 100644
--- a/CoqOfRust/core/slice/links/mod.v
+++ b/CoqOfRust/core/slice/links/mod.v
@@ -17,7 +17,7 @@ Module Impl_Slice.
       (T : Set) `{Link T}
       {I : Set} `{Link I} 
       {Output : Set} `{Link Output}
-      (run_SliceIndex_for_I : SliceIndex.Run I (T := Self T) (Output := Output))
+      {run_SliceIndex_for_I : SliceIndex.Run I (T := Self T) (Output := Output)}
       (self : Ref.t Pointer.Kind.Ref (Self T)) 
       (index : I) :
     Run.Trait (slice.Impl_slice_T.get (Φ T)) [] [Φ I] [φ self; φ index]
@@ -48,6 +48,17 @@ Module Impl_Slice.
       Usize.t.
   Admitted.
 
+  (* pub const fn is_empty(&self) -> bool *)
+  Instance run_is_empty
+      (T : Set) `{Link T}
+      (self : Ref.t Pointer.Kind.Ref (Self T)) :
+    Run.Trait (slice.Impl_slice_T.is_empty (Φ T)) [] [] [φ self]
+      bool.
+  Proof.
+    constructor.
+    run_symbolic.
+  Defined.
+
   (* pub fn iter_mut(&mut self) -> IterMut<'_, T> *)
   Instance run_iter_mut
       (T : Set) `{Link T}
@@ -55,4 +66,30 @@ Module Impl_Slice.
     Run.Trait (slice.Impl_slice_T.iter_mut (Φ T)) [] [] [φ self]
       (IterMut.t T).
   Admitted.
+
+  (* pub const fn as_mut_ptr(&mut self) -> *mut T *)
+  Instance run_as_mut_ptr
+      (T : Set) `{Link T}
+      (self : Ref.t Pointer.Kind.MutRef (Self T)) :
+    Run.Trait (slice.Impl_slice_T.as_mut_ptr (Φ T)) [] [] [φ self]
+      (Ref.t Pointer.Kind.MutPointer T).
+  Admitted.
+
+  (* pub fn chunks_exact(&self, chunk_size: usize) -> ChunksExact<'_, T> *)
+  Instance run_chunks_exact
+      (T : Set) `{Link T}
+      (self : Ref.t Pointer.Kind.Ref (Self T))
+      (chunk_size : Usize.t) :
+    Run.Trait (slice.Impl_slice_T.chunks_exact (Φ T)) [] [] [φ self; φ chunk_size]
+      (ChunksExact.t T).
+  Admitted.
+
+  (* pub fn rchunks_exact(&self, chunk_size: usize) -> RChunksExact<'_, T> *)
+  Instance run_rchunks_exact
+      (T : Set) `{Link T}
+      (self : Ref.t Pointer.Kind.Ref (Self T))
+      (chunk_size : Usize.t) :
+    Run.Trait (slice.Impl_slice_T.rchunks_exact (Φ T)) [] [] [φ self; φ chunk_size]
+      (RChunksExact.t T).
+  Admitted.
 End Impl_Slice.
diff --git a/CoqOfRust/links/M.v b/CoqOfRust/links/M.v
index ff45196fe..20fb628c2 100644
--- a/CoqOfRust/links/M.v
+++ b/CoqOfRust/links/M.v
@@ -1255,7 +1255,11 @@ Ltac run_main_rewrites :=
       Ref.rewrite_deref_eq ||
       Ref.rewrite_borrow_eq ||
       Ref.rewrite_cast_cast_eq ||
-      rewrite_if_then_else_bool_eq
+      rewrite_if_then_else_bool_eq ||
+      erewrite IsTraitAssociatedType_eq
+        by match goal with
+        | H : _ |- _ => apply H
+        end
     ));
     reflexivity
   |].
diff --git a/CoqOfRust/revm/revm_bytecode/eof/links/types_section.v b/CoqOfRust/revm/revm_bytecode/eof/links/types_section.v
index d6dae997b..ecccf385b 100644
--- a/CoqOfRust/revm/revm_bytecode/eof/links/types_section.v
+++ b/CoqOfRust/revm/revm_bytecode/eof/links/types_section.v
@@ -23,4 +23,75 @@ Module TypesSection.
   Definition of_ty : OfTy.t (Ty.path "revm_bytecode::eof::types_section::TypesSection").
   Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
   Smpl Add apply of_ty : of_ty.
+
+  Lemma of_value_with inputs inputs' outputs outputs' max_stack_size max_stack_size' :
+    inputs' = φ inputs ->
+    outputs' = φ outputs ->
+    max_stack_size' = φ max_stack_size ->
+    Value.StructRecord "revm_bytecode::eof::types_section::TypesSection" [
+      ("inputs", inputs');
+      ("outputs", outputs');
+      ("max_stack_size", max_stack_size')
+    ] = φ (Build_t inputs outputs max_stack_size).
+  Proof. now intros; subst. Qed.
+  Smpl Add apply of_value_with : of_value.
+
+  Definition of_value
+    (inputs : U8.t) inputs'
+    (outputs : U8.t) outputs'
+    (max_stack_size : U16.t) max_stack_size' :
+    inputs' = φ inputs ->
+    outputs' = φ outputs ->
+    max_stack_size' = φ max_stack_size ->
+    OfValue.t (Value.StructRecord "revm_bytecode::eof::types_section::TypesSection" [
+      ("inputs", inputs');
+      ("outputs", outputs');
+      ("max_stack_size", max_stack_size')
+    ]).
+  Proof. econstructor; apply of_value_with; eassumption. Defined.
+  Smpl Add eapply of_value : of_value.
+
+  Module SubPointer.
+    Definition get_inputs : SubPointer.Runner.t t
+      (Pointer.Index.StructRecord "revm_bytecode::eof::types_section::TypesSection" "inputs") :=
+    {|
+      SubPointer.Runner.projection x := Some x.(inputs);
+      SubPointer.Runner.injection x y := Some (x <| inputs := y |>);
+    |}.
+
+    Lemma get_inputs_is_valid :
+      SubPointer.Runner.Valid.t get_inputs.
+    Proof.
+      now constructor.
+    Qed.
+    Smpl Add apply get_inputs_is_valid : run_sub_pointer.
+
+    Definition get_outputs : SubPointer.Runner.t t
+      (Pointer.Index.StructRecord "revm_bytecode::eof::types_section::TypesSection" "outputs") :=
+    {|
+      SubPointer.Runner.projection x := Some x.(outputs);
+      SubPointer.Runner.injection x y := Some (x <| outputs := y |>);
+    |}.
+
+    Lemma get_outputs_is_valid :
+      SubPointer.Runner.Valid.t get_outputs.
+    Proof.
+      now constructor.
+    Qed.
+    Smpl Add apply get_outputs_is_valid : run_sub_pointer.
+
+    Definition get_max_stack_size : SubPointer.Runner.t t
+      (Pointer.Index.StructRecord "revm_bytecode::eof::types_section::TypesSection" "max_stack_size") :=
+    {|
+      SubPointer.Runner.projection x := Some x.(max_stack_size);
+      SubPointer.Runner.injection x y := Some (x <| max_stack_size := y |>);
+    |}.
+
+    Lemma get_max_stack_size_is_valid :
+      SubPointer.Runner.Valid.t get_max_stack_size.
+    Proof.
+      now constructor.
+    Qed.
+    Smpl Add apply get_max_stack_size_is_valid : run_sub_pointer.
+  End SubPointer.
 End TypesSection.
diff --git a/CoqOfRust/revm/revm_context_interface/block/links/blob.v b/CoqOfRust/revm/revm_context_interface/block/links/blob.v
new file mode 100644
index 000000000..73e9c3ae5
--- /dev/null
+++ b/CoqOfRust/revm/revm_context_interface/block/links/blob.v
@@ -0,0 +1,59 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+
+(*
+pub struct BlobExcessGasAndPrice {
+    pub excess_blob_gas: u64,
+    pub blob_gasprice: u128,
+}
+*)
+Module BlobExcessGasAndPrice.
+  Record t : Set := {
+    excess_blob_gas : U64.t;
+    blob_gasprice : U128.t;
+  }.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "revm_context_interface::block::BlobExcessGasAndPrice";
+    φ '(Build_t excess_blob_gas blob_gasprice) :=
+      Value.StructRecord "revm_context_interface::block::BlobExcessGasAndPrice" [
+        ("excess_blob_gas", φ excess_blob_gas);
+        ("blob_gasprice", φ blob_gasprice)
+      ]
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "revm_context_interface::block::BlobExcessGasAndPrice").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add simple apply of_ty : of_ty.
+
+  Lemma of_value_with
+      excess_blob_gas excess_blob_gas'
+      blob_gasprice blob_gasprice' :
+    excess_blob_gas' = φ excess_blob_gas ->
+    blob_gasprice' = φ blob_gasprice ->
+    Value.StructRecord "revm_context_interface::block::BlobExcessGasAndPrice" [
+      ("excess_blob_gas", excess_blob_gas');
+      ("blob_gasprice", blob_gasprice')
+    ] =
+    φ (Build_t excess_blob_gas blob_gasprice).
+  Proof. now intros; subst. Qed.
+  Smpl Add eapply of_value_with : of_value.
+
+  Definition of_value
+      (excess_blob_gas : U64.t) excess_blob_gas'
+      (blob_gasprice : U128.t) blob_gasprice' :
+    excess_blob_gas' = φ excess_blob_gas ->
+    blob_gasprice' = φ blob_gasprice ->
+    OfValue.t (
+      Value.StructRecord "revm_context_interface::block::BlobExcessGasAndPrice" [
+        ("excess_blob_gas", excess_blob_gas');
+        ("blob_gasprice", blob_gasprice')
+      ]
+    ).
+  Proof.
+    intros.
+    eapply OfValue.Make with (A := t).
+    apply of_value_with; eassumption.
+  Defined.
+  Smpl Add eapply of_value : of_value.
+End BlobExcessGasAndPrice.
diff --git a/CoqOfRust/revm/revm_context_interface/links/block.v b/CoqOfRust/revm/revm_context_interface/links/block.v
index 72a50164e..61623cb3a 100644
--- a/CoqOfRust/revm/revm_context_interface/links/block.v
+++ b/CoqOfRust/revm/revm_context_interface/links/block.v
@@ -3,7 +3,7 @@ Require Import CoqOfRust.links.M.
 Require Import alloy_primitives.bits.links.address.
 Require Import alloy_primitives.links.aliases.
 Require Import core.links.option.
-
+Require Import revm.revm_context_interface.block.links.blob.
 (* 
 #[auto_impl(&, &mut, Box, Arc)]
 pub trait Block {
@@ -29,55 +29,66 @@ Module Block.
   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
     ).
 
-  (* fn beneficiary(&self) -> Address; *)
   Definition Run_beneficiary (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "beneficiary" (fun method =>
       forall (self : Ref.t Pointer.Kind.Ref Self),
         Run.Trait method [] [] [ φ self ] Address.t
     ).
 
-  (* 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
     ).
 
-  (* fn gas_limit(&self) -> u64; *)
   Definition Run_gas_limit (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "gas_limit" (fun method =>
       forall (self : Ref.t Pointer.Kind.Ref Self),
         Run.Trait method [] [] [ φ self ] U64.t
     ).
 
-  (* fn basefee(&self) -> u64; *)
   Definition Run_basefee (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "basefee" (fun method =>
       forall (self : Ref.t Pointer.Kind.Ref Self),
         Run.Trait method [] [] [ φ self ] U64.t
     ).
 
-  (* fn difficulty(&self) -> U256; *)
   Definition Run_difficulty (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "difficulty" (fun method =>
       forall (self : Ref.t Pointer.Kind.Ref Self),
         Run.Trait method [] [] [ φ self ] aliases.U256.t
     ).
 
-  (* fn blob_gasprice(&self) -> Option<u128> *)
+  Definition Run_prevrandao (Self : Set) `{Link Self} : Set :=
+    TraitMethod.C (trait Self) "prevrandao" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+        Run.Trait method [] [] [ φ self ] (option aliases.B256.t)
+    ).
+
+  Definition Run_blob_excess_gas_and_price (Self : Set) `{Link Self} : Set :=
+    TraitMethod.C (trait Self) "blob_excess_gas_and_price" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+        Run.Trait method [] [] [ φ self ] (option BlobExcessGasAndPrice.t)
+    ).
+
   Definition Run_blob_gasprice (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "blob_gasprice" (fun method =>
       forall (self : Ref.t Pointer.Kind.Ref Self),
         Run.Trait method [] [] [ φ self ] (option U128.t)
     ).
 
+  Definition Run_blob_excess_gas (Self : Set) `{Link Self} : Set :=
+    TraitMethod.C (trait Self) "blob_excess_gas" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+        Run.Trait method [] [] [ φ self ] (option U64.t)
+    ).
+
   Class Run (Self : Set) `{Link Self} : Set := {
     number : Run_number Self;
     beneficiary : Run_beneficiary Self;
@@ -85,11 +96,14 @@ Module Block.
     gas_limit : Run_gas_limit Self;
     basefee : Run_basefee Self;
     difficulty : Run_difficulty Self;
+    prevrandao : Run_prevrandao Self;
+    blob_excess_gas_and_price : Run_blob_excess_gas_and_price Self;
     blob_gasprice : Run_blob_gasprice Self;
+    blob_excess_gas : Run_blob_excess_gas Self;
   }.
 End Block. 
 
-(* 
+(*
 #[auto_impl(&, &mut, Box, Arc)]
 pub trait BlockGetter {
     type Block: Block;
diff --git a/CoqOfRust/revm/revm_context_interface/links/host.v b/CoqOfRust/revm/revm_context_interface/links/host.v
index 656da6ea5..0726ddd30 100644
--- a/CoqOfRust/revm/revm_context_interface/links/host.v
+++ b/CoqOfRust/revm/revm_context_interface/links/host.v
@@ -3,17 +3,11 @@ Require Import CoqOfRust.links.M.
 Require Import alloy_primitives.bits.links.address.
 Require Import alloy_primitives.bytes.links.mod.
 Require Import alloy_primitives.links.aliases.
+Require Import alloy_primitives.log.links.mod.
 Require Import revm.revm_context_interface.links.cfg.
 Require Import revm.revm_context_interface.links.block.
 Require Import revm.revm_context_interface.links.journaled_state.
-
-(* TODO: Add source code *)
-Module Log.
-  Parameter t : Set.
-
-  Global Instance IsLink : Link t.
-  Admitted.
-End Log.
+Require Import revm.revm_context_interface.links.transaction.
 
 (*
 pub struct SStoreResult {
@@ -70,23 +64,30 @@ pub trait Host: TransactionGetter + BlockGetter + CfgGetter {
 Module Host.
   Module Types.
     Record t : Type := {
+      Transaction : Set;
+      TransactionTypes : Transaction.Types.t;
       Cfg : Set; (* For CfgGetter *)
       Spec : Set; (* For CfgGetter *)
       Block : Set; (* For BlockGetter *)
     }.
 
     Class AreLinks (types : t) : Set := {
+      H_Transaction : Link types.(Transaction);
+      H_TransactionTypes : Transaction.Types.AreLinks types.(TransactionTypes);
       H_Cfg : Link types.(Cfg);
       H_Spec : Link types.(Spec);
       H_Block : Link types.(Block);
     }.
 
+    Global Instance IsLinkTransaction (types : t) (H : AreLinks types) : Link types.(Transaction) :=
+      H.(H_Transaction _).
+    Global Instance AreLinksTransactionTypes (types : t) (H : AreLinks types) :
+      Transaction.Types.AreLinks types.(TransactionTypes) :=
+      H.(H_TransactionTypes _).
     Global Instance IsLinkCfg (types : t) (H : AreLinks types) : Link types.(Cfg) :=
       H.(H_Cfg _).
-
     Global Instance IsLinkSpec (types : t) (H : AreLinks types) : Link types.(Spec) :=
       H.(H_Spec _).
-
     Global Instance IsLinkBlock (types : t) (H : AreLinks types) : Link types.(Block) :=
       H.(H_Block _).
 
@@ -232,8 +233,10 @@ Module Host.
     (types : Types.t) `{Types.AreLinks types} :
     Set :=
   {
-    run_BlockGetter : BlockGetter.Run Self (Types.to_BlockGetter_types types);
-    run_CfgGetter : CfgGetter.Run Self (Types.to_CfgGetter_types types);
+    run_TransactionGetter_for_Self :
+      TransactionGetter.Run Self types.(Types.Transaction) types.(Types.TransactionTypes);
+    run_BlockGetter_for_Self : BlockGetter.Run Self (Types.to_BlockGetter_types types);
+    run_CfgGetter_for_Self : CfgGetter.Run Self (Types.to_CfgGetter_types types);
     load_account_delegated : Run_load_account_delegated Self;
     block_hash : Run_block_hash Self;
     balance : Run_balance Self;
@@ -246,4 +249,20 @@ Module Host.
     log : Run_log Self;
     selfdestruct : Run_selfdestruct Self;
   }.
+
+  Ltac destruct_run :=
+    cbn;
+    eapply Run.Rewrite; [
+      progress repeat erewrite IsTraitAssociatedType_eq
+        by match goal with
+        | H : Run _ _ |- _ => apply H
+        end;
+      reflexivity
+    |];
+    match goal with
+    | H : Run _ _ |- _ =>
+      (* We make a duplicate for future calls *)
+      pose H;
+      destruct H
+    end.
 End Host.
diff --git a/CoqOfRust/revm/revm_context_interface/links/transaction.v b/CoqOfRust/revm/revm_context_interface/links/transaction.v
new file mode 100644
index 000000000..624af3a1e
--- /dev/null
+++ b/CoqOfRust/revm/revm_context_interface/links/transaction.v
@@ -0,0 +1,313 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.links.aliases.
+Require Import alloy_primitives.links.common.
+Require Import core.convert.links.mod.
+Require Import core.links.error.
+Require Import core.links.option.
+Require Import revm.revm_context_interface.transaction.links.eip4844.
+Require Import revm.revm_context_interface.transaction.links.transaction_type.
+
+(* pub trait TransactionError: Debug + core::error::Error {} *)
+Module TransactionError.
+  Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
+    ("revm_context_interface::transaction::TransactionError", [], [], Φ Self).
+
+  Class Run (Self : Set) `{Link Self} : Set := {
+    run_Error_for_Self : Error.Run Self;
+  }.
+End TransactionError.
+
+(*
+pub trait Transaction {
+    type TransactionError: TransactionError;
+    type TransactionType: Into<TransactionType>;
+    type AccessList: AccessListTrait;
+    type Legacy: LegacyTx;
+    type Eip2930: Eip2930Tx<AccessList = Self::AccessList>;
+    type Eip1559: Eip1559Tx<AccessList = Self::AccessList>;
+    type Eip4844: Eip4844Tx<AccessList = Self::AccessList>;
+    type Eip7702: Eip7702Tx<AccessList = Self::AccessList>;
+
+    fn tx_type(&self) -> Self::TransactionType;
+    fn legacy(&self) -> &Self::Legacy;
+    fn eip2930(&self) -> &Self::Eip2930;
+    fn eip1559(&self) -> &Self::Eip1559;
+    fn eip4844(&self) -> &Self::Eip4844;
+    fn eip7702(&self) -> &Self::Eip7702;
+    fn common_fields(&self) -> &dyn CommonTxFields
+    fn max_fee(&self) -> u128
+    fn effective_gas_price(&self, base_fee: u128) -> u128
+    fn kind(&self) -> TxKind
+    fn access_list(&self) -> Option<&Self::AccessList>
+}
+*)
+Module Transaction.
+  Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
+    ("revm_context_interface::transaction::Transaction", [], [], Φ Self).
+
+  Module Types.
+    Record t : Type := {
+      TransactionError : Set;
+      TransactionType : Set;
+      AccessList : Set;
+      Legacy : Set;
+      Eip2930 : Set;
+      Eip1559 : Set;
+      Eip4844 : Set;
+      Eip7702 : Set;
+    }.
+
+    Class AreLinks (types : t) : Set := {
+      H_TransactionError : Link types.(TransactionError);
+      H_TransactionType : Link types.(TransactionType);
+      H_AccessList : Link types.(AccessList);
+      H_Legacy : Link types.(Legacy);
+      H_Eip2930 : Link types.(Eip2930);
+      H_Eip1559 : Link types.(Eip1559);
+      H_Eip4844 : Link types.(Eip4844);
+      H_Eip7702 : Link types.(Eip7702);
+    }.
+
+    Global Instance IsLinkTransactionError (types : t) (H : AreLinks types) : Link types.(TransactionError) :=
+      H.(H_TransactionError _).
+    Global Instance IsLinkTransactionType (types : t) (H : AreLinks types) : Link types.(TransactionType) :=
+      H.(H_TransactionType _).
+    Global Instance IsLinkAccessList (types : t) (H : AreLinks types) : Link types.(AccessList) :=
+      H.(H_AccessList _).
+    Global Instance IsLinkLegacy (types : t) (H : AreLinks types) : Link types.(Legacy) :=
+      H.(H_Legacy _).
+    Global Instance IsLinkEip2930 (types : t) (H : AreLinks types) : Link types.(Eip2930) :=
+      H.(H_Eip2930 _).
+    Global Instance IsLinkEip1559 (types : t) (H : AreLinks types) : Link types.(Eip1559) :=
+      H.(H_Eip1559 _).
+    Global Instance IsLinkEip4844 (types : t) (H : AreLinks types) : Link types.(Eip4844) :=
+      H.(H_Eip4844 _).
+    Global Instance IsLinkEip7702 (types : t) (H : AreLinks types) : Link types.(Eip7702) :=
+      H.(H_Eip7702 _).
+  End Types.
+
+  Definition Run_tx_type
+    (Self : Set) `{Link Self}
+    (types : Types.t) `{Types.AreLinks types} :
+    Set :=
+    TraitMethod.C (trait Self) "tx_type" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] types.(Types.TransactionType)
+    ).
+
+  Definition Run_legacy
+    (Self : Set) `{Link Self}
+    (types : Types.t) `{Types.AreLinks types} :
+    Set :=
+    TraitMethod.C (trait Self) "legacy" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] (Ref.t Pointer.Kind.Ref types.(Types.Legacy))
+    ).
+
+  Definition Run_eip2930
+    (Self : Set) `{Link Self}
+    (types : Types.t) `{Types.AreLinks types} :
+    Set :=
+    TraitMethod.C (trait Self) "eip2930" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] (Ref.t Pointer.Kind.Ref types.(Types.Eip2930))
+    ).
+
+  Definition Run_eip1559
+    (Self : Set) `{Link Self}
+    (types : Types.t) `{Types.AreLinks types} :
+    Set :=
+    TraitMethod.C (trait Self) "eip1559" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] (Ref.t Pointer.Kind.Ref types.(Types.Eip1559))
+    ).
+
+  Definition Run_eip4844
+    (Self : Set) `{Link Self}
+    (types : Types.t) `{Types.AreLinks types} :
+    Set :=
+    TraitMethod.C (trait Self) "eip4844" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] (Ref.t Pointer.Kind.Ref types.(Types.Eip4844))
+    ).
+
+  Definition Run_eip7702
+    (Self : Set) `{Link Self}
+    (types : Types.t) `{Types.AreLinks types} :
+    Set :=
+    TraitMethod.C (trait Self) "eip7702" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] (Ref.t Pointer.Kind.Ref types.(Types.Eip7702))
+    ).
+
+  (* Definition Run_common_fields
+    (Self : Set) `{Link Self}
+    (types : Types.t) `{Types.AreLinks types} :
+    Set :=
+    TraitMethod.C (trait Self) "common_fields" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] (Ref.t Pointer.Kind.Ref types.(Types.CommonTxFields))
+    ). *)
+
+  Definition Run_max_fee
+    (Self : Set) `{Link Self}
+    (types : Types.t) `{Types.AreLinks types} :
+    Set :=
+    TraitMethod.C (trait Self) "max_fee" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] U128.t
+    ).
+
+  Definition Run_effective_gas_price
+    (Self : Set) `{Link Self}
+    (types : Types.t) `{Types.AreLinks types} :
+    Set :=
+    TraitMethod.C (trait Self) "effective_gas_price" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self) (base_fee : U128.t),
+      Run.Trait method [] [] [ φ self; φ base_fee ] U128.t
+    ).
+
+  Definition Run_kind
+    (Self : Set) `{Link Self}
+    (types : Types.t) `{Types.AreLinks types} :
+    Set :=
+    TraitMethod.C (trait Self) "kind" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] TxKind.t
+    ).
+
+  Definition Run_access_list
+    (Self : Set) `{Link Self}
+    (types : Types.t) `{Types.AreLinks types} :
+    Set :=
+    TraitMethod.C (trait Self) "access_list" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] (option (Ref.t Pointer.Kind.Ref types.(Types.AccessList)))
+    ).
+
+  Class Run
+      (Self : Set) `{Link Self}
+      (types : Types.t) `{Types.AreLinks types} :
+      Set := {
+    TransactionError_IsAssociated :
+      IsTraitAssociatedType
+        "revm_context_interface::transaction::Transaction" [] [] (Φ Self)
+        "TransactionError" (Φ types.(Types.TransactionError));
+    TransactionType_IsAssociated :
+      IsTraitAssociatedType
+        "revm_context_interface::transaction::Transaction" [] [] (Φ Self)
+        "TransactionType" (Φ types.(Types.TransactionType));
+    run_Into_for_TransactionType :
+      Into.Run types.(Types.TransactionType) TransactionType.t;
+    AccessList_IsAssociated :
+      IsTraitAssociatedType
+        "revm_context_interface::transaction::Transaction" [] [] (Φ Self)
+        "AccessList" (Φ types.(Types.AccessList));
+    Legacy_IsAssociated :
+      IsTraitAssociatedType
+        "revm_context_interface::transaction::Transaction" [] [] (Φ Self)
+        "Legacy" (Φ types.(Types.Legacy));
+    Eip2930_IsAssociated :
+      IsTraitAssociatedType
+        "revm_context_interface::transaction::Transaction" [] [] (Φ Self)
+        "Eip2930" (Φ types.(Types.Eip2930));
+    Eip1559_IsAssociated :
+      IsTraitAssociatedType
+        "revm_context_interface::transaction::Transaction" [] [] (Φ Self)
+        "Eip1559" (Φ types.(Types.Eip1559));
+    Eip4844_IsAssociated :
+      IsTraitAssociatedType
+        "revm_context_interface::transaction::Transaction" [] [] (Φ Self)
+        "Eip4844" (Φ types.(Types.Eip4844));
+    run_Eip4844Tx_for_Eip4844 : Eip4844Tx.Run types.(Types.Eip4844);
+    Eip7702_IsAssociated :
+      IsTraitAssociatedType
+        "revm_context_interface::transaction::Transaction" [] [] (Φ Self)
+        "Eip7702" (Φ types.(Types.Eip7702));
+    tx_type : Run_tx_type Self types;
+    legacy : Run_legacy Self types;
+    eip2930 : Run_eip2930 Self types;
+    eip1559 : Run_eip1559 Self types;
+    eip4844 : Run_eip4844 Self types;
+    eip7702 : Run_eip7702 Self types;
+    (* common_fields : Run_common_fields Self types; *)
+    max_fee : Run_max_fee Self types;
+    effective_gas_price : Run_effective_gas_price Self types;
+    kind : Run_kind Self types;
+    access_list : Run_access_list Self types;
+  }.
+End Transaction.
+
+Module Impl_Transaction_for_Ref_Transaction.
+  Instance run
+    (Self : Set) `{Link Self}
+    (types : Transaction.Types.t) `{Transaction.Types.AreLinks types}
+    (run_Transaction_for_Self : Transaction.Run Self types) :
+    Transaction.Run (Ref.t Pointer.Kind.Ref Self) types.
+  Admitted.
+End Impl_Transaction_for_Ref_Transaction.
+
+(*
+pub trait TransactionGetter {
+    type Transaction: Transaction;
+
+    fn tx(&self) -> &Self::Transaction;
+}
+*)
+Module TransactionGetter.
+  Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
+    ("revm_context_interface::transaction::TransactionGetter", [], [], Φ Self).
+
+  Definition Run_tx
+    (Self : Set) `{Link Self}
+    (Transaction : Set) `{Link Transaction} :
+    Set :=
+    TraitMethod.C (trait Self) "tx" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] (Ref.t Pointer.Kind.Ref Transaction)
+    ).
+
+  Class Run
+      (Self : Set) `{Link Self}
+      (Transaction : Set) `{Link Transaction}
+      (types : Transaction.Types.t) `{Transaction.Types.AreLinks types} :
+      Set := {
+    Transaction_IsAssociated :
+      IsTraitAssociatedType
+        "revm_context_interface::transaction::TransactionGetter" [] [] (Φ Self)
+        "Transaction" (Φ Transaction);
+    run_Transaction_for_Transaction :
+      Transaction.Run Transaction types;
+    tx : Run_tx Self Transaction;
+  }.
+End TransactionGetter.
+
+(*
+pub trait TransactionSetter: TransactionGetter {
+    fn set_tx(&mut self, tx: <Self as TransactionGetter>::Transaction);
+}
+*)
+Module TransactionSetter.
+  Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
+    ("revm_context_interface::transaction::TransactionSetter", [], [], Φ Self).
+
+  Definition Run_set_tx
+    (Self : Set) `{Link Self}
+    (Transaction : Set) `{Link Transaction} :
+    Set :=
+    TraitMethod.C (trait Self) "set_tx" (fun method =>
+      forall (self : Ref.t Pointer.Kind.MutRef Self) (tx : Transaction),
+      Run.Trait method [] [] [ φ self; φ tx ] unit
+    ).
+
+  Class Run
+      (Self : Set) `{Link Self}
+      (Transaction : Set) `{Link Transaction}
+      (types : Transaction.Types.t) `{Transaction.Types.AreLinks types} :
+      Set := {
+    run_TransactionGetter_for_Self :
+      TransactionGetter.Run Self Transaction types;
+    set_tx : Run_set_tx Self Transaction;
+  }.
+End TransactionSetter.
diff --git a/CoqOfRust/revm/revm_context_interface/transaction/links/eip4844.v b/CoqOfRust/revm/revm_context_interface/transaction/links/eip4844.v
new file mode 100644
index 000000000..197e0129c
--- /dev/null
+++ b/CoqOfRust/revm/revm_context_interface/transaction/links/eip4844.v
@@ -0,0 +1,68 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.bits.links.address.
+Require Import alloy_primitives.links.aliases.
+
+(*
+pub trait Eip4844Tx: Eip1559CommonTxFields {
+    fn destination(&self) -> Address;
+    fn blob_versioned_hashes(&self) -> &[B256];
+    fn max_fee_per_blob_gas(&self) -> u128;
+    fn total_blob_gas(&self) -> u64;
+    fn calc_max_data_fee(&self) -> U256;
+}
+*)
+Module Eip4844Tx.
+  Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
+    ("revm_context_interface::transaction::eip4844::Eip4844Tx", [], [], Φ Self).
+
+  Definition Run_destination
+    (Self : Set) `{Link Self} :
+    Set :=
+    TraitMethod.C (trait Self) "destination" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] Address.t
+    ).
+
+  Definition Run_blob_versioned_hashes
+    (Self : Set) `{Link Self} :
+    Set :=
+    TraitMethod.C (trait Self) "blob_versioned_hashes" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] (Ref.t Pointer.Kind.Ref (list aliases.B256.t))
+    ).
+
+  Definition Run_max_fee_per_blob_gas
+    (Self : Set) `{Link Self} :
+    Set :=
+    TraitMethod.C (trait Self) "max_fee_per_blob_gas" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] U128.t
+    ).
+
+  Definition Run_total_blob_gas
+    (Self : Set) `{Link Self} :
+    Set :=
+    TraitMethod.C (trait Self) "total_blob_gas" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] U64.t
+    ).
+
+  Definition Run_calc_max_data_fee
+    (Self : Set) `{Link Self} :
+    Set :=
+    TraitMethod.C (trait Self) "calc_max_data_fee" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+      Run.Trait method [] [] [ φ self ] aliases.U256.t
+    ).
+
+  Class Run (Self : Set) `{Link Self} : Set := {
+    (* TODO *)
+    (* run_Eip1559CommonTxFields_for_Self : Eip1559CommonTxFields.Run Self; *)
+    destination : Run_destination Self;
+    blob_versioned_hashes : Run_blob_versioned_hashes Self;
+    max_fee_per_blob_gas : Run_max_fee_per_blob_gas Self;
+    total_blob_gas : Run_total_blob_gas Self;
+    calc_max_data_fee : Run_calc_max_data_fee Self;
+  }.
+End Eip4844Tx.
diff --git a/CoqOfRust/revm/revm_context_interface/transaction/links/transaction_type.v b/CoqOfRust/revm/revm_context_interface/transaction/links/transaction_type.v
new file mode 100644
index 000000000..b2d1c8588
--- /dev/null
+++ b/CoqOfRust/revm/revm_context_interface/transaction/links/transaction_type.v
@@ -0,0 +1,107 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import core.links.cmp.
+
+(*
+pub enum TransactionType {
+    Legacy,
+    Eip2930,
+    Eip1559,
+    Eip4844,
+    Eip7702,
+    Custom,
+}
+*)
+Module TransactionType.
+  Inductive t : Set :=
+  | Legacy
+  | Eip2930
+  | Eip1559
+  | Eip4844
+  | Eip7702
+  | Custom.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "revm_context_interface::transaction::transaction_type::TransactionType";
+    φ x :=
+      match x with
+      | Legacy => Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Legacy" []
+      | Eip2930 => Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Eip2930" []
+      | Eip1559 => Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Eip1559" []
+      | Eip4844 => Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Eip4844" []
+      | Eip7702 => Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Eip7702" []
+      | Custom => Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Custom" []
+      end;
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "revm_context_interface::transaction::transaction_type::TransactionType").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add apply of_ty : of_ty.
+
+  Lemma of_value_with_Legacy :
+    Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Legacy" [] = φ Legacy.
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_Legacy : of_value.
+
+  Lemma of_value_with_Eip2930 :
+    Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Eip2930" [] = φ Eip2930.
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_Eip2930 : of_value.
+
+  Lemma of_value_with_Eip1559 :
+    Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Eip1559" [] = φ Eip1559.
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_Eip1559 : of_value.
+
+  Lemma of_value_with_Eip4844 :
+    Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Eip4844" [] = φ Eip4844.
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_Eip4844 : of_value.
+
+  Lemma of_value_with_Eip7702 :
+    Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Eip7702" [] = φ Eip7702.
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_Eip7702 : of_value.
+
+  Lemma of_value_with_Custom :
+    Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Custom" [] = φ Custom.
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_Custom : of_value.
+
+  Definition of_value_Legacy :
+    OfValue.t (Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Legacy" []).
+  Proof. econstructor; apply of_value_with_Legacy. Defined.
+  Smpl Add apply of_value_Legacy : of_value.
+
+  Definition of_value_Eip2930 :
+    OfValue.t (Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Eip2930" []).
+  Proof. econstructor; apply of_value_with_Eip2930. Defined.
+  Smpl Add apply of_value_Eip2930 : of_value.
+
+  Definition of_value_Eip1559 :
+    OfValue.t (Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Eip1559" []).
+  Proof. econstructor; apply of_value_with_Eip1559. Defined.
+  Smpl Add apply of_value_Eip1559 : of_value.
+
+  Definition of_value_Eip4844 :
+    OfValue.t (Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Eip4844" []).
+  Proof. econstructor; apply of_value_with_Eip4844. Defined.
+  Smpl Add apply of_value_Eip4844 : of_value.
+
+  Definition of_value_Eip7702 :
+    OfValue.t (Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Eip7702" []).
+  Proof. econstructor; apply of_value_with_Eip7702. Defined.
+  Smpl Add apply of_value_Eip7702 : of_value.
+
+  Definition of_value_Custom :
+    OfValue.t (Value.StructTuple "revm_context_interface::transaction::transaction_type::TransactionType::Custom" []).
+  Proof. econstructor; apply of_value_with_Custom. Defined.
+  Smpl Add apply of_value_Custom : of_value.
+End TransactionType.
+
+Module Impl_PartialEq_for_TransactionType.
+  Definition Self : Set := TransactionType.t.
+
+  Instance run : PartialEq.Run Self Self.
+  Admitted.
+End Impl_PartialEq_for_TransactionType.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v
index cca617ca3..2e57d583a 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v
@@ -1,22 +1,26 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.bits.links.address.
+Require Import alloy_primitives.bits.links.fixed.
+Require Import core.convert.links.mod.
+Require Import core.links.option.
 Require Import revm.revm_context_interface.links.host.
 Require Import revm.revm_context_interface.links.block.
 Require Import revm.revm_interpreter.gas.links.constants.
 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.utility.
 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.
-Require Import core.convert.links.mod.
-Require Import core.links.option.
 
-Import Impl_SpecId.
+Import Impl_Address.
 Import Impl_Gas.
 Import from.Impl_Uint.
 Import Impl_Option.
+Import Impl_SpecId.
 
 (*
 pub fn chainid<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -41,18 +45,12 @@ Instance run_chainid
     unit.
 Proof.
   constructor.
-  cbn.
-  eapply Run.Rewrite. {
-    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.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
   destruct run_Host_for_H.
-  destruct run_CfgGetter.
+  destruct run_CfgGetter_for_Self.
   destruct run_Cfg_for_Cfg.
   run_symbolic.
 Defined.
@@ -74,27 +72,17 @@ Instance run_coinbase
   Run.Trait
     instructions.block_info.coinbase [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
     unit.
-Proof. 
+Proof.
   constructor.
-  cbn.
-  eapply Run.Rewrite. {
-    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.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
   destruct run_Host_for_H.
-  destruct run_BlockGetter.
+  destruct run_BlockGetter_for_Self.
   destruct run_Block_for_Block.
-  (* destruct alloy_primitives.bits.links.fixed.Impl_Into_U256_for_FixedBytes.run. *)
-  (* TODO: resolve axiomatization for:
-  - Impl_Address::into_word(?)
-  - FixedBytes::into()
-  *)
+  destruct (Impl_Into_for_From_T.run Impl_From_FixedBytes_32_for_U256.run).
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn timestamp<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -116,19 +104,13 @@ Instance run_timestamp
   Run.Trait
     instructions.block_info.timestamp [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
     unit.
-Proof. 
+Proof.
   constructor.
-  cbn.
-  eapply Run.Rewrite. {
-    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.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
   destruct run_Host_for_H.
-  destruct run_BlockGetter.
+  destruct run_BlockGetter_for_Self.
   destruct run_Block_for_Block.
   run_symbolic.
 Defined.
@@ -153,24 +135,18 @@ Instance run_block_number
   Run.Trait
     instructions.block_info.block_number [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
     unit.
-Proof. 
+Proof.
   constructor.
-  cbn.
-  eapply Run.Rewrite. {
-    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.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
   destruct run_Host_for_H.
-  destruct run_BlockGetter.
+  destruct run_BlockGetter_for_Self.
   destruct run_Block_for_Block.
   run_symbolic.
 Defined.
 
-(* 
+(*
 pub fn difficulty<WIRE: InterpreterTypes, H: Host + ?Sized>(
     interpreter: &mut Interpreter<WIRE>,
     host: &mut H,
@@ -187,29 +163,20 @@ Instance run_difficulty
   Run.Trait
     instructions.block_info.difficulty [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
     unit.
-Proof. 
+Proof.
   constructor.
-  cbn.
-  eapply Run.Rewrite. {
-    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.
   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_BlockGetter_for_Self.
   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
-  *)
+  destruct Impl_IntoU256_for_B256.run.
   run_symbolic.
-Admitted.
+Defined.
 
-(* 
+(*
 pub fn gaslimit<WIRE: InterpreterTypes, H: Host + ?Sized>(
     interpreter: &mut Interpreter<WIRE>,
     host: &mut H,
@@ -226,24 +193,18 @@ Instance run_gaslimit
   Run.Trait
     instructions.block_info.gaslimit [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
     unit.
-Proof. 
+Proof.
   constructor.
-  cbn.
-  eapply Run.Rewrite. {
-    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.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
   destruct run_Host_for_H.
-  destruct run_BlockGetter.
+  destruct run_BlockGetter_for_Self.
   destruct run_Block_for_Block.
   run_symbolic.
 Defined.
 
-(* 
+(*
 pub fn basefee<WIRE: InterpreterTypes, H: Host + ?Sized>(
     interpreter: &mut Interpreter<WIRE>,
     host: &mut H,
@@ -260,25 +221,19 @@ Instance run_basefee
   Run.Trait
     instructions.block_info.basefee [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
     unit.
-Proof. 
+Proof.
   constructor.
-  cbn.
-  eapply Run.Rewrite. {
-    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.
   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_BlockGetter_for_Self.
   destruct run_Block_for_Block.
   run_symbolic.
 Defined.
 
-(* 
+(*
 pub fn blob_basefee<WIRE: InterpreterTypes, H: Host + ?Sized>(
     interpreter: &mut Interpreter<WIRE>,
     host: &mut H,
@@ -295,20 +250,14 @@ Instance run_blob_basefee
   Run.Trait
     instructions.block_info.blob_basefee [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
     unit.
-Proof. 
+Proof.
   constructor.
-  cbn.
-  eapply Run.Rewrite. {
-    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.
   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_BlockGetter_for_Self.
   destruct run_Block_for_Block.
   run_symbolic.
 Defined.
\ No newline at end of file
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/control.v b/CoqOfRust/revm/revm_interpreter/instructions/links/control.v
index eb94e498b..7d70a9cdf 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/control.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/control.v
@@ -1,9 +1,33 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.bytes.links.mod.
+Require Import alloy_primitives.links.aliases.
+Require Import core.convert.links.num.
+Require Import core.links.option.
+Require Import core.links.result.
+Require Import core.num.links.mod.
+Require Import revm.revm_interpreter.gas.links.constants.
 Require Import revm.revm_interpreter.instructions.control.
+Require Import revm.revm_interpreter.interpreter.links.shared_memory.
+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.links.instruction_result.
+Require Import revm.revm_specification.links.hardfork.
+Require Import ruint.links.cmp.
+Require Import ruint.links.from.
+Require Import ruint.links.lib.
+
+Import Impl_Gas.
+Import Impl_Option.
+Import Impl_Result_T_E.
+Import Impl_SpecId.
+Import cmp.Impl_Uint.
+Import from.Impl_Uint.
+Import lib.Impl_Uint.
+Import Impl_u64.
+Import Impl_isize.
+Import Impl_usize.
 
 (*
 pub fn rjump<WIRE: InterpreterTypes, H: ?Sized>(
@@ -22,8 +46,13 @@ Instance run_rjump
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_LoopControl_for_Control.
+  destruct run_Jumps_for_Bytecode.
+  destruct run_Immediates_for_Bytecode.
+  destruct run_RuntimeFlag_for_RuntimeFlag.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn rjumpi<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -42,8 +71,14 @@ Instance run_rjumpi
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack. 
+  destruct run_LoopControl_for_Control.
+  destruct run_Jumps_for_Bytecode.
+  destruct run_Immediates_for_Bytecode.
+  destruct run_RuntimeFlag_for_RuntimeFlag.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn rjumpv<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -62,8 +97,33 @@ Instance run_rjumpv
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack. 
+  destruct run_LoopControl_for_Control.
+  destruct run_Jumps_for_Bytecode.
+  destruct run_Immediates_for_Bytecode.
+  destruct run_RuntimeFlag_for_RuntimeFlag.
+  destruct Impl_TryFrom_u64_for_isize.run.
   run_symbolic.
-Admitted.
+Defined.
+
+(* fn jump_inner<WIRE: InterpreterTypes>(interpreter: &mut Interpreter<WIRE>, target: U256) *)
+Instance run_jump_inner
+    {WIRE : Set} `{Link WIRE}
+    {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))
+    (target : aliases.U256.t) :
+  Run.Trait
+    instructions.control.jump_inner [] [ Φ WIRE ] [ φ interpreter; φ target ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_LoopControl_for_Control.
+  destruct run_Jumps_for_Bytecode.
+  run_symbolic.
+Defined.
 
 (*
 pub fn jump<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -82,8 +142,11 @@ Instance run_jump
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE eqn:?.
+  destruct run_StackTrait_for_Stack. 
+  destruct run_LoopControl_for_Control.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn jumpi<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -102,21 +165,11 @@ Instance run_jumpi
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE eqn:?.
+  destruct run_StackTrait_for_Stack. 
+  destruct run_LoopControl_for_Control.
   run_symbolic.
-Admitted.
-
-(* fn jump_inner<WIRE: InterpreterTypes>(interpreter: &mut Interpreter<WIRE>, target: U256) *)
-Instance run_jump_inner
-    {WIRE : Set} `{Link WIRE}
-    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
-    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) :
-  Run.Trait
-    instructions.control.jump_inner [] [ Φ WIRE ] [ φ interpreter ]
-    unit.
-Proof.
-  constructor.
-  run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn jumpdest_or_nop<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -135,8 +188,10 @@ Instance run_jumpdest_or_nop
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_LoopControl_for_Control.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn callf<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -155,8 +210,16 @@ Instance run_callf
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_Jumps_for_Bytecode.
+  destruct run_Immediates_for_Bytecode.
+  destruct run_EofCodeInfo_for_Bytecode.
+  destruct run_SubRoutineStack_for_SubRoutineStack.
+  destruct run_RuntimeFlag_for_RuntimeFlag.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn retf<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -175,8 +238,13 @@ Instance run_retf
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_LoopControl_for_Control.
+  destruct run_Jumps_for_Bytecode.
+  destruct run_SubRoutineStack_for_SubRoutineStack.
+  destruct run_RuntimeFlag_for_RuntimeFlag.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn jumpf<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -195,8 +263,16 @@ Instance run_jumpf
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_Jumps_for_Bytecode.
+  destruct run_Immediates_for_Bytecode.
+  destruct run_EofCodeInfo_for_Bytecode.
+  destruct run_SubRoutineStack_for_SubRoutineStack.
+  destruct run_RuntimeFlag_for_RuntimeFlag.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn pc<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -215,8 +291,12 @@ Instance run_pc
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_Jumps_for_Bytecode.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 fn return_inner(
@@ -227,13 +307,19 @@ fn return_inner(
 Instance run_return_inner
     {WIRE : Set} `{Link WIRE}
     {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))
-    (instruction_result : Ref.t Pointer.Kind.MutRef InstructionResult.t) :
+    (instruction_result : InstructionResult.t) :
   Run.Trait
     instructions.control.return_inner [] [ Φ WIRE ] [ φ interpreter; φ instruction_result ]
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_MemoryTrait_for_Memory.
+  destruct Impl_Default_for_Bytes.run.
   run_symbolic.
 Admitted.
 
@@ -255,7 +341,7 @@ Instance run_ret
 Proof.
   constructor.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn revert<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -274,8 +360,11 @@ Instance run_revert
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE eqn:?.
+  destruct run_LoopControl_for_Control.
+  destruct run_RuntimeFlag_for_RuntimeFlag.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn stop<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -294,11 +383,6 @@ Instance run_stop
     unit.
 Proof.
   constructor.
-  cbn.
-  eapply Run.Rewrite. {
-    erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE.
-    reflexivity.
-  }
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_LoopControl_for_Control.
   run_symbolic.
@@ -321,8 +405,10 @@ Instance run_invalid
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_LoopControl_for_Control.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn unknown<WIRE: InterpreterTypes, H: Host + ?Sized>(
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md b/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md
index e01a1f101..0454cdba7 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md
@@ -19,10 +19,10 @@
 ## Block_info
 
 - [x] `chainid`
-- [ ] `coinbase`
+- [x] `coinbase`
 - [x] `timestamp`
 - [x] `block_number`
-- [ ] `difficulty`
+- [x] `difficulty`
 - [x] `gaslimit`
 - [x] `basefee`
 - [x] `blob_basefee`
@@ -45,22 +45,22 @@
 
 ## Control
 
-- [ ] `rjump`
-- [ ] `rjumpi`
-- [ ] `rjumpv`
-- [ ] `jump`
-- [ ] `jumpi`
-- [ ] `jump_inner`
-- [ ] `jumpdest_or_nop`
-- [ ] `callf`
-- [ ] `retf`
-- [ ] `jumpf`
-- [ ] `pc`
+- [x] `rjump`
+- [x] `rjumpi`
+- [x] `rjumpv`
+- [x] `jump_inner`
+- [x] `jump`
+- [x] `jumpi`
+- [x] `jumpdest_or_nop`
+- [x] `callf`
+- [x] `retf`
+- [x] `jumpf`
+- [x] `pc`
 - [ ] `return_inner`
-- [ ] `ret`
-- [ ] `revert`
+- [x] `ret`
+- [x] `revert`
 - [x] `stop`
-- [ ] `invalid`
+- [x] `invalid`
 - [x] `unknown`
 
 ## Data
@@ -133,7 +133,7 @@
 
 ## Tx_info
 
-- [ ] `gasprice`
+- [x] `gasprice`
 - [ ] `origin`
 - [ ] `blob_hash`
 
@@ -144,6 +144,6 @@
 ## Summary
 
 - Total: 103
-- Admitted: 68
-- Defined: 35
-- Percentage: 33.98%
+- Admitted: 51
+- Defined: 52
+- Percentage: 50.49%
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/system.v b/CoqOfRust/revm/revm_interpreter/instructions/links/system.v
index 91bd42832..be8ab9618 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/system.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/system.v
@@ -22,7 +22,6 @@ Require Import revm.revm_specification.links.hardfork.
 Require Import ruint.links.from.
 
 Import Impl_Address.
-
 Import Impl_FixedBytes.
 Import Impl_Gas.
 Import Impl_Result_T_E.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/tx_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/tx_info.v
index dd8296fb5..355f85518 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/tx_info.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/tx_info.v
@@ -1,9 +1,35 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.bits.links.fixed.
+Require Import core.convert.links.mod.
+Require Import core.convert.links.num.
 Require Import core.links.cmp.
+Require Import core.links.option.
+Require Import core.links.result.
+Require Import core.num.links.mod.
+Require Import core.slice.links.index.
+Require Import core.slice.links.mod.
+Require Import revm.revm_context_interface.links.host.
+Require Import revm.revm_context_interface.links.transaction.
+Require Import revm.revm_context_interface.transaction.links.transaction_type.
+Require Import revm.revm_interpreter.gas.links.constants.
 Require Import revm.revm_interpreter.instructions.tx_info.
+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_specification.links.hardfork.
+Require Import ruint.links.from.
+
+Import Impl_Gas.
+Import Impl_Option.
+Import Impl_Result_T_E.
+Import Impl_Slice.
+Import Impl_SliceIndex_for_Usize.
+Import Impl_SpecId.
+Import from.Impl_Uint.
+Import lib.Impl_Uint.
+Import Impl_u64.
+Import Impl_usize.
 
 (*
 pub fn gasprice<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -15,6 +41,8 @@ Instance run_gasprice
   {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
@@ -22,8 +50,16 @@ Instance run_gasprice
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_Host_for_H.
+  destruct run_BlockGetter_for_Self.
+  destruct run_Block_for_Block.
+  destruct run_TransactionGetter_for_Self.
+  destruct run_Transaction_for_Transaction.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn origin<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -42,6 +78,10 @@ Instance run_origin
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct (Impl_Into_for_From_T.run Impl_From_FixedBytes_32_for_U256.run).
   run_symbolic.
 Admitted.
 
@@ -55,6 +95,8 @@ Instance run_blob_hash
   {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
@@ -62,5 +104,17 @@ Instance run_blob_hash
     unit.
 Proof.
   constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_RuntimeFlag_for_RuntimeFlag.
+  destruct run_Host_for_H.
+  destruct run_TransactionGetter_for_Self.
+  destruct Impl_TryFrom_u64_for_usize.run.
+  destruct Impl_PartialEq_for_TransactionType.run.
+  destruct (Impl_Transaction_for_Ref_Transaction.run _ _ run_Transaction_for_Transaction).
+  destruct run_Transaction_for_Transaction.
+  destruct run_Into_for_TransactionType.
+  destruct run_Eip4844Tx_for_Eip4844.
   run_symbolic.
 Admitted.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/utility.v b/CoqOfRust/revm/revm_interpreter/instructions/links/utility.v
index f36aef146..1d69484b4 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/utility.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/utility.v
@@ -4,10 +4,24 @@ Require Import alloy_primitives.bits.links.address.
 Require Import alloy_primitives.bits.links.fixed.
 Require Import alloy_primitives.links.aliases.
 Require Import core.convert.links.mod.
+Require Import core.fmt.links.mod.
+Require Import core.iter.traits.links.collect.
+Require Import core.links.panicking.
+Require Import core.num.links.mod.
+Require Import core.ptr.links.mut_ptr.
+Require Import core.slice.links.iter.
+Require Import core.slice.links.mod.
 Require Import revm.revm_interpreter.instructions.utility.
 Require Import ruint.links.bytes.
 
+Import Impl_Arguments.
+Import Impl_ChunksExact.
+Import Impl_pointer_mut_T.
+Import Impl_RChunksExact.
+Import Impl_Slice.
 Import bytes.Impl_Uint.
+Import lib.Impl_Uint.
+Import Impl_u64.
 
 (* pub fn cast_slice_to_u256(slice: &[u8], dest: &mut U256) *)
 Instance run_cast_slice_to_u256
@@ -16,6 +30,10 @@ Instance run_cast_slice_to_u256
   Run.Trait instructions.utility.cast_slice_to_u256 [] [] [ φ slice; φ dest ] unit.
 Proof.
   constructor.
+  destruct (Impl_IntoIterator_for_Iterator_I.run (ChunksExact.t U8.t) U8.t).
+  destruct (Impl_Iterator_for_ChunksExact.run U8.t).
+  destruct (Impl_IntoIterator_for_Iterator_I.run (RChunksExact.t U8.t) U8.t).
+  destruct (Impl_Iterator_for_RChunksExact.run U8.t).
   run_symbolic.
 Admitted.
 
diff --git a/CoqOfRust/revm/revm_interpreter/links/gas.v b/CoqOfRust/revm/revm_interpreter/links/gas.v
index 61cd41c2c..5a7858817 100644
--- a/CoqOfRust/revm/revm_interpreter/links/gas.v
+++ b/CoqOfRust/revm/revm_interpreter/links/gas.v
@@ -13,9 +13,7 @@ Require Import revm_interpreter.gas.
 
 (*
 pub struct MemoryGas {
-    /// Current memory length
     pub words_num: usize,
-    /// Current memory expansion cost
     pub expansion_cost: u64,
 }
 *)
diff --git a/CoqOfRust/ruint/links/lib.v b/CoqOfRust/ruint/links/lib.v
index 35d002a1f..200b8330b 100644
--- a/CoqOfRust/ruint/links/lib.v
+++ b/CoqOfRust/ruint/links/lib.v
@@ -66,4 +66,16 @@ Module Impl_Uint.
     constructor.
     run_symbolic.
   Admitted.
+
+  (* pub unsafe fn as_limbs_mut(&mut self) -> &mut [u64; LIMBS] *)
+  Instance run_as_limbs_mut
+    (BITS LIMBS : Usize.t)
+    (self : Ref.t Pointer.Kind.MutRef (Uint.t BITS LIMBS)) :
+    Run.Trait
+      (Impl_ruint_Uint_BITS_LIMBS.as_limbs_mut (φ BITS) (φ LIMBS)) [] [] [ φ self ]
+      (Ref.t Pointer.Kind.MutRef (array.t U64.t LIMBS)).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
 End Impl_Uint.