diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v index 8013edcf5835c1339030c8638add3e8c7d28a0ba..47598bb8e61c674640ed640d6dae78d8c4c63c21 100644 --- a/src/correct_store_buffer.v +++ b/src/correct_store_buffer.v @@ -169,13 +169,25 @@ Section monotonicity. Ltac work_on_e He' := rewrite Htc, Htc', Ht; - rewrite Ht', <- He' in HfreeLsuPersists, HfreeFromLsuPersists, HbusFree |- *; + match goal with + | [ _ : e = e' |- _ ] => + rewrite Ht', <- He' in HfreeLsuPersists, HfreeFromLsuPersists, HbusFree |- * + | [ _ : e <> e' |- _ ] => + rewrite Ht' + end; unfold cycle; rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ (eq_refl _) Hi), - (map_in_the_middle _ _ e d _ _ tpre' tpost' _ (eq_refl _) Hi'); + (map_in_the_middle _ _ _ d _ _ tpre' tpost' _ (eq_refl _) Hi'); unfold cycle_elt; rewrite <- Ht; - subst e. + match goal with + | [ _ : e = e' |- _ ] => + subst e + | [ _ : e <> e' |- _ ] => + rewrite <- Ht'; + subst e; + subst e' + end. Lemma unmoved_no_lat_can_advance : e = (opc, (st, 0)) -> e = e' -> forall n, @@ -271,17 +283,9 @@ Section monotonicity. intros He He' Hed Hsl. specialize (Hsu st' opc). - (* work_on_e replacement. *) (* Goal transformation: show exactly how e and e' are modified by the * cycle function. *) - rewrite Htc, Htc', Ht, Ht'. - unfold cycle. - rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ (eq_refl _) Hi), - (map_in_the_middle _ _ e' d _ _ tpre' tpost' _ (eq_refl _) Hi'). - unfold cycle_elt. - rewrite <- Ht, <- Ht'. - subst e. - subst e'. + work_on_e Hed. (* Case-by-case analysis *) destruct st, st'; @@ -326,14 +330,7 @@ Section monotonicity. (* n and n' are = 0. We have a lemma for that. *) now apply moved_no_lat_is_monotonic | (* Other cases: rewrite the goal to make cycle appear. *) - rewrite Htc, Htc', Ht, Ht'; - unfold cycle; - rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _ (eq_refl _) Hi), - (map_in_the_middle _ _ e' d _ _ tpre' tpost' _ (eq_refl _) Hi'); - unfold cycle_elt; - rewrite <- Ht, <- Ht'; - subst e; - subst e'; + work_on_e Hed; (* Since n or n' is not equal to 0, opc is a load. Remove other cases. *) destruct opc; [| discriminate (HvalidStLat (eq_refl _))