diff --git a/coq/Arbiter.v b/coq/Arbiter.v
index 5a7c7bb9c31c037aa91d111a14333499d5c1a004..6e799d71c00a5b1a0ad1fec25e3df97654dbae01 100644
--- a/coq/Arbiter.v
+++ b/coq/Arbiter.v
@@ -1,5 +1,4 @@
Set Warnings "-notation-overridden,-parsing".
-From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
From sdram Require Export Trace.
Section Arbiter.
diff --git a/coq/Commands.v b/coq/Commands.v
index c124f1a260e91627933a22eb3ff31cae30315fef..88727e10a5f54544b44e2146b3fac131ec7e6d78 100644
--- a/coq/Commands.v
+++ b/coq/Commands.v
@@ -80,5 +80,28 @@ Section Commands.
Definition Cmd_of_req req t :=
mkCmd t (Kind_of_req req) req.
+ Lemma Command_ne_ACT_PRE
+ reqa ta reqb tb: (ACT_of_req reqa ta) != (PRE_of_req reqb tb).
+ Proof.
+ unfold ACT_of_req, PRE_of_req. unfold "==". simpl. unfold Commands.Command_eqdef. simpl.
+ rewrite negb_and. apply /orP. by right.
+ Qed.
+
+ Lemma Command_ne_CMD_ACT
+ reqa ta reqb tb: (Cmd_of_req reqa ta) != (ACT_of_req reqb tb).
+ Proof.
+ unfold ACT_of_req, Cmd_of_req, Kind_of_req. unfold "==". simpl. unfold Commands.Command_eqdef. simpl.
+ rewrite negb_and. apply /orP.
+ destruct (Kind reqa);by right.
+ Qed.
+
+ Lemma Command_ne_CMD_PRE
+ reqa ta reqb tb: (Cmd_of_req reqa ta) != (PRE_of_req reqb tb).
+ Proof.
+ unfold PRE_of_req, Cmd_of_req, Kind_of_req. unfold "==". simpl. unfold Commands.Command_eqdef. simpl.
+ rewrite negb_and. apply /orP.
+ destruct (Kind reqa);by right.
+ Qed.
+
Definition Commands_t := seq Command_t.
End Commands.
diff --git a/coq/FIFO.v b/coq/FIFO.v
index 65328890e21145c48f70e949a79a6e9b45b0dd0a..59b70a8b8174d5f2a39d37655c4a67b98b9aa531 100644
--- a/coq/FIFO.v
+++ b/coq/FIFO.v
@@ -1,51 +1,170 @@
Set Warnings "-notation-overridden,-parsing".
-From sdram Require Import Arbiter.
+From sdram Require Export Arbiter Requests.
Section FIFO.
Context {BANK_CFG : Bank_configuration}.
Context {Input : Requests_t}.
+ Class FIFO_configuration :=
+ {
+ FIFO_wait : {T : nat | 3 < T (* have to issue at least 3 commands *)
+ /\ T_RC_NAT <= T (* have to respect T_RC *)}
+ }.
+
+ Context {FIFO_CFG : FIFO_configuration }.
+
Local Record FIFO_state_t := mkFIFO
{
Cmds : Commands_t;
Time : nat;
}.
- Definition FIFO_wait := T_RC.
Local Program Definition FIFO_req req State : FIFO_state_t :=
- let PRE_date := State.(Time) + 1 in
- let ACT_date := State.(Time) + 2 in
- let CMD_date := State.(Time) + 3 in
+ let time := maxn State.(Time) req.(Date) in
+ let PRE_date := time + 1 in
+ let ACT_date := time + 2 in
+ let CMD_date := time + 3 in
let PRE := PRE_of_req req PRE_date in
let ACT := ACT_of_req req ACT_date in
let CMD := Cmd_of_req req CMD_date in
- let Cmds := PRE::ACT::CMD::State.(Cmds) in
- mkFIFO Cmds (State.(Time) + FIFO_wait).
+ let Cmds := CMD::ACT::PRE::State.(Cmds) in
+ mkFIFO Cmds (time + FIFO_wait).
- Local Fixpoint FIFO_trace Reqs State : FIFO_state_t :=
+ Local Fixpoint FIFO_trace Reqs : FIFO_state_t :=
match Reqs with
- | [::] => State
- | req::Reqs' => FIFO_req req (FIFO_trace Reqs' State)
+ | [::] => (mkFIFO [::] 0)
+ | req::Reqs' => FIFO_req req (FIFO_trace Reqs')
end.
- Lemma FIFO_trace_time_monotone Reqs State:
- State.(Time) <= (FIFO_trace Reqs State).(Time).
- Proof.
+ Lemma FIFO_trace_time_monotone req Reqs:
+ (FIFO_trace Reqs).(Time) < (FIFO_trace (req::Reqs)).(Time).
+ Proof.
+ simpl. destruct FIFO_wait. simpl.
+ apply proj1 in a as H.
+ apply ltn_trans with (m := 0) in H.
+ by move : H => /nat_ltmaxn_l_add H.
+ auto.
+ Qed.
+
+ Lemma FIFO_trace_time_ok Reqs:
+ forall cmd, cmd \in (FIFO_trace Reqs).(Cmds) -> cmd.(CDate) <= (FIFO_trace Reqs).(Time).
+ Proof.
+ intros.
induction Reqs.
- auto.
- {
- simpl. destruct FIFO_wait. simpl.
- specialize (leq_addr x (Time (FIFO_trace Reqs State))) as H.
- specialize leq_trans with (n := Time (FIFO_trace Reqs State)) (m := Time State) (p := Time (FIFO_trace Reqs State) + x) as H1.
- apply H1 in IHReqs; auto.
- }
+ - auto.
+ - simpl. destruct FIFO_wait. simpl in *.
+ rewrite -> 3 in_cons in H.
+ move : H => /orP [/eqP H | /orP [ /eqP H | /orP [/eqP H | H]]]; subst; simpl.
+ - rewrite leq_add2l.
+ apply proj1 in a0 as H.
+ by apply ltn_trans with (m := 2) in H.
+ - rewrite leq_add2l.
+ apply proj1 in a0 as H.
+ by apply ltn_trans with (m := 1) in H.
+ - rewrite leq_add2l.
+ apply proj1 in a0 as H.
+ by apply ltn_trans with (m := 0) in H.
+ - apply IHReqs in H.
+ by apply nat_le_lemaxn_add with (x := x) (o := (Date a)) in H.
+ Qed.
+
+ Lemma FIFO_trace_cmd_notin cmd Reqs:
+ is_true ((FIFO_trace Reqs).(Time) < cmd.(CDate)) -> is_true (cmd \notin (FIFO_trace Reqs).(Cmds)).
+ Proof.
+ intros.
+ specialize (FIFO_trace_time_ok Reqs cmd) as H1.
+ destruct (cmd \in Cmds (FIFO_trace Reqs)) eqn:Hin.
+ - apply H1 in Hin.
+ contradict Hin.
+ rewrite -> leqNgt.
+ by apply /negP /negPn.
+ - by apply isT.
Qed.
+ Lemma FIFO_trace_uniq req Reqs:
+ is_true (uniq (FIFO_trace Reqs).(Cmds)) -> is_true (uniq (FIFO_trace (req::Reqs)).(Cmds)).
+ intros.
+ simpl.
+ apply /andP; split.
+ - rewrite in_cons negb_or. apply /andP. split.
+ - apply Command_ne_CMD_ACT.
+ - rewrite in_cons negb_or. apply /andP. split.
+ - apply Command_ne_CMD_PRE.
+ - apply FIFO_trace_cmd_notin.
+ by apply nat_ltmaxn_l_add.
+ apply /andP; split.
+ - rewrite in_cons negb_or. apply /andP. split.
+ - apply Command_ne_ACT_PRE.
+ - apply FIFO_trace_cmd_notin.
+ by apply nat_ltmaxn_l_add.
+ apply /andP; split.
+ - apply FIFO_trace_cmd_notin.
+ by apply nat_ltmaxn_l_add.
+ - auto.
+ Qed.
+
+ Lemma FIFO_trace_T_RC_ok Reqs:
+ forall a b, a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
+ ACT_to_ACT a b -> Same_Bank a b -> Before a b ->
+ Apart a b T_RC_NAT.
+ Proof.
+ set T := (FIFO_trace (Reqs)).(Time).
+ induction Reqs as [| req Reqs'].
+ - auto.
+ - intros a b Ia Ib AtA SB aBb.
+ simpl in *.
+ move : Ib => /orP [ /eqP Cmdb | /orP [ /eqP Cmdb | /orP [ /eqP Cmdb | Ib]] ];
+ move : Ia => /orP [ /eqP Cmda | /orP [ /eqP Cmda | /orP [ /eqP Cmda | Ia]] ].
+ - contradict AtA. subst a.
+ unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
+ by destruct (Kind req).
+ - contradict AtA. subst b.
+ unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
+ destruct (Kind req); apply /negP; rewrite negb_and; apply /orP; by right.
+ - contradict AtA. subst a.
+ by unfold ACT_to_ACT, isACT.
+ - contradict AtA. subst b.
+ unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
+ destruct (Kind req); apply /negP; rewrite negb_and; apply /orP; by right.
+ - contradict AtA. subst a.
+ unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
+ by destruct (Kind req).
+ - contradict aBb. subst a b.
+ unfold Before. simpl. apply /negP. by rewrite ltnn.
+ - contradict AtA. subst a.
+ unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
+ by destruct (Kind req).
+ - admit.
+ - contradict AtA. subst b.
+ unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
+ destruct (Kind req); apply /negP; rewrite negb_and; apply /orP; by right.
+ - contradict AtA. subst b.
+ unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
+ destruct (Kind req); apply /negP; rewrite negb_and; apply /orP; by right.
+ - contradict AtA. subst a.
+ unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
+ by destruct (Kind req).
+ - contradict AtA. subst b.
+ unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
+ destruct (Kind req); apply /negP; rewrite negb_and; apply /orP; by right.
+ - contradict AtA. subst a.
+ unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
+ by destruct (Kind req).
+ - admit.
+ - contradict AtA. subst a.
+ unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
+ by destruct (Kind req).
+ - by apply (IHReqs' a b) in Ia.
+ Admitted.
+
Program Definition FIFO_arbitrate :=
- let State := FIFO_trace Requests (mkFIFO [::] 0) in
- mkTrace State.(Cmds) State.(Time) _ _ _.
- Admit Obligations.
+ let State := FIFO_trace Requests in
+ mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests) (FIFO_trace_T_RC_ok Requests).
+ Next Obligation.
+ induction Requests; auto.
+ by apply (FIFO_trace_uniq a) in IHl.
+ Qed.
Program Instance FIFO_arbiter : Arbiter_t :=
mkArbiter Input FIFO_arbitrate _.
@@ -56,18 +175,22 @@ Section Test.
Program Instance BANK_CFG : Bank_configuration :=
{
BANKS := 1;
- T_RC := 2;
+ T_RC := 3
+ }.
+
+ Program Instance FIFO_CFG : FIFO_configuration :=
+ {
+ FIFO_wait := 4
}.
Program Definition Req1 := mkReq 3 RD 0.
Program Definition Req2 := mkReq 4 RD 0.
- Program Instance Input : Requests_t := mkReqs [:: Req1; Req2] _ _ _.
+ Program Instance Input : Requests_t := mkReqs [:: Req2; Req1] _ _ _.
Admit Obligations.
- Program Instance My_arbiter : Arbiter_t :=
- mkArbiter Input FIFO_arbitrate _.
- Admit Obligations.
+ Definition test (A : Arbiter_t) :=
+ Arbitrate.(Commands).
- Compute Arbitrate.(Commands).
+ Compute test FIFO_arbiter.
End Test.
diff --git a/coq/Requests.v b/coq/Requests.v
index 9762b705617d03077a8537fb72344af51588c44f..c0d7be89e9f9bee7a8ba9aac19cf7436ce93213a 100644
--- a/coq/Requests.v
+++ b/coq/Requests.v
@@ -54,7 +54,7 @@ Section Requests.
}
apply ReflectF. unfold Request_eqdef, not in *.
intro BUG.
- apply negbT in H; rewrite negb_and in H.
+ apply negbT in H. rewrite negb_and in H.
destruct x, y.
rewrite negb_and in H.
move: H => /orP [H | /eqP B].
@@ -71,11 +71,11 @@ Section Requests.
Local Fixpoint sorted_ (Reqs : seq Request_t) a :=
match Reqs with
| [::] => true
- | b::Reqs' => (a.(Date) <= b.(Date)) &&
+ | b::Reqs' => (a.(Date) >= b.(Date)) &&
sorted_ Reqs' b
end.
- Local Definition sorted (Reqs : seq Request_t) :=
+ Definition Reqs_sorted_ok (Reqs : seq Request_t) :=
match Reqs with
| [::] => true
| a::Reqs' => sorted_ Reqs' a
@@ -89,7 +89,7 @@ Section Requests.
Reqs_uniq : uniq Requests;
(* Requests are sorted by date. *)
- Reqs_sorted : sorted Requests;
+ Reqs_sorted : Reqs_sorted_ok Requests;
(* A requestor may only issue a single request to a bank at a time *)
Reqs_issue : forall a b, a \in Requests -> b \in Requests -> a != b ->
diff --git a/coq/Trace.v b/coq/Trace.v
index e4fe177994588f218c445f81b3f3761104074412..e6d4feef6db0622e250be9243a3fcb9fbbc026c6 100644
--- a/coq/Trace.v
+++ b/coq/Trace.v
@@ -1,5 +1,5 @@
Set Warnings "-notation-overridden,-parsing".
-From mathcomp Require Import ssreflect ssrnat ssrbool seq eqtype.
+From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
From sdram Require Export Commands Bank.
Section Trace.
diff --git a/coq/Util.v b/coq/Util.v
index e0eba38b23bd33345c4db11795b85bc25b196968..cc94c5a5366da7ae122b93f00e33a9477a982f8e 100644
--- a/coq/Util.v
+++ b/coq/Util.v
@@ -1,8 +1,46 @@
Set Warnings "-notation-overridden,-parsing".
-From mathcomp Require Import ssreflect ssrnat ssrbool seq eqtype.
+From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
+
+Lemma nat_ltnn_add n: forall x, 0 < x -> is_true (n < n + x).
+Proof.
+ intros.
+ induction n.
+ - apply /ltP. apply PeanoNat.Nat.lt_lt_add_l. by apply /ltP.
+ - auto.
+Qed.
+
+Lemma nat_ltmaxn_l_add a b: forall x, 0 < x -> is_true (a < (maxn a b) + x).
+Proof.
+ intros.
+ unfold maxn.
+ destruct (a < b) eqn:Hlt.
+ - by apply /ltn_addr.
+ - by move : H => /nat_ltnn_add H.
+Qed.
+
+Lemma nat_lt_ltmaxn_add a b c x: 0 < x -> is_true (maxn a b + x < c) -> is_true (a < c).
+Proof.
+ unfold maxn.
+ intros Hz H.
+ destruct (a < b) eqn:Hlt.
+ - apply (ltn_addr x) in Hlt.
+ by apply (ltn_trans (m := a) (n := b+x)) in H.
+ - move : Hz => /(nat_ltnn_add a x) Hz.
+ by apply (ltn_trans (m := a) (n := a+x)) in H.
+Qed.
+
+Lemma nat_le_lemaxn_add n m o: forall x, (n <= m) -> (n <= (maxn m o) + x).
+Proof.
+ intros.
+ unfold maxn.
+ destruct (m < o) eqn:Hlt.
+ - move : H => /leP /(PeanoNat.Nat.le_trans n m o) H.
+ by move : Hlt => /ltP /PeanoNat.Nat.lt_le_incl /H /(Plus.le_plus_trans n o x) /leP.
+ - by move : H => /leP /(Plus.le_plus_trans n m x) /leP.
+Qed.
Lemma all_filter [T : eqType] a (p : pred T) S:
- all a S -> all a [seq x <- S | p x].
+ all a S -> all a [seq x <- S | p x].
Proof.
intros.
induction S.