correct_store_buffer: if an instruction remains in the same stage, it progresses

This proves that if an instruction in the same stage while the pipeline
is in a more advanced state, if the one in the less advanced pipeline
can progress, the one in the more advanced pipeline can, too.

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

src/correct_store_buffer.v

@@ -163,6 +163,97 @@ Section monotonicity.
   Hypothesis HbusFree :
     busFree (existsb is_in_su t) sbState = true ->
     busFree (existsb is_in_su t') sbState' = true.
+
+  Ltac work_on_e He' :=
+    rewrite Htc, Htc', Ht;
+      rewrite Ht', <- He' in HfreeLsuPersists, HfreeFromLsuPersists, HbusFree |- *;
+      unfold cycle;
+      rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ (eq_refl _) Hi),
+        (map_in_the_middle _ _ e d _ _ tpre' tpost' _ (eq_refl _) Hi');
+      unfold cycle_elt;
+      rewrite <- Ht;
+      subst e.
+
+  Lemma unmoved_no_lat_can_advance :
+    e = (opc, (st, 0)) -> e = e' ->
+    List.nth_error tc i = Some (opc, (nstg st opc, 0)) ->
+    List.nth_error tc' i = Some (opc, (nstg st opc, 0)).
+  Proof.
+    intros He He'.
+    specialize (Hlu st opc).
+    specialize (Hsu st opc).
+
+    (* Delve onto e, then handle stages on a case-by-case basis. *)
+    work_on_e He'.
+    destruct st.
+
+    (* Sp.  The proof does not rely on the kind of instruction. *)
+    - destruct (free _ _ t _) in HfreeLsuPersists |- *.
+      + (* LSU is free in t. *)
+        now destruct (free _ _ _ _) in HfreeLsuPersists |- *;
+          (* Either the next stage is also free in t': trivial. *)
+          (* Otherwise, the next stage is not free in t':
+             this is impossible per HfreeLsuPersists. *)
+          [| discriminate HfreeLsuPersists].
+      + (* LSU is not free in t: this is irrelevant. *)
+        rewrite andb_false_r.
+        discriminate.
+
+    (* Lsu *)
+    - destruct opc, (free _ _ t _) in HfreeFromLsuPersists |- *.
+
+      (* Loads *)
+      + unfold ready.
+        destruct (busFree _ sbState).
+        * now destruct (busFree _ _);
+            [
+              destruct (free _ _ _ _) in HfreeFromLsuPersists |- *;
+                try discriminate HfreeFromLsuPersists |
+              discriminate HbusFree
+            ].
+        * discriminate.
+      + rewrite andb_false_r.
+        discriminate.
+
+      (* Stores *)
+      + now destruct (free _ _ _ _) in HfreeFromLsuPersists |- *;
+          [| discriminate HfreeFromLsuPersists].
+      + discriminate.
+
+    (* Lu: instructions without latency (this is the case here) move to Sn. *)
+    - now rewrite Hlu.
+
+    (* Su: if there is space in the store buffer, move to Sn, otherwise, remain
+       in Su.  Eliminate cases where sbState/sbState' are inconsistent. *)
+    - now rewrite Hsu;
+        destruct sbState, sbState', Hlsbt.
+
+    (* Sn: instructions remains in Sn. *)
+    - auto.
+  Qed.
+
+  Lemma unmoved_can_advance :
+    forall n, e = (opc, (st, n)) -> e = e' ->
+         compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
+  Proof.
+    intros n He He'.
+
+    pose proof (unmoved_no_lat_can_advance) as Huca.
+    revert Huca.
+    work_on_e He'.
+    intro Huca.
+
+    destruct n.
+    - destruct (ready _ _ _ && free _ _ t _).
+      + rewrite (Huca (eq_refl _) (eq_refl _) (eq_refl _)).
+        apply compare_two_eq_true.
+        discriminate.
+      + now destruct (ready _ _ _ && free _ _ _ _), st;
+          [| destruct opc |..].
+
+    - apply compare_two_eq_true.
+      discriminate.
+  Qed.
 End monotonicity.
 
 Section constrained.