diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v index 3438fe32137cf93815b5eeb06c99c57ff5437bb3..8013edcf5835c1339030c8638add3e8c7d28a0ba 100644 --- a/src/correct_store_buffer.v +++ b/src/correct_store_buffer.v @@ -347,8 +347,11 @@ Section monotonicity. rewrite Hst' in Hsl, Hed |- *. destruct st; try discriminate. - + now destruct (_ && _). - + destruct (_ && _). + + (* st = Sp. In this case, the next stage is either Sp or Lsu, which are + * both lower than Lu. *) + now destruct (_ && _). + + (* st = Lsu. In this case, the next stage is either Lsu or Lu. *) + destruct (_ && _). * simpl. rewrite Nat.leb_le. lia. @@ -358,11 +361,19 @@ Section monotonicity. - (* st = Lu. *) destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat]. rewrite Hst in Hsl, Hed |- *. - now destruct st'. + destruct st'; + (* Sp, Lsu: impossible since e' would be lower than e. *) + (* Su: impossible since loads cannot be in Su. *) + discriminate + (* Lu: since n' = 0, e' will be in Sn in the next cycle, e will still be + * in Lu. *) + (* Sn: e' will remain in Sn, e will still be in Lu. *) + || reflexivity. (* n and n' <> 0. *) - destruct (HvalidLdLat n0 (eq_refl _) (O_S n)) as [Hst Hlat]. rewrite Hst in Hsl, Hed |- *. + (* e is lower than e', hence n > n'. *) now destruct (HvalidLdLat' n0 (eq_refl _) (O_S n')). Qed.