diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
index 587dafe60..5fb87a691 100644
--- a/.github/workflows/rust.yml
+++ b/.github/workflows/rust.yml
@@ -156,7 +156,7 @@ jobs:
           endGroup
           startGroup "Translate alloy-core"
             cd third-party/alloy-rs-core/crates/primitives
-            cp ../../rust-toolchain ./
+            cp ../../../../rust-toolchain ./
             cargo coq-of-rust
             touch src/lib.rs
             cargo coq-of-rust
diff --git a/CoqOfRust/alloy_primitives/bits/links/address.v b/CoqOfRust/alloy_primitives/bits/links/address.v
new file mode 100644
index 000000000..dc5f60d00
--- /dev/null
+++ b/CoqOfRust/alloy_primitives/bits/links/address.v
@@ -0,0 +1,39 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.bits.links.fixed.
+Require Import alloy_primitives.bits.address.
+
+Module Address.
+  Parameter t : Set.
+
+  Parameter to_value : t -> Value.t.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "alloy_primitives::bits::address::Address";
+    φ := to_value;
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "alloy_primitives::bits::address::Address").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add apply of_ty : of_ty.
+End Address.
+
+(* impl Address { *)
+Module Impl_Address.
+  Definition Self : Set :=
+    Address.t.
+
+  (* pub fn from_word(word: FixedBytes<32>) -> Self *)
+  Instance run_from_word (word : fixed.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) :
+    Run.Trait
+      bits.address.Impl_alloy_primitives_bits_address_Address.into_word [] [] [ φ self ]
+      (fixed.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
new file mode 100644
index 000000000..6d55af5a5
--- /dev/null
+++ b/CoqOfRust/alloy_primitives/bits/links/fixed.v
@@ -0,0 +1,23 @@
+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; subst.
+    eapply OfTy.Make with (A := t N); reflexivity.
+  Defined.
+  Smpl Add eapply of_ty : of_ty.
+End FixedBytes.
diff --git a/CoqOfRust/alloy_primitives/bytes/links/mod.v b/CoqOfRust/alloy_primitives/bytes/links/mod.v
new file mode 100644
index 000000000..1d6a998ca
--- /dev/null
+++ b/CoqOfRust/alloy_primitives/bytes/links/mod.v
@@ -0,0 +1,79 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.bytes.mod.
+Require Import core.links.clone.
+Require Import core.links.default.
+
+(* pub struct Bytes(pub bytes::Bytes); *)
+Module Bytes.
+  Parameter t : Set.
+
+  Parameter to_value : t -> Value.t.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "alloy_primitives::bytes_::Bytes";
+    φ := to_value;
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "alloy_primitives::bytes_::Bytes").
+  Proof.
+    eapply OfTy.Make with (A := t); reflexivity.
+  Defined.
+  Smpl Add apply of_ty : of_ty.
+End Bytes.
+
+Module Impl_Clone_for_Bytes.
+  Definition Self : Set :=
+    Bytes.t.
+
+  Definition run_clone : Clone.Run_clone Self.
+  Proof.
+    eexists.
+    { eapply IsTraitMethod.Defined.
+      { apply bytes_.Impl_core_clone_Clone_for_alloy_primitives_bytes__Bytes.Implements. }
+      { reflexivity. }
+    }
+    { constructor.
+      run_symbolic.
+      admit.
+    }
+  Admitted.
+
+  Instance run : Clone.Run Self := {
+    Clone.clone := run_clone;
+  }.
+End Impl_Clone_for_Bytes.
+
+Module Impl_Default_for_Bytes.
+  Definition Self : Set :=
+    Bytes.t.
+
+  Definition run_default : Default.Run_default Self.
+  Proof.
+    eexists.
+    { eapply IsTraitMethod.Defined.
+      { apply bytes_.Impl_core_default_Default_for_alloy_primitives_bytes__Bytes.Implements. }
+      { reflexivity. }
+    }
+    { constructor.
+      run_symbolic.
+      admit.
+    }
+  Admitted.
+
+  Instance run : Default.Run Self := {
+    Default.default := run_default;
+  }.
+End Impl_Default_for_Bytes.
+
+Module Impl_Bytes.
+  Definition Self : Set :=
+    Bytes.t.
+
+  (* pub const fn new() -> Self *)
+  Instance run_new : Run.Trait bytes_.Impl_alloy_primitives_bytes__Bytes.new [] [] [] Self.
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+End Impl_Bytes.
diff --git a/CoqOfRust/alloy_primitives/links/aliases.v b/CoqOfRust/alloy_primitives/links/aliases.v
new file mode 100644
index 000000000..76a642b4f
--- /dev/null
+++ b/CoqOfRust/alloy_primitives/links/aliases.v
@@ -0,0 +1,473 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.bits.links.fixed.
+Require Import alloy_primitives.signed.links.int.
+Require Import ruint.links.lib.
+
+(** We define the aliases for convenience. They are actually expanded in the translation
+    from Rust.
+
+    We wrap everything in a module to avoid name clashes.
+*)
+
+Module aliases.
+  Module I0.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 0 |} {| Integer.value := 0 |}.
+  End I0.
+
+  Module I1.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 1 |} {| Integer.value := 1 |}.
+  End I1.
+
+  Module U8.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 8 |} {| Integer.value := 1 |}.
+  End U8.
+
+  Module I8.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 8 |} {| Integer.value := 1 |}.
+  End I8.
+
+  Module U16.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 16 |} {| Integer.value := 1 |}.
+  End U16.
+
+  Module I16.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 16 |} {| Integer.value := 1 |}.
+  End I16.
+
+  Module U24.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 24 |} {| Integer.value := 1 |}.
+  End U24.
+
+  Module I24.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 24 |} {| Integer.value := 1 |}.
+  End I24.
+
+  Module U32.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 32 |} {| Integer.value := 1 |}.
+  End U32.
+
+  Module I32.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 32 |} {| Integer.value := 1 |}.
+  End I32.
+
+  Module U40.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 40 |} {| Integer.value := 1 |}.
+  End U40.
+
+  Module I40.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 40 |} {| Integer.value := 1 |}.
+  End I40.
+
+  Module U48.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 48 |} {| Integer.value := 1 |}.
+  End U48.
+
+  Module I48.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 48 |} {| Integer.value := 1 |}.
+  End I48.
+
+  Module U56.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 56 |} {| Integer.value := 1 |}.
+  End U56.
+
+  Module I56.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 56 |} {| Integer.value := 1 |}.
+  End I56.
+
+  Module U64.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 64 |} {| Integer.value := 1 |}.
+  End U64.
+
+  Module I64.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 64 |} {| Integer.value := 1 |}.
+  End I64.
+
+  Module U72.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 72 |} {| Integer.value := 2 |}.
+  End U72.
+
+  Module I72.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 72 |} {| Integer.value := 2 |}.
+  End I72.
+
+  Module U80.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 80 |} {| Integer.value := 2 |}.
+  End U80.
+
+  Module I80.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 80 |} {| Integer.value := 2 |}.
+  End I80.
+
+  Module U88.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 88 |} {| Integer.value := 2 |}.
+  End U88.
+
+  Module I88.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 88 |} {| Integer.value := 2 |}.
+  End I88.
+
+  Module U96.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 96 |} {| Integer.value := 2 |}.
+  End U96.
+
+  Module I96.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 96 |} {| Integer.value := 2 |}.
+  End I96.
+
+  Module U104.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 104 |} {| Integer.value := 2 |}.
+  End U104.
+
+  Module I104.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 104 |} {| Integer.value := 2 |}.
+  End I104.
+
+  Module U112.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 112 |} {| Integer.value := 2 |}.
+  End U112.
+
+  Module I112.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 112 |} {| Integer.value := 2 |}.
+  End I112.
+
+  Module U120.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 120 |} {| Integer.value := 2 |}.
+  End U120.
+
+  Module I120.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 120 |} {| Integer.value := 2 |}.
+  End I120.
+
+  Module U128.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 128 |} {| Integer.value := 2 |}.
+  End U128.
+
+  Module I128.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 128 |} {| Integer.value := 2 |}.
+  End I128.
+
+  Module U136.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 136 |} {| Integer.value := 3 |}.
+  End U136.
+
+  Module I136.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 136 |} {| Integer.value := 3 |}.
+  End I136.
+
+  Module U144.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 144 |} {| Integer.value := 3 |}.
+  End U144.
+
+  Module I144.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 144 |} {| Integer.value := 3 |}.
+  End I144.
+
+  Module U152.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 152 |} {| Integer.value := 3 |}.
+  End U152.
+
+  Module I152.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 152 |} {| Integer.value := 3 |}.
+  End I152.
+
+  Module U160.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 160 |} {| Integer.value := 3 |}.
+  End U160.
+
+  Module I160.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 160 |} {| Integer.value := 3 |}.
+  End I160.
+
+  Module U168.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 168 |} {| Integer.value := 3 |}.
+  End U168.
+
+  Module I168.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 168 |} {| Integer.value := 3 |}.
+  End I168.
+
+  Module U176.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 176 |} {| Integer.value := 3 |}.
+  End U176.
+
+  Module I176.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 176 |} {| Integer.value := 3 |}.
+  End I176.
+
+  Module U184.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 184 |} {| Integer.value := 3 |}.
+  End U184.
+
+  Module I184.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 184 |} {| Integer.value := 3 |}.
+  End I184.
+
+  Module U192.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 192 |} {| Integer.value := 3 |}.
+  End U192.
+
+  Module I192.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 192 |} {| Integer.value := 3 |}.
+  End I192.
+
+  Module U200.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 200 |} {| Integer.value := 4 |}.
+  End U200.
+
+  Module I200.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 200 |} {| Integer.value := 4 |}.
+  End I200.
+
+  Module U208.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 208 |} {| Integer.value := 4 |}.
+  End U208.
+
+  Module I208.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 208 |} {| Integer.value := 4 |}.
+  End I208.
+
+  Module U216.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 216 |} {| Integer.value := 4 |}.
+  End U216.
+
+  Module I216.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 216 |} {| Integer.value := 4 |}.
+  End I216.
+
+  Module U224.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 224 |} {| Integer.value := 4 |}.
+  End U224.
+
+  Module I224.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 224 |} {| Integer.value := 4 |}.
+  End I224.
+
+  Module U232.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 232 |} {| Integer.value := 4 |}.
+  End U232.
+
+  Module I232.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 232 |} {| Integer.value := 4 |}.
+  End I232.
+
+  Module U240.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 240 |} {| Integer.value := 4 |}.
+  End U240.
+
+  Module I240.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 240 |} {| Integer.value := 4 |}.
+  End I240.
+
+  Module U248.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 248 |} {| Integer.value := 4 |}.
+  End U248.
+
+  Module I248.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 248 |} {| Integer.value := 4 |}.
+  End I248.
+
+  Module U256.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}.
+  End U256.
+
+  Module I256.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 256 |} {| Integer.value := 4 |}.
+  End I256.
+
+  Module U512.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 512 |} {| Integer.value := 8 |}.
+  End U512.
+
+  Module I512.
+    Definition t : Set :=
+      Signed.t {| Integer.value := 512 |} {| Integer.value := 8 |}.
+  End I512.
+
+  Module B8.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 1 |}.
+  End B8.
+
+  Module B16.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 2 |}.
+  End B16.
+
+  Module B32.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 4 |}.
+  End B32.
+
+  Module B64.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 8 |}.
+  End B64.
+
+  Module B96.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 12 |}.
+  End B96.
+
+  Module B128.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 16 |}.
+  End B128.
+
+  Module B160.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 20 |}.
+  End B160.
+
+  Module B192.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 24 |}.
+  End B192.
+
+  Module B224.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 28 |}.
+  End B224.
+
+  Module B256.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 32 |}.
+  End B256.
+
+  Module B512.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 64 |}.
+  End B512.
+
+  Module B1024.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 128 |}.
+  End B1024.
+
+  Module B2048.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 256 |}.
+  End B2048.
+
+  Module BlockHash.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 32 |}.
+  End BlockHash.
+
+  Module BlockNumber.
+    Definition t : Set :=
+      U64.t.
+  End BlockNumber.
+
+  Module BlockTimestamp.
+    Definition t : Set :=
+      U64.t.
+  End BlockTimestamp.
+
+  Module TxHash.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 32 |}.
+  End TxHash.
+
+  Module TxNumber.
+    Definition t : Set :=
+      U64.t.
+  End TxNumber.
+
+  Module TxNonce.
+    Definition t : Set :=
+      U64.t.
+  End TxNonce.
+
+  Module TxIndex.
+    Definition t : Set :=
+      U64.t.
+  End TxIndex.
+
+  Module ChainId.
+    Definition t : Set :=
+      U64.t.
+  End ChainId.
+
+  Module StorageKey.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 32 |}.
+  End StorageKey.
+
+  Module StorageValue.
+    Definition t : Set :=
+      Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}.
+  End StorageValue.
+
+  Module Selector.
+    Definition t : Set :=
+      FixedBytes.t {| Integer.value := 4 |}.
+  End Selector.
+End aliases.
diff --git a/CoqOfRust/alloy_primitives/links/lib.v b/CoqOfRust/alloy_primitives/links/lib.v
new file mode 100644
index 000000000..e69de29bb
diff --git a/CoqOfRust/alloy_primitives/signed/links/int.v b/CoqOfRust/alloy_primitives/signed/links/int.v
new file mode 100644
index 000000000..63ea14b98
--- /dev/null
+++ b/CoqOfRust/alloy_primitives/signed/links/int.v
@@ -0,0 +1,18 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import ruint.links.lib.
+
+(* pub struct Signed<const BITS: usize, const LIMBS: usize>(pub(crate) Uint<BITS, LIMBS>); *)
+Module Signed.
+  Record t {BITS LIMBS: Usize.t} : Set := {
+    value : Uint.t BITS LIMBS;
+  }.
+  Arguments t : clear implicits.
+
+  Parameter to_value : forall {BITS: Usize.t} {LIMBS: Usize.t}, t BITS LIMBS -> Value.t.
+
+  Global Instance IsLink (BITS: Usize.t) (LIMBS: Usize.t): Link (t BITS LIMBS) := {
+    Φ := Ty.apply (Ty.path "alloy_primitives::signed::int::Signed") [ φ BITS; φ LIMBS ] [];
+    φ := to_value;
+  }.
+End Signed.
diff --git a/CoqOfRust/alloy_primitives/utils/links/mod.v b/CoqOfRust/alloy_primitives/utils/links/mod.v
new file mode 100644
index 000000000..d602b9415
--- /dev/null
+++ b/CoqOfRust/alloy_primitives/utils/links/mod.v
@@ -0,0 +1,16 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.links.aliases.
+Require Import alloy_primitives.utils.mod.
+
+(* pub fn keccak256<T: AsRef<[u8]>>(bytes: T) -> B256 *)
+Instance run_keccak256
+  {T : Set} `{Link T}
+  (bytes : T) :
+  Run.Trait
+    utils.keccak256 [] [ Φ T ] [ φ bytes ]
+    aliases.B256.t.
+Proof.
+  constructor.
+  run_symbolic.
+Admitted.
diff --git a/CoqOfRust/revm/links/dependencies.v b/CoqOfRust/revm/links/dependencies.v
deleted file mode 100644
index f86621596..000000000
--- a/CoqOfRust/revm/links/dependencies.v
+++ /dev/null
@@ -1,260 +0,0 @@
-Require Import CoqOfRust.CoqOfRust.
-Require Import CoqOfRust.links.M.
-Require Import core.convert.links.mod.
-Require Import core.links.array.
-Require Import core.ops.links.range.
-Require Import core.links.clone.
-Require Import core.links.default.
-Require Import ruint.links.lib.
-
-Module U256.
-  Definition t : Set :=
-    Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}.
-End U256.
-
-Module alloy_primitives.
-  Module bits.
-    Module links.
-      Module fixed.
-        (* pub struct FixedBytes<const N: usize>(#[into_iterator(owned, ref, ref_mut)] 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 : Usize.t) (N' : Value.t) :
-            N' = φ N ->
-            OfTy.t (Ty.apply (Ty.path "alloy_primitives::bits::fixed::FixedBytes") [ N' ] []).
-          Proof.
-            intros.
-            eapply OfTy.Make with (A := t N).
-            now subst.
-          Defined.
-          Smpl Add eapply of_ty : of_ty.
-        End FixedBytes.
-
-        Module Impl_From_for_FixedBytes.
-          Definition Self (N : Usize.t) : Set :=
-            FixedBytes.t N.
-
-          Parameter from : forall (N : Usize.t), PolymorphicFunction.t.
-
-          Axiom Implements :
-            forall (N : Usize.t),
-            M.IsTraitInstance
-              "core::convert::From"
-              (* Trait polymorphic consts *) []
-              (* Trait polymorphic types *) [ Φ (array.t U8.t N) ]
-              (Φ (Self N))
-              (* Instance *) [ ("from", InstanceField.Method (from N)) ].
-
-          Parameter run :
-            forall (N : Usize.t),
-            core.convert.links.mod.From.Run (Self N) (T := array.t U8.t N).
-        End Impl_From_for_FixedBytes.
-
-        Module Impl_Into_array_for_FixedBytes.
-          Definition Self (N : Usize.t) : Set :=
-            FixedBytes.t N.
-
-          (* fn into(self) -> Uint *)
-          Parameter into : forall (N : Usize.t), PolymorphicFunction.t.
-
-          Axiom Implements :
-            forall (N : Usize.t),
-            M.IsTraitInstance
-              "core::convert::Into" [] [ Φ (array.t U8.t N) ] (Φ (Self N))
-              [ ("into", InstanceField.Method (into N)) ].
-
-          Parameter run :
-            forall (N : Usize.t),
-            core.convert.links.mod.Into.Run (Self N) (array.t U8.t N).
-        End Impl_Into_array_for_FixedBytes.
-
-        Module Impl_Into_U256_for_FixedBytes.
-          Definition Self : Set :=
-            FixedBytes.t {| Integer.value := 32 |}.
-
-          Parameter into : PolymorphicFunction.t.
-
-          Axiom Implements :
-            M.IsTraitInstance
-              "core::convert::Into" [] [ Φ U256.t ] (Φ Self)
-              [ ("into", InstanceField.Method into) ].
-
-          Parameter run :
-            core.convert.links.mod.Into.Run Self U256.t.
-        End Impl_Into_U256_for_FixedBytes.
-      End fixed.
-
-      Module address.
-        Module Address.
-          Parameter t : Set.
-
-          Parameter to_value : t -> Value.t.
-
-          Global Instance IsLink : Link t := {
-            Φ := Ty.path "alloy_primitives::bits::address::Address";
-            φ := to_value;
-          }.
-
-          Definition of_ty : OfTy.t (Ty.path "alloy_primitives::bits::address::Address").
-          Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
-          Smpl Add apply of_ty : of_ty.
-        End Address.
-
-        (* impl Address { *)
-        Module Impl_Address.
-          Definition Self : Set :=
-            Address.t.
-
-          (* pub fn from_word(word: FixedBytes<32>) -> Self *)
-          Parameter from_word : PolymorphicFunction.t.
-
-          Global Instance AssociatedFunction_from_word :
-            M.IsAssociatedFunction.Trait (Φ Self) "from_word" from_word.
-          Admitted.
-
-          Global Instance run_from_word (word : fixed.FixedBytes.t {| Integer.value := 32 |}) :
-            Run.Trait from_word [] [] [ φ word ] Address.t.
-          Admitted.
-
-          (* pub fn into_word(&self) -> FixedBytes<32> *)
-          Parameter into_word : PolymorphicFunction.t.
-
-          Global Instance AssociatedFunction_into_word :
-            M.IsAssociatedFunction.Trait (Φ Self) "into_word" into_word.
-          Admitted.
-
-          Global Instance run_into_word (self : Address.t) :
-            Run.Trait into_word [] [] [ φ self ] (fixed.FixedBytes.t {| Integer.value := 32 |}).
-          Admitted.
-
-        End Impl_Address.
-      End address.
-    End links.
-  End bits.
-
-  Module links.
-    Module bytes_.
-      Module Bytes.
-        Parameter t : Set.
-
-        Parameter to_value : t -> Value.t.
-
-        Global Instance IsLink : Link t := {
-          Φ := Ty.path "alloy_primitives::bytes_::Bytes";
-          φ := to_value;
-        }.
-
-        Definition of_ty : OfTy.t (Ty.path "alloy_primitives::bytes_::Bytes").
-        Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
-        Smpl Add apply of_ty : of_ty.
-      End Bytes.
-
-      Module Impl_Bytes.
-        Definition Self : Set :=
-          Bytes.t.
-
-        (* pub fn new() -> Self *)
-        Parameter new : PolymorphicFunction.t.
-
-        Global Instance AssociatedFunction_new :
-          M.IsAssociatedFunction.Trait (Φ Self) "new" new.
-        Admitted.
-
-        Global Instance run_new : Run.Trait new [] [] [] Bytes.t.
-        Admitted.
-
-        (* pub fn slice(&self, range: impl RangeBounds<usize>) -> Self *)
-        Parameter slice : PolymorphicFunction.t.
-
-        Global Instance AssociatedFunction_slice :
-          M.IsAssociatedFunction.Trait (Φ Self) "slice" slice.
-        Admitted.
-
-        Global Instance run_slice {A : Set} `{Link A} 
-          (self : Ref.t Pointer.Kind.Ref Self) 
-          (range : A) 
-          (run_RangeBounds_for_A : RangeBounds.Run A) :
-          Run.Trait slice [] [] [φ self; φ range] Self.
-        Admitted.
-      End Impl_Bytes.
-      
-      Module Impl_Clone_for_Bytes.
-        Definition Self : Ty.t := Ty.path "alloy_primitives::bytes_::Bytes".
-
-        Parameter clone : PolymorphicFunction.t.
-
-        Axiom Implements :
-          M.IsTraitInstance
-            "core::clone::Clone"
-            (* Trait polymorphic consts *) []
-            (* Trait polymorphic types *) []
-            Self
-            (* Instance *) [ ("clone", InstanceField.Method clone) ].
-
-        Definition run_clone : clone.Clone.Run_clone Bytes.t.
-        Admitted.
-      
-        Instance run : Clone.Run Bytes.t := {
-          CLone.clone := run_clone;
-        }.
-      End Impl_Clone_for_Bytes.
-
-      Module Impl_Default_for_Bytes.
-        Definition Self : Ty.t := Ty.path "alloy_primitives::bytes_::Bytes".
-
-        Parameter default : PolymorphicFunction.t.
-
-        Axiom Implements :
-          M.IsTraitInstance
-            "default::default::Default"
-            (* Trait polymorphic consts *) []
-            (* Trait polymorphic types *) []
-            Self
-            (* Instance *) [ ("default", InstanceField.Method default) ].
-
-        Definition run_default : default.Default.Run_default Bytes.t.
-        Admitted.
-      
-        Instance run : Default.Run Bytes.t := {
-          Default.default := run_default;
-        }.
-      End Impl_Default_for_Bytes.
-    End bytes_.
-  End links.
-End alloy_primitives.
-
-Module FixedBytes.
-  Parameter t : Set.
-
-  Parameter to_value : t -> Value.t.
-
-  Global Instance IsLink : Link t := {
-    Φ := Ty.path "alloy_primitives::bits::fixed::FixedBytes";
-    φ := to_value;
-  }.
-End FixedBytes.
-
-(** ** Here we define some aliases that are convenient *)
-
-Module B256.
-  Definition t : Set :=
-    alloy_primitives.bits.links.fixed.FixedBytes.t {| Integer.value := 32 |}.
-End B256.
-
-Module Address.
-  Definition t : Set :=
-    alloy_primitives.bits.links.address.Address.t.
-End Address.
-
-Module Bytes.
-  Definition t : Set :=
-    alloy_primitives.links.bytes_.Bytes.t.
-End Bytes.
diff --git a/CoqOfRust/revm/revm_bytecode/eof/links/body.v b/CoqOfRust/revm/revm_bytecode/eof/links/body.v
index 92b308817..65fd5c333 100644
--- a/CoqOfRust/revm/revm_bytecode/eof/links/body.v
+++ b/CoqOfRust/revm/revm_bytecode/eof/links/body.v
@@ -2,11 +2,11 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
 Require Import alloc.links.alloc.
 Require Import alloc.vec.links.mod.
+Require Import alloy_primitives.bytes.links.mod.
 Require Import core.links.clone.
 Require Import core.links.default.
 Require Import core.links.result.
 Require Import core.links.option.
-Require Import revm.links.dependencies.
 Require Export revm.revm_bytecode.eof.links.body_EofBody.
 Require Export revm.revm_bytecode.eof.links.header.
 Require Import revm.revm_bytecode.eof.links.types_section.
@@ -16,11 +16,11 @@ Require Import core.slice.links.mod.
 
 Module EofBody.
   Record t : Set := {
-    types_section: Vec.t revm_bytecode.eof.links.types_section.TypesSection.t Global.t;
+    types_section: Vec.t TypesSection.t Global.t;
     code_section: Vec.t Usize.t Global.t;
-    code: alloy_primitives.links.bytes_.Bytes.t;
-    container_section: Vec.t alloy_primitives.links.bytes_.Bytes.t Global.t;
-    data_section: alloy_primitives.links.bytes_.Bytes.t;
+    code: Bytes.t;
+    container_section: Vec.t Bytes.t Global.t;
+    data_section: Bytes.t;
     is_data_filled: bool;
   }.
 
@@ -42,11 +42,11 @@ Module EofBody.
   Smpl Add apply of_ty : of_ty.
 
   Lemma of_value_with
-      (types_section : Vec.t revm_bytecode.eof.links.types_section.TypesSection.t Global.t) types_section'
+      (types_section : Vec.t TypesSection.t Global.t) types_section'
       (code_section : Vec.t Usize.t Global.t) code_section'
-      (code : alloy_primitives.links.bytes_.Bytes.t) code'
-      (container_section : Vec.t alloy_primitives.links.bytes_.Bytes.t Global.t) container_section'
-      (data_section : alloy_primitives.links.bytes_.Bytes.t) data_section'
+      (code : Bytes.t) code'
+      (container_section : Vec.t Bytes.t Global.t) container_section'
+      (data_section : Bytes.t) data_section'
       (is_data_filled : bool) is_data_filled' :
     types_section' = φ types_section ->
     code_section' = φ code_section ->
@@ -66,11 +66,11 @@ Module EofBody.
   Smpl Add apply of_value_with : of_value.
 
   Definition of_value
-      (types_section : Vec.t revm_bytecode.eof.links.types_section.TypesSection.t Global.t)
+      (types_section : Vec.t TypesSection.t Global.t)
       (code_section : Vec.t Usize.t Global.t)
-      (code : alloy_primitives.links.bytes_.Bytes.t)
-      (container_section : Vec.t alloy_primitives.links.bytes_.Bytes.t Global.t)
-      (data_section : alloy_primitives.links.bytes_.Bytes.t)
+      (code : Bytes.t)
+      (container_section : Vec.t Bytes.t Global.t)
+      (data_section : Bytes.t)
       (is_data_filled : bool) :
     OfValue.t (
       Value.StructRecord "revm_bytecode::eof::body::EofBody" [
@@ -183,12 +183,12 @@ Module Impl_Clone_for_EofBody.
     { constructor.
       destruct (vec.links.mod.Impl_Clone_for_Vec.run (T := TypesSection.t) (A := Global.t)).
       destruct (vec.links.mod.Impl_Clone_for_Vec.run (T := Usize.t) (A := Global.t)).
-      destruct alloy_primitives.links.bytes_.Impl_Clone_for_Bytes.run.
-      destruct (vec.links.mod.Impl_Clone_for_Vec.run (T := alloy_primitives.links.bytes_.Bytes.t) (A := Global.t)).
+      destruct alloy_primitives.bytes.links.mod.Impl_Clone_for_Bytes.run.
+      destruct (vec.links.mod.Impl_Clone_for_Vec.run (T := Bytes.t) (A := Global.t)).
       destruct clone.Impl_Clone_for_bool.run.
       run_symbolic.
     }
-  Defined.
+  Admitted.
 
   Instance run : Clone.Run EofBody.t := {
     Clone.clone := run_clone;
@@ -206,10 +206,10 @@ Module Impl_Default_for_EofBody.
     { constructor.
       destruct (vec.links.mod.Impl_Default_for_Vec.run (T := TypesSection.t) (A := Global.t)).
       destruct (vec.links.mod.Impl_Default_for_Vec.run (T := Usize.t) (A := Global.t)).
-      destruct alloy_primitives.links.bytes_.Impl_Default_for_Bytes.run.
-      destruct (vec.links.mod.Impl_Default_for_Vec.run (T := alloy_primitives.links.bytes_.Bytes.t) (A := Global.t)).
+      destruct alloy_primitives.bytes.links.mod.Impl_Default_for_Bytes.run.
+      destruct (vec.links.mod.Impl_Default_for_Vec.run (T := Bytes.t) (A := Global.t)).
       destruct default.Impl_Default_for_bool.run.
-      run_symbolic. 
+      run_symbolic.
     }
   Defined.
 
@@ -230,7 +230,7 @@ Module Impl_EofBody.
     pub fn code(&self, index: usize) -> Option<Bytes>
   *)
   Instance run_code (self : Ref.t Pointer.Kind.Ref Self) (index : Usize.t) :
-    Run.Trait body.eof.body.Impl_revm_bytecode_eof_body_EofBody.code [] [] [φ self; φ index] (option alloy_primitives.links.bytes_.Bytes.t).
+    Run.Trait body.eof.body.Impl_revm_bytecode_eof_body_EofBody.code [] [] [φ self; φ index] (option Bytes.t).
   Proof.
     constructor.
     destruct (vec.links.mod.Impl_Index_for_Vec_T_A.run Usize.t Usize.t Global.t Usize.t).
@@ -273,7 +273,7 @@ Module Impl_EofBody.
   (*
     pub fn decode(input: &Bytes, header: &EofHeader) -> Result<Self, EofDecodeError>
   *)
-  Instance run_decode (input : Ref.t Pointer.Kind.Ref alloy_primitives.links.bytes_.Bytes.t) (header : Ref.t Pointer.Kind.Ref EofHeader.t) :
+  Instance run_decode (input : Ref.t Pointer.Kind.Ref Bytes.t) (header : Ref.t Pointer.Kind.Ref EofHeader.t) :
     Run.Trait body.eof.body.Impl_revm_bytecode_eof_body_EofBody.decode [] [] [φ input; φ header] (Result.t EofBody.t EofDecodeError.t).
   Proof.  
     constructor.
diff --git a/CoqOfRust/revm/revm_bytecode/eof/links/body_EofBody.v b/CoqOfRust/revm/revm_bytecode/eof/links/body_EofBody.v
index 4885612c1..4aafeb5ca 100644
--- a/CoqOfRust/revm/revm_bytecode/eof/links/body_EofBody.v
+++ b/CoqOfRust/revm/revm_bytecode/eof/links/body_EofBody.v
@@ -2,22 +2,22 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
 Require Import alloc.links.alloc.
 Require Import alloc.vec.links.mod.
-Require core.links.clone.
-Require core.links.default.
+Require Import alloy_primitives.bytes.links.mod.
+Require Import core.links.clone.
+Require Import core.links.default.
 Require Import core.links.option.
 Require Import core.slice.links.index.
 Require Import core.slice.links.mod.
-Require Import revm.links.dependencies.
 Require Import revm.revm_bytecode.eof.links.types_section.
 Require Import revm_bytecode.eof.body.
 
 Module EofBody.
   Record t : Set := {
-    types_section: Vec.t revm_bytecode.eof.links.types_section.TypesSection.t Global.t;
+    types_section: Vec.t TypesSection.t Global.t;
     code_section: Vec.t Usize.t Global.t;
-    code: alloy_primitives.links.bytes_.Bytes.t;
-    container_section: Vec.t alloy_primitives.links.bytes_.Bytes.t Global.t;
-    data_section: alloy_primitives.links.bytes_.Bytes.t;
+    code: Bytes.t;
+    container_section: Vec.t Bytes.t Global.t;
+    data_section: Bytes.t;
     is_data_filled: bool;
   }.
 
@@ -39,11 +39,11 @@ Module EofBody.
   Smpl Add apply of_ty : of_ty.
 
   Lemma of_value_with
-      (types_section : Vec.t revm_bytecode.eof.links.types_section.TypesSection.t Global.t) types_section'
+      (types_section : Vec.t TypesSection.t Global.t) types_section'
       (code_section : Vec.t Usize.t Global.t) code_section'
-      (code : alloy_primitives.links.bytes_.Bytes.t) code'
-      (container_section : Vec.t alloy_primitives.links.bytes_.Bytes.t Global.t) container_section'
-      (data_section : alloy_primitives.links.bytes_.Bytes.t) data_section'
+      (code : Bytes.t) code'
+      (container_section : Vec.t Bytes.t Global.t) container_section'
+      (data_section : Bytes.t) data_section'
       (is_data_filled : bool) is_data_filled' :
     types_section' = φ types_section ->
     code_section' = φ code_section ->
@@ -63,11 +63,11 @@ Module EofBody.
   Smpl Add apply of_value_with : of_value.
 
   Definition of_value
-      (types_section : Vec.t revm_bytecode.eof.links.types_section.TypesSection.t Global.t)
+      (types_section : Vec.t TypesSection.t Global.t)
       (code_section : Vec.t Usize.t Global.t)
-      (code : alloy_primitives.links.bytes_.Bytes.t)
-      (container_section : Vec.t alloy_primitives.links.bytes_.Bytes.t Global.t)
-      (data_section : alloy_primitives.links.bytes_.Bytes.t)
+      (code : Bytes.t)
+      (container_section : Vec.t Bytes.t Global.t)
+      (data_section : Bytes.t)
       (is_data_filled : bool) :
     OfValue.t (
       Value.StructRecord "revm_bytecode::eof::body::EofBody" [
diff --git a/CoqOfRust/revm/revm_bytecode/eof/links/types_section.v b/CoqOfRust/revm/revm_bytecode/eof/links/types_section.v
index 17f5c9c39..d6dae997b 100644
--- a/CoqOfRust/revm/revm_bytecode/eof/links/types_section.v
+++ b/CoqOfRust/revm/revm_bytecode/eof/links/types_section.v
@@ -2,7 +2,6 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
 Require alloc.links.alloc.
 Require alloc.vec.links.mod.
-Require Import revm.links.dependencies.
 
 Module TypesSection.
   Record t : Set := {
diff --git a/CoqOfRust/revm/revm_bytecode/links/bytecode.v b/CoqOfRust/revm/revm_bytecode/links/bytecode.v
index 60d249086..7ad7a622e 100644
--- a/CoqOfRust/revm/revm_bytecode/links/bytecode.v
+++ b/CoqOfRust/revm/revm_bytecode/links/bytecode.v
@@ -1,6 +1,5 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
-Require Import revm.links.dependencies.
 
 (* Module Bytecode.
   Inductive t : Set :=
diff --git a/CoqOfRust/revm/revm_bytecode/links/eof.v b/CoqOfRust/revm/revm_bytecode/links/eof.v
index 615b44ddf..f6c709d29 100644
--- a/CoqOfRust/revm/revm_bytecode/links/eof.v
+++ b/CoqOfRust/revm/revm_bytecode/links/eof.v
@@ -1,15 +1,15 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require alloc.links.alloc.
-Require Import revm.links.dependencies.
+Require Import alloc.links.alloc.
+Require Import alloy_primitives.bytes.links.mod.
 Require Import revm.revm_bytecode.eof.links.body_EofBody.
-Require revm.revm_bytecode.eof.links.header.
+Require Import revm.revm_bytecode.eof.links.header.
 
 Module Eof.
   Record t : Set := {
     header: revm_bytecode.eof.links.header.EofHeader.t;
     body: EofBody.t;
-    raw: alloy_primitives.links.bytes_.Bytes.t;
+    raw: Bytes.t;
   }.
 
   Global Instance IsLink : Link t := {
diff --git a/CoqOfRust/revm/revm_context_interface/links/block.v b/CoqOfRust/revm/revm_context_interface/links/block.v
index b090dfff7..72a50164e 100644
--- a/CoqOfRust/revm/revm_context_interface/links/block.v
+++ b/CoqOfRust/revm/revm_context_interface/links/block.v
@@ -1,8 +1,8 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import CoqOfRust.revm.links.dependencies.
-
-Module Address := dependencies.alloy_primitives.bits.links.address.Address.
+Require Import alloy_primitives.bits.links.address.
+Require Import alloy_primitives.links.aliases.
+Require Import core.links.option.
 
 (* 
 #[auto_impl(&, &mut, Box, Arc)]
@@ -68,7 +68,7 @@ Module Block.
   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 ] U256.t
+        Run.Trait method [] [] [ φ self ] aliases.U256.t
     ).
 
   (* fn blob_gasprice(&self) -> Option<u128> *)
diff --git a/CoqOfRust/revm/revm_context_interface/links/cfg.v b/CoqOfRust/revm/revm_context_interface/links/cfg.v
index 83e0d8b21..6a88c0ad5 100644
--- a/CoqOfRust/revm/revm_context_interface/links/cfg.v
+++ b/CoqOfRust/revm/revm_context_interface/links/cfg.v
@@ -1,9 +1,8 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import CoqOfRust.core.convert.links.mod.
-Require Import CoqOfRust.revm.links.dependencies.
-Require Import CoqOfRust.revm.revm_specification.links.hardfork.
-
+Require Import alloy_primitives.links.aliases.
+Require Import core.convert.links.mod.
+Require Import revm.revm_specification.links.hardfork.
 (*
   /// Create scheme.
   #[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
@@ -22,7 +21,7 @@ Require Import CoqOfRust.revm.revm_specification.links.hardfork.
 Module CreateScheme.
   Inductive t : Set :=
   | Create
-  | Create2 : U256.t -> t.
+  | Create2 : aliases.U256.t -> t.
 
   Global Instance IsLink : Link t := {
     Φ := Ty.path "revm_primitives::env::CreateScheme";
diff --git a/CoqOfRust/revm/revm_context_interface/links/host.v b/CoqOfRust/revm/revm_context_interface/links/host.v
index 0258d0bdc..656da6ea5 100644
--- a/CoqOfRust/revm/revm_context_interface/links/host.v
+++ b/CoqOfRust/revm/revm_context_interface/links/host.v
@@ -1,9 +1,11 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import CoqOfRust.revm.links.dependencies.
-Require Import CoqOfRust.revm.revm_context_interface.links.cfg.
-Require Import CoqOfRust.revm.revm_context_interface.links.block.
-Require Import CoqOfRust.revm.revm_context_interface.links.journaled_state.
+Require Import alloy_primitives.bits.links.address.
+Require Import alloy_primitives.bytes.links.mod.
+Require Import alloy_primitives.links.aliases.
+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.
@@ -125,7 +127,7 @@ Module Host.
       IsTraitMethod.t "revm_context_interface::cfg::Cfg" [] [] (Φ Self) "load_account_delegated" load_account_delegated *
       forall
           (self : Ref.t Pointer.Kind.MutRef Self)
-          (address : alloy_primitives.bits.links.address.Address.t),
+          (address : Address.t),
         {{ load_account_delegated [] [] [ φ self; φ address ] 🔽 option AccountLoad.t }}
     }.
 
@@ -135,7 +137,7 @@ Module Host.
       forall
           (self : Ref.t Pointer.Kind.MutRef Self)
           (number : U64.t),
-        {{ block_hash [] [] [ φ self; φ number ] 🔽 option B256.t }}
+        {{ block_hash [] [] [ φ self; φ number ] 🔽 option aliases.B256.t }}
     }.
 
   Definition Run_balance (Self : Set) `{Link Self} : Set :=
@@ -143,8 +145,8 @@ Module Host.
       IsTraitMethod.t "revm_context_interface::cfg::Cfg" [] [] (Φ Self) "balance" balance *
       forall
           (self : Ref.t Pointer.Kind.MutRef Self)
-          (address : alloy_primitives.bits.links.address.Address.t),
-        {{ balance [] [] [ φ self; φ address ] 🔽 option (StateLoad.t U256.t) }}
+          (address : Address.t),
+        {{ balance [] [] [ φ self; φ address ] 🔽 option (StateLoad.t aliases.U256.t) }}
     }.
 
   Definition Run_code (Self : Set) `{Link Self} : Set :=
@@ -152,8 +154,8 @@ Module Host.
       IsTraitMethod.t "revm_context_interface::cfg::Cfg" [] [] (Φ Self) "code" code *
       forall
           (self : Ref.t Pointer.Kind.MutRef Self)
-          (address : alloy_primitives.bits.links.address.Address.t),
-        {{ code [] [] [ φ self; φ address ] 🔽 option (Eip7702CodeLoad.t alloy_primitives.links.bytes_.Bytes.t) }}
+          (address : Address.t),
+        {{ code [] [] [ φ self; φ address ] 🔽 option (Eip7702CodeLoad.t Bytes.t) }}
     }.
 
   Definition Run_code_hash (Self : Set) `{Link Self} : Set :=
@@ -161,8 +163,8 @@ Module Host.
       IsTraitMethod.t "revm_context_interface::cfg::Cfg" [] [] (Φ Self) "code_hash" code_hash *
       forall
           (self : Ref.t Pointer.Kind.MutRef Self)
-          (address : alloy_primitives.bits.links.address.Address.t),
-        {{ code_hash [] [] [ φ self; φ address ] 🔽 option (Eip7702CodeLoad.t B256.t) }}
+          (address : Address.t),
+        {{ code_hash [] [] [ φ self; φ address ] 🔽 option (Eip7702CodeLoad.t aliases.B256.t) }}
     }.
 
   Definition Run_sload (Self : Set) `{Link Self} : Set :=
@@ -170,9 +172,9 @@ Module Host.
       IsTraitMethod.t "revm_context_interface::cfg::Cfg" [] [] (Φ Self) "sload" sload *
       forall
           (self : Ref.t Pointer.Kind.MutRef Self)
-          (address : alloy_primitives.bits.links.address.Address.t)
-          (index : U256.t),
-        {{ sload [] [] [ φ self; φ address; φ index ] 🔽 option (StateLoad.t U256.t) }}
+          (address : Address.t)
+          (index : aliases.U256.t),
+        {{ sload [] [] [ φ self; φ address; φ index ] 🔽 option (StateLoad.t aliases.U256.t) }}
     }.
 
   Definition Run_sstore (Self : Set) `{Link Self} : Set :=
@@ -180,9 +182,9 @@ Module Host.
       IsTraitMethod.t "revm_context_interface::cfg::Cfg" [] [] (Φ Self) "sstore" sstore *
       forall
           (self : Ref.t Pointer.Kind.MutRef Self)
-          (address : alloy_primitives.bits.links.address.Address.t)
-          (index : U256.t)
-          (value : U256.t),
+          (address : Address.t)
+          (index : aliases.U256.t)
+          (value : aliases.U256.t),
         {{ sstore [] [] [ φ self; φ address; φ index; φ value ] 🔽 option (StateLoad.t SStoreResult.t) }}
     }.
 
@@ -191,9 +193,9 @@ Module Host.
       IsTraitMethod.t "revm_context_interface::cfg::Cfg" [] [] (Φ Self) "tload" tload *
       forall
           (self : Ref.t Pointer.Kind.MutRef Self)
-          (address : alloy_primitives.bits.links.address.Address.t)
-          (index : U256.t),
-        {{ tload [] [] [ φ self; φ address; φ index ] 🔽 U256.t }}
+          (address : Address.t)
+          (index : aliases.U256.t),
+        {{ tload [] [] [ φ self; φ address; φ index ] 🔽 aliases.U256.t }}
     }.
 
   Definition Run_tstore (Self : Set) `{Link Self} : Set :=
@@ -201,9 +203,9 @@ Module Host.
       IsTraitMethod.t "revm_context_interface::cfg::Cfg" [] [] (Φ Self) "tstore" tstore *
       forall
           (self : Ref.t Pointer.Kind.MutRef Self)
-          (address : alloy_primitives.bits.links.address.Address.t)
-          (index : U256.t)
-          (value : U256.t),
+          (address : Address.t)
+          (index : aliases.U256.t)
+          (value : aliases.U256.t),
         {{ tstore [] [] [ φ self; φ address; φ index; φ value ] 🔽 unit }}
     }.
 
@@ -221,8 +223,8 @@ Module Host.
       IsTraitMethod.t "revm_context_interface::cfg::Cfg" [] [] (Φ Self) "selfdestruct" selfdestruct *
       forall
           (self : Ref.t Pointer.Kind.MutRef Self)
-          (address : alloy_primitives.bits.links.address.Address.t)
-          (target : alloy_primitives.bits.links.address.Address.t),
+          (address : Address.t)
+          (target : Address.t),
         {{ selfdestruct [] [] [ φ self; φ address; φ target ] 🔽 option (StateLoad.t SelfDestructResult.t) }}
     }.
 
diff --git a/CoqOfRust/revm/revm_interpreter/gas/links/calc.v b/CoqOfRust/revm/revm_interpreter/gas/links/calc.v
index cc7629eda..101fcd047 100644
--- a/CoqOfRust/revm/revm_interpreter/gas/links/calc.v
+++ b/CoqOfRust/revm/revm_interpreter/gas/links/calc.v
@@ -1,8 +1,8 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.links.aliases.
 Require Import core.num.mod.
 Require Import core.num.links.mod.
-Require Import revm.links.dependencies.
 Require Import revm.revm_context_interface.links.host.
 Require Import revm.revm_context_interface.links.journaled_state.
 Require Import revm.revm_interpreter.gas.links.constants.
@@ -33,7 +33,7 @@ Proof.
 Admitted.
 
 (* pub const fn log2floor(value: U256) -> u64 *)
-Instance run_log2floor (value : U256.t) :
+Instance run_log2floor (value : aliases.U256.t) :
   Run.Trait
     gas.calc.log2floor [] [] [ φ value ]
     U64.t.
@@ -43,7 +43,7 @@ Proof.
 Admitted.
 
 (* pub fn exp_cost(spec_id: SpecId, power: U256) -> Option<u64> *)
-Instance run_exp_cost (spec_id : SpecId.t) (power : U256.t) :
+Instance run_exp_cost (spec_id : SpecId.t) (power : aliases.U256.t) :
   Run.Trait
     gas.calc.exp_cost [] [] [ φ spec_id; φ power ]
     (option U64.t).
diff --git a/CoqOfRust/revm/revm_interpreter/gas/simulations/calc.v b/CoqOfRust/revm/revm_interpreter/gas/simulations/calc.v
index db6e91227..a41f2116c 100644
--- a/CoqOfRust/revm/revm_interpreter/gas/simulations/calc.v
+++ b/CoqOfRust/revm/revm_interpreter/gas/simulations/calc.v
@@ -1,6 +1,4 @@
 Require Import CoqOfRust.CoqOfRust.
-Require Import revm.links.dependencies.
-Require Import revm.simulations.dependencies.
 Require Import revm_interpreter.gas.simulations.constants.
 
 (*
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v
index d1618ddf4..8da631616 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/block_info.v
@@ -1,6 +1,5 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import CoqOfRust.revm.links.dependencies.
 Require Import revm.revm_context_interface.links.host.
 Require Import revm.revm_context_interface.links.block.
 Require Import revm.revm_interpreter.links.gas.
@@ -88,7 +87,7 @@ Proof.
   destruct run_Host_for_H.
   destruct run_BlockGetter.
   destruct run_Block_for_Block.
-  destruct alloy_primitives.bits.links.fixed.Impl_Into_U256_for_FixedBytes.run.
+  (* destruct alloy_primitives.bits.links.fixed.Impl_Into_U256_for_FixedBytes.run. *)
   (* TODO: resolve axiomatization for:
   - Impl_Address::into_word(?)
   - FixedBytes::into()
@@ -202,7 +201,7 @@ Proof.
   destruct run_Host_for_H.
   destruct run_BlockGetter.
   destruct run_Block_for_Block.
-  destruct alloy_primitives.bits.links.fixed.Impl_Into_U256_for_FixedBytes.run.
+  (* destruct alloy_primitives.bits.links.fixed.Impl_Into_U256_for_FixedBytes.run. *)
   (* TODO: 
   - revm_interpreter::instructions::utility::IntoU256::into_u256
   *)
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract.v
index 109d1236a..456576a11 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/contract.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract.v
@@ -1,6 +1,7 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import CoqOfRust.revm.links.dependencies.
+Require Import alloy_primitives.bits.links.address.
+Require Import alloy_primitives.bytes.links.mod.
 Require Import revm.revm_context_interface.links.host.
 Require Import revm.revm_interpreter.links.interpreter.
 Require Import revm.revm_interpreter.links.interpreter_types.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/data.v b/CoqOfRust/revm/revm_interpreter/instructions/links/data.v
index 705d22763..57f69c6bb 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/data.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/data.v
@@ -1,6 +1,5 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import CoqOfRust.revm.links.dependencies.
 Require Import revm.revm_context_interface.links.host.
 Require Import revm.revm_interpreter.links.interpreter.
 Require Import revm.revm_interpreter.links.interpreter_types.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/host.v b/CoqOfRust/revm/revm_interpreter/instructions/links/host.v
index b63a1ed1c..48f5f576d 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/host.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/host.v
@@ -1,6 +1,6 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import revm.links.dependencies.
+Require Import alloy_primitives.links.aliases.
 Require Import revm.revm_interpreter.instructions.host.
 Require Import revm.revm_interpreter.instructions.links.utility.
 Require Import revm.revm_interpreter.links.interpreter.
@@ -34,7 +34,6 @@ Proof.
   run_symbolic.
 Admitted.
 
-
 (*
 pub fn selfbalance<WIRE: InterpreterTypes, H: Host + ?Sized>(
     interpreter: &mut Interpreter<WIRE>,
@@ -69,13 +68,12 @@ Instance run_extcodesize
   (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
     instructions.host.extcodesize [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
-    U256.t.
+    aliases.U256.t.
 Proof.
   constructor.
   run_symbolic.
 Admitted.
 
-
 (*
 pub fn extcodehash<WIRE: InterpreterTypes, H: Host + ?Sized>(
     interpreter: &mut Interpreter<WIRE>,
@@ -90,13 +88,12 @@ Instance run_extcodehash
   (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
     instructions.host.extcodehash [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
-    U256.t.
+    aliases.U256.t.
 Proof.
   constructor.
   run_symbolic.
 Admitted.
 
-
 (*
 pub fn extcodecopy<WIRE: InterpreterTypes, H: Host + ?Sized>(
     interpreter: &mut Interpreter<WIRE>,
@@ -131,7 +128,7 @@ Instance run_blockhash
   (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
     instructions.host.blockhash [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
-    U256.t.
+    aliases.U256.t.
 Proof.
   constructor.
   run_symbolic.
@@ -151,7 +148,7 @@ Instance run_sload
   (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
     instructions.host.sload [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
-    U256.t.
+    aliases.U256.t.
 Proof.
   constructor.
   run_symbolic.
@@ -211,7 +208,7 @@ Instance run_tload
   (host : Ref.t Pointer.Kind.MutRef H) :
   Run.Trait
     instructions.host.tload [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ]
-    U256.t.
+    aliases.U256.t.
 Proof.
   constructor.
   run_symbolic.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v
index 42a9cd543..fca887c65 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/i256.v
@@ -1,7 +1,7 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.links.aliases.
 Require Import core.links.cmp.
-Require Import revm.links.dependencies.
 Require Import revm.revm_interpreter.instructions.i256.
 
 (*
@@ -71,7 +71,7 @@ Module Sign.
 End Sign.
 
 (* pub fn i256_sign(val: &U256) -> Sign *)
-Instance run_i256_sign (val : Ref.t Pointer.Kind.Ref U256.t) :
+Instance run_i256_sign (val : Ref.t Pointer.Kind.Ref aliases.U256.t) :
   Run.Trait instructions.i256.i256_sign [] [] [ φ val ] Sign.t.
 Proof.
   constructor.
@@ -79,7 +79,7 @@ Proof.
 Admitted.
 
 (* pub fn i256_sign_compl(val: &mut U256) -> Sign *)
-Instance run_i256_sign_compl (val : Ref.t Pointer.Kind.MutRef U256.t) :
+Instance run_i256_sign_compl (val : Ref.t Pointer.Kind.MutRef aliases.U256.t) :
   Run.Trait instructions.i256.i256_sign_compl [] [] [ φ val ] Sign.t.
 Proof.
   constructor.
@@ -87,7 +87,7 @@ Proof.
 Admitted.
 
 (* pub fn u256_remove_sign(val: &mut U256) *)
-Instance run_u256_remove_sign (val : Ref.t Pointer.Kind.MutRef U256.t) :
+Instance run_u256_remove_sign (val : Ref.t Pointer.Kind.MutRef aliases.U256.t) :
   Run.Trait instructions.i256.u256_remove_sign [] [] [ φ val ] unit.
 Proof.
   constructor.
@@ -95,7 +95,7 @@ Proof.
 Admitted.
 
 (* pub fn two_compl_mut(op: &mut U256) *)
-Instance run_two_compl_mut (op : Ref.t Pointer.Kind.MutRef U256.t) :
+Instance run_two_compl_mut (op : Ref.t Pointer.Kind.MutRef aliases.U256.t) :
   Run.Trait instructions.i256.two_compl_mut [] [] [ φ op ] unit.
 Proof.
   constructor.
@@ -104,7 +104,7 @@ Admitted.
 
 
 (* pub fn i256_cmp(first: &U256, second: &U256) -> Ordering *)
-Instance run_i256_cmp (first second : U256.t) :
+Instance run_i256_cmp (first second : aliases.U256.t) :
   Run.Trait instructions.i256.i256_cmp [] [] [ φ first; φ second ] Ordering.t.
 Proof.
   constructor.
@@ -112,16 +112,16 @@ Proof.
 Admitted.
 
 (* pub fn i256_div(mut first: U256, mut second: U256) -> U256 *)
-Instance run_i256_div (first second : U256.t) :
-  Run.Trait instructions.i256.i256_div [] [] [ φ first; φ second ] U256.t.
+Instance run_i256_div (first second : aliases.U256.t) :
+  Run.Trait instructions.i256.i256_div [] [] [ φ first; φ second ] aliases.U256.t.
 Proof.
   constructor.
   run_symbolic.
 Admitted.
 
 (* pub fn i256_mod(mut first: U256, mut second: U256) -> U256 *)
-Instance run_i256_mod (first second : U256.t) :
-  Run.Trait instructions.i256.i256_mod [] [] [ φ first; φ second ] U256.t.
+Instance run_i256_mod (first second : aliases.U256.t) :
+  Run.Trait instructions.i256.i256_mod [] [] [ φ first; φ second ] aliases.U256.t.
 Proof.
   constructor.
   run_symbolic.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/memory.v b/CoqOfRust/revm/revm_interpreter/instructions/links/memory.v
index a9ae875b4..3b754eb50 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/memory.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/memory.v
@@ -1,7 +1,6 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import core.links.cmp.
-Require Import revm.links.dependencies.
 Require Import revm.revm_interpreter.instructions.memory.
 Require Import revm.revm_interpreter.links.interpreter.
 Require Import revm.revm_interpreter.links.interpreter_types.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/stack.v b/CoqOfRust/revm/revm_interpreter/instructions/links/stack.v
index 0efe85d31..cd770e5fe 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/stack.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/stack.v
@@ -1,7 +1,6 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import core.links.cmp.
-Require Import revm.links.dependencies.
 Require Import revm.revm_interpreter.instructions.links.utility.
 Require Import revm.revm_interpreter.instructions.stack.
 Require Import revm.revm_interpreter.links.gas.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/system.v b/CoqOfRust/revm/revm_interpreter/instructions/links/system.v
index b00d83d0e..ecb0bfbf1 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/system.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/system.v
@@ -1,9 +1,11 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
+Require Import alloy_primitives.links.aliases.
+Require Import alloy_primitives.bits.links.fixed.
+Require Import alloy_primitives.utils.links.mod.
 Require Import core.links.cmp.
 Require Import core.num.links.mod.
 Require Import core.slice.links.mod.
-Require Import revm.links.dependencies.
 Require Import revm.revm_interpreter.gas.links.calc.
 Require Import revm.revm_interpreter.instructions.system.
 Require Import revm.revm_interpreter.interpreter.links.shared_memory.
@@ -212,7 +214,7 @@ Instance run_memory_resize
   {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 : U256.t)
+  (memory_offset : aliases.U256.t)
   (len : Usize.t) :
   Run.Trait
     instructions.system.memory_resize [] [ Φ WIRE ] [ φ interpreter; φ memory_offset; φ len ]
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/tx_info.v b/CoqOfRust/revm/revm_interpreter/instructions/links/tx_info.v
index 3e94a9b87..dd8296fb5 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/tx_info.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/tx_info.v
@@ -1,7 +1,6 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import core.links.cmp.
-Require Import revm.links.dependencies.
 Require Import revm.revm_interpreter.instructions.tx_info.
 Require Import revm.revm_interpreter.links.interpreter.
 Require Import revm.revm_interpreter.links.interpreter_types.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/utility.v b/CoqOfRust/revm/revm_interpreter/instructions/links/utility.v
index 255197af2..f36aef146 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/links/utility.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/links/utility.v
@@ -1,8 +1,10 @@
 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 alloy_primitives.links.aliases.
 Require Import core.convert.links.mod.
 Require Import revm.revm_interpreter.instructions.utility.
-Require Import revm.links.dependencies.
 Require Import ruint.links.bytes.
 
 Import bytes.Impl_Uint.
@@ -10,7 +12,7 @@ Import bytes.Impl_Uint.
 (* pub fn cast_slice_to_u256(slice: &[u8], dest: &mut U256) *)
 Instance run_cast_slice_to_u256
   (slice : Ref.t Pointer.Kind.Ref (list U8.t))
-  (dest : Ref.t Pointer.Kind.MutRef U256.t) :
+  (dest : Ref.t Pointer.Kind.MutRef aliases.U256.t) :
   Run.Trait instructions.utility.cast_slice_to_u256 [] [] [ φ slice; φ dest ] unit.
 Proof.
   constructor.
@@ -29,7 +31,7 @@ Module IntoU256.
   Definition Run_into_u256 (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "into_u256" (fun method =>
       forall (self : Self),
-      Run.Trait method [] [] [ φ self ] U256.t
+      Run.Trait method [] [] [ φ self ] aliases.U256.t
     ).
 
   Class Run (Self : Set) `{Link Self} : Set := {
@@ -40,7 +42,7 @@ End IntoU256.
 (* impl IntoU256 for B256 { *)
 Module Impl_IntoU256_for_B256.
   Definition Self : Set :=
-    B256.t.
+    aliases.B256.t.
 
   (* fn into_u256(self) -> U256 *)
   Definition run_into_u256 : IntoU256.Run_into_u256 Self.
@@ -65,7 +67,7 @@ End Impl_IntoU256_for_B256.
 (* impl IntoU256 for Address { *)
 Module Impl_IntoU256_for_Address.
   Definition Self : Set :=
-    alloy_primitives.bits.links.address.Address.t.
+    Address.t.
 
   (* fn into_u256(self) -> U256 *)
   Definition run_into_u256 : IntoU256.Run_into_u256 Self.
@@ -78,8 +80,7 @@ Module Impl_IntoU256_for_Address.
     { intros.
       constructor.
       destruct Impl_IntoU256_for_B256.run.
-      run_symbolic.
-      admit.
+      run_symbolic; admit.
     }
   Admitted.
 
@@ -100,7 +101,7 @@ Module IntoAddress.
   Definition Run_into_address (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "into_address" (fun method =>
       forall (self : Self),
-      Run.Trait method [] [] [ φ self ] alloy_primitives.bits.links.address.Address.t
+      Run.Trait method [] [] [ φ self ] Address.t
     ).
 
   Class Run (Self : Set) `{Link Self} : Set := {
@@ -111,7 +112,7 @@ End IntoAddress.
 (* impl IntoAddress for U256 { *)
 Module Impl_IntoAddress_for_U256.
   Definition Self : Set :=
-    U256.t.
+    aliases.U256.t.
 
   (* fn into_address(self) -> Address *)
   Definition run_into_address : IntoAddress.Run_into_address Self.
@@ -123,12 +124,10 @@ Module Impl_IntoAddress_for_U256.
     }
     { intros.
       constructor.
-      destruct (
-        alloy_primitives.bits.links.fixed.Impl_From_for_FixedBytes.run {| Integer.value := 32 |}
-      ).
       run_symbolic.
+      admit.
     }
-  Defined.
+  Admitted.
 
   Instance run : IntoAddress.Run Self := {
     IntoAddress.into_address := run_into_address;
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/simulations/arithmetic.v b/CoqOfRust/revm/revm_interpreter/instructions/simulations/arithmetic.v
index 310238a86..950700cc4 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/simulations/arithmetic.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/simulations/arithmetic.v
@@ -2,7 +2,7 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import CoqOfRust.simulations.M.
 Import simulations.M.Notations.
-Require Import revm.links.dependencies.
+
 (*
 Require Import revm.interpreter.links.interpreter.
 Require Import revm.interpreter.interpreter.links.instruction_result.
diff --git a/CoqOfRust/revm/revm_interpreter/instructions/simulations/macros.v b/CoqOfRust/revm/revm_interpreter/instructions/simulations/macros.v
index 18c377fed..cda515b6f 100644
--- a/CoqOfRust/revm/revm_interpreter/instructions/simulations/macros.v
+++ b/CoqOfRust/revm/revm_interpreter/instructions/simulations/macros.v
@@ -2,7 +2,6 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import CoqOfRust.simulations.M.
 Import simulations.M.Notations.
-Require Import revm.links.dependencies.
 (*Require Import revm.interpreter.links.interpreter.
 Require Import revm.interpreter.interpreter.links.gas.
 Require Import revm.interpreter.interpreter.links.stack.
diff --git a/CoqOfRust/revm/revm_interpreter/interpreter/links/stack.v b/CoqOfRust/revm/revm_interpreter/interpreter/links/stack.v
index b65e90766..92d271392 100644
--- a/CoqOfRust/revm/revm_interpreter/interpreter/links/stack.v
+++ b/CoqOfRust/revm/revm_interpreter/interpreter/links/stack.v
@@ -2,6 +2,7 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import alloc.links.alloc.
 Require Import alloc.vec.links.mod.
+Require Import alloy_primitives.links.aliases.
 Require Import core.links.array.
 Require Import core.links.hint.
 Require Import core.links.option.
@@ -9,7 +10,6 @@ Require Import core.links.panicking.
 Require Import core.links.result.
 Require Import core.slice.links.index.
 Require Import core.slice.links.mod.
-Require Import revm.links.dependencies.
 Require Import revm.revm_interpreter.interpreter.stack.
 Require Import revm.revm_interpreter.links.instruction_result.
 Require Import ruint.links.lib.
@@ -27,7 +27,7 @@ Import Impl_Vec_T_A.
 *)
 Module Stack.
   Record t : Set := {
-    data : Vec.t U256.t Global.t;
+    data : Vec.t aliases.U256.t Global.t;
   }.
 
   Global Instance IsLink : Link t := {
@@ -41,7 +41,7 @@ Module Stack.
   Smpl Add apply of_ty : of_ty.
 
   Lemma of_value_with
-      (data : Vec.t U256.t Global.t) data' :
+      (data : Vec.t aliases.U256.t Global.t) data' :
     data' = φ data ->
     Value.StructRecord "revm_interpreter::interpreter::stack::Stack" [
       ("data", data')
@@ -49,7 +49,7 @@ Module Stack.
   Proof. now intros; subst. Qed.
   Smpl Add apply of_value_with : of_value.
 
-  Definition of_value (data : Vec.t U256.t Global.t) data' :
+  Definition of_value (data : Vec.t aliases.U256.t Global.t) data' :
     data' = φ data ->
     OfValue.t (Value.StructRecord "revm_interpreter::interpreter::stack::Stack" [
       ("data", data')
@@ -122,7 +122,7 @@ Module Impl_Stack.
   Instance run_data (self : Ref.t Pointer.Kind.Ref Self) :
     Run.Trait
       interpreter.stack.Impl_revm_interpreter_interpreter_stack_Stack.data [] [] [φ self]
-      (Ref.t Pointer.Kind.Ref (Vec.t U256.t Global.t)).
+      (Ref.t Pointer.Kind.Ref (Vec.t aliases.U256.t Global.t)).
   Proof.
     constructor.
     run_symbolic.
@@ -132,7 +132,7 @@ Module Impl_Stack.
   Instance run_data_mut (self : Ref.t Pointer.Kind.MutRef Self) :
     Run.Trait
       interpreter.stack.Impl_revm_interpreter_interpreter_stack_Stack.data_mut [] [] [φ self]
-      (Ref.t Pointer.Kind.MutRef (Vec.t U256.t Global.t)).
+      (Ref.t Pointer.Kind.MutRef (Vec.t aliases.U256.t Global.t)).
   Proof.
     constructor.
     run_symbolic.
@@ -142,7 +142,7 @@ Module Impl_Stack.
   Instance run_into_data (self : Self) :
     Run.Trait
       interpreter.stack.Impl_revm_interpreter_interpreter_stack_Stack.into_data [] [] [φ self]
-      (Vec.t U256.t Global.t).
+      (Vec.t aliases.U256.t Global.t).
   Proof.
     constructor.
     run_symbolic.
@@ -152,7 +152,7 @@ Module Impl_Stack.
   Instance run_pop (self : Ref.t Pointer.Kind.MutRef Self) :
     Run.Trait
       interpreter.stack.Impl_revm_interpreter_interpreter_stack_Stack.pop [] [] [φ self]
-      (Result.t U256.t InstructionResult.t).
+      (Result.t aliases.U256.t InstructionResult.t).
   Proof.
     constructor.
     run_symbolic.
@@ -162,7 +162,7 @@ Module Impl_Stack.
   Instance run_pop_unsafe (self : Ref.t Pointer.Kind.MutRef Self) :
     Run.Trait
       interpreter.stack.Impl_revm_interpreter_interpreter_stack_Stack.pop_unsafe [] [] [φ self]
-      U256.t.
+      aliases.U256.t.
   Proof.
     constructor.
     run_symbolic.
@@ -172,10 +172,10 @@ Module Impl_Stack.
   Instance run_top_unsafe (self : Ref.t Pointer.Kind.MutRef Self) :
     Run.Trait
       interpreter.stack.Impl_revm_interpreter_interpreter_stack_Stack.top_unsafe [] [] [φ self]
-      (Ref.t Pointer.Kind.MutRef U256.t).
+      (Ref.t Pointer.Kind.MutRef aliases.U256.t).
   Proof.
     constructor.
-    destruct (Impl_DerefMut_for_Vec.run (T := U256.t) (A := Global.t)).
+    destruct (Impl_DerefMut_for_Vec.run (T := aliases.U256.t) (A := Global.t)).
     run_symbolic.
   Defined.
 
@@ -183,7 +183,7 @@ Module Impl_Stack.
   Instance run_popn (N : Usize.t) (self : Ref.t Pointer.Kind.MutRef Self) :
     Run.Trait
       interpreter.stack.Impl_revm_interpreter_interpreter_stack_Stack.popn [φ N] [] [φ self]
-      (array.t U256.t N).
+      (array.t aliases.U256.t N).
   Proof.
     constructor.
     assert (H_N_eq :
@@ -211,14 +211,14 @@ Module Impl_Stack.
   Instance run_popn_top (self : Ref.t Pointer.Kind.MutRef Self) (POPN : Usize.t) :
     Run.Trait
       interpreter.stack.Impl_revm_interpreter_interpreter_stack_Stack.popn_top [φ POPN] [] [φ self]
-      (array.t U256.t POPN * Ref.t Pointer.Kind.MutRef U256.t).
+      (array.t aliases.U256.t POPN * Ref.t Pointer.Kind.MutRef aliases.U256.t).
   Proof.
     constructor.
     run_symbolic.
   Defined.
 
   (* pub fn push(&mut self, value: U256) -> bool *)
-  Instance run_push (self : Ref.t Pointer.Kind.MutRef Self) (value : U256.t) :
+  Instance run_push (self : Ref.t Pointer.Kind.MutRef Self) (value : aliases.U256.t) :
     Run.Trait
       interpreter.stack.Impl_revm_interpreter_interpreter_stack_Stack.push [] [] [φ self; φ value]
       bool.
@@ -232,10 +232,10 @@ Module Impl_Stack.
     Run.Trait
       interpreter.stack.Impl_revm_interpreter_interpreter_stack_Stack.peek
         [] [] [φ self; φ no_from_top]
-      (Result.t U256.t InstructionResult.t).
+      (Result.t aliases.U256.t InstructionResult.t).
   Proof.
     constructor.
-    destruct (Impl_Index_for_Vec_T_A.run U256.t Usize.t Global.t U256.t).
+    destruct (Impl_Index_for_Vec_T_A.run aliases.U256.t Usize.t Global.t aliases.U256.t).
     run_symbolic.
   Admitted.
 
@@ -286,7 +286,7 @@ Module Impl_Stack.
   Instance run_set
       (self : Ref.t Pointer.Kind.MutRef Self)
       (no_from_top : Usize.t)
-      (val : U256.t) :
+      (val : aliases.U256.t) :
     Run.Trait
       interpreter.stack.Impl_revm_interpreter_interpreter_stack_Stack.set
         [] [] [φ self; φ no_from_top; φ val]
diff --git a/CoqOfRust/revm/revm_interpreter/interpreter/simulations/stack.v b/CoqOfRust/revm/revm_interpreter/interpreter/simulations/stack.v
index 95afdfb7b..8d4dfd189 100644
--- a/CoqOfRust/revm/revm_interpreter/interpreter/simulations/stack.v
+++ b/CoqOfRust/revm/revm_interpreter/interpreter/simulations/stack.v
@@ -3,7 +3,6 @@ Require Import CoqOfRust.links.M.
 Require Import CoqOfRust.simulations.M.
 Import simulations.M.Notations.
 Require Import core.links.array.
-Require Import revm.links.dependencies.
 Require Import revm_interpreter.interpreter.links.stack.
 
 (*
diff --git a/CoqOfRust/revm/revm_interpreter/interpreter_action/links/call_inputs.v b/CoqOfRust/revm/revm_interpreter/interpreter_action/links/call_inputs.v
index 557f5c064..6517f720e 100644
--- a/CoqOfRust/revm/revm_interpreter/interpreter_action/links/call_inputs.v
+++ b/CoqOfRust/revm/revm_interpreter/interpreter_action/links/call_inputs.v
@@ -1,6 +1,8 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import CoqOfRust.revm.links.dependencies.
+Require Import alloy_primitives.bits.links.address.
+Require Import alloy_primitives.bytes.links.mod.
+Require Import alloy_primitives.links.aliases.
 
 (*
   /// Call value.
@@ -18,8 +20,8 @@ Require Import CoqOfRust.revm.links.dependencies.
 
 Module CallValue.
   Inductive t : Set :=
-  | Transfer : U256.t -> t
-  | Apparent : U256.t -> t.
+  | Transfer : aliases.U256.t -> t
+  | Apparent : aliases.U256.t -> t.
 
   Global Instance IsLink : Link t := {
     Φ := Ty.path "revm_interpreter::interpreter_action::call_inputs::CallValue";
@@ -111,12 +113,12 @@ End CallScheme.
 (* TODO: Ranges? *)
 Module CallInputs.
   Record t : Set := {
-    input : alloy_primitives.links.bytes_.Bytes.t;
+    input : Bytes.t;
     return_memory_offset : Usize.t * Usize.t;
     gas_limit : U64.t;
-    bytecode_address : alloy_primitives.bits.links.address.Address.t;
-    target_address : alloy_primitives.bits.links.address.Address.t;
-    caller : alloy_primitives.bits.links.address.Address.t;
+    bytecode_address : Address.t;
+    target_address : Address.t;
+    caller : Address.t;
     value : CallValue.t;
     scheme : CallScheme.t;
     is_static : bool;
diff --git a/CoqOfRust/revm/revm_interpreter/interpreter_action/links/create_inputs.v b/CoqOfRust/revm/revm_interpreter/interpreter_action/links/create_inputs.v
index ffb2327af..0a4674a1d 100644
--- a/CoqOfRust/revm/revm_interpreter/interpreter_action/links/create_inputs.v
+++ b/CoqOfRust/revm/revm_interpreter/interpreter_action/links/create_inputs.v
@@ -1,32 +1,26 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import revm.links.dependencies.
+Require Import alloy_primitives.bits.links.address.
+Require Import alloy_primitives.bytes.links.mod.
+Require Import alloy_primitives.links.aliases.
 Require Import revm_context_interface.links.cfg.
 
 (*
-  /// Inputs for a create call.
-  #[derive(Clone, Debug, PartialEq, Eq, Hash)]
-  #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
   pub struct CreateInputs {
-      /// Caller address of the EVM.
       pub caller: Address,
-      /// The create scheme.
       pub scheme: CreateScheme,
-      /// The value to transfer.
       pub value: U256,
-      /// The init code of the contract.
       pub init_code: Bytes,
-      /// The gas limit of the call.
       pub gas_limit: u64,
   }
 *)
 
 Module CreateInputs.
   Record t : Set := {
-    caller : alloy_primitives.bits.links.address.Address.t;
+    caller : Address.t;
     scheme : CreateScheme.t;
-    value : U256.t;
-    init_code : alloy_primitives.links.bytes_.Bytes.t;
+    value : aliases.U256.t;
+    init_code : Bytes.t;
     gas_limit : U64.t;
   }.
 
diff --git a/CoqOfRust/revm/revm_interpreter/interpreter_action/links/eof_create_inputs.v b/CoqOfRust/revm/revm_interpreter/interpreter_action/links/eof_create_inputs.v
index 097cba34a..139b42b11 100644
--- a/CoqOfRust/revm/revm_interpreter/interpreter_action/links/eof_create_inputs.v
+++ b/CoqOfRust/revm/revm_interpreter/interpreter_action/links/eof_create_inputs.v
@@ -1,16 +1,18 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
-Require Import revm.links.dependencies.
-Require revm.revm_bytecode.links.eof.
+Require Import alloy_primitives.bits.links.address.
+Require Import alloy_primitives.bytes.links.mod.
+Require Import alloy_primitives.links.aliases.
+Require Import revm.revm_bytecode.links.eof.
 
 Module EOFCreateKind.
   Inductive t : Set :=
   | Tx
-    (initdata : alloy_primitives.links.bytes_.Bytes.t)
+    (initdata : Bytes.t)
   | Opcode
     (initcode : revm_bytecode.links.eof.Eof.t)
-    (input : alloy_primitives.links.bytes_.Bytes.t)
-    (created_address : alloy_primitives.bits.links.address.Address.t)
+    (input : Bytes.t)
+    (created_address : Address.t)
   .
 
   Global Instance IsLink : Link t := {
@@ -33,10 +35,10 @@ End EOFCreateKind.
 
 Module EOFCreateInputs.
   Record t : Set := {
-    caller: alloy_primitives.bits.links.address.Address.t;
-    value: U256.t;
+    caller: Address.t;
+    value: aliases.U256.t;
     gas_limit: U64.t;
-    kind: revm_interpreter.interpreter_action.links.eof_create_inputs.EOFCreateKind.t;
+    kind: EOFCreateKind.t;
   }.
 
   Global Instance IsLink : Link t := {
diff --git a/CoqOfRust/revm/revm_interpreter/links/interpreter.v b/CoqOfRust/revm/revm_interpreter/links/interpreter.v
index 5da45d70a..2c20756e0 100644
--- a/CoqOfRust/revm/revm_interpreter/links/interpreter.v
+++ b/CoqOfRust/revm/revm_interpreter/links/interpreter.v
@@ -1,6 +1,6 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import revm.links.dependencies.
+Require Import alloy_primitives.bytes.links.mod.
 Require Import revm_interpreter.interpreter.links.shared_memory.
 Require Import revm_interpreter.interpreter.links.stack.
 Require Import revm_interpreter.links.gas.
@@ -12,6 +12,8 @@ Require Import revm_interpreter.interpreter.
 
 Require Export revm.revm_interpreter.links.interpreter_Interpreter.
 
+Import Impl_Bytes.
+
 (* impl<IW: InterpreterTypes> Interpreter<IW> { *)
 Module Impl_Interpreter.
   Import Impl_InstructionResult.
diff --git a/CoqOfRust/revm/revm_interpreter/links/interpreter_Interpreter.v b/CoqOfRust/revm/revm_interpreter/links/interpreter_Interpreter.v
index 3deff69ca..e3b609ffa 100644
--- a/CoqOfRust/revm/revm_interpreter/links/interpreter_Interpreter.v
+++ b/CoqOfRust/revm/revm_interpreter/links/interpreter_Interpreter.v
@@ -1,6 +1,5 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import revm.links.dependencies.
 Require Import revm_interpreter.interpreter.links.shared_memory.
 Require Import revm_interpreter.interpreter.links.stack.
 Require Import revm_interpreter.links.gas.
diff --git a/CoqOfRust/revm/revm_interpreter/links/interpreter_InterpreterResult.v b/CoqOfRust/revm/revm_interpreter/links/interpreter_InterpreterResult.v
index 8754fadcb..39abc2802 100644
--- a/CoqOfRust/revm/revm_interpreter/links/interpreter_InterpreterResult.v
+++ b/CoqOfRust/revm/revm_interpreter/links/interpreter_InterpreterResult.v
@@ -1,13 +1,13 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require Import revm.links.dependencies.
+Require Import alloy_primitives.bytes.links.mod.
 Require Import revm.revm_interpreter.links.instruction_result.
 Require Import revm_interpreter.links.gas.
 
 Module InterpreterResult.
   Record t : Set := {
     result: InstructionResult.t;
-    output: alloy_primitives.links.bytes_.Bytes.t;
+    output: Bytes.t;
     gas: Gas.t;
   }.
 
@@ -43,7 +43,7 @@ Module InterpreterResult.
 
   Definition of_value
       (result : InstructionResult.t) result'
-      (output : alloy_primitives.links.bytes_.Bytes.t) output'
+      (output : Bytes.t) output'
       (gas : Gas.t) gas' :
     result' = φ result ->
     output' = φ output ->
diff --git a/CoqOfRust/revm/revm_interpreter/links/interpreter_action.v b/CoqOfRust/revm/revm_interpreter/links/interpreter_action.v
index cbf183607..368779be9 100644
--- a/CoqOfRust/revm/revm_interpreter/links/interpreter_action.v
+++ b/CoqOfRust/revm/revm_interpreter/links/interpreter_action.v
@@ -1,7 +1,6 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require alloc.links.boxed.
-Require Import revm.links.dependencies.
+Require Import alloc.links.boxed.
 Require Import revm.revm_interpreter.interpreter_action.links.call_inputs.
 Require Import revm.revm_interpreter.interpreter_action.links.create_inputs.
 Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs.
diff --git a/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v b/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v
index 4e72416b7..3508ca57b 100644
--- a/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v
+++ b/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v
@@ -1,8 +1,11 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
-Require core.links.array.
-Require core.ops.links.deref.
-Require core.ops.links.range.
+Require Import alloy_primitives.bits.links.address.
+Require Import alloy_primitives.bytes.links.mod.
+Require Import alloy_primitives.links.aliases.
+Require Import core.links.array.
+Require Import core.ops.links.deref.
+Require Import core.ops.links.range.
 Require Import core.links.option.
 Require Import revm.revm_bytecode.eof.links.types_section.
 Require Import revm.revm_interpreter.links.gas.
@@ -10,7 +13,6 @@ Require Import revm.revm_interpreter.links.instruction_result.
 Require Import revm.revm_interpreter.links.interpreter_action.
 Require Import revm.revm_interpreter.interpreter_types.
 Require Import revm.revm_specification.links.hardfork.
-Require Import revm.links.dependencies.
 
 (*
 pub trait StackTrait {
@@ -45,39 +47,39 @@ Module StackTrait.
 
   Definition Run_push (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "push" (fun method =>
-      forall (self : Ref.t Pointer.Kind.MutRef Self) (value : U256.t),
+      forall (self : Ref.t Pointer.Kind.MutRef Self) (value : aliases.U256.t),
       Run.Trait method [] [] [ φ self; φ value ] bool
     ).
 
   Definition Run_push_b256 (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "push_b256" (fun method =>
-      forall (self : Ref.t Pointer.Kind.MutRef Self) (value : B256.t),
+      forall (self : Ref.t Pointer.Kind.MutRef Self) (value : aliases.B256.t),
       Run.Trait method [] [] [ φ self; φ value ] bool
     ).
 
   Definition Run_popn (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "popn" (fun method =>
       forall (N : Usize.t) (self : Ref.t Pointer.Kind.MutRef Self),
-      Run.Trait method [ φ N ] [] [ φ self ] (option (array.t U256.t N))
+      Run.Trait method [ φ N ] [] [ φ self ] (option (array.t aliases.U256.t N))
     ).
 
   Definition Run_popn_top (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "popn_top" (fun method =>
       forall (POPN : Usize.t) (self : Ref.t Pointer.Kind.MutRef Self),
       Run.Trait method [ φ POPN ] [] [ φ self ]
-        (option (array.t U256.t POPN * Ref.t Pointer.Kind.MutRef U256.t))
+        (option (array.t aliases.U256.t POPN * Ref.t Pointer.Kind.MutRef aliases.U256.t))
     ).
 
   Definition Run_top (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "top" (fun method =>
       forall (self : Ref.t Pointer.Kind.MutRef Self),
-      Run.Trait method [] [ Φ U256.t ] [ φ self ] (option (Ref.t Pointer.Kind.MutRef U256.t))
+      Run.Trait method [] [ Φ aliases.U256.t ] [ φ self ] (option (Ref.t Pointer.Kind.MutRef aliases.U256.t))
     ).
 
   Definition Run_pop (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "pop" (fun method =>
       forall (self : Ref.t Pointer.Kind.MutRef Self),
-      Run.Trait method [] [ Φ U256.t ] [ φ self ] (option U256.t)
+      Run.Trait method [] [ Φ aliases.U256.t ] [ φ self ] (option aliases.U256.t)
     ).
 
   Definition Run_pop_address (Self : Set) `{Link Self} : Set :=
@@ -490,7 +492,7 @@ Module InputsTrait.
   Definition Run_call_value (Self : Set) `{Link Self} : Set :=
     TraitMethod.C (trait Self) "call_value" (fun method =>
       forall (self : Ref.t Pointer.Kind.Ref Self),
-      Run.Trait method [] [] [ φ self ] U256.t
+      Run.Trait method [] [] [ φ self ] aliases.U256.t
     ).
 
   Class Run (Self : Set) `{Link Self} : Set := {
diff --git a/CoqOfRust/revm/simulations/dependencies.v b/CoqOfRust/revm/simulations/dependencies.v
deleted file mode 100644
index e3e1e1bad..000000000
--- a/CoqOfRust/revm/simulations/dependencies.v
+++ /dev/null
@@ -1,63 +0,0 @@
-Require Import CoqOfRust.CoqOfRust.
-Require Import CoqOfRust.revm.links.dependencies.
-
-(*Module U256.
-  Import links.dependencies.U256.
-
-  Definition limb_size : Z := 64.
-
-  Definition BITS : Z := 256.
-  Definition LIMBS : Z := 4.
-
-  Definition ZERO : t := 0.
-  Definition from : Z -> t := id.
-
-  Definition u64_try_from (a : t) : option Z :=
-    if a <? 2 ^ BITS
-    then Some a
-    else None.
-
-  Definition eq : t -> t -> bool := Z.eqb.
-  Definition lt : t -> t -> bool := Z.ltb.
-  Definition gt : t -> t -> bool := Z.gtb.
-  Definition le : t -> t -> bool := Z.leb.
-  Definition ge : t -> t -> bool := Z.geb.
-
-  Definition wrapping_add (a b : t) : t := (a + b) mod size.
-  Definition wrapping_sub (a b : t) : t := (a - b) mod size.
-  Definition wrapping_mul (a b : t) : t := (a * b) mod size.
-  Definition wrapping_div (a b : t) : t := (Z.quot a b) mod size.
-  Definition wrapping_rem (a b : t) : t := (Z.rem a b) mod size.
-  Definition wrapping_pow (a b : t) : t := (Z.pow a b) mod size.
-
-  Definition log2floor : t -> Z := Z.log2.
-
-  Definition add_mod (a b m : t) : t := ((a + b) mod m) mod size.
-  Definition mul_mod (a b m : t) : t := ((a * b) mod m) mod size.
-
-  Definition checked_add (a b : t) : option t :=
-    let r := (a + b)%Z in
-    if r <? 2 ^ BITS
-    then Some r
-    else None.
-  
-  Definition checked_mul (a b : t) : option t :=
-    let r := (a * b)%Z in
-    if r <? 2 ^ BITS
-    then Some r
-    else None.
-
-  (* bit operations *)
-  Definition bit : t -> Z -> bool := Z.testbit.
-  Definition not : t -> t := Z.lnot.
-  Definition and : t -> t -> t := Z.land.
-  Definition or  : t -> t -> t := Z.lor.
-  Definition shl : t -> Z -> t := Z.shiftl.
-  Definition shr : t -> Z -> t := Z.shiftr.    
-
-  Definition as_limbs (a : t) : list Z :=
-    List.map
-      (fun n => (Z.shiftr a (limb_size * Z.of_nat n)) mod (2 ^ limb_size))
-      (List.seq 0 (Z.to_nat LIMBS)).
-End U256.
-*)