diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v index 4fa210e537441ffc84c2f8e97ec76bff7bf138a1..ad294d4dfd04cdfa471f54416a17d2fd4b42ce6a 100644 --- a/src/correct_store_buffer.v +++ b/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.