From 648758e4f5c04808303350d905591939b2aaf633 Mon Sep 17 00:00:00 2001
From: Florian Brandner <florian.brandner@telecom-paris.fr>
Date: Thu, 6 May 2021 20:52:13 +0200
Subject: [PATCH] correct Req_handled constraint and its proof.
---
coq/Arbiter.v | 16 +---------------
coq/FIFO.v | 34 +++++++++++++---------------------
2 files changed, 14 insertions(+), 36 deletions(-)
diff --git a/coq/Arbiter.v b/coq/Arbiter.v
index 45d5864..8074d40 100644
--- a/coq/Arbiter.v
+++ b/coq/Arbiter.v
@@ -4,20 +4,6 @@ From sdram Require Export Trace.
Section Arbiter.
Context {BANK_CFG : Bank_configuration}.
- Definition Match (req : Request_t) (cmd : Command_t) : bool :=
- match req.(Kind), cmd.(CKind) with
- | RD, CRD
- | WR, CWR => (cmd.(Request) == req)
- | _, _ => false
- end.
-
- Lemma Match_CmdT req t:
- Match req (Cmd_of_req req t).
- Proof.
- unfold Match, Cmd_of_req, Kind_of_req.
- destruct (Kind _); by simpl.
- Qed.
-
Class Arbiter_t := mkArbiter
{
Input : Requests_t;
@@ -26,6 +12,6 @@ Section Arbiter.
(* All Requests must handled *)
Req_handled : forall req, req \in Requests ->
- exists cmd : Command_t, (cmd \in Arbitrate.(Commands)) && ((Match req cmd))
+ exists t, (Cmd_of_req req t) \in Arbitrate.(Commands)
}.
End Arbiter.
diff --git a/coq/FIFO.v b/coq/FIFO.v
index 6e48417..05f3c79 100644
--- a/coq/FIFO.v
+++ b/coq/FIFO.v
@@ -301,32 +301,24 @@ Section FIFO.
- by apply (FIFO_trace_uniq a) in IHl.
*)
- Lemma FIFO_arbiter_handled req:
- req \in Requests -> exists cmd : Command_t, (cmd \in FIFO_arbitrate.(Commands)) /\
- ((cmd \in FIFO_arbitrate.(Commands)) -> Match req cmd).
+ Lemma FIFO_trace_Req_handled Reqs:
+ forall req, req \in Reqs ->
+ exists t, (Cmd_of_req req t) \in (FIFO_trace Reqs).(Cmds).
Proof.
intros.
- exists (Cmd_of_req req 5).
- split.
- - admit.
- -
- unfold FIFO_arbitrate in *. simpl in *.
- induction Requests.
- - by rewrite in_nil in H.
- - rewrite in_cons in H.
- destruct (req == a) eqn:Heq; move : Heq => /eqP Heq.
- - intros. subst. by apply Match_CmdT.
- - intros Hc.
- simpl in Hc. rewrite -> 3 in_cons in Hc.
- decompose_FIFO_cmds Hc Cmdb.
- - contradict Cmdb. by apply /eqP /Command_neq_req_CMD.
- - contradict Cmdb. by apply /eqP /Command_neq_CMD_ACT.
- - contradict Cmdb. by apply /eqP /Command_neq_CMD_PRE.
- - rewrite Bool.orb_false_l in H. by apply IHl.
+ induction Reqs.
+ - by contradict H.
+ - move : H => /orP [/eqP Heq | H].
+ - exists ((maxn (FIFO_trace Reqs).(Time) req.(Date)) + FIFO_CMD_date).
+ subst. rewrite in_cons. apply /orP. by left.
+ - apply IHReqs in H.
+ destruct H as [t IH].
+ exists (t).
+ by do 3 (rewrite in_cons; apply /orP; right).
Qed.
Instance FIFO_arbiter : Arbiter_t :=
- mkArbiter Input FIFO_arbitrate FIFO_arbiter_handled.
+ mkArbiter Input FIFO_arbitrate (FIFO_trace_Req_handled Requests).
End FIFO.
Section Test.
--
GitLab