correct_store_buffer: exclude cases that are not possible

Instead of proving that impossible cases (ie. stores in the Lu or loads
in the Su) are monotonic in moved_no_lat_is_monotonic, this exclude them from
the proof.

This also adds some comments to improve the clarity of the proof.

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

src/correct_store_buffer.v

@@ -282,7 +282,9 @@ Section monotonicity.
     compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
   Proof.
     intros He He' Hed Hsl.
-    specialize (Hsu st' opc).
+    specialize (Hlu st opc 0).
+    pose proof (Hsu st' opc) as Hsu'.
+    specialize (Hsu st opc).
 
     (* Goal transformation: show exactly how e and e' are modified by the
      * cycle function. *)
@@ -303,14 +305,22 @@ Section monotonicity.
     - now destruct (ready _ _ _ && free _ _ _ _), opc.
     - destruct (ready _ _ _ && free _ _ _ _), (ready _ _ _ && free _ _ _ _), opc;
         try reflexivity.
-      now discriminate Hsu.
+      now discriminate Hsu'.
     - now destruct (ready _ _ _ && free _ _ _ _), opc.
 
     (* st = Lu, st' = Sn *)
-    - now destruct opc.
+    - now destruct opc;
+        (* Trivial when opc = Load, eliminate the case where opc = Store. *)
+        [| discriminate Hlu].
 
     (* st = Su, st' = Sn *)
-    - now destruct (ready _ _ _ && free _ _ _ _), opc.
+    - now destruct opc; [
+          (* Eliminate the case where opc = Load. *)
+          discriminate Hsu |
+          (* Either the instruction remains in Su, or it progresses in Sn. *)
+          (* Both cases are trivial. *)
+          destruct (_ && _)
+        ].
   Qed.
 
   Hypothesis HvalidStLat : forall (e : instr_kind) st n, e = (Store, (st, n)) -> n = 0.