From 7ee4f3525022698bea742b819a2a711fb063001c Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 5 Jul 2022 00:04:36 +0200
Subject: [PATCH] correct_store_buffer: redefine constaints and use it in the
proofs
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/correct_store_buffer.v | 16 +++++++++++++---
1 file changed, 13 insertions(+), 3 deletions(-)
diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 4fa210e..ad294d4 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -66,6 +66,15 @@ Definition cycle sbState trace :=
let isSuUsed := List.existsb is_in_su trace in
List.map (cycle_elt isSuUsed sbState trace) trace.
+Definition is_constrained (elt : instr_kind) trace sbState :=
+ match elt, sbState with
+ | (_, (Sp, _)), _ => List.existsb is_in_lsu trace
+ | (Load, (Lsu, _)), Empty => List.existsb is_in_lu trace || List.existsb is_in_su trace
+ | (Load, (Lsu, _)), _ => true
+ | (Store, (Lsu, _)), _ => List.existsb is_in_su trace
+ | _, _ => false
+ end.
+
Section can_advance.
Variable isSuUsed : bool.
Variable sbState : sbStateT.
@@ -139,10 +148,11 @@ Section constrained.
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 ->
+ is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
List.nth_error tc i = Some (opc, (Lsu, 0)) -> List.nth_error tc' i = Some (opc, (Lsu, 0)).
Proof.
intros He HconstT HconstT'.
+ rewrite He in HconstT'.
constraint_delve He.
@@ -153,15 +163,15 @@ Section constrained.
- exact HconstT'.
Qed.
- (* If a constrained Lsu can advance, an unconstrained Lsu can advance. *)
(* Store version *)
Theorem constrained_lsu_store_advance_unconstrained_too :
e = (Store, (Lsu, 0)) ->
(* t is constrained, t' is unconstrained *)
- (List.existsb is_in_su t) = true -> (List.existsb is_in_su t') = false ->
+ is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
List.nth_error tc i = Some (Store, (Su, 0)) -> List.nth_error tc' i = Some (Store, (Su, 0)).
Proof.
intros He HconstT HconstT'.
+ rewrite He in HconstT'.
constraint_delve He.
--
GitLab