correct T_RC parameter for FIFO, some more proofs.

coq/Bank.v

 Set Warnings "-notation-overridden,-parsing".
-From mathcomp Require Export ssreflect ssrnat ssrbool seq.
+From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
 
 
-Definition Bank_number_t := {B : nat | B <> 0}.
-Definition Timing_parameter_t := {T : nat | T <> 0}.
-
 Class Bank_configuration :=
 {
-  BANKS  : Bank_number_t;
+  BANKS  : nat;
+
+  T_RC   : nat;    (* ACT to ACT delay intra-bank *)
 
-  T_RC   : Timing_parameter_t    (* ACT to ACT delay intra-bank *)
+  BANKS_pos : BANKS != 0;
+  T_RC_pos  : T_RC != 0
 }.
 
 Section Banks.
   Context {BANK_CFG : Bank_configuration}.
 
-  Definition BANKS_NAT := proj1_sig BANKS.
-  Definition T_RC_NAT := proj1_sig T_RC.
-
-  Definition Bank_t := { a : nat | a < BANKS_NAT }.
+  Definition Bank_t := { a : nat | a < BANKS }.
 
   Program Definition Nat_to_bank a : Bank_t :=
-    match a < BANKS_NAT with
+    match a < BANKS with
     | true  => (exist _ a _)
-    | false => (exist _ (BANKS_NAT - 1) _)
+    | false => (exist _ (BANKS - 1) _)
     end.
   Next Obligation.
-    unfold BANKS_NAT in *.
-    destruct BANKS. simpl in *.      
-    apply PeanoNat.Nat.lt_pred_l in n as H. move : H => /ltP H. by rewrite subn1.
+    rewrite subn1 ltn_predL lt0n. 
+    by specialize BANKS_pos.
   Qed.
 
   Definition Bank_to_nat (a : Bank_t) : nat :=
     proj1_sig a.
 
-  Notation "'#B' b" := (Nat_to_bank b) (only parsing, at level 0).
-  Notation "'#B' b" := ((exist _ b  _) Bank_t) (only printing, at level 0).
-
   Definition Banks_t := seq Bank_t.
 
   Definition All_banks : Banks_t := 
-    map Nat_to_bank (iota 0 BANKS_NAT).
+    map Nat_to_bank (iota 0 BANKS).
 End Banks.
 

coq/Commands.v

@@ -71,6 +71,9 @@ Section Commands.
       | WR => CWR
     end.
 
+  Definition isACT (cmd : Command_t) :=
+    cmd.(CKind) == ACT.
+
   Definition PRE_of_req req t :=
     mkCmd t PRE req.
 
@@ -80,6 +83,17 @@ Section Commands.
   Definition Cmd_of_req req t :=
     mkCmd t (Kind_of_req req) req.
 
+  Lemma Command_nisACT_PRE req t: ~ isACT (PRE_of_req req t).
+  Proof.
+    by unfold isACT, PRE_of_req.
+  Qed.
+
+  Lemma Command_nisACT_CMD req t: ~ isACT (Cmd_of_req req t).
+  Proof.
+    unfold isACT, Cmd_of_req, Kind_of_req.
+    by destruct (Kind req).
+  Qed.
+
   Lemma Command_neq_ACT_PRE reqa ta reqb tb: 
     (ACT_of_req reqa ta) != (PRE_of_req reqb tb).
   Proof.

coq/FIFO.v

@@ -7,8 +7,12 @@ Section FIFO.
 
   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 *)}
+    FIFO_wait : nat;
+
+    (* have to issue at least 3 commands *)
+    FIFO_cmds : 3 < FIFO_wait;
+    (* have to respect T_RC *)
+    FIFO_T_RC : T_RC < FIFO_wait;
   }.
 
   Context {FIFO_CFG : FIFO_configuration }.
@@ -19,8 +23,7 @@ Section FIFO.
     Time   : nat;
   }.
 
-
-  Local Program Definition FIFO_req req State : FIFO_state_t :=
+  Local Definition FIFO_req req State : FIFO_state_t :=
     let time := maxn State.(Time) req.(Date) in
     let PRE_date := time + 1 in
     let ACT_date := time + 2 in
@@ -40,33 +43,39 @@ Section FIFO.
   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.
+    simpl.
+    specialize FIFO_cmds as H.
     apply ltn_trans with (m := 0) in H.
-    by move : H  => /nat_ltmaxn_l_add H.
-    auto.
+    - by move : H  => /nat_ltmaxn_l_add H.
+    - auto.
+  Qed.
+
+  Lemma FIFO_trace_dist req Reqs:
+    (FIFO_trace Reqs).(Time) + FIFO_wait <= (FIFO_trace (req::Reqs)).(Time).
+  Proof.
+    simpl.
+    apply nat_le_add_lemaxn_add.
+    apply leqnn.
   Qed.
 
   Lemma FIFO_trace_time_ok Reqs: 
     forall cmd, cmd \in (FIFO_trace Reqs).(Cmds) -> cmd.(CDate) <= (FIFO_trace Reqs).(Time).
   Proof.
     intros.
+    specialize FIFO_cmds as Hc.
     induction Reqs.
       - auto.
-      - simpl. destruct FIFO_wait. simpl in *.
+      - 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.
+          by apply ltn_trans with (m := 2) in Hc.
         - rewrite leq_add2l.
-          apply proj1 in a0 as H.
-          by apply ltn_trans with (m := 1) in H.
+          by apply ltn_trans with (m := 1) in Hc.
         - rewrite leq_add2l.
-          apply proj1 in a0 as H.
-          by apply ltn_trans with (m := 0) in H.
+          by apply ltn_trans with (m := 0) in Hc.
         - apply IHReqs in H.
-          by apply nat_le_lemaxn_add with (x := x) (o := (Date a)) in H.
+          by apply nat_le_lemaxn_add with (x := FIFO_wait) (o := (Date a)) in H.
   Qed.
 
   Lemma FIFO_trace_cmd_notin cmd Reqs:
@@ -84,6 +93,7 @@ Section FIFO.
 
   Lemma FIFO_trace_uniq req Reqs:
     is_true (uniq (FIFO_trace Reqs).(Cmds)) -> is_true (uniq (FIFO_trace (req::Reqs)).(Cmds)).
+  Proof.
   intros.
     simpl.
     apply /andP; split.
@@ -107,9 +117,8 @@ Section FIFO.
   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.
+                    Apart a b T_RC.
   Proof.
-    set T := (FIFO_trace (Reqs)).(Time).
     induction Reqs as [| req Reqs'].
       - auto.
       - intros a b Ia Ib AtA SB aBb.
@@ -151,7 +160,15 @@ Section FIFO.
         - contradict AtA. subst a.
           unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
           by destruct (Kind req).
-        - admit.
+        - contradict aBb. subst a. 
+          apply /negP.
+          unfold Before, ACT_of_req. rewrite <- leqNgt. simpl. 
+          apply (FIFO_trace_time_ok Reqs') in Ib.
+          apply leq_trans with (p := maxn (Time (FIFO_trace Reqs')) (Date req)) in Ib.
+          -  apply leq_add with (m2 := 0) (n2 := 2) in Ib. 
+            - by rewrite addn0 in Ib.
+            - by apply leq0n.
+          apply leq_maxl. 
         - contradict AtA. subst a.
           unfold ACT_to_ACT, isACT, Cmd_of_req, Kind_of_req. simpl.
           by destruct (Kind req).
@@ -162,11 +179,12 @@ Section FIFO.
     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.
+    induction Requests.
+    - auto. 
+    - by apply (FIFO_trace_uniq a) in IHl.
   Qed.
 
-  Program Lemma FIFO_arbiter_handled req:
+  Lemma FIFO_arbiter_handled req:
     req \in Requests -> exists cmd : Command_t, cmd \in FIFO_arbitrate.(Commands) ->
                     Match req cmd.
   Proof.
@@ -229,7 +247,7 @@ Section Test.
         - by contradict Ha.
   Qed.
 
-  Definition test (A := FIFO_arbiter) :=Arbitrate.(Commands).
+  Definition test (Input : Requests_t) (A := FIFO_arbiter) := Arbitrate.(Commands).
 
-  Compute test.
+  Compute test Input.
 End Test.

coq/Requests.v

@@ -20,8 +20,8 @@ Section Requests.
   Proof.
     unfold Equality.axiom. intros.
     destruct (Request_kind_eqdef x y) eqn:H; unfold Request_kind_eqdef in *.
-      apply ReflectT. destruct x, y; inversion H; auto.
-      apply ReflectF; destruct x, y; inversion H; unfold not; intros; inversion H0.
+    - apply ReflectT. destruct x, y; inversion H; auto.
+    - apply ReflectF; destruct x, y; inversion H; unfold not; intros; inversion H0.
   Qed.
 
   Canonical Request_kind_eqMixin := EqMixin Request_kind_eqn.

coq/Trace.v

@@ -5,9 +5,6 @@ From sdram Require Export Commands Bank.
 Section Trace.
   Context {BANK_CFG : Bank_configuration}.
 
-  Definition isACT (cmd : Command_t) :=
-    cmd.(CKind) == ACT.
-
   Definition Same_Bank (a b : Command_t) :=
     a.(Request).(Bank) == b.(Request).(Bank).
 
@@ -34,7 +31,7 @@ Section Trace.
     (* Ensure that the time between two ACT commands respects T_RC *)
     Cmds_T_RC_ok : forall a b, a \in Commands -> b \in Commands ->
                     ACT_to_ACT a b -> Same_Bank a b -> Before a b ->
-                    Apart a b T_RC_NAT;
+                    Apart a b T_RC;
   }.
 
   Program Definition Trace_empty := mkTrace [::] 0 _ _ _.

coq/Util.v

@@ -29,14 +29,34 @@ Proof.
       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).
+Lemma nat_le_lemaxn n m o: (n <= m) -> (n <= (maxn m o)).
+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 /leP.
+  - auto.
+Qed.
+
+Lemma nat_le_add_lemaxn_add n m o: forall x, (n <= m + x) -> is_true (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.
+  - rewrite <- (ltn_add2r x m o) in Hlt.
+    apply ltnW in Hlt.
+    by apply leq_trans with (n := m + x) (m := n) (p := o + x) in Hlt.
+  - auto.
+Qed.
+
+Lemma nat_le_lemaxn_add n m o: forall x, (n <= m) -> (n <= (maxn m o) + x).
+Proof.
+  intros.
+  apply nat_le_lemaxn with (o := o) in H.
+  apply leq_trans with (p := (maxn m o) + x) in H.
+  - auto.
+  - apply leq_addr.
 Qed.
 
 Lemma all_filter [T : eqType] a (p : pred T) S: