correct_store_buffer: prove that an unconstrained Sp can advance

This proves that if a constrained Sp can advance, then an unconstrained
Sp can advance, too.

Note that the pipeline may not be strictly in the same state: the state
of the store buffer may change.

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

src/correct_store_buffer.v

@@ -96,3 +96,60 @@ Section can_advance.
         lia.
   Qed.
 End can_advance.
+
+Section constrained.
+  Variable opc : opcode.
+  Variable e d : instr_kind.
+  Variable t tpre tpost t' tpre' tpost' tc tc' : trace_kind.
+  Variable i : nat.
+  Variable sbState sbState' : sbStateT.
+
+  Hypothesis Ht : t = tpre ++ e :: tpost.
+  Hypothesis Ht' : t' = tpre' ++ e :: tpost'.
+  Hypothesis Hi : i = List.length tpre.
+  Hypothesis Hl : List.length tpre' = List.length tpre.
+  Hypothesis Hl' : List.length tpost' = List.length tpost.
+  Hypothesis Htc : tc = cycle sbState t.
+  Hypothesis Htc' : tc' = cycle sbState' t'.
+
+  (* Delve into tc, tc', cycle, cycle_elt, etc.
+   * Pretty specific to these constraints, do not use it outside this section. *)
+  Ltac constraint_delve He :=
+    rewrite Htc, Htc';
+      unfold cycle;
+      rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _),
+        (map_in_the_middle _ _ e d _ _ tpre' tpost' _);
+      [ unfold cycle_elt;
+          destruct e;
+          match goal with
+          | [ s : state |- _ ] =>
+              destruct s;
+                injection He;
+                intros Hn Hs Ho;
+                rewrite Ho, Hs, Hn;
+                simpl
+          end |
+        exact Ht' |
+        rewrite Hi, Hl;
+          reflexivity |
+        exact Ht |
+        exact Hi ].
+
+  (* If a constrained Sp can advance, an unconstrained Sp can advance. *)
+  Theorem constrained_sp_can_advance_unconstrained_too :
+    e = (opc, (Sp, 0)) ->
+    (* t is constrained, t' is unconstrained *)
+    (List.existsb is_in_lsu t) = true -> (List.existsb is_in_lsu t') = false ->
+    List.nth_error tc i = Some (opc, (Lsu, 0)) -> List.nth_error tc' i = Some (opc, (Lsu, 0)).
+  Proof.
+    intros He HconstT HconstT'.
+
+    constraint_delve He.
+
+    unfold lsuFree, get_instr_in_stage.
+    rewrite (not_existsb_means_cannot_find _ _ t').
+    - destruct opc;
+        reflexivity.
+    - exact HconstT'.
+  Qed.
+End constrained.