correct_store_buffer: the behaviour is monotonic if e ⊏ e'

This proves that if e <> e', and if state_leb e e' = true, then the
behaviour of the store buffer is monotonic.

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

src/correct_store_buffer.v

@@ -307,4 +307,62 @@ Section monotonicity.
     (* st = Su, st' = Sn *)
     - now destruct (ready _ _ _ && free _ _ _ _), opc.
   Qed.
+
+  Hypothesis HvalidStLat : forall (e : instr_kind) st n, e = (Store, (st, n)) -> n = 0.
+  Hypothesis HvalidLdLat : forall (e : instr_kind) st n dlat, e = (Load dlat, (st, n)) -> 0 <> n -> st = Lu /\ n <= dlat.
+
+  Lemma moved_lat_is_lower :
+    forall n n', e = (opc, (st, n)) -> e' = (opc, (st', n')) -> e <> e' ->
+                 state_leb (st, n) (st', n') = true ->
+                 compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
+  Proof.
+    intros n n' He He' Hed Hsl.
+    pose proof (HvalidStLat e' st' n') as HvalidStLat'.
+    specialize (HvalidStLat e st n).
+    pose proof (HvalidLdLat e' st' n') as HvalidLdLat'.
+    specialize (HvalidLdLat e st n).
+
+    destruct n, n'; [
+        (* n and n' are = 0.  We have a lemma for that. *)
+        now apply moved_no_lat_is_lower |
+        (* Other cases: rewrite the goal to make cycle appear. *)
+        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';
+          (* Since n or n' is not equal to 0, opc is a load.  Remove other cases. *)
+          destruct opc;
+          [| discriminate (HvalidStLat (eq_refl _))
+             || discriminate (HvalidStLat' (eq_refl _))] ..
+      ].
+
+    (* From there, opc = Load. *)
+    (* n = 0 and n' <> 0. *)
+    - (* st' = Lu. *)
+      destruct (HvalidLdLat' n (eq_refl _) (O_S n')) as [Hst' Hlat'].
+      rewrite Hst' in Hsl, Hed |- *.
+      destruct st;
+        try discriminate.
+      + now destruct (_ && _).
+      + destruct (_ && _).
+        * simpl.
+          rewrite Nat.leb_le.
+          lia.
+        * reflexivity.
+
+    (* n <> 0 and n' = 0. *)
+    - (* st = Lu. *)
+      destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat].
+      rewrite Hst in Hsl, Hed |- *.
+      now destruct st'.
+
+    (* n and n' <> 0. *)
+    - destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat].
+      rewrite Hst in Hsl, Hed |- *.
+      now destruct (HvalidLdLat' n0 (eq_refl _) (O_S n')).
+  Qed.
 End monotonicity.