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

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