From 10da722cda08bd35d7ad2ba3e7172372abb9bc7e Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 26 Jul 2022 16:47:15 +0200
Subject: [PATCH] correct_store_buffer: an more advanced instruction stays more
advanced
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/correct_store_buffer.v | 49 ++++++++++++++++++++++++++++++++++++++
1 file changed, 49 insertions(+)
diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 4a5e566..5f858ca 100644
--- a/src/correct_store_buffer.v
+++ b/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.
--
GitLab