From 23412a35fd4f0f6b5db04aed59aa35775f8bec27 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 5 Jul 2022 19:49:19 +0200
Subject: [PATCH] correct_sb: cleanup proofs
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/correct_store_buffer.v | 16 +++++++---------
1 file changed, 7 insertions(+), 9 deletions(-)
diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 7dd8dbc..f49d3f6 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -110,6 +110,7 @@ Section constrained.
Hypothesis Hl' : List.length tpost' = List.length tpost.
Hypothesis Htc : tc = cycle sbState t.
Hypothesis Htc' : tc' = cycle sbState' t'.
+ Hypothesis HconstT : is_constrained e t sbState = true.
(* Delve into tc, tc', cycle, cycle_elt, etc.
* Pretty specific to these constraints, do not use it outside this section. *)
@@ -136,12 +137,11 @@ Section constrained.
(* 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 *)
- is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
+ e = (opc, (Sp, 0)) -> 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'.
+ intros He HconstT'.
rewrite He in HconstT'.
constraint_delve He.
@@ -155,12 +155,11 @@ Section constrained.
(* If a constrained Lsu can advance, an unconstrained Lsu can advance. *)
(* Load version *)
Theorem constrained_lsu_load_advance_unconstrained_too :
- e = (Load, (Lsu, 0)) ->
(* t is constrained, t' is unconstrained *)
- is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
+ e = (Load, (Lsu, 0)) -> is_constrained e t' sbState' = false ->
List.nth_error tc i = Some (Load, (Lu, 0)) -> List.nth_error tc' i = Some (Load, (Lu, 0)).
Proof.
- intros He Hconst.
+ intro He.
rewrite He.
unfold is_constrained.
@@ -181,12 +180,11 @@ Section constrained.
(* Store version *)
Theorem constrained_lsu_store_advance_unconstrained_too :
- e = (Store, (Lsu, 0)) ->
(* t is constrained, t' is unconstrained *)
- is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
+ e = (Store, (Lsu, 0)) -> 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'.
+ intros He HconstT'.
rewrite He in HconstT'.
constraint_delve He.
--
GitLab