From 335b54b26ab65d2d78580cae75953913a2d80345 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Fri, 29 Jul 2022 15:41:01 +0200
Subject: [PATCH] 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 | 18 ++++++++++++++----
1 file changed, 14 insertions(+), 4 deletions(-)
diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index e375b48..4616ed4 100644
--- a/src/correct_store_buffer.v
+++ b/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.
--
GitLab