Formalizing bitwise.rs

CoqOfRust/core/links/intrinsics.v

@@ -16,3 +16,15 @@ 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.
+

CoqOfRust/revm/links/dependencies.v

@@ -68,6 +68,56 @@ Module ruint.
         (array.t U8.t BYTES).
     Admitted.
   End Impl_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.
+
+    Parameter run_from :
+      forall (BITS LIMBS : Usize.t) (value : Usize.t),
+      {{ from (φ BITS) (φ LIMBS) [] [] [ φ value ] 🔽 Self BITS LIMBS }}.
+    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.
+
+      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)) ].
+
+      Definition run_lt :
+        forall (BITS LIMBS : Usize.t),
+        forall (x1 x2 : ruint.Uint.t BITS LIMBS),
+        {{ lt (φ 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.
 End ruint.
 
 Module alloy_primitives.

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

@@ -0,0 +1,75 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.lib.
+Require Import CoqOfRust.links.M.
+Require Import core.links.intrinsics.
+Require Import revm.revm_context_interface.links.host.
+Require revm.links.dependencies.
+Import revm.links.dependencies.ruint.
+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.bitwise.
+
+Import Run.
+(*
+pub fn lt<WIRE: InterpreterTypes, H: Host + ?Sized>(
+    interpreter: &mut Interpreter<WIRE>,
+    _host: &mut H,
+)
+*)
+
+Ltac solve_one_branch e :=
+  constructor;
+  cbn;
+  eapply Run.Rewrite; [
+    repeat erewrite IsTraitAssociatedType_eq by apply e;
+    reflexivity
+  |
+  ];
+  run_symbolic.
+
+Instance run_lt
+    {WIRE H : Set} `{Link WIRE} `{Link H}
+    {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types}
+    (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types)
+    (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types))
+    (_host : Ref.t Pointer.Kind.MutRef H) :
+  Run.Trait
+    instructions.bitwise.lt [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ]
+    unit.
+Proof.
+  constructor.
+  cbn.
+  eapply Run.Rewrite. {
+    repeat erewrite IsTraitAssociatedType_eq by apply run_InterpreterTypes_for_WIRE.
+    reflexivity.
+  }
+  destruct run_InterpreterTypes_for_WIRE.
+  destruct run_StackTrait_for_Stack.
+  destruct popn_top as [popn_top [H_popn_top run_popn_top]].
+  destruct run_LoopControl_for_Control.
+  destruct gas as [gas [H_gas run_gas]].
+  destruct set_instruction_result as [set_instruction_result [H_set_instruction_result run_set_instruction_result]].
+  run_symbolic. {
+    repeat solve_one_branch run_InterpreterTypes_for_WIRE.
+  }
+  eapply Run.CallPrimitiveGetTraitMethod.
+  - eapply IsTraitMethod.Defined.
+    + specialize (Impl_PartialOrd_for_Uint.Implements
+    (Value.Integer IntegerKind.Usize 256)
+    (Value.Integer IntegerKind.Usize 4)).
+      intros.
+      unfold Impl_PartialOrd_for_Uint.Self in H3.
+      apply H3 with (trait_tys := [Ty.apply (Ty.path "ruint::Uint")
+        [Value.Integer IntegerKind.Usize 256;
+         Value.Integer IntegerKind.Usize 4] []]).
+    + simpl.
+      reflexivity.
+  - run_symbolic.
+    + 
+
+Qed.
+
+
+
+