Adding links to precompile crate (#658)

CoqOfRust/core/clone.v

@@ -846,4 +846,6 @@ Module clone.
           (* Instance *) [].
     End Impl_core_clone_Clone_where_core_marker_Sized_T_for_ref_mut_T.
   End impls.
+
+
 End clone.

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.

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.
@@ -156,10 +157,34 @@ 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;
         }.
       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.

CoqOfRust/revm/revm_precompile/links/identity.v

@@ -0,0 +1,41 @@
+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;
+*)
+
+Module identity.
+
+  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.
+
+

CoqOfRust/revm/revm_precompile/links/interface.v

@@ -1,10 +1,157 @@
 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 Import revm.revm_precompile.interface.
+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::interface::PrecompileOutput";
+    φ x :=
+        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.
+
+    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.
+
+  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.
+  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.
+
+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.
+         destruct Impl_Clone_for_Bytes.run.
+         destruct clone.
+         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.
+
 Module PrecompileError.
   Inductive t : Set :=
   | OutOfGas
@@ -255,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.