correct_store_buffer: redefine constaints and use it in the proofs

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>

src/correct_store_buffer.v

@@ -66,6 +66,15 @@ Definition cycle sbState trace :=
   let isSuUsed := List.existsb is_in_su trace in
   List.map (cycle_elt isSuUsed sbState trace) trace.
 
+Definition is_constrained (elt : instr_kind) trace sbState :=
+  match elt, sbState with
+  | (_, (Sp, _)), _ => List.existsb is_in_lsu trace
+  | (Load, (Lsu, _)), Empty => List.existsb is_in_lu trace || List.existsb is_in_su trace
+  | (Load, (Lsu, _)), _ => true
+  | (Store, (Lsu, _)), _ => List.existsb is_in_su trace
+  | _, _ => false
+  end.
+
 Section can_advance.
   Variable isSuUsed : bool.
   Variable sbState : sbStateT.
@@ -139,10 +148,11 @@ Section constrained.
   Theorem constrained_sp_can_advance_unconstrained_too :
     e = (opc, (Sp, 0)) ->
     (* t is constrained, t' is unconstrained *)
-    (List.existsb is_in_lsu t) = true -> (List.existsb is_in_lsu t') = false ->
+    is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
     List.nth_error tc i = Some (opc, (Lsu, 0)) -> List.nth_error tc' i = Some (opc, (Lsu, 0)).
   Proof.
     intros He HconstT HconstT'.
+    rewrite He in HconstT'.
 
     constraint_delve He.
 
@@ -153,15 +163,15 @@ Section constrained.
     - 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 ->
+    is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
     List.nth_error tc i = Some (Store, (Su, 0)) -> List.nth_error tc' i = Some (Store, (Su, 0)).
   Proof.
     intros He HconstT HconstT'.
+    rewrite He in HconstT'.
 
     constraint_delve He.