From 9cfc8c03e6b6ced1e7eb8620c408ff0837e04c2c Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Wed, 27 Jul 2022 23:34:00 +0200
Subject: [PATCH] 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: Alban Gruin <alban.gruin@irit.fr>
---
src/correct_store_buffer.v | 13 +++++++++++++
1 file changed, 13 insertions(+)
diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 35430b2..66839c4 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -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.
--
GitLab