From 3cc8a0fbcb32d65426989e0569583899766cb8cf Mon Sep 17 00:00:00 2001
From: Yeji Han <yeji.han@sf.snu.ac.kr>
Date: Sun, 12 Oct 2025 00:27:21 +0900
Subject: [PATCH 1/4] Implement Promise-First optimization

Fix VM_promising_exe

Pass MP, MPDMBS tests with address translation
---
 ArchSem/GenPromising.v             | 130 ++++++++++++++++++++------
 ArchSemArm/UMPromising.v           | 143 ++++++++++++++++++++--------
 ArchSemArm/VMPromising.v           | 144 +++++++++++++++++++++--------
 ArchSemArm/tests/UMPromisingTest.v |  46 ++++++++-
 ArchSemArm/tests/VMPromisingTest.v | 110 +++++++++++++++++-----
 5 files changed, 436 insertions(+), 137 deletions(-)

diff --git a/ArchSem/GenPromising.v b/ArchSem/GenPromising.v
index c9c4839..10f00ef 100644
--- a/ArchSem/GenPromising.v
+++ b/ArchSem/GenPromising.v
@@ -170,27 +170,38 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
       it generic *)
   Structure BasicExecutablePM := {
       pModel :> PromisingModel;
-      (** try to compute ALL allowed promises, if that is not possible (not
-          enough fuel) then fail with error message.
 
-          Soundness and completeness proofs are required to show that when not
-          failing, promise_select effectively computes the allowed_promises
-          set.*)
-      promise_select :
+      enumerate_promises_and_terminal_states :
         (* fuel *) nat → (* tid *) nat →
         (* termination condition *) (registerMap → bool) →
         memoryMap → pModel.(tState) → PromMemory.t pModel.(mEvent) →
-        Exec.res string pModel.(mEvent);
+        result string (list pModel.(mEvent) * list pModel.(tState));
 
       promise_select_sound :
-      ∀ fuel tid term initMem ts mem,
-        ∀ ev ∈ (promise_select fuel tid term initMem ts mem),
-          ev ∈ pModel.(allowed_promises) tid initMem ts mem;
+        ∀ fuel tid term initMem ts mem promises tstates,
+          Ok (promises, tstates) =
+            enumerate_promises_and_terminal_states fuel tid term initMem ts mem →
+          ∀ ev ∈ promises, ev ∈ pModel.(allowed_promises) tid initMem ts mem;
+
       promise_select_complete :
-      ∀ fuel tid term initMem ts mem,
-        ¬ Exec.has_error (promise_select fuel tid term initMem ts mem) →
-        ∀ ev ∈ pModel.(allowed_promises) tid initMem ts mem,
-          ev ∈ promise_select fuel tid term initMem ts mem
+        ∀ fuel tid term initMem ts mem promises tstates,
+          Ok (promises, tstates) =
+            enumerate_promises_and_terminal_states fuel tid term initMem ts mem →
+          ∀ ev ∈ pModel.(allowed_promises) tid initMem ts mem, ev ∈ promises;
+
+      terminal_state_no_outstanding_promise :
+        ∀ fuel tid term initMem ts mem promises tstates,
+          Ok (promises, tstates) =
+            enumerate_promises_and_terminal_states fuel tid term initMem ts mem →
+          ∀ tts ∈ tstates, pModel.(tState_nopromises) tts;
+
+      terminal_state_is_terminated :
+        ∀ fuel tid term initMem ts mem promises tstates,
+          Ok (promises, tstates) =
+            enumerate_promises_and_terminal_states fuel tid term initMem ts mem →
+          ∀ tts ∈ tstates, term (pModel.(tState_regs) tts);
+
+      (* TODO: add terminal_state_is_reachable *)
     }.
   Arguments BasicExecutablePM : clear implicits.
 
@@ -328,10 +339,24 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
     Local Notation mEvent := (mEvent prom).
     Local Notation t := (t tState mEvent n).
 
+    (** The type of final promising state return by run *)
+    Definition final := { x : t | terminated prom term x }.
+
+    Definition make_final (p : t) := exist (terminated prom term) p.
+
+    (** Convert a final promising state to a generic final state *)
+    Program Definition to_final_archState (f : final) :
+        {s & archState.is_terminated term s} :=
+      existT (to_archState prom f) _.
+    Solve All Obligations with
+      hauto unfold:terminated unfold:archState.is_terminated l:on db:vec, brefl.
+
     (** Get a list of possible promises for a thread by tid *)
     Definition promise_select_tid (fuel : nat) (st : t)
         (tid : fin n) : Exec.res string mEvent :=
-      prom.(promise_select) fuel tid (term tid) (initmem st) (tstate tid st) (events st).
+      '(promises, _) ← mlift $ prom.(enumerate_promises_and_terminal_states)
+                        fuel tid (term tid) (initmem st) (tstate tid st) (events st);
+      mchoosel promises.
 
     (** Take any promising step for that tid and promise it *)
     Definition cpromise_tid (fuel : nat) (tid : fin n)
@@ -355,19 +380,6 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
         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 prom term x }.
-
-    Definition make_final (p : t) := exist (terminated prom term) p.
-
-
-    (** Convert a final promising state to a generic final state *)
-    Program Definition to_final_archState (f : final) :
-        {s & archState.is_terminated term s} :=
-      existT (to_archState prom f) _.
-    Solve All Obligations with
-      hauto unfold:terminated unfold:archState.is_terminated l:on db:vec, brefl.
-
     (** Computational evaluate all the possible allowed final states according
         to the promising model prom starting from st *)
     Fixpoint run (fuel : nat) : Exec.t t string final :=
@@ -378,6 +390,56 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
           run_step (S fuel);;
           run fuel
         else mthrow "Could not finish running within the size of the fuel".
+
+    (** Explore all possible promise-based executions across all threads. *)
+    Fixpoint prune_promises_and_states (fuel_per_tid fuel : nat)
+        (finals : list final) : Exec.t t string (list final) :=
+      if fuel is S fuel then
+        st ← mGet;
+        (* Find out next possible promises or terminating states at the current thread *)
+        executions ←
+          for (tid : fin n) in enum (fin n) do
+            '(promises_per_tid, tstates_per_tid) ←
+              mlift $ prom.(enumerate_promises_and_terminal_states)
+                        fuel_per_tid tid (term tid) (initmem st) (tstate tid st) (events st);
+            mret (map (λ ev, (ev, tid)) promises_per_tid, tstates_per_tid)
+          end;
+
+        (* Compute cartesian products of the possible thread states *)
+        let tstates_sys :=
+          fold_left (λ partial_sts tstates_tid,
+            List.flat_map (λ tstate,
+              if is_emptyb partial_sts then [[tstate]]
+              else map (λ partial_st, partial_st ++ [tstate]) partial_sts
+            ) tstates_tid
+          ) (map snd executions) [] in
+        let new_finals :=
+          omap (λ tstates,
+            if (list_to_vec_n n tstates) is Some tstates_vec then
+              let st := Make tstates_vec st.(PState.initmem) st.(PState.events) in
+              if decide $ terminated prom term st is left pt
+              then Some (make_final st pt)
+              else None
+            else None
+          ) tstates_sys in
+
+        (* Non-deterministically choose the next promise and the tid for pruning *)
+        let promises_all := List.concat (map fst executions) in
+        if is_emptyb promises_all then
+          mret (new_finals ++ finals)
+        else
+          '(next_ev, tid) ← mchoosel promises_all;
+          mSet (λ st, promise_tid prom st tid next_ev);;
+          prune_promises_and_states fuel_per_tid fuel (new_finals ++ finals)
+      else mret finals.
+
+    (** Computational evaluate all the possible allowed final states according
+        to the promising model prom starting from st
+        with promise-first optimization *)
+    Definition run_promise_first (fuel : nat) : Exec.t t string final :=
+      finals ← prune_promises_and_states fuel fuel [];
+      mchoosel finals.
+
     End CPS.
     Arguments to_final_archState {_ _ _}.
   End CPState.
@@ -385,12 +447,22 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
   (** Create a computational model from an ISA model and promising model *)
   Definition Promising_to_Modelc (isem : iMon ()) (prom : BasicExecutablePM)
       (fuel : nat) : archModel.c ∅ :=
-    fun n term (initMs : archState n) =>
+    λ n term (initMs : archState n),
       PState.from_archState prom initMs |>
       archModel.Res.from_exec
         $ CPState.to_final_archState
         <$> CPState.run isem prom term fuel.
 
+  (** Create a computational model from an ISA model and promising model
+      with promise-free optimization *)
+  Definition Promising_to_Modelc_pf (isem : iMon ()) (prom : BasicExecutablePM)
+      (fuel : nat) : archModel.c ∅ :=
+    λ n term (initMs : archState n),
+      PState.from_archState prom initMs |>
+      archModel.Res.from_exec
+        $ CPState.to_final_archState
+        <$> CPState.run_promise_first prom term fuel.
+
     (* TODO state some soundness lemma between Promising_to_Modelnc and
         Promising_Modelc *)
 
diff --git a/ArchSemArm/UMPromising.v b/ArchSemArm/UMPromising.v
index 7616dc9..e910140 100644
--- a/ArchSemArm/UMPromising.v
+++ b/ArchSemArm/UMPromising.v
@@ -416,7 +416,7 @@ Definition read_fwd_view (macc : mem_acc) (f : FwdItem.t) :=
 Definition read_mem (loc : Loc.t) (vaddr : view) (macc : mem_acc)
            (init : Memory.initial) (mem : Memory.t) :
     Exec.t TState.t string (view * val) :=
-  guard_or "Atomic RMV unsupported" (¬ (is_atomic_rmw macc));;
+  guard_or "Atomic RMW unsupported" (¬ (is_atomic_rmw macc));;
   ts ← mGet;
   let vbob := ts.(TState.vdmb) ⊔ ts.(TState.visb) ⊔ ts.(TState.vacq)
                 (* SC Acquire loads are ordered after Release stores *)
@@ -457,15 +457,18 @@ Definition read_mem4 (addr : address) (macc : mem_acc) (init : Memory.initial) :
     This may mutate memory if no existing promise can be fullfilled *)
 Definition write_mem (tid : nat) (loc : Loc.t) (vdata : view)
            (macc : mem_acc) (mem : Memory.t)
-           (data : val) : Exec.t TState.t string (Memory.t * view * option view):=
+           (data : val) (mem_update : bool) :
+          Exec.t TState.t string (Memory.t * view * option view):=
   let msg := Msg.make tid loc data in
   let is_release := is_rel_acq macc in
   ts ← mGet;
-  let '(time, mem, new_promise) :=
+  '(time, mem, new_promise) ←
     match Memory.fulfill msg (TState.prom ts) mem with
-    | Some t => (t, mem, false)
-    | None => (Memory.promise msg mem, true)
-    end in
+    | Some t => mret (t, mem, false)
+    | None =>
+      if mem_update then mret (Memory.promise msg mem, true)
+      else mdiscard
+    end;
   let vbob :=
     ts.(TState.vdmbst) ⊔ ts.(TState.vdmb) ⊔ ts.(TState.visb) ⊔ ts.(TState.vacq)
     ⊔ view_if is_release (ts.(TState.vrd) ⊔ ts.(TState.vwr)) in
@@ -475,8 +478,10 @@ Definition write_mem (tid : nat) (loc : Loc.t) (vdata : view)
   mSet $ TState.update_coh loc time;;
   mSet $ TState.update TState.vwr time;;
   mSet $ TState.update TState.vrel (view_if is_release time);;
-  mret (mem, time, (if new_promise then Some vpre else None)).
-
+  mret $ match new_promise with
+        | true => (mem, time, Some vpre)
+        | false => (mem, time, None)
+        end.
 
 (** Tries to perform a memory write.
 
@@ -487,12 +492,12 @@ Definition write_mem (tid : nat) (loc : Loc.t) (vdata : view)
     return value indicate the success (true for success, false for error) *)
 Definition write_mem_xcl (tid : nat) (loc : Loc.t)
            (vdata : view) (macc : mem_acc)
-           (mem : Memory.t) (data : val)
+           (mem : Memory.t) (data : val) (mem_update : bool)
   : Exec.t TState.t string (Memory.t * option view) :=
-  guard_or "Atomic RMV unsupported" (¬ (is_atomic_rmw macc));;
+  guard_or "Atomic RMW unsupported" (¬ (is_atomic_rmw macc));;
   let xcl := is_exclusive macc in
   if xcl then
-    '(mem, time, vpre_opt) ← write_mem tid loc vdata macc mem data;
+    '(mem, time, vpre_opt) ← write_mem tid loc vdata macc mem data mem_update;
     ts ← mGet;
     match TState.xclb ts with
     | None => mdiscard
@@ -503,7 +508,7 @@ Definition write_mem_xcl (tid : nat) (loc : Loc.t)
     mSet TState.clear_xclb;;
     mret (mem, vpre_opt)
   else
-    '(mem, time, vpre_opt) ← write_mem tid loc vdata macc mem data;
+    '(mem, time, vpre_opt) ← write_mem tid loc vdata macc mem data mem_update;
     mSet $ TState.set_fwdb loc (FwdItem.make time vdata false);;
     mret (mem, vpre_opt).
 
@@ -533,9 +538,9 @@ End IIS.
 Section RunOutcome.
   Context (tid : nat) (initmem : memoryMap).
 
-  Equations run_outcome (out : outcome) :
+  Equations run_outcome (out : outcome) (mem_update : bool) :
       Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out * option view) :=
-  | RegWrite reg racc val =>
+  | RegWrite reg racc val, mem_update =>
       guard_or "Non trivial reg access types unsupported" (racc = None);;
       vreg ← mget (IIS.strict ∘ PPState.iis);
       vreg' ←
@@ -549,14 +554,14 @@ Section RunOutcome.
         TState.set_reg reg (val, vreg') ts;
       msetv PPState.state nts;;
       mret ((), None)
-  | RegRead reg racc =>
+  | RegRead reg racc, mem_update =>
       guard_or "Non trivial reg access types unsupported" (racc = None);;
       ts ← mget PPState.state;
       '(val, view) ← othrow "Register isn't mapped can't read" $
           dmap_lookup reg ts.(TState.regs);
     mset PPState.iis $ IIS.add view;;
     mret (val, None)
-  | MemRead (MemReq.make macc addr addr_space 8 0) =>
+  | MemRead (MemReq.make macc addr addr_space 8 0), mem_update =>
       guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
       loc ← othrow "PA not supported" $ Loc.from_addr addr;
       if is_ifetch macc then
@@ -570,28 +575,28 @@ Section RunOutcome.
         mset PPState.iis $ IIS.add view;;
         mret (Ok (val, bv_0 0), None)
       else mthrow "Read is not explicit or ifetch"
-  | MemRead (MemReq.make macc addr addr_space 4 0) => (* ifetch *)
+  | MemRead (MemReq.make macc addr addr_space 4 0), mem_update => (* ifetch *)
       guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
       let initmem := Memory.initial_from_memMap initmem in
       opcode ← Exec.liftSt PPState.mem $ read_mem4 addr macc initmem;
       mret (Ok (opcode, 0%bv), None)
-  | MemRead _ => mthrow "Memory read of size other than 8 and 4"
-  | MemWriteAddrAnnounce _ =>
+  | MemRead _, mem_update => mthrow "Memory read of size other than 8 and 4"
+  | MemWriteAddrAnnounce _, mem_update =>
       vaddr ← mget (IIS.strict ∘ PPState.iis);
       mset PPState.state $ TState.update TState.vcap vaddr;;
       mret ((), None)
-  | MemWrite (MemReq.make macc addr addr_space 8 0) val tags =>
+  | MemWrite (MemReq.make macc addr addr_space 8 0) val tags, mem_update =>
       guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
       addr ← othrow "PA not supported" $ Loc.from_addr addr;
       if is_explicit macc then
         mem ← mget PPState.mem;
         vdata ← mget (IIS.strict ∘ PPState.iis);
         '(mem, vpre_opt) ← Exec.liftSt PPState.state
-                $ write_mem_xcl tid addr vdata macc mem val;
+                $ write_mem_xcl tid addr vdata macc mem val mem_update;
         msetv PPState.mem mem;;
         mret (Ok (), vpre_opt)
       else mthrow "Unsupported non-explicit write"
-  | Barrier (Barrier_DMB dmb) => (* dmb *)
+  | Barrier (Barrier_DMB dmb), mem_update => (* dmb *)
       ts ← mget PPState.state;
       match dmb.(DxB_types) with
       | MBReqTypes_All (* dmb sy *) =>
@@ -602,17 +607,16 @@ Section RunOutcome.
           mset PPState.state $ TState.update TState.vdmbst ts.(TState.vwr)
       end;;
       mret ((), None)
-  | Barrier (Barrier_ISB ()) => (* isb *)
+  | Barrier (Barrier_ISB ()), mem_update => (* isb *)
       ts ← mget PPState.state;
     mset PPState.state $ TState.update TState.visb (TState.vcap ts);;
     mret ((), None)
-  | GenericFail s => mthrow ("Instruction failure: " ++ s)%string
-  | _ => mthrow "Unsupported outcome".
+  | GenericFail s, mem_update => mthrow ("Instruction failure: " ++ s)%string
+  | _, _ => mthrow "Unsupported outcome".
 
   Definition run_outcome' (out : outcome) :
       Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out) :=
-    run_outcome out |$> fst.
-
+    run_outcome out true |$> fst.
 End RunOutcome.
 
 Module CProm.
@@ -651,7 +655,7 @@ Section ComputeProm.
               (base : view)
               (out : outcome) :
         Exec.t (CProm.t * PPState.t TState.t Msg.t IIS.t) string (eff_ret out) :=
-    '(res, vpre_opt) ← Exec.liftSt snd $ run_outcome tid initmem out;
+    '(res, vpre_opt) ← Exec.liftSt snd $ run_outcome tid initmem out true;
     if vpre_opt is Some vpre then
       mem ← mget (PPState.mem ∘ snd);
       mset fst (CProm.add_if mem vpre base);;
@@ -659,11 +663,11 @@ Section ComputeProm.
     else
       mret res.
 
-  Fixpoint runSt_to_termination
+  Fixpoint run_to_termination_promise
                       (isem : iMon ())
                       (fuel : nat)
-                      (base : nat)
-      : Exec.t (CProm.t * PPState.t TState.t Msg.t IIS.t) string bool :=
+                      (base : nat) :
+      Exec.t (CProm.t * PPState.t TState.t Msg.t IIS.t) string bool :=
     match fuel with
     | 0%nat =>
       ts ← mget (PPState.state ∘ snd);
@@ -675,20 +679,62 @@ Section ComputeProm.
       if term (TState.reg_map ts) then
         mret true
       else
-        runSt_to_termination isem fuel base
+        run_to_termination_promise isem fuel base
     end.
 
-  Definition run_to_termination (isem : iMon ())
+    Definition run_to_termination (isem : iMon ())
+                                (fuel : nat)
+                                (ts : TState.t)
+                                (mem : Memory.t) :
+      result string (list Msg.t * list TState.t) :=
+    let base := List.length mem in
+    let res := Exec.results $
+      run_to_termination_promise isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
+    guard_or ("Could not finish promises within the size of the fuel")%string
+      (∀ r ∈ res, r.2 = true);;
+    mret $ (CProm.proms (union_list res.*1.*1), []).
+
+    Definition run_outcome_with_no_promise
+              (out : outcome) :
+        Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out) :=
+    '(res, _) ← run_outcome tid initmem out false;
+    mret res.
+
+  Fixpoint run_to_termination_no_promise
+                      (isem : iMon ())
+                      (fuel : nat) :
+      Exec.t (PPState.t TState.t Msg.t IIS.t) string bool :=
+    match fuel with
+    | 0%nat =>
+      ts ← mget PPState.state;
+      mret (term (TState.reg_map ts))
+    | S fuel =>
+      let handler := run_outcome_with_no_promise in
+      cinterp handler isem;;
+      ts ← mget PPState.state;
+      if term (TState.reg_map ts) then
+        mret true
+      else
+        run_to_termination_no_promise isem fuel
+    end.
+
+  Definition run_to_termination_pf (isem : iMon ())
                                 (fuel : nat)
                                 (ts : TState.t)
                                 (mem : Memory.t)
-      : Exec.res string Msg.t :=
+      : result string (list Msg.t * list TState.t) :=
     let base := List.length mem in
-    let res := Exec.results $ runSt_to_termination isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
-    guard_or ("Could not finish promises within the size of the fuel")%string (∀ r ∈ res, r.2 = true);;
-    res.*1.*1
-    |> union_list
-    |> mchoosel ∘ CProm.proms.
+    let res_proms := Exec.results $
+      run_to_termination_promise isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
+    guard_or ("Could not finish promises within the size of the fuel")%string
+      (∀ r ∈ res_proms, r.2 = true);;
+    let promises := res_proms.*1.*1 |> CProm.proms ∘ union_list in
+    let res := Exec.results $
+      run_to_termination_no_promise isem fuel (PPState.Make ts mem IIS.init) in
+    guard_or ("Could not finish the remaining states within the size of the fuel")%string
+      (∀ r ∈ res, r.2 = true);;
+    let tstates := map PPState.state res.*1 in
+    mret (promises, tstates).
 
 End ComputeProm.
 
@@ -764,12 +810,29 @@ Definition UMPromising_cert_nc isem :=
 Program Definition UMPromising_exe' (isem : iMon ())
     : BasicExecutablePM :=
   {|pModel := UMPromising_cert' isem;
-    promise_select :=
+    enumerate_promises_and_terminal_states :=
       λ fuel tid term initmem ts mem,
           run_to_termination tid initmem term isem fuel ts mem
   |}.
 Next Obligation. Admitted.
 Next Obligation. Admitted.
+Next Obligation. Admitted.
+Next Obligation. Admitted.
+
+Program Definition UMPromising_exe_pf' (isem : iMon ())
+    : BasicExecutablePM :=
+  {|pModel := UMPromising_cert' isem;
+    enumerate_promises_and_terminal_states :=
+      λ fuel tid term initmem ts mem,
+          run_to_termination_pf tid initmem term isem fuel ts mem
+  |}.
+Next Obligation. Admitted.
+Next Obligation. Admitted.
+Next Obligation. Admitted.
+Next Obligation. Admitted.
 
 Definition UMPromising_cert_c isem fuel :=
   Promising_to_Modelc isem (UMPromising_exe' isem) fuel.
+
+Definition UMPromising_cert_c_pf isem fuel :=
+  Promising_to_Modelc_pf isem (UMPromising_exe_pf' isem) fuel.
diff --git a/ArchSemArm/VMPromising.v b/ArchSemArm/VMPromising.v
index e80f164..c8a217a 100644
--- a/ArchSemArm/VMPromising.v
+++ b/ArchSemArm/VMPromising.v
@@ -1540,7 +1540,7 @@ Definition run_mem_read (addr : address) (macc : mem_acc) (init : Memory.initial
     mret val
   else mthrow "Unsupported 8 bytes access".
 
-Definition run_mem_read4  (addr : address) (macc : mem_acc) (init : Memory.initial) :
+Definition run_mem_read4 (addr : address) (macc : mem_acc) (init : Memory.initial) :
     Exec.t Memory.t string (bv 32) :=
   if is_ifetch macc then
     let aligned_addr := bv_unset_bit 2 addr in
@@ -1559,7 +1559,8 @@ Definition run_mem_read4  (addr : address) (macc : mem_acc) (init : Memory.initi
     This may mutate memory if no existing promise can be fullfilled *)
 Definition write_mem (tid : nat) (loc : Loc.t) (viio : view)
     (invalidation_time : option nat) (macc : mem_acc)
-    (data : val) : Exec.t (TState.t * Memory.t) string (view * option view) :=
+    (data : val) (mem_update : bool) :
+    Exec.t (TState.t * Memory.t) string (view * option view) :=
   let msg := Msg.make tid loc data in
   let is_release := is_rel_acq macc in
   '(ts, mem) ← mGet;
@@ -1567,8 +1568,10 @@ Definition write_mem (tid : nat) (loc : Loc.t) (viio : view)
     match Memory.fulfill msg (TState.prom ts) mem with
     | Some t => mret (t, false)
     | None =>
-      t ← Exec.liftSt snd $ Memory.promise msg;
-      mret (t, true)
+      if mem_update then
+        t ← Exec.liftSt snd $ Memory.promise msg;
+        mret (t, true)
+      else mdiscard
     end;
   let vbob :=
     ts.(TState.vdmbst) ⊔ ts.(TState.vdmb) ⊔ ts.(TState.vdsb)
@@ -1598,12 +1601,12 @@ Definition write_mem (tid : nat) (loc : Loc.t) (viio : view)
     If the store is exclusive the write may succeed or fail and the third
     return value indicate the success (true for success, false for error) *)
 Definition write_mem_xcl (tid : nat) (loc : Loc.t) (viio : view)
-    (invalidation_time : option nat) (macc : mem_acc) (data : val) :
+    (invalidation_time : option nat) (macc : mem_acc) (data : val) (mem_update : bool) :
   Exec.t (TState.t * Memory.t) string (option view) :=
   guard_or "Atomic RMW unsupported" (¬ (is_atomic_rmw macc));;
   let xcl := is_exclusive macc in
   if xcl then
-    '(time, vpre_opt) ← write_mem tid loc viio invalidation_time macc data;
+    '(time, vpre_opt) ← write_mem tid loc viio invalidation_time macc data mem_update;
     '(ts, mem) ← mGet;
     match TState.xclb ts with
     | None => mdiscard
@@ -1614,7 +1617,7 @@ Definition write_mem_xcl (tid : nat) (loc : Loc.t) (viio : view)
     mset fst TState.clear_xclb;;
     mret vpre_opt
   else
-    '(time, vpre_opt) ← write_mem tid loc viio invalidation_time macc data;
+    '(time, vpre_opt) ← write_mem tid loc viio invalidation_time macc data mem_update;
     mset fst $ TState.set_fwdb loc (FwdItem.make time viio false);;
     mret vpre_opt.
 
@@ -1833,30 +1836,30 @@ Definition run_take_exception (fault : exn) (vmax_t : view) :
 Section RunOutcome.
   Context (tid : nat) (initmem : memoryMap).
 
-  Equations run_outcome (out : outcome) :
+  Equations run_outcome (out : outcome) (mem_update : bool) :
       Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out * option view) :=
-  | RegRead reg racc =>
+  | RegRead reg racc, mem_update =>
       val ← Exec.liftSt (PPState.state ×× PPState.iis) $ (run_reg_read reg racc);
       mret (val, None)
-  | RegWrite reg racc val =>
+  | RegWrite reg racc val, mem_update =>
       run_reg_write reg racc val;;
       mret ((), None)
-  | MemRead (MemReq.make macc addr addr_space 8 0) =>
+  | MemRead (MemReq.make macc addr addr_space 8 0), mem_update =>
       guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
       let initmem := Memory.initial_from_memMap initmem in
       val ← run_mem_read addr macc initmem;
       mret (Ok (val, 0%bv), None)
-  | MemRead (MemReq.make macc addr addr_space 4 0) => (* ifetch *)
+  | MemRead (MemReq.make macc addr addr_space 4 0), mem_update => (* ifetch *)
       guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
       let initmem := Memory.initial_from_memMap initmem in
       opcode ← Exec.liftSt PPState.mem $ run_mem_read4 addr macc initmem;
       mret (Ok (opcode, 0%bv), None)
-  | MemRead _ => mthrow "Memory read of size other than 8 or 4, or with tags"
-  | MemWriteAddrAnnounce _ =>
+  | MemRead _, mem_update => mthrow "Memory read of size other than 8 or 4, or with tags"
+  | MemWriteAddrAnnounce _, mem_update =>
       vaddr ← mget (IIS.strict ∘ PPState.iis);
       mset PPState.state $ TState.update TState.vspec vaddr;;
       mret ((), None)
-  | MemWrite (MemReq.make macc addr addr_space 8 0) val _ =>
+  | MemWrite (MemReq.make macc addr addr_space 8 0) val _, mem_update =>
       guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
       addr ← othrow "Address not supported" $ Loc.from_addr addr;
       viio ← mget (IIS.strict ∘ PPState.iis);
@@ -1865,40 +1868,39 @@ Section RunOutcome.
         trans_res ← othrow "Explicit access before translation" tres_opt;
         let invalidation := trans_res.(IIS.TransRes.invalidation) in
         vpre_opt ← Exec.liftSt (PPState.state ×× PPState.mem) $
-                      write_mem_xcl tid addr viio invalidation macc val;
+                      write_mem_xcl tid addr viio invalidation macc val mem_update;
         mret (Ok (), vpre_opt)
       else mthrow "Unsupported non-explicit write"
-  | MemWrite _ _ _ => mthrow "Memory write of size other than 8, or with tags"
-  | Barrier barrier =>
+  | MemWrite _ _ _, mem_update => mthrow "Memory write of size other than 8, or with tags"
+  | Barrier barrier, mem_update =>
       mem ← mget PPState.mem;
       Exec.liftSt (PPState.state ×× PPState.iis) $ run_barrier barrier (length mem);;
       mret ((), None)
-  | TlbOp tlbi =>
+  | TlbOp tlbi, mem_update =>
       viio ← mget (IIS.strict ∘ PPState.iis);
       run_tlbi tid viio tlbi;;
       mret ((), None)
-  | ReturnException =>
+  | ReturnException, mem_update =>
       mem ← mget PPState.mem;
       Exec.liftSt (PPState.state ×× PPState.iis) $ run_cse (length mem);;
       mret ((), None)
-  | TranslationStart trans_start =>
+  | TranslationStart trans_start, mem_update =>
       let initmem := Memory.initial_from_memMap initmem in
       run_trans_start trans_start tid initmem;;
       mret ((), None)
-  | TranslationEnd trans_end =>
+  | TranslationEnd trans_end, mem_update =>
       Exec.liftSt (PPState.state ×× PPState.iis) $ run_trans_end trans_end;;
       mret ((), None)
-  | GenericFail s => mthrow ("Instruction failure: " ++ s)%string
-  | TakeException fault =>
+  | GenericFail s, mem_update => mthrow ("Instruction failure: " ++ s)%string
+  | TakeException fault, mem_update =>
       mem ← mget PPState.mem;
       Exec.liftSt (PPState.state ×× PPState.iis) $ run_take_exception fault (length mem);;
       mret ((), None)
-  | _ => mthrow "Unsupported outcome".
+  | _, mem_update => mthrow "Unsupported outcome".
 
   Definition run_outcome' (out : outcome) :
-    Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
-    run_outcome out |$> fst.
-
+      Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
+    run_outcome out true |$> fst.
 End RunOutcome.
 
 Module CProm.
@@ -1937,7 +1939,7 @@ Section ComputeProm.
               (base : view)
               (out : outcome) :
         Exec.t (CProm.t * PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
-    '(res, vpre_opt) ← Exec.liftSt snd $ run_outcome tid initmem out;
+    '(res, vpre_opt) ← Exec.liftSt snd $ run_outcome tid initmem out true;
     if vpre_opt is Some vpre then
       mem ← mget (PPState.mem ∘ snd);
       mset fst (CProm.add_if mem vpre base);;
@@ -1945,11 +1947,11 @@ Section ComputeProm.
     else
       mret res.
 
-  Fixpoint runSt_to_termination
+  Fixpoint run_to_termination_promise
                       (isem : iMon ())
                       (fuel : nat)
-                      (base : nat)
-      : Exec.t (CProm.t * PPState.t TState.t Ev.t IIS.t) string bool :=
+                      (base : nat) :
+      Exec.t (CProm.t * PPState.t TState.t Ev.t IIS.t) string bool :=
     match fuel with
     | 0%nat =>
       ts ← mget (PPState.state ∘ snd);
@@ -1961,20 +1963,62 @@ Section ComputeProm.
       if term (TState.reg_map ts) then
         mret true
       else
-        runSt_to_termination isem fuel base
+        run_to_termination_promise isem fuel base
+    end.
+
+    Definition run_to_termination (isem : iMon ())
+                                (fuel : nat)
+                                (ts : TState.t)
+                                (mem : Memory.t) :
+      result string (list Ev.t * list TState.t) :=
+    let base := List.length mem in
+    let res := Exec.results $
+      run_to_termination_promise isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
+    guard_or ("Could not finish promises within the size of the fuel")%string
+      (∀ r ∈ res, r.2 = true);;
+    mret $ (CProm.proms (union_list res.*1.*1), []).
+
+    Definition run_outcome_with_no_promise
+              (out : outcome) :
+        Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
+    '(res, _) ← run_outcome tid initmem out false;
+    mret res.
+
+  Fixpoint run_to_termination_no_promise
+                      (isem : iMon ())
+                      (fuel : nat) :
+      Exec.t (PPState.t TState.t Ev.t IIS.t) string bool :=
+    match fuel with
+    | 0%nat =>
+      ts ← mget PPState.state;
+      mret (term (TState.reg_map ts))
+    | S fuel =>
+      let handler := run_outcome_with_no_promise in
+      cinterp handler isem;;
+      ts ← mget PPState.state;
+      if term (TState.reg_map ts) then
+        mret true
+      else
+        run_to_termination_no_promise isem fuel
     end.
 
-  Definition run_to_termination (isem : iMon ())
+  Definition run_to_termination_pf (isem : iMon ())
                                 (fuel : nat)
                                 (ts : TState.t)
                                 (mem : Memory.t)
-      : Exec.res string Ev.t :=
+      : result string (list Ev.t * list TState.t) :=
     let base := List.length mem in
-    let res := Exec.results $ runSt_to_termination isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
-    guard_or ("Could not finish promises within the size of the fuel")%string (∀ r ∈ res, r.2 = true);;
-    res.*1.*1
-    |> union_list
-    |> mchoosel ∘ CProm.proms.
+    let res_proms := Exec.results $
+      run_to_termination_promise isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
+    guard_or ("Could not finish promises within the size of the fuel")%string
+      (∀ r ∈ res_proms, r.2 = true);;
+    let promises := res_proms.*1.*1 |> CProm.proms ∘ union_list in
+    let res := Exec.results $
+      run_to_termination_no_promise isem fuel (PPState.Make ts mem IIS.init) in
+    guard_or ("Could not finish the remaining states within the size of the fuel")%string
+      (∀ r ∈ res, r.2 = true);;
+    let tstates := map PPState.state res.*1 in
+    mret (promises, tstates).
 
 End ComputeProm.
 
@@ -2040,16 +2084,34 @@ Definition VMPromising_cert' (isem : iMon ()) : PromisingModel  :=
       λ initmem, Memory.to_memMap (Memory.initial_from_memMap initmem);
   |}.
 
+(** Implement the Executable Promising Model *)
+
 Program Definition VMPromising_exe' (isem : iMon ())
     : BasicExecutablePM :=
   {|pModel := VMPromising_cert' isem;
-    promise_select :=
+    enumerate_promises_and_terminal_states :=
       λ fuel tid term initmem ts mem,
           run_to_termination tid initmem term isem fuel ts mem
   |}.
 Next Obligation. Admitted.
 Next Obligation. Admitted.
+Next Obligation. Admitted.
+Next Obligation. Admitted.
 
+Program Definition VMPromising_exe_pf' (isem : iMon ())
+    : BasicExecutablePM :=
+  {|pModel := VMPromising_cert' isem;
+    enumerate_promises_and_terminal_states :=
+      λ fuel tid term initmem ts mem,
+          run_to_termination_pf tid initmem term isem fuel ts mem
+  |}.
+Next Obligation. Admitted.
+Next Obligation. Admitted.
+Next Obligation. Admitted.
+Next Obligation. Admitted.
 
 Definition VMPromising_cert_c isem fuel :=
   Promising_to_Modelc isem (VMPromising_exe' isem) fuel.
+
+Definition VMPromising_cert_c_pf isem fuel :=
+  Promising_to_Modelc_pf isem (VMPromising_exe_pf' isem) fuel.
diff --git a/ArchSemArm/tests/UMPromisingTest.v b/ArchSemArm/tests/UMPromisingTest.v
index 3107b03..9a0685c 100644
--- a/ArchSemArm/tests/UMPromisingTest.v
+++ b/ArchSemArm/tests/UMPromisingTest.v
@@ -123,6 +123,14 @@ Module EOR.
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
+
+  Definition test_results_pf :=
+    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x110%Z].
+    vm_compute (_ <$> _).
+    reflexivity.
+  Qed.
 End EOR.
 
 Module LDR. (* LDR X0, [X1, X0] at 0x500, loading from 0x1000 *)
@@ -158,6 +166,14 @@ Module LDR. (* LDR X0, [X1, X0] at 0x500, loading from 0x1000 *)
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
+
+  Definition test_results_pf :=
+    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x2a%Z].
+    vm_compute (_ <$> _).
+    reflexivity.
+  Qed.
 End LDR.
 
 Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1100 *)
@@ -195,6 +211,14 @@ Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1
     vm_compute (_ <$> _).
     set_solver.
   Qed.
+
+  Definition test_results_pf :=
+    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal reg_extract R0 0%fin <$> test_results_pf ≡ Listset [Ok 0x2a%Z].
+    vm_compute (_ <$> _).
+    set_solver.
+  Qed.
 End STRLDR.
 
 Module MP.
@@ -266,13 +290,22 @@ Module MP.
     vm_compute (elements _).
     apply NoDup_Permutation; try solve_NoDup; set_solver.
   Qed.
+
+  Definition test_results_pf :=
+    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
+    [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]; Ok [0x1%Z; 0x0%Z]].
+  Proof.
+    vm_compute (elements _).
+    apply NoDup_Permutation; try solve_NoDup; set_solver.
+  Qed.
 End MP.
 
 Module MPDMBS.
   (* A classic MP litmus test
      Thread 1: STR X2, [X1, X0]; DMB SY; STR X5, [X4, X3]
      Thread 2: LDR X5, [X4, X3]; DMB SY; LDR X2, [X1, X0]
-
      Expected outcome of (R5, R2) at Thread 2:
        (0x1, 0x2a), (0x0, 0x2a), (0x0, 0x0)
   *)
@@ -333,11 +366,20 @@ Module MPDMBS.
   Definition test_results :=
     UMPromising_cert_c arm_sem fuel n_threads termCond initState.
 
-  (** The test is fenced enough, the 0x1;0x0 outcome is impossible*)
   Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
     [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
   Proof.
     vm_compute (elements _).
     apply NoDup_Permutation; try solve_NoDup; set_solver.
   Qed.
+
+  Definition test_results_pf :=
+    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
+    [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
+  Proof.
+    vm_compute (elements _).
+    apply NoDup_Permutation; try solve_NoDup; set_solver.
+  Qed.
 End MPDMBS.
diff --git a/ArchSemArm/tests/VMPromisingTest.v b/ArchSemArm/tests/VMPromisingTest.v
index 4b39827..c076bd8 100644
--- a/ArchSemArm/tests/VMPromisingTest.v
+++ b/ArchSemArm/tests/VMPromisingTest.v
@@ -133,6 +133,14 @@ Module EORMMUOFF.
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
+
+  Definition test_results_pf :=
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x110%Z].
+    vm_compute (_ <$> _).
+    reflexivity.
+  Qed.
 End EORMMUOFF.
 
 (* Run EOR X0, X1, X2 at PC.
@@ -199,6 +207,14 @@ Module EOR.
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
+
+  Definition test_results_pf :=
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x110%Z].
+    vm_compute (_ <$> _).
+    reflexivity.
+  Qed.
 End EOR.
 
 (* LDR X0, [X1, X0] at VA 0x8000000500, loading from VA 0x8000001000
@@ -252,6 +268,14 @@ Module LDR.
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
+
+  Definition test_results_pf :=
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x2a%Z].
+    vm_compute (_ <$> _).
+    reflexivity.
+  Qed.
 End LDR.
 
 (* STR X2, [X1, X0]; LDR X0, [X1, X0] at VA 0x8000000500,
@@ -304,6 +328,14 @@ Module STRLDR.
     vm_compute (_ <$> _).
     set_solver.
   Qed.
+
+  Definition test_results_pf :=
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal reg_extract R0 0%fin <$> test_results_pf ≡ Listset [Ok 0x2a%Z].
+    vm_compute (_ <$> _).
+    set_solver.
+  Qed.
 End STRLDR.
 
 (* Sequential page table modification in single thread *)
@@ -376,9 +408,20 @@ Module LDRPT.
     vm_compute (elements _).
     apply NoDup_Permutation; try solve_NoDup; set_solver.
   Qed.
+
+  Definition test_results_pf :=
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  (* R0 should be 0x2a (from old mapping), R4 should be 0x42 (from new mapping) *)
+  Goal elements (regs_extract [(0%fin, R0); (0%fin, R4)] <$> test_results_pf) ≡ₚ
+      [Ok [0x2a%Z; 0x2a%Z]; Ok [0x2a%Z; 0x42%Z]].
+  Proof.
+    vm_compute (elements _).
+    apply NoDup_Permutation; try solve_NoDup; set_solver.
+  Qed.
 End LDRPT.
 
-(* Module MP.
+Module MP.
   (* A classic MP litmus test with address translation
      Thread 1: STR X2, [X1, X0]; STR X5, [X4, X3]
      Thread 2: LDR X5, [X4, X3]; LDR X2, [X1, X0]
@@ -433,15 +476,15 @@ End LDRPT.
     |> mem_insert 0x1100 8 0x0
     |> mem_insert 0x1200 8 0x0
     (* L0[1] -> L1  (for VA with L0 index = 1) *)
-    |> mem_insert 0x80008 8 0x81003
+    |> mem_insert 0x80008 8 0x81803
     (* L1[0] -> L2 *)
-    |> mem_insert 0x81000 8 0x82003
+    |> mem_insert 0x81000 8 0x82803
     (* L2[0] -> L3 *)
-    |> mem_insert 0x82000 8 0x83003
+    |> mem_insert 0x82000 8 0x83803
     (* L3[0] : map VA page 0x8000000000 -> PA page 0x0000 (executable) *)
-    |> mem_insert 0x83000 8 0x3
+    |> mem_insert 0x83000 8 0x403
     (* L3[1] : map VA page 0x8000001000 -> PA page 0x1000 (data) *)
-    |> mem_insert 0x83008 8 0x1003.
+    |> mem_insert 0x83008 8 0x1443.
 
   Definition n_threads := 2%nat.
 
@@ -453,26 +496,34 @@ End LDRPT.
     (λ tid rm, reg_lookup _PC rm =? terminate_at !!! tid).
 
   Definition initState :=
-    {| MState.state :=
-        {| MState.memory := init_mem;
-            MState.regs := [# init_reg_t1; init_reg_t2];
-            MState.address_space := PAS_NonSecure |};
-      MState.termCond := termCond |}.
+    {|archState.memory := init_mem;
+      archState.regs := [# init_reg_t1; init_reg_t2];
+      archState.address_space := PAS_NonSecure |}.
 
   Definition fuel := 6%nat.
 
-  Definition test_results :=
-    VMPromising_cert_c arm_sem fuel n_threads initState.
+  (* Definition test_results :=
+    VMPromising_cert_c arm_sem fuel n_threads termCond initState.
 
   Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
     [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]; Ok [0x1%Z; 0x0%Z]].
   Proof.
     vm_compute (elements _).
     apply NoDup_Permutation; try solve_NoDup; set_solver.
+  Qed. *)
+
+  Definition test_results_pf :=
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
+    [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]; Ok [0x1%Z; 0x0%Z]].
+  Proof.
+    vm_compute (elements _).
+    apply NoDup_Permutation; try solve_NoDup; set_solver.
   Qed.
-End MP. *)
+End MP.
 
-(* Module MPDMBS.
+Module MPDMBS.
   (* A classic MP litmus test with address translation
      Thread 1: STR X2, [X1, X0]; DMB SY; STR X5, [X4, X3]
      Thread 2: LDR X5, [X4, X3]; DMB SY; LDR X2, [X1, X0]
@@ -534,9 +585,9 @@ End MP. *)
     (* L2[0] -> L3 *)
     |> mem_insert 0x82000 8 0x83003
     (* L3[0] : map VA page 0x8000000000 -> PA page 0x0000 (executable) *)
-    |> mem_insert 0x83000 8 0x3
+    |> mem_insert 0x83000 8 0x403
     (* L3[1] : map VA page 0x8000001000 -> PA page 0x1000 (data) *)
-    |> mem_insert 0x83008 8 0x1003.
+    |> mem_insert 0x83008 8 0x60000000001443.
 
   Definition n_threads := 2%nat.
 
@@ -547,16 +598,14 @@ End MP. *)
     (λ tid rm, reg_lookup _PC rm =? terminate_at !!! tid).
 
   Definition initState :=
-    {| MState.state :=
-        {| MState.memory := init_mem;
-            MState.regs := [# init_reg_t1; init_reg_t2];
-            MState.address_space := PAS_NonSecure |};
-      MState.termCond := termCond |}.
+    {|archState.memory := init_mem;
+      archState.regs := [# init_reg_t1; init_reg_t2];
+      archState.address_space := PAS_NonSecure |}.
 
   Definition fuel := 8%nat.
 
-  Definition test_results :=
-    VMPromising_cert_c arm_sem fuel n_threads initState.
+  (* Definition test_results :=
+    VMPromising_cert_c arm_sem fuel n_threads termCond initState.
 
   (** The test is fenced enough, the 0x1; 0x0 outcome is impossible*)
   Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
@@ -564,5 +613,16 @@ End MP. *)
   Proof.
     vm_compute (elements _).
     apply NoDup_Permutation; try solve_NoDup; set_solver.
+  Qed. *)
+
+  Definition test_results_pf :=
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  (** The test is fenced enough, the 0x1; 0x0 outcome is impossible*)
+  Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
+    [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
+  Proof.
+    vm_compute (elements _).
+    apply NoDup_Permutation; try solve_NoDup; set_solver.
   Qed.
-End MPDMBS. *)
+End MPDMBS.

From fbfa855614849830ccb9b52ba25864b2a46895e1 Mon Sep 17 00:00:00 2001
From: Yeji Han <yeji.han@sf.snu.ac.kr>
Date: Wed, 12 Nov 2025 20:14:40 +0900
Subject: [PATCH 2/4] Add venumerate

---
 Common/CVec.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Common/CVec.v b/Common/CVec.v
index d5b2742..76027a4 100644
--- a/Common/CVec.v
+++ b/Common/CVec.v
@@ -258,3 +258,7 @@ Fixpoint vmapM {A B} `{MBind M, MRet M} (f : A → M B) {n} (v : vec A n) :
       ntl ← vmapM f tl;
       mret (nhd ::: ntl)
   end.
+
+(** * venumerate *)
+Definition venumerate {A n} (v : vec A n) : vec ((fin n) * A) n :=
+  fun_to_vec (λ i, (i, v !!! i)).

From 53d1c39d3dd8f0c4ee6b3486b143dab7b8b1ceaf Mon Sep 17 00:00:00 2001
From: Yeji Han <yeji.han@sf.snu.ac.kr>
Date: Wed, 12 Nov 2025 20:14:50 +0900
Subject: [PATCH 3/4] Simplify promise-first code - Apply code reviews

Apply code reviews
---
 ArchSem/GenPromising.v             |  80 ++++++------------
 ArchSemArm/UMPromising.v           | 121 ++++++++-------------------
 ArchSemArm/VMPromising.v           | 130 +++++++++--------------------
 ArchSemArm/tests/UMPromisingTest.v |  50 +----------
 ArchSemArm/tests/VMPromisingTest.v |  72 +---------------
 5 files changed, 108 insertions(+), 345 deletions(-)

diff --git a/ArchSem/GenPromising.v b/ArchSem/GenPromising.v
index 10f00ef..5baf196 100644
--- a/ArchSem/GenPromising.v
+++ b/ArchSem/GenPromising.v
@@ -380,7 +380,7 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
         promise ← mchoosel (enum bool);
         if (promise : bool) then cpromise_tid fuel tid else run_tid isem prom tid.
 
-    (** Computational evaluate all the possible allowed final states according
+    (** Computationally evaluate all the possible allowed final states according
         to the promising model prom starting from st *)
     Fixpoint run (fuel : nat) : Exec.t t string final :=
       st ← mGet;
@@ -391,54 +391,41 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
           run fuel
         else mthrow "Could not finish running within the size of the fuel".
 
-    (** Explore all possible promise-based executions across all threads. *)
-    Fixpoint prune_promises_and_states (fuel_per_tid fuel : nat)
-        (finals : list final) : Exec.t t string (list final) :=
+    (** Computationally evaluate all the possible allowed final states according
+        to the promising model prom starting from st with promise-first optimization.
+        The size of fuel should be at least (# of promises) + max(# of instructions) + 1 *)
+    Fixpoint run_promise_first (fuel : nat) : Exec.t t string final :=
       if fuel is S fuel then
         st ← mGet;
         (* Find out next possible promises or terminating states at the current thread *)
         executions ←
-          for (tid : fin n) in enum (fin n) do
+          vmapM (λ '(tid, ts),
             '(promises_per_tid, tstates_per_tid) ←
               mlift $ prom.(enumerate_promises_and_terminal_states)
-                        fuel_per_tid tid (term tid) (initmem st) (tstate tid st) (events st);
-            mret (map (λ ev, (ev, tid)) promises_per_tid, tstates_per_tid)
-          end;
-
-        (* Compute cartesian products of the possible thread states *)
-        let tstates_sys :=
-          fold_left (λ partial_sts tstates_tid,
-            List.flat_map (λ tstate,
-              if is_emptyb partial_sts then [[tstate]]
-              else map (λ partial_st, partial_st ++ [tstate]) partial_sts
-            ) tstates_tid
-          ) (map snd executions) [] in
-        let new_finals :=
-          omap (λ tstates,
-            if (list_to_vec_n n tstates) is Some tstates_vec then
-              let st := Make tstates_vec st.(PState.initmem) st.(PState.events) in
-              if decide $ terminated prom term st is left pt
-              then Some (make_final st pt)
-              else None
-            else None
-          ) tstates_sys in
+                        fuel (fin_to_nat tid) (term tid) (initmem st) ts (events st);
+            mret (map (.,tid) promises_per_tid, tstates_per_tid)
+          ) (venumerate (tstates st));
 
-        (* Non-deterministically choose the next promise and the tid for pruning *)
-        let promises_all := List.concat (map fst executions) in
-        if is_emptyb promises_all then
-          mret (new_finals ++ finals)
-        else
+        promise ← mchoosel (enum bool);
+        if (promise : bool) then
+          (* Non-deterministically choose the next promise and the tid for pruning *)
+          let promises_all := List.concat (vmap fst executions) in
           '(next_ev, tid) ← mchoosel promises_all;
           mSet (λ st, promise_tid prom st tid next_ev);;
-          prune_promises_and_states fuel_per_tid fuel (new_finals ++ finals)
-      else mret finals.
-
-    (** Computational evaluate all the possible allowed final states according
-        to the promising model prom starting from st
-        with promise-first optimization *)
-    Definition run_promise_first (fuel : nat) : Exec.t t string final :=
-      finals ← prune_promises_and_states fuel fuel [];
-      mchoosel finals.
+          run_promise_first fuel
+        else
+          (* Compute cartesian products of the possible thread states *)
+          let tstates_all := cprodn (vmap snd executions) in
+          let new_finals :=
+            omap (λ tstates,
+              let st := Make tstates st.(PState.initmem) st.(PState.events) in
+              if decide $ terminated prom term st is left pt
+              then Some (make_final st pt)
+              else None
+            ) tstates_all in
+          mchoosel new_finals
+      else
+        mthrow "Could not finish running within the size of the fuel".
 
     End CPS.
     Arguments to_final_archState {_ _ _}.
@@ -447,25 +434,12 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
   (** Create a computational model from an ISA model and promising model *)
   Definition Promising_to_Modelc (isem : iMon ()) (prom : BasicExecutablePM)
       (fuel : nat) : archModel.c ∅ :=
-    λ n term (initMs : archState n),
-      PState.from_archState prom initMs |>
-      archModel.Res.from_exec
-        $ CPState.to_final_archState
-        <$> CPState.run isem prom term fuel.
-
-  (** Create a computational model from an ISA model and promising model
-      with promise-free optimization *)
-  Definition Promising_to_Modelc_pf (isem : iMon ()) (prom : BasicExecutablePM)
-      (fuel : nat) : archModel.c ∅ :=
     λ n term (initMs : archState n),
       PState.from_archState prom initMs |>
       archModel.Res.from_exec
         $ CPState.to_final_archState
         <$> CPState.run_promise_first prom term fuel.
 
-    (* TODO state some soundness lemma between Promising_to_Modelnc and
-        Promising_Modelc *)
-
 End GenPromising.
 
 Module Type GenPromisingT (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
diff --git a/ArchSemArm/UMPromising.v b/ArchSemArm/UMPromising.v
index e910140..cee7657 100644
--- a/ArchSemArm/UMPromising.v
+++ b/ArchSemArm/UMPromising.v
@@ -457,18 +457,16 @@ Definition read_mem4 (addr : address) (macc : mem_acc) (init : Memory.initial) :
     This may mutate memory if no existing promise can be fullfilled *)
 Definition write_mem (tid : nat) (loc : Loc.t) (vdata : view)
            (macc : mem_acc) (mem : Memory.t)
-           (data : val) (mem_update : bool) :
+           (data : val) :
           Exec.t TState.t string (Memory.t * view * option view):=
   let msg := Msg.make tid loc data in
   let is_release := is_rel_acq macc in
   ts ← mGet;
-  '(time, mem, new_promise) ←
+  let '(time, mem, new_promise) :=
     match Memory.fulfill msg (TState.prom ts) mem with
-    | Some t => mret (t, mem, false)
-    | None =>
-      if mem_update then mret (Memory.promise msg mem, true)
-      else mdiscard
-    end;
+    | Some t => (t, mem, false)
+    | None => (Memory.promise msg mem, true)
+    end in
   let vbob :=
     ts.(TState.vdmbst) ⊔ ts.(TState.vdmb) ⊔ ts.(TState.visb) ⊔ ts.(TState.vacq)
     ⊔ view_if is_release (ts.(TState.vrd) ⊔ ts.(TState.vwr)) in
@@ -478,10 +476,8 @@ Definition write_mem (tid : nat) (loc : Loc.t) (vdata : view)
   mSet $ TState.update_coh loc time;;
   mSet $ TState.update TState.vwr time;;
   mSet $ TState.update TState.vrel (view_if is_release time);;
-  mret $ match new_promise with
-        | true => (mem, time, Some vpre)
-        | false => (mem, time, None)
-        end.
+  mret (mem, time, (if new_promise then Some vpre else None)).
+
 
 (** Tries to perform a memory write.
 
@@ -492,12 +488,12 @@ Definition write_mem (tid : nat) (loc : Loc.t) (vdata : view)
     return value indicate the success (true for success, false for error) *)
 Definition write_mem_xcl (tid : nat) (loc : Loc.t)
            (vdata : view) (macc : mem_acc)
-           (mem : Memory.t) (data : val) (mem_update : bool)
+           (mem : Memory.t) (data : val)
   : Exec.t TState.t string (Memory.t * option view) :=
   guard_or "Atomic RMW unsupported" (¬ (is_atomic_rmw macc));;
   let xcl := is_exclusive macc in
   if xcl then
-    '(mem, time, vpre_opt) ← write_mem tid loc vdata macc mem data mem_update;
+    '(mem, time, vpre_opt) ← write_mem tid loc vdata macc mem data;
     ts ← mGet;
     match TState.xclb ts with
     | None => mdiscard
@@ -508,7 +504,7 @@ Definition write_mem_xcl (tid : nat) (loc : Loc.t)
     mSet TState.clear_xclb;;
     mret (mem, vpre_opt)
   else
-    '(mem, time, vpre_opt) ← write_mem tid loc vdata macc mem data mem_update;
+    '(mem, time, vpre_opt) ← write_mem tid loc vdata macc mem data;
     mSet $ TState.set_fwdb loc (FwdItem.make time vdata false);;
     mret (mem, vpre_opt).
 
@@ -538,9 +534,9 @@ End IIS.
 Section RunOutcome.
   Context (tid : nat) (initmem : memoryMap).
 
-  Equations run_outcome (out : outcome) (mem_update : bool) :
+  Equations run_outcome (out : outcome) :
       Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out * option view) :=
-  | RegWrite reg racc val, mem_update =>
+  | RegWrite reg racc val =>
       guard_or "Non trivial reg access types unsupported" (racc = None);;
       vreg ← mget (IIS.strict ∘ PPState.iis);
       vreg' ←
@@ -554,14 +550,14 @@ Section RunOutcome.
         TState.set_reg reg (val, vreg') ts;
       msetv PPState.state nts;;
       mret ((), None)
-  | RegRead reg racc, mem_update =>
+  | RegRead reg racc =>
       guard_or "Non trivial reg access types unsupported" (racc = None);;
       ts ← mget PPState.state;
       '(val, view) ← othrow "Register isn't mapped can't read" $
           dmap_lookup reg ts.(TState.regs);
     mset PPState.iis $ IIS.add view;;
     mret (val, None)
-  | MemRead (MemReq.make macc addr addr_space 8 0), mem_update =>
+  | MemRead (MemReq.make macc addr addr_space 8 0) =>
       guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
       loc ← othrow "PA not supported" $ Loc.from_addr addr;
       if is_ifetch macc then
@@ -575,28 +571,28 @@ Section RunOutcome.
         mset PPState.iis $ IIS.add view;;
         mret (Ok (val, bv_0 0), None)
       else mthrow "Read is not explicit or ifetch"
-  | MemRead (MemReq.make macc addr addr_space 4 0), mem_update => (* ifetch *)
+  | MemRead (MemReq.make macc addr addr_space 4 0) => (* ifetch *)
       guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
       let initmem := Memory.initial_from_memMap initmem in
       opcode ← Exec.liftSt PPState.mem $ read_mem4 addr macc initmem;
       mret (Ok (opcode, 0%bv), None)
-  | MemRead _, mem_update => mthrow "Memory read of size other than 8 and 4"
-  | MemWriteAddrAnnounce _, mem_update =>
+  | MemRead _ => mthrow "Memory read of size other than 8 and 4"
+  | MemWriteAddrAnnounce _ =>
       vaddr ← mget (IIS.strict ∘ PPState.iis);
       mset PPState.state $ TState.update TState.vcap vaddr;;
       mret ((), None)
-  | MemWrite (MemReq.make macc addr addr_space 8 0) val tags, mem_update =>
+  | MemWrite (MemReq.make macc addr addr_space 8 0) val tags =>
       guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
       addr ← othrow "PA not supported" $ Loc.from_addr addr;
       if is_explicit macc then
         mem ← mget PPState.mem;
         vdata ← mget (IIS.strict ∘ PPState.iis);
         '(mem, vpre_opt) ← Exec.liftSt PPState.state
-                $ write_mem_xcl tid addr vdata macc mem val mem_update;
+                $ write_mem_xcl tid addr vdata macc mem val;
         msetv PPState.mem mem;;
         mret (Ok (), vpre_opt)
       else mthrow "Unsupported non-explicit write"
-  | Barrier (Barrier_DMB dmb), mem_update => (* dmb *)
+  | Barrier (Barrier_DMB dmb) => (* dmb *)
       ts ← mget PPState.state;
       match dmb.(DxB_types) with
       | MBReqTypes_All (* dmb sy *) =>
@@ -607,16 +603,17 @@ Section RunOutcome.
           mset PPState.state $ TState.update TState.vdmbst ts.(TState.vwr)
       end;;
       mret ((), None)
-  | Barrier (Barrier_ISB ()), mem_update => (* isb *)
+  | Barrier (Barrier_ISB ()) => (* isb *)
       ts ← mget PPState.state;
     mset PPState.state $ TState.update TState.visb (TState.vcap ts);;
     mret ((), None)
-  | GenericFail s, mem_update => mthrow ("Instruction failure: " ++ s)%string
-  | _, _ => mthrow "Unsupported outcome".
+  | GenericFail s => mthrow ("Instruction failure: " ++ s)%string
+  | _ => mthrow "Unsupported outcome".
 
   Definition run_outcome' (out : outcome) :
       Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out) :=
-    run_outcome out true |$> fst.
+    run_outcome out |$> fst.
+
 End RunOutcome.
 
 Module CProm.
@@ -655,7 +652,7 @@ Section ComputeProm.
               (base : view)
               (out : outcome) :
         Exec.t (CProm.t * PPState.t TState.t Msg.t IIS.t) string (eff_ret out) :=
-    '(res, vpre_opt) ← Exec.liftSt snd $ run_outcome tid initmem out true;
+    '(res, vpre_opt) ← Exec.liftSt snd $ run_outcome tid initmem out;
     if vpre_opt is Some vpre then
       mem ← mget (PPState.mem ∘ snd);
       mset fst (CProm.add_if mem vpre base);;
@@ -663,6 +660,9 @@ Section ComputeProm.
     else
       mret res.
 
+  (* Run the thread state until termination, collecting certified promises.
+     Returns true if termination occurs within the given fuel,
+     false otherwise. *)
   Fixpoint run_to_termination_promise
                       (isem : iMon ())
                       (fuel : nat)
@@ -682,43 +682,7 @@ Section ComputeProm.
         run_to_termination_promise isem fuel base
     end.
 
-    Definition run_to_termination (isem : iMon ())
-                                (fuel : nat)
-                                (ts : TState.t)
-                                (mem : Memory.t) :
-      result string (list Msg.t * list TState.t) :=
-    let base := List.length mem in
-    let res := Exec.results $
-      run_to_termination_promise isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
-    guard_or ("Could not finish promises within the size of the fuel")%string
-      (∀ r ∈ res, r.2 = true);;
-    mret $ (CProm.proms (union_list res.*1.*1), []).
-
-    Definition run_outcome_with_no_promise
-              (out : outcome) :
-        Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out) :=
-    '(res, _) ← run_outcome tid initmem out false;
-    mret res.
-
-  Fixpoint run_to_termination_no_promise
-                      (isem : iMon ())
-                      (fuel : nat) :
-      Exec.t (PPState.t TState.t Msg.t IIS.t) string bool :=
-    match fuel with
-    | 0%nat =>
-      ts ← mget PPState.state;
-      mret (term (TState.reg_map ts))
-    | S fuel =>
-      let handler := run_outcome_with_no_promise in
-      cinterp handler isem;;
-      ts ← mget PPState.state;
-      if term (TState.reg_map ts) then
-        mret true
-      else
-        run_to_termination_no_promise isem fuel
-    end.
-
-  Definition run_to_termination_pf (isem : iMon ())
+  Definition run_to_termination (isem : iMon ())
                                 (fuel : nat)
                                 (ts : TState.t)
                                 (mem : Memory.t)
@@ -729,11 +693,11 @@ Section ComputeProm.
     guard_or ("Could not finish promises within the size of the fuel")%string
       (∀ r ∈ res_proms, r.2 = true);;
     let promises := res_proms.*1.*1 |> CProm.proms ∘ union_list in
-    let res := Exec.results $
-      run_to_termination_no_promise isem fuel (PPState.Make ts mem IIS.init) in
-    guard_or ("Could not finish the remaining states within the size of the fuel")%string
-      (∀ r ∈ res, r.2 = true);;
-    let tstates := map PPState.state res.*1 in
+    let tstates :=
+      res_proms
+      |> omap (λ '((cp, st), _),
+          if is_emptyb (CProm.proms cp) then Some (PPState.state st)
+          else None) in
     mret (promises, tstates).
 
 End ComputeProm.
@@ -819,20 +783,5 @@ Next Obligation. Admitted.
 Next Obligation. Admitted.
 Next Obligation. Admitted.
 
-Program Definition UMPromising_exe_pf' (isem : iMon ())
-    : BasicExecutablePM :=
-  {|pModel := UMPromising_cert' isem;
-    enumerate_promises_and_terminal_states :=
-      λ fuel tid term initmem ts mem,
-          run_to_termination_pf tid initmem term isem fuel ts mem
-  |}.
-Next Obligation. Admitted.
-Next Obligation. Admitted.
-Next Obligation. Admitted.
-Next Obligation. Admitted.
-
 Definition UMPromising_cert_c isem fuel :=
   Promising_to_Modelc isem (UMPromising_exe' isem) fuel.
-
-Definition UMPromising_cert_c_pf isem fuel :=
-  Promising_to_Modelc_pf isem (UMPromising_exe_pf' isem) fuel.
diff --git a/ArchSemArm/VMPromising.v b/ArchSemArm/VMPromising.v
index c8a217a..8d52b35 100644
--- a/ArchSemArm/VMPromising.v
+++ b/ArchSemArm/VMPromising.v
@@ -1558,8 +1558,7 @@ Definition run_mem_read4 (addr : address) (macc : mem_acc) (init : Memory.initia
 
     This may mutate memory if no existing promise can be fullfilled *)
 Definition write_mem (tid : nat) (loc : Loc.t) (viio : view)
-    (invalidation_time : option nat) (macc : mem_acc)
-    (data : val) (mem_update : bool) :
+      (invalidation_time : option nat) (macc : mem_acc) (data : val) :
     Exec.t (TState.t * Memory.t) string (view * option view) :=
   let msg := Msg.make tid loc data in
   let is_release := is_rel_acq macc in
@@ -1568,10 +1567,8 @@ Definition write_mem (tid : nat) (loc : Loc.t) (viio : view)
     match Memory.fulfill msg (TState.prom ts) mem with
     | Some t => mret (t, false)
     | None =>
-      if mem_update then
-        t ← Exec.liftSt snd $ Memory.promise msg;
-        mret (t, true)
-      else mdiscard
+      t ← Exec.liftSt snd $ Memory.promise msg;
+      mret (t, true)
     end;
   let vbob :=
     ts.(TState.vdmbst) ⊔ ts.(TState.vdmb) ⊔ ts.(TState.vdsb)
@@ -1588,10 +1585,7 @@ Definition write_mem (tid : nat) (loc : Loc.t) (viio : view)
   mset fst $ TState.update_coh loc time;;
   mset fst $ TState.update TState.vwr time;;
   mset fst $ TState.update TState.vrel (view_if is_release time);;
-  match new_promise with
-  | true => mret (time, Some vpre)
-  | false => mret (time, None)
-  end.
+  mret (time, if (new_promise : bool) then Some vpre else None).
 
 (** Tries to perform a memory write.
 
@@ -1601,12 +1595,12 @@ Definition write_mem (tid : nat) (loc : Loc.t) (viio : view)
     If the store is exclusive the write may succeed or fail and the third
     return value indicate the success (true for success, false for error) *)
 Definition write_mem_xcl (tid : nat) (loc : Loc.t) (viio : view)
-    (invalidation_time : option nat) (macc : mem_acc) (data : val) (mem_update : bool) :
+    (invalidation_time : option nat) (macc : mem_acc) (data : val) :
   Exec.t (TState.t * Memory.t) string (option view) :=
   guard_or "Atomic RMW unsupported" (¬ (is_atomic_rmw macc));;
   let xcl := is_exclusive macc in
   if xcl then
-    '(time, vpre_opt) ← write_mem tid loc viio invalidation_time macc data mem_update;
+    '(time, vpre_opt) ← write_mem tid loc viio invalidation_time macc data;
     '(ts, mem) ← mGet;
     match TState.xclb ts with
     | None => mdiscard
@@ -1617,7 +1611,7 @@ Definition write_mem_xcl (tid : nat) (loc : Loc.t) (viio : view)
     mset fst TState.clear_xclb;;
     mret vpre_opt
   else
-    '(time, vpre_opt) ← write_mem tid loc viio invalidation_time macc data mem_update;
+    '(time, vpre_opt) ← write_mem tid loc viio invalidation_time macc data;
     mset fst $ TState.set_fwdb loc (FwdItem.make time viio false);;
     mret vpre_opt.
 
@@ -1836,30 +1830,30 @@ Definition run_take_exception (fault : exn) (vmax_t : view) :
 Section RunOutcome.
   Context (tid : nat) (initmem : memoryMap).
 
-  Equations run_outcome (out : outcome) (mem_update : bool) :
+  Equations run_outcome (out : outcome) :
       Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out * option view) :=
-  | RegRead reg racc, mem_update =>
+  | RegRead reg racc =>
       val ← Exec.liftSt (PPState.state ×× PPState.iis) $ (run_reg_read reg racc);
       mret (val, None)
-  | RegWrite reg racc val, mem_update =>
+  | RegWrite reg racc val =>
       run_reg_write reg racc val;;
       mret ((), None)
-  | MemRead (MemReq.make macc addr addr_space 8 0), mem_update =>
+  | MemRead (MemReq.make macc addr addr_space 8 0) =>
       guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
       let initmem := Memory.initial_from_memMap initmem in
       val ← run_mem_read addr macc initmem;
       mret (Ok (val, 0%bv), None)
-  | MemRead (MemReq.make macc addr addr_space 4 0), mem_update => (* ifetch *)
+  | MemRead (MemReq.make macc addr addr_space 4 0) => (* ifetch *)
       guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
       let initmem := Memory.initial_from_memMap initmem in
       opcode ← Exec.liftSt PPState.mem $ run_mem_read4 addr macc initmem;
       mret (Ok (opcode, 0%bv), None)
-  | MemRead _, mem_update => mthrow "Memory read of size other than 8 or 4, or with tags"
-  | MemWriteAddrAnnounce _, mem_update =>
+  | MemRead _ => mthrow "Memory read of size other than 8 or 4, or with tags"
+  | MemWriteAddrAnnounce _ =>
       vaddr ← mget (IIS.strict ∘ PPState.iis);
       mset PPState.state $ TState.update TState.vspec vaddr;;
       mret ((), None)
-  | MemWrite (MemReq.make macc addr addr_space 8 0) val _, mem_update =>
+  | MemWrite (MemReq.make macc addr addr_space 8 0) val _ =>
       guard_or "Access outside Non-Secure" (addr_space = PAS_NonSecure);;
       addr ← othrow "Address not supported" $ Loc.from_addr addr;
       viio ← mget (IIS.strict ∘ PPState.iis);
@@ -1868,39 +1862,40 @@ Section RunOutcome.
         trans_res ← othrow "Explicit access before translation" tres_opt;
         let invalidation := trans_res.(IIS.TransRes.invalidation) in
         vpre_opt ← Exec.liftSt (PPState.state ×× PPState.mem) $
-                      write_mem_xcl tid addr viio invalidation macc val mem_update;
+                      write_mem_xcl tid addr viio invalidation macc val;
         mret (Ok (), vpre_opt)
       else mthrow "Unsupported non-explicit write"
-  | MemWrite _ _ _, mem_update => mthrow "Memory write of size other than 8, or with tags"
-  | Barrier barrier, mem_update =>
+  | MemWrite _ _ _ => mthrow "Memory write of size other than 8, or with tags"
+  | Barrier barrier =>
       mem ← mget PPState.mem;
       Exec.liftSt (PPState.state ×× PPState.iis) $ run_barrier barrier (length mem);;
       mret ((), None)
-  | TlbOp tlbi, mem_update =>
+  | TlbOp tlbi =>
       viio ← mget (IIS.strict ∘ PPState.iis);
       run_tlbi tid viio tlbi;;
       mret ((), None)
-  | ReturnException, mem_update =>
+  | ReturnException =>
       mem ← mget PPState.mem;
       Exec.liftSt (PPState.state ×× PPState.iis) $ run_cse (length mem);;
       mret ((), None)
-  | TranslationStart trans_start, mem_update =>
+  | TranslationStart trans_start =>
       let initmem := Memory.initial_from_memMap initmem in
       run_trans_start trans_start tid initmem;;
       mret ((), None)
-  | TranslationEnd trans_end, mem_update =>
+  | TranslationEnd trans_end =>
       Exec.liftSt (PPState.state ×× PPState.iis) $ run_trans_end trans_end;;
       mret ((), None)
-  | GenericFail s, mem_update => mthrow ("Instruction failure: " ++ s)%string
-  | TakeException fault, mem_update =>
+  | GenericFail s => mthrow ("Instruction failure: " ++ s)%string
+  | TakeException fault =>
       mem ← mget PPState.mem;
       Exec.liftSt (PPState.state ×× PPState.iis) $ run_take_exception fault (length mem);;
       mret ((), None)
-  | _, mem_update => mthrow "Unsupported outcome".
+  | _ => mthrow "Unsupported outcome".
 
   Definition run_outcome' (out : outcome) :
       Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
-    run_outcome out true |$> fst.
+    run_outcome out |$> fst.
+
 End RunOutcome.
 
 Module CProm.
@@ -1939,7 +1934,7 @@ Section ComputeProm.
               (base : view)
               (out : outcome) :
         Exec.t (CProm.t * PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
-    '(res, vpre_opt) ← Exec.liftSt snd $ run_outcome tid initmem out true;
+    '(res, vpre_opt) ← Exec.liftSt snd $ run_outcome tid initmem out;
     if vpre_opt is Some vpre then
       mem ← mget (PPState.mem ∘ snd);
       mset fst (CProm.add_if mem vpre base);;
@@ -1947,6 +1942,9 @@ Section ComputeProm.
     else
       mret res.
 
+  (* Run the thread state until termination, collecting certified promises.
+    Returns true if termination occurs within the given fuel,
+    false otherwise. *)
   Fixpoint run_to_termination_promise
                       (isem : iMon ())
                       (fuel : nat)
@@ -1966,43 +1964,7 @@ Section ComputeProm.
         run_to_termination_promise isem fuel base
     end.
 
-    Definition run_to_termination (isem : iMon ())
-                                (fuel : nat)
-                                (ts : TState.t)
-                                (mem : Memory.t) :
-      result string (list Ev.t * list TState.t) :=
-    let base := List.length mem in
-    let res := Exec.results $
-      run_to_termination_promise isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
-    guard_or ("Could not finish promises within the size of the fuel")%string
-      (∀ r ∈ res, r.2 = true);;
-    mret $ (CProm.proms (union_list res.*1.*1), []).
-
-    Definition run_outcome_with_no_promise
-              (out : outcome) :
-        Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
-    '(res, _) ← run_outcome tid initmem out false;
-    mret res.
-
-  Fixpoint run_to_termination_no_promise
-                      (isem : iMon ())
-                      (fuel : nat) :
-      Exec.t (PPState.t TState.t Ev.t IIS.t) string bool :=
-    match fuel with
-    | 0%nat =>
-      ts ← mget PPState.state;
-      mret (term (TState.reg_map ts))
-    | S fuel =>
-      let handler := run_outcome_with_no_promise in
-      cinterp handler isem;;
-      ts ← mget PPState.state;
-      if term (TState.reg_map ts) then
-        mret true
-      else
-        run_to_termination_no_promise isem fuel
-    end.
-
-  Definition run_to_termination_pf (isem : iMon ())
+  Definition run_to_termination (isem : iMon ())
                                 (fuel : nat)
                                 (ts : TState.t)
                                 (mem : Memory.t)
@@ -2013,11 +1975,11 @@ Section ComputeProm.
     guard_or ("Could not finish promises within the size of the fuel")%string
       (∀ r ∈ res_proms, r.2 = true);;
     let promises := res_proms.*1.*1 |> CProm.proms ∘ union_list in
-    let res := Exec.results $
-      run_to_termination_no_promise isem fuel (PPState.Make ts mem IIS.init) in
-    guard_or ("Could not finish the remaining states within the size of the fuel")%string
-      (∀ r ∈ res, r.2 = true);;
-    let tstates := map PPState.state res.*1 in
+    let tstates :=
+      res_proms
+      |> omap (λ '((cp, st), _),
+          if is_emptyb (CProm.proms cp) then Some (PPState.state st)
+          else None) in
     mret (promises, tstates).
 
 End ComputeProm.
@@ -2067,8 +2029,7 @@ Definition allowed_promises_cert (isem : iMon ()) tid (initmem : memoryMap)
         TState.prom ts' = []
   ]}.
 
-
-Definition VMPromising_cert' (isem : iMon ()) : PromisingModel  :=
+Definition VMPromising_cert' (isem : iMon ()) : PromisingModel :=
   {|tState := TState.t;
     tState_init := λ tid, TState.init;
     tState_regs := TState.reg_map;
@@ -2098,20 +2059,5 @@ Next Obligation. Admitted.
 Next Obligation. Admitted.
 Next Obligation. Admitted.
 
-Program Definition VMPromising_exe_pf' (isem : iMon ())
-    : BasicExecutablePM :=
-  {|pModel := VMPromising_cert' isem;
-    enumerate_promises_and_terminal_states :=
-      λ fuel tid term initmem ts mem,
-          run_to_termination_pf tid initmem term isem fuel ts mem
-  |}.
-Next Obligation. Admitted.
-Next Obligation. Admitted.
-Next Obligation. Admitted.
-Next Obligation. Admitted.
-
 Definition VMPromising_cert_c isem fuel :=
   Promising_to_Modelc isem (VMPromising_exe' isem) fuel.
-
-Definition VMPromising_cert_c_pf isem fuel :=
-  Promising_to_Modelc_pf isem (VMPromising_exe_pf' isem) fuel.
diff --git a/ArchSemArm/tests/UMPromisingTest.v b/ArchSemArm/tests/UMPromisingTest.v
index 9a0685c..7e88e34 100644
--- a/ArchSemArm/tests/UMPromisingTest.v
+++ b/ArchSemArm/tests/UMPromisingTest.v
@@ -123,14 +123,6 @@ Module EOR.
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
-
-  Definition test_results_pf :=
-    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
-
-  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x110%Z].
-    vm_compute (_ <$> _).
-    reflexivity.
-  Qed.
 End EOR.
 
 Module LDR. (* LDR X0, [X1, X0] at 0x500, loading from 0x1000 *)
@@ -166,14 +158,6 @@ Module LDR. (* LDR X0, [X1, X0] at 0x500, loading from 0x1000 *)
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
-
-  Definition test_results_pf :=
-    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
-
-  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x2a%Z].
-    vm_compute (_ <$> _).
-    reflexivity.
-  Qed.
 End LDR.
 
 Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1100 *)
@@ -202,7 +186,7 @@ Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1
       archState.regs := [# init_reg];
       archState.address_space := PAS_NonSecure |}.
 
-  Definition fuel := 3%nat.
+  Definition fuel := 4%nat.
 
   Definition test_results :=
     UMPromising_cert_c arm_sem fuel n_threads termCond initState.
@@ -211,14 +195,6 @@ Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1
     vm_compute (_ <$> _).
     set_solver.
   Qed.
-
-  Definition test_results_pf :=
-    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
-
-  Goal reg_extract R0 0%fin <$> test_results_pf ≡ Listset [Ok 0x2a%Z].
-    vm_compute (_ <$> _).
-    set_solver.
-  Qed.
 End STRLDR.
 
 Module MP.
@@ -290,22 +266,13 @@ Module MP.
     vm_compute (elements _).
     apply NoDup_Permutation; try solve_NoDup; set_solver.
   Qed.
-
-  Definition test_results_pf :=
-    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
-
-  Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
-    [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]; Ok [0x1%Z; 0x0%Z]].
-  Proof.
-    vm_compute (elements _).
-    apply NoDup_Permutation; try solve_NoDup; set_solver.
-  Qed.
 End MP.
 
 Module MPDMBS.
   (* A classic MP litmus test
      Thread 1: STR X2, [X1, X0]; DMB SY; STR X5, [X4, X3]
      Thread 2: LDR X5, [X4, X3]; DMB SY; LDR X2, [X1, X0]
+
      Expected outcome of (R5, R2) at Thread 2:
        (0x1, 0x2a), (0x0, 0x2a), (0x0, 0x0)
   *)
@@ -361,25 +328,16 @@ Module MPDMBS.
       archState.regs := [# init_reg_t1; init_reg_t2];
       archState.address_space := PAS_NonSecure |}.
 
-  Definition fuel := 8%nat.
+  Definition fuel := 9%nat.
 
   Definition test_results :=
     UMPromising_cert_c arm_sem fuel n_threads termCond initState.
 
+  (** The test is fenced enough, the 0x1;0x0 outcome is impossible*)
   Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
     [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
   Proof.
     vm_compute (elements _).
     apply NoDup_Permutation; try solve_NoDup; set_solver.
   Qed.
-
-  Definition test_results_pf :=
-    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
-
-  Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
-    [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
-  Proof.
-    vm_compute (elements _).
-    apply NoDup_Permutation; try solve_NoDup; set_solver.
-  Qed.
 End MPDMBS.
diff --git a/ArchSemArm/tests/VMPromisingTest.v b/ArchSemArm/tests/VMPromisingTest.v
index c076bd8..810aba8 100644
--- a/ArchSemArm/tests/VMPromisingTest.v
+++ b/ArchSemArm/tests/VMPromisingTest.v
@@ -133,14 +133,6 @@ Module EORMMUOFF.
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
-
-  Definition test_results_pf :=
-    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
-
-  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x110%Z].
-    vm_compute (_ <$> _).
-    reflexivity.
-  Qed.
 End EORMMUOFF.
 
 (* Run EOR X0, X1, X2 at PC.
@@ -207,14 +199,6 @@ Module EOR.
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
-
-  Definition test_results_pf :=
-    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
-
-  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x110%Z].
-    vm_compute (_ <$> _).
-    reflexivity.
-  Qed.
 End EOR.
 
 (* LDR X0, [X1, X0] at VA 0x8000000500, loading from VA 0x8000001000
@@ -268,14 +252,6 @@ Module LDR.
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
-
-  Definition test_results_pf :=
-    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
-
-  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x2a%Z].
-    vm_compute (_ <$> _).
-    reflexivity.
-  Qed.
 End LDR.
 
 (* STR X2, [X1, X0]; LDR X0, [X1, X0] at VA 0x8000000500,
@@ -328,14 +304,6 @@ Module STRLDR.
     vm_compute (_ <$> _).
     set_solver.
   Qed.
-
-  Definition test_results_pf :=
-    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
-
-  Goal reg_extract R0 0%fin <$> test_results_pf ≡ Listset [Ok 0x2a%Z].
-    vm_compute (_ <$> _).
-    set_solver.
-  Qed.
 End STRLDR.
 
 (* Sequential page table modification in single thread *)
@@ -396,7 +364,7 @@ Module LDRPT.
       archState.regs := [# init_reg];
       archState.address_space := PAS_NonSecure |}.
 
-  Definition fuel := 4%nat.
+  Definition fuel := 5%nat.
 
   Definition test_results :=
     VMPromising_cert_c arm_sem fuel n_threads termCond initState.
@@ -408,17 +376,6 @@ Module LDRPT.
     vm_compute (elements _).
     apply NoDup_Permutation; try solve_NoDup; set_solver.
   Qed.
-
-  Definition test_results_pf :=
-    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
-
-  (* R0 should be 0x2a (from old mapping), R4 should be 0x42 (from new mapping) *)
-  Goal elements (regs_extract [(0%fin, R0); (0%fin, R4)] <$> test_results_pf) ≡ₚ
-      [Ok [0x2a%Z; 0x2a%Z]; Ok [0x2a%Z; 0x42%Z]].
-  Proof.
-    vm_compute (elements _).
-    apply NoDup_Permutation; try solve_NoDup; set_solver.
-  Qed.
 End LDRPT.
 
 Module MP.
@@ -500,9 +457,9 @@ Module MP.
       archState.regs := [# init_reg_t1; init_reg_t2];
       archState.address_space := PAS_NonSecure |}.
 
-  Definition fuel := 6%nat.
+  Definition fuel := 8%nat.
 
-  (* Definition test_results :=
+  Definition test_results :=
     VMPromising_cert_c arm_sem fuel n_threads termCond initState.
 
   Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
@@ -510,16 +467,6 @@ Module MP.
   Proof.
     vm_compute (elements _).
     apply NoDup_Permutation; try solve_NoDup; set_solver.
-  Qed. *)
-
-  Definition test_results_pf :=
-    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
-
-  Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
-    [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]; Ok [0x1%Z; 0x0%Z]].
-  Proof.
-    vm_compute (elements _).
-    apply NoDup_Permutation; try solve_NoDup; set_solver.
   Qed.
 End MP.
 
@@ -604,7 +551,7 @@ Module MPDMBS.
 
   Definition fuel := 8%nat.
 
-  (* Definition test_results :=
+  Definition test_results :=
     VMPromising_cert_c arm_sem fuel n_threads termCond initState.
 
   (** The test is fenced enough, the 0x1; 0x0 outcome is impossible*)
@@ -613,16 +560,5 @@ Module MPDMBS.
   Proof.
     vm_compute (elements _).
     apply NoDup_Permutation; try solve_NoDup; set_solver.
-  Qed. *)
-
-  Definition test_results_pf :=
-    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
-
-  (** The test is fenced enough, the 0x1; 0x0 outcome is impossible*)
-  Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
-    [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
-  Proof.
-    vm_compute (elements _).
-    apply NoDup_Permutation; try solve_NoDup; set_solver.
   Qed.
 End MPDMBS.

From 6d10f9e6c8528b45bb79df51183cbd02ab0bf99a Mon Sep 17 00:00:00 2001
From: Yeji Han <yeji.han@sf.snu.ac.kr>
Date: Wed, 26 Nov 2025 15:32:28 +0900
Subject: [PATCH 4/4] Re-add the computational model without promise-free
 optimization

---
 ArchSem/GenPromising.v             | 10 +++++++-
 ArchSemArm/UMPromising.v           |  7 ++++--
 ArchSemArm/VMPromising.v           |  7 ++++--
 ArchSemArm/tests/UMPromisingTest.v | 37 +++++++++++++++++++++++++++++
 ArchSemArm/tests/VMPromisingTest.v | 38 +++++++++++++++++++++++++++---
 5 files changed, 91 insertions(+), 8 deletions(-)

diff --git a/ArchSem/GenPromising.v b/ArchSem/GenPromising.v
index 5baf196..af6fbc6 100644
--- a/ArchSem/GenPromising.v
+++ b/ArchSem/GenPromising.v
@@ -431,9 +431,17 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
     Arguments to_final_archState {_ _ _}.
   End CPState.
 
-  (** Create a computational model from an ISA model and promising model *)
+  (** Create computational models from an ISA model and promising model *)
   Definition Promising_to_Modelc (isem : iMon ()) (prom : BasicExecutablePM)
       (fuel : nat) : archModel.c ∅ :=
+    λ n term (initMs : archState n),
+      PState.from_archState prom initMs |>
+      archModel.Res.from_exec
+        $ CPState.to_final_archState
+        <$> CPState.run isem prom term fuel.
+
+  Definition Promising_to_Modelc_pf (isem : iMon ()) (prom : BasicExecutablePM)
+      (fuel : nat) : archModel.c ∅ :=
     λ n term (initMs : archState n),
       PState.from_archState prom initMs |>
       archModel.Res.from_exec
diff --git a/ArchSemArm/UMPromising.v b/ArchSemArm/UMPromising.v
index cee7657..7def266 100644
--- a/ArchSemArm/UMPromising.v
+++ b/ArchSemArm/UMPromising.v
@@ -690,9 +690,9 @@ Section ComputeProm.
     let base := List.length mem in
     let res_proms := Exec.results $
       run_to_termination_promise isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
-    guard_or ("Could not finish promises within the size of the fuel")%string
+    guard_or ("Out of fuel when searching for new promises")%string
       (∀ r ∈ res_proms, r.2 = true);;
-    let promises := res_proms.*1.*1 |> CProm.proms ∘ union_list in
+    let promises := res_proms.*1.*1 |> union_list |> CProm.proms in
     let tstates :=
       res_proms
       |> omap (λ '((cp, st), _),
@@ -785,3 +785,6 @@ Next Obligation. Admitted.
 
 Definition UMPromising_cert_c isem fuel :=
   Promising_to_Modelc isem (UMPromising_exe' isem) fuel.
+
+Definition UMPromising_cert_c_pf isem fuel :=
+  Promising_to_Modelc_pf isem (UMPromising_exe' isem) fuel.
diff --git a/ArchSemArm/VMPromising.v b/ArchSemArm/VMPromising.v
index 8d52b35..8d41be2 100644
--- a/ArchSemArm/VMPromising.v
+++ b/ArchSemArm/VMPromising.v
@@ -1972,9 +1972,9 @@ Section ComputeProm.
     let base := List.length mem in
     let res_proms := Exec.results $
       run_to_termination_promise isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
-    guard_or ("Could not finish promises within the size of the fuel")%string
+    guard_or ("Out of fuel when searching for new promises")%string
       (∀ r ∈ res_proms, r.2 = true);;
-    let promises := res_proms.*1.*1 |> CProm.proms ∘ union_list in
+    let promises := res_proms.*1.*1 |> union_list |> CProm.proms in
     let tstates :=
       res_proms
       |> omap (λ '((cp, st), _),
@@ -2061,3 +2061,6 @@ Next Obligation. Admitted.
 
 Definition VMPromising_cert_c isem fuel :=
   Promising_to_Modelc isem (VMPromising_exe' isem) fuel.
+
+Definition VMPromising_cert_c_pf isem fuel :=
+  Promising_to_Modelc_pf isem (VMPromising_exe' isem) fuel.
diff --git a/ArchSemArm/tests/UMPromisingTest.v b/ArchSemArm/tests/UMPromisingTest.v
index 7e88e34..9a1f5c7 100644
--- a/ArchSemArm/tests/UMPromisingTest.v
+++ b/ArchSemArm/tests/UMPromisingTest.v
@@ -158,6 +158,14 @@ Module LDR. (* LDR X0, [X1, X0] at 0x500, loading from 0x1000 *)
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
+
+  Definition test_results_pf :=
+    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x2a%Z].
+    vm_compute (_ <$> _).
+    reflexivity.
+  Qed.
 End LDR.
 
 Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1100 *)
@@ -195,6 +203,14 @@ Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1
     vm_compute (_ <$> _).
     set_solver.
   Qed.
+
+  Definition test_results_pf :=
+    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal reg_extract R0 0%fin <$> test_results_pf ≡ Listset [Ok 0x2a%Z].
+    vm_compute (_ <$> _).
+    set_solver.
+  Qed.
 End STRLDR.
 
 Module MP.
@@ -266,6 +282,16 @@ Module MP.
     vm_compute (elements _).
     apply NoDup_Permutation; try solve_NoDup; set_solver.
   Qed.
+
+  Definition test_results_pf :=
+    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
+    [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]; Ok [0x1%Z; 0x0%Z]].
+  Proof.
+    vm_compute (elements _).
+    apply NoDup_Permutation; try solve_NoDup; set_solver.
+  Qed.
 End MP.
 
 Module MPDMBS.
@@ -340,4 +366,15 @@ Module MPDMBS.
     vm_compute (elements _).
     apply NoDup_Permutation; try solve_NoDup; set_solver.
   Qed.
+
+  Definition test_results_pf :=
+    UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  (** The test is fenced enough, the 0x1;0x0 outcome is impossible*)
+  Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
+    [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
+  Proof.
+    vm_compute (elements _).
+    apply NoDup_Permutation; try solve_NoDup; set_solver.
+  Qed.
 End MPDMBS.
diff --git a/ArchSemArm/tests/VMPromisingTest.v b/ArchSemArm/tests/VMPromisingTest.v
index 810aba8..58521b0 100644
--- a/ArchSemArm/tests/VMPromisingTest.v
+++ b/ArchSemArm/tests/VMPromisingTest.v
@@ -133,6 +133,14 @@ Module EORMMUOFF.
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
+
+  Definition test_results_pf :=
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x110%Z].
+    vm_compute (_ <$> _).
+    reflexivity.
+  Qed.
 End EORMMUOFF.
 
 (* Run EOR X0, X1, X2 at PC.
@@ -199,6 +207,14 @@ Module EOR.
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
+
+  Definition test_results_pf :=
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x110%Z].
+    vm_compute (_ <$> _).
+    reflexivity.
+  Qed.
 End EOR.
 
 (* LDR X0, [X1, X0] at VA 0x8000000500, loading from VA 0x8000001000
@@ -252,6 +268,14 @@ Module LDR.
     vm_compute (_ <$> _).
     reflexivity.
   Qed.
+
+  Definition test_results_pf :=
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x2a%Z].
+    vm_compute (_ <$> _).
+    reflexivity.
+  Qed.
 End LDR.
 
 (* STR X2, [X1, X0]; LDR X0, [X1, X0] at VA 0x8000000500,
@@ -304,6 +328,14 @@ Module STRLDR.
     vm_compute (_ <$> _).
     set_solver.
   Qed.
+
+  Definition test_results_pf :=
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
+
+  Goal reg_extract R0 0%fin <$> test_results_pf ≡ Listset [Ok 0x2a%Z].
+    vm_compute (_ <$> _).
+    set_solver.
+  Qed.
 End STRLDR.
 
 (* Sequential page table modification in single thread *)
@@ -367,7 +399,7 @@ Module LDRPT.
   Definition fuel := 5%nat.
 
   Definition test_results :=
-    VMPromising_cert_c arm_sem fuel n_threads termCond initState.
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
 
   (* R0 should be 0x2a (from old mapping), R4 should be 0x42 (from new mapping) *)
   Goal elements (regs_extract [(0%fin, R0); (0%fin, R4)] <$> test_results) ≡ₚ
@@ -460,7 +492,7 @@ Module MP.
   Definition fuel := 8%nat.
 
   Definition test_results :=
-    VMPromising_cert_c arm_sem fuel n_threads termCond initState.
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
 
   Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
     [Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]; Ok [0x1%Z; 0x0%Z]].
@@ -552,7 +584,7 @@ Module MPDMBS.
   Definition fuel := 8%nat.
 
   Definition test_results :=
-    VMPromising_cert_c arm_sem fuel n_threads termCond initState.
+    VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
 
   (** The test is fenced enough, the 0x1; 0x0 outcome is impossible*)
   Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ