diff --git a/CoqOfRust/alloy_primitives/bytes/links/mod.v b/CoqOfRust/alloy_primitives/bytes/links/mod.v
index 6fba7d417..0a42efafb 100644
--- a/CoqOfRust/alloy_primitives/bytes/links/mod.v
+++ b/CoqOfRust/alloy_primitives/bytes/links/mod.v
@@ -121,3 +121,4 @@ Module Impl_From_Vec_u8_for_Bytes.
   Instance run : From.Run Self (Vec.t U8.t Global.t).
   Admitted.
 End Impl_From_Vec_u8_for_Bytes.
+Export Impl_From_Vec_u8_for_Bytes.
diff --git a/CoqOfRust/core/iter/traits/links/iterator.v b/CoqOfRust/core/iter/traits/links/iterator.v
index 9d3b1f495..ec0bbedde 100644
--- a/CoqOfRust/core/iter/traits/links/iterator.v
+++ b/CoqOfRust/core/iter/traits/links/iterator.v
@@ -199,7 +199,7 @@ Module Iterator.
       Set :=
     TraitMethod.C (trait Self) "any" (fun method =>
       forall
-         (F : Set) `{Link F}
+         (F : Set) `(Link F)
          (self : Ref.t Pointer.Kind.MutRef Self)
          (f : F)
          `(FnMut.Run F Item bool),
diff --git a/CoqOfRust/core/links/default.v b/CoqOfRust/core/links/default.v
index 2f0dee7d4..92932efb3 100644
--- a/CoqOfRust/core/links/default.v
+++ b/CoqOfRust/core/links/default.v
@@ -61,10 +61,12 @@ Module Impl_Default_for_bool.
     Default.default := run_default;
   }.
 End Impl_Default_for_bool.
+Export Impl_Default_for_bool.
 
 Module Impl_Default_for_char.
   (* TODO *)
 End Impl_Default_for_char.
+Export Impl_Default_for_char.
 
 Module Impl_Default_for_integer.
   Definition Self (kind : IntegerKind.t) : Set :=
@@ -123,3 +125,4 @@ Module Impl_Default_for_integer.
     Default.default := run_default kind;
   }.
 End Impl_Default_for_integer.
+Export Impl_Default_for_integer.
diff --git a/CoqOfRust/core/links/option.v b/CoqOfRust/core/links/option.v
index 8e51449e0..f6a5f5e5d 100644
--- a/CoqOfRust/core/links/option.v
+++ b/CoqOfRust/core/links/option.v
@@ -1,6 +1,9 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
 Require Import core.convert.links.mod.
+Require Import core.links.default.
+Require Import core.links.hint.
+Require Import core.links.panickingAux.
 Require Import core.links.result.
 Require Import core.option.
 Require Import core.ops.links.function.
@@ -86,6 +89,26 @@ Module Option.
   End SubPointer.
 End Option.
 
+(* const fn unwrap_failed() -> ! *)
+Instance run_unwrap_failed :
+  Run.Trait
+    option.unwrap_failed [] [] []
+    Empty_set.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.
+
+(* const fn expect_failed(msg: &str) -> ! *)
+Instance run_expect_failed (msg : Ref.t Pointer.Kind.Ref string) :
+  Run.Trait
+    option.expect_failed [] [] [ φ msg ]
+    Empty_set.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.
+
 Module Impl_Option.
   Definition Self (T : Set) `{Link T} : Set := option T.
 
@@ -120,7 +143,7 @@ Module Impl_Option.
   Proof.
     constructor.
     run_symbolic.
-  Admitted.
+  Defined.
 
   (* pub const unsafe fn unwrap_unchecked(self) -> T *)
   Instance run_unwrap_unchecked {T : Set} `{Link T}
@@ -128,15 +151,27 @@ Module Impl_Option.
     Run.Trait
       (option.Impl_core_option_Option_T.unwrap_unchecked (Φ T)) [] [] [ φ self ]
       T.
-  Admitted.
+  Proof.
+    constructor.
+    run_symbolic.
+  Defined.
 
-  (* pub fn unwrap_or_default(self) -> T *)
+  (*
+    pub fn unwrap_or_default(self) -> T
+    where
+        T: Default,
+  *)
   Instance run_unwrap_or_default {T : Set} `{Link T}
+      {run_Default_for_T : Default.Run T}
       (self : Self T) :
     Run.Trait
       (option.Impl_core_option_Option_T.unwrap_or_default (Φ T)) [] [] [ φ self ]
       T.
-  Admitted.
+  Proof.
+    constructor.
+    destruct run_Default_for_T.
+    run_symbolic.
+  Defined.
 
   (* pub fn unwrap_or(self, default: T) -> T *)
   Instance run_unwrap_or {T : Set} `{Link T}
@@ -155,7 +190,10 @@ Module Impl_Option.
     Run.Trait
       (option.Impl_core_option_Option_T.expect (Φ T)) [] [] [ φ self; φ msg ]
       T.
-  Admitted.
+  Proof.
+    constructor.
+    run_symbolic.
+  Defined.
 End Impl_Option.
 Export Impl_Option.
 
diff --git a/CoqOfRust/core/links/panicking.v b/CoqOfRust/core/links/panicking.v
index e4927cf20..0879373b4 100644
--- a/CoqOfRust/core/links/panicking.v
+++ b/CoqOfRust/core/links/panicking.v
@@ -4,21 +4,7 @@ Require Import core.fmt.links.mod.
 Require Import core.links.option.
 Require Import core.panicking.
 
-(* pub const fn panic_fmt(fmt: fmt::Arguments<'_>) -> ! *)
-Instance run_panic_fmt (fmt : Arguments.t) :
-  Run.Trait panicking.panic_fmt [] [] [φ fmt] Empty_set.
-Proof.
-  constructor.
-  run_symbolic.
-Admitted.
-
-(* pub const fn panic(expr: &'static str) -> ! *)
-Instance run_panic (expr : Ref.t Pointer.Kind.Ref string) :
-  Run.Trait panicking.panic [] [] [φ expr] Empty_set.
-Proof.
-  constructor.
-  run_symbolic.
-Admitted.
+Require Export core.links.panickingAux.
 
 (*
 pub enum AssertKind {
diff --git a/CoqOfRust/core/links/panickingAux.v b/CoqOfRust/core/links/panickingAux.v
new file mode 100644
index 000000000..fab58ff00
--- /dev/null
+++ b/CoqOfRust/core/links/panickingAux.v
@@ -0,0 +1,31 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import core.fmt.links.mod.
+Require Import core.panicking.
+
+(* pub const fn panic_fmt(fmt: fmt::Arguments<'_>) -> ! *)
+Instance run_panic_fmt (fmt : Arguments.t) :
+  Run.Trait panicking.panic_fmt [] [] [φ fmt] Empty_set.
+Proof.
+  constructor.
+  run_symbolic.
+Admitted.
+
+(* pub const fn panic(expr: &'static str) -> ! *)
+Instance run_panic (expr : Ref.t Pointer.Kind.Ref string) :
+  Run.Trait panicking.panic [] [] [φ expr] Empty_set.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.
+
+(* pub const fn panic_display<T: fmt::Display>(x: &T) -> ! *)
+Instance run_panic_display {T : Set} `{Link T}
+    (x : Ref.t Pointer.Kind.Ref T) :
+  Run.Trait
+    panicking.panic_display [] [Φ T] [φ x]
+    Empty_set.
+Proof.
+  constructor.
+  run_symbolic.
+Admitted.
diff --git a/CoqOfRust/revm/revm_context_interface/links/host.v b/CoqOfRust/revm/revm_context_interface/links/host.v
index bc8e4dc84..edf72a264 100644
--- a/CoqOfRust/revm/revm_context_interface/links/host.v
+++ b/CoqOfRust/revm/revm_context_interface/links/host.v
@@ -17,10 +17,45 @@ pub struct SStoreResult {
 }
 *)
 Module SStoreResult.
-  Parameter t : Set.
+  Record t : Set := {
+    original_value : aliases.U256.t;
+    present_value : aliases.U256.t;
+    new_value : aliases.U256.t;
+  }.
 
-  Global Instance IsLink : Link t.
-  Admitted.
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "revm_context_interface::host::SStoreResult";
+    φ x :=
+      Value.StructRecord "revm_context_interface::host::SStoreResult" [] [] [
+        ("original_value", φ x.(original_value));
+        ("present_value", φ x.(present_value));
+        ("new_value", φ x.(new_value))
+      ]
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "revm_context_interface::host::SStoreResult").
+  Proof.
+    eapply OfTy.Make with (A := t).
+    reflexivity.
+  Defined.
+  Smpl Add apply of_ty : of_ty.
+
+  Lemma of_value_with
+      original_value' original_value
+      present_value' present_value
+      new_value' new_value :
+    original_value' = φ original_value ->
+    present_value' = φ present_value ->
+    new_value' = φ new_value ->
+    Value.StructRecord "revm_context_interface::host::SStoreResult" [] [] [
+      ("original_value", original_value');
+      ("present_value", present_value');
+      ("new_value", new_value')
+    ] = φ (Build_t original_value present_value new_value).
+  Proof.
+    now intros; subst.
+  Qed.
+  Smpl Add unshelve eapply of_value_with : of_value.
 End SStoreResult.
 
 (*
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v
index af741bbdf..443928b68 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v
@@ -3,6 +3,7 @@ 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.default.
 Require Import core.links.option.
 Require Import revm.revm_context_interface.links.host.
 Require Import revm.revm_context_interface.links.block.
@@ -256,4 +257,4 @@ Proof.
   destruct run_BlockGetter_for_Self.
   destruct run_Block_for_Block.
   run_symbolic.
-Defined.
\ No newline at end of file
+Defined.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call.v
index fd9c7e042..36960c9e0 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call.v
@@ -66,4 +66,4 @@ Proof.
   destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
   destruct Impl_IntoAddress_for_U256.run.
   run_symbolic.
-Defined.
+Admitted.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call_code.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call_code.v
index 391f26047..313a0d4e2 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call_code.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call_code.v
@@ -67,4 +67,4 @@ Proof.
   destruct Impl_From_U256_for_FixedBytes_32.run.
   destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
   run_symbolic.
-Defined.
+Admitted.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/delegate_call.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/delegate_call.v
index dd264c8aa..23d167167 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/delegate_call.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/delegate_call.v
@@ -66,4 +66,4 @@ Proof.
   destruct Impl_From_U256_for_FixedBytes_32.run.
   destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
   run_symbolic.
-Defined.
+Admitted.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall.v
index 9b1968cf1..5a0a9e764 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall.v
@@ -66,4 +66,4 @@ Proof.
   destruct run_InputsTrait_for_Input.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   run_symbolic.
-Defined.
+Admitted.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extdelegatecall.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extdelegatecall.v
index 4c489038d..5d784e668 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extdelegatecall.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extdelegatecall.v
@@ -65,4 +65,4 @@ Proof.
   destruct run_InputsTrait_for_Input.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   run_symbolic.
-Defined.
+Admitted.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extstaticcall.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extstaticcall.v
index 051a3a1d6..361722361 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extstaticcall.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extstaticcall.v
@@ -65,4 +65,4 @@ Proof.
   destruct run_InputsTrait_for_Input.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   run_symbolic.
-Defined.
+Admitted.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/pop_extcall_target_address.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/pop_extcall_target_address.v
index 35a6d8955..0df6113b0 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/pop_extcall_target_address.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/pop_extcall_target_address.v
@@ -61,4 +61,4 @@ Proof.
   destruct (Impl_Iterator_for_Iter.run U8.t).
   destruct (Impl_Index_for_FixedBytes_N.run {| Integer.value := 32 |} (RangeTo.t Usize.t)).
   run_symbolic.
-Defined.
+Admitted.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/static_call.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/static_call.v
index e4fa16896..5348df418 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/static_call.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/static_call.v
@@ -66,4 +66,4 @@ Proof.
   destruct Impl_From_U256_for_FixedBytes_32.run.
   destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
   run_symbolic.
-Defined.
+Admitted.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/control.v b/CoqOfRust/revm/revm_interpreter/instructions/links/control.v
index a60d20365..9167a1915 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/control.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/control.v
@@ -1,7 +1,9 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
+Require Import alloc.links.slice.
 Require Import alloy_primitives.bytes.links.mod.
 Require Import alloy_primitives.links.aliases.
+Require Import core.convert.links.mod.
 Require Import core.convert.links.num.
 Require Import core.links.option.
 Require Import core.links.result.
@@ -308,7 +310,9 @@ Proof.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_MemoryTrait_for_Memory.
+  destruct run_Deref_for_Synthetic1.
   destruct Impl_Default_for_Bytes.run.
+  destruct (Impl_Into_for_From_T.run Impl_From_Vec_u8_for_Bytes.run).
   run_symbolic.
 Admitted.
 
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/host.v b/CoqOfRust/revm/revm_interpreter/instructions/links/host.v
index d82aa7d18..5a848e661 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/host.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/host.v
@@ -1,8 +1,10 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.bits.links.fixed.
 Require Import alloy_primitives.bytes.links.mod.
 Require Import alloy_primitives.links.aliases.
 Require Import bytes.links.bytes.
+Require Import core.convert.links.mod.
 Require Import revm.revm_context_interface.links.host.
 Require Import revm.revm_context_interface.links.journaled_state.
 Require Import revm.revm_interpreter.gas.links.calc.
@@ -87,7 +89,7 @@ Instance run_extcodesize
   (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
     instructions.host.extcodesize [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
-    aliases.U256.t.
+    unit.
 Proof.
   constructor.
   destruct run_InterpreterTypes_for_WIRE.
@@ -98,8 +100,7 @@ Proof.
   destruct Impl_IntoAddress_for_U256.run.
   destruct alloy_primitives.bytes.links.mod.Impl_Deref_for_Bytes.run.
   run_symbolic.
-  (* Errors in the type annotations *)
-Admitted.
+Defined.
 
 (*
 pub fn extcodehash<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -112,24 +113,23 @@ Instance run_extcodehash
   {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
   {H_types : Host.Types.t} `{Host.Types.AreLinks H_types}
   (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+  (run_Host_for_H : Host.Run H H_types)
   (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
   (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
     instructions.host.extcodehash [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
-    aliases.U256.t.
+    unit.
 Proof.
   constructor.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
-  (* destruct run_Host_for_H. *)
+  destruct run_Host_for_H.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   destruct run_LoopControl_for_Control.
-  (* TODO:
-  - Value.Tuple [] = lib.Uint.IsLink.(φ) ?return_
-  ^ (?What is this?)
-  *)
+  destruct (Impl_Into_for_From_T.run Impl_From_FixedBytes_32_for_U256.run).
+  destruct Impl_IntoAddress_for_U256.run.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn extcodecopy<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -142,6 +142,7 @@ Instance run_extcodecopy
   {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
   {H_types : Host.Types.t} `{Host.Types.AreLinks H_types}
   (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+  (run_Host_for_H : Host.Run H H_types)
   (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
   (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
@@ -151,14 +152,13 @@ Proof.
   constructor.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
-  (* destruct run_Host_for_H. *)
+  destruct run_MemoryTrait_for_Memory.
+  destruct run_Host_for_H.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   destruct run_LoopControl_for_Control.
-  (* TODO:
-  - "revm_interpreter::instructions::utility::IntoAddress"::into_address
-  ^ with a correct instance of Self maybe?
-  *)
+  destruct Impl_IntoAddress_for_U256.run.
   run_symbolic.
+  (* A lot of functions to link *)
 Admitted.
 
 (*
@@ -168,25 +168,23 @@ pub fn blockhash<WIRE: InterpreterTypes, H: Host + ?Sized>(
 )
 *)
 Instance run_blockhash
-  {WIRE H : Set} `{Link WIRE} `{Link H}
-  {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
-  {H_types : Host.Types.t} `{Host.Types.AreLinks H_types}
-  (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
-  (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
-  (host : Ref.t Pointer.Kind.MutRef H) :
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    {H_types : Host.Types.t} `{Host.Types.AreLinks H_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (run_Host_for_H : Host.Run H H_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
     instructions.host.blockhash [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
-    aliases.U256.t.
+    unit.
 Proof.
   constructor.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
-  (* destruct run_Host_for_H. *)
+  destruct run_Host_for_H.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   destruct run_LoopControl_for_Control.
-  (* TODO:
-  - Value.Tuple [] = lib.Uint.IsLink.(φ) ?return_
-  *)
   run_symbolic.
 Admitted.
 
@@ -197,29 +195,26 @@ pub fn sload<WIRE: InterpreterTypes, H: Host + ?Sized>(
 )
 *)
 Instance run_sload
-  {WIRE H : Set} `{Link WIRE} `{Link H}
-  {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
-  {H_types : Host.Types.t} `{Host.Types.AreLinks H_types}
-  (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
-  (run_Host_for_H : Host.Run H H_types)
-  (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
-  (host : Ref.t Pointer.Kind.MutRef H) :
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    {H_types : Host.Types.t} `{Host.Types.AreLinks H_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (run_Host_for_H : Host.Run H H_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
     instructions.host.sload [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
-    aliases.U256.t.
+    unit.
 Proof.
   constructor.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
-  destruct run_Host_for_H.
+  destruct run_InputsTrait_for_Input.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   destruct run_LoopControl_for_Control.
-  (* TODO:
-  - revm_interpreter::interpreter_types::InputsTrait::target_address
-  ^ `Self` issue?
-  *)
+  destruct run_Host_for_H.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn sstore<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -228,13 +223,13 @@ pub fn sstore<WIRE: InterpreterTypes, H: Host + ?Sized>(
 )
 *)
 Instance run_sstore
-  {WIRE H : Set} `{Link WIRE} `{Link H}
-  {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
-  {H_types : Host.Types.t} `{Host.Types.AreLinks H_types}
-  (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
-  (run_Host_for_H : Host.Run H H_types)
-  (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
-  (host : Ref.t Pointer.Kind.MutRef H) :
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    {H_types : Host.Types.t} `{Host.Types.AreLinks H_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (run_Host_for_H : Host.Run H H_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
     instructions.host.sstore [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
     unit.
@@ -242,12 +237,10 @@ Proof.
   constructor.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
-  destruct run_Host_for_H.
+  destruct run_InputsTrait_for_Input.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   destruct run_LoopControl_for_Control.
-  (* TODO:
-  - "revm_interpreter::interpreter_types::InputsTrait"::target_address
-  *)
+  destruct run_Host_for_H.
   run_symbolic.
 Admitted.
 
@@ -258,13 +251,13 @@ pub fn tstore<WIRE: InterpreterTypes, H: Host + ?Sized>(
 )
 *)
 Instance run_tstore
-  {WIRE H : Set} `{Link WIRE} `{Link H}
-  {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
-  {H_types : Host.Types.t} `{Host.Types.AreLinks H_types}  
-  (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
-  (run_Host_for_H : Host.Run H H_types)
-  (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
-  (host : Ref.t Pointer.Kind.MutRef H) :
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    {H_types : Host.Types.t} `{Host.Types.AreLinks H_types}  
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (run_Host_for_H : Host.Run H H_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
     instructions.host.tstore [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
     unit.
@@ -272,14 +265,12 @@ Proof.
   constructor.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
-  destruct run_Host_for_H.
+  destruct run_InputsTrait_for_Input.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   destruct run_LoopControl_for_Control.
-  (* TODO:
-  - "revm_interpreter::interpreter_types::InputsTrait"::target_address
-  *)
+  destruct run_Host_for_H.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn tload<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -288,22 +279,26 @@ pub fn tload<WIRE: InterpreterTypes, H: Host + ?Sized>(
 )
 *)
 Instance run_tload
-  {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) :
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    {H_types : Host.Types.t} `{Host.Types.AreLinks H_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (run_Host_for_H : Host.Run H H_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
     instructions.host.tload [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
-    aliases.U256.t.
+    unit.
 Proof.
   constructor.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   destruct run_LoopControl_for_Control.
+  destruct run_InputsTrait_for_Input.
+  destruct run_Host_for_H.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn log<const N: usize, H: Host + ?Sized>(
@@ -311,26 +306,27 @@ pub fn log<const N: usize, H: Host + ?Sized>(
     host: &mut H,
 )
 *)
-(* TODO: fill in parameter `N` : usize *)
 Instance run_log
-  {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) :
+    {N : Usize.t}
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    {H_types : Host.Types.t} `{Host.Types.AreLinks H_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (run_Host_for_H : Host.Run H H_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
-    instructions.host.log [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
+    instructions.host.log [ φ N ] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
     unit.
 Proof.
   constructor.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
+  destruct run_MemoryTrait_for_Memory.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   destruct run_LoopControl_for_Control.
-  (* TODO: 
-  - {{impossible "wrong number of arguments" 🔽 unit}}
-  *)
-  (* run_symbolic. *)
+  destruct run_Host_for_H.
+  run_symbolic.
 Admitted.
 
 (*
@@ -340,11 +336,13 @@ pub fn selfdestruct<WIRE: InterpreterTypes, H: Host + ?Sized>(
 )
 *)
 Instance run_selfdestruct
-  {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) :
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    {H_types : Host.Types.t} `{Host.Types.AreLinks H_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (run_Host_for_H : Host.Run H H_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
     instructions.host.selfdestruct [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
     unit.
@@ -354,8 +352,11 @@ Proof.
   destruct run_StackTrait_for_Stack.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   destruct run_LoopControl_for_Control.
-  (* TODO: 
-  - "revm_interpreter::instructions::utility::IntoAddress"::into_address
-  *)
+  destruct run_Host_for_H.
+  run_symbolic.
+  { destruct Impl_IntoAddress_for_U256.run.
+    run_symbolic.
+  }
+  destruct run_InputsTrait_for_Input.
   run_symbolic.
 Admitted.
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 bdcd5bee9..d8d71c796 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md
@@ -77,14 +77,14 @@
 
 - [x] `balance`
 - [x] `selfbalance`
-- [ ] `extcodesize`
-- [ ] `extcodehash`
+- [x] `extcodesize`
+- [x] `extcodehash`
 - [ ] `extcodecopy`
 - [ ] `blockhash`
-- [ ] `sload`
+- [x] `sload`
 - [ ] `sstore`
-- [ ] `tstore`
-- [ ] `tload`
+- [x] `tstore`
+- [x] `tload`
 - [ ] `log`
 - [ ] `selfdestruct`
 
@@ -150,11 +150,11 @@
 
 ## Contract/Call
 
-- [x] `call`
+- [ ] `call`
 
 ## Contract/Call_code
 
-- [x] `call_code`
+- [ ] `call_code`
 
 ## Contract/Create
 
@@ -162,7 +162,7 @@
 
 ## Contract/Delegate_call
 
-- [x] `delegate_call`
+- [ ] `delegate_call`
 
 ## Contract/Eofcreate
 
@@ -170,7 +170,7 @@
 
 ## Contract/Extcall
 
-- [x] `extcall`
+- [ ] `extcall`
 
 ## Contract/Extcall_gas_calc
 
@@ -182,15 +182,15 @@
 
 ## Contract/Extdelegatecall
 
-- [x] `extdelegatecall`
+- [ ] `extdelegatecall`
 
 ## Contract/Extstaticcall
 
-- [x] `extstaticcall`
+- [ ] `extstaticcall`
 
 ## Contract/Pop_extcall_target_address
 
-- [x] `pop_extcall_target_address`
+- [ ] `pop_extcall_target_address`
 
 ## Contract/Return_contract
 
@@ -198,11 +198,11 @@
 
 ## Contract/Static_call
 
-- [x] `static_call`
+- [ ] `static_call`
 
 ## Summary
 
 - Total: 120
-- Admitted: 21
-- Defined: 99
-- Percentage: 82.50%
+- Admitted: 24
+- Defined: 96
+- Percentage: 80.00%