Re-add the computational model without promise-free optimization

Author: febyeji

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

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.

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.

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.

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) ≡ₚ