From d943294e1c9e8454a550dea6eefac57eef171c0a Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Mon, 4 Jul 2022 17:43:07 +0200
Subject: [PATCH] correct_store_buffer: prove that a constrained store can
advance
This proves that if a constrained store can advance, then an
unconstrained store can also advance, even in the case of a store buffer
in a different state.
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/correct_store_buffer.v | 18 ++++++++++++++++++
1 file changed, 18 insertions(+)
diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 009f1e5..4fa210e 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -152,4 +152,22 @@ Section constrained.
reflexivity.
- exact HconstT'.
Qed.
+
+ (* If a constrained Lsu can advance, an unconstrained Lsu can advance. *)
+ (* Store version *)
+ Theorem constrained_lsu_store_advance_unconstrained_too :
+ e = (Store, (Lsu, 0)) ->
+ (* t is constrained, t' is unconstrained *)
+ (List.existsb is_in_su t) = true -> (List.existsb is_in_su t') = false ->
+ List.nth_error tc i = Some (Store, (Su, 0)) -> List.nth_error tc' i = Some (Store, (Su, 0)).
+ Proof.
+ intros He HconstT HconstT'.
+
+ constraint_delve He.
+
+ unfold suFree, get_instr_in_stage.
+ rewrite (not_existsb_means_cannot_find _ _ t').
+ - reflexivity.
+ - exact HconstT'.
+ Qed.
End constrained.
--
GitLab