From ae48254e313d60796ff146adf188c7bc16a85d8a Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Mon, 4 Jul 2022 17:41:47 +0200
Subject: [PATCH] correct_store_buffer: prove that an unconstrained Sp can
advance
This proves that if a constrained Sp can advance, then an unconstrained
Sp can advance, too.
Note that the pipeline may not be strictly in the same state: the state
of the store buffer may change.
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/correct_store_buffer.v | 57 ++++++++++++++++++++++++++++++++++++++
1 file changed, 57 insertions(+)
diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 8ffa7ce..009f1e5 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -96,3 +96,60 @@ Section can_advance.
lia.
Qed.
End can_advance.
+
+Section constrained.
+ Variable opc : opcode.
+ Variable e d : instr_kind.
+ Variable t tpre tpost t' tpre' tpost' tc tc' : trace_kind.
+ Variable i : nat.
+ Variable sbState sbState' : sbStateT.
+
+ Hypothesis Ht : t = tpre ++ e :: tpost.
+ Hypothesis Ht' : t' = tpre' ++ e :: tpost'.
+ Hypothesis Hi : i = List.length tpre.
+ Hypothesis Hl : List.length tpre' = List.length tpre.
+ Hypothesis Hl' : List.length tpost' = List.length tpost.
+ Hypothesis Htc : tc = cycle sbState t.
+ Hypothesis Htc' : tc' = cycle sbState' t'.
+
+ (* Delve into tc, tc', cycle, cycle_elt, etc.
+ * Pretty specific to these constraints, do not use it outside this section. *)
+ Ltac constraint_delve He :=
+ rewrite Htc, Htc';
+ unfold cycle;
+ rewrite (map_in_the_middle _ _ e d _ _ tpre tpost _),
+ (map_in_the_middle _ _ e d _ _ tpre' tpost' _);
+ [ unfold cycle_elt;
+ destruct e;
+ match goal with
+ | [ s : state |- _ ] =>
+ destruct s;
+ injection He;
+ intros Hn Hs Ho;
+ rewrite Ho, Hs, Hn;
+ simpl
+ end |
+ exact Ht' |
+ rewrite Hi, Hl;
+ reflexivity |
+ exact Ht |
+ exact Hi ].
+
+ (* If a constrained Sp can advance, an unconstrained Sp can advance. *)
+ Theorem constrained_sp_can_advance_unconstrained_too :
+ e = (opc, (Sp, 0)) ->
+ (* t is constrained, t' is unconstrained *)
+ (List.existsb is_in_lsu t) = true -> (List.existsb is_in_lsu t') = false ->
+ List.nth_error tc i = Some (opc, (Lsu, 0)) -> List.nth_error tc' i = Some (opc, (Lsu, 0)).
+ Proof.
+ intros He HconstT HconstT'.
+
+ constraint_delve He.
+
+ unfold lsuFree, get_instr_in_stage.
+ rewrite (not_existsb_means_cannot_find _ _ t').
+ - destruct opc;
+ reflexivity.
+ - exact HconstT'.
+ Qed.
+End constrained.
--
GitLab