fix FIFO arbiter, start proofs

coq/Arbiter.v

 Set Warnings "-notation-overridden,-parsing".
-From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
 From sdram Require Export Trace.
 
 Section Arbiter.

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.

coq/FIFO.v

 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.

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 ->

coq/Trace.v

 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.

coq/Util.v

 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.