correct_store_buffer: prove that a constrained store can advance

This proves that if a constrained store can advance, then an
unconstrained store can also advance, even in the case of a store buffer
in a different state.

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>

src/correct_store_buffer.v

@@ -152,4 +152,22 @@ Section constrained.
         reflexivity.
     - exact HconstT'.
   Qed.
+
+  (* If a constrained Lsu can advance, an unconstrained Lsu can advance. *)
+  (* Store version *)
+  Theorem constrained_lsu_store_advance_unconstrained_too :
+    e = (Store, (Lsu, 0)) ->
+    (* t is constrained, t' is unconstrained *)
+    (List.existsb is_in_su t) = true -> (List.existsb is_in_su t') = false ->
+    List.nth_error tc i = Some (Store, (Su, 0)) -> List.nth_error tc' i = Some (Store, (Su, 0)).
+  Proof.
+    intros He HconstT HconstT'.
+
+    constraint_delve He.
+
+    unfold suFree, get_instr_in_stage.
+    rewrite (not_existsb_means_cannot_find _ _ t').
+    - reflexivity.
+    - exact HconstT'.
+  Qed.
 End constrained.