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

@@ -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