Add states natively to execution monad

ArchSem/GenPromising.v

@@ -140,13 +140,13 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
       tState_init : (* tid *) nat → memoryMap → registerMap → tState;
       tState_regs : tState → registerMap;
       tState_nopromises : tState → bool;
-      (** Intra instruction thread, reset after each instruction *)
+      (** Intra instruction state, reset after each instruction *)
       iis : Type;
       iis_init : iis;
       mEvent : Type;
       handler : (* tid *) nat → memoryMap →
                 fHandler outcome
-                  (stateT (tState * PromMemory.t mEvent * iis) (Exec.t string));
+                  (Exec.t (tState * PromMemory.t mEvent * iis) string);
       allowed_promises : (* tid *) nat → memoryMap → tState →
                          PromMemory.t mEvent → propset mEvent;
       (** I'm not considering that emit_promise can fail or have a
@@ -169,7 +169,7 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
           set.*)
       promise_select :
         (* fuel *) nat -> (* tid *) nat → memoryMap → pModel.(tState) →
-        PromMemory.t pModel.(mEvent) → Exec.t string pModel.(mEvent);
+        PromMemory.t pModel.(mEvent) → Exec.res string pModel.(mEvent);
 
       promise_select_sound :
       ∀ n tid initMem ts mem,
@@ -234,16 +234,17 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
       (** Check if all threads have no outstanding promises *)
       Definition nopromises (ps : t) := fforallb (nopromises_tid ps).
 
+      (* Definition liftSt {St St' E A} (getter : St → St') `{Setter St St' getter} (inner : Exec.t St' E A) : Exec.t St E A. *)
       (** Run on instruction in specific thread by tid *)
-      Definition run_tid (st: t) (tid : fin n) :=
-        let handler := prom.(handler) tid st.(initmem) in
+      Definition run_tid (tid : fin n) : Exec.t t string () :=
+        st ←@{Exec.t t string} mGet;
+        let handler := prom.(handler) tid (st.(initmem)) in
         let sem := (isem.(semantic) (istate tid st)) in
         let init := (tstate tid st, st.(events), prom.(iis_init)) in
-        '(ts, mem, iis, ist) ← cinterp handler sem init;
-        st |> setv (tstate tid) ts
-           |> setv (istate tid) ist
-           |> setv events mem
-           |> mret.
+        ist ← Exec.liftSt
+                (tstate tid ×× events ×× const_getter prom.(iis_init))
+                (cinterp handler sem);
+        msetv (istate tid) ist.
 
       (** Compute the set of allowed promises by a thread indexed by tid *)
       Definition allowed_promises_tid (st : t) (tid : fin n) :=
@@ -258,7 +259,7 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
       (** The inductive stepping relation of the promising model *)
       Inductive step (ps : t) : (t) -> Prop :=
       | SRun (tid : fin n) (ps' : t) :
-        ps' ∈ (run_tid ps tid) → step ps ps'
+        (ps', ()) ∈ (run_tid tid ps) → step ps ps'
       | SPromise (tid : fin n) (event : mEvent) :
         event ∈ allowed_promises_tid ps tid → step ps (promise_tid ps tid event).
 
@@ -302,7 +303,7 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
                         PState.nopromises isem prom finPs
          | Model.Res.Error s =>
              ∃ finPs tid, rtc (PState.step isem prom) initPs finPs ∧
-                            Error s ∈ PState.run_tid isem prom finPs tid
+                            Error s ∈ PState.run_tid isem prom tid finPs
          | _ => False
          end]}.
 
@@ -320,31 +321,40 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
     Local Notation iState := isem.(isa_state).
     Local Notation t := (t iState tState mEvent n).
 
-    (** Get a list of possible promising for a thread by tid *)
+    (** Get a list of possible promises for a thread by tid *)
     Definition promise_select_tid (fuel : nat) (st : t)
-        (tid : fin n) : Exec.t string mEvent :=
+        (tid : fin n) : Exec.res string mEvent :=
       prom.(promise_select) n tid (initmem st) (tstate tid st) (events st).
 
     (** Take any promising step for that tid and promise it *)
-    Definition cpromise_tid (fuel : nat) (st : t) (tid : fin n)
-      : Exec.t string t :=
-      ev ← promise_select_tid fuel st tid;
-      mret $ promise_tid isem prom st tid ev.
+    Program Definition cpromise_tid (fuel : nat) (tid : fin n)
+      : Exec.t t string () :=
+    λ st,
+      let res_st :=
+        ev ← promise_select_tid fuel st tid;
+        mret $ promise_tid isem prom st tid ev
+      in
+        Exec.make ((.,()) <$> res_st.(Exec.results)) ((st,.) <$> res_st.(Exec.errors)).
 
     (** Run any possible step, this is the most exhaustive and expensive kind of
         search but it is obviously correct. If a thread has reached termination
         no progress is made in the thread (either instruction running or
         promises *)
-    Definition run_step (fuel : nat) (st : t) :=
+    (* TODO make if only on bool *)
+    Program Definition run_step (fuel : nat) : Exec.t t string () :=
+      st ← mGet;
       tid ← mchoose n;
       if terminated_tid isem prom term st tid then mdiscard
-      else Exec.merge (run_tid isem prom st tid) (cpromise_tid fuel st tid).
+      else
+        promise ← mchoosel (enum bool);
+        if (promise : bool) then cpromise_tid fuel tid else run_tid isem prom tid.
 
     (** The type of final promising state return by run *)
     Definition final := { x : t | terminated isem prom term x }.
 
     Definition make_final (p : t) := exist (terminated isem prom term) p.
 
+
     (** Convert a final promising state to a generic final state *)
     Program Definition to_final_MState (f : final) : MState.final n :=
       {|MState.istate :=
@@ -356,14 +366,15 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
 
     (** Computational evaluate all the possible allowed final states according
         to the promising model prom starting from st *)
-    Program Fixpoint run (fuel : nat) (st : t) : Exec.t string final :=
+    Program Fixpoint run (fuel : nat) : Exec.t t string final :=
       match fuel with
       | 0%nat => mthrow "not enough fuel"
       | S fuel =>
+          st ← mGet;
           if dec $ terminated isem prom term st then mret (make_final st _)
           else
-            nextSt ← run_step fuel st;
-            run fuel st
+            nextSt ← run_step fuel;
+            run fuel
       end.
     Solve All Obligations with naive_solver.
     End CPS.
@@ -373,13 +384,13 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
 
 
   (** Create a computational model from an ISA model and promising model *)
-    Definition Promising_to_Modelc {isem : iSem} (prom : BasicExecutablePM)
+(* TODO: Definition Promising_to_Modelc {isem : iSem} (prom : BasicExecutablePM)
       (fuel : nat) : Model.c ∅ :=
       fun n (initMs : MState.init n) =>
         let initPs := PState.from_MState isem prom initMs in
         Model.Res.from_exec
           $ CPState.to_final_MState
-          <$> CPState.run isem prom initMs.(MState.termCond) fuel initPs.
+          <$> CPState.run isem prom initMs.(MState.termCond) fuel initPs. *)
 
     (* TODO state some soundness lemma between Promising_to_Modelnc and
         Promising_Modelc *)

ArchSem/TermModels.v

@@ -281,9 +281,9 @@ Module TermModels (IWA : InterfaceWithArch). (* to be imported *)
       End MR.
       Arguments t : clear implicits.
 
-      Definition from_exec {n} (e : Exec.t string (MState.final n)) :
+      Definition from_exec {St n} (e : Exec.t St string (MState.final n)) (st : St) :
           listset (t ∅ n) :=
-        e |> Exec.to_result_list |$> from_result |> Listset.
+        e st |> Exec.to_stateful_result_list |$> snd |$> from_result |> Listset.
 
     End Res.
 

ArchSemArm/ArmSeqModel.v

@@ -64,7 +64,7 @@ Record seq_state := {
 Global Instance eta_seq_state : Settable seq_state :=
   settable! Build_seq_state <initSt;mem;regs>.
 
-Notation seqmon := (stateT seq_state (Exec.t string)).
+Notation seqmon := (Exec.t seq_state string).
 
 Definition read_reg_seq_state (reg : reg) (seqst : seq_state) : regval :=
   if (seqst.(regs) !! reg) is Some v
@@ -161,14 +161,6 @@ Fixpoint sequential_model_seqmon (fuel : nat) (isem : iMon ())
     else sequential_model_seqmon fuel isem
   else mthrow "Out of fuel".
 
-(** Run the model on given initial MState and an initially blank sequential state.
-    The sequential state gets discarded and only the final state is returned *)
-Definition sequential_model_exec (fuel : nat) (isem : iMon ())
-  (initSt : MState.init 1) : Exec.t string (MState.final 1) :=
-  '(_, fs) ← sequential_model_seqmon fuel isem
-             {| initSt := initSt; regs := ∅; mem := ∅ |};
-  mret fs.
-
 (** Top-level one-threaded sequential model function that takes fuel (guaranteed
     termination) and an instruction monad, and returns a computational set of
     all possible final states. *)
@@ -177,8 +169,9 @@ Definition sequential_modelc (fuel : nat) (isem : iMon ()) : (Model.c ∅) :=
   match n with
   | 1 => λ initSt : MState.init 1,
            Listset
-            (sequential_model_exec fuel isem initSt
+            (sequential_model_seqmon fuel isem {| initSt := initSt; regs := ∅; mem := ∅ |}
              |> Exec.to_result_list
+             |$> snd
              |$> Model.Res.from_result)
   | _ => λ _, mret (Model.Res.Error "Exptected one thread")
   end.

Common/CDestruct.v

@@ -291,6 +291,9 @@ Global Hint Extern 3 (ObvTrue _) =>
 Global Hint Extern 4 (ObvTrue _) =>
          constructor; symmetry; assumption : typeclass_instances.
 
+#[global] Instance obv_true_not_False : ObvTrue (¬ False).
+Proof. now tcclean. Qed.
+
 (** * CDestruct
 
 See the top of the file comment for details about what [cdestruct] does. *)
@@ -883,3 +886,23 @@ Proof. tcclean. tauto. Qed.
 Instance cdestruct_not_or_and b P Q :
   CDestrSimpl b (¬ (P ∨ Q)) (¬ P ∧ ¬ Q).
 Proof. tcclean. naive_solver. Qed.
+
+Instance cdestruct_is_Some {A} (x : option A) :
+  CDestrSimpl false (is_Some x) (∃ y, x = Some y).
+Proof. tcclean. naive_solver. Qed.
+
+Instance cdestruct_or_False_l b P :
+  CDestrSimpl b (False ∨ P) P.
+Proof. tcclean. naive_solver. Qed.
+
+Instance cdestruct_or_False_r b P :
+  CDestrSimpl b (P ∨ False) P.
+Proof. tcclean. naive_solver. Qed.
+
+Instance cdestruct_and_True_l b P :
+  CDestrSimpl b (True ∧ P) P.
+Proof. tcclean. naive_solver. Qed.
+
+Instance cdestruct_and_True_r b P :
+  CDestrSimpl b (P ∧ True) P.
+Proof. tcclean. naive_solver. Qed.

Common/CList.v

@@ -42,7 +42,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
-Require Import CBase CBool CMaps CArith.
+Require Import CBase CBool CMaps CArith CDestruct.
 Require Import Options.
 From stdpp Require Import base.
 From stdpp Require Export list.
@@ -70,6 +70,10 @@ Proof. tcclean. unfold mret, list_ret. set_solver. Qed.
 
 #[export] Instance list_elements {A} : Elements A (list A) := λ x, x.
 
+#[global] Instance cdestruct_list_elements b {A} x (l : list A) :
+  CDestrSimpl b (x ∈ elements l) (x ∈ l).
+Proof. tcclean. done. Qed.
+
 (** * List simplification *)
 
 #[global] Hint Rewrite <- app_assoc : list.
@@ -357,10 +361,28 @@ Lemma fold_left_inv {C B} (I : C → list B → Prop) (f : C → B → C)
   (I i l)
   → (∀ (a : C) (x : B) (tl : list B), x ∈ l → I a (x :: tl) → I (f a x) tl)
   → I (fold_left f l i) [].
+Proof.
   generalize dependent i.
   induction l; sauto lq:on.
 Qed.
 
+Lemma fold_left_inv_complete_list {C B} (I : C → list B → list B → Prop) (f : C → B → C)
+    (l l' : list B) (i : C) :
+  (I i l [])
+  → (∀ (a : C) (x : B) (tl strt : list B), x ∈ l → I a (x :: tl) strt → I (f a x) tl (x :: strt))
+  → I (fold_left f l i) [] (rev l).
+Proof.
+  replace (rev l) with (rev l ++ []) by by rewrite app_nil_r.
+  generalize (@nil B) at 1 3.
+  revert dependent i.
+  induction l.
+  1: done.
+  cdestruct |- ***.
+  rewrite <- app_assoc.
+  eapply IHl.
+  all: intros; eapply H0; set_solver.
+Qed.
+
 (** Tries to find a fold_left in the goal and pose the proofs of the
 [fold_left_inv] on that one *)
 Tactic Notation "fold_left_inv_pose" uconstr(I) "as" simple_intropattern(pat) :=
@@ -380,6 +402,7 @@ Lemma fold_left_inv_ND {C B} (I : C → list B → Prop) (f : C → B → C)
   → (I i l)
   → (∀ (a : C) (x : B) (t : list B), x ∈ l → x ∉ t → I a (x :: t) → I (f a x) t)
   → I (fold_left f l i) [].
+Proof.
   generalize dependent i.
   induction l; sauto lq:on.
 Qed.

Common/CResult.v

@@ -44,6 +44,7 @@
 
 Require Import CBase.
 Require Import Options.
+Require Import CDestruct.
 From stdpp Require Import option.
 
 (** The point of this module is to keep the [sum] type symmetric and use this to
@@ -135,6 +136,16 @@ Section Result.
       naive_solver.
   Defined.
 
+  #[export] Instance cdestruct_is_Ok r :
+    CDestrSimpl false (is_Ok r) (∃ o, r = Ok o).
+  Proof. tcclean. now unfold is_Ok. Qed.
+
+  #[export] Instance obv_true_is_Ok_Ok x : ObvTrue (is_Ok (Ok x)).
+  Proof. tcclean. unfold is_Ok. eauto. Qed.
+
+  #[export] Instance obv_false_is_Ok_Error x : ObvFalse (is_Ok (Error x)).
+  Proof. tcclean. unfold is_Ok. naive_solver. Qed.
+
   (** Unpack a result into any monad that supports that error type *)
   Definition unpack_result `{MThrow E M, MRet M} (r : result) : M A :=
     match r with