Skip to content
Snippets Groups Projects
Commit 9cfc8c03 authored by Alban Gruin's avatar Alban Gruin
Browse files

correct_store_buffer: the store buffer is monotonic


Since the store buffer is monotonic when e = e' and state_leb e e' =
true, and is also monotonic when e <> e' and state_leb e e' = true, and
since (e = e') \/ (e <> e'), then the store buffer is monotonic.

The proof invokes the instr_kind comparison lemma to split the two
cases, and applies the monotonicity lemmas on each corresponding case.

Signed-off-by: default avatarAlban Gruin <alban.gruin@irit.fr>
parent 47a9db6d
No related branches found
No related tags found
No related merge requests found
......@@ -365,4 +365,17 @@ Section monotonicity.
rewrite Hst in Hsl, Hed |- *.
now destruct (HvalidLdLat' n0 (eq_refl _) (O_S n')).
Qed.
Theorem is_monotonic :
forall n n', e = (opc, (st, n)) -> e' = (opc, (st', n')) ->
state_leb (st, n) (st', n') = true ->
compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
Proof.
intros n n' He He' Hsl.
pose proof (instr_kind_is_comparable e e') as Heqd.
destruct Heqd as [Heq | Hdiff].
- now apply (unmoved_can_advance n).
- now apply (moved_lat_is_lower n n').
Qed.
End monotonicity.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment