revm: add links for alloy and remove the dependencies file

.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

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.

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.

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.