FIFO.v

Set Warnings "-notation-overridden,-parsing".
From sdram Require Export  Arbiter Requests.

Section FIFO.
  Context {BANK_CFG : Bank_configuration}.
  Context {Input    : Requests_t}.

  Class FIFO_configuration :=
  {
    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 }.

  Local Record FIFO_state_t := mkFIFO
  {
    Cmds   : Commands_t;
    Time   : nat;
  }.

  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
    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 := CMD::ACT::PRE::State.(Cmds) in
          mkFIFO Cmds (time + FIFO_wait).

  Local Fixpoint FIFO_trace Reqs : FIFO_state_t :=
    match Reqs with
      | [::]       => (mkFIFO [::] 0)
      | req::Reqs' => FIFO_req req (FIFO_trace Reqs')
    end.

  Ltac decompose_FIFO_cmds H suffix :=
    let cmd := fresh suffix in
      move : H => /orP [ /eqP cmd | /orP [ /eqP cmd  | /orP [ /eqP cmd | H]] ].

  Lemma lt_FIFO_wait n: n < 3 -> n < FIFO_wait.
  Proof.
    specialize FIFO_cmds as H.
    intros.
    by apply ltn_trans with (m := n) in H.
  Qed.

  Lemma FIFO_trace_time_monotone req Reqs:
    (FIFO_trace Reqs).(Time) < (FIFO_trace (req::Reqs)).(Time).
  Proof.
    simpl.
    specialize FIFO_cmds as H.
    apply ltn_trans with (m := 0) in H.
    - 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 in *.
    rewrite -> 3 in_cons in H.
    decompose_FIFO_cmds H H; subst;
      try (rewrite leq_add2l; by apply lt_FIFO_wait).
    apply IHReqs in H.
    by apply nat_le_lemaxn_add with (x := FIFO_wait) (o := a.(Date)) 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.
    destruct (cmd \in Cmds (FIFO_trace Reqs)) eqn:Hin;
      try by apply isT.
    apply (FIFO_trace_time_ok Reqs cmd) in Hin.
    contradict Hin. rewrite -> leqNgt. by apply /negP /negPn.
  Qed.

  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.
    - rewrite in_cons negb_or. apply /andP. split.
      - apply Command_neq_CMD_ACT.
      - rewrite in_cons negb_or. apply /andP. split.
        - apply Command_neq_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_neq_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.
  Proof.
    induction Reqs as [| req Reqs']; auto.
    intros a b Ia Ib AtA SB aBb.
    decompose_FIFO_cmds Ib Cmdb; decompose_FIFO_cmds Ia Cmda;
      try contradict_AtoA AtA req.
    - contradict aBb. subst. unfold Before. apply /negP. by rewrite ltnn.
    - destruct Reqs'.
      - by contradict Ia.
      - decompose_FIFO_cmds Ia Cmda;
          try contradict_AtoA AtA req; try contradict_AtoA AtA r;
          subst; unfold Apart, ACT_of_req; simpl.
        - set T := maxn (FIFO_trace Reqs').(Time) r.(Date).
          unfold maxn. simpl.
          destruct (T + FIFO_wait < req.(Date)) eqn:Hlt.
          1  : rewrite <- (ltn_add2r 2) in Hlt.
          1  : apply ltn_trans with (n := T + FIFO_wait + 2); auto.
          1,2: rewrite addnCAC [T + FIFO_wait + 2]addnCAC.
          1,2: rewrite [2 + _]addnC.
          1,2: rewrite ltn_add2r ltn_add2r.
          1,2: by specialize FIFO_T_RC.
         - set T := maxn (FIFO_trace (r :: Reqs')).(Time) req.(Date).
          set Tf := (FIFO_trace Reqs').(Time) + FIFO_wait.
          specialize (FIFO_trace_dist r Reqs') as Hdist.
          apply leq_trans with (p := T) in Hdist.
          - rewrite <- (leq_add2r 2) in Hdist.
            rewrite addnS in Hdist.
            apply FIFO_trace_time_ok in Ia as H.
            rewrite <- (leq_add2r T_RC) in H.
            apply leq_ltn_trans with (p := Tf) in H.
            - apply ltn_trans with (p := Tf + 1) in H.
              - by apply ltn_trans with (p := T + 2) in H.
              - rewrite <- addn1. by rewrite leqnn.
            - rewrite ltn_add2l. by specialize FIFO_T_RC.
          - unfold T. by apply leq_maxl.
    - contradict aBb. subst a.
      apply /negP.
      unfold Before, ACT_of_req. rewrite <- leqNgt. apply nat_le_lemaxn_add.
      by apply (FIFO_trace_time_ok Reqs') in Ib.
    - by apply (IHReqs' a b) in Ia.
  Qed.

  Program Definition FIFO_arbitrate :=
    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.

  Lemma FIFO_arbiter_handled req:
    req \in Requests -> exists cmd : Command_t, cmd \in FIFO_arbitrate.(Commands) ->
                    Match req cmd.
  Proof.
    intros.
    exists (Cmd_of_req req 5).
    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.
  Qed.

  Instance FIFO_arbiter : Arbiter_t := 
    mkArbiter Input FIFO_arbitrate FIFO_arbiter_handled.
End FIFO.

Section Test.
  Program Instance BANK_CFG : Bank_configuration :=
  {
    BANKS := 1;
    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 [:: Req2; Req1] _ _ _.
  Next Obligation.
    rewrite in_cons in H.
    rewrite in_cons in H0.
    move : H => /orP [ /eqP reqa | Ha]; move : H0 => /orP [ /eqP reqb | Hb].
      - contradict H1. apply /negP /negPn. by subst. 
      - rewrite in_cons in Hb.
        move : Hb => /orP [ /eqP regb | Hb].
        - contradict H1. subst. by simpl.
        - by contradict Hb.
      - rewrite in_cons in Ha.
        move : Ha => /orP [ /eqP rega | Ha].
        - contradict H1. subst. by simpl.
        - by contradict Ha.
      - rewrite in_cons in Ha. 
        rewrite in_cons in Hb.
        move : Ha => /orP [ /eqP rega | Ha];  move : Hb => /orP [ /eqP regb | Hb].
        - contradict H1. apply /negP /negPn. by subst.  
        - by contradict Hb.
        - by contradict Ha.
        - by contradict Ha.
  Qed.

  Definition test (Input : Requests_t) (A := FIFO_arbiter) := Arbitrate.(Commands).

  Compute test Input.
End Test.