From 5286bdbe301c2e7dc63819a02ea83509a6f709c0 Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Mon, 17 Feb 2025 15:49:56 -0300
Subject: [PATCH 01/14] Starting links by identity

---
 CoqOfRust/revm/revm_precompile/links/identity.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 CoqOfRust/revm/revm_precompile/links/identity.v

diff --git a/CoqOfRust/revm/revm_precompile/links/identity.v b/CoqOfRust/revm/revm_precompile/links/identity.v
new file mode 100644
index 000000000..31b21f9be
--- /dev/null
+++ b/CoqOfRust/revm/revm_precompile/links/identity.v
@@ -0,0 +1,17 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.lib.
+Require Import CoqOfRust.links.M.
+Require core.links.default.
+Require Import revm_precompile.identity.
+
+Import Run.
+(*
+pub const IDENTITY_BASE: u64 = 15;
+*)
+
+Definition BASE_eq : M.get_constant "revm_precompile::identity::IDENTITY_BASE" =
+  φ (Ref.immediate Pointer.Kind.Raw (Integer.Build_t IntegerKind.U64 15)).
+Proof.
+  repeat (autorewrite with constant_rewrites || cbn).
+  reflexivity.
+Defined.

From 8c37e06254b5b569d5a2433e025fe008a7ba2707 Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Tue, 18 Feb 2025 14:18:53 -0300
Subject: [PATCH 02/14] Adding proofs

---
 CoqOfRust/revm/revm_precompile/links/identity.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/CoqOfRust/revm/revm_precompile/links/identity.v b/CoqOfRust/revm/revm_precompile/links/identity.v
index 31b21f9be..0f6b2a0b8 100644
--- a/CoqOfRust/revm/revm_precompile/links/identity.v
+++ b/CoqOfRust/revm/revm_precompile/links/identity.v
@@ -15,3 +15,13 @@ Proof.
   repeat (autorewrite with constant_rewrites || cbn).
   reflexivity.
 Defined.
+
+Definition IDENTITY_PER_WORD_eq : M.get_constant "revm_precompile::identity::IDENTITY_PER_WORD" =
+  φ (Ref.immediate Pointer.Kind.Raw (Integer.Build_t IntegerKind.U64 3)).
+Proof.
+  repeat (autorewrite with constant_rewrites || cbn).
+  reflexivity.
+Defined.
+
+
+

From 078fc41b1e2343a23ffa811aca076038ed72313f Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Sat, 22 Feb 2025 15:16:04 -0300
Subject: [PATCH 03/14] Defining link for PrecompileOutput

---
 .../revm/revm_precompile/links/identity.v     | 38 +++++++++++++------
 .../revm/revm_precompile/links/interface.v    | 38 +++++++++++++++++++
 2 files changed, 64 insertions(+), 12 deletions(-)
 create mode 100644 CoqOfRust/revm/revm_precompile/links/interface.v

diff --git a/CoqOfRust/revm/revm_precompile/links/identity.v b/CoqOfRust/revm/revm_precompile/links/identity.v
index 0f6b2a0b8..79f74b8ee 100644
--- a/CoqOfRust/revm/revm_precompile/links/identity.v
+++ b/CoqOfRust/revm/revm_precompile/links/identity.v
@@ -9,19 +9,33 @@ Import Run.
 pub const IDENTITY_BASE: u64 = 15;
 *)
 
-Definition BASE_eq : M.get_constant "revm_precompile::identity::IDENTITY_BASE" =
-  φ (Ref.immediate Pointer.Kind.Raw (Integer.Build_t IntegerKind.U64 15)).
-Proof.
-  repeat (autorewrite with constant_rewrites || cbn).
-  reflexivity.
-Defined.
+Module identity.
 
-Definition IDENTITY_PER_WORD_eq : M.get_constant "revm_precompile::identity::IDENTITY_PER_WORD" =
-  φ (Ref.immediate Pointer.Kind.Raw (Integer.Build_t IntegerKind.U64 3)).
-Proof.
-  repeat (autorewrite with constant_rewrites || cbn).
-  reflexivity.
-Defined.
+  Definition BASE_eq : M.get_constant "revm_precompile::identity::IDENTITY_BASE" =
+    φ (Ref.immediate Pointer.Kind.Raw (Integer.Build_t IntegerKind.U64 15)).
+  Proof.
+    repeat (autorewrite with constant_rewrites || cbn).
+    reflexivity.
+  Defined.
 
+  Definition IDENTITY_PER_WORD_eq : M.get_constant "revm_precompile::identity::IDENTITY_PER_WORD" =
+    φ (Ref.immediate Pointer.Kind.Raw (Integer.Build_t IntegerKind.U64 3)).
+  Proof.
+    repeat (autorewrite with constant_rewrites || cbn).
+    reflexivity.
+  Defined.
+  
+  
+  
+  (* 
+  Definition FUN_eq : M.get_constant "revm_precompile::identity::FUN" = 
+  (Value.Error "unexpected closure call").
+  Proof.
+    autorewrite with constant_rewrites.
+    reflexivity.
+  Defined.
+  *)
+
+End identity.
 
 
diff --git a/CoqOfRust/revm/revm_precompile/links/interface.v b/CoqOfRust/revm/revm_precompile/links/interface.v
new file mode 100644
index 000000000..55b86f21e
--- /dev/null
+++ b/CoqOfRust/revm/revm_precompile/links/interface.v
@@ -0,0 +1,38 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.lib.
+Require Import CoqOfRust.links.M.
+Require core.links.default.
+Require revm.links.dependencies.
+Import revm.links.dependencies.alloy_primitives.links.bytes_.
+Require Import revm_precompile.interface.
+
+Import Run.
+
+
+(* 
+    pub struct PrecompileOutput {
+        /// Gas used by the precompile
+        pub gas_used: u64,
+        /// Output bytes
+        pub bytes: Bytes,
+    }
+*)
+
+Module PrecompileOutput.
+  Record t : Set := {
+    gas_used : U64.t;
+    bytes : Bytes.t;
+  }.
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "revm_precompile::PrecompileOutput";
+    φ x :=
+        Value.StructRecord "revm_precompile::PrecompileOutput" [
+          ("gas_used", φ x.(gas_used));
+          ("bytes", φ x.(bytes))
+        ];
+    }.
+
+  
+
+End PrecompileOutput.
\ No newline at end of file

From edb78cb6eef7dfbaebc6d41587c9535c6908adad Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Sat, 22 Feb 2025 16:17:53 -0300
Subject: [PATCH 04/14] Defining impl PrecompileOutput

---
 .../revm/revm_precompile/links/interface.v    | 53 +++++++++++++++++--
 1 file changed, 49 insertions(+), 4 deletions(-)

diff --git a/CoqOfRust/revm/revm_precompile/links/interface.v b/CoqOfRust/revm/revm_precompile/links/interface.v
index 55b86f21e..c69776f4b 100644
--- a/CoqOfRust/revm/revm_precompile/links/interface.v
+++ b/CoqOfRust/revm/revm_precompile/links/interface.v
@@ -25,14 +25,59 @@ Module PrecompileOutput.
   }.
 
   Global Instance IsLink : Link t := {
-    Φ := Ty.path "revm_precompile::PrecompileOutput";
+    Φ := Ty.path "revm_precompile::interface::PrecompileOutput";
     φ x :=
-        Value.StructRecord "revm_precompile::PrecompileOutput" [
+        Value.StructRecord "revm_precompile::interface::PrecompileOutput" [
           ("gas_used", φ x.(gas_used));
           ("bytes", φ x.(bytes))
         ];
     }.
 
-  
+    Definition of_ty : OfTy.t (Ty.path "revm_precompile::interface::PrecompileOutput").
+    Proof. eapply OfTy.Make with (A := t); reflexivity.
+    Defined.
+    Smpl Add apply of_ty : of_ty.
 
-End PrecompileOutput.
\ No newline at end of file
+    Lemma of_value_with gas_used gas_used' bytes bytes' :
+    gas_used' = φ gas_used ->
+    bytes' = φ bytes ->
+    Value.StructRecord "revm_precompile::interface::PrecompileOutput" [
+      ("gas_used", gas_used');
+      ("bytes", bytes')
+    ] = φ (Build_t gas_used bytes).
+  Proof. now intros; subst. Qed.
+  Smpl Add apply of_value_with : of_value.
+
+  Definition of_value (gas_used : U64.t) gas_used' (bytes : Bytes.t) bytes' :
+    gas_used' = φ gas_used ->
+    bytes' = φ bytes ->
+    OfValue.t (
+      Value.StructRecord "revm_precompile::interface::PrecompileOutput" [
+        ("gas_used", gas_used');
+        ("bytes", bytes')
+      ]
+    ).
+  Proof. econstructor; apply of_value_with; repeat eassumption.
+  Defined.
+  Smpl Add apply of_value : of_value.
+
+End PrecompileOutput.
+
+Module Impl_PrecompileOutput.
+  Definition Self : Set := PrecompileOutput.t.
+
+  (*
+     pub fn new(gas_used: u64, bytes: Bytes) -> Self {
+        Self { gas_used, bytes }
+    }
+  *)
+
+  Definition run_new 
+      (gas_used : U64.t) 
+      (bytes : Bytes.t)
+    : {{ interface.Impl_revm_precompile_interface_PrecompileOutput.new [] [] [φ gas_used; φ bytes] 🔽 PrecompileOutput.t }}.
+  Proof.
+    run_symbolic.
+  Defined.
+  Smpl Add apply run_new : run_closure.
+End Impl_PrecompileOutput.

From ee7ecd23fc3ce50b541b7682fa6ea7ea9baf8646 Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Sat, 22 Feb 2025 16:29:58 -0300
Subject: [PATCH 05/14] Including subpointer for PrecompileOutput

---
 .../revm/revm_precompile/links/interface.v    | 35 +++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/CoqOfRust/revm/revm_precompile/links/interface.v b/CoqOfRust/revm/revm_precompile/links/interface.v
index c69776f4b..e7695a347 100644
--- a/CoqOfRust/revm/revm_precompile/links/interface.v
+++ b/CoqOfRust/revm/revm_precompile/links/interface.v
@@ -61,6 +61,39 @@ Module PrecompileOutput.
   Defined.
   Smpl Add apply of_value : of_value.
 
+  Module SubPointer.
+    Definition get_gas_used : SubPointer.Runner.t t
+      (Pointer.Index.StructRecord "revm_precompile::interface::PrecompileOutput" "gas_used") :=
+    {|
+      SubPointer.Runner.projection x := Some x.(gas_used);
+      SubPointer.Runner.injection x y := Some (x <| gas_used := y |>);
+    |}.
+
+    Lemma get_gas_used_is_valid :
+      SubPointer.Runner.Valid.t get_gas_used.
+    Proof.
+      now constructor.
+    Qed.
+
+    Smpl Add apply get_gas_used_is_valid : run_sub_pointer.
+
+    Definition get_bytes : SubPointer.Runner.t t
+      (Pointer.Index.StructRecord "revm_precompile::interface::PrecompileOutput" "bytes") :=
+    {|
+      SubPointer.Runner.projection x := Some x.(bytes);
+      SubPointer.Runner.injection x y := Some (x <| bytes := y |>);
+    |}.
+
+    Lemma get_bytes_is_valid :
+      SubPointer.Runner.Valid.t get_bytes.
+    Proof.
+      now constructor.
+    Qed.
+
+    Smpl Add apply get_bytes_is_valid : run_sub_pointer.
+
+  End SubPointer.
+
 End PrecompileOutput.
 
 Module Impl_PrecompileOutput.
@@ -81,3 +114,5 @@ Module Impl_PrecompileOutput.
   Defined.
   Smpl Add apply run_new : run_closure.
 End Impl_PrecompileOutput.
+
+

From c69133a49522dbaef579695a5816dc7b705e05eb Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Mon, 24 Feb 2025 15:11:04 -0300
Subject: [PATCH 06/14] Including clone for u64 type

---
 CoqOfRust/core/clone.v                        |  2 ++
 CoqOfRust/core/links/clone.v                  | 24 +++++++++++++++++++
 .../revm/revm_precompile/links/interface.v    | 17 +++++++++++++
 3 files changed, 43 insertions(+)

diff --git a/CoqOfRust/core/clone.v b/CoqOfRust/core/clone.v
index d5abab86c..a2199639d 100644
--- a/CoqOfRust/core/clone.v
+++ b/CoqOfRust/core/clone.v
@@ -819,4 +819,6 @@ Module clone.
           (* Instance *) [].
     End Impl_core_clone_Clone_where_core_marker_Sized_T_for_ref_mut_T.
   End impls.
+
+  
 End clone.
diff --git a/CoqOfRust/core/links/clone.v b/CoqOfRust/core/links/clone.v
index 5df01b71e..caa9e9e8d 100644
--- a/CoqOfRust/core/links/clone.v
+++ b/CoqOfRust/core/links/clone.v
@@ -1,5 +1,6 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import links.M.
+Require Import core.clone.
 
 Import Run.
 
@@ -25,3 +26,26 @@ Module Clone.
     (* TODO: add [clone_from] *)
   }.
 End Clone.
+
+Module Impl_Clone_for_u64.
+  Definition run_clone : clone.Clone.Run_clone U64.t.
+  Proof.
+    eexists; split.
+    { eapply IsTraitMethod.Defined.
+      { apply clone.impls.Impl_core_clone_Clone_for_u64.Implements. }
+      { reflexivity. }
+    }
+    { intros.
+      run_symbolic.
+    }
+  Defined.
+
+
+  Definition run : clone.Clone.Run U64.t.
+  Proof.
+    constructor.
+    { (* clone *)
+      exact run_clone.
+    }
+  Defined.
+End Impl_Clone_for_u64.
diff --git a/CoqOfRust/revm/revm_precompile/links/interface.v b/CoqOfRust/revm/revm_precompile/links/interface.v
index e7695a347..1f5d48dfa 100644
--- a/CoqOfRust/revm/revm_precompile/links/interface.v
+++ b/CoqOfRust/revm/revm_precompile/links/interface.v
@@ -1,11 +1,13 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.lib.
 Require Import CoqOfRust.links.M.
+Require Import core.links.clone.
 Require core.links.default.
 Require revm.links.dependencies.
 Import revm.links.dependencies.alloy_primitives.links.bytes_.
 Require Import revm_precompile.interface.
 
+
 Import Run.
 
 
@@ -115,4 +117,19 @@ Module Impl_PrecompileOutput.
   Smpl Add apply run_new : run_closure.
 End Impl_PrecompileOutput.
 
+Module Impl_Clone_for_PrecompileOutput.
+
+  Definition run_clone : clone.Clone.Run_clone PrecompileOutput.t.
+  Proof.
+    eexists; split.
+    - eapply IsTraitMethod.Defined.
+      + apply interface.Impl_core_clone_Clone_for_revm_precompile_interface_PrecompileOutput.Implements.
+      + reflexivity.
+    - intros self.
+    destruct Impl_Clone_for_u64.run.
+    destruct clone.
+      run_symbolic.
+  Defined.
+End Impl_Clone_for_PrecompileOutput.
+
 

From 072053a5ec41fd8cf9f809afe844c0d8c6a19ea6 Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Mon, 24 Feb 2025 16:44:01 -0300
Subject: [PATCH 07/14] Cherry picking clone methods for Bytes

---
 CoqOfRust/revm/links/dependencies.v | 55 +++++++++++++++++++++++++++--
 1 file changed, 52 insertions(+), 3 deletions(-)

diff --git a/CoqOfRust/revm/links/dependencies.v b/CoqOfRust/revm/links/dependencies.v
index cb14b9a74..b81bdc9ff 100644
--- a/CoqOfRust/revm/links/dependencies.v
+++ b/CoqOfRust/revm/links/dependencies.v
@@ -1,12 +1,33 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
+Require core.links.clone.
+
+Module ruint.
+  Module Uint.
+    Parameter t : Usize.t -> Usize.t -> Set.
+
+    Parameter to_value : forall {BITS LIMBS : Usize.t}, t BITS LIMBS -> Value.t.
+
+    Global Instance IsLink : forall {BITS LIMBS : Usize.t}, Link (t BITS LIMBS) := {
+      Φ := Ty.apply (Ty.path "ruint::Uint") [ φ BITS; φ LIMBS ] [];
+      φ := to_value;
+    }.
+
+    Definition of_ty (BITS' LIMBS' : Value.t) (BITS LIMBS : Usize.t) :
+      BITS' = φ BITS ->
+      LIMBS' = φ LIMBS ->
+      OfTy.t (Ty.apply (Ty.path "ruint::Uint") [ BITS' ; LIMBS' ] []).
+    Proof. intros. eapply OfTy.Make with (A := t BITS LIMBS). now subst. Defined.
+    Smpl Add eapply of_ty : of_ty.
+  End Uint.
+End ruint.
 
 Module alloy_primitives.
   Module bits.
     Module links.
       Module address.
         Module Address.
-          Parameter t: Set.
+          Parameter t : Set.
 
           Parameter to_value : t -> Value.t.
 
@@ -27,10 +48,39 @@ Module alloy_primitives.
         Parameter to_value : t -> Value.t.
 
         Global Instance IsLink : Link t := {
-          Φ := Ty.path "bytes::bytes::Bytes";
+          Φ := 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 : 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.
+      
+        Definition run : clone.Clone.Run Bytes.t.
+        Proof.
+          constructor.
+          { (* clone *)
+            exact run_clone.
+          }
+        Defined.
+      End Impl_Clone_for_Bytes.
     End bytes_.
   End links.
 End alloy_primitives.
@@ -45,7 +95,6 @@ Module Address.
     φ := to_value;
   }.
 End Address.
-
 Module FixedBytes.
   Parameter t : Set.
 

From 972fdd567e53573a7820ef9a89f5077b10369dcf Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Mon, 24 Feb 2025 16:48:51 -0300
Subject: [PATCH 08/14] Fixed clone proof for PrecompileOutput

---
 CoqOfRust/revm/links/dependencies.v              | 3 +--
 CoqOfRust/revm/revm_precompile/links/interface.v | 8 +++++---
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/CoqOfRust/revm/links/dependencies.v b/CoqOfRust/revm/links/dependencies.v
index b81bdc9ff..46b6b3e0f 100644
--- a/CoqOfRust/revm/links/dependencies.v
+++ b/CoqOfRust/revm/links/dependencies.v
@@ -65,9 +65,8 @@ Module alloy_primitives.
         Axiom Implements :
           M.IsTraitInstance
             "core::clone::Clone"
-            (* Trait polymorphic consts *) []
-            (* Trait polymorphic types *) []
             Self
+            (* Trait polymorphic types *) []
             (* Instance *) [ ("clone", InstanceField.Method clone) ].
 
         Definition run_clone : clone.Clone.Run_clone Bytes.t.
diff --git a/CoqOfRust/revm/revm_precompile/links/interface.v b/CoqOfRust/revm/revm_precompile/links/interface.v
index 1f5d48dfa..39ccfac9e 100644
--- a/CoqOfRust/revm/revm_precompile/links/interface.v
+++ b/CoqOfRust/revm/revm_precompile/links/interface.v
@@ -126,9 +126,11 @@ Module Impl_Clone_for_PrecompileOutput.
       + apply interface.Impl_core_clone_Clone_for_revm_precompile_interface_PrecompileOutput.Implements.
       + reflexivity.
     - intros self.
-    destruct Impl_Clone_for_u64.run.
-    destruct clone.
-      run_symbolic.
+       + destruct Impl_Clone_for_u64.run.
+         destruct clone.
+         destruct Impl_Clone_for_Bytes.run.
+         destruct clone.
+         run_symbolic.
   Defined.
 End Impl_Clone_for_PrecompileOutput.
 

From 529226164730f0e871f6d02f5ae618ae46cd88a2 Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Tue, 25 Feb 2025 16:17:38 -0300
Subject: [PATCH 09/14] Adding string.v and PrecompileError type

---
 CoqOfRust/alloc/links/string.v                | 16 ++++++
 .../revm/revm_precompile/links/interface.v    | 53 ++++++++++++++++++-
 2 files changed, 68 insertions(+), 1 deletion(-)
 create mode 100644 CoqOfRust/alloc/links/string.v

diff --git a/CoqOfRust/alloc/links/string.v b/CoqOfRust/alloc/links/string.v
new file mode 100644
index 000000000..455fcf060
--- /dev/null
+++ b/CoqOfRust/alloc/links/string.v
@@ -0,0 +1,16 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import links.M.
+
+Module String.
+    Record t : Set := {
+      value : string;
+    }.
+  
+    Global Instance IsLink : Link t := {
+      Φ := Ty.path "alloc::string::String";
+      φ s := Value.String s.(value)
+    }.
+  
+    Definition of_ty : OfTy.t (Ty.path "alloc::string::String").
+    Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  End String.
\ No newline at end of file
diff --git a/CoqOfRust/revm/revm_precompile/links/interface.v b/CoqOfRust/revm/revm_precompile/links/interface.v
index 39ccfac9e..361c06bd8 100644
--- a/CoqOfRust/revm/revm_precompile/links/interface.v
+++ b/CoqOfRust/revm/revm_precompile/links/interface.v
@@ -3,6 +3,7 @@ Require Import CoqOfRust.links.lib.
 Require Import CoqOfRust.links.M.
 Require Import core.links.clone.
 Require core.links.default.
+Require Import alloc.links.string.
 Require revm.links.dependencies.
 Import revm.links.dependencies.alloy_primitives.links.bytes_.
 Require Import revm_precompile.interface.
@@ -118,7 +119,6 @@ Module Impl_PrecompileOutput.
 End Impl_PrecompileOutput.
 
 Module Impl_Clone_for_PrecompileOutput.
-
   Definition run_clone : clone.Clone.Run_clone PrecompileOutput.t.
   Proof.
     eexists; split.
@@ -134,4 +134,55 @@ Module Impl_Clone_for_PrecompileOutput.
   Defined.
 End Impl_Clone_for_PrecompileOutput.
 
+Module PrecompileError.
+  Inductive t : Set :=
+  | OutOfGas
+  | Blake2WrongLength
+  | Blake2WrongFinalIndicatorFlag
+  | ModexpExpOverflow
+  | ModexpBaseOverflow
+  | ModexpModOverflow
+  | Bn128FieldPointNotAMember
+  | Bn128AffineGFailedToCreate
+  | Bn128PairLength
+  | BlobInvalidInputLength
+  | BlobMismatchedVersion
+  | BlobVerifyKzgProofFailed
+  | Other (msg : String.t).
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "revm_precompile::interface::PrecompileError";
+    φ x :=
+    match x with
+    | OutOfGas =>
+        Value.StructTuple "revm_precompile::interface::PrecompileError::OutOfGas" []
+    | Blake2WrongLength =>
+        Value.StructTuple "revm_precompile::interface::PrecompileError::Blake2WrongLength" []
+    | Blake2WrongFinalIndicatorFlag =>
+        Value.StructTuple "revm_precompile::interface::PrecompileError::Blake2WrongFinalIndicatorFlag" []
+    | ModexpExpOverflow =>
+        Value.StructTuple "revm_precompile::interface::PrecompileError::ModexpExpOverflow" []
+    | ModexpBaseOverflow =>
+        Value.StructTuple "revm_precompile::interface::PrecompileError::ModexpBaseOverflow" []
+    | ModexpModOverflow =>
+        Value.StructTuple "revm_precompile::interface::PrecompileError::ModexpModOverflow" []
+    | Bn128FieldPointNotAMember =>
+        Value.StructTuple "revm_precompile::interface::PrecompileError::Bn128FieldPointNotAMember" []
+    | Bn128AffineGFailedToCreate =>
+        Value.StructTuple "revm_precompile::interface::PrecompileError::Bn128AffineGFailedToCreate" []
+    | Bn128PairLength =>
+        Value.StructTuple "revm_precompile::interface::PrecompileError::Bn128PairLength" []
+    | BlobInvalidInputLength =>
+        Value.StructTuple "revm_precompile::interface::PrecompileError::BlobInvalidInputLength" []
+    | BlobMismatchedVersion =>
+        Value.StructTuple "revm_precompile::interface::PrecompileError::BlobMismatchedVersion" []
+    | BlobVerifyKzgProofFailed =>
+        Value.StructTuple "revm_precompile::interface::PrecompileError::BlobVerifyKzgProofFailed" []
+    | Other msg =>
+        Value.StructRecord "revm_precompile::interface::PrecompileError::Other" [("msg", φ msg)]
+    end;
+}.
+
+End PrecompileError.
+
 

From 0a21ee7242f18a23fc2fd099545b1b1d90012517 Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Tue, 25 Feb 2025 16:28:07 -0300
Subject: [PATCH 10/14] Lemmas for PrecompileOutputError

---
 .../revm/revm_precompile/links/interface.v    | 71 ++++++++++++++++++-
 1 file changed, 70 insertions(+), 1 deletion(-)

diff --git a/CoqOfRust/revm/revm_precompile/links/interface.v b/CoqOfRust/revm/revm_precompile/links/interface.v
index 361c06bd8..f4916c9bb 100644
--- a/CoqOfRust/revm/revm_precompile/links/interface.v
+++ b/CoqOfRust/revm/revm_precompile/links/interface.v
@@ -181,7 +181,76 @@ Module PrecompileError.
     | Other msg =>
         Value.StructRecord "revm_precompile::interface::PrecompileError::Other" [("msg", φ msg)]
     end;
-}.
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "revm_precompile::interface::PrecompileError").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add apply of_ty : of_ty.
+
+  Lemma of_value_with_OutOfGas :
+    Value.StructTuple "revm_precompile::interface::PrecompileError::OutOfGas" [] = φ OutOfGas.
+  Proof. reflexivity. Qed.
+  Smpl Add apply of_value_with_OutOfGas : of_value.
+
+  Lemma of_value_with_Blake2WrongLength :
+  Value.StructTuple "revm_precompile::interface::PrecompileError::Blake2WrongLength" [] = φ Blake2WrongLength.
+Proof. reflexivity. Qed.
+Smpl Add apply of_value_with_Blake2WrongLength : of_value.
+
+Lemma of_value_with_Blake2WrongFinalIndicatorFlag :
+  Value.StructTuple "revm_precompile::interface::PrecompileError::Blake2WrongFinalIndicatorFlag" [] = φ Blake2WrongFinalIndicatorFlag.
+Proof. reflexivity. Qed.
+Smpl Add apply of_value_with_Blake2WrongFinalIndicatorFlag : of_value.
+
+Lemma of_value_with_ModexpExpOverflow :
+  Value.StructTuple "revm_precompile::interface::PrecompileError::ModexpExpOverflow" [] = φ ModexpExpOverflow.
+Proof. reflexivity. Qed.
+Smpl Add apply of_value_with_ModexpExpOverflow : of_value.
+
+Lemma of_value_with_ModexpBaseOverflow :
+  Value.StructTuple "revm_precompile::interface::PrecompileError::ModexpBaseOverflow" [] = φ ModexpBaseOverflow.
+Proof. reflexivity. Qed.
+Smpl Add apply of_value_with_ModexpBaseOverflow : of_value.
+
+Lemma of_value_with_ModexpModOverflow :
+  Value.StructTuple "revm_precompile::interface::PrecompileError::ModexpModOverflow" [] = φ ModexpModOverflow.
+Proof. reflexivity. Qed.
+Smpl Add apply of_value_with_ModexpModOverflow : of_value.
+
+Lemma of_value_with_Bn128FieldPointNotAMember :
+  Value.StructTuple "revm_precompile::interface::PrecompileError::Bn128FieldPointNotAMember" [] = φ Bn128FieldPointNotAMember.
+Proof. reflexivity. Qed.
+Smpl Add apply of_value_with_Bn128FieldPointNotAMember : of_value.
+
+Lemma of_value_with_Bn128AffineGFailedToCreate :
+  Value.StructTuple "revm_precompile::interface::PrecompileError::Bn128AffineGFailedToCreate" [] = φ Bn128AffineGFailedToCreate.
+Proof. reflexivity. Qed.
+Smpl Add apply of_value_with_Bn128AffineGFailedToCreate : of_value.
+
+Lemma of_value_with_Bn128PairLength :
+  Value.StructTuple "revm_precompile::interface::PrecompileError::Bn128PairLength" [] = φ Bn128PairLength.
+Proof. reflexivity. Qed.
+Smpl Add apply of_value_with_Bn128PairLength : of_value.
+
+Lemma of_value_with_BlobInvalidInputLength :
+  Value.StructTuple "revm_precompile::interface::PrecompileError::BlobInvalidInputLength" [] = φ BlobInvalidInputLength.
+Proof. reflexivity. Qed.
+Smpl Add apply of_value_with_BlobInvalidInputLength : of_value.
+
+Lemma of_value_with_BlobMismatchedVersion :
+  Value.StructTuple "revm_precompile::interface::PrecompileError::BlobMismatchedVersion" [] = φ BlobMismatchedVersion.
+Proof. reflexivity. Qed.
+Smpl Add apply of_value_with_BlobMismatchedVersion : of_value.
+
+Lemma of_value_with_BlobVerifyKzgProofFailed :
+  Value.StructTuple "revm_precompile::interface::PrecompileError::BlobVerifyKzgProofFailed" [] = φ BlobVerifyKzgProofFailed.
+Proof. reflexivity. Qed.
+Smpl Add apply of_value_with_BlobVerifyKzgProofFailed : of_value.
+
+Lemma of_value_with_Other (msg : String.t) :
+  Value.StructRecord "revm_precompile::interface::PrecompileError::Other" [("msg", φ msg)] = φ (Other msg).
+Proof. reflexivity. Qed.
+Smpl Add apply of_value_with_Other : of_value.
 
 End PrecompileError.
 

From 48d9f00bfa97c1e4cd410a7ea4ae9ea2ce1efc5e Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Wed, 26 Feb 2025 14:14:45 -0300
Subject: [PATCH 11/14] Remove PrecompileError

---
 .../revm/revm_precompile/links/interface.v    | 124 +-----------------
 1 file changed, 1 insertion(+), 123 deletions(-)

diff --git a/CoqOfRust/revm/revm_precompile/links/interface.v b/CoqOfRust/revm/revm_precompile/links/interface.v
index f4916c9bb..c9dee25a3 100644
--- a/CoqOfRust/revm/revm_precompile/links/interface.v
+++ b/CoqOfRust/revm/revm_precompile/links/interface.v
@@ -132,126 +132,4 @@ Module Impl_Clone_for_PrecompileOutput.
          destruct clone.
          run_symbolic.
   Defined.
-End Impl_Clone_for_PrecompileOutput.
-
-Module PrecompileError.
-  Inductive t : Set :=
-  | OutOfGas
-  | Blake2WrongLength
-  | Blake2WrongFinalIndicatorFlag
-  | ModexpExpOverflow
-  | ModexpBaseOverflow
-  | ModexpModOverflow
-  | Bn128FieldPointNotAMember
-  | Bn128AffineGFailedToCreate
-  | Bn128PairLength
-  | BlobInvalidInputLength
-  | BlobMismatchedVersion
-  | BlobVerifyKzgProofFailed
-  | Other (msg : String.t).
-
-  Global Instance IsLink : Link t := {
-    Φ := Ty.path "revm_precompile::interface::PrecompileError";
-    φ x :=
-    match x with
-    | OutOfGas =>
-        Value.StructTuple "revm_precompile::interface::PrecompileError::OutOfGas" []
-    | Blake2WrongLength =>
-        Value.StructTuple "revm_precompile::interface::PrecompileError::Blake2WrongLength" []
-    | Blake2WrongFinalIndicatorFlag =>
-        Value.StructTuple "revm_precompile::interface::PrecompileError::Blake2WrongFinalIndicatorFlag" []
-    | ModexpExpOverflow =>
-        Value.StructTuple "revm_precompile::interface::PrecompileError::ModexpExpOverflow" []
-    | ModexpBaseOverflow =>
-        Value.StructTuple "revm_precompile::interface::PrecompileError::ModexpBaseOverflow" []
-    | ModexpModOverflow =>
-        Value.StructTuple "revm_precompile::interface::PrecompileError::ModexpModOverflow" []
-    | Bn128FieldPointNotAMember =>
-        Value.StructTuple "revm_precompile::interface::PrecompileError::Bn128FieldPointNotAMember" []
-    | Bn128AffineGFailedToCreate =>
-        Value.StructTuple "revm_precompile::interface::PrecompileError::Bn128AffineGFailedToCreate" []
-    | Bn128PairLength =>
-        Value.StructTuple "revm_precompile::interface::PrecompileError::Bn128PairLength" []
-    | BlobInvalidInputLength =>
-        Value.StructTuple "revm_precompile::interface::PrecompileError::BlobInvalidInputLength" []
-    | BlobMismatchedVersion =>
-        Value.StructTuple "revm_precompile::interface::PrecompileError::BlobMismatchedVersion" []
-    | BlobVerifyKzgProofFailed =>
-        Value.StructTuple "revm_precompile::interface::PrecompileError::BlobVerifyKzgProofFailed" []
-    | Other msg =>
-        Value.StructRecord "revm_precompile::interface::PrecompileError::Other" [("msg", φ msg)]
-    end;
-  }.
-
-  Definition of_ty : OfTy.t (Ty.path "revm_precompile::interface::PrecompileError").
-  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
-  Smpl Add apply of_ty : of_ty.
-
-  Lemma of_value_with_OutOfGas :
-    Value.StructTuple "revm_precompile::interface::PrecompileError::OutOfGas" [] = φ OutOfGas.
-  Proof. reflexivity. Qed.
-  Smpl Add apply of_value_with_OutOfGas : of_value.
-
-  Lemma of_value_with_Blake2WrongLength :
-  Value.StructTuple "revm_precompile::interface::PrecompileError::Blake2WrongLength" [] = φ Blake2WrongLength.
-Proof. reflexivity. Qed.
-Smpl Add apply of_value_with_Blake2WrongLength : of_value.
-
-Lemma of_value_with_Blake2WrongFinalIndicatorFlag :
-  Value.StructTuple "revm_precompile::interface::PrecompileError::Blake2WrongFinalIndicatorFlag" [] = φ Blake2WrongFinalIndicatorFlag.
-Proof. reflexivity. Qed.
-Smpl Add apply of_value_with_Blake2WrongFinalIndicatorFlag : of_value.
-
-Lemma of_value_with_ModexpExpOverflow :
-  Value.StructTuple "revm_precompile::interface::PrecompileError::ModexpExpOverflow" [] = φ ModexpExpOverflow.
-Proof. reflexivity. Qed.
-Smpl Add apply of_value_with_ModexpExpOverflow : of_value.
-
-Lemma of_value_with_ModexpBaseOverflow :
-  Value.StructTuple "revm_precompile::interface::PrecompileError::ModexpBaseOverflow" [] = φ ModexpBaseOverflow.
-Proof. reflexivity. Qed.
-Smpl Add apply of_value_with_ModexpBaseOverflow : of_value.
-
-Lemma of_value_with_ModexpModOverflow :
-  Value.StructTuple "revm_precompile::interface::PrecompileError::ModexpModOverflow" [] = φ ModexpModOverflow.
-Proof. reflexivity. Qed.
-Smpl Add apply of_value_with_ModexpModOverflow : of_value.
-
-Lemma of_value_with_Bn128FieldPointNotAMember :
-  Value.StructTuple "revm_precompile::interface::PrecompileError::Bn128FieldPointNotAMember" [] = φ Bn128FieldPointNotAMember.
-Proof. reflexivity. Qed.
-Smpl Add apply of_value_with_Bn128FieldPointNotAMember : of_value.
-
-Lemma of_value_with_Bn128AffineGFailedToCreate :
-  Value.StructTuple "revm_precompile::interface::PrecompileError::Bn128AffineGFailedToCreate" [] = φ Bn128AffineGFailedToCreate.
-Proof. reflexivity. Qed.
-Smpl Add apply of_value_with_Bn128AffineGFailedToCreate : of_value.
-
-Lemma of_value_with_Bn128PairLength :
-  Value.StructTuple "revm_precompile::interface::PrecompileError::Bn128PairLength" [] = φ Bn128PairLength.
-Proof. reflexivity. Qed.
-Smpl Add apply of_value_with_Bn128PairLength : of_value.
-
-Lemma of_value_with_BlobInvalidInputLength :
-  Value.StructTuple "revm_precompile::interface::PrecompileError::BlobInvalidInputLength" [] = φ BlobInvalidInputLength.
-Proof. reflexivity. Qed.
-Smpl Add apply of_value_with_BlobInvalidInputLength : of_value.
-
-Lemma of_value_with_BlobMismatchedVersion :
-  Value.StructTuple "revm_precompile::interface::PrecompileError::BlobMismatchedVersion" [] = φ BlobMismatchedVersion.
-Proof. reflexivity. Qed.
-Smpl Add apply of_value_with_BlobMismatchedVersion : of_value.
-
-Lemma of_value_with_BlobVerifyKzgProofFailed :
-  Value.StructTuple "revm_precompile::interface::PrecompileError::BlobVerifyKzgProofFailed" [] = φ BlobVerifyKzgProofFailed.
-Proof. reflexivity. Qed.
-Smpl Add apply of_value_with_BlobVerifyKzgProofFailed : of_value.
-
-Lemma of_value_with_Other (msg : String.t) :
-  Value.StructRecord "revm_precompile::interface::PrecompileError::Other" [("msg", φ msg)] = φ (Other msg).
-Proof. reflexivity. Qed.
-Smpl Add apply of_value_with_Other : of_value.
-
-End PrecompileError.
-
-
+End Impl_Clone_for_PrecompileOutput.
\ No newline at end of file

From 933612a2e9489bc6ca87f2c4c2f6e7b25498a40b Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Sat, 1 Mar 2025 11:30:43 -0300
Subject: [PATCH 12/14] Clone proved in the new setting

---
 CoqOfRust/revm/links/dependencies.v           | 37 +++++++++++--------
 .../revm/revm_precompile/links/interface.v    | 23 +++++++++++-
 2 files changed, 43 insertions(+), 17 deletions(-)

diff --git a/CoqOfRust/revm/links/dependencies.v b/CoqOfRust/revm/links/dependencies.v
index e44860e92..a1fbc3b78 100644
--- a/CoqOfRust/revm/links/dependencies.v
+++ b/CoqOfRust/revm/links/dependencies.v
@@ -1,6 +1,7 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import core.links.array.
+Require Import core.links.clone.
 Require Import core.convert.links.mod.
 
 Import Run.
@@ -159,12 +160,7 @@ Module alloy_primitives.
           Φ := 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 : Ty.t := Ty.path "alloy_primitives::bytes_::Bytes".
 
@@ -173,20 +169,31 @@ Module alloy_primitives.
         Axiom Implements :
           M.IsTraitInstance
             "core::clone::Clone"
-            Self
+            (* Trait polymorphic consts *) []
             (* Trait polymorphic types *) []
+            Self
             (* Instance *) [ ("clone", InstanceField.Method clone) ].
 
-        Definition run_clone : clone.Clone.Run_clone Bytes.t.
-        Admitted.
-      
-        Definition run : clone.Clone.Run Bytes.t.
-        Proof.
-          constructor.
-          { (* clone *)
-            exact run_clone.
-          }
+           Definition run_clone : clone.Clone.Run_clone Bytes.t.
+           Admitted.
+
+          Definition run : clone.Clone.Run Bytes.t.
+          Proof.
+            constructor.
+            { (* clone *)
+              exact run_clone.
+            }
         Defined.
+        Definition getMethod :
+          IsTraitMethod.t "core::clone::Clone" [] []
+          Self 
+          "clone"
+          clone.
+        Proof.
+          eapply IsTraitMethod.Defined.
+          - apply Implements. 
+          - reflexivity.       
+        Qed.
       End Impl_Clone_for_Bytes.
     End bytes_.
   End links.
diff --git a/CoqOfRust/revm/revm_precompile/links/interface.v b/CoqOfRust/revm/revm_precompile/links/interface.v
index d77f89bb2..c90dc6839 100644
--- a/CoqOfRust/revm/revm_precompile/links/interface.v
+++ b/CoqOfRust/revm/revm_precompile/links/interface.v
@@ -130,7 +130,25 @@ Module Impl_Clone_for_PrecompileOutput.
          destruct clone.
          destruct Impl_Clone_for_Bytes.run.
          destruct clone.
-         run_symbolic.
+         run_symbolic. 
+         run_symbolic_closure.
+         { apply p with (self := Ref.cast_to Pointer.Kind.Ref sub_ref). }
+         {
+          intros []; run_symbolic.
+          run_symbolic_closure.
+          {
+            eapply OfTy.Make with (A := Bytes.t).
+            reflexivity.
+          }
+          {
+            run_symbolic.
+            destruct p0 as [pProof pMeth].
+            apply pMeth.
+          }
+          {
+            intros []; run_symbolic.
+          }
+         }
   Defined.
 End Impl_Clone_for_PrecompileOutput.
 
@@ -381,6 +399,7 @@ Module Impl_PrecompileError.
     }}.
   Proof.
     run_symbolic.
-    destruct_all Self; run_symbolic.
+    destruct_all Self. 
+    run_symbolic.
   Defined.
 End Impl_PrecompileError.

From b25b4de70efe552abecd6679288a233c5e341394 Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Mon, 3 Mar 2025 10:24:14 -0300
Subject: [PATCH 13/14] Shortening is_oog

---
 CoqOfRust/revm/links/dependencies.v              | 10 ----------
 CoqOfRust/revm/revm_precompile/links/interface.v |  3 +--
 2 files changed, 1 insertion(+), 12 deletions(-)

diff --git a/CoqOfRust/revm/links/dependencies.v b/CoqOfRust/revm/links/dependencies.v
index a1fbc3b78..ab745b09b 100644
--- a/CoqOfRust/revm/links/dependencies.v
+++ b/CoqOfRust/revm/links/dependencies.v
@@ -184,16 +184,6 @@ Module alloy_primitives.
               exact run_clone.
             }
         Defined.
-        Definition getMethod :
-          IsTraitMethod.t "core::clone::Clone" [] []
-          Self 
-          "clone"
-          clone.
-        Proof.
-          eapply IsTraitMethod.Defined.
-          - apply Implements. 
-          - reflexivity.       
-        Qed.
       End Impl_Clone_for_Bytes.
     End bytes_.
   End links.
diff --git a/CoqOfRust/revm/revm_precompile/links/interface.v b/CoqOfRust/revm/revm_precompile/links/interface.v
index c90dc6839..f49bc5b83 100644
--- a/CoqOfRust/revm/revm_precompile/links/interface.v
+++ b/CoqOfRust/revm/revm_precompile/links/interface.v
@@ -399,7 +399,6 @@ Module Impl_PrecompileError.
     }}.
   Proof.
     run_symbolic.
-    destruct_all Self. 
-    run_symbolic.
+    destruct_all Self; run_symbolic.
   Defined.
 End Impl_PrecompileError.

From 4494db6380fbdf93a182163a1ac926dd25661144 Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Mon, 3 Mar 2025 15:07:49 -0300
Subject: [PATCH 14/14] Clone for PrecompileError

---
 .../revm/revm_precompile/links/interface.v    | 75 ++++++++++++++++++-
 1 file changed, 74 insertions(+), 1 deletion(-)

diff --git a/CoqOfRust/revm/revm_precompile/links/interface.v b/CoqOfRust/revm/revm_precompile/links/interface.v
index f49bc5b83..d738fb5a2 100644
--- a/CoqOfRust/revm/revm_precompile/links/interface.v
+++ b/CoqOfRust/revm/revm_precompile/links/interface.v
@@ -2,13 +2,13 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.lib.
 Require Import CoqOfRust.links.M.
 Require Import core.links.clone.
+Require core.links.option.
 Require core.links.default.
 Require Import alloc.links.string.
 Require revm.links.dependencies.
 Import revm.links.dependencies.alloy_primitives.links.bytes_.
 Require Import revm_precompile.interface.
 
-
 Import Run.
 
 
@@ -402,3 +402,76 @@ Module Impl_PrecompileError.
     destruct_all Self; run_symbolic.
   Defined.
 End Impl_PrecompileError.
+
+Module Impl_Clone_for_PrecompileError.
+  Definition run_clone : clone.Clone.Run_clone PrecompileError.t.
+  Proof.
+  Admitted. 
+  
+End Impl_Clone_for_PrecompileError.
+
+
+Module Impl_PrecompileErrors.
+  Inductive t : Set := 
+  | Error (_ : PrecompileError.t)
+  | Fatal
+      (_ : alloc.links.string.String.t)
+  .
+
+  Global Instance IsLink : Link t := {
+    Φ := Ty.path "revm_precompile::interface::PrecompileErrors";
+    φ x :=
+      match x with
+      | Error γ0 =>
+        Value.StructTuple "revm_precompile::interface::PrecompileErrors::Error" [φ γ0]
+      | Fatal γ0 => Value.StructTuple "revm_precompile::interface::PrecompileErrors::Fatal" [φ γ0]
+      end
+  }.
+
+  Definition of_ty : OfTy.t (Ty.path "revm_precompile::interface::PrecompileErrors").
+  Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
+  Smpl Add simple apply of_ty : of_ty.
+
+  Lemma of_value_with_Error
+    (γ0 : PrecompileError.t) (γ0' : Value.t) :
+    γ0' = φ γ0 ->
+    Value.StructTuple "revm_precompile::interface::PrecompileErrors::Error" [
+      γ0'
+    ] =
+    φ (Error γ0).
+  Proof. now intros; subst. Qed.
+  Smpl Add simple apply of_value_with_Error : of_value.
+
+  Definition of_value_Error
+    (γ0 : PrecompileError.t) (γ0' : Value.t) :
+    γ0' = φ γ0 ->
+    OfValue.t (
+      Value.StructTuple "revm_precompile::interface::PrecompileErrors::Error" [
+        γ0'
+      ]
+    ).
+  Proof. econstructor; apply of_value_with_Error; eassumption. Defined.
+  Smpl Add simple apply of_value_Error : of_value.
+
+  Lemma of_value_with_Fatal
+    (γ0 : alloc.links.string.String.t) (γ0' : Value.t) :
+    γ0' = φ γ0 ->
+    Value.StructTuple "revm_precompile::interface::PrecompileErrors::Fatal" [
+      γ0'
+    ] =
+    φ (Fatal γ0).
+  Proof. now intros; subst. Qed.
+  Smpl Add simple apply of_value_with_Fatal : of_value.
+
+  Definition of_value_Fatal
+    (γ0 : alloc.links.string.String.t) (γ0' : Value.t) :
+    γ0' = φ γ0 ->
+    OfValue.t (
+      Value.StructTuple "revm_precompile::interface::PrecompileErrors::Fatal" [
+        γ0'
+      ]
+    ).
+  Proof. econstructor; apply of_value_with_Fatal; eassumption. Defined.
+  Smpl Add simple apply of_value_Fatal : of_value.
+  
+End Impl_PrecompileErrors.