correct_store_buffer: an more advanced instruction stays more advanced

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

src/correct_store_buffer.v

@@ -254,6 +254,55 @@ Section monotonicity.
     - apply compare_two_eq_true.
       discriminate.
   Qed.
+
+  Variable st' : stage.
+
+  Lemma moved_no_lat_is_lower :
+    e = (opc, (st, 0)) -> e' = (opc, (st', 0)) -> e <> e' ->
+    state_leb (st, 0) (st', 0) = true ->
+    compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
+  Proof.
+    intros He He' Hed Hsl.
+    specialize (Hlu st opc).
+    specialize (Hsu st' opc).
+
+    (* work_on_e replacement. *)
+    (* Goal transformation: show exactly how e and e' are modified by the
+     * cycle function. *)
+    rewrite Htc, Htc', Ht, Ht'.
+    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, <- Ht'.
+    subst e.
+    subst e'.
+
+    (* Case-by-case analysis *)
+    destruct st, st';
+      try contradiction;
+      try discriminate.
+
+    (* st = Sp, st' = Lsu, Lu, Su, Sn *)
+    - now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc.
+    - now destruct (ready _ _ _ && free _ _ _ _), opc.
+    - now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _).
+    - now destruct (ready _ _ _ && free _ _ _ _), opc.
+
+    (* st = Lsu, st' = Lu, Su, Sn *)
+    - now destruct (ready _ _ _ && free _ _ _ _), opc.
+    - destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc;
+        try reflexivity.
+      now discriminate Hsu.
+    - now destruct (ready _ _ _ && free _ _ _ _), opc.
+
+    (* st = Lu, st' = Sn *)
+    - now destruct opc;
+        [| discriminate Hlu].
+
+    (* st = Su, st' = Sn *)
+    - now destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _).
+  Qed.
 End monotonicity.
 
 Section constrained.