diff --git a/CoqOfRust/alloy_primitives/bits/links/address.v b/CoqOfRust/alloy_primitives/bits/links/address.v
index dc5f60d00..e5205fc4d 100644
--- a/CoqOfRust/alloy_primitives/bits/links/address.v
+++ b/CoqOfRust/alloy_primitives/bits/links/address.v
@@ -24,16 +24,16 @@ Module Impl_Address.
     Address.t.
 
   (* pub fn from_word(word: FixedBytes<32>) -> Self *)
-  Instance run_from_word (word : fixed.FixedBytes.t {| Integer.value := 32 |}) :
+  Instance run_from_word (word : FixedBytes.t {| Integer.value := 32 |}) :
     Run.Trait
       bits.address.Impl_alloy_primitives_bits_address_Address.from_word [] [] [ φ word ]
       Self.
   Admitted.
 
   (* pub fn into_word(&self) -> FixedBytes<32> *)
-  Instance run_into_word (self : Address.t) :
+  Instance run_into_word (self : Ref.t Pointer.Kind.Ref Self) :
     Run.Trait
       bits.address.Impl_alloy_primitives_bits_address_Address.into_word [] [] [ φ self ]
-      (fixed.FixedBytes.t {| Integer.value := 32 |}).
+      (FixedBytes.t {| Integer.value := 32 |}).
   Admitted.
 End Impl_Address.
\ No newline at end of file
diff --git a/CoqOfRust/alloy_primitives/bits/links/fixed.v b/CoqOfRust/alloy_primitives/bits/links/fixed.v
index b13b807e3..31243b0a8 100644
--- a/CoqOfRust/alloy_primitives/bits/links/fixed.v
+++ b/CoqOfRust/alloy_primitives/bits/links/fixed.v
@@ -1,35 +1,24 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import core.links.array.
+Require Import alloy_primitives.links.aliases.
+Require Export alloy_primitives.bits.links.fixed_FixedBytes.
 Require Import alloy_primitives.bits.fixed.
-
-(* pub struct FixedBytes<const N: usize>(pub [u8; N]); *)
-Module FixedBytes.
-  Parameter t : Usize.t -> Set.
-
-  Parameter to_value : forall {N: Usize.t}, t N -> Value.t.
-
-  Global Instance IsLink (N: Usize.t): Link (t N) := {
-    Φ := Ty.apply (Ty.path "alloy_primitives::bits::fixed::FixedBytes") [ φ N ] [];
-    φ := to_value;
-  }.
-
-  Definition of_ty (N' : Value.t) (N: Usize.t) :
-    N' = φ N ->
-    OfTy.t (Ty.apply (Ty.path "alloy_primitives::bits::fixed::FixedBytes") [ N' ] []).
-  Proof.
-    intros.
-    eapply OfTy.Make with (A := t N).
-    subst.
-    reflexivity.
-  Defined.
-  Smpl Add eapply of_ty : of_ty.
-End FixedBytes.
+Require Import core.convert.links.mod.
+Require Import core.links.array.
 
 Module Impl_FixedBytes.
   Definition Self (N: Usize.t) : Set :=
     FixedBytes.t N.
 
+  (* pub const ZERO: Self *)
+  Instance run_zero (N: Usize.t) :
+    Run.Trait
+      (bits.fixed.Impl_alloy_primitives_bits_fixed_FixedBytes_N.value_ZERO (φ N)) [] [] []
+      (Self N).
+  Proof.
+    constructor.
+  Admitted.
+
   (* pub fn new(bytes: [u8; N]) -> Self *)
   Instance run_new (N: Usize.t) (bytes: array.t U8.t N) :
     Run.Trait
@@ -40,3 +29,26 @@ Module Impl_FixedBytes.
     run_symbolic.
   Admitted.
 End Impl_FixedBytes.
+
+Module Impl_From_FixedBytes_32_for_U256.
+  Definition Self : Set :=
+    aliases.U256.t.
+
+  Definition run_from : From.Run_from aliases.U256.t (FixedBytes.t {| Integer.value := 32 |}).
+  Proof.
+    eexists.
+    { eapply IsTraitMethod.Defined.
+      { apply bits.fixed.Impl_core_convert_From_alloy_primitives_bits_fixed_FixedBytes_Usize_32_for_ruint_Uint_Usize_256_Usize_4.Implements. }
+      { reflexivity. }
+    }
+    { constructor.
+      run_symbolic.
+      all: admit.
+    }
+  Admitted.
+
+  Instance run : From.Run aliases.U256.t (FixedBytes.t {| Integer.value := 32 |}) :=
+  {
+    From.from := run_from;
+  }.
+End Impl_From_FixedBytes_32_for_U256.
diff --git a/CoqOfRust/alloy_primitives/bits/links/fixed_FixedBytes.v b/CoqOfRust/alloy_primitives/bits/links/fixed_FixedBytes.v
new file mode 100644
index 000000000..b8a95bedd
--- /dev/null
+++ b/CoqOfRust/alloy_primitives/bits/links/fixed_FixedBytes.v
@@ -0,0 +1,25 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+
+(* pub struct FixedBytes<const N: usize>(pub [u8; N]); *)
+Module FixedBytes.
+  Parameter t : Usize.t -> Set.
+
+  Parameter to_value : forall {N: Usize.t}, t N -> Value.t.
+
+  Global Instance IsLink (N: Usize.t): Link (t N) := {
+    Φ := Ty.apply (Ty.path "alloy_primitives::bits::fixed::FixedBytes") [ φ N ] [];
+    φ := to_value;
+  }.
+
+  Definition of_ty (N' : Value.t) (N: Usize.t) :
+    N' = φ N ->
+    OfTy.t (Ty.apply (Ty.path "alloy_primitives::bits::fixed::FixedBytes") [ N' ] []).
+  Proof.
+    intros.
+    eapply OfTy.Make with (A := t N).
+    subst.
+    reflexivity.
+  Defined.
+  Smpl Add eapply of_ty : of_ty.
+End FixedBytes.
diff --git a/CoqOfRust/alloy_primitives/links/aliases.v b/CoqOfRust/alloy_primitives/links/aliases.v
index 76a642b4f..d2cf393fc 100644
--- a/CoqOfRust/alloy_primitives/links/aliases.v
+++ b/CoqOfRust/alloy_primitives/links/aliases.v
@@ -1,6 +1,6 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import alloy_primitives.bits.links.fixed.
+Require Import alloy_primitives.bits.links.fixed_FixedBytes.
 Require Import alloy_primitives.signed.links.int.
 Require Import ruint.links.lib.
 
diff --git a/CoqOfRust/core/convert/links/mod.v b/CoqOfRust/core/convert/links/mod.v
index 2d6fcba22..9a752870d 100644
--- a/CoqOfRust/core/convert/links/mod.v
+++ b/CoqOfRust/core/convert/links/mod.v
@@ -1,7 +1,7 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
 Require Import core.convert.mod.
-
+Require Import core.links.result.
 (*
 pub trait From<T>: Sized {
     fn from(value: T) -> Self;
@@ -17,7 +17,7 @@ Module From.
       Run.Trait method [] [] [ φ value ] Self
     ).
 
-  Class Run (Self : Set) {T : Set} `{Link Self} `{Link T} : Set := {
+  Class Run (Self : Set) (T : Set) `{Link Self} `{Link T} : Set := {
     from : Run_from Self T;
   }.
 End From.
@@ -33,7 +33,7 @@ Module Into.
 
   Definition Run_into (Self T : Set) `{Link Self} `{Link T} : Set :=
     TraitMethod.C (trait Self T) "into" (fun method =>
-      forall (self : Ref.t Pointer.Kind.Ref Self),
+      forall (self : Self),
         Run.Trait method [] [] [ φ self ] T
     ).
 
@@ -41,3 +41,99 @@ Module Into.
     into : Run_into Self T;
   }.
 End Into.
+
+(*
+impl<T, U> Into<U> for T
+where
+    U: From<T>,
+*)
+Module Impl_Into_for_From_T.
+  Definition run_into
+    (T U : Set) `{Link T} `{Link U}
+    (run_From_for_U : From.Run U T) :
+    Into.Run_into T U.
+  Proof.
+    eexists.
+    { eapply IsTraitMethod.Defined.
+      { apply convert.Impl_core_convert_Into_where_core_convert_From_U_T_U_for_T.Implements. }
+      { reflexivity. }
+    }
+    { constructor.
+      destruct run_From_for_U.
+      run_symbolic.
+    }
+  Defined.
+
+  Instance run
+    {T U : Set} `{Link T} `{Link U}
+    (run_From_for_U : From.Run U T) :
+    Into.Run T U :=
+  {
+    Into.into := run_into T U run_From_for_U;
+  }.
+End Impl_Into_for_From_T.
+
+(*
+pub trait AsRef<T: ?Sized> {
+    fn as_ref(&self) -> &T;
+}
+*)
+Module AsRef.
+  Definition trait (Self T : Set) `{Link Self} `{Link T} : TraitMethod.Header.t :=
+    ("core::convert::AsRef", [], [Φ T], Φ Self).
+
+  Definition Run_as_ref (Self T : Set) `{Link Self} `{Link T} : Set :=
+    TraitMethod.C (trait Self T) "as_ref" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+        Run.Trait method [] [] [ φ self ] (Ref.t Pointer.Kind.Ref T)
+    ).
+
+  Class Run (Self : Set) (T : Set) `{Link Self} `{Link T} : Set := {
+    as_ref : Run_as_ref Self T;
+  }.
+End AsRef.
+
+(* impl<T> AsRef<[T]> for [T] *)
+Module Impl_AsRef_for_Slice.
+  Definition run_as_ref
+    (T : Set) `{Link T} :
+    AsRef.Run_as_ref (list T) (list T).
+  Proof.
+    eexists.
+    { eapply IsTraitMethod.Defined.
+      { apply convert.Impl_core_convert_AsRef_slice_T_for_slice_T.Implements. }
+      { reflexivity. }
+    }
+    { constructor.
+      run_symbolic.
+    }
+  Defined.
+
+  Instance run
+    (T : Set) `{Link T} :
+    AsRef.Run (list T) (list T) :=
+  {
+    AsRef.as_ref := run_as_ref T;
+  }.
+End Impl_AsRef_for_Slice.
+
+(*
+pub trait TryFrom<T>: Sized {
+    type Error;
+    fn try_from(value: T) -> Result<Self, Self::Error>;
+}
+*)
+Module TryFrom.
+  Definition trait (Self T : Set) `{Link Self} `{Link T} : TraitMethod.Header.t :=
+    ("core::convert::TryFrom", [], [Φ T], Φ Self).
+
+  Definition Run_try_from (Self T Error : Set) `{Link Self} `{Link T} `{Link Error} : Set :=
+    TraitMethod.C (trait Self T) "try_from" (fun method =>
+      forall (value : T),
+        Run.Trait method [] [] [ φ value ] (Result.t Self Error)
+    ).
+
+  Class Run (Self : Set) (T : Set) (Error : Set) `{Link Self} `{Link T} `{Link Error} : Set := {
+    try_from : Run_try_from Self T Error;
+  }.
+End TryFrom.
diff --git a/CoqOfRust/core/convert/links/num.v b/CoqOfRust/core/convert/links/num.v
new file mode 100644
index 000000000..3ac76fed6
--- /dev/null
+++ b/CoqOfRust/core/convert/links/num.v
@@ -0,0 +1,29 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import links.M.
+Require Import core.convert.links.mod.
+Require Import core.convert.num.
+Require Import core.links.result.
+Require Import core.num.links.error.
+
+Module Impl_TryFrom_u64_for_usize.
+  Definition Self : Set :=
+    Usize.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_usize.Implements. }
+      { reflexivity. }
+    }
+    { constructor.
+      run_symbolic.
+      instantiate (1 := Result.Ok _).
+      with_strategy transparent [φ] reflexivity.
+    }
+  Defined.
+
+  Instance run : TryFrom.Run Self U64.t TryFromIntError.t := {
+    TryFrom.try_from := run_try_from;
+  }.
+End Impl_TryFrom_u64_for_usize.
diff --git a/CoqOfRust/core/links/result.v b/CoqOfRust/core/links/result.v
index 2bde86d68..64d8d34d1 100644
--- a/CoqOfRust/core/links/result.v
+++ b/CoqOfRust/core/links/result.v
@@ -1,6 +1,6 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
-
+Require Import core.result.
 Module Result.
   Inductive t {T E : Set} : Set :=
   | Ok : T -> t
@@ -26,3 +26,21 @@ Module Result.
   Defined.
   Smpl Add apply of_ty : of_ty.
 End Result.
+
+Module Impl_Result_T_E.
+  Definition Self (T E : Set) : Set :=
+    Result.t T E.
+
+  (* pub fn unwrap_or(self, default: T) -> T *)
+  Instance run_unwrap_or
+    (T E : Set) `{Link T} `{Link E}
+    (self : Self T E)
+    (default : T) :
+    Run.Trait
+      (result.Impl_core_result_Result_T_E.unwrap_or (Φ T) (Φ E)) [] [] [ φ self; φ default ]
+      T.
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+End Impl_Result_T_E.
diff --git a/CoqOfRust/core/num/links/error.v b/CoqOfRust/core/num/links/error.v
new file mode 100644
index 000000000..c656a6d6e
--- /dev/null
+++ b/CoqOfRust/core/num/links/error.v
@@ -0,0 +1,19 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import links.M.
+Require Import core.num.error.
+
+(* pub struct TryFromIntError(/* private fields */); *)
+Module TryFromIntError.
+  Parameter t : Set.
+
+  Parameter to_value : t -> Value.t.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "core::num::error::TryFromIntError";
+    φ := to_value;
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "core::num::error::TryFromIntError").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add apply of_ty : of_ty.
+End TryFromIntError.
diff --git a/CoqOfRust/core/num/links/mod.v b/CoqOfRust/core/num/links/mod.v
index 956761483..d565e30f6 100644
--- a/CoqOfRust/core/num/links/mod.v
+++ b/CoqOfRust/core/num/links/mod.v
@@ -6,6 +6,22 @@ Require Import core.num.mod.
 Module Impl_u64.
   Definition Self : Set := U64.t.
 
+  (* pub const MIN: Self *)
+  Instance run_min :
+    Run.Trait num.Impl_u64.value_MIN [] [] [] (Ref.t Pointer.Kind.Raw Self).
+  Proof.
+    constructor.
+    run_symbolic.
+  Defined.
+
+  (* pub const MAX: Self *)
+  Instance run_max :
+    Run.Trait num.Impl_u64.value_MAX [] [] [] (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_u64.saturating_add [] [] [ φ self; φ rhs ] Self.
diff --git a/CoqOfRust/lib/lib.v b/CoqOfRust/lib/lib.v
index 3e638b444..ecbf088db 100644
--- a/CoqOfRust/lib/lib.v
+++ b/CoqOfRust/lib/lib.v
@@ -246,14 +246,31 @@ Module BinOp.
     Definition shr : Value.t :=
       make_arithmetic Z.shiftr.
 
+    Definition make_bool_or_arithmetic
+      (bin_op_bool : bool -> bool -> bool)
+      (bin_op_Z : Z -> Z -> Z)
+      : Value.t :=
+      M.closure (fun args =>
+        match args with
+        | [Value.Bool b1; Value.Bool b2] => M.pure (Value.Bool (bin_op_bool b1 b2))
+        | [Value.Integer kind1 v1; Value.Integer kind2 v2] =>
+          if negb (IntegerKind.eqb kind1 kind2) then
+            M.impossible "expected the same kind of integers"
+          else
+            let z := bin_op_Z v1 v2 in
+            M.pure (Value.Integer kind1 (Integer.normalize_wrap kind1 z))
+        | _ => M.impossible "expected two values for bool or arithmetic"
+        end
+      ).
+
     Definition bit_xor : Value.t :=
-      make_arithmetic Z.lxor.
+      make_bool_or_arithmetic xorb Z.lxor.
 
     Definition bit_and : Value.t :=
-      make_arithmetic Z.land.
+      make_bool_or_arithmetic andb Z.land.
 
     Definition bit_or : Value.t :=
-      make_arithmetic Z.lor.
+      make_bool_or_arithmetic orb Z.lor.
   End Wrap.
 End BinOp.
 
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 c13bafe32..e01a1f101 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md
@@ -117,16 +117,16 @@
 ## System
 
 - [ ] `keccak256`
-- [ ] `address`
-- [ ] `caller`
-- [ ] `codesize`
-- [ ] `codecopy`
+- [x] `address`
+- [x] `caller`
+- [x] `codesize`
+- [x] `memory_resize`
+- [x] `codecopy`
 - [ ] `calldataload`
 - [x] `calldatasize`
 - [x] `callvalue`
-- [ ] `memory_resize`
-- [ ] `calldatacopy`
-- [ ] `returndatasize`
+- [x] `calldatacopy`
+- [x] `returndatasize`
 - [ ] `returndatacopy`
 - [ ] `returndataload`
 - [x] `gas`
@@ -144,6 +144,6 @@
 ## Summary
 
 - Total: 103
-- Admitted: 75
-- Defined: 28
-- Percentage: 27.18%
+- Admitted: 68
+- Defined: 35
+- Percentage: 33.98%
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/system.v b/CoqOfRust/revm/revm_interpreter/instructions/links/system.v
index dd340e8b7..91bd42832 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/system.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/system.v
@@ -1,9 +1,13 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import alloy_primitives.links.aliases.
+Require Import alloy_primitives.bits.links.address.
 Require Import alloy_primitives.bits.links.fixed.
 Require Import alloy_primitives.utils.links.mod.
+Require Import core.convert.links.mod.
+Require Import core.convert.links.num.
 Require Import core.links.cmp.
+Require Import core.links.result.
 Require Import core.num.links.mod.
 Require Import core.slice.links.mod.
 Require Import revm.revm_interpreter.gas.links.calc.
@@ -14,12 +18,19 @@ 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_primitives.links.lib.
+Require Import revm.revm_specification.links.hardfork.
 Require Import ruint.links.from.
 
-Import Impl_Slice.
+Import Impl_Address.
+
+Import Impl_FixedBytes.
 Import Impl_Gas.
+Import Impl_Result_T_E.
+Import Impl_Slice.
+Import Impl_SpecId.
 Import from.Impl_Uint.
 Import lib.Impl_Uint.
+Import Impl_u64.
 Import Impl_usize.
 
 (*
@@ -43,6 +54,8 @@ Proof.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_MemoryTrait_for_Memory.
+  destruct (Impl_Into_for_From_T.run Impl_From_FixedBytes_32_for_U256.run).
+  destruct (Impl_AsRef_for_Slice.run U8.t).
   run_symbolic.
 Admitted.
 
@@ -66,8 +79,10 @@ Proof.
   InterpreterTypes.destruct_run.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
+  destruct run_InputsTrait_for_Input.
+  destruct (Impl_Into_for_From_T.run Impl_From_FixedBytes_32_for_U256.run).
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn caller<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -86,8 +101,13 @@ Instance run_caller
     unit.
 Proof.
   constructor.
+  InterpreterTypes.destruct_run.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_InputsTrait_for_Input.
+  destruct (Impl_Into_for_From_T.run Impl_From_FixedBytes_32_for_U256.run).
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn codesize<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -106,8 +126,37 @@ Instance run_codesize
     unit.
 Proof.
   constructor.
+  InterpreterTypes.destruct_run.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_LegacyBytecode_for_Bytecode.
   run_symbolic.
-Admitted.
+Defined.
+
+(*
+pub fn memory_resize(
+    interpreter: &mut Interpreter<impl InterpreterTypes>,
+    memory_offset: U256,
+    len: usize,
+) -> Option<usize>
+*)
+Instance run_memory_resize
+  {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))
+  (memory_offset : aliases.U256.t)
+  (len : Usize.t) :
+  Run.Trait
+    instructions.system.memory_resize [] [ Φ WIRE ] [ φ interpreter; φ memory_offset; φ len ]
+    (option Usize.t).
+Proof.
+  constructor.
+  InterpreterTypes.destruct_run.
+  destruct run_LoopControl_for_Control.
+  destruct run_MemoryTrait_for_Memory.
+  run_symbolic.
+Defined.
 
 (*
 pub fn codecopy<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -126,8 +175,14 @@ Instance run_codecopy
     unit.
 Proof.
   constructor.
+  InterpreterTypes.destruct_run.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_MemoryTrait_for_Memory.
+  destruct run_LegacyBytecode_for_Bytecode.
+  destruct Impl_TryFrom_u64_for_usize.run.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn calldataload<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -146,6 +201,11 @@ Instance run_calldataload
     unit.
 Proof.
   constructor.
+  InterpreterTypes.destruct_run.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_InputsTrait_for_Input.
+  destruct Impl_TryFrom_u64_for_usize.run.
   run_symbolic.
 Admitted.
 
@@ -197,30 +257,6 @@ Proof.
   run_symbolic.
 Defined.
 
-(*
-pub fn memory_resize(
-    interpreter: &mut Interpreter<impl InterpreterTypes>,
-    memory_offset: U256,
-    len: usize,
-) -> Option<usize>
-*)
-Instance run_memory_resize
-  {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))
-  (memory_offset : aliases.U256.t)
-  (len : Usize.t) :
-  Run.Trait
-    instructions.system.memory_resize [] [ Φ WIRE ] [ φ interpreter; φ memory_offset; φ len ]
-    (option Usize.t).
-Proof.
-  constructor.
-  destruct run_InterpreterTypes_for_WIRE.
-  destruct run_LoopControl_for_Control.
-  run_symbolic.
-Admitted.
-
 (*
 pub fn calldatacopy<WIRE: InterpreterTypes, H: Host + ?Sized>(
     interpreter: &mut Interpreter<WIRE>,
@@ -239,8 +275,13 @@ Instance run_calldatacopy
 Proof.
   constructor.
   InterpreterTypes.destruct_run.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_MemoryTrait_for_Memory.
+  destruct run_InputsTrait_for_Input.
+  destruct Impl_TryFrom_u64_for_usize.run.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn returndatasize<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -259,8 +300,13 @@ Instance run_returndatasize
     unit.
 Proof.
   constructor.
+  InterpreterTypes.destruct_run.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_RuntimeFlag_for_RuntimeFlag.
+  destruct run_ReturnData_for_ReturnData.
   run_symbolic.
-Admitted.
+Defined.
 
 (*
 pub fn returndatacopy<WIRE: InterpreterTypes, H: Host + ?Sized>(
@@ -279,6 +325,13 @@ Instance run_returndatacopy
     unit.
 Proof.
   constructor.
+  InterpreterTypes.destruct_run.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_RuntimeFlag_for_RuntimeFlag.
+  destruct run_ReturnData_for_ReturnData.
+  destruct run_MemoryTrait_for_Memory.
+  destruct Impl_TryFrom_u64_for_usize.run.
   run_symbolic.
 Admitted.
 
@@ -304,6 +357,7 @@ Proof.
   destruct run_LoopControl_for_Control.
   destruct run_RuntimeFlag_for_RuntimeFlag.
   destruct run_ReturnData_for_ReturnData.
+  destruct Impl_TryFrom_u64_for_usize.run.
   run_symbolic.
 Admitted.
 
diff --git a/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v b/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v
index bf831e63d..31ccb388f 100644
--- a/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v
+++ b/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v
@@ -782,6 +782,9 @@ Module InterpreterTypes.
       reflexivity
     |];
     match goal with
-    | H : Run _ _ |- _ => destruct H
+    | H : Run _ _ |- _ =>
+      (* We make a duplicate for future calls *)
+      pose H;
+      destruct H
     end.
 End InterpreterTypes.