Merge pull request #646 from formal-land/guillaume-claret@add-some-revm-simulations

links: more fixes to the compilation

Author: clarus

CoqOfRust/M.v

@@ -235,14 +235,14 @@ Module Value.
       end
     | Pointer.Index.Array index =>
       match value with
-      | Array fields => Some (Array (List.replace_at fields (Z.to_nat index) value))
+      | Array fields => Some (Array (List.replace_at fields (Z.to_nat index) update))
       | _ => None
       end
     | Pointer.Index.StructRecord constructor field =>
       match value with
       | StructRecord c fields =>
         if String.eqb c constructor then
-          Some (StructRecord c (List.assoc_replace fields field value))
+          Some (StructRecord c (List.assoc_replace fields field update))
         else
           None
       | _ => None
@@ -251,7 +251,7 @@ Module Value.
       match value with
       | StructTuple c fields =>
         if String.eqb c constructor then
-          Some (StructTuple c (List.replace_at fields (Z.to_nat index) value))
+          Some (StructTuple c (List.replace_at fields (Z.to_nat index) update))
         else
           None
       | _ => None

CoqOfRust/alloc/vec/links/mod.v

@@ -5,4 +5,15 @@ Require Import move_sui.translations.move_binary_format.file_format.
 Import Run.
 
 Module Vec.
+  Record t {A : Set} : Set := {
+    value : list A;
+  }.
+  Arguments t : clear implicits.
+
+  Parameter to_value : forall {A : Set}, t A -> Value.t.
+
+  Global Instance IsLink (A : Set) (_ : Link A) : Link (t A) := {
+    Φ := Ty.apply (Ty.path "vec") [] [Φ A];
+    φ := to_value;
+  }.
 End Vec.

CoqOfRust/blacklist.txt

@@ -7,9 +7,7 @@ examples/axiomatized/examples/custom/provided_method.v
 examples/axiomatized/examples/rust_book/traits/traits.v
 examples/axiomatized/examples/subtle.v
 # examples/
-revm/links
 revm/simulations
-revm/translations/precompile/utilities.v
 # This file works but is taking a very long time (ten minutes)
 revm/translations/interpreter/opcode.v
 core/array/mod.v
@@ -18,7 +16,6 @@ core/net/ip_addr.v
 core/num/int_sqrt.v
 token-2022
 # Links that are not working yet
-core/links/cmp.v
 move_sui/links/
 # We ignore the metering for now
 move_sui/simulations/move_bytecode_verifier_meter/lib.v

CoqOfRust/core/links/array.v

@@ -7,9 +7,9 @@ Module Array.
   Arguments Make {_ _} _.
 
   Global Instance IsLink (length : Z) (A : Set) (_ : Link A) : Link (t length A) := {
-    to_ty :=
-      Ty.apply (Ty.path "array") [Value.Integer IntegerKind.Usize length] [to_ty A];
-    to_value '(Make x) :=
-      Value.Array (List.map to_value x);
+    Φ :=
+      Ty.apply (Ty.path "array") [Value.Integer IntegerKind.Usize length] [Φ A];
+    φ '(Make x) :=
+      Value.Array (List.map φ x);
   }.
 End Array.

CoqOfRust/core/links/bool.v

@@ -15,10 +15,10 @@ Import Run.
 Module Clone.
   Definition Run_clone (Self : Set) `{Link Self} : Set :=
     {clone @
-      IsTraitMethod.t "core::clone::Clone" (to_ty Self) [] "clone" clone *
+      IsTraitMethod.t "core::clone::Clone" (Φ Self) [] "clone" clone *
       forall (self : Ref.t Pointer.Kind.Ref Self),
         {{
-          clone [] [] [ to_value self ] ⇓
+          clone [] [] [ φ self ] ⇓
           output_pure Self
         }}
     }.

CoqOfRust/core/links/clone.v

@@ -19,8 +19,8 @@ Module Ordering.
   | Greater : t.
 
   Global Instance IsLink : Link t := {
-    to_ty := Ty.path "core::cmp::Ordering";
-    to_value x :=
+    Φ := Ty.path "core::cmp::Ordering";
+    φ x :=
       match x with
       | Less => Value.StructTuple "core::cmp::Ordering::Less" []
       | Equal => Value.StructTuple "core::cmp::Ordering::Equal" []
@@ -29,6 +29,7 @@ Module Ordering.
   }.
 End Ordering.
 
+(*
 (*
     pub fn max_by<T, F: FnOnce(&T, &T) -> Ordering>(v1: T, v2: T, compare: F) -> T {
         match compare(&v1, &v2) {
@@ -222,3 +223,4 @@ Module Impl_Ord_for_u64.
     }
   Admitted.
 End Impl_Ord_for_u64.
+*)

CoqOfRust/core/links/cmp.v

@@ -13,7 +13,7 @@ Import Run.
 Module Default.
   Definition Run_default (Self : Set) `{Link Self} : Set :=
     {default @
-      IsTraitMethod.t "core::default::Default" (to_ty Self) [] "default" default *
+      IsTraitMethod.t "core::default::Default" (Φ Self) [] "default" default *
       {{
         default [] [] [] ⇓
         output_pure Self
@@ -100,7 +100,7 @@ Module Impl_Default_for_integer.
 
   Definition implements_of_integer_kind (kind : IntegerKind.t) :
       IsTraitInstance "core::default::Default"
-        (to_ty (Self kind))
+        (Φ (Self kind))
         []
         [("default", InstanceField.Method (method_of_ingeter_kind kind))] :=
     match kind with

CoqOfRust/core/links/default.v

@@ -3,11 +3,11 @@ Require Import links.M.
 
 Module Option.
   Global Instance IsLink (A : Set) (_ : Link A) : Link (option A) := {
-    to_ty := Ty.apply (Ty.path "core::option::Option") [] [to_ty A];
-    to_value x :=
+    Φ := Ty.apply (Ty.path "core::option::Option") [] [Φ A];
+    φ x :=
       match x with
       | None => Value.StructTuple "core::option::Option::None" []
-      | Some x => Value.StructTuple "core::option::Option::Some" [to_value x]
+      | Some x => Value.StructTuple "core::option::Option::Some" [φ x]
       end;
   }.
 End Option.

CoqOfRust/core/links/option.v

@@ -3,11 +3,11 @@ Require Import links.M.
 
 Module Result.
   Global Instance IsLink (A B : Set) (_ : Link A) (_ : Link B) : Link (A + B) := {
-    to_ty := Ty.apply (Ty.path "core::result::Result") [] [to_ty A; to_ty B];
-    to_value x :=
+    Φ := Ty.apply (Ty.path "core::result::Result") [] [Φ A; Φ B];
+    φ x :=
       match x with
-      | inl x => Value.StructTuple "core::result::Result::Ok" [to_value x]
-      | inr e => Value.StructTuple "core::result::Result::Err" [to_value e]
+      | inl x => Value.StructTuple "core::result::Result::Ok" [φ x]
+      | inr e => Value.StructTuple "core::result::Result::Err" [φ e]
       end;
   }.
 End Result.

CoqOfRust/core/links/result.v

@@ -16,10 +16,10 @@ Module FnOnce.
   Definition Run_call_once (Self Args : Set) {Output : Set}
       `{Link Self} `{Link Args} `{Link Output} : Set :=
     {call_once @
-      IsTraitMethod.t "core::ops::function::FnOnce" (to_ty Self) [ to_ty Args ] "call_once" call_once *
+      IsTraitMethod.t "core::ops::function::FnOnce" (Φ Self) [ Φ Args ] "call_once" call_once *
       forall (self : Self) (args : Args),
       {{
-        call_once [] [] [ to_value self; to_value args ] ⇓
+        call_once [] [] [ φ self; φ args ] ⇓
         output_pure Output
       }}
     }.

CoqOfRust/core/ops/links/function.v

@@ -1,3 +1,5 @@
+Require Import CoqOfRust.CoqOfRust.
+
 Module Eq.
   Class Trait (Self : Set) : Set := {
     eqb: Self -> Self -> bool
@@ -15,3 +17,7 @@ End Eq.
 Module Notations.
   Notation "x =? y" := (Eq.eqb x y) (at level 70).
 End Notations.
+
+Global Instance ZIsEq : Eq.Trait Z := {
+  Eq.eqb := Z.eqb
+}.