diff --git a/CoqOfRust/core/intrinsics/links/mod.v b/CoqOfRust/core/intrinsics/links/mod.v
index 8862049b1..f77d65e09 100644
--- a/CoqOfRust/core/intrinsics/links/mod.v
+++ b/CoqOfRust/core/intrinsics/links/mod.v
@@ -24,9 +24,26 @@ Instance run_saturating_sub (integer_kind : IntegerKind.t) (x y : Integer.t inte
 Proof.
 Admitted.
 
+Instance run_sub_with_overflow
+  (x y : Integer.t IntegerKind.U64) :
+  Run.Trait
+    intrinsics.sub_with_overflow
+    []
+    [ Φ (Integer.t IntegerKind.U64) ]
+    [ φ x; φ y ]
+    (Integer.t IntegerKind.U64 * bool).
+Proof.
+Admitted.
+
 (* pub const unsafe fn transmute<Src, Dst>(_src: Src) -> Dst *)
 Instance run_transmute (Src Dst : Set) `{Link Src} `{Link Dst} (src : Src) :
   Run.Trait
     intrinsics.transmute [] [ Φ Src; Φ Dst ] [ φ src ] Dst.
 Proof.
 Admitted.
+
+Instance run_discriminant_value (ref : Ref.t Pointer.Kind.Ref Ordering.t) :
+  Run.Trait intrinsics.discriminant_value [] [Φ Ordering.t] [φ ref]
+             (Integer.t IntegerKind.I8).
+Proof.
+Admitted.
diff --git a/CoqOfRust/core/links/cmp.v b/CoqOfRust/core/links/cmp.v
index 6cb830745..cb2091a41 100644
--- a/CoqOfRust/core/links/cmp.v
+++ b/CoqOfRust/core/links/cmp.v
@@ -267,3 +267,11 @@ Module PartialOrd.
     ge : Run_ge Self Rhs;
   }.
 End PartialOrd.
+
+Module Impl_PartialEq_for_Ordering.
+  Definition Self : Set := Ordering.t.
+
+  Instance run : PartialEq.Run Self Self.
+  Admitted.
+End Impl_PartialEq_for_Ordering.
+Export Impl_PartialEq_for_Ordering.
diff --git a/CoqOfRust/revm/revm_context_interface/links/host.v b/CoqOfRust/revm/revm_context_interface/links/host.v
index a5c06d94c..bc8e4dc84 100644
--- a/CoqOfRust/revm/revm_context_interface/links/host.v
+++ b/CoqOfRust/revm/revm_context_interface/links/host.v
@@ -241,20 +241,4 @@ 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_interpreter/instructions/links/bitwise.v b/CoqOfRust/revm/revm_interpreter/instructions/links/bitwise.v
new file mode 100644
index 000000000..e284307bf
--- /dev/null
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/bitwise.v
@@ -0,0 +1,262 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import core.convert.links.num.
+Require Import core.links.cmp.
+Require Import core.links.result.
+Require Import core.num.links.error.
+Require Import core.num.links.mod.
+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.i256.
+Require Import revm.revm_interpreter.instructions.bitwise.
+Require Import revm.revm_specification.links.hardfork.
+Require Import ruint.links.bits.
+Require Import ruint.links.cmp.
+Require Import ruint.links.from.
+Require Import ruint.links.lib.
+
+(*
+pub fn lt<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    _host: &mut H,
+)
+*)
+Instance run_lt
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.lt [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_LoopControl_for_Control.
+  destruct run_StackTrait_for_Stack.
+  destruct (Impl_PartialOrd_for_Uint.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
+  run_symbolic.
+Defined.
+
+Instance run_gt
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.gt [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_LoopControl_for_Control.
+  destruct run_StackTrait_for_Stack.
+  destruct (Impl_PartialOrd_for_Uint.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
+  run_symbolic.
+Defined.
+
+Instance run_slt
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.slt [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_LoopControl_for_Control.
+  destruct run_StackTrait_for_Stack.
+  destruct Impl_PartialEq_for_Ordering.run.
+  run_symbolic.
+Defined.
+
+Instance run_sgt
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.sgt [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_LoopControl_for_Control.
+  destruct run_StackTrait_for_Stack.
+  destruct Impl_PartialEq_for_Ordering.run.
+  run_symbolic.
+Defined.
+
+Instance run_bitwise_eq
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.eq [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct (Impl_PartialEq_for_Uint.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
+  run_symbolic.
+Defined.
+
+Instance run_bitwise_is_zero
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.iszero [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  run_symbolic.
+Defined.
+
+Instance run_bitwise_bitand
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.bitand [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct (Impl_BitAnd_for_Uint.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
+  run_symbolic.
+Defined.
+
+Instance run_bitwise_bitor
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.bitor [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct (Impl_BitOr_for_Uint.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
+  run_symbolic.
+Defined.
+
+Instance run_bitwise_bitxor
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.bitxor [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct (Impl_BitXor_for_Uint.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
+  run_symbolic.
+Defined.
+
+Instance run_bitwise_not
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.not [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct (Impl_Not_for_Uint.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
+  run_symbolic.
+Defined.
+
+Instance run_bitwise_sar
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.sar [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_RuntimeFlag_for_RuntimeFlag.
+  destruct Impl_TryFrom_u64_for_usize.run.
+  run_symbolic.
+Defined.
+
+Instance run_bitwise_shl
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.shl [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_RuntimeFlag_for_RuntimeFlag.
+  destruct Impl_TryFrom_u64_for_usize.run.
+  destruct (Impl_Shl_for_Uint.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
+  run_symbolic.
+Defined.
+
+Instance run_bitwise_shr
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.shr [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct run_LoopControl_for_Control.
+  destruct run_RuntimeFlag_for_RuntimeFlag.
+  destruct Impl_TryFrom_u64_for_usize.run.
+  destruct (Impl_Shr_for_Uint.run {| Integer.value := 256 |} {| Integer.value := 4 |}).
+  run_symbolic.
+Defined.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v
index f284a9000..988d0b4a8 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v
@@ -68,6 +68,7 @@ Module Sign.
     apply of_value_with_Zero.
   Defined.
   Smpl Add apply of_value_Zero : of_value.
+
   Definition of_value_Plus :
     OfValue.t (Value.StructTuple "revm_interpreter::instructions::i256::Sign::Plus" []).
   Proof.
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 fc0f622cb..491e40e04 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md
@@ -16,6 +16,22 @@
 - [x] `exp`
 - [x] `signextend`
 
+## Bitwise
+
+- [x] `lt`
+- [x] `gt`
+- [x] `slt`
+- [x] `sgt`
+- [x] `bitwise_eq`
+- [x] `bitwise_is_zero`
+- [x] `bitwise_bitand`
+- [x] `bitwise_bitor`
+- [x] `bitwise_bitxor`
+- [x] `bitwise_not`
+- [x] `bitwise_sar`
+- [x] `bitwise_shl`
+- [x] `bitwise_shr`
+
 ## Block_info
 
 - [x] `chainid`
@@ -147,7 +163,7 @@
 
 ## Summary
 
-- Total: 107
+- Total: 120
 - Admitted: 37
-- Defined: 70
-- Percentage: 65.42%
+- Defined: 83
+- Percentage: 69.17%
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/stack.v b/CoqOfRust/revm/revm_interpreter/instructions/links/stack.v
index e255fd111..bd94d687a 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/stack.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/stack.v
@@ -28,7 +28,7 @@ Instance run_pop
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
   run_symbolic.
@@ -51,7 +51,7 @@ Instance run_push0
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
   destruct run_RuntimeFlag_for_RuntimeFlag.
@@ -76,7 +76,7 @@ Instance run_push
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
   destruct run_Jumps_for_Bytecode.
@@ -102,7 +102,7 @@ Instance run_dup
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
   run_symbolic.
@@ -126,7 +126,7 @@ Instance run_swap
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
   run_symbolic.
@@ -149,7 +149,7 @@ Instance run_dupn
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
   destruct run_RuntimeFlag_for_RuntimeFlag.
@@ -175,7 +175,7 @@ Instance run_swapn
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
   destruct run_RuntimeFlag_for_RuntimeFlag.
@@ -201,7 +201,7 @@ Instance run_exchange
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_LoopControl_for_Control.
   destruct run_StackTrait_for_Stack.
   destruct run_RuntimeFlag_for_RuntimeFlag.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/system.v b/CoqOfRust/revm/revm_interpreter/instructions/links/system.v
index 6190f937e..3016a774a 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/system.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/system.v
@@ -39,7 +39,7 @@ Instance run_keccak256
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_MemoryTrait_for_Memory.
@@ -65,7 +65,7 @@ Instance run_address
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_InputsTrait_for_Input.
@@ -90,7 +90,7 @@ Instance run_caller
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_InputsTrait_for_Input.
@@ -107,7 +107,7 @@ pub fn codesize<WIRE: InterpreterTypes, H: Host + ?Sized>(
 Instance run_codesize
   {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)
+  {run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types}
   (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
   (_host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
@@ -115,7 +115,7 @@ Instance run_codesize
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_LegacyBytecode_for_Bytecode.
@@ -132,7 +132,7 @@ pub fn memory_resize(
 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)
+  {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) :
@@ -141,7 +141,7 @@ Instance run_memory_resize
     (option Usize.t).
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_LoopControl_for_Control.
   destruct run_MemoryTrait_for_Memory.
   run_symbolic.
@@ -164,7 +164,7 @@ Instance run_codecopy
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE eqn:?.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_MemoryTrait_for_Memory.
@@ -190,7 +190,7 @@ Instance run_calldataload
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_InputsTrait_for_Input.
@@ -215,7 +215,7 @@ Instance run_calldatasize
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_InputsTrait_for_Input.
@@ -239,7 +239,7 @@ Instance run_callvalue
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_InputsTrait_for_Input.
@@ -263,7 +263,7 @@ Instance run_calldatacopy
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE eqn:?.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_MemoryTrait_for_Memory.
@@ -289,7 +289,7 @@ Instance run_returndatasize
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_RuntimeFlag_for_RuntimeFlag.
@@ -314,7 +314,7 @@ Instance run_returndatacopy
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_RuntimeFlag_for_RuntimeFlag.
@@ -341,7 +341,7 @@ Instance run_returndataload
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   destruct run_RuntimeFlag_for_RuntimeFlag.
@@ -367,7 +367,7 @@ Instance run_gas
     unit.
 Proof.
   constructor.
-  InterpreterTypes.destruct_run.
+  destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack.
   destruct run_LoopControl_for_Control.
   run_symbolic.
diff --git a/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v b/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v
index 31ccb388f..3508ca57b 100644
--- a/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v
+++ b/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v
@@ -771,20 +771,4 @@ Module InterpreterTypes.
         "RuntimeFlag" (Φ types.(Types.RuntimeFlag));
     run_RuntimeFlag_for_RuntimeFlag : RuntimeFlag.Run types.(Types.RuntimeFlag);
   }.
-
-  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 InterpreterTypes.
diff --git a/CoqOfRust/ruint/links/bits.v b/CoqOfRust/ruint/links/bits.v
index 3b5599495..2f08e1752 100644
--- a/CoqOfRust/ruint/links/bits.v
+++ b/CoqOfRust/ruint/links/bits.v
@@ -27,6 +27,16 @@ Module Impl_Uint.
       (bits.Impl_ruint_Uint_BITS_LIMBS.byte (φ BITS) (φ LIMBS)) [] [] [ φ x; φ index ]
       U8.t.
   Admitted.
+
+  (* pub fn arithmetic_shr(self, rhs: usize) -> Self *)
+  Instance run_arithmetic_shr
+    (BITS LIMBS : Usize.t)
+    (self : Self BITS LIMBS)
+    (rhs : Usize.t) :
+    Run.Trait
+      (bits.Impl_ruint_Uint_BITS_LIMBS.arithmetic_shr (φ BITS) (φ LIMBS)) [] [] [ φ self; φ rhs ]
+      (Self BITS LIMBS).
+  Admitted.
 End Impl_Uint.
 Export Impl_Uint.
 
diff --git a/CoqOfRust/ruint/links/cmp.v b/CoqOfRust/ruint/links/cmp.v
index 86eda1359..77fe1916f 100644
--- a/CoqOfRust/ruint/links/cmp.v
+++ b/CoqOfRust/ruint/links/cmp.v
@@ -28,3 +28,4 @@ Module Impl_PartialOrd_for_Uint.
   Instance run (BITS LIMBS : Usize.t) : PartialOrd.Run (Self BITS LIMBS) (Self BITS LIMBS).
   Admitted.
 End Impl_PartialOrd_for_Uint.
+Export Impl_PartialOrd_for_Uint.
diff --git a/CoqOfRust/ruint/links/lib.v b/CoqOfRust/ruint/links/lib.v
index 5af5c499c..3bddb3fcc 100644
--- a/CoqOfRust/ruint/links/lib.v
+++ b/CoqOfRust/ruint/links/lib.v
@@ -85,6 +85,26 @@ Module Impl_Uint.
     apply Run.run_f.
   Defined.
 
+  (* pub const MIN: Self *)
+  Instance run_MIN (BITS LIMBS : Usize.t) :
+    Run.Trait
+      (Impl_ruint_Uint_BITS_LIMBS.value_MIN (φ BITS) (φ LIMBS)) [] [] []
+      (Ref.t Pointer.Kind.Raw (Self BITS LIMBS)).
+  Proof.
+    constructor.
+    run_symbolic.
+  Defined.
+
+  (* pub const MAX: Self *)
+  Instance run_MAX (BITS LIMBS : Usize.t) :
+    Run.Trait
+      (Impl_ruint_Uint_BITS_LIMBS.value_MAX (φ BITS) (φ LIMBS)) [] [] []
+      (Ref.t Pointer.Kind.Raw (Self BITS LIMBS)).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
   (* pub const fn as_limbs(&self) -> &[u64; LIMBS] *)
   Instance run_as_limbs
     (BITS LIMBS : Usize.t)