diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v index ad294d4dfd04cdfa471f54416a17d2fd4b42ce6a..c000ebf945f11846adac85e35f203dd4cb56e57b 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.