Formalizing bitwise.rs

CoqOfRust/core/links/cmpOrdering.v

@@ -56,4 +56,8 @@ Module Ordering.
   Definition of_value_Greater : OfValue.t (Value.StructTuple "core::cmp::Ordering::Greater" []).
   Proof. eapply OfValue.Make with (value := Greater); reflexivity. Defined.
   Smpl Add apply of_value_Greater : of_value.
+
+  Module Impl_PartialOrd_for_Ordering.
+
+  End Impl_PartialOrd_for_Ordering.
 End Ordering.

CoqOfRust/core/links/intrinsics.v

@@ -16,3 +16,20 @@ Instance run_saturating_add (integer_kind : IntegerKind.t) (x y : Integer.t inte
     (Integer.t integer_kind).
 Proof.
 Admitted.
+
+Instance run_sub_with_overflow
+  (x y : Integer.t IntegerKind.U64) :
+  Run.Trait
+    intrinsics.intrinsics.sub_with_overflow
+    []
+    [ Φ (Integer.t IntegerKind.U64) ]
+    [ φ x; φ y ]
+    (Integer.t IntegerKind.U64 * bool).
+Proof.
+Admitted.
+
+Instance run_discriminant_value (ref : Ref.t Pointer.Kind.Ref Ordering.t) :
+  Run.Trait intrinsics.discriminant_value [] [Φ Ordering.t] [φ ref]
+             (Integer.t IntegerKind.I8).
+Proof.
+Admitted.

CoqOfRust/links/M.v

@@ -114,6 +114,7 @@ Module PrimitiveEq.
 End PrimitiveEq.
 
 Module Bool.
+
   Global Instance IsLink : Link bool := {
     Φ := Ty.path "bool";
     φ b := Value.Bool b;

CoqOfRust/revm/links/dependencies.v

@@ -71,6 +71,263 @@ Module ruint.
         (array.t U8.t BYTES).
     Admitted.
   End Impl_Uint.
+
+  Module Impl_bit_for_Uint.
+    (* Define Self as the underlying Uint type parameterized by BITS and LIMBS. *)
+    Definition Self (BITS LIMBS : Usize.t) : Set :=
+      ruint.Uint.t BITS LIMBS.
+
+    (* The linked type for Self is given by the application of the Uint path to the bit and limb parameters. *)
+    Definition Self_ty (BITS LIMBS : Value.t) : Ty.t :=
+      Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] [].
+
+    (* Declare the polymorphic function "bit". The type here is abstract;
+       it represents the associated function in Rust that takes an extra argument
+       (for example, a Usize) and returns a Uint. Adjust the argument list as needed. *)
+    Parameter bit : forall (BITS LIMBS : Value.t), PolymorphicFunction.t.
+
+    (* Declare the associated function instance. This tells our framework that "bit"
+       is the associated function for the Uint type with the given BITS and LIMBS. *)
+    Global Instance bit_IsAssociated :
+      forall (BITS LIMBS : Value.t),
+        M.IsAssociatedFunction.Trait
+          (Self_ty BITS LIMBS)
+          "bit"
+          (bit BITS LIMBS).
+    Admitted.
+
+    (* Provide a run-instance for "bit" in case the function takes an extra argument.
+       For instance, if "bit" takes a Usize.t argument (say, a bit index or similar),
+       then the run instance might look like this. Adjust the argument types as needed.
+
+       Here we assume it takes one Usize.t argument. If it takes no arguments, simply leave the list empty.
+    *)
+    Global Instance run_bit :
+      forall (BITS LIMBS : Usize.t) (input : Usize.t),
+        Run.Trait (bit (φ BITS) (φ LIMBS))
+                  []           (* no polymorphic constants *)
+                  []           (* no trait polymorphic types; adjust if needed *)
+                  [ φ input ]  (* the argument list *)
+                  (Self BITS LIMBS).
+    Admitted.
+
+  End Impl_bit_for_Uint.
+
+  Module Impl_is_zero_Uint.
+    (* We assume the type of Uint is already defined, e.g.: *)
+    Definition Self (BITS LIMBS : Usize.t) : Set :=
+      ruint.Uint.t BITS LIMBS.
+
+    Definition Self_ty (BITS LIMBS : Value.t) : Ty.t :=
+      Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] [].
+
+    (* The associated function "is_zero" as a polymorphic function.
+       Its parameters are the polymorphic parameters for BITS and LIMBS.
+       Its intended meaning is that when invoked on a Uint, it returns a bool. *)
+    Parameter is_zero : forall (BITS LIMBS : Value.t), PolymorphicFunction.t.
+
+    Global Instance is_zero_IsAssociated :
+      forall (BITS LIMBS : Value.t),
+        M.IsAssociatedFunction.Trait
+          (Self_ty BITS LIMBS)
+          "is_zero"
+          (is_zero BITS LIMBS).
+    Admitted.
+
+    (* The runtime instance: when you run "is_zero" (with the linked BITS and LIMBS) on an
+       argument – here a reference to the Uint – you get a bool. *)
+    Global Instance run_is_zero :
+      forall (BITS LIMBS : Usize.t)
+             (self : Ref.t Pointer.Kind.Ref (Self BITS LIMBS)),
+        Run.Trait (is_zero (φ BITS) (φ LIMBS)) [] [] [ Ref.IsLink.(φ) self ] bool.
+    Admitted.
+  End Impl_is_zero_Uint.
+
+  Module Impl_from_Uint.
+    Definition Self (BITS LIMBS : Usize.t) : Set :=
+      ruint.Uint.t BITS LIMBS.
+
+    Definition Self_ty (BITS LIMBS : Value.t) : Ty.t :=
+      Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] [].
+
+    (* pub const fn from(value: Usize.t) -> Self *)
+    Parameter from : forall (BITS LIMBS : Value.t), PolymorphicFunction.t.
+
+    Global Instance from_IsAssociated :
+      forall (BITS LIMBS : Value.t),
+      M.IsAssociatedFunction.Trait
+        (Self_ty BITS LIMBS)
+        "from"
+        (from BITS LIMBS).
+    Admitted.
+
+    Global Instance run_from :
+      forall (BITS LIMBS : Usize.t) (value : Usize.t),
+      Run.Trait (from (φ BITS) (φ LIMBS)) [] [] [ φ value ] (Self BITS LIMBS).
+    Admitted.
+
+    Global Instance run_from_bool :
+      forall (BITS LIMBS : Usize.t) (value : bool),
+      Run.Trait (from (φ BITS) (φ LIMBS)) [] [ Φ bool ] [ φ value ] (Self BITS LIMBS).
+    Admitted.
+  End Impl_from_Uint.
+
+  Module Impl_PartialOrd_for_Uint.
+      Definition Self (BITS LIMBS : Value.t) : Ty.t :=
+        Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] [].
+
+      Parameter lt : forall (BITS LIMBS : Value.t), PolymorphicFunction.t.
+      Parameter gt : forall (BITS LIMBS : Value.t), PolymorphicFunction.t.
+
+      Axiom Implements :
+        forall (BITS LIMBS : Value.t) (trait_tys : list Ty.t),
+          M.IsTraitInstance
+            "core::cmp::PartialOrd"
+            (* Trait polymorphic consts *) []
+            (* Trait polymorphic types *) trait_tys
+            (Self BITS LIMBS)
+            (* Instance *) [ ("lt", InstanceField.Method (lt BITS LIMBS)); ("gt", InstanceField.Method (gt BITS LIMBS)) ].
+
+      Definition run_lt :
+        forall (BITS LIMBS : Usize.t),
+        forall (x1 x2 : Ref.t Pointer.Kind.Ref (ruint.Uint.t BITS LIMBS)),
+        {{ lt (φ BITS) (φ LIMBS) [] [] [ φ x1; φ x2 ] 🔽 bool }}.
+      Admitted.
+
+      Definition run_gt :
+        forall (BITS LIMBS : Usize.t),
+        forall (x1 x2 : Ref.t Pointer.Kind.Ref (ruint.Uint.t BITS LIMBS)),
+        {{ gt (φ BITS) (φ LIMBS) [] [] [ φ x1; φ x2 ] 🔽 bool }}.
+      Admitted.
+
+      Definition run (BITS LIMBS : Value.t) :
+        PolymorphicFunction.t.
+      Proof.
+        exact (lt BITS LIMBS).
+      Defined.
+    End Impl_PartialOrd_for_Uint.
+
+    Module Impl_PartialEq_for_Uint.
+      Definition Self (BITS LIMBS : Value.t) : Ty.t :=
+        Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] [].
+
+      Parameter eq : forall (BITS LIMBS : Value.t), PolymorphicFunction.t.
+
+      Axiom Implements :
+        forall (BITS LIMBS : Value.t),
+          M.IsTraitInstance
+            "core::cmp::PartialEq"
+            []
+            [Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []]
+            (Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] [])
+            [("eq", InstanceField.Method (Impl_PartialEq_for_Uint.eq BITS LIMBS))].
+
+      Definition run_eq :
+          forall (BITS LIMBS : Usize.t),
+          forall (x1 x2 : Ref.t Pointer.Kind.Ref (ruint.Uint.t BITS LIMBS)),
+          {{ eq (φ BITS) (φ LIMBS) [] [] [ φ x1; φ x2 ] 🔽 bool }}.
+      Proof.
+      Admitted.
+
+      Instance run_eq_Uint :
+        forall (BITS LIMBS : Usize.t) (x y : Ref.t Pointer.Kind.Ref (Uint.t BITS LIMBS)),
+        Run.Trait (eq (φ BITS) (φ LIMBS)) [] [] [ φ x; φ y ] bool.
+      Admitted.
+
+    End Impl_PartialEq_for_Uint.
+
+    Module Impl_BitAnd_for_Uint.
+      Definition Self (BITS LIMBS : Value.t) : Ty.t :=
+        Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] [].
+
+      Parameter bitand : forall (BITS LIMBS : Value.t), PolymorphicFunction.t.
+
+      Axiom Implements :
+        forall (BITS LIMBS : Value.t),
+          M.IsTraitInstance
+            "core::ops::bit::BitAnd"
+            []
+            [Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []]
+            (Self BITS LIMBS)
+            [("bitand", InstanceField.Method (bitand BITS LIMBS))].
+
+      Instance run_bitand :
+        forall (BITS LIMBS : Usize.t)
+               (x y : Uint.t BITS LIMBS),
+          Run.Trait (bitand (φ BITS) (φ LIMBS)) [] [] [ φ x; φ y ] (Uint.t BITS LIMBS).
+      Proof.
+      Admitted.
+    End Impl_BitAnd_for_Uint.
+
+    Module Impl_BitOr_for_Uint.
+      Definition Self (BITS LIMBS : Value.t) : Ty.t :=
+        Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] [].
+
+      Parameter bitor : forall (BITS LIMBS : Value.t), PolymorphicFunction.t.
+
+      Axiom Implements :
+        forall (BITS LIMBS : Value.t),
+          M.IsTraitInstance
+            "core::ops::bit::BitOr"
+            []
+            [Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []]
+            (Self BITS LIMBS)
+            [("bitor", InstanceField.Method (bitor BITS LIMBS))].
+
+      Instance run_bitor :
+        forall (BITS LIMBS : Usize.t)
+               (x y : Uint.t BITS LIMBS),
+          Run.Trait (bitor (φ BITS) (φ LIMBS)) [] [] [ φ x; φ y ] (Uint.t BITS LIMBS).
+      Proof.
+      Admitted.
+    End Impl_BitOr_for_Uint.
+
+    Module Impl_BitXor_for_Uint.
+      Definition Self (BITS LIMBS : Value.t) : Ty.t :=
+        Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] [].
+
+      Parameter bitxor : forall (BITS LIMBS : Value.t), PolymorphicFunction.t.
+
+      Axiom Implements :
+        forall (BITS LIMBS : Value.t),
+          M.IsTraitInstance
+            "core::ops::bit::BitXor"
+            []
+            [Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] []]
+            (Self BITS LIMBS)
+            [("bitxor", InstanceField.Method (bitxor BITS LIMBS))].
+
+      Instance run_bitxor :
+        forall (BITS LIMBS : Usize.t)
+               (x y : Uint.t BITS LIMBS),
+          Run.Trait (bitxor (φ BITS) (φ LIMBS)) [] [] [ φ x; φ y ] (Uint.t BITS LIMBS).
+      Proof.
+      Admitted.
+    End Impl_BitXor_for_Uint.
+
+    Module Impl_BitNot_for_Uint.
+      Definition Self (BITS LIMBS : Value.t) : Ty.t :=
+        Ty.apply (Ty.path "ruint::Uint") [BITS; LIMBS] [].
+
+      Parameter bitnot : forall (BITS LIMBS : Value.t), PolymorphicFunction.t.
+
+      Axiom Implements :
+        forall (BITS LIMBS : Value.t),
+          M.IsTraitInstance
+            "core::ops::bit::Not"
+            []
+            []
+            (Self BITS LIMBS)
+            [("not", InstanceField.Method (bitnot BITS LIMBS))].
+
+      Instance run_bitnot :
+        forall (BITS LIMBS : Usize.t)
+               (x : Uint.t BITS LIMBS),
+          Run.Trait (bitnot (φ BITS) (φ LIMBS)) [] [] [ φ x ] (Uint.t BITS LIMBS).
+      Proof.
+      Admitted.
+    End Impl_BitNot_for_Uint.
+
 End ruint.
 
 Module alloy_primitives.

CoqOfRust/revm/revm_interpreter/instructions/i256.v

@@ -913,7 +913,7 @@ Module instructions.
           |)))
       | _, _, _ => M.impossible "wrong number of arguments"
       end.
-    
+
     Global Instance Instance_IsFunction_i256_cmp :
       M.IsFunction.Trait "revm_interpreter::instructions::i256::i256_cmp" i256_cmp.
     Admitted.