simulations: add simulation of the add instruction

Author: clarus

CoqOfRust/links/M.v

@@ -1017,14 +1017,14 @@ Module LowM.
   Inductive t (R Output : Set) : Set :=
   | Pure (value : Output.t R Output)
   | CallPrimitive {A : Set} (primitive : Primitive.t A) (k : A -> t R Output)
-  | Call {A : Set} (e : t A A) (k : SuccessOrPanic.t A -> t R Output)
+  | Call {A : Set} `{Link A} {e : M} (run : {{ e 🔽 A, A }}) (k : SuccessOrPanic.t A -> t R Output)
   | LetAlloc {A : Set} `{Link A}
       (e : t R A)
       (k : Output.t R (Ref.t Pointer.Kind.Raw A) -> t R Output)
   | Loop {A : Set} (body : t R A) (k : Output.t R A -> t R Output).
   Arguments Pure {_ _}.
   Arguments CallPrimitive {_ _ _}.
-  Arguments Call {_ _ _}.
+  Arguments Call {_ _ _ _ _}.
   Arguments LetAlloc {_ _ _ _}.
   Arguments Loop {_ _ _}.
 End LowM.
@@ -1123,7 +1123,7 @@ Proof.
   }
   { (* CallClosure *)
     eapply (LowM.Call (A := Output')). {
-      exact (evaluate _ _ _ _ _ run).
+      exact run.
     }
     intros output'; eapply evaluate.
     match goal with

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

@@ -6,8 +6,10 @@ Require Import revm.revm_interpreter.links.interpreter_types.
 Require Import revm.revm_interpreter.simulations.gas.
 Require Import revm.revm_interpreter.simulations.interpreter_types.
 Require Import revm.revm_interpreter.instructions.links.arithmetic.
+Require Import ruint.simulations.add.
 
 Import Impl_Gas.
+Import add.Impl_Uint.
 
 Instance run_add Stack
     {WIRE H : Set} `{Link WIRE} `{Link H}
@@ -20,69 +22,8 @@ Proof.
   constructor.
   destruct run_InterpreterTypes_for_WIRE.
   destruct run_StackTrait_for_Stack, run_LoopControl_for_Control.
-  (* destruct popn_top as [? []].
-  destruct gas as [? []].
-  destruct set_instruction_result as [? []]. *)
-  Time simulate.
-  { Time simulate_destruct; simulate.
-    match goal with
-    | H : _ |- Run.Trait ?Stack (_ ?x1 ?x2) =>
-      apply (H Stack x1 x2)
-    end.
-  }
-    progress cbn in *.
-    idtac.
-    (* destruct link; cbn in *.
-    destruct run_StackTrait_for_Stack, run_LoopControl_for_Control; cbn in *. *)
-    generalize set_instruction_result; clear; intros.
-    match goal with
-    | |- Run.Trait _ (?f _ _) =>
-      set (f' := f) in |- *
-    end.
-    destruct WIRE_types; cbn in *.
-    destruct link, run_LoopControl_for_Control, set_instruction_result0; cbn in *.
-    progress fold f' in set_instruction_result.
-    unfold InterpreterTypes.Types.IsLinkControl in *; cbn in *.
-    with_strategy transparent [Φ φ] apply set_instruction_result.
-    progress fold f' in set_instruction_result.
-    apply set_instruction_result.
-    match goal with
-    | H : forall _ _ _, ?f _ _ _ = _ |- _ =>
-      specialize (H _ _ _ eq_refl)
-    end.
-    Check set_instruction_result.
-    refine (set_instruction_result _ _ _).
-    best.
-    match goal with.
-    dependent apply set_instruction_result.
-    epose proof (set_instruction_result Stack
-      (* ((Ref.cast_to Pointer.Kind.MutRef
-      {|
-        Ref.core :=
-          SubPointer.Runner.apply interpreter.(Ref.core)
-            Interpreter.get_control
-      |})) *)
-      (* instruction_result.InstructionResult.OutOfGas *)
-    ).
-    apply H5.
-    apply set_instruction_result.
-    typeclasses eauto.
-    match goal with
-    | |- context[if ?condition then _ else _] =>
-      let condition' := eval cbv in condition in
-      change condition with condition'
-    end.
-    Time match goal with
-    | |- context[if ?condition then _ else _] =>
-      destruct condition
-    end.
-    { Show.
-    simulate_reduce.
-
-  }
-  4: { intros. apply Impl_Gas.run_record_cost.
-    cbn in output.
-    Show.
+  simulate.
+Defined.
 
 (*
 Require Import revm.interpreter.links.interpreter.

CoqOfRust/ruint/simulations/add.v

@@ -0,0 +1,18 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.simulations.M.
+Require Import ruint.links.add.
+Require Import ruint.links.lib.
+
+Module Impl_Uint.
+  (* Uint<BITS, LIMBS> *)
+  Definition Self (BITS LIMBS : Usize.t) : Set :=
+    Uint.t BITS LIMBS.
+
+  Instance run_wrapping_add Stack
+      (BITS LIMBS : Usize.t)
+      (x1 x2 : Self BITS LIMBS) :
+    Run.Trait Stack
+      (Impl_Uint.run_wrapping_add BITS LIMBS x1 x2).
+  Admitted.
+End Impl_Uint.

CoqOfRust/simulations/M.v

@@ -613,19 +613,25 @@ Module Stack.
         end
       end.
 
+    Axiom admit_access_for_now :
+      forall {A : Set} `{Link A} (Stack : Stack.t) (ref_core : Ref.Core.t A),
+      t Stack ref_core.
+
     Ltac infer :=
       cbn ||
       match goal with
       | |- t _ (SubPointer.Runner.apply _ ?r) =>
         apply (runner r)
       end ||
-      assumption.
+      assumption ||
+      apply Stack.CanAccess.Immediate ||
+      apply admit_access_for_now.
   End CanAccess.
 End Stack.
 
 (** Here we define an execution mode where we keep dynamic cast to retrieve data from the stack. In
     practice, these casts should always be correct as the original Rust code was well typed. *)
-Module StackM.
+(* Module StackM.
   Inductive t (A : Set) : Set :=
   | Pure (value : A)
   | GetCanAccess {B : Set} `{Link B}
@@ -747,9 +753,8 @@ Module Run.
     {{ StackM.GetCanAccess Stack ref_core k 🌲 result }}
 
   where "{{ e 🌲 result }}" := (t result e).
-End Run.
+End Run. *)
 
-(*
 Module Run.
   Reserved Notation "{{ StackIn 🌲 e }}".
 
@@ -927,17 +932,29 @@ Ltac simulate_one_step :=
   (apply Run.StateRead; [repeat Stack.CanAccess.infer | intros]) ||
   (apply Run.StateWrite; [repeat Stack.CanAccess.infer |]) ||
   simulate_get_sub_pointer ||
-  (apply Run.Call; [unshelve eapply Run.simulation | intros []]) ||
+  (apply Run.Call; [
+    (
+      unshelve eapply Run.simulation;
+      try match goal with
+      | H : _ |- Run.Trait ?Stack (_ ?x1) =>
+        apply (H Stack x1)
+      | H : _ |- Run.Trait ?Stack (_ ?x1 ?x2) =>
+        apply (H Stack x1 x2)
+      | H : _ |- Run.Trait ?Stack (_ ?x1 ?x2 ?x3) =>
+        apply (H Stack x1 x2 x3)
+      end
+    ) |
+    intros []
+  ]) ||
   (apply Run.LetAlloc; [|intros []]).
 
-Ltac simulate :=
-  progress repeat simulate_one_step.
-
 Ltac simulate_destruct :=
   match goal with
   | |- {{ _ 🌲 ?e }} =>
     match e with
     | context [match ?e with _ => _ end] => destruct e
     end
   end.
- *)
+
+Ltac simulate :=
+  progress repeat (simulate_one_step || simulate_destruct).