diff --git a/ArchSem/GenPromising.v b/ArchSem/GenPromising.v
index c9c4839..af6fbc6 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,20 +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.
 
-    (** 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
+    (** 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;
@@ -378,21 +390,63 @@ 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".
+
+    (** 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 ←
+          vmapM (λ '(tid, ts),
+            '(promises_per_tid, tstates_per_tid) ←
+              mlift $ prom.(enumerate_promises_and_terminal_states)
+                        fuel (fin_to_nat tid) (term tid) (initmem st) ts (events st);
+            mret (map (.,tid) promises_per_tid, tstates_per_tid)
+          ) (venumerate (tstates st));
+
+        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);;
+          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 {_ _ _}.
   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 ∅ :=
-    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.
 
-    (* TODO state some soundness lemma between Promising_to_Modelnc and
-        Promising_Modelc *)
+  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.
 
 End GenPromising.
 
diff --git a/ArchSemArm/UMPromising.v b/ArchSemArm/UMPromising.v
index 7616dc9..7def266 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,7 +457,8 @@ 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) :
+          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;
@@ -489,7 +490,7 @@ Definition write_mem_xcl (tid : nat) (loc : Loc.t)
            (vdata : view) (macc : mem_acc)
            (mem : Memory.t) (data : val)
   : 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;
@@ -659,11 +660,14 @@ Section ComputeProm.
     else
       mret res.
 
-  Fixpoint runSt_to_termination
+  (* 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)
-                      (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,26 @@ 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)
-      : 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 ("Out of fuel when searching for new promises")%string
+      (∀ r ∈ res_proms, r.2 = true);;
+    let promises := res_proms.*1.*1 |> union_list |> CProm.proms 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.
 
@@ -764,12 +774,17 @@ 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.
 
 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 e80f164..8d41be2 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
@@ -1558,8 +1558,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) :=
+      (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
   '(ts, mem) ← mGet;
@@ -1585,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.
 
@@ -1896,7 +1893,7 @@ Section RunOutcome.
   | _ => mthrow "Unsupported outcome".
 
   Definition run_outcome' (out : outcome) :
-    Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
+      Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
     run_outcome out |$> fst.
 
 End RunOutcome.
@@ -1945,11 +1942,14 @@ Section ComputeProm.
     else
       mret res.
 
-  Fixpoint runSt_to_termination
+  (* 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)
-                      (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 +1961,26 @@ 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)
-      : 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 ("Out of fuel when searching for new promises")%string
+      (∀ r ∈ res_proms, r.2 = true);;
+    let promises := res_proms.*1.*1 |> union_list |> CProm.proms 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.
 
@@ -2023,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;
@@ -2040,16 +2045,22 @@ 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.
 
 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 3107b03..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 *)
@@ -186,7 +194,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.
@@ -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.
@@ -328,7 +354,7 @@ 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.
@@ -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 4b39827..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 *)
@@ -364,10 +396,10 @@ 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.
+    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) ≡ₚ
@@ -378,7 +410,7 @@ Module LDRPT.
   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 +465,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,16 +485,14 @@ 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 fuel := 8%nat.
 
   Definition test_results :=
-    VMPromising_cert_c arm_sem fuel n_threads 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]].
@@ -470,9 +500,9 @@ End LDRPT.
     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 +564,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 +577,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.
+    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) ≡ₚ
@@ -565,4 +593,4 @@ End MP. *)
     vm_compute (elements _).
     apply NoDup_Permutation; try solve_NoDup; set_solver.
   Qed.
-End MPDMBS. *)
+End MPDMBS.
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)).