From 6977e6b7e1678404ee9bba07b341e3c3938bb328 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Fri, 29 Jul 2022 15:39:19 +0200
Subject: [PATCH] correct_store_buffer: add a parameter to HbusFree
This add a stage as a parameter to HbusFree. This is to make it more
correct (this hypothesis is only true if we are in the Lsu), and forbid
from using it in theorems where it is not specialized.
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/correct_store_buffer.v | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 47598bb..e375b48 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -164,6 +164,7 @@ Section monotonicity.
free (existsb is_in_su t') sbState' t' (opc, (Lsu, 0)) = true.
Hypothesis HbusFree :
+ forall st, st = Lsu ->
busFree (existsb is_in_su t) sbState = true ->
busFree (existsb is_in_su t') sbState' = true.
@@ -197,6 +198,7 @@ Section monotonicity.
intros He He' n.
specialize (Hlu st opc).
specialize (Hsu st opc).
+ specialize (HbusFree st).
(* Delve onto e, then handle stages on a case-by-case basis. *)
work_on_e He'.
@@ -220,8 +222,7 @@ Section monotonicity.
(* Loads *)
+ unfold ready.
destruct (busFree _ sbState).
- * now destruct (busFree _ _);
- [
+ * now destruct (busFree _ _); [
destruct (free _ _ _ _) in HfreeFromLsuPersists |- *;
try discriminate HfreeFromLsuPersists |
discriminate HbusFree
--
GitLab