From c6795c42f587d4882409274912f81f714e3dcdc3 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 5 Jul 2022 00:06:39 +0200
Subject: [PATCH] correct_store_buffer: prove that an unconstrained Load in Lsu
 can advance

Signed-off-by: Alban Gruin <alban@pa1ch.fr>
---
 src/correct_store_buffer.v | 30 ++++++++++++++++++++++++++++--
 1 file changed, 28 insertions(+), 2 deletions(-)

diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index ad294d4..c000ebf 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -157,9 +157,35 @@ Section constrained.
     constraint_delve He.
 
     unfold lsuFree, get_instr_in_stage.
+    rewrite (not_existsb_means_cannot_find _ _ t');
+      destruct opc;
+      reflexivity || exact HconstT'.
+  Qed.
+
+  (* If a constrained Lsu can advance, an unconstrained Lsu can advance. *)
+  (* Load version *)
+  Theorem constrained_lsu_load_advance_unconstrained_too :
+    e = (Load, (Lsu, 0)) ->
+    (* t is constrained, t' is unconstrained *)
+    is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
+    List.nth_error tc i = Some (Load, (Lu, 0)) -> List.nth_error tc' i = Some (Load, (Lu, 0)).
+  Proof.
+    intros He Hconst.
+
+    rewrite He.
+    unfold is_constrained.
+    destruct sbState';
+      try discriminate.
+    intro HconstT'.
+    apply orb_false_elim in HconstT'.
+    destruct HconstT' as [HconstT' HconstT'2].
+
+    constraint_delve He.
+
+    unfold luFree, get_instr_in_stage.
     rewrite (not_existsb_means_cannot_find _ _ t').
-    - destruct opc;
-        reflexivity.
+    - rewrite HconstT'2.
+      reflexivity.
     - exact HconstT'.
   Qed.
 
-- 
GitLab