Merge pull request #683 from formal-land/guillaume-claret@add-translation-of-ruint

Add a translation of ruint

Author: clarus

.github/workflows/rust.yml

@@ -139,6 +139,15 @@ jobs:
             cd ..
             cd ../../..
           endGroup
+          startGroup "Translate ruint"
+            cd third-party/uint
+            cp ../../rust-toolchain ./
+            cargo coq-of-rust
+            touch src/lib.rs
+            cargo coq-of-rust
+            rsync -rcv src/ ../../CoqOfRust/ruint/ --include='*/' --include='*.v' --exclude='*'
+            cd ../..
+          endGroup
           startGroup "Translate Move Sui"
             cd third-party/move-sui
             cp ../../rust-toolchain ./

.gitmodules

@@ -10,3 +10,6 @@
 [submodule "third-party/move-sui"]
 	path = third-party/move-sui
 	url = https://github.com/formal-land/move-sui.git
+[submodule "third-party/uint"]
+	path = third-party/uint
+	url = https://github.com/recmo/uint.git

CoqOfRust/revm/links/dependencies.v

@@ -4,74 +4,7 @@ Require Import core.convert.links.mod.
 Require Import core.links.array.
 Require core.links.clone.
 Require core.links.default.
-Import Run.
-
-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.
-
-  Module Impl_Uint.
-    (* Uint<BITS, LIMBS> *)
-    Definition Self (BITS LIMBS : Usize.t) : Set :=
-      Uint.t BITS LIMBS.
-
-    Definition Self_ty (BITS LIMBS : Value.t) : Ty.t :=
-      Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] [].
-
-    (* pub fn wrapping_add(self, rhs: Self) -> Self *)
-    Parameter wrapping_add : forall (BITS LIMBS : Value.t), PolymorphicFunction.t.
-
-    Global Instance wrapping_add_IsAssociated :
-      forall (BITS LIMBS : Value.t),
-      M.IsAssociatedFunction.Trait
-        (Self_ty BITS LIMBS)
-        "wrapping_add"
-        (wrapping_add BITS LIMBS).
-    Admitted.
-
-    Global Instance run_wrapping_add :
-      forall (BITS LIMBS : Usize.t),
-      forall (x1 x2 : Self BITS LIMBS),
-      Run.Trait
-        (wrapping_add (φ BITS) (φ LIMBS)) [] [] [ φ x1; φ x2 ]
-        (Self BITS LIMBS).
-    Admitted.
-
-    (* pub const fn to_be_bytes<const BYTES: usize>(&self) -> [u8; BYTES] *)
-    Parameter to_be_bytes : forall (BITS LIMBS : Value.t), PolymorphicFunction.t.
-
-    Global Instance to_be_bytes_IsAssociated :
-      forall (BITS LIMBS : Value.t),
-      M.IsAssociatedFunction.Trait
-        (Self_ty BITS LIMBS)
-        "to_be_bytes"
-        (to_be_bytes BITS LIMBS).
-    Admitted.
-
-    Global Instance run_to_be_bytes :
-      forall (BITS LIMBS BYTES : Usize.t),
-      forall (x : Ref.t Pointer.Kind.Ref (Self BITS LIMBS)),
-      Run.Trait
-        (to_be_bytes (φ BITS) (φ LIMBS)) [ φ BYTES ] [] [ φ x ]
-        (array.t U8.t BYTES).
-    Admitted.
-  End Impl_Uint.
-End ruint.
+Require Import ruint.links.lib.
 
 Module alloy_primitives.
   Module bits.
@@ -254,7 +187,7 @@ End FixedBytes.
 
 Module U256.
   Definition t : Set :=
-    ruint.Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}.
+    Uint.t {| Integer.value := 256 |} {| Integer.value := 4 |}.
 End U256.
 
 Module B256.

CoqOfRust/revm/revm_interpreter/instructions/links/arithmetic.v

@@ -5,8 +5,10 @@ Require Import revm.revm_interpreter.links.gas.
 Require Import revm.revm_interpreter.links.interpreter.
 Require Import revm.revm_interpreter.links.interpreter_types.
 Require Import revm.revm_interpreter.instructions.arithmetic.
+Require Import ruint.links.add.
 
 Import Impl_Gas.
+Import Impl_Uint.
 
 (*
 pub fn add<WIRE: InterpreterTypes, H: Host + ?Sized>(

CoqOfRust/revm/revm_interpreter/instructions/links/utility.v

@@ -3,6 +3,9 @@ Require Import CoqOfRust.links.M.
 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.
 
 (*
 pub trait IntoAddress {