FIFO.v

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

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

  Definition FIFO_PRE_date := 1.
  Definition FIFO_ACT_date := FIFO_PRE_date + T_RP + 1.
  Definition FIFO_CMD_date := FIFO_ACT_date + T_RCD + 1.

  Class FIFO_configuration :=
  {
    FIFO_wait : nat;

    (* have to issue at least 3 commands *)
    (* have to respect T_RC, T_RAS, T_RP *)
    FIFO_T_RC   : T_RC < FIFO_wait;
    FIFO_T_RAS  : T_RAS + (1 + T_RP) < FIFO_wait;

    FIFO_T_PRE : FIFO_PRE_date <= FIFO_wait;
    FIFO_T_ACT : FIFO_ACT_date <= FIFO_wait;
    FIFO_T_CMD : FIFO_CMD_date <= FIFO_wait;
  }.

  Context {FIFO_CFG : FIFO_configuration }.

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

  Local Definition FIFO_next_time req State :=
    maxn State.(Time) req.(Date).

  Local Definition FIFO_req req State : FIFO_state_t :=
    let time := FIFO_next_time req State in
    let PRE_date := time + FIFO_PRE_date in
    let ACT_date := time + FIFO_ACT_date in
    let CMD_date := time + FIFO_CMD_date 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.

  Local Fixpoint FIFO_Req_before (req' req : Request_t) Reqs :=
    match Reqs with
      | [::]     => false
      | x::Reqs' => if req == x then true
                    else if req' == x then false
                    else FIFO_Req_before req' req Reqs'
    end.

  Local Fixpoint FIFO_Reqs_before (req : Request_t) Reqs :=
    if req \notin Reqs then Reqs
    else
      match Reqs with
        | [::]        => [::]
        | req'::Reqs' => if (req' == req) then Reqs'
                         else FIFO_Reqs_before req Reqs'
      end.

  Local Definition FIFO_trace_base_date req Reqs :=
    FIFO_next_time req (FIFO_trace (FIFO_Reqs_before req Reqs)).

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

  Lemma FIFO_Req_before_in o req' req Reqs:
    uniq (o::Reqs) -> req \in Reqs -> req' \in Reqs ->
      (FIFO_Req_before req' req (o::Reqs)) = (FIFO_Req_before req' req Reqs).
  Proof.
    intros Hu Ir Ir'.
    decompose_Reqs_uniq Hu Nio.
    simpl. destruct (req == o) eqn:Heq, (req' == o) eqn:Heq';
      move : Heq Heq' => /eqP Heq /eqP Heq'; subst; auto;
    contradict Nio; by (rewrite Ir + rewrite Ir').
  Qed.

  Lemma FIFO_Reqs_before_head req Reqs:
    FIFO_Reqs_before req (req::Reqs) = Reqs.
  Proof.
    simpl. by rewrite eq_refl mem_head.
  Qed.

  Lemma FIFO_trace_base_date_head req Reqs:
    req \notin Reqs ->
    FIFO_trace_base_date req (req::Reqs) = FIFO_next_time req (FIFO_trace Reqs).
  Proof.
    intros Ni.
    by rewrite /FIFO_trace_base_date FIFO_Reqs_before_head.
  Qed.

  Lemma FIFO_Reqs_before_in req' req Reqs:
    req \notin Reqs -> req' \in Reqs ->
    FIFO_Reqs_before req' (req::Reqs) = FIFO_Reqs_before req' Reqs.
  Proof.
    intros Ni Ir.
    simpl. rewrite in_cons Ir Bool.orb_true_r. simpl.
    destruct (req == req') eqn:Heq;
      move : Heq => /eqP Heq; auto.
    contradict Ni. subst. by rewrite Ir.
  Qed.

  Lemma FIFO_trace_base_date_in req' req Reqs:
    req \notin Reqs -> req' \in Reqs ->
    FIFO_trace_base_date req' (req::Reqs) = FIFO_trace_base_date req' Reqs.
  Proof.
    intros Ni Ir'.
    by rewrite /FIFO_trace_base_date FIFO_Reqs_before_in.
  Qed.

  Lemma FIFO_trace_Req_Before_date x y req Reqs:
    Reqs_sorted_ok Reqs -> uniq Reqs -> req \in Reqs -> x < y + FIFO_wait ->
      req.(Date) + x < (FIFO_trace Reqs).(Time) + y.
  Proof.
    induction Reqs; auto.
    intros Hs Hu Ir Hltw.
    simpl. unfold FIFO_next_time.
    decompose_Reqs_in Ir Heq; subst; auto.
    - unfold maxn.
      destruct ((FIFO_trace Reqs).(Time) < a.(Date)) eqn:Hlt.
      - by rewrite addnCAC addnC ltn_add2r.
      - move : Hlt => /ltP /ltP Hlt. rewrite <- leqNgt in Hlt.
        rewrite <- (leq_add2l x) in Hlt.
        apply leq_ltn_trans with (p := (FIFO_trace Reqs).(Time) + FIFO_wait + y) in Hlt.
        - by rewrite addnC.
        - by rewrite addnCAC ltn_add2r.
    - apply Reqs_sorted_cons in Hs.
      decompose_Reqs_uniq Hu Nia.
      rewrite addnACl [y + _]addnC nat_maxn_add [FIFO_wait + _]addnC.
      apply nat_le_lemaxn_add.
      by apply IHReqs.
  Qed.

  Lemma FIFO_trace_Req_Before_date_offs x y req req' Reqs:
    Reqs_sorted_ok Reqs -> uniq Reqs -> req \in Reqs -> req' \in Reqs ->
      req != req' -> FIFO_Req_before req' req Reqs -> x < y + FIFO_wait ->
      req'.(Date) + x < (FIFO_trace (FIFO_Reqs_before req Reqs)).(Time) + y.
  Proof.
    induction Reqs; auto.
    intros Hs Hu Ir Ir' Hneq Rb Hltw.
    decompose_Reqs_in Ir Heq; decompose_Reqs_in Ir' Heq'; subst; auto.
    - contradict Hneq. by rewrite eq_refl.
    - rewrite FIFO_Reqs_before_head.
      apply Reqs_sorted_cons in Hs.
      decompose_Reqs_uniq Hu Nia.
      by apply (FIFO_trace_Req_Before_date x y req').
    - contradict Rb.
      move : Hneq => /negPf Hneq.
      simpl. by rewrite Hneq eq_refl.
    - apply Reqs_sorted_cons in Hs.
      rewrite FIFO_Req_before_in in Rb; auto.
      decompose_Reqs_uniq Hu Nia.
      rewrite FIFO_Reqs_before_in; auto.
  Qed.

  Lemma FIFO_Reqs_Before_Reqs_trace_offs x y req Reqs:
    Reqs_sorted_ok Reqs -> uniq Reqs -> req \in Reqs -> x < y + FIFO_wait ->
      (FIFO_trace (FIFO_Reqs_before req Reqs)).(Time) + x < (FIFO_trace Reqs).(Time) + y.
  Proof.
    induction Reqs; auto.
    intros Hs Hu Ir Hltw.
    decompose_Reqs_in Ir Heq; subst; auto.
    - rewrite FIFO_Reqs_before_head.
      simpl. rewrite /FIFO_next_time addnACl [y + _]addnC [FIFO_wait + _]addnC nat_maxn_add.
      apply nat_lt_add_lemaxn_add.
      by rewrite addnCAC addnC ltn_add2r addnC.
    - decompose_Reqs_uniq Hu Nia.
      apply Reqs_sorted_cons in Hs.
      rewrite FIFO_Reqs_before_in; auto.
      simpl. rewrite /FIFO_next_time addnACl [y + _]addnC addnC [FIFO_wait + _]addnC nat_maxn_add addnC.
      apply nat_le_lemaxn_add.
      by apply IHReqs.
  Qed.

  Lemma FIFO_Reqs_Before_trace_offs x y req' req Reqs:
    Reqs_sorted_ok Reqs -> uniq Reqs -> req \in Reqs -> req' \in Reqs -> req != req' ->
      FIFO_Req_before req' req Reqs -> x < y + FIFO_wait ->
        (FIFO_trace (FIFO_Reqs_before req' Reqs)).(Time) + x < (FIFO_trace (FIFO_Reqs_before req Reqs)).(Time) + y.
  Proof.
    induction Reqs; auto.
    intros Hs Hu Ir Ir' Hneq Rb Hltw.
    decompose_Reqs_in Ir Heq; decompose_Reqs_in Ir' Heq'; subst; auto.
    - contradict Hneq. by rewrite eq_refl.
    - decompose_Reqs_uniq Hu Nia.
      rewrite FIFO_Reqs_before_in; auto.
      rewrite FIFO_Reqs_before_head; auto.
      apply Reqs_sorted_cons in Hs.
      by apply FIFO_Reqs_Before_Reqs_trace_offs.
    - contradict Rb. simpl.
      destruct (req == a) eqn:Heq.
      - move : Heq => /eqP Heq. subst.
        decompose_Reqs_uniq Hu Nia.
        contradict Nia. by rewrite Ir.
      - by rewrite eq_refl.
    - apply Reqs_sorted_cons in Hs.
      rewrite FIFO_Req_before_in in Rb; auto.
      decompose_Reqs_uniq Hu Nia.
      rewrite -> 2 FIFO_Reqs_before_in; auto.
  Qed.

  Lemma FIFO_trace_base_date_dist x y req' req Reqs:
    Reqs_sorted_ok Reqs -> uniq Reqs -> req \in Reqs -> req' \in Reqs -> req != req' ->
      FIFO_Req_before req' req Reqs -> x < y + FIFO_wait ->
      ((FIFO_trace_base_date req' Reqs) + x) < (FIFO_trace_base_date req Reqs) + y.
  Proof.
    intros Hs Hu Ir Ir' Hneq Rb Hltw.
    rewrite /FIFO_trace_base_date /FIFO_next_time [_ + y]nat_maxn_add.
    apply nat_le_lemaxn.
    unfold maxn.
    destruct (Time (FIFO_trace (FIFO_Reqs_before req' Reqs)) < Date req').
    - by apply FIFO_trace_Req_Before_date_offs.
    - by apply FIFO_Reqs_Before_trace_offs.
  Qed.

  Lemma FIFO_trace_base_date_dist0 x req' req Reqs:
    Reqs_sorted_ok Reqs -> uniq Reqs -> req \in Reqs -> req' \in Reqs -> req != req' ->
      FIFO_Req_before req' req Reqs -> x < FIFO_wait ->
      ((FIFO_trace_base_date req' Reqs) + x) < (FIFO_trace_base_date req Reqs).
  Proof.
    intros Hs Hu Ir Ir' Hneq Rb Hltw.
    rewrite <- (addn0 (FIFO_trace_base_date req Reqs)).
    by apply FIFO_trace_base_date_dist.
  Qed.

  Lemma FIFO_cmd_req_in cmd Reqs:
    cmd \in (FIFO_trace Reqs).(Cmds) ->
      cmd.(Request) \in Reqs.
  Proof.
    induction Reqs; auto.
    intros Ic.
    simpl.
    rewrite in_cons. apply /orP.
    destruct (cmd.(Request) == a) eqn:Heqn.
    - by left.
    - right.
      simpl in Ic. decompose_FIFO_cmds Ic c; subst; simpl in Heqn.
      - 1,2,3: contradict Heqn; by rewrite eq_refl.
      - by apply IHReqs.
  Qed.

  Ltac FIFO_contradict_isCmd H :=
    contradict H;
    unfold isACT, isPRE, isCMD,
      ACT_of_req, PRE_of_req, Cmd_of_req, Kind_of_req;
    by (simpl + destruct (Kind _)).

  Lemma FIFO_ACT_at_Reqs_before cmd Reqs:
    uniq Reqs -> cmd \in (FIFO_trace Reqs).(Cmds) -> isACT cmd ->
      cmd.(CDate) = FIFO_trace_base_date cmd.(Request) Reqs + FIFO_ACT_date.
  Proof.
    induction Reqs;
      intros Hu Ic iA.
    - contradict Ic. by rewrite in_nil.
    - decompose_FIFO_cmds Ic c; subst.
      - FIFO_contradict_isCmd iA.
      - move : Hu => /andP [Nia Hu].
        fold FIFO_trace.
        by rewrite FIFO_trace_base_date_head.
      - FIFO_contradict_isCmd iA.
      - move : Hu => /andP [Nia Hu].
        rewrite FIFO_trace_base_date_in; auto.
        by apply FIFO_cmd_req_in.
  Qed.

  Lemma FIFO_PRE_at_Reqs_before cmd Reqs:
    uniq Reqs -> cmd \in (FIFO_trace Reqs).(Cmds) -> isPRE cmd ->
      cmd.(CDate) = FIFO_trace_base_date cmd.(Request) Reqs + FIFO_PRE_date.
  Proof.
    induction Reqs;
      intros Hu Ic iP.
    - contradict  Ic. by rewrite in_nil.
    - decompose_FIFO_cmds Ic c; subst.
      - FIFO_contradict_isCmd iP.
      - FIFO_contradict_isCmd iP.
      - move : Hu => /andP [Nia Hu].
        fold FIFO_trace.
        by rewrite FIFO_trace_base_date_head.
      - move : Hu => /andP [Nia Hu].
        rewrite FIFO_trace_base_date_in; auto.
       fold FIFO_trace in Ic. fold mem_seq in Ic. simpl in Ic.
       by apply FIFO_cmd_req_in.
  Qed.

  Lemma FIFO_CMD_at_Reqs_before cmd Reqs:
    uniq Reqs -> cmd \in (FIFO_trace Reqs).(Cmds) -> isCMD cmd ->
      cmd.(CDate) = FIFO_trace_base_date cmd.(Request) Reqs + FIFO_CMD_date.
  Proof.
    induction Reqs;
      intros Hu Ic iC.
    - contradict  Ic. by rewrite in_nil.
    - decompose_FIFO_cmds Ic c; subst.
      - move : Hu => /andP [Nia Hu].
        fold FIFO_trace.
        by rewrite FIFO_trace_base_date_head.
      - FIFO_contradict_isCmd iC.
      - FIFO_contradict_isCmd iC.
      - move : Hu => /andP [Nia Hu].
        rewrite FIFO_trace_base_date_in; auto.
       fold FIFO_trace in Ic. fold mem_seq in Ic. simpl in Ic.
       by apply FIFO_cmd_req_in.
  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 in *.
    rewrite -> 3 in_cons in H.
    specialize FIFO_T_PRE as Hpre.
    specialize FIFO_T_ACT as Hact.
    specialize FIFO_T_CMD as Hcmd.
    decompose_FIFO_cmds H H; subst; simpl;
      try by rewrite leq_add2l.
    apply IHReqs in H.
    by apply nat_le_lemaxn_add with (x := FIFO_wait) (o := a.(Date)) in H.
  Qed.

  Lemma FIFO_next_time_lt_cmd x req' c Reqs :
    x > 0 -> c \in (FIFO_trace Reqs).(Cmds) ->
      (CDate c < FIFO_next_time req' (FIFO_trace Reqs) + x).
  Proof.
    intros gt1 Ic.
    apply FIFO_trace_time_ok in Ic.
    apply leq_ltn_trans with (p := (FIFO_trace Reqs).(Time) + x) in Ic.
    - unfold FIFO_next_time.
      by apply nat_lt_add_lemaxn_add with (o := req'.(Date)) in Ic.
    - by apply nat_ltnn_add.
  Qed.

  Lemma FIFO_trace_head_in c req Reqs:
    uniq (req::Reqs) -> c.(Request) \in Reqs ->
    c \in Cmds (FIFO_trace (req :: Reqs)) ->
      c \in Cmds (FIFO_trace (Reqs)).
  Proof.
    intros Hu Ir Ic.
    simpl in Hu; move : Hu => /andP [Nia Hu].
    decompose_FIFO_cmds Ic cmd; subst.
    1,2,3: simpl in Ir; contradict Nia; by rewrite Ir.
    exact Ic.
  Qed.

  Lemma FIFO_Before_Req_before a b Reqs:
    uniq Reqs -> a \in (FIFO_trace Reqs).(Cmds) ->
      b \in (FIFO_trace Reqs).(Cmds) -> Before a b ->
        FIFO_Req_before a.(Request) b.(Request) Reqs.
  Proof.
    intros Hu Ia Ib aBb.
    apply FIFO_cmd_req_in in Ia as Ir'.
    apply FIFO_cmd_req_in in Ib as Ir.
    induction Reqs; auto.
    rewrite -> in_cons in Ir, Ir'.
    move : Ir => /orP [/eqP Heq | Ir]; move : Ir' => /orP [/eqP Heq' | Ir']; subst.
    - simpl. by rewrite eq_refl.
    - simpl. by rewrite eq_refl.
    - contradict aBb. unfold Before.
      simpl in Ia, Ib.
      simpl in Hu; move : Hu => /andP [Nia Hu].
      decompose_FIFO_cmds Ia cmda; decompose_FIFO_cmds Ib cmdb; subst;
      try (simpl in Ir; contradict Nia; by rewrite Ir).
      - rewrite cmda. simpl.
        apply FIFO_next_time_lt_cmd with (x := FIFO_CMD_date) (req' := a.(Request)) in Ib; auto.
        by apply /negP /ltP /PeanoNat.Nat.lt_asymm /ltP.
      - rewrite cmda. simpl.
        apply FIFO_next_time_lt_cmd with (x := FIFO_ACT_date) (req' := a.(Request)) in Ib; auto.
        by apply /negP /ltP /PeanoNat.Nat.lt_asymm /ltP.
      - rewrite cmda. simpl.
        apply FIFO_next_time_lt_cmd with (x := FIFO_PRE_date) (req' := a.(Request)) in Ib; auto.
        by apply /negP /ltP /PeanoNat.Nat.lt_asymm /ltP.
      - contradict Nia.
        apply /negP. rewrite Bool.negb_involutive.
        by apply FIFO_cmd_req_in.
    - simpl.
      destruct (Request b == a0) eqn:Heqb, (Request a == a0) eqn:Heqa; auto;
        move : Heqa Heqb => /eqP Heqa /eqP Heqb; subst.
      - simpl in Hu; move : Hu => /andP [Nia Hu].
        contradict Nia. by rewrite Ir'.
      - apply FIFO_trace_head_in in Ia; auto.
        apply FIFO_trace_head_in in Ib; auto.
        simpl in Hu; move : Hu => /andP [Nia Hu].
        apply IHReqs; auto.
  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:
    uniq (FIFO_trace Requests).(Cmds).
  Proof.
    induction Requests; auto.
    intros. simpl.
    apply /andP; split.
    - rewrite in_cons negb_or. apply /andP. split.
      - by apply Command_neq_CMD_ACT.
      - rewrite in_cons negb_or. apply /andP. split.
        - by 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.
        - by 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.
        - done.
  Qed.

  Lemma FIFO_trace_T_RC_ok:
    forall a b, a \in (FIFO_trace Requests).(Cmds) -> b \in (FIFO_trace Requests).(Cmds) ->
                    ACT_to_ACT a b -> Same_Bank a b -> Before a b ->
                    Apart a b T_RC.
  Proof.
    intros a b Ia Ib AtA SB aBb.
    destruct Input.
    move : AtA => /andP [iAa iAb].
    apply FIFO_ACT_at_Reqs_before in Ia as Da;
    apply FIFO_ACT_at_Reqs_before in Ib as Db; try exact.
    apply FIFO_Before_Req_before with (Reqs := Requests) in aBb as RB; auto.
    apply FIFO_cmd_req_in in Ia as Ir.
    apply FIFO_cmd_req_in in Ib as Ir'.
    rewrite /Apart Da Db addnACl addnC ltn_add2r addnC.
    destruct (Request b == Request a) eqn:Heq;
      move : Heq => /eqP Heq.
    - contradict aBb. rewrite -> Heq in *.
      by rewrite /Before Da Db ltnn.
    - move : Heq => /eqP Heq. specialize FIFO_T_RC.
      by apply FIFO_trace_base_date_dist0.
  Qed.

  Lemma FIFO_T_RP_neq:
    T_RP + FIFO_PRE_date < FIFO_ACT_date + FIFO_wait.
  Proof.
    rewrite /FIFO_ACT_date addnC addnCAC [_ + (FIFO_PRE_date + T_RP)]addnC.
    apply nat_ltnn_add. rewrite addn1. by apply ltn0Sn.
  Qed.

  Lemma FIFO_T_RP_eq:
    (T_RP + FIFO_PRE_date) < FIFO_ACT_date.
  Proof.
    rewrite /FIFO_ACT_date addnCAC ltn_add2r addnC addn1. by apply ltnSn.
  Qed.

  Lemma FIFO_trace_T_RP_ok:
    forall a b, a \in (FIFO_trace Requests).(Cmds) -> b \in (FIFO_trace Requests).(Cmds) ->
                    PRE_to_ACT a b -> Same_Bank a b -> Before a b ->
                    Apart a b T_RP.
  Proof.
    intros a b Ia Ib AtA SB aBb.
    destruct Input.
    move : AtA => /andP [iAa iAb].
    apply FIFO_PRE_at_Reqs_before in Ia as Da; auto.
    apply FIFO_ACT_at_Reqs_before in Ib as Db; auto.
    apply FIFO_Before_Req_before with (Reqs := Requests) in aBb as RB; auto.
    apply FIFO_cmd_req_in in Ia as Ir.
    apply FIFO_cmd_req_in in Ib as Ir'.
    rewrite /Apart Da Db addnCAC addnC.
    destruct (Request b == Request a) eqn:Heq;
      move : Heq => /eqP Heq.
    - rewrite Heq ltn_add2l. by apply FIFO_T_RP_eq.
    - move : Heq => /eqP Heq. specialize FIFO_T_RP_neq.
      by apply FIFO_trace_base_date_dist.
  Qed.

  Lemma FIFO_trace_T_RCD_eq:
    (T_RCD + FIFO_ACT_date) < FIFO_CMD_date.
  Proof.
    rewrite /FIFO_CMD_date addn1 addnC. by apply ltnSn.
  Qed.

  Lemma FIFO_trace_T_RCD_neq:
    (T_RCD + FIFO_ACT_date) < (FIFO_CMD_date + FIFO_wait).
  Proof.
    rewrite /FIFO_CMD_date addnC addnCAC. rewrite [(_+_) + (_+_)]addnC addn1.
    apply nat_ltnn_add. by apply ltn0Sn.
  Qed.

  Lemma FIFO_trace_T_RCD_ok:
    forall a b, a \in (FIFO_trace Requests).(Cmds)  -> b \in (FIFO_trace Requests).(Cmds)  ->
                ACT_to_CMD a b -> Same_Bank a b -> Before a b ->
                  Apart a b T_RCD.
  Proof.
    intros a b Ia Ib AtA SB aBb.
    destruct Input.
    move : AtA => /andP [iAa iAb].
    apply FIFO_ACT_at_Reqs_before in Ia as Da; auto.
    apply FIFO_CMD_at_Reqs_before in Ib as Db; auto.
    apply FIFO_Before_Req_before with (Reqs := Requests) in aBb as RB; auto.
    apply FIFO_cmd_req_in in Ia as Ir.
    apply FIFO_cmd_req_in in Ib as Ir'.
    rewrite /Apart Da Db addnCAC addnC.
    destruct (Request b == Request a) eqn:Heq;
      move : Heq => /eqP Heq.
    - rewrite Heq ltn_add2l. by apply FIFO_trace_T_RCD_eq.
    - move : Heq => /eqP Heq. specialize FIFO_trace_T_RCD_neq.
      by apply FIFO_trace_base_date_dist.
  Qed.

Ltac contradict_AtoP H req :=
  (contradict H; subst; unfold ACT_to_PRE, isACT, PRE_of_req, Cmd_of_req, Kind_of_req; simpl; destruct (Kind req));
  (done + apply /negP; rewrite negb_and; apply /orP; by right).

  Lemma FIFO_trace_T_RAS_eq:
    ~ FIFO_ACT_date < FIFO_PRE_date.
  Proof.
    apply /negP. rewrite <- leqNgt.
    rewrite /FIFO_ACT_date addnCAC addnC add1n. by apply leq_addr.
  Qed.

  Lemma FIFO_trace_T_RAS_neq:
    (T_RAS + FIFO_ACT_date) < (FIFO_PRE_date + FIFO_wait).
  Proof.
    rewrite /FIFO_ACT_date [FIFO_PRE_date + _]addnC addnACl addnC addnCAC addnC ltn_add2l.
    by apply FIFO_T_RAS.
  Qed.

  Lemma FIFO_trace_T_RAS_ok:
    forall a b, a \in (FIFO_trace Requests).(Cmds) -> b \in (FIFO_trace Requests).(Cmds) ->
                ACT_to_PRE a b -> Same_Bank a b -> Before a b ->
                Apart a b T_RAS.
  Proof.
    intros a b Ia Ib AtA SB aBb.
    destruct Input.
    move : AtA => /andP [iAa iAb].
    apply FIFO_ACT_at_Reqs_before in Ia as Da; auto.
    apply FIFO_PRE_at_Reqs_before in Ib as Db; auto.
    apply FIFO_Before_Req_before with (Reqs := Requests) in aBb as RB; auto.
    apply FIFO_cmd_req_in in Ia as Ir.
    apply FIFO_cmd_req_in in Ib as Ir'.
    rewrite /Apart Da Db addnCAC addnC.
    destruct (Request b == Request a) eqn:Heq;
      move : Heq => /eqP Heq.
    - contradict aBb. rewrite -> Heq in *.
      rewrite /Before Da Db ltn_add2l.
      by apply FIFO_trace_T_RAS_eq.
    - move : Heq => /eqP Heq. specialize FIFO_trace_T_RAS_neq.
      by apply FIFO_trace_base_date_dist.
  Qed.

  Lemma Between_cons req Reqs a b:
    a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
    Between ((FIFO_trace Reqs).(Cmds)) a b =
    Between (FIFO_trace (req :: Reqs)).(Cmds) a b.
  Proof.
  Admitted.

  Lemma FIFO_trace_Cmds_PRE_ok Reqs :
    forall a b, a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
                  PRE_to_PRE a b -> Same_Bank a b -> Before a b ->
                  exists c : Command_t, isACT c /\ Same_Bank a c /\ c \in Between (FIFO_trace Reqs).(Cmds) a b.
  Proof.
    intros a b a_cmds b_cmds ab_PRE ab_BANK a_not_b.
    evar (req_date : nat).
    evar (t : nat).
    evar (req_kind : Request_kind_t).
    set (req := mkReq req_date req_kind a.(Request).(Bank)).
    exists (ACT_of_req req t).
    split.
    - auto.
    - split.
      - by unfold ACT_of_req, Same_Bank.
      - induction Reqs.
          - auto.
          - simpl in a_cmds.
            move : a_cmds => /orP [ /eqP a_eq | /orP [ /eqP a_eq  | /orP [ /eqP a_eq | Ia]] ];
            move : b_cmds => /orP [ /eqP b_eq | /orP [ /eqP b_eq  | /orP [ /eqP b_eq | Ib]] ].
            - admit.
            - admit.
            - admit.
            - admit.
            - admit.
            - admit.
            - admit.
            - admit.
            - admit.
            - admit.
            - (*they are the same*) admit.
            - (*easy due to order*) admit.
            - admit.
            - admit.
            - (* interesting - induction on Reqs until find request of A until I find my ACT cmd (?)*) admit.
            - rewrite <- Between_cons. apply IHReqs in Ia. apply Ia. all : auto.
  Admitted.

  Definition FIFO_arbitrate :=
    let State := FIFO_trace Requests in
      mkTrace State.(Cmds) State.(Time) FIFO_trace_uniq (FIFO_trace_time_ok Requests)
        (FIFO_trace_Cmds_PRE_ok Requests) FIFO_trace_T_RC_ok FIFO_trace_T_RP_ok
        FIFO_trace_T_RCD_ok FIFO_trace_T_RAS_ok.

  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.
    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_trace_Req_handled Requests).
End FIFO.

Section Test.
  Program Instance BANK_CFG : Bank_configuration :=
  {
    BANKS := 1;
    T_RC  := 3;
    T_RP  := 7;
    T_RCD := 2;
    T_RAS := 4
  }.

  Program Instance FIFO_CFG : FIFO_configuration :=
  {
    FIFO_wait := 13
  }.

  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.