diff --git a/framework/DDR4/Arbiter.v b/framework/DDR4/Arbiter.v
deleted file mode 100644
index 0babd47e92bd60a36f250d413c7ebd885da68a8a..0000000000000000000000000000000000000000
--- a/framework/DDR4/Arbiter.v
+++ /dev/null
@@ -1,108 +0,0 @@
-Set Warnings "-notation-overridden,-parsing".
-Set Printing Projections.
-From sdram Require Export Trace.
-
-Section Arbiter.
-
-
-
- Context {REQESTOR_CFG : Requestor_configuration}.
- Context {ARBITER_CFG : Arbiter_configuration}.
- Context {BANK_CFG : Bank_configuration}.
-
- Class Arrival_function_t := mkArrivalFunction
- {
- Arrival_at : nat -> Requests_t;
-
- Arrival_date : forall ta x,
- (x \in (Arrival_at ta)) -> x.(Date) == ta;
-
- Arrival_uniq : forall t,
- uniq (Arrival_at t);
- }.
-
- Record Arbiter_state_t := mkArbiterState
- {
- Arbiter_Commands : Commands_t;
- Arbiter_Time : nat;
-
- (* This is implementation specific *)
- Implementation_State : State_t;
-
- (* Commented for now because can't solve the proof obligation with Default_arbitrate writen the way it is *)
- (* Arbiter_Commands_date :
- forall c,
- c \in Arbiter_Commands -> c.(CDate) <= Arbiter_Time *)
- }.
-
- Class Implementation_t := mkImplementation
- {
- Init : Requests_t -> State_t;
- Next : Requests_t -> State_t -> State_t * (Command_kind_t * Request_t);
- }.
-
- Class Arbiter_t {AF : Arrival_function_t} := mkArbiter
- {
- Arbitrate : nat -> Trace_t;
-
- (* All requests must handled *)
- Requests_handled :
- forall ta req, req \in (Arrival_at ta) ->
- exists tc, (CAS_of_req req tc) \in ((Arbitrate tc).(Commands));
-
- (* Time has to match *)
- Time_match :
- forall t, (Arbitrate t).(Time) == t
- }.
-
- Definition Default_arrival_at Input t :=
- [seq x <- Input | x.(Date) == t].
-
- Program Instance Default_arrival_function_t (R : Requests_t) `{uniq R} : Arrival_function_t :=
- mkArrivalFunction (Default_arrival_at R) _ _.
- Next Obligation.
- induction R.
- - contradict H. simpl. by rewrite in_nil.
- - simpl in H.
- rewrite cons_uniq in uniq0. move : uniq0 => /andP [_ Hu].
- destruct (a.(Date) == ta) eqn:Hd.
- - rewrite in_cons in H.
- move : H => /orP [/eqP H | H].
- - by subst.
- - by apply IHR in Hu.
- - by apply IHR in Hu.
- Qed.
- Next Obligation.
- unfold Default_arrival_at.
- by rewrite filter_uniq.
- Qed.
-
- Program Fixpoint Default_arbitrate {AF : Arrival_function_t} {IM : Implementation_t} t {struct t}: Arbiter_state_t :=
- let R := Arrival_at t in
- match t with
- | 0 => mkArbiterState [::] t (Init R)
- | S(t') => let old_state := Default_arbitrate t' in
- let (new_state,acmd) := Next R old_state.(Implementation_State) in
- let (ckind, creq) := acmd in
- let new_cmd := mkCmd t ckind creq in
- let cmd_list := (new_cmd :: old_state.(Arbiter_Commands)) in
- mkArbiterState cmd_list t new_state
- end.
-
- Lemma Default_arbitrate_time_match {AF: Arrival_function_t} {IM : Implementation_t} t:
- (Default_arbitrate t).(Arbiter_Time) == t.
- Proof.
- induction t.
- { done. }
- simpl; destruct (Next (Arrival_at t.+1) (Default_arbitrate t).(Implementation_State)); simpl.
- destruct p.
- simpl; apply /eqP; reflexivity.
- Qed.
-
- Lemma Default_arbitrate_time {AF: Arrival_function_t} {IM : Implementation_t} t:
- (Default_arbitrate t).(Arbiter_Time) = t.
- Proof.
- apply /eqP. apply Default_arbitrate_time_match.
- Qed.
-
-End Arbiter.
\ No newline at end of file
diff --git a/framework/DDR4/Bank.v b/framework/DDR4/Bank.v
deleted file mode 100644
index e9b52b7f68b551a04b4c861bf8ded6277975eebb..0000000000000000000000000000000000000000
--- a/framework/DDR4/Bank.v
+++ /dev/null
@@ -1,33 +0,0 @@
-Set Warnings "-notation-overridden,-parsing".
-Set Printing Projections.
-From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
-(* Require Export System. *)
-From DDR4 Require Export System.
-(* From DDR3 Require Export System. *)
-
-Section Banks.
-
- Definition Row_t := nat.
- Context {SYS_CFG : System_configuration}.
-
- Definition Bank_t :=
- { a : nat | a < BANKS }.
-
- Program Definition Nat_to_bank a : Bank_t :=
- match a < BANKS with
- | true => (exist _ a _)
- | false => (exist _ (BANKS - 1) _)
- end.
- Next Obligation.
- rewrite subn1 ltn_predL lt0n.
- by specialize BANKS_pos.
- Qed.
-
- Definition Bank_to_nat (a : Bank_t) : nat :=
- proj1_sig a.
-
- Definition Banks_t := seq Bank_t.
-
- Definition All_banks : Banks_t :=
- map Nat_to_bank (iota 0 BANKS).
-End Banks.
diff --git a/framework/DDR4/Commands.v b/framework/DDR4/Commands.v
deleted file mode 100644
index 6a0d4ef2e7d6fbff70dec873ad46c7fefd8314f5..0000000000000000000000000000000000000000
--- a/framework/DDR4/Commands.v
+++ /dev/null
@@ -1,135 +0,0 @@
-Set Warnings "-notation-overridden,-parsing".
-Set Printing Projections.
-From sdram Require Export Requests.
-
-Section Commands.
- Context {REQESTOR_CFG : Requestor_configuration}.
- Context {BANK_CFG : Bank_configuration}.
-
- Inductive Command_kind_t : Set :=
- ACT |
- PRE |
- PREA |
- CRD |
- CWR |
- REF |
- NOP.
-
- Local Definition Command_kind_eqdef (a b : Command_kind_t) :=
- match a, b with
- | ACT, ACT
- | PRE, PRE
- | PREA, PREA
- | CRD, CRD
- | CWR, CWR
- | REF, REF
- | NOP, NOP => true
- | _, _ => false
- end.
-
- Lemma Command_kind_eqn : Equality.axiom Command_kind_eqdef.
- Proof.
- unfold Equality.axiom. intros.
- destruct (Command_kind_eqdef x y) eqn:H; unfold Command_kind_eqdef in *.
- apply ReflectT. destruct x, y; inversion H; auto.
- apply ReflectF; destruct x, y; inversion H; unfold not; intros; inversion H0.
- Qed.
-
- Canonical Command_kind_eqMixin := EqMixin Command_kind_eqn.
- Canonical Command_kind_eqType := Eval hnf in EqType Command_kind_t Command_kind_eqMixin.
-
- Record Command_t := mkCmd
- {
- CDate : nat;
- CKind : Command_kind_t;
- Request : Request_t
- }.
-
- Record Arbiter_command_t := mkArbiterCmd
- {
- Arbiter_CKind : Command_kind_t;
- Arbiter_Request : Request_t
- }.
-
- Local Definition Command_eqdef (a b : Command_t) :=
- (a.(CDate) == b.(CDate)) &&
- (a.(Request) == b.(Request)) &&
- (a.(CKind) == b.(CKind)).
-
- Lemma Command_eqn : Equality.axiom Command_eqdef.
- Proof.
- unfold Equality.axiom. intros. destruct Command_eqdef eqn:H; unfold Command_eqdef in *.
- {
- apply ReflectT.
- move: H => /andP [/andP [/eqP CD /eqP R /eqP C]].
- destruct x,y. simpl in *. subst. auto.
- }
- apply ReflectF. unfold not in *. intro BUG.
- apply negbT in H; rewrite negb_and in H.
- destruct x, y.
- rewrite negb_and in H.
- move: H => /orP [H | /eqP CK].
- move: H => /orP [H | /eqP R].
- move: H => /eqP CD.
- by apply CD; inversion BUG.
- by apply R; inversion BUG.
- by apply CK; inversion BUG.
- Qed.
-
- Canonical Command_eqMixin := EqMixin Command_eqn.
- Canonical Command_eqType := Eval hnf in EqType Command_t Command_eqMixin.
-
- Definition Command_lt a b :=
- a.(CDate) > b.(CDate).
-
- Definition Kind_of_req req :=
- match req.(Kind) with
- | RD => CRD
- | WR => CWR
- end.
-
- Definition isACT (cmd : Command_t) :=
- cmd.(CKind) == ACT.
-
- Definition isPRE (cmd : Command_t) :=
- cmd.(CKind) == PRE.
-
- Definition isPRE_or_PREA (cmd : Command_t):=
- match cmd.(CKind) with
- | PRE => true
- | PREA => true
- | _ => false
- end.
-
- Definition isNOP cmd :=
- cmd.(CKind) == NOP.
-
- Definition isPREA (cmd : Command_t) :=
- cmd.(CKind) == PREA.
-
- Definition isCRD (cmd : Command_t) :=
- (cmd.(CKind) == CRD).
-
- Definition isCWR (cmd : Command_t) :=
- (cmd.(CKind) == CWR).
-
- Definition isCAS (cmd : Command_t) :=
- (cmd.(CKind) == CRD) || (cmd.(CKind) == CWR).
-
- Definition isREF (cmd : Command_t) :=
- (cmd.(CKind) == REF).
-
- Definition PRE_of_req req t :=
- mkCmd t PRE req.
-
- Definition ACT_of_req req t :=
- mkCmd t ACT req.
-
- Definition CAS_of_req req t :=
- mkCmd t (Kind_of_req req) req.
-
- Definition issueREF req t :=
- mkCmd t REF req.
-
- Definition Commands_t := seq Command_t.
-End Commands.
diff --git a/framework/DDR4/ExtractionFIFO.v b/framework/DDR4/ExtractionFIFO.v
deleted file mode 100644
index 4e03ace9a41022dc012879e06ccb0a6e337e28dd..0000000000000000000000000000000000000000
--- a/framework/DDR4/ExtractionFIFO.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Set Warnings "-notation-overridden,-parsing".
-From sdram Require Export FIFO.
-From Coq Require Extraction.
-Require Import Arith.
-Require Import ExtrHaskellNatNum.
-
-Extraction Language Haskell.
-
-Extract Inductive nat => "Prelude.Int" [ "0" "Prelude.succ" ]
- "(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
-
-Cd "haskell_gencode_fifo".
-Separate Extraction FIFO.
-Cd "..".
diff --git a/framework/DDR4/ExtractionTDM.v b/framework/DDR4/ExtractionTDM.v
deleted file mode 100644
index 307da70bcc0fba1767ccfb0d954cc2ea1964bf49..0000000000000000000000000000000000000000
--- a/framework/DDR4/ExtractionTDM.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Set Warnings "-notation-overridden,-parsing".
-From sdram Require Export TDM.
-From Coq Require Extraction.
-Require Import Arith.
-Require Import ExtrHaskellNatNum.
-
-Extraction Language Haskell.
-
-Extract Inductive nat => "Prelude.Int" [ "0" "Prelude.succ" ]
- "(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
-
-Cd "haskell_gencode_tdm".
-Separate Extraction TDM.
-Cd "..".
diff --git a/framework/DDR4/FIFO.v b/framework/DDR4/FIFO.v
deleted file mode 100644
index 7da65ecb34f94bea9fa8b591585f82b0ac33d1bb..0000000000000000000000000000000000000000
--- a/framework/DDR4/FIFO.v
+++ /dev/null
@@ -1,2374 +0,0 @@
-Set Warnings "-notation-overridden,-parsing".
-Set Printing Projections.
-
-From sdram Require Export Arbiter Requests.
-From mathcomp Require Export fintype div.
-Require Import Program.
-
-Section FIFO.
-
- Context {BANK_CFG : Bank_configuration}.
-
- Instance REQESTOR_CFG : Requestor_configuration :=
- {
- Requestor_t := unit_eqType
- }.
-
- Local Definition ACT_date := T_RP.-1.
- Local Definition CAS_date := ACT_date + T_RCD.
-
- Class FIFO_configuration :=
- {
- WAIT : nat;
-
- T_RP_GT_ONE : 1 < T_RP;
- T_RCD_GT_ONE : 1 < T_RCD;
- T_RTP_GT_ONE : 1 < T_RTP;
-
- WAIT_gt_one : 0 < WAIT.-1;
- WAIT_pos : 0 < WAIT;
- WAIT_ACT : ACT_date < WAIT;
- WAIT_CAS : CAS_date < WAIT;
- WAIT_END : CAS_date + T_RTP < WAIT;
-
- RRD_WAIT : T_RRD < WAIT;
- FAW_WAIT : T_FAW < WAIT + WAIT + WAIT;
- }.
-
- Context {FIFO_CFG : FIFO_configuration}.
- Context {AF : Arrival_function_t}.
-
- Definition Counter_t := ordinal WAIT.
-
- Variant FIFO_state_t :=
- | IDLE : Counter_t -> Requests_t -> FIFO_state_t
- | RUNNING : Counter_t -> Requests_t -> Request_t -> FIFO_state_t.
-
- Global Instance ARBITER_CFG : Arbiter_configuration :=
- {
- State_t := FIFO_state_t;
- }.
-
- Local Definition OCycle0 := Ordinal WAIT_pos.
- Local Definition OACT_date := Ordinal WAIT_ACT.
- Local Definition OCAS_date := Ordinal WAIT_CAS.
-
- (* Increment counter for cycle ofset (with wrap-arround). *)
- Definition Next_cycle (c : Counter_t) :=
- let nextc := c.+1 < WAIT in
- (if nextc as X return (nextc = X -> Counter_t) then
- fun (P : nextc = true) => Ordinal (P : nextc)
- else
- fun _ => OCycle0) Logic.eq_refl.
-
- Set Printing Coercions.
-
- Local Definition Enqueue (R P : Requests_t) :=
- P ++ R.
-
- Local Definition Dequeue r (P : Requests_t) :=
- rem r P.
-
- Local Definition Init_state R :=
- IDLE OCycle0 (Enqueue R [::]).
-
- Local Definition nullreq :=
- mkReq tt 0 RD 0 (Nat_to_bank 0) 0.
-
- Local Definition Next_state R (AS : FIFO_state_t) : (FIFO_state_t * (Command_kind_t * Request_t)) :=
- match AS return FIFO_state_t * (Command_kind_t * Request_t) with
- | IDLE c P =>
- let c' := Next_cycle c in
- let P' := Enqueue R P in
- match P with
- | [::] => (IDLE c' P', (NOP,nullreq))
- | r :: PP => (RUNNING OCycle0 (Enqueue R (Dequeue r P)) r, (PRE,r))
- end
- | RUNNING c P r =>
- let P' := Enqueue R P in
- let c' := Next_cycle c in
- if nat_of_ord c == OACT_date then (RUNNING c' P' r, (ACT,r))
- else if nat_of_ord c == OCAS_date then (RUNNING c' P' r, ((Kind_of_req r), r))
- else if nat_of_ord c == WAIT.-1 then
- match P with
- | [::] => (IDLE OCycle0 P', (NOP, nullreq))
- | r :: PP => (RUNNING OCycle0 (Enqueue R (Dequeue r P)) r, (PRE,r))
- end
- else (RUNNING c' P' r, (NOP,nullreq))
- end.
-
- Global Instance FIFO_arbiter_trace : Implementation_t :=
- mkImplementation Init_state Next_state.
-
- (* ------------------------------------------------------------------ *)
- (* --------------------- UTILITIES----------------------------------- *)
- (* ------------------------------------------------------------------ *)
-
- Definition FIFO_counter (AS : State_t) :=
- match AS with
- | IDLE c _ => nat_of_ord c
- | RUNNING c _ _ => nat_of_ord c
- end.
-
- Definition isRUNNING (AS : State_t) :=
- match AS with
- | IDLE _ __ => false
- | RUNNING _ _ _ => true
- end.
-
- Definition isIDLE (AS : State_t) :=
- match AS with
- | IDLE _ __ => true
- | RUNNING _ _ _ => false
- end.
-
- Definition Requestor_slot_start ta :=
- match (Default_arbitrate ta).(Implementation_State) with
- | IDLE c R => ta
- | RUNNING c R r => ta + (WAIT.-1 - c)
- end.
-
- Definition FIFO_pending (AS : State_t) :=
- match AS with
- | IDLE _ P => P
- | RUNNING _ P _ => P
- end.
-
- Definition FIFO_request (AS : State_t ) : option Request_t :=
- match AS with
- | IDLE _ _ => None
- | RUNNING _ _ r => Some r
- end.
-
- Ltac isCommand :=
- unfold isPRE, isACT, isCAS, PRE_of_req, ACT_of_req, CAS_of_req, Kind_of_req;
- match goal with
- | |- context G [?r.(Kind)] => destruct (r.(Kind)); discriminate
- | |- (_) => discriminate
- end.
-
- Ltac in_cons_cmd Hi Hp IHt :=
- rewrite in_cons in Hi; move: Hi => /orP [/eqP Hi | Hi];
- ( (apply IHt in Hi; (exact Hp || exact Hi)) || (contradict Hp; by rewrite Hi) ).
-
- Lemma isIDLE_notRunning ta:
- isIDLE (Default_arbitrate ta).(Implementation_State) -> isRUNNING (Default_arbitrate ta).(Implementation_State) == false.
- Proof.
- intros.
- rewrite /isRUNNING; rewrite /isIDLE in H; simpl in H.
- by destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- Qed.
-
- Lemma isIDLE_fromstate ta c0 r:
- (Default_arbitrate ta).(Implementation_State) = IDLE c0 r ->
- isIDLE (Default_arbitrate ta).(Implementation_State).
- Proof.
- rewrite /isIDLE.
- intros H; by rewrite H.
- Qed.
-
- Lemma isRUNNING_fromstate ta c0 r r0:
- (Default_arbitrate ta).(Implementation_State) = RUNNING c0 r r0 ->
- isRUNNING (Default_arbitrate ta).(Implementation_State).
- Proof.
- rewrite /isRUNNING; intros H; by rewrite H.
- Qed.
-
- Lemma FIFO_wait_neq_act :
- (WAIT.-1 == OACT_date) = false.
- Proof.
- apply /negbTE; rewrite neq_ltn.
- apply /orP; right.
- rewrite ltn_predRL.
- apply ltn_trans with (n := OCAS_date).
- 2: exact WAIT_CAS.
- unfold OCAS_date, OACT_date; simpl; unfold CAS_date.
- rewrite -ltn_subLR.
- 2: auto.
- rewrite subSnn.
- exact T_RCD_GT_ONE.
- Qed.
-
- Lemma FIFO_wait_neq_cas :
- (WAIT.-1 == OCAS_date) = false.
- Proof.
- apply /negbTE; rewrite neq_ltn.
- apply /orP; right.
- rewrite ltn_predRL.
- apply ltn_trans with (n := CAS_date + T_RTP).
- 2: exact WAIT_END.
- rewrite -ltn_subLR.
- 2: auto.
- rewrite subSnn.
- exact T_RTP_GT_ONE.
- Qed.
-
- Lemma FIFO_counter_lt_WAIT t:
- FIFO_counter (Default_arbitrate t).(Implementation_State) < WAIT.
- Proof.
- set (c := FIFO_counter (Default_arbitrate t).(Implementation_State)).
- unfold FIFO_counter in c.
- destruct (Default_arbitrate t).(Implementation_State) eqn:HS.
- all: subst c; (done || by destruct c0).
- Qed.
-
- Lemma FIFO_WAIT_GT_ACTp1 :
- ACT_date.+1 < WAIT.
- Proof.
- apply ltn_trans with (n := CAS_date).
- 2: exact WAIT_CAS.
- unfold CAS_date, ACT_date.
- rewrite prednK.
- 2: specialize T_RP_GT_ONE as H; apply ltn_trans with (n := 1); done || exact H.
- rewrite addnC -nat_add_pred addnC nat_add_pred.
- apply nat_ltn_add.
- rewrite ltn_predRL; exact T_RCD_GT_ONE.
- Qed.
-
- Lemma FIFO_WAIT_GT_CASp1 :
- CAS_date.+1 < WAIT.
- Proof.
- apply ltn_trans with (n := CAS_date + T_RTP).
- 2: exact WAIT_END.
- rewrite -ltn_predRL nat_add_pred nat_ltn_add; done || (rewrite ltn_predRL; exact T_RTP_GT_ONE).
- Qed.
-
- Lemma FIFO_nextcycle_act_eq_actS:
- nat_of_ord (Next_cycle OACT_date) = ACT_date.+1.
- Proof.
- unfold Next_cycle.
- set (Hc := OACT_date.+1 < WAIT).
- dependent destruction Hc.
- all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
- 1: done.
- contradict x.
- apply Bool.not_false_iff_true.
- unfold OACT_date; simpl.
- apply FIFO_WAIT_GT_ACTp1.
- Qed.
-
- Lemma FIFO_next_cycle_cas_eq_casS:
- nat_of_ord (Next_cycle OCAS_date) = CAS_date.+1.
- Proof.
- unfold Next_cycle.
- set (Hc := OCAS_date.+1 < WAIT).
- dependent destruction Hc.
- all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
- 1: done.
- contradict x.
- apply Bool.not_false_iff_true.
- unfold OCAS_date; simpl.
- apply FIFO_WAIT_GT_CASp1.
- Qed.
-
- Lemma CAS_neq_ACT:
- (CAS_date == ACT_date) = false.
- Proof.
- rewrite /CAS_date /ACT_date.
- rewrite -{2}[T_RP.-1]addn0 eqn_add2l.
- rewrite eqn0Ngt. apply Bool.negb_false_iff.
- specialize T_RCD_pos as H. rewrite -lt0n in H.
- by rewrite H.
- Qed.
-
- Lemma FIFO_date_gt_0 cmd t:
- cmd \in (Default_arbitrate t).(Arbiter_Commands) -> cmd.(CDate) > 0.
- Proof.
- induction t.
- { simpl; intros H; inversion H. }
- simpl.
- unfold Next_state.
- destruct (Default_arbitrate t).(Implementation_State) eqn:HS, r eqn:HR; simpl.
- all: try (intros H; rewrite in_cons in H; move: H => /orP [/eqP H | H]).
- all: try (by rewrite H).
- all: try (by apply IHt in H).
- all: try (destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait); simpl.
- all: try (intros H; rewrite in_cons in H; move: H => /orP [/eqP H | H]).
- all: try (by rewrite H).
- all: try (by apply IHt in H).
- Qed.
-
- Lemma FIFO_in_the_past t t' a:
- t <= t' ->
- a \in (Default_arbitrate t).(Arbiter_Commands) ->
- a \in (Default_arbitrate t').(Arbiter_Commands).
- Proof.
- intros. rewrite leq_eqVlt in H; move: H => /orP [/eqP H | H]. { by rewrite -H. }
- induction t'.
- { inversion H. }
- rewrite leq_eqVlt in H; move: H => /orP [/eqP H | H].
- { apply eq_add_S in H.
- simpl; rewrite /Next_state //=.
- destruct (Default_arbitrate t').(Implementation_State), r eqn:HP; simpl.
- all: try (rewrite in_cons; apply /orP; right; subst t; exact H0).
- all: try (destruct (nat_of_ord c == ACT_date), (nat_of_ord c == CAS_date), (nat_of_ord c == WAIT.-1); simpl).
- all: try (rewrite in_cons; apply /orP; right; subst t; exact H0).
- }
- apply ltnSE in H; apply IHt' in H; simpl; rewrite /Next_state //=.
- destruct (Default_arbitrate t').(Implementation_State), r; simpl.
- all: try (rewrite in_cons; apply /orP; right; exact H).
- all: try (destruct (nat_of_ord c == ACT_date), (nat_of_ord c == CAS_date), (nat_of_ord c == WAIT.-1); simpl).
- all: try (rewrite in_cons; apply /orP; right; exact H).
- Qed.
-
- Lemma nat_of_counter_eq (ca cb : Counter_t) :
- (nat_of_ord ca == nat_of_ord cb) = (ca == cb).
- Proof.
- apply inj_eq.
- exact (ord_inj (n := WAIT)).
- Qed.
-
- (* ------------------------------------------------------------------ *)
- (* --------------------- PROOFS ABOUT THE COUNTER ------------------- *)
- (* ------------------------------------------------------------------ *)
-
- Lemma FIFO_l_inc_counter (t : nat) (c : Counter_t):
- isRUNNING (Default_arbitrate t).(Implementation_State) -> c < WAIT.-1 ->
- FIFO_counter (Default_arbitrate t).(Implementation_State) = c ->
- FIFO_counter (Default_arbitrate t.+1).(Implementation_State) = c.+1.
- Proof.
- intros Hrun H Hc; simpl.
- unfold FIFO_counter, Next_state.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (r) eqn:HP; simpl.
- all: try (by discriminate Hrun).
- all: try (destruct c0; simpl in *; destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl).
- all: try (unfold Next_cycle; simpl; set (HH := m.+1 < WAIT); dependent destruction HH).
- all: try (apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e).
- all: try (apply eq_S; exact Hc).
- all: try (rewrite Hc in x; move: x => /negbT x; contradict x; apply /negP /negPn; rewrite -ltn_predRL; exact H).
- all: try (move: Hwait => /eqP Hwait; rewrite Hwait in Hc; rewrite -Hc in H; contradict H; by rewrite ltnn).
- Qed.
-
- Lemma FIFO_l_inc_run (c : Counter_t) t:
- isRUNNING (Default_arbitrate t).(Implementation_State) -> FIFO_counter (Default_arbitrate t).(Implementation_State) = c ->
- c < WAIT.-1 -> isRUNNING (Default_arbitrate t.+1).(Implementation_State).
- Proof.
- intros Hrun Hc Hw.
- apply FIFO_l_inc_counter with (t := t) (c := c) in Hrun as Hc'.
- all: try done.
- simpl; unfold Next_state, isRUNNING.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (r) eqn:HP; simpl.
- all: try (by discriminate Hrun).
- all: destruct (nat_of_ord c0 == ACT_date) eqn:Hact, (nat_of_ord c0 == CAS_date) eqn:Hcas, (nat_of_ord c0 == WAIT.-1) eqn:Hwait; simpl.
- all: try done.
- all: try (unfold FIFO_counter in Hc; rewrite Hc in Hwait; move: Hwait => /eqP Hwait; rewrite Hwait in Hw; by rewrite ltnn in Hw).
- Qed.
-
- Lemma FIFO_l_add_counter (c : Counter_t) d t:
- isRUNNING (Default_arbitrate t).(Implementation_State) -> (c + d) < WAIT ->
- FIFO_counter (Default_arbitrate t).(Implementation_State) = c ->
- isRUNNING (Default_arbitrate (t + d)).(Implementation_State) /\
- FIFO_counter (Default_arbitrate (t + d)).(Implementation_State) = c + d.
- Proof.
- intros Hrun Hbound Hc.
- induction d.
- { by rewrite !addn0. }
- move: Hbound; rewrite !addnS; intros Hbound.
- apply ltn_trans with (m := c+d) in Hbound as IH.
- 2: apply ltnSn.
- apply IHd in IH as H; destruct H as [Hrun' Hcd].
- split.
- { apply FIFO_l_inc_run with (t := t + d) (c := Ordinal IH) in Hrun' as HH.
- 3: rewrite - ltn_predRL in Hbound; simpl; exact Hbound.
- 2: simpl; exact Hcd.
- 1: exact HH.
- }
- apply FIFO_l_inc_counter with (t := t + d) (c := Ordinal IH) in Hrun' as HH.
- 3: simpl; exact Hcd.
- 2: simpl; rewrite - ltn_predRL in Hbound; simpl; exact Hbound.
- 1: simpl in HH; simpl. exact HH.
- Qed.
-
- Lemma FIFO_l_counter_bound t:
- isRUNNING (Default_arbitrate t).(Implementation_State) -> FIFO_counter (Default_arbitrate t).(Implementation_State) <= WAIT.-1.
- Proof.
- induction t.
- { simpl; unfold isRUNNING, Init_state; by simpl. }
- simpl; unfold FIFO_counter, isRUNNING, Next_state.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (r) eqn:HP; simpl.
- all: try (by intros).
- all: try (destruct (nat_of_ord c == ACT_date) eqn:Hact,
- (nat_of_ord c == CAS_date) eqn:Hcas,
- (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl; intros).
- all: try done.
- all: try (unfold Next_cycle; set (Hc := c.+1 < WAIT); dependent destruction Hc).
- all: try (apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e).
- all: try (apply leq0n).
- all: try (by rewrite -ltn_predRL in x).
- Qed.
-
- Lemma FIFO_l_counter_border t :
- FIFO_counter (Default_arbitrate t).(Implementation_State) = WAIT.-1 ->
- FIFO_counter (Default_arbitrate t.+1).(Implementation_State) = 0.
- Proof.
- intros Hco; simpl.
- unfold Next_state.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (r) eqn:HP; simpl.
- all: try done.
- all: destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas,
- (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl; intros.
- all: try done.
- all: unfold Next_cycle; set (HH := c.+1 < WAIT).
- all: dependent destruction HH.
- all: try (apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e).
- all: try done.
- all: try (move: Hwait => /eqP Hwait; rewrite Hwait prednK in x; (exact WAIT_pos || by rewrite ltnn in x)).
- all: try (unfold FIFO_counter in Hco; move: Hwait => /eqP Hwait; contradict Hwait; exact Hco).
- Qed.
-
- Lemma FIFO_l_counter_border_run t :
- FIFO_pending (Default_arbitrate t).(Implementation_State) != [::] ->
- FIFO_counter (Default_arbitrate t).(Implementation_State) = WAIT.-1 ->
- FIFO_counter (Default_arbitrate t.+1).(Implementation_State) = 0 /\ isRUNNING (Default_arbitrate t.+1).(Implementation_State).
- Proof.
- intros HP Hc; simpl.
- rewrite /Next_state //=.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs; simpl.
- { destruct r eqn:HPP; simpl.
- 2: done.
- by rewrite /FIFO_pending in HP.
- }
- { destruct c; simpl. destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait, r eqn:HPP; simpl in *.
- all: try done.
- all: unfold Next_cycle; simpl; set (H := m.+1 < WAIT); dependent destruction H.
- all: try (apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e).
- all: try done.
- all: rewrite Hc prednK in x.
- all: try exact WAIT_pos.
- all: by rewrite ltnn in x.
- }
- Qed.
-
- (* ------------------------------------------------------------------ *)
- (* --------------------- PROOFS ------------------------------------- *)
- (* ------------------------------------------------------------------ *)
-
- Lemma FIFO_PRE_date t cmd:
- cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isPRE cmd ->
- (FIFO_counter (Default_arbitrate cmd.(CDate)).(Implementation_State) = OCycle0) /\
- (isRUNNING (Default_arbitrate cmd.(CDate)).(Implementation_State)).
- Proof.
- induction t.
- { done. }
- intros Hi Hp; simpl in *.
- rewrite /Next_state //= in Hi.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, r eqn:HP; simpl in Hi.
- all: try (rewrite in_cons in Hi; move: Hi => /orP [/eqP Hi | Hi]).
- all: try (apply IHt in Hi; (exact Hp || exact Hi)).
- all: try (contradict Hp; by rewrite Hi).
- all: try (rewrite Hi //= /Next_state //= Hs //=).
- all: destruct c; simpl in Hi.
- all: destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl in Hi.
- all: try (rewrite in_cons in Hi; move: Hi => /orP [/eqP Hi | Hi]).
- all: try (apply IHt in Hi; (exact Hp || exact Hi)).
- all: try (contradict Hp; by rewrite Hi).
- all: try (rewrite Hi /isPRE /Kind_of_req //= in Hp; contradict Hp; by case (r0.(Kind))).
- rewrite Hi //= /Next_state //= Hs //= Hact Hcas Hwait //=.
- Qed.
-
- Lemma FIFO_ACT_date t cmd:
- cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isACT cmd ->
- (FIFO_counter (Default_arbitrate cmd.(CDate)).(Implementation_State)) = Next_cycle OACT_date /\
- (isRUNNING (Default_arbitrate cmd.(CDate)).(Implementation_State)) /\
- (FIFO_request (Default_arbitrate cmd.(CDate)).(Implementation_State) == Some cmd.(Request)).
- Proof.
- induction t.
- { done. }
- intros Hi Hp; simpl in *.
- unfold Next_state in *.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs; simpl in Hi.
- { destruct r; simpl in Hi.
- { rewrite in_cons in Hi; move: Hi => /orP [/eqP Hi | Hi].
- { contradict Hp; by rewrite Hi. }
- { apply IHt in Hi; (exact Hp || exact Hi). }}
- { rewrite in_cons in Hi; move: Hi => /orP [/eqP Hi | Hi].
- { contradict Hp; by rewrite Hi. }
- { apply IHt in Hi; (exact Hp || exact Hi). }}}
- { destruct c; simpl in *; destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl in Hi.
- 7: destruct r eqn:HPP.
- all: try (rewrite in_cons in Hi; move: Hi => /orP [/eqP Hi | Hi]).
- all: try (apply IHt in Hi; (exact Hp || exact Hi)).
- all: try (rewrite Hi /isPRE /Kind_of_req //= in Hp; contradict Hp; by case (r0.(Kind))).
- all: rewrite Hi //= Hs //= Hact //=; move: Hact => /eqP Hact; unfold Next_cycle; simpl; by rewrite Hact eq_refl.
- }
- Qed.
-
- Lemma FIFO_CAS_date t cmd:
- cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isCAS cmd ->
- (FIFO_counter (Default_arbitrate cmd.(CDate)).(Implementation_State)) = Next_cycle OCAS_date /\
- (isRUNNING (Default_arbitrate cmd.(CDate)).(Implementation_State)).
- Proof.
- induction t.
- { done. }
- intros Hi Hp; simpl in *.
- unfold Next_state in *.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (r) eqn:HP; simpl in Hi.
- all: try (rewrite in_cons in Hi; move: Hi => /orP [/eqP Hi | Hi]).
- all: try (contradict Hp; by rewrite Hi).
- all: try (apply IHt in Hi; (exact Hp || exact Hi)).
- all: try (destruct c; simpl in *; destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl in Hi).
- all: try (rewrite in_cons in Hi; move: Hi => /orP [/eqP Hi | Hi]).
- all: try (apply IHt in Hi; (exact Hp || exact Hi)).
- all: try (contradict Hp; by rewrite Hi).
- all: try (rewrite Hi; simpl; rewrite Hs; simpl; rewrite Hact Hcas; simpl; move: Hcas => /eqP Hcas; unfold Next_cycle; simpl; by rewrite Hcas).
- Qed.
-
- Lemma FIFO_l_helper_2 t t' d:
- isRUNNING (Default_arbitrate t).(Implementation_State) ->
- t < t' -> FIFO_counter (Default_arbitrate t).(Implementation_State) = FIFO_counter (Default_arbitrate t').(Implementation_State) ->
- FIFO_counter (Default_arbitrate t).(Implementation_State) + d < WAIT ->
- t + d < t'.
- Proof.
- intros Hrun Hlt Hc Hd.
- induction d.
- { by rewrite addn0. }
- rewrite addnS in Hd.
- apply ltn_trans with (m := FIFO_counter (Default_arbitrate t).(Implementation_State)) in Hd as HH.
- 2: rewrite -addnS; apply nat_ltnn_add; auto.
- apply ltn_trans with (m := FIFO_counter (Default_arbitrate t).(Implementation_State) + d) in Hd as IH.
- 2: apply ltnSn.
- apply IHd in IH as H.
- rewrite addnS ltn_neqAle H andbT.
- destruct (_ == t') eqn:He.
- { contradict Hc.
- move: He => /eqP He. rewrite - He.
- rewrite - addnS.
- apply FIFO_l_add_counter with (c := Ordinal HH) (d := d.+1) in Hrun as [_ HHH].
- 3: done.
- 2: rewrite addnS; exact Hd.
- simpl in HHH; rewrite HHH; apply /eqP; rewrite neq_ltn; apply /orP; left.
- by rewrite addnS ltnS leq_addr.
- }
- trivial.
- Qed.
-
- Lemma FIFO_l_helper_4 ta tb cb:
- ta < tb ->
- FIFO_counter (Default_arbitrate ta.+1).(Implementation_State) = 0 ->
- FIFO_counter (Default_arbitrate tb).(Implementation_State) = cb ->
- cb > 0 ->
- ta.+1 < tb.
- Proof.
- intros Hlt Hca Hcb Hcb_pos.
- rewrite ltn_neqAle Hlt andbT.
- destruct (_ == tb) eqn:He.
- 2: done.
- move: He => /eqP He.
- rewrite -He in Hcb.
- rewrite Hcb in Hca.
- contradict Hca.
- apply /eqP.
- rewrite neq_ltn; apply /orP; right; exact Hcb_pos.
- Qed.
-
- Lemma FIFO_l_helper_3 ta tb d (cb : Counter_t) :
- isRUNNING (Default_arbitrate ta).(Implementation_State) ->
- FIFO_counter (Default_arbitrate ta).(Implementation_State) = 0 ->
- FIFO_counter (Default_arbitrate tb).(Implementation_State) = cb ->
- d < cb -> ta < tb -> ta + d < tb.
- Proof.
- intros Hrun_a Hca Hcb Hd Hlt.
- induction d.
- { by rewrite addn0. }
- apply ltn_trans with (m:= d) in Hd as Hd'.
- 2: apply ltnSn.
- apply IHd in Hd' as H.
- rewrite addnS ltn_neqAle H andbT.
- destruct ( _ == tb) eqn:He.
- 2: done.
- move: He => /eqP He.
- apply FIFO_l_add_counter with (d := d.+1) (c := Ordinal WAIT_pos) in Hrun_a as HH.
- 3: { simpl; exact Hca. }
- 2: { simpl; rewrite add0n. apply ltn_trans with (n := cb); (exact Hd || by destruct cb). }
- destruct HH as [Hrun_adp1 Hc_adp1]; simpl in Hc_adp1.
- rewrite -He in Hcb.
- rewrite add0n addnS in Hc_adp1.
- rewrite Hc_adp1 in Hcb.
- contradict Hcb; apply /eqP.
- rewrite neq_ltn; apply /orP; left; exact Hd.
- Qed.
-
- Lemma FIFO_IDLE_to_running ta tb (d : Counter_t):
- isIDLE (Default_arbitrate ta).(Implementation_State)
- -> isRUNNING (Default_arbitrate tb).(Implementation_State)
- -> ta < tb
- -> FIFO_counter (Default_arbitrate ta).(Implementation_State) = 0
- -> ((ta + d < tb) && (isRUNNING (Default_arbitrate (ta + d)).(Implementation_State) == false))
- \/ (exists r, (ta + r <= tb) && (r <= d) && (isRUNNING (Default_arbitrate (ta + r)).(Implementation_State))
- && (FIFO_counter ((Default_arbitrate (ta + r)).(Implementation_State)) == 0)).
- Proof.
- intros Hidle_a Hrun_b Hlt Hc.
- destruct d as [d Hd].
- induction d.
- { apply isIDLE_notRunning in Hidle_a; left; simpl; by rewrite addn0 Hlt andTb Hidle_a. }
- apply ltn_trans with (m := d) in Hd as Hd'.
- 2: apply ltnSn.
- specialize IHd with (Hd := Hd') as [IH | IH]; simpl in IH.
- { (* we're still idle after D cycles, next cycle could be IDLE, RUNNING or REFRESH *)
- move : IH => /andP [IH Hrun_a'].
- rewrite leq_eqVlt in IH; move : IH => /orP [/eqP IH | IH].
- { (* tb is the cycle after *)
- right. simpl. subst tb. exists (d.+1).
- rewrite ltnSn andbT addnS Hrun_b andbT leqnn andTb /FIFO_counter.
- rewrite /isRUNNING //= /Next_state in Hrun_b Hrun_a' *.
- destruct ((Default_arbitrate (ta + d)).(Implementation_State)) eqn:HS, (r) eqn:HP; simpl.
- all: done.
- }
- { (* now tb is in the future *)
- simpl; rewrite /isIDLE in Hrun_a'.
- destruct ((Default_arbitrate (ta + d)).(Implementation_State)) eqn:HS; simpl.
- { (* from IDLE to REFRESH 1 *)
- rewrite addnS IH andTb //= /Next_state HS.
- destruct r; simpl.
- { by left. }
- right; exists (d.+1); apply ltnW in IH.
- rewrite addnS IH andTb ltnSn andTb.
- by rewrite /isRUNNING /FIFO_counter //= HS.
- }
- by contradict Hrun_a'.
- }
- }
- right. destruct IH as [r H]; move : H => /andP [/andP [/andP [Hlt' Hrd ] Hrun_a'] Hc'].
- exists (r); simpl.
- rewrite Hlt' andTb; apply /andP; split.
- { apply /andP. split.
- { apply leq_trans with (n := d); (exact Hrd || apply ltnW, ltnSn). }
- exact Hrun_a'.
- }
- exact Hc'.
- Qed.
-
- Lemma FIFO_running_at_zero_lt_at_c t t' d:
- isRUNNING (Default_arbitrate t).(Implementation_State) ->
- t < t' -> FIFO_counter (Default_arbitrate t).(Implementation_State) = 0 ->
- d < FIFO_counter (Default_arbitrate t').(Implementation_State) ->
- t + d < t'.
- Proof.
- intros Hrun Hlt HcZ Hd.
- induction d.
- - by rewrite addn0.
- - apply ltn_trans with (m := d) in Hd as IH.
- 2: apply ltnSn.
- apply IHd in IH; clear IHd.
- rewrite addnS ltn_neqAle IH andbT.
- specialize (FIFO_counter_lt_WAIT t') as HW.
- destruct ((t + d).+1 == t') eqn:H.
- - apply FIFO_l_add_counter with (c := OCycle0) (d := d.+1) in Hrun as [_ HcD].
- 3: exact HcZ.
- 2: rewrite add0n; apply ltn_trans with (n := FIFO_counter (Default_arbitrate t').(Implementation_State)); exact Hd || exact HW.
- move : H => /eqP H; subst.
- contradict Hd.
- by rewrite -addnS HcD add0n ltnn.
- - trivial.
- Qed.
-
- Ltac leqWAIT Hc Hrun :=
- rewrite Hc subnKC;
- ((apply FIFO_l_counter_bound in Hrun; by rewrite Hc in Hrun) ||
- (rewrite - ltnS prednK; (apply ltnSn || exact WAIT_pos))).
-
- Lemma FIFO_l_eq_bound ta tb (c : Counter_t) :
- isRUNNING (Default_arbitrate ta).(Implementation_State) ->
- isRUNNING (Default_arbitrate tb).(Implementation_State) ->
- ta < tb ->
- FIFO_counter (Default_arbitrate ta).(Implementation_State) = c ->
- FIFO_counter (Default_arbitrate tb).(Implementation_State) = c ->
- ta + WAIT <= tb.
- Proof.
- intros Hrun_a Hrun_b Hlt Hc_a Hc_b.
- apply FIFO_l_helper_2 with (t' := tb) (d := WAIT.-1 - c) in Hrun_a as Hlt'.
- 4: leqWAIT Hc_a Hrun_a.
- 3: by rewrite Hc_a Hc_b.
- 2: exact Hlt.
- apply FIFO_l_add_counter with (c := c) (d := WAIT.-1 - c) in Hrun_a as H.
- destruct H as [Hrun_a' Hc_a'].
- 3: done.
- 2: rewrite - {1} Hc_a; leqWAIT Hc_a Hrun_a.
- assert (c + (WAIT.-1 - c) = WAIT.-1). { rewrite subnKC. reflexivity. destruct c. simpl. by apply nat_ltn_leq_pred. }
- rewrite H in Hc_a'; clear H.
- apply FIFO_l_counter_border in Hc_a' as Hc_a''.
- destruct (FIFO_counter (Default_arbitrate tb).(Implementation_State) == 0) eqn:HcZ.
- { move : HcZ => /eqP HcZ.
- rewrite HcZ in Hc_b; rewrite -Hc_b subn0 -addnS prednK in Hlt'; exact WAIT_pos || exact Hlt'.
- }
- move : HcZ => /negbT HcZ; rewrite -lt0n in HcZ.
- destruct (Default_arbitrate (ta + (WAIT.-1 - c)).+1).(Implementation_State) eqn:Hs.
- { (* IDLE branch *)
- assert (FIFO_counter (Default_arbitrate (ta + (WAIT.-1 - c)).+1).(Implementation_State) = 0) as Haux.
- { rewrite /FIFO_counter Hs. by rewrite /FIFO_counter in Hc_a''. }
- clear Hc_a''; rename Haux into Hc_a''; apply isIDLE_fromstate in Hs as Hrun_a''.
- rewrite leq_eqVlt in Hlt'; move : Hlt' => /orP [/eqP Hlt' | Hlt'].
- { subst tb.
- rewrite Hc_b in Hc_a''.
- rewrite Hc_a'' subn0 -addnS prednK.
- 2: exact WAIT_pos.
- apply leqnn.
- }
- apply FIFO_IDLE_to_running with (tb := tb) (d := c) in Hrun_a'' as [Hlt'' | Hlt''].
- 5: exact Hc_a''.
- 4: exact Hlt'.
- 3: exact Hrun_b.
- { (* Stays IDLE until the counter equals c again *)
- move : Hlt'' => /andP [Hlt'' _].
- rewrite -[(ta + _).+1]addnS -subSn in Hlt''.
- 2: rewrite -ltnS prednK; ( by destruct c) || exact WAIT_pos.
- rewrite prednK in Hlt''.
- 2: exact WAIT_pos.
- rewrite addnBA in Hlt''.
- 2: apply ltnW; by destruct c.
- rewrite subnK in Hlt''.
- 2: apply nat_leq_addl; apply ltnW; by destruct c.
- by apply ltnW.
- }
- move : Hlt'' => [r1 /andP [/andP [/andP [Hlt'' Hr ] Hrun_a'''] /eqP Hc_a''']].
- rewrite leq_eqVlt in Hlt''; move : Hlt'' => /orP [/eqP Hlt'' | Hlt''].
- { subst tb.
- rewrite Hc_b in Hc_a'''.
- rewrite Hc_a''' subn0 -addnS prednK.
- 2: exact WAIT_pos.
- apply leq_addr.
- }
- apply FIFO_running_at_zero_lt_at_c with (t' := tb) (d := (FIFO_counter (Default_arbitrate tb).(Implementation_State)).-1) in Hrun_a''' as Hlt'''.
- 4: rewrite ltn_predL; exact HcZ.
- 3: exact Hc_a'''.
- 2: exact Hlt''.
- rewrite Hc_b in Hlt'''.
- rewrite -[(ta + _).+1]addnS -subSn in Hlt'''.
- 2: rewrite -ltnS prednK; (by destruct c) || exact WAIT_pos.
- rewrite prednK in Hlt'''.
- 2: exact WAIT_pos.
- rewrite -subn1 addnBA in Hlt'''.
- 2: rewrite -Hc_b; exact HcZ.
- rewrite subn1 addnBA in Hlt'''.
- 2: apply ltnW; by destruct c.
- rewrite prednK in Hlt'''.
- 2: apply ltn_addl; by rewrite -Hc_b.
- rewrite addnBAC in Hlt'''.
- 2: apply nat_leq_addl; apply ltnW; (by destruct c) || exact WAIT_pos.
- rewrite subnK in Hlt'''.
- 2: apply nat_leq_addr, nat_leq_addl; apply ltnW; (by destruct c) || exact WAIT_pos.
- apply leq_trans with (m := ta + WAIT ) in Hlt'''.
- 2: by apply nat_leq_addr.
- exact Hlt'''.
- }
- { (* RUNNING branch *)
- assert (FIFO_counter (Default_arbitrate (ta + (WAIT.-1 - c)).+1).(Implementation_State) = 0) as Haux.
- { rewrite /FIFO_counter Hs. by rewrite /FIFO_counter in Hc_a''. }
- clear Hc_a''; rename Haux into Hc_a''.
- apply isRUNNING_fromstate in Hs as Hrun_a''.
- apply FIFO_l_helper_4 with (cb := c) in Hlt' as Hlt''.
- 4: by rewrite -Hc_b.
- 3: exact Hc_b.
- 2: exact Hc_a''.
- apply FIFO_l_helper_3 with (tb := tb) (d := c.-1) (cb := c) in Hrun_a'' as Hlt'''.
- 5: exact Hlt''.
- 4: by rewrite ltn_predL -Hc_b.
- 3: exact Hc_b.
- 2: exact Hc_a''.
- rewrite -addnS prednK in Hlt'''.
- 2: by rewrite -Hc_b.
- rewrite -addnS -subSS prednK in Hlt'''.
- 2: exact WAIT_pos.
- rewrite subnS prednK in Hlt'''.
- 2: rewrite subn_gt0; by destruct c.
- rewrite -addnA subnK in Hlt'''.
- 2: { destruct c; simpl; rewrite leq_eqVlt; apply /orP; by right. }
- exact Hlt'''.
- }
- Qed.
-
- (* ------------------------------------------------------------------ *)
- (* --------------------- TIMING PROOFS ------------------------------ *)
- (* ------------------------------------------------------------------ *)
-
- Lemma Cmds_T_RCD_ok t a b:
- a \in Commands -> b \in Commands ->
- ACT_to_CAS a b -> Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RCD.
-
- Lemma Cmds_T_RRD_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- ACT_to_ACT a b -> ~~ Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RRD.
- Proof.
- intros Ha Hb AtA nSb aBb.
- move : AtA => /andP [Aa Ab].
- apply FIFO_ACT_date in Ha as [Hc_a [Hrun_a _]].
- 2: exact Aa; clear Aa.
- apply FIFO_ACT_date in Hb as [Hc_b [Hrun_b _]].
- 2: exact Ab; clear Ab.
- apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OACT_date) in Hrun_a as Hlt.
- 5: exact Hc_b.
- 4: exact Hc_a.
- 3: exact aBb.
- 2: exact Hrun_b.
- unfold Apart_at_least.
- apply leq_trans with (n := (a.(CDate) + WAIT)).
- 2: exact Hlt.
- rewrite leq_add2l.
- by rewrite leq_eqVlt RRD_WAIT orbT.
- Qed.
-
- Lemma Cmds_T_FAW_ok t a b c d:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- c \in (Default_arbitrate t).(Arbiter_Commands) -> d \in (Default_arbitrate t).(Arbiter_Commands) ->
- isACT a -> isACT b -> isACT c -> isACT d -> Diff_Bank [::a;b;c;d] ->
- Before a b -> Before b c -> Before c d ->
- Apart_at_least a d T_FAW.
- Proof.
- intros Ha Hb Hc Hd iAa iAb iAc iAd dB aBb bBc cBd.
- apply FIFO_date_gt_0 in Ha as Ha_pos.
- apply FIFO_date_gt_0 in Hb as Hb_pos.
- apply FIFO_date_gt_0 in Hc as Hc_pos.
- apply FIFO_date_gt_0 in Hd as Hd_pos.
- unfold Apart_at_least.
- apply FIFO_ACT_date in Ha as [Hc_a [Hrun_a _]].
- apply FIFO_ACT_date in Hb as [Hc_b [Hrun_b _]].
- apply FIFO_ACT_date in Hc as [Hc_c [Hrun_c _]].
- apply FIFO_ACT_date in Hd as [Hc_d [Hrun_d _]].
- all: try done.
- clear iAa iAb iAc iAd.
- apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate)) (c := Next_cycle OACT_date) in Hrun_a as Hlt_ab.
- all: try done.
- apply FIFO_l_eq_bound with (ta := b.(CDate)) (tb := c.(CDate)) (c := Next_cycle OACT_date) in Hrun_b as Hlt_bc.
- all: try done.
- apply FIFO_l_eq_bound with (ta := c.(CDate)) (tb := d.(CDate)) (c := Next_cycle OACT_date) in Hrun_c as Hlt_cd.
- all: try done.
- apply leq_trans with (p := c.(CDate) - WAIT) in Hlt_ab as Hlt_ac.
- 2: rewrite leq_psubRL; (rewrite -addnC; exact Hlt_bc) || exact Hb_pos.
- rewrite leq_psubRL addnC in Hlt_ac.
- 2: rewrite addn_gt0; apply /orP; left; exact WAIT_pos.
- apply leq_trans with (p := d.(CDate) - WAIT) in Hlt_ac as Hlt_ad.
- 2: rewrite leq_psubRL; (by rewrite -addnC) || exact Hc_pos.
- rewrite leq_psubRL addnC in Hlt_ad.
- 2: rewrite addn_gt0; apply /orP; left; exact WAIT_pos.
- apply leq_trans with (n := (a.(CDate) + WAIT + WAIT + WAIT)).
- 2: exact Hlt_ad.
- by rewrite -addnA -addnA leq_add2l addnA leq_eqVlt FAW_WAIT orbT.
- Qed.
-
- Lemma Cmds_T_RP_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- PRE_to_ACT a b -> Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RP.
- Proof.
- intros Ha Hb pTa sB aBb.
- rewrite /PRE_to_ACT in pTa; move: pTa => /andP [iPa iAb].
- apply FIFO_ACT_date in Hb as [Hc_b [Hrun_b _]].
- 2: exact iAb.
- apply FIFO_PRE_date in Ha as [Hc_a Hrun_a].
- 2: exact iPa.
- unfold Apart_at_least.
- apply FIFO_running_at_zero_lt_at_c with (t':= b.(CDate)) (d := ACT_date) in Hc_a as H.
- 4: rewrite Hc_b; by rewrite FIFO_nextcycle_act_eq_actS.
- 3: by unfold Before in aBb.
- 2: exact Hrun_a.
- unfold ACT_date in H.
- rewrite -addnS prednK in H.
- 2: specialize T_RP_GT_ONE as H; apply ltn_trans with (n := 1); done || exact H.
- exact H.
- Qed.
-
- Lemma Cmds_T_RTP_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CRD_to_PRE a b -> Same_Bank a b -> Before a b -> Apart_at_least a b T_RTP.
- Proof.
- intros Ha Hb Htype sB aBb.
- rewrite /CRD_to_PRE in Htype; move: Htype => /andP [iCa iPb].
- apply FIFO_CAS_date in Ha as [Hc_a Hrun_a].
- 2: unfold isCAS; unfold isCRD in iCa; apply /orP; left; exact iCa.
- apply FIFO_PRE_date in Hb as [Hc_b Hrun_b].
- 2: exact iPb.
- unfold Apart_at_least.
- apply FIFO_l_add_counter with (c := OCycle0) (d := CAS_date.+1) in Hrun_b as [Hrun_b' Hc_b'].
- 3: exact Hc_b.
- 2: simpl; rewrite add0n; exact FIFO_WAIT_GT_CASp1.
- rewrite -{2}FIFO_next_cycle_cas_eq_casS in Hc_b'; simpl in Hc_b'; rewrite add0n in Hc_b'.
- apply FIFO_l_eq_bound with (ta := a.(CDate)) (tb := b.(CDate) + CAS_date.+1) (c := Next_cycle OCAS_date) in Hrun_a as H.
- 5: exact Hc_b'.
- 4: exact Hc_a.
- 3: unfold Before in aBb; apply ltn_trans with (p := b.(CDate) + CAS_date.+1) in aBb; exact aBb || (by rewrite nat_ltn_add).
- 2: exact Hrun_b'.
- rewrite [b.(CDate) + _]addnC -leq_subLR in H.
- apply leq_trans with (n := a.(CDate) + WAIT - CAS_date.+1).
- 2: exact H.
- rewrite -addnBA.
- 2: exact WAIT_CAS.
- rewrite leq_add2l leq_subRL.
- 2: exact WAIT_CAS.
- rewrite addnC addnS addnC.
- exact WAIT_END.
- Qed.
-
- (* ------------------------------------------------------------------ *)
- (* -------------------- REQUEST PROOFS ------------------------------ *)
- (* ------------------------------------------------------------------ *)
-
- Lemma Pending_on_arrival ta ra:
- ra \in Arrival_at ta
- -> ra \in (FIFO_pending ((Default_arbitrate ta).(Implementation_State))).
- Proof.
- intros HA.
- destruct ta.
- { by rewrite /FIFO_pending //= /Enqueue mem_cat HA orTb. }
- { rewrite /FIFO_pending //= /Next_state.
- destruct (Default_arbitrate ta).(Implementation_State) as [c P | c P rb] eqn:HSS; simpl.
- { destruct P eqn:HP.
- { simpl. exact HA. }
- { simpl. assert (r == r). apply /eqP. reflexivity. by rewrite H /Enqueue mem_cat HA orbT. }
- }
- { destruct c; simpl.
- destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl.
- all: try by rewrite /Enqueue mem_cat HA orbT.
- destruct P eqn:HP; simpl.
- { exact HA. }
- { by rewrite /Enqueue mem_cat HA orbT. }
- }
- }
- Qed.
-
- Lemma Pending_requestor ta ra:
- ra \in FIFO_pending (Default_arbitrate ta).(Implementation_State)
- -> isRUNNING (Default_arbitrate ta).(Implementation_State)
- -> FIFO_counter (Default_arbitrate ta).(Implementation_State) != WAIT.-1
- -> ra \in FIFO_pending (Default_arbitrate ta.+1).(Implementation_State).
- Proof.
- intros HP Hrun HCS.
- simpl; unfold Next_state, FIFO_pending, isRUNNING in *.
- destruct (Default_arbitrate ta).(Implementation_State); simpl.
- { discriminate Hrun. }
- { destruct c; simpl. destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait, r eqn:HPP; simpl.
- all: try discriminate HP.
- all: try by rewrite /Enqueue -cat_cons mem_cat HP orTb.
- move: Hwait => /eqP Hwait; simpl in HCS.
- contradict Hwait. apply /eqP. exact HCS.
- }
- Qed.
-
- Lemma Running_on_next_cycle ra ta:
- ra \in (FIFO_pending (Default_arbitrate ta).(Implementation_State)) ->
- isIDLE (Default_arbitrate ta).(Implementation_State) ->
- (isRUNNING (Default_arbitrate ta.+1).(Implementation_State)) && (FIFO_counter (Default_arbitrate ta.+1).(Implementation_State) == OCycle0).
- Proof.
- intros HP Hidle.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- 2: discriminate Hidle.
- clear Hidle.
- rewrite /FIFO_pending in HP.
- simpl. rewrite /Next_state Hs.
- destruct r eqn:HP'.
- { discriminate HP. }
- simpl. done.
- Qed.
-
- Lemma Request_index_decrements_within_period_idle ta ra:
- let S := (Default_arbitrate ta).(Implementation_State) in
- (ra \in (FIFO_pending S))
- -> isIDLE (S)
- -> (0 < index ra (FIFO_pending S))
- -> forall tb, ta < tb
- -> tb <= ta + WAIT
- -> let S' := (Default_arbitrate tb).(Implementation_State) in
- (ra \in (FIFO_pending S')) && ((index ra (FIFO_pending S)) == (index ra (FIFO_pending S')).+1).
- Proof.
- intros S HP Hidle HI.
- unfold S in *; clear S.
- destruct ((Default_arbitrate ta).(Implementation_State)) eqn:HSS; simpl.
- 2: discriminate Hidle.
- induction tb; intros HL HU.
- { contradict HL. by rewrite ltn0. }
- { rewrite leq_eqVlt in HL; move: HL => /orP [HL | HL].
- { clear IHtb.
- rewrite eqSS in HL; move: HL => /eqP HL; subst.
- simpl; unfold FIFO_counter, FIFO_pending, Next_state in *.
- rewrite HSS.
- destruct r eqn:HPP; simpl.
- { discriminate HP. }
- { assert (r0 == r0) as H'. apply /eqP. reflexivity. rewrite H'. clear H'.
- simpl in HI. destruct (r0 == ra) eqn:Heq.
- { discriminate HI. }
- rewrite in_cons in HP. move: HP => /orP [/eqP HP | HP].
- { contradict Heq. rewrite HP. apply /eqP. by rewrite eq_refl. }
- { rewrite /Enqueue mem_cat HP orTb index_cat HP. apply /eqP. reflexivity. }
- }
- }
- rewrite ltnS in HL.
- apply ltnW in HU as HU'.
- apply IHtb in HL as IH. clear IHtb.
- 2: exact HU'.
- move: IH => /andP [HP' /eqP IH'].
- rewrite -HSS in HP. apply Running_on_next_cycle in HP as HC. move: HC => /andP [Hrun /eqP Hc].
- 2: by rewrite HSS.
- apply FIFO_l_add_counter with (c := OCycle0) (d := tb - (ta.+1)) in Hrun as Haux. destruct Haux as [Hrun_a' Hca'].
- 3: exact Hc.
- 2: {
- rewrite /OCycle0 //= add0n ltn_subLR.
- 2: exact HL.
- apply ltn_trans with (n := ta + WAIT).
- exact HU.
- rewrite ltn_add2r. done.
- }
- assert (ta.+1 + (tb - ta.+1) = tb).
- { rewrite subnKC. reflexivity. exact HL. }
- rewrite H in Hrun_a', Hca'. clear H.
- rewrite /OCycle0 //= add0n in Hca'.
- apply Pending_requestor with (ra := ra) in Hrun_a' as Hpen.
- 3: {
- rewrite Hca' neq_ltn. apply /orP. left.
- rewrite ltn_subLR.
- 2: exact HL.
- rewrite addnC -subn1 addnBAC.
- 2: exact WAIT_pos.
- rewrite subn1 nat_add_pred. rewrite PeanoNat.Nat.pred_succ addnC. exact HU.
- }
- 2: exact HP'.
- rewrite Hpen andTb. rewrite IH'. clear HP HI Hpen. rename Hrun_a' into Hrun_b. rename Hca' into Hcb.
- rewrite eqSS.
- simpl. unfold FIFO_pending, Next_state.
- destruct (Default_arbitrate tb).(Implementation_State) eqn:HS.
- { discriminate Hrun_b. }
- { destruct c0; simpl.
- destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl.
- all: try by rewrite /Enqueue index_cat HP'.
- simpl in Hrun_b, Hcb, IH',HP', HS.
- assert (FIFO_counter (Default_arbitrate tb).(Implementation_State) = WAIT.-1) as Heq.
- { rewrite HS //=; move: Hwait => /eqP Hwait; exact Hwait. }
- apply FIFO_l_counter_border_run in Heq as [Hcb' Hrun_b'].
- 2: rewrite HS //=; by apply Queue_non_empty in HP'.
- apply FIFO_l_eq_bound with (tb := tb.+1) (c := OCycle0) in Hrun as Hbug.
- 5,4: rewrite /OCycle0 //=.
- 3: by rewrite -[ta.+1]addn1 -[tb.+1]addn1 ltn_add2r.
- 2: exact Hrun_b'.
- contradict Hbug.
- apply /negP; rewrite leqNgt; apply /negPn.
- rewrite [ta.+1 + _]addnC -[ta.+1]addn1 addnA -[tb.+1]addn1.
- rewrite addnCAC [tb +1 ]addnC -addnA ltn_add2l.
- exact HU.
- }
- }
- Qed.
-
- Lemma Request_index_decrements_within_period ta ra:
- let S := (Default_arbitrate ta).(Implementation_State) in
- (ra \in (FIFO_pending S))
- -> (FIFO_counter S) == WAIT.-1
- -> (0 < index ra (FIFO_pending S))
- -> forall tb, ta < tb
- -> tb <= ta + WAIT
- -> let S' := (Default_arbitrate tb).(Implementation_State) in
- (ra \in (FIFO_pending S')) && ((index ra (FIFO_pending S)) == (index ra (FIFO_pending S')).+1).
- Proof.
- intros S HP HC HI.
- unfold S in *; clear S.
- induction tb; intros HL HU.
- { contradict HL. by rewrite ltn0. }
- { rewrite leq_eqVlt in HL; move: HL => /orP [HL | HL].
- { clear IHtb.
- rewrite eqSS in HL; move: HL => /eqP HL; subst.
- simpl; unfold FIFO_counter, FIFO_pending, Next_state in *.
- destruct (Default_arbitrate tb).(Implementation_State) as [c P | c P rb] eqn:HSS; move: HC => /eqP HC; subst.
- { destruct P eqn:HPP; simpl. (* IDLE state *)
- { discriminate HP. }
- { assert (r == r) as H'. apply /eqP. reflexivity. rewrite H'. clear H'.
- simpl in HI. destruct (r == ra) eqn:He.
- { discriminate HI. }
- { rewrite in_cons in HP. move: HP => /orP [/eqP HP | HP].
- { contradict He. rewrite HP. apply /eqP. by rewrite eq_refl. }
- { rewrite /Enqueue mem_cat HP orTb index_cat HP.
- apply /eqP. reflexivity.
- }
- }
- }
- }
- { rewrite HC FIFO_wait_neq_act FIFO_wait_neq_cas. (* RUNNING state *)
- assert (WAIT.-1 == WAIT.-1 = true). { apply /eqP. reflexivity. }
- rewrite H; clear H.
- destruct P eqn:HPP; simpl.
- { discriminate HP. }
- { assert (r == r) as H'. apply /eqP. reflexivity. rewrite H'. clear H'.
- simpl in HI. destruct (r == ra) eqn:He.
- { discriminate HI. }
- { rewrite in_cons in HP. move: HP => /orP [/eqP HP | HP].
- { contradict He. rewrite HP. apply /eqP. by rewrite eq_refl. }
- { rewrite /Enqueue mem_cat HP orTb index_cat HP.
- apply /eqP. reflexivity.
- }
- }
- }
- }
- }
- { rewrite ltnS in HL.
- apply IHtb in HL as IH; clear IHtb.
- 2: by apply ltnW in HU.
- move: IH => /andP [HP' /eqP HI']; rewrite HI'; move: HC => /eqP HC.
- apply FIFO_l_counter_border_run in HC.
- 2: by apply Queue_non_empty in HP.
- destruct HC as [Hca Hrun_a].
- assert (FIFO_counter (Default_arbitrate ta.+1).(Implementation_State) = OCycle0).
- { rewrite Hca /OCycle0 //=. }
- apply FIFO_l_add_counter with (c := OCycle0) (d := tb - (ta.+1)) in Hrun_a as Haux. destruct Haux as [Hrun_a' Hca'].
- 3: exact H.
- 2: {
- rewrite //= /OCycle0 add0n ltn_subLR.
- 2: exact HL.
- apply ltn_trans with (n := ta + WAIT).
- 2: by rewrite ltn_add2r ltnSn.
- exact HU.
- }
- assert (ta.+1 + (tb - ta.+1) = tb).
- { rewrite subnKC. reflexivity. exact HL. }
- rewrite H0 in Hrun_a',Hca'.
- rewrite /OCycle0 //= add0n in Hca'.
- apply Pending_requestor with (ra := ra) in Hrun_a' as Hpen.
- 3: {
- rewrite Hca' neq_ltn. apply /orP. left.
- rewrite ltn_subLR.
- 2: exact HL.
- rewrite addnC -subn1 addnBAC.
- 2: exact WAIT_pos.
- rewrite subn1 nat_add_pred. rewrite PeanoNat.Nat.pred_succ addnC. exact HU.
- }
- 2: exact HP'.
- rewrite Hpen andTb; clear H H0 HP HI Hpen. rename Hrun_a' into Hrun_b.
- rewrite eqSS.
- simpl. unfold FIFO_pending, Next_state.
- destruct (Default_arbitrate tb).(Implementation_State) as [c P | c P rb] eqn:HSS.
- { discriminate Hrun_b. }
- { destruct c; simpl.
- destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl.
- all: try by rewrite /Enqueue index_cat HP'.
- simpl in Hrun_b, Hca', HI', HP', HSS.
- assert (FIFO_counter (Default_arbitrate tb).(Implementation_State) = WAIT.-1) as Heq.
- { rewrite HSS //=; move: Hwait => /eqP Hwait; exact Hwait. }
- apply FIFO_l_counter_border_run in Heq as [Hcb Hrun_b'].
- 2: rewrite HSS //=; by apply Queue_non_empty in HP'.
- apply FIFO_l_eq_bound with (tb := tb.+1) (c := OCycle0) in Hrun_a as Hbug.
- 5: rewrite /OCycle0 //=.
- 4: rewrite /OCycle0 //=.
- 3: by rewrite -[ta.+1]addn1 -[tb.+1]addn1 ltn_add2r.
- 2: exact Hrun_b'.
- contradict Hbug.
- apply /negP; rewrite leqNgt; apply /negPn.
- rewrite [ta.+1 + _]addnC -[ta.+1]addn1 addnA -[tb.+1]addn1.
- rewrite addnCAC [tb +1 ]addnC -addnA ltn_add2l.
- exact HU.
- }
- }
- }
- Qed.
-
- Lemma Still_pending_on_running_border ra ta:
- let S := (Default_arbitrate ta).(Implementation_State) in
- let S' := (Default_arbitrate ta.+1).(Implementation_State) in
- ra \in (FIFO_pending S) ->
- isRUNNING (S) ->
- 0 < index ra (FIFO_pending S) ->
- FIFO_counter (S) == WAIT.-1 ->
- (isRUNNING S') &&
- (FIFO_counter S' == OCycle0) &&
- (ra \in FIFO_pending S') &&
- (index ra (FIFO_pending S) == (index ra (FIFO_pending S')).+1).
- Proof.
- intros S S' HP Hrun Hi_pos Hc.
- unfold S,S' in *; clear S S'.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- { discriminate Hrun. }
- { simpl. rewrite /Next_state Hs //=.
- destruct c; simpl in *.
- destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait.
- all: try done.
- 4: destruct r eqn:HPP.
- all: simpl.
- 4: { discriminate HP. }
- 4: {
- assert (r1 == r1). done. rewrite H.
- destruct (r1 == ra) eqn:Heq.
- { move: Heq => /eqP Heq. rewrite Heq //= in Hi_pos.
- assert (ra == ra). done. by rewrite H0 in Hi_pos.
- }
- rewrite in_cons in HP. move: HP => /orP [/eqP Hbug | HP].
- { rewrite Hbug in Heq. contradict Heq. apply Bool.not_false_iff_true. rewrite eq_refl. trivial. }
- by rewrite /Enqueue mem_cat HP orTb index_cat HP eq_refl.
- }
- all: try (move: Hwait => /eqP Hwait; rewrite Hwait in Hact; specialize FIFO_wait_neq_act as H;
- rewrite /OACT_date //= in H; by rewrite H in Hact).
- move: Hwait => /eqP Hwait; rewrite Hwait in Hcas; specialize FIFO_wait_neq_cas as H;
- rewrite /OCAS_date //= in H; by rewrite H in Hcas.
- }
- Qed.
-
- Lemma Still_pending_on_idle_border ra ta:
- let S := (Default_arbitrate ta).(Implementation_State) in
- let S' := (Default_arbitrate ta.+1).(Implementation_State) in
- ra \in (FIFO_pending S) ->
- isIDLE (S) ->
- 0 < index ra (FIFO_pending S) ->
- (isRUNNING S') &&
- (FIFO_counter S' == OCycle0) &&
- (ra \in FIFO_pending S') &&
- (index ra (FIFO_pending S) == (index ra (FIFO_pending S')).+1).
- Proof.
- intros S S' HP Hidle Hi.
- unfold S,S' in *; clear S S'.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- 2: discriminate Hidle.
- clear Hidle; rewrite /FIFO_pending in HP, Hi.
- simpl; rewrite /Next_state Hs.
- destruct r eqn:HPP; simpl.
- 1: discriminate HP.
- { assert (r0 == r0). done.
- rewrite H.
- destruct (r0 == ra) eqn:Heq.
- { move: Heq => /eqP Heq. by rewrite Heq //= eq_refl in Hi. }
- rewrite in_cons in HP; move: HP => /orP [Hbug | HP].
- { by rewrite eq_sym Heq in Hbug. }
- by rewrite /Enqueue mem_cat HP orTb andTb index_cat HP eq_refl.
- }
- Qed.
-
- Lemma Still_pending_during_window ra ta (c : Counter_t):
- let S := (Default_arbitrate ta).(Implementation_State) in
- ra \in (FIFO_pending S) ->
- isRUNNING (S) ->
- FIFO_counter (S) == c ->
- forall d, c + d < WAIT -> let S' := (Default_arbitrate (ta + d)).(Implementation_State) in
- (ra \in (FIFO_pending S')) &&
- (index ra (FIFO_pending S) == index ra (FIFO_pending S')).
- Proof.
- intros S HP Hrun Hc d Hlt; simpl.
- unfold S in *; clear S.
- induction d.
- { rewrite addn0 HP andTb. apply /eqP. reflexivity. }
- { apply ltn_trans with (m := c + d) in Hlt as Hlt'.
- 2: rewrite addnS; done.
- apply IHd in Hlt' as IH. clear IHd.
- move: IH => /andP [HP' Hi].
- apply FIFO_l_add_counter with (c := c) (d := d) in Hrun as H. destruct H as [Hrun' Hc'].
- 3: by apply /eqP.
- 2: exact Hlt'.
- destruct (Default_arbitrate (ta + d)).(Implementation_State) eqn:Hs.
- { discriminate Hrun'. }
- { clear Hrun'.
- rewrite addnS; simpl; rewrite /Next_state Hs //=.
- rewrite /FIFO_counter in Hc'.
- destruct c0; simpl in *.
- destruct (m == ACT_date) eqn:Hact, (m == CAS_date) eqn:Hcas, (m == WAIT.-1) eqn:Hwait; simpl.
- all: try (rewrite addnS -Hc' in Hlt; move: Hwait => /eqP Hwait; rewrite Hwait prednK in Hlt; (by rewrite ltnn in Hlt || exact WAIT_pos)).
- all: rewrite /Enqueue mem_cat HP' orTb //=.
- all: move: Hi => /eqP Hi; by rewrite Hi index_cat HP'.
- }
- }
- Qed.
-
- Lemma Request_index_decrements_over_period ta ra:
- let S := (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) in
- ra \in (FIFO_pending S) ->
- forall i, let S' := (Default_arbitrate ((Requestor_slot_start ta) + i * WAIT)).(Implementation_State) in
- i > 0 -> i <= (index ra (FIFO_pending S)) ->
- (ra \in (FIFO_pending S')) && ((index ra (FIFO_pending S)) == (index ra (FIFO_pending S')) + i).
- Proof.
- intros S HP i S' Hi_pos HU.
- unfold S,S' in *; clear S S'.
- induction i.
- { discriminate Hi_pos. }
- { rewrite leq_eqVlt in Hi_pos. move: Hi_pos => /orP [/eqP Heq | Hi_pos].
- { clear IHi.
- rewrite -Heq mul1n.
- rewrite -[i.+1]add1n addnC -{1}[1]add0n in Heq. move: Heq => /eqP Heq. rewrite eqn_add2r in Heq. move: Heq => /eqP Heq.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- { unfold Requestor_slot_start in *. rewrite Hs in HP, HU. (* IDLE leg *)
- rewrite Hs.
- rewrite -Heq in HU.
- apply Still_pending_on_idle_border in HP as H. move: H => /andP [ /andP [ /andP [Hrun Hc] HP' ] Hi].
- 3: exact HU.
- 2: by rewrite Hs.
- apply Still_pending_during_window with (c := OCycle0) (d := WAIT.-1) in HP' as H. move: H => /andP [HP'' Hi'].
- 4: rewrite ltn_predL; exact WAIT_pos.
- 3: exact Hc.
- 2: exact Hrun.
- assert (ta.+1 + WAIT.-1 = ta + WAIT).
- { by rewrite -nat_add_pred addnC addnS -pred_Sn addnC. }
- rewrite H in HP'' Hi'. clear H.
- rewrite HP'' andTb.
- move: Hi => /eqP Hi. rewrite Hi.
- move: Hi' => /eqP Hi'. rewrite Hi'.
- rewrite addn1 eqSS. apply /eqP. reflexivity.
- }
- { unfold Requestor_slot_start in *. rewrite Hs. rewrite Hs in HP,HU.
- assert (isRUNNING (Default_arbitrate ta).(Implementation_State)) as Hrun.
- { by rewrite Hs. }
- apply FIFO_l_add_counter with (c:= c) (d := (WAIT.-1 - c)) in Hrun as Hc.
- 3: by rewrite /FIFO_counter Hs.
- 2: { rewrite subnKC.
- 2: destruct c; simpl; clear Hs HP HU; by apply nat_ltn_leq_pred in i0.
- 1: rewrite ltn_predL. exact WAIT_pos.
- }
- destruct Hc as [Hrun' Hc].
- rewrite subnKC in Hc.
- 2: destruct c; simpl; clear Hs HP HU Hrun Hrun'; by apply nat_ltn_leq_pred in i0.
- apply Still_pending_on_running_border in HP as H. move: H => /andP [ /andP [ /andP [Hrun'' Hc'] HP'] Hi].
- 4: by rewrite Hc.
- 3: by rewrite -Heq in HU.
- 2: exact Hrun'.
- apply Still_pending_during_window with (c := OCycle0) (d := WAIT.-1) in HP' as H. move: H => /andP [HP'' Hi'].
- 4: rewrite ltn_predL; exact WAIT_pos.
- 3: exact Hc'.
- 2: exact Hrun''.
- assert ((ta + (WAIT.-1 -c)).+1 + WAIT.-1 = ta + (WAIT.-1 - c) + WAIT) as H.
- { rewrite -addnS -addn1 addnA -addnA [1 + WAIT.-1]addnC addn1 prednK. reflexivity. exact WAIT_pos. }
- rewrite H in HP'',Hi'.
- rewrite HP'' andTb.
- move: Hi => /eqP Hi. rewrite Hi.
- move: Hi' => /eqP Hi'. rewrite Hi'.
- rewrite addn1 eqSS. apply /eqP. reflexivity.
- }
- }
- { rewrite -[i.+1]addn1 -{1}[1]add0n ltn_add2r in Hi_pos.
- apply ltnW in HU as HU'.
- apply IHi in Hi_pos as IH. clear IHi. move: IH => /andP [HP' /eqP Hi].
- 2: exact HU'.
- destruct (Default_arbitrate (Requestor_slot_start ta + i * WAIT)).(Implementation_State) eqn:Hs.
- { assert (isIDLE(Default_arbitrate (Requestor_slot_start ta + i * WAIT)).(Implementation_State)) as Hidle.
- { by rewrite Hs. }
- apply Request_index_decrements_within_period_idle with (ra := ra) (tb := Requestor_slot_start ta + i.+1 * WAIT) in Hidle.
- 5: by rewrite mulSn -addnA leq_add2l addnC leqnn.
- 4: rewrite mulSn ltn_add2l addnC; apply nat_ltnn_add; exact WAIT_pos.
- 3: { rewrite -Hs in Hi. rewrite Hi in HU. rewrite addnC in HU. by apply nat_ltn_add_rev in HU. }
- 2: { by rewrite -Hs in HP'. }
- move: Hidle => /andP [HP'' Hi'].
- rewrite HP'' andTb.
- rewrite -Hs in Hi. rewrite Hi. move: Hi' => /eqP Hi'.
- rewrite Hi' -addn1 -addnA [1 + i]addnC addn1.
- apply /eqP. reflexivity.
- }
- { rewrite -Hs in HP'.
- assert (c + (WAIT.-1 -c ) = WAIT.-1) as Hcounter.
- { rewrite subnKC. reflexivity. destruct c. simpl in *. clear Hs. by apply nat_ltn_leq_pred in i0. }
- assert (isRUNNING (Default_arbitrate (Requestor_slot_start ta + i * WAIT)).(Implementation_State)) as Hrun.
- { by rewrite Hs. }
- apply FIFO_l_add_counter with (c := c) (d := (WAIT.-1 -c)) in Hrun as Hc. destruct Hc as [Hrun' Hc].
- 3: by rewrite Hs.
- 2: { rewrite Hcounter ltn_predL. exact WAIT_pos. }
- apply Still_pending_during_window with (c := c) (d := (WAIT.-1 -c)) in HP' as H. move: H => /andP [HP'' Hi'].
- 4: { rewrite Hcounter ltn_predL. exact WAIT_pos. }
- 3: by rewrite Hs.
- 2: by rewrite Hs.
- apply Still_pending_on_running_border in HP'' as H.
- 4: { rewrite Hcounter in Hc. apply /eqP. exact Hc. }
- 3: { move: Hi' => /eqP Hi'. rewrite -Hi'. rewrite -Hs in Hi. rewrite Hi in HU. rewrite addnC in HU. by apply nat_ltn_add_rev in HU. }
- 2: exact Hrun'.
- move: H => /andP [/andP [/andP [Hrun'' Hc'] HP'''] Hi''].
- apply Still_pending_during_window with (c := OCycle0) (d := c) in HP''' as H.
- 4: by destruct c.
- 3: exact Hc'.
- 2: exact Hrun''.
- move: H => /andP [HP'''' Hi'''].
- rewrite mulSn -![WAIT + i * WAIT]addnC addnA.
- assert ((Requestor_slot_start ta + i * WAIT + (WAIT.-1 - c)).+1 + c = Requestor_slot_start ta + i * WAIT + WAIT).
- { rewrite -addnS -addnA.
- apply /eqP.
- rewrite eqn_add2l -subSn.
- 2: { destruct c; simpl in *. clear Hs. by apply nat_ltn_leq_pred in i0. }
- rewrite prednK.
- 2: exact WAIT_pos.
- rewrite subnK.
- 2: { destruct c; simpl in *. clear Hs. by apply ltnW in i0. }
- apply /eqP. reflexivity.
- }
- rewrite H in HP''''; rewrite HP'''' andTb.
- rewrite H in Hi'''. move: Hi''' => /eqP Hi'''. rewrite -Hi'''.
- rewrite -Hs in Hi. rewrite Hi.
- move: Hi' => /eqP Hi'. rewrite Hi'.
- move: Hi'' => /eqP Hi''. rewrite Hi''.
- rewrite -addn1 -addnA [1 + i]addnC addn1; apply /eqP; reflexivity.
- }
- }
- }
- Qed.
-
- Lemma Request_index_zero ta ra:
- let S := (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) in
- let i := (index ra (FIFO_pending S)) in
- ra \in (FIFO_pending S)
- -> let S' := (Default_arbitrate ((Requestor_slot_start ta) + i * WAIT)).(Implementation_State) in
- (ra \in (FIFO_pending S')) && ((index ra (FIFO_pending S')) == 0).
- Proof.
- intros S i HP; simpl.
- unfold S in *. simpl in *. clear S.
- destruct i eqn:Hi.
- { rewrite mul0n addn0 HP andTb.
- fold i. apply /eqP. exact Hi.
- }
- { apply Request_index_decrements_over_period with (i := i) in HP.
- 3: { subst i. by rewrite leqnn. }
- 2: { by rewrite Hi. }
- rewrite -Hi.
- move: HP => /andP [HP' Hindex].
- subst i.
- rewrite -{1}[index ra (FIFO_pending (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State))]add0n eqn_add2r eq_sym in Hindex.
- by rewrite HP' Hindex.
- }
- Qed.
-
- Lemma Pending_requestor_slot_start ta ra:
- ra \in (FIFO_pending (Default_arbitrate ta).(Implementation_State)) ->
- forall tb, ta <= tb -> tb <= (Requestor_slot_start ta) ->
- ra \in (FIFO_pending (Default_arbitrate tb).(Implementation_State)).
- Proof.
- intros HP.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- { intros tb HL HU. (* IDLE *)
- rewrite /Requestor_slot_start Hs in HU.
- assert (ta == tb) as Heq.
- { rewrite leq_eqVlt in HL. move: HL => /orP [HL | HL].
- { exact HL. }
- { contradict HU. apply /negP. by rewrite -ltnNge HL. }
- }
- move: Heq => /eqP Heq; subst.
- unfold FIFO_pending in *. rewrite Hs. exact HP.
- }
- { intros tb HL HU. (* RUNNING*)
- rewrite /Requestor_slot_start Hs in HU.
- assert (isRUNNING (Default_arbitrate ta).(Implementation_State)) as Hrun_a. { by rewrite Hs. }
- assert (FIFO_counter (Default_arbitrate ta).(Implementation_State) = c) as Hca. { by rewrite Hs. }
- induction tb.
- { rewrite leq_eqVlt in HL. move: HL => /orP [/eqP HL | HL].
- { rewrite HL in Hrun_a. by simpl in Hrun_a. }
- inversion HL.
- }
- rewrite leq_eqVlt in HL. move: HL => /orP [/eqP HL | HL].
- { rewrite -HL. rewrite -Hs in HP. exact HP. }
- rewrite ltnS in HL. apply ltnW in HU as HH.
- apply IHtb in HL as IH. clear IHtb.
- 2: exact HH.
- apply FIFO_l_add_counter with (c := c) (d := (tb - ta)) in Hrun_a as H'. destruct H' as [Hrun_b Hcb].
- 3: exact Hca.
- 2: {
- rewrite -ltn_subLR in HU.
- 2: exact HL.
- rewrite ltn_subRL in HU. apply ltn_trans with (n := WAIT.-1). exact HU. rewrite ltn_predL WAIT_pos. done.
- }
- assert (ta + (tb - ta) = tb). { rewrite subnKC. reflexivity. exact HL. }
- rewrite H in Hrun_b Hcb. clear H.
- apply Pending_requestor in IH.
- 3: {
- rewrite Hcb neq_ltn. apply /orP. left.
- rewrite -ltn_subLR in HU.
- 2: exact HL.
- rewrite ltn_subRL in HU. exact HU.
- }
- 2: exact Hrun_b.
- exact IH.
- }
- Qed.
-
- Lemma Request_processing_starts ta ra:
- ra \in (Arrival_at ta)
- -> let t := (Requestor_slot_start ta) in
- let i := index ra (FIFO_pending (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State)) * WAIT in
- let S := (Default_arbitrate (t + i)).(Implementation_State) in
- (ra \in FIFO_pending S) && (index ra (FIFO_pending S) == 0).
- Proof.
- intros HP.
- apply Pending_on_arrival in HP.
- apply Pending_requestor_slot_start with (tb := (Requestor_slot_start ta)) in HP.
- 3: apply leqnn.
- 2: {
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hsa.
- all: rewrite /Requestor_slot_start Hsa.
- 2: by rewrite leq_addr.
- 1: by rewrite leqnn.
- }
- apply Request_index_zero in HP; simpl in HP.
- exact HP.
- Qed.
-
- Lemma Running_at_slot_start ta:
- isRUNNING (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) ->
- FIFO_counter (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) == WAIT.-1.
- Proof.
- intros H.
- unfold Requestor_slot_start in *.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- { rewrite Hs in H. discriminate H. }
- { assert (c + (WAIT.-1 - c) = WAIT.-1).
- { rewrite subnKC. reflexivity. destruct c. simpl in *. clear Hs. by apply nat_ltn_leq_pred in i. }
- assert (isRUNNING (Default_arbitrate ta).(Implementation_State)) as Hrun.
- { by rewrite Hs. }
- apply FIFO_l_add_counter with (c := c) (d := (WAIT.-1 -c)) in Hrun as [_ Hc].
- 3: by rewrite Hs.
- 2: { rewrite H0. rewrite ltn_predL. exact WAIT_pos. }
- rewrite H0 in Hc.
- apply /eqP; rewrite Hc. reflexivity.
- }
- Qed.
-
- Lemma Counter_reaches ra ta:
- let S := (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) in
- ra \in FIFO_pending (S) ->
- forall i, i > 0 -> i <= index ra (FIFO_pending S) ->
- let S' := (Default_arbitrate (Requestor_slot_start ta + i * WAIT)).(Implementation_State) in
- (isRUNNING S') &&
- (FIFO_counter (S') == WAIT.-1).
- Proof.
- intros S HP i Hi_pos Hi.
- set (S' := (Default_arbitrate (Requestor_slot_start ta + i * WAIT)).(Implementation_State)); simpl.
- unfold S,S' in *; clear S S'.
- induction i.
- { discriminate Hi_pos. }
- { rewrite leq_eqVlt in Hi_pos; move: Hi_pos => /orP [/eqP Hz | Hi_pos].
- { clear IHi.
- move:Hz => /eqP Hz; rewrite -addn1 -[i.+1]addn1 eqn_add2r in Hz; move:Hz => /eqP Hz.
- rewrite -Hz mul1n.
- destruct (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) eqn:Hs.
- { rewrite -Hs in HP.
- apply Still_pending_on_idle_border in HP as H. move: H => /andP [/andP [/andP [Hrun HC] HP'] HI].
- 3: by rewrite -Hz -Hs in Hi.
- 2: by rewrite Hs.
- apply FIFO_l_add_counter with (c := OCycle0) (d := WAIT.-1) in Hrun as H. destruct H as [Hrun' HC'].
- 3: { apply /eqP. exact HC. }
- 2: { rewrite /OCycle0 //= add0n ltn_predL. exact WAIT_pos. }
- assert ((Requestor_slot_start ta).+1 + WAIT.-1 = (Requestor_slot_start ta) + WAIT).
- { rewrite -addn1 -addnA [1 + WAIT.-1]addnC. rewrite addn1 prednK. reflexivity. exact WAIT_pos. }
- rewrite H in HC',Hrun'.
- rewrite /OCycle0 add0n in HC'.
- by rewrite HC' Hrun' eq_refl.
- }
- { rewrite -Hs in HP.
- assert (c + (WAIT.-1 -c) = WAIT.-1) as Hcounter.
- { rewrite subnKC. reflexivity. destruct c; simpl in *. clear Hs. by apply nat_ltn_leq_pred in i0. }
- assert (isRUNNING (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State)) as Hrun.
- { by rewrite Hs. }
- apply Running_at_slot_start in Hrun as Hc.
- apply Still_pending_on_running_border in HP as H.
- 4: exact Hc.
- 3: by rewrite -Hz -Hs in Hi.
- 2: exact Hrun.
- move: H => /andP [/andP [/andP [Hrun' Hc']HP']HI'].
- apply FIFO_l_add_counter with (c := OCycle0) (d := WAIT.-1) in Hrun' as [Hrun'' Hc''].
- 3: by apply /eqP.
- 2: rewrite /OCycle0 add0n ltn_predL; exact WAIT_pos.
- assert ((Requestor_slot_start ta).+1 + WAIT.-1 = Requestor_slot_start ta + WAIT).
- { apply /eqP.
- rewrite -addn1 -addnA eqn_add2l addnC addn1 prednK; (by rewrite eq_refl || exact WAIT_pos).
- }
- rewrite H in Hrun'', Hc''.
- rewrite /OCycle0 add0n in Hc''.
- by rewrite Hrun'' Hc'' eq_refl.
- }
- }
- { rename Hi into HU. rewrite -[i.+1]addn1 -{1}[1]add0n ltn_add2r in Hi_pos.
- apply ltnW in HU as HU'.
- apply IHi in Hi_pos as IH. clear IHi. move: IH => /andP [Hrun /eqP Hc].
- 2: exact HU'.
- apply Request_index_decrements_over_period with (i := i) in HP.
- 3: exact HU'.
- 2: exact Hi_pos.
- move: HP => /andP [HP' Hi].
-
- apply Still_pending_on_running_border in HP' as H.
- 4: by apply /eqP.
- 3: { move: Hi => /eqP Hi. rewrite Hi addnC in HU. by apply nat_ltn_add_rev in HU. }
- 2: exact Hrun.
- move: H => /andP [/andP [/andP [Hrun' Hc']HP'']Hi'].
- apply FIFO_l_add_counter with (c := OCycle0) (d := WAIT.-1) in Hrun' as [Hrun'' Hc''].
- 3: by apply /eqP.
- 2: rewrite /OCycle0 add0n; rewrite ltn_predL; exact WAIT_pos.
- rewrite mulSn. rewrite [WAIT + i * WAIT]addnC addnA.
- rewrite -addn1 -addnA [1 + WAIT.-1]addnC addn1 prednK in Hrun'', Hc''.
- 2: exact WAIT_pos.
- rewrite Hrun''.
- rewrite /OCycle0 add0n in Hc''.
- by rewrite Hc'' eq_refl.
- }
- }
- Qed.
-
- Lemma Request_starts_running ra ta:
- let S := (Default_arbitrate ta).(Implementation_State) in
- isRUNNING (S) ->
- FIFO_counter (S) == WAIT.-1 ->
- ra \in FIFO_pending (S) ->
- index ra (FIFO_pending S) = 0 ->
- (FIFO_request (Default_arbitrate ta.+1).(Implementation_State) == Some ra) &&
- (FIFO_counter (Default_arbitrate ta.+1).(Implementation_State) == OCycle0) &&
- (isRUNNING (Default_arbitrate ta.+1).(Implementation_State)).
- Proof.
- intros S Hrun Hc HP Hi.
- unfold S in *; clear S.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- 1: discriminate Hrun.
- simpl; rewrite /Next_state Hs.
- destruct (nat_of_ord c == OACT_date) eqn:Hact, (nat_of_ord c == OCAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl.
- all: rewrite /FIFO_counter in Hc.
- all: try by rewrite Hc in Hwait.
- 4: destruct r eqn:HPP; simpl.
- 4: { discriminate HP. }
- 4: {
- destruct (r1 == ra) eqn:Heq.
- { move: Heq => /eqP Heq. by rewrite Heq eq_refl. }
- { simpl in Hi. rewrite Heq in Hi. discriminate Hi. }
- }
- 1,2: move: Hc => /eqP Hc; rewrite Hc in Hact; by rewrite FIFO_wait_neq_act in Hact.
- move: Hc => /eqP Hc; rewrite Hc in Hcas; by rewrite FIFO_wait_neq_cas in Hcas.
- Qed.
-
- Lemma Request_starts_idle ra ta:
- let S := (Default_arbitrate ta).(Implementation_State) in
- isIDLE (S) ->
- ra \in FIFO_pending (S) ->
- index ra (FIFO_pending S) = 0 ->
- (FIFO_request (Default_arbitrate ta.+1).(Implementation_State) == Some ra) &&
- (FIFO_counter (Default_arbitrate ta.+1).(Implementation_State) == OCycle0) &&
- (isRUNNING (Default_arbitrate ta.+1).(Implementation_State)).
- Proof.
- intros S Hidle HP Hi.
- unfold S in *; clear S.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- 2: discriminate Hidle.
- simpl; rewrite /Next_state Hs.
- destruct r eqn:HPP.
- { discriminate HP. }
- simpl; rewrite eq_refl !andbT.
- rewrite /FIFO_pending in Hi.
- destruct (r0 == ra) eqn:Heq.
- { move: Heq => /eqP Heq. by rewrite Heq. }
- simpl in Hi. rewrite Heq in Hi. discriminate Hi.
- Qed.
-
- Lemma Request_starts_idle_ ra ta:
- let S := (Default_arbitrate ta).(Implementation_State) in
- isIDLE (S) ->
- ra \in FIFO_pending (S) ->
- index ra (FIFO_pending S) = 0 ->
- (FIFO_request (Default_arbitrate ta.+1).(Implementation_State) == Some ra) &&
- (FIFO_counter (Default_arbitrate ta.+1).(Implementation_State) == OCycle0) &&
- (isRUNNING (Default_arbitrate ta.+1).(Implementation_State)) &&
- (FIFO_pending (Default_arbitrate ta.+1).(Implementation_State) == Enqueue (Arrival_at ta.+1) (Dequeue ra (FIFO_pending S))).
- Proof.
- intros S Hidle HP Hi.
- unfold S in *; clear S.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- 2: discriminate Hidle.
- simpl; rewrite /Next_state Hs.
- destruct r eqn:HPP.
- { discriminate HP. }
- simpl; rewrite !eq_refl !andbT.
- rewrite /FIFO_pending in Hi.
- destruct (r0 == ra) eqn:Heq.
- { move: Heq => /eqP Heq. rewrite Heq; by rewrite !eq_refl. }
- simpl in Hi. rewrite Heq in Hi. discriminate Hi.
- Qed.
-
- Lemma Request_running_in_slot ra ta d:
- FIFO_request (Default_arbitrate ta).(Implementation_State) == Some ra ->
- FIFO_counter (Default_arbitrate ta).(Implementation_State) == OCycle0 ->
- d < WAIT ->
- (FIFO_request (Default_arbitrate (ta + d)).(Implementation_State) == Some ra).
- Proof.
- intros Hreq Hc Hd.
- induction d.
- { by rewrite addn0 Hreq. }
- apply ltn_trans with (m := d) in Hd as Hd'.
- 2: done.
- apply IHd in Hd' as IH. clear IHd.
- assert (isRUNNING (Default_arbitrate ta).(Implementation_State)) as Hrun.
- { destruct (Default_arbitrate ta).(Implementation_State).
- { rewrite /FIFO_request in Hreq. discriminate Hreq. }
- { done. }
- }
- destruct (Default_arbitrate (ta + d)).(Implementation_State) eqn:Hs.
- { rewrite /FIFO_request in IH. discriminate IH. }
- { apply FIFO_l_add_counter with (c := OCycle0) (d := d) in Hrun as H. destruct H as [Hrun' Hc'].
- 3: apply /eqP; exact Hc.
- 2: rewrite /OCycle0 //= add0n.
- rewrite /OCycle0 //= add0n in Hc'.
- rewrite addnS; simpl; rewrite /Next_state Hs //=.
- destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl.
- all: try by rewrite /FIFO_request in IH.
- destruct r eqn:HPP; simpl.
- all: rewrite Hs /FIFO_counter in Hc'; move: Hwait => /eqP Hwait; rewrite Hc' in Hwait; rewrite Hwait prednK in Hd.
- all: try exact WAIT_pos.
- all: try by rewrite ltnn in Hd.
- }
- Qed.
-
- Lemma Request_processing ta ra d:
- ra \in (Arrival_at ta)
- -> let t := Requestor_slot_start ta in
- let i := index ra (FIFO_pending (Default_arbitrate t).(Implementation_State)) * WAIT in
- d < WAIT ->
- let S' := (Default_arbitrate ((t + i).+1 + d)).(Implementation_State) in
- (FIFO_counter (S') == d) && (FIFO_request (S') == Some ra).
- Proof.
- intros HA t i Hd.
- apply Pending_on_arrival in HA as HP.
- apply Pending_requestor_slot_start with (tb := Requestor_slot_start ta) in HP as HP'.
- 3: by rewrite leqnn.
- 2: { rewrite /Requestor_slot_start. destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- by rewrite leqnn.
- by rewrite leq_addr.
- }
- destruct (index ra (FIFO_pending (Default_arbitrate t).(Implementation_State))) eqn:Hz.
- { subst i.
- rewrite mul0n addn0; subst t.
- unfold Requestor_slot_start in *.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- { rewrite -Hs in HP. apply Request_starts_idle in HP as H. move: H => /andP [/andP [Hreq Hc] Hrun].
- 3: exact Hz.
- 2: by rewrite Hs.
- apply Request_running_in_slot with (d := d) in Hreq as Hreq'.
- 3: exact Hd.
- 2: exact Hc.
- rewrite Hreq' andbT.
- apply FIFO_l_add_counter with (c:=OCycle0) (d:=d) in Hrun. destruct Hrun as [_ H].
- 3: by apply /eqP.
- 2: rewrite /OCycle0 //= add0n.
- rewrite /OCycle0 add0n in H; by apply /eqP.
- }
- { assert (isRUNNING (Default_arbitrate ta).(Implementation_State)) as Hrun.
- { by rewrite Hs. }
- assert (c + (WAIT.-1 - c ) = WAIT.-1).
- { rewrite subnKC. reflexivity. destruct c; simpl in *. clear Hs. by apply nat_ltn_leq_pred in i. }
- apply FIFO_l_add_counter with (c := c) (d := (WAIT.-1 -c)) in Hrun as H'. destruct H' as [Hrun' Hc'].
- 3: by rewrite Hs.
- 2: rewrite H ltn_predL; exact WAIT_pos.
- rewrite H in Hc'.
- apply Request_starts_running with (ra := ra) in Hrun' as H'. move: H' => /andP [/andP [Hreq Hc''] Hrun''].
- 4: exact Hz.
- 3: exact HP'.
- 2: by rewrite Hc' eq_refl.
- apply FIFO_l_add_counter with (c := OCycle0) (d:= d) in Hrun'' as H'. destruct H' as [Hrun''' Hc'''].
- 3: by apply /eqP.
- 2: by rewrite /OCycle0 add0n.
- apply Request_running_in_slot with (d := d) in Hreq.
- 3: exact Hd.
- 2: exact Hc''.
- rewrite Hreq andbT.
- rewrite /OCycle0 add0n in Hc'''; by rewrite Hc''' eq_refl.
- }
- }
- apply Counter_reaches with (i := index ra (FIFO_pending (Default_arbitrate t).(Implementation_State))) in HP'.
- 3: by subst t.
- 2: by rewrite Hz.
- move: HP' => /andP [Hrun HC].
- apply Request_processing_starts in HA as H. move: H => /andP [HP' Hiz].
- fold t in Hrun,HC; rewrite Hz in Hrun,HC.
- fold i in Hrun,HC; fold t in HP',Hiz.
- rewrite Hz in HP',Hiz; fold i in HP',Hiz.
- apply Request_starts_running with (ra := ra) in HC as H. move: H => /andP [/andP [Hreq HC'] H].
- 4: by apply /eqP.
- 3: exact HP'.
- 2: exact Hrun.
- apply FIFO_l_add_counter with (c := OCycle0) (d := d) in H. destruct H as [Hrun' HC''].
- 3: by apply /eqP.
- 2: rewrite /OCycle0 add0n; exact Hd.
- rewrite /OCycle0 add0n in HC''.
- apply Request_running_in_slot with (d := d) in Hreq as H.
- 3: exact Hd.
- 2: exact HC'.
- set S' := (Default_arbitrate ((t + i).+1 + d)).(Implementation_State); simpl.
- by fold S' in HC'',H; rewrite H; rewrite HC'' eq_refl.
- Qed.
-
- Lemma Request_CAS ta ra:
- ra \in (Arrival_at ta)
- -> let tc := (Requestor_slot_start ta + (index ra (FIFO_pending (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State)) * WAIT) + CAS_date).+1 in
- (CAS_of_req ra tc.+1) \in (Default_arbitrate tc.+1).(Arbiter_Commands).
- Proof.
- intros HA.
- apply Request_processing with (d := CAS_date) in HA as H.
- 2: exact WAIT_CAS.
- move: H => /andP [HC HR]; clear HA.
- rewrite addSn in HC, HR; set (tc := _ + CAS_date); fold tc in HC, HR.
- destruct (Default_arbitrate tc.+1).(Implementation_State) eqn:Hs; simpl.
- { by rewrite /FIFO_request in HR. }
- simpl in Hs; rewrite Hs.
- rewrite /Next_state.
- rewrite /FIFO_counter in HC.
- assert ((nat_of_ord c == ACT_date) = false) as Hact.
- { move: HC => /eqP HC. by rewrite HC CAS_neq_ACT. }
- rewrite //= Hact HC //= /CAS_of_req in_cons; apply /orP; left.
- rewrite /FIFO_request inj_eq in HR. move: HR => /eqP HR.
- 2: exact ssrfun.Some_inj.
- by rewrite HR.
- Qed.
-
- Lemma Counter_at_running_slot_start ta c:
- FIFO_counter (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) == c ->
- isRUNNING (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) ->
- c == WAIT.-1.
- Proof.
- intros Hc Hrun.
- unfold Requestor_slot_start in *.
- destruct (Default_arbitrate ta).(Implementation_State) eqn:Hs.
- { by rewrite Hs in Hrun. }
- { clear Hrun.
- assert (isRUNNING (Default_arbitrate ta).(Implementation_State)) as H.
- { by rewrite Hs. }
- assert (c0 + (WAIT.-1 - c0) = WAIT.-1).
- { rewrite subnKC. reflexivity. destruct c0; simpl in *; clear Hs; by apply nat_ltn_leq_pred in i. }
- apply FIFO_l_add_counter with (c := c0) (d := (WAIT.-1 - c0)) in H as [Hrun Hc'].
- 3: by rewrite Hs.
- 2: rewrite H0; rewrite ltn_predL; exact WAIT_pos.
- rewrite H0 in Hc'; by rewrite Hc' eq_sym in Hc.
- }
- Qed.
-
- Lemma Request_PRE ta ra:
- ra \in (Arrival_at ta)
- -> let i := index ra (FIFO_pending (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State)) * WAIT in
- let tc := ((Requestor_slot_start ta) + i).+1 in
- (PRE_of_req ra tc) \in (Default_arbitrate tc).(Arbiter_Commands).
- Proof.
- intros HA.
-
- apply Request_processing_starts in HA as HP; move: HP => /andP [HP HI].
- set i := index _ _; fold i in HP,HI.
- set t := Requestor_slot_start ta + i * WAIT; fold t in HP,HI.
-
- destruct i eqn:Hz. (* Case i = 0 *)
- { rewrite mul0n //= addn0; subst t.
- rewrite mul0n addn0 in HP,HI.
- rewrite /Next_state.
- destruct (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) eqn:Hs.
- { rewrite /FIFO_pending in HP,HI.
- destruct r eqn:HPP.
- { discriminate HP. }
- { destruct (ra == r0) eqn:Heq.
- { simpl; move: Heq => /eqP Heq; rewrite /PRE_of_req in_cons Heq; apply /orP; left; by rewrite eq_refl. }
- { rewrite eq_sym in Heq; by rewrite //= Heq in HI. }}}
- { rewrite /FIFO_pending in HP,HI.
- assert (FIFO_counter (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State) == c).
- { by rewrite Hs. }
- apply Counter_at_running_slot_start in H.
- 2: by rewrite Hs.
- move: H => /eqP H; rewrite H FIFO_wait_neq_act FIFO_wait_neq_cas eq_refl.
- destruct r eqn:HPP.
- { discriminate HP. }
- { destruct (r1 == ra) eqn:Heq.
- { simpl; move: Heq => /eqP Heq; rewrite /PRE_of_req in_cons Heq; apply /orP; left; by rewrite eq_refl. }
- { by rewrite //= Heq in HI. }}}}
-
- apply Pending_on_arrival in HA as H.
- apply Pending_requestor_slot_start with (tb := Requestor_slot_start ta) in H.
- 3: by rewrite leqnn.
- 2: { rewrite /Requestor_slot_start; destruct (Default_arbitrate ta).(Implementation_State).
- by rewrite leqnn. by rewrite leq_addr. }
- apply Counter_reaches with (i := i) in H. move: H => /andP [Hrun HC]; fold t in Hrun,HC.
- 3: subst i; by rewrite leqnn.
- 2: by rewrite Hz.
-
- simpl; fold t; rewrite /Next_state.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
- { destruct r eqn:HPP.
- { simpl in HP; discriminate HP. }
- { destruct (r0 == ra) eqn:Heq.
- { by simpl; move: Heq => /eqP Heq; rewrite in_cons /PRE_of_req //= Heq eq_refl orTb. }
- { by rewrite /FIFO_pending //= Heq in HI. }
- }}
- { unfold FIFO_pending in HP,HI. subst t; rewrite -Hz in Hs; rewrite Hs /FIFO_counter in HC; move: HC => /eqP HC.
- rewrite HC FIFO_wait_neq_act FIFO_wait_neq_cas eq_refl.
- destruct r eqn:HPP.
- { discriminate HP. }
- { destruct (r1 == ra) eqn:Heq.
- { simpl; move: Heq => /eqP Heq; by rewrite in_cons /PRE_of_req //= Heq eq_refl orTb. }
- { by rewrite /FIFO_pending //= Heq in HI. }
- }
- }
- Qed.
-
- Theorem Requests_handled ta ra:
- ra \in (Arrival_at ta)
- -> exists tc, (CAS_of_req ra tc) \in ((Default_arbitrate tc).(Arbiter_Commands)).
- Proof.
- intros HA.
- apply Request_CAS in HA as H.
- set tc := _.+1 in H.
- exists (tc.+1).
- exact H.
- Qed.
-
- (* ------------------------------------------------------------------ *)
- (* -------------------- PROTOCOL PROOFS ----------------------------- *)
- (* ------------------------------------------------------------------ *)
-
- Lemma Command_from_request_matches cmd t c reqlist r0:
- ~ isNOP cmd -> cmd \in (Default_arbitrate t).(Arbiter_Commands) ->
- (Default_arbitrate cmd.(CDate)).(Implementation_State) = RUNNING c reqlist r0 ->
- cmd.(Request) = r0.
- Proof.
- intros nop H Hrun.
- induction t.
- { simpl in H; discriminate H. }
- { simpl in H; rewrite /Next_state in H.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
- { destruct r eqn:Hp; simpl in H.
- { rewrite in_cons in H; move: H => /orP [/eqP H | H].
- { rewrite H //= /Next_state Hs //= in Hrun. }
- { by apply IHt in H. }}
- { rewrite in_cons in H; move: H => /orP [/eqP H | H].
- { rewrite H //= /Next_state Hs //= eq_refl in Hrun.
- injection Hrun as _ _ Hreq; rewrite H //=.
- }
- { by apply IHt in H. }}}
- { simpl in H.
- destruct (nat_of_ord c0 == ACT_date) eqn:Hact, (nat_of_ord c0 == CAS_date) eqn:Hcas, (nat_of_ord c0 == WAIT.-1) eqn:Hwait; simpl in H.
- 7: {
- destruct r eqn:HPP; simpl in H.
- { rewrite in_cons in H; move: H => /orP [/eqP H | H].
- { rewrite H //= /Next_state Hs //= Hact Hcas Hwait //= in Hrun. }
- { by apply IHt in H. }}
- { rewrite in_cons in H; move: H => /orP [/eqP H | H].
- { rewrite H //= /Next_state Hs //= Hact Hcas Hwait //= eq_refl in Hrun.
- injection Hrun as _ _ Hreq; rewrite H //=. }
- { by apply IHt in H. }}
- }
- all: rewrite in_cons in H; move: H => /orP [/eqP H | H].
- all: try by apply IHt in H.
- all: try (rewrite H //= /Next_state Hs //= Hact //= in Hrun; injection Hrun as _ _ Hreq; rewrite H //=).
- all: try (rewrite H //= /Next_state Hs //= Hact Hcas //= in Hrun; injection Hrun as _ _ Hreq; rewrite H //=).
- rewrite H /isNOP //= in nop.
- }
- }
- Qed.
-
- Lemma Pending_arrived t:
- forall r, r \in FIFO_pending (Default_arbitrate t).(Implementation_State) ->
- exists t', r \in Arrival_at t'.
- Proof.
- intros r HP.
- induction t.
- { simpl in HP. exists (0). exact HP. }
- { simpl in HP; rewrite /Next_state in HP.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
- { destruct r0 eqn:HPP; simpl in HP.
- { exists(t.+1); exact HP. }
- { rewrite eq_refl /Enqueue mem_cat in HP; move: HP => /orP [HP | HP].
- simpl in IHt; rewrite in_cons HP orbT in IHt. by apply IHt.
- exists(t.+1); exact HP.
- }}
- { simpl in HP.
- destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl in HP.
- all: try (rewrite /Enqueue mem_cat in HP; move: HP => /orP [HP | HP]).
- all: try (simpl in IHt; by apply IHt in HP as IH).
- all: try (exists(t.+1); exact HP).
- destruct (r0) eqn:HPP; simpl in HP.
- 2: {
- rewrite eq_refl /Enqueue mem_cat in HP; move: HP => /orP [HP | HP].
- simpl in IHt; rewrite in_cons HP orbT in IHt. by apply IHt.
- exists(t.+1); exact HP.
- }
- exists(t.+1); exact HP.
- }
- }
- Qed.
-
- Lemma Was_in_pending_queue t ra:
- isRUNNING (Default_arbitrate t).(Implementation_State) ->
- FIFO_request (Default_arbitrate t).(Implementation_State) == Some ra ->
- exists t', ra \in FIFO_pending (Default_arbitrate t').(Implementation_State).
- Proof.
- intros Hrun Hreq.
- induction t.
- { by simpl in Hrun. }
- { simpl in Hrun,Hreq; rewrite /Next_state in Hrun Hreq.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
- { destruct r eqn:HP; simpl in Hrun, Hreq.
- { done. }
- { rewrite inj_eq in Hreq. move: Hreq => /eqP Hreq.
- 2: exact ssrfun.Some_inj.
- exists (t); rewrite Hs -Hreq /FIFO_pending; by apply mem_head. }}
- { simpl in Hrun,Hreq.
- destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl in Hrun,Hreq.
- 7: {
- destruct r eqn:Hp; simpl in Hrun,Hreq.
- 1: done.
- rewrite inj_eq in Hreq. move: Hreq => /eqP Hreq.
- 2: exact ssrfun.Some_inj.
- exists (t); rewrite Hs -Hreq /FIFO_pending; by apply mem_head.
- }
- all: simpl in IHt; by apply IHt.
- }
- }
- Qed.
-
- Lemma Running_arrived t ra:
- isRUNNING (Default_arbitrate t).(Implementation_State) ->
- (FIFO_request (Default_arbitrate t).(Implementation_State)) == Some ra ->
- exists t', ra \in (Arrival_at t').
- Proof.
- intros Hrun Hreq.
- apply Was_in_pending_queue with (ra := ra) in Hrun as [ta HP].
- 2: done.
- by apply Pending_arrived in HP as H.
- Qed.
-
- Lemma Cmd_in_trace cmd t:
- cmd \in (Default_arbitrate t).(Arbiter_Commands) ->
- cmd.(CDate) <= t.
- Admitted.
-
- Lemma l0 t1 t2:
- (Default_arbitrate t1).(Implementation_State) =
- (Default_arbitrate t2).(Implementation_State) ->
- t1 = t2.
- Admitted.
-
- (* got to have some lemma that states *)
- Lemma laux t r P :
- FIFO_request (Default_arbitrate t).(Implementation_State) = Some r ->
- FIFO_pending (Default_arbitrate t).(Implementation_State) = P ->
- FIFO_counter (Default_arbitrate t).(Implementation_State) = OCycle0 ->
- FIFO_pending (Default_arbitrate t.-1).(Implementation_State) = r :: P.
- Admitted.
-
- Lemma l1 t' P ra ta :
- let t := Requestor_slot_start ta in
- let S := (Default_arbitrate t).(Implementation_State) in
- let i := index ra (FIFO_pending S) in
- let tc := t + i * WAIT in
- ra \in Arrival_at ta ->
- FIFO_pending (Default_arbitrate tc).(Implementation_State) = ra :: P ->
- FIFO_request (Default_arbitrate t').(Implementation_State) = Some ra ->
- FIFO_counter (Default_arbitrate t').(Implementation_State) = OCycle0 ->
- FIFO_pending (Default_arbitrate t').(Implementation_State) = Enqueue (Arrival_at tc.+1) P.
- Proof.
- intros t S i tc HA Hp_tc HR_t' HC_t'.
-
- apply Request_processing_starts in HA; move: HA => /andP [HP_tc HI_tc]; fold t S i tc in HP_tc,HI_tc.
-
- destruct (Default_arbitrate tc).(Implementation_State) eqn:Hs.
- { rewrite -Hs in HI_tc,Hp_tc,HP_tc.
- apply Request_starts_idle_ in HP_tc as H.
- 3: by apply /eqP.
- 2: by rewrite Hs.
- move: H => /andP [/andP [/andP [HR_tcp1 HC_tcp1]Hrun_tcp1]HP_tcp1].
- simpl in *; unfold Next_state in *; rewrite Hs in HP_tcp1,Hrun_tcp1,HC_tcp1,HR_tcp1; simpl in *.
- destruct r eqn:HPP.
- { done. }
- simpl in *.
- rewrite Hs /FIFO_pending in Hp_tc.
- rewrite eq_refl in HP_tcp1.
- admit.
-
- }
- Admitted.
-
- Lemma l2_idle t ra P:
- FIFO_pending (Default_arbitrate t).(Implementation_State) = ra :: P ->
- isIDLE (Default_arbitrate t).(Implementation_State) ->
- FIFO_pending (Default_arbitrate t.+1).(Implementation_State) = Enqueue (Arrival_at t.+1) P.
- Proof.
- intros HP Hidle; simpl; rewrite /Next_state.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
- 2: by discriminate Hidle.
- destruct r eqn:HPP.
- 1: by rewrite /FIFO_pending in HP.
- rewrite //= eq_refl.
- assert (index ra (FIFO_pending (Default_arbitrate t).(Implementation_State)) = 0).
- { rewrite -Hs in HP. rewrite HP //= eq_refl. reflexivity. }
- destruct (r0 == ra) eqn:Heq.
- { move: HP => /eqP HP.
- rewrite /FIFO_pending eqseq_cons Heq in HP; move: HP => /andP [_ /eqP HP].
- by rewrite HP. }
- { by rewrite Hs /FIFO_pending //= Heq in H. }
- Qed.
-
- Lemma l2_running t ra P:
- FIFO_pending (Default_arbitrate t).(Implementation_State) = ra :: P ->
- isRUNNING (Default_arbitrate t).(Implementation_State) ->
- FIFO_counter (Default_arbitrate t).(Implementation_State) = WAIT.-1 ->
- FIFO_pending (Default_arbitrate t.+1).(Implementation_State) = Enqueue (Arrival_at t.+1) P.
- Admitted.
-
- (* FIFO_pending (Default_arbitrate t').(Implementation_State) = P -> *)
- Lemma l3 ra ta t':
- let t := Requestor_slot_start ta in
- let S := (Default_arbitrate t).(Implementation_State) in
- let i := index ra (FIFO_pending S) in
- let tc := t + i * WAIT in
- ra \in Arrival_at ta ->
- FIFO_request (Default_arbitrate t').(Implementation_State) = Some ra ->
- FIFO_counter (Default_arbitrate t').(Implementation_State) = OCycle0 ->
- tc.+1 = t'.
- Proof.
- intros t S i tc HA Hreq' Hc'.
- apply Request_processing_starts in HA as H; move: H => /andP [HP HI]; fold t S i tc in HP,HI.
- destruct (Default_arbitrate tc).(Implementation_State) eqn:Hs.
- { destruct r eqn:HPP.
- { simpl in HP; discriminate HP. }
- { rewrite /FIFO_pending in HP,HI.
-
- apply l1 with (P := r1) (ta := ta) in Hreq' as HP'. fold t S i tc in HP'.
- 4: exact Hc'.
- 3: {
- fold t S i tc; rewrite Hs /FIFO_pending.
- destruct (r0 == ra) eqn:Heq.
- { move: Heq => /eqP Heq; by rewrite Heq. }
- { simpl in HI; by rewrite Heq in HI. }
- }
- 2: exact HA.
- assert (isIDLE (Default_arbitrate tc).(Implementation_State)) as Hidle.
- { by rewrite Hs. }
- apply Request_starts_idle with (ra := ra) in Hidle as HH.
- 3,2: (rewrite Hs /FIFO_pending; (done || by apply /eqP)).
- move: HH => /andP [/andP [Hreq Hc] Hrun].
- apply l2_idle with (ra := ra) (P := r1) in Hidle.
- 2: {
- fold t S i tc; rewrite Hs /FIFO_pending.
- destruct (r0 == ra) eqn:Heq.
- { move: Heq => /eqP Heq; by rewrite Heq. }
- { simpl in HI; by rewrite Heq in HI. }
- }
- assert ((Default_arbitrate t').(Implementation_State) = (Default_arbitrate (tc.+1)).(Implementation_State)).
- { destruct (Default_arbitrate t').(Implementation_State).
- { by rewrite /FIFO_request in Hreq'. }
- move: Hreq' => /eqP Hreq'. rewrite /FIFO_request inj_eq in Hreq'. move: Hreq' => /eqP Hreq'. rewrite Hreq'.
- 2: exact ssrfun.Some_inj.
- move: Hc' => /eqP Hc'. rewrite /FIFO_counter nat_of_counter_eq in Hc'. move: Hc' => /eqP Hc'. rewrite Hc'.
- rewrite /FIFO_pending in HP'. rewrite HP'.
-
- destruct (Default_arbitrate tc.+1).(Implementation_State) eqn:Hss.
- { discriminate Hrun. }
- rewrite /FIFO_request inj_eq in Hreq. move: Hreq => /eqP Hreq. rewrite Hreq.
- 2: exact ssrfun.Some_inj.
- rewrite /FIFO_counter nat_of_counter_eq in Hc. move: Hc => /eqP Hc. rewrite Hc.
- rewrite /FIFO_pending in Hidle. rewrite Hidle.
- reflexivity.
- }
- apply l0 in H. by rewrite H. }}
- { admit. }
- Admitted.
-
- Lemma Requests_starts_before_zero t' ta cmd:
- let t := Requestor_slot_start ta in
- let S := (Default_arbitrate t).(Implementation_State) in
- let i := index cmd.(Request) (FIFO_pending S) in
- let tc := (t + i * WAIT) in
- cmd \in (Default_arbitrate t').(Arbiter_Commands) ->
- FIFO_request (Default_arbitrate cmd.(CDate)).(Implementation_State) == Some cmd.(Request) ->
- FIFO_counter (Default_arbitrate cmd.(CDate)).(Implementation_State) == OCycle0 ->
- cmd.(Request) \in Arrival_at ta ->
- tc.+1 = cmd.(CDate).
- Proof.
- intros t S i tc Hin Hreq Hc HA.
- apply Request_PRE in HA as H.
- rewrite /PRE_of_req in H; fold t S i tc in H.
- apply l3 with (t' := cmd.(CDate)) in HA as HH.
- 3,2: by apply /eqP.
- by fold t S i tc in HH.
- Qed.
-
- Lemma Requests_starts_before t' ta cmd c:
- let t := Requestor_slot_start ta in
- let S := (Default_arbitrate t).(Implementation_State) in
- let i := index cmd.(Request) (FIFO_pending S) in
- let tc := t + i * WAIT in
- cmd \in (Default_arbitrate t').(Arbiter_Commands) ->
- FIFO_request (Default_arbitrate cmd.(CDate)).(Implementation_State) == Some cmd.(Request) ->
- FIFO_counter (Default_arbitrate cmd.(CDate)).(Implementation_State) == c ->
- cmd.(Request) \in Arrival_at ta ->
- tc.+1 + c = cmd.(CDate).
- Proof.
- intros t S i tc Hin Hreq Hc HA.
- apply Request_PRE in HA as H; fold t S i tc in H.
- (* got to have an alternate version of l3 that works with a counter value *)
- Admitted.
-
- Lemma Cmds_ACT_ok a b t:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- isACT a \/ isCAS a -> isACT b -> Same_Bank a b -> Before a b ->
- exists c, (c \in (Default_arbitrate t).(Arbiter_Commands)) && isPRE c && Same_Bank b c && Same_Bank a c && ~~ Before_at c a && Before c b.
- Proof.
- intros Ha Hb iA iAb SB aBb.
- destruct iA as [iAa | iCa].
- { apply FIFO_ACT_date in Ha as H. destruct H as [Hca [Hrun_a Hreq_a]].
- apply FIFO_ACT_date in Hb as H. destruct H as [Hcb [Hrun_b Hreq_b]].
- all: try done.
- destruct (Default_arbitrate b.(CDate)).(Implementation_State) eqn:Hsb.
- 1: by simpl in Hrun_b.
-
- rewrite -Hsb in Hreq_b. apply Running_arrived in Hreq_b as HH. destruct HH as [ta H].
- 2: by rewrite Hsb.
-
- apply Request_PRE in H as Hpre.
- set i := index b.(Request) (FIFO_pending (Default_arbitrate (Requestor_slot_start ta)).(Implementation_State)); fold i in Hpre.
- set tc := (Requestor_slot_start ta + i * WAIT).+1; fold tc in Hpre.
-
- exists (mkCmd tc PRE b.(Request)).
- rewrite /Same_Bank in SB; move: SB => /eqP SB.
- rewrite /isPRE /Same_Bank //= eq_refl andbT SB eq_refl andbT andbT /Before /Before_at //= -ltnNge.
-
- (* apply Request_ACT in H as Hact. *)
-
- (* apply Requests_starts_before_zero with (ta := ta) in Hb. *)
-
- apply Requests_starts_before with (ta := ta) (c := Next_cycle OACT_date) in Hb as Hlt.
- 4: exact H.
- 3: rewrite -Hsb in Hcb; by rewrite Hcb.
- 2: exact Hreq_b.
- fold i tc in Hlt.
-
- rewrite {2 3}Hlt.
- apply /andP; split.
- 2: {
- rewrite ltn_subrL; apply FIFO_date_gt_0 in Hb.
- rewrite Hb FIFO_nextcycle_act_eq_actS /ACT_date prednK.
- rewrite andbT.
- all: by rewrite lt0n T_RP_pos.
- }
- apply /andP; split.
- 2: {
- apply FIFO_l_eq_bound with (ta := a.(CDate)) (c := Next_cycle OACT_date) in Hrun_b.
- all: try (done || by rewrite -Hsb in Hcb).
- rewrite ltn_subRL addnC.
- rewrite leq_eqVlt in Hrun_b; move: Hrun_b => /orP [/eqP Hrun_b | Hrun_b].
- { by rewrite -Hrun_b ltn_add2l FIFO_nextcycle_act_eq_actS FIFO_WAIT_GT_ACTp1. }
- { apply ltn_trans with (n := a.(CDate) + WAIT).
- 2: exact Hrun_b.
- by rewrite ltn_add2l FIFO_nextcycle_act_eq_actS FIFO_WAIT_GT_ACTp1.
- }
- }
-
- apply FIFO_in_the_past with (t := b.(CDate)).
- { by apply Cmd_in_trace in Hb. }
- apply FIFO_in_the_past with (t := tc).
- { by rewrite Hlt leq_subr. }
- by rewrite /PRE_of_req in Hpre; fold tc in Hpre.
- }
- Admitted.
-
- Lemma FIFO_idle_to_running t c r:
- (Default_arbitrate t).(Implementation_State) = IDLE c r ->
- isRUNNING (Default_arbitrate t.+1).(Implementation_State) ->
- r != [::].
- Proof.
- intros.
- simpl in H0; rewrite /Next_state //= H in H0.
- destruct r eqn:HP; simpl.
- 2: done.
- discriminate H0.
- Qed.
-
- Lemma FIFO_running_before t c d:
- isRUNNING (Default_arbitrate t).(Implementation_State) ->
- FIFO_counter (Default_arbitrate t).(Implementation_State) = c ->
- c >= d -> isRUNNING (Default_arbitrate (t - d)).(Implementation_State).
- Proof.
- intros.
- induction d.
- Admitted.
-
- Lemma FIFO_issues_pre a t:
- let pre := mkCmd (a.(CDate) - T_RP) PRE a.(Request) in
- a \in (Default_arbitrate t).(Arbiter_Commands) -> isACT a ->
- pre \in (Default_arbitrate t).(Arbiter_Commands).
- Proof.
- intros pre Ha iAa.
- apply FIFO_ACT_date in Ha as H'. destruct H' as [Hc_a Hrun_a].
- 2: exact iAa.
- apply FIFO_in_the_past with (t := (a.(CDate) - T_RP).-1.+1).
- 1: admit.
- simpl; rewrite /Next_state //=.
- destruct (Default_arbitrate (a.(CDate) - T_RP).-1).(Implementation_State) eqn:Hs; simpl.
- { destruct r eqn:HP; simpl.
- { apply FIFO_running_before with (c := Next_cycle OACT_date) (d := T_RP) in Hrun_a as Hrun_a'.
- 3: { rewrite /Next_cycle /OACT_date //= FIFO_nextcycle_act_eq_actS /ACT_date prednK.
- by rewrite leqnn.
- rewrite lt0n; exact T_RP_pos.
- }
- 2: exact Hc_a.
- apply FIFO_idle_to_running in Hs.
- 2: admit.
- discriminate Hs.
- }
- rewrite in_cons; apply /orP; left; subst pre; rewrite prednK.
- 2: admit.
- admit. (* should be trivial *)
- }
- destruct (nat_of_ord c == ACT_date) eqn:Hact, (nat_of_ord c == CAS_date) eqn:Hcas, (nat_of_ord c == WAIT.-1) eqn:Hwait; simpl.
- (* if I'm running at the next cycle (need run_before) with counter equal to 0, then the counter here should be WAIT .-1 *)
- 7: destruct r.
- all: simpl.
- 7: { (* there should be a request in the queue, contradict that *) admit. }
- Admitted.
-
- Lemma Cmds_ACT_ok a b t:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- isACT a \/ isCAS a -> isACT b -> Same_Bank a b -> Before a b ->
- exists c, (c \in (Default_arbitrate t).(Arbiter_Commands) /\ isPRE c /\ Same_Bank a c /\ Before c b /\ ~ Before_at c a).
- Proof.
- intros Ha Hb iA iB SB aBb.
- destruct iA as [iAa | iCa].
- { apply FIFO_ACT_date in Ha as H'. destruct H' as [Hc_a Hrun_a].
- 2: exact iAa.
- assert (Next_cycle OACT_date + (WAIT.-1 - ACT_date.+1) = WAIT.-1).
- { rewrite FIFO_nextcycle_act_eq_actS subnKC. 2: admit. 1: done. }
- apply FIFO_l_add_counter with (c := Next_cycle OACT_date) (d := WAIT.-1 - ACT_date.+1) in Hrun_a as [Hrun_a' Hc_a'].
- 3: exact Hc_a.
- 2: by rewrite H ltn_predL WAIT_pos.
- rewrite H in Hc_a'.
- apply FIFO_l_counter_border in Hc_a' as Hc_a''.
- 2: exact Hrun_a'.
- destruct (Default_arbitrate (a.(CDate) + (WAIT.-1 - ACT_date.+1)).+1).(Implementation_State) eqn:Hs.
- { admit. }
- { }
-
- (* ------------------------------------------------------------------ *)
- (* --------------------- REQUEST PROOFS ----------------------------- *)
- (* ------------------------------------------------------------------ *)
-
- Obligation Tactic := simpl.
- Program Definition FIFO_arbitrate t :=
- mkTrace (Default_arbitrate t).(Arbiter_Commands) (Default_arbitrate t).(Arbiter_Time)
- (Default_arbitrate_cmds_uniq t) (Default_arbitrate_cmds_date t)
- (Cmds_T_RRD_ok t) (Cmds_T_FAW_ok t) _ (Cmds_T_RP_ok t) _ _ (Cmds_T_RTP_ok t) _ _ _ _ _ _ _.
- Admit Obligations.
-
- Global Program Instance FIFO_arbiter : Arbiter_t :=
- mkArbiter AF FIFO_arbitrate _ _.
- Admit Obligations.
-
-End FIFO.
-
-Section Test.
- Program Instance BANK_CFG : Bank_configuration :=
- {
- BANKS := 1;
-
- T_BURST := 1;
- T_WL := 1;
-
- T_RRD := 3;
- T_FAW := 20;
-
- T_RC := 3;
- T_RP := 4;
- T_RCD := 2;
- T_RAS := 4;
- T_RTP := 4;
- T_WR := 1;
-
- T_RTW := 10;
- T_WTR := 10;
- T_CCD := 12;
- }.
-
- Program Instance FIFO_CFG : FIFO_configuration :=
- {
- WAIT := 10
- }.
-
- Instance REQESTOR_CFG : Requestor_configuration :=
- {
- Requestor_t := unit_eqType
- }.
-
- Program Definition Req1 := mkReq tt 1 RD 0 1 0.
- Program Definition Req2 := mkReq tt 2 RD 0 1 0.
-
- Definition Input : Requests_t := [:: Req2; Req1].
-
- Program Instance AF : Arrival_function_t := Default_arrival_function_t Input.
-End Test.
\ No newline at end of file
diff --git a/framework/DDR4/Requestor.v b/framework/DDR4/Requestor.v
deleted file mode 100644
index f983405cc3f799b65678025290c9e7977bbc101d..0000000000000000000000000000000000000000
--- a/framework/DDR4/Requestor.v
+++ /dev/null
@@ -1,6 +0,0 @@
-From mathcomp Require Export ssreflect eqtype.
-
-Class Requestor_configuration :=
-{
- Requestor_t : eqType;
-}.
\ No newline at end of file
diff --git a/framework/DDR4/Requests.v b/framework/DDR4/Requests.v
deleted file mode 100644
index 4aec13d7d1ecd94aee0b66a6155005865a50e0f0..0000000000000000000000000000000000000000
--- a/framework/DDR4/Requests.v
+++ /dev/null
@@ -1,87 +0,0 @@
-Set Warnings "-notation-overridden,-parsing".
-Set Printing Projections.
-From mathcomp Require Export ssreflect eqtype.
-Set Printing Projections.
-From DDR4 Require Export Util System Requestor Bank.
-
-Section Requests.
-
- Context {REQESTOR_CFG : Requestor_configuration}.
- Context {ARBITER_CFG : Arbiter_configuration}.
- Context {SYS_CFG : System_configuration}.
-
- Inductive Request_kind_t : Set :=
- RD |
- WR.
-
- Local Definition Request_kind_eqdef (a b : Request_kind_t) :=
- match a, b with
- | RD, RD
- | WR, WR => true
- | _, _ => false
- end.
-
- Lemma Request_kind_eqn : Equality.axiom Request_kind_eqdef.
- 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.
- Qed.
-
- Canonical Request_kind_eqMixin := EqMixin Request_kind_eqn.
- Canonical Request_kind_eqType:= Eval hnf in EqType Request_kind_t Request_kind_eqMixin.
-
- Record Request_t := mkReq
- {
- Requestor : Requestor_t;
- Date : nat;
- Kind : Request_kind_t;
- Bankgroup : Bankgroup_t;
- Bank : Bank_t;
- Row : Row_t
- }.
-
- Local Definition Request_eqdef (a b : Request_t) :=
- (a.(Requestor) == b.(Requestor)) &&
- (a.(Date) == b.(Date)) &&
- (a.(Kind) == b.(Kind)) &&
- (a.(Bankgroup) == b.(Bankgroup)) &&
- (a.(Bank) == b.(Bank)) &&
- (a.(Row) == b.(Row)).
-
- Lemma Request_eqn : Equality.axiom Request_eqdef.
- Proof.
- unfold Equality.axiom. intros. destruct Request_eqdef eqn:H.
- {
- apply ReflectT. unfold Request_eqdef in *.
- move: H => /andP [/andP [/andP [/andP [ /andP [/eqP RQ /eqP Hdate /eqP Hkind /eqP Bg /eqP B /eqP R]]]]].
- destruct x,y; simpl in *. by subst.
- }
- apply ReflectF. unfold Request_eqdef, not in *.
- intro BUG.
- apply negbT in H. rewrite negb_and in H.
- destruct x, y.
- move: H => /orP [H | /eqP Row].
- rewrite negb_and in H.
- move: H => /orP [H | /eqP Bank].
- rewrite negb_and in H.
- move: H => /orP [H | /eqP Bg].
- rewrite negb_and in H.
- move: H => /orP [H | /eqP Kind].
- rewrite negb_and in H.
- move: H => /orP [/eqP Req | /eqP Date].
- by apply Req; inversion BUG.
- by apply Date; inversion BUG.
- by apply Kind; inversion BUG.
- by apply Bg; inversion BUG.
- by apply Bank; inversion BUG.
- by apply Row; inversion BUG.
- Qed.
-
- Canonical Request_eqMixin := EqMixin Request_eqn.
- Canonical Request_eqType := Eval hnf in EqType Request_t Request_eqMixin.
-
- Definition Requests_t := seq Request_t.
-End Requests.
-
diff --git a/framework/DDR4/System.v b/framework/DDR4/System.v
deleted file mode 100644
index c60be2461d46e624e1d381d9db94d6c4a4c369bb..0000000000000000000000000000000000000000
--- a/framework/DDR4/System.v
+++ /dev/null
@@ -1,54 +0,0 @@
-Set Warnings "-notation-overridden,-parsing".
-Set Printing Projections.
-From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
-
-Section System.
-
-(* The arbiter state *)
-Class Arbiter_configuration :=
-{
- State_t : Type;
-}.
-
-(* The system *)
-Class System_configuration :=
-{
- BANKS : nat;
-
- T_BURST : nat; (* delay of a burst transfer RD/WR *)
- T_WL : nat; (* delay between a WR and its bus transfer *)
-
- T_RRD : nat; (* ACT to ACT delay inter-bank *)
- T_FAW : nat; (* Four ACT window inter-bank *)
-
- T_RC : nat; (* ACT to ACT delay intra-bank *)
- T_RP : nat; (* PRE to ACT delay intra-bank *)
- T_RCD : nat; (* ACT to CAS delay intra-bank *)
- T_RAS : nat; (* ACT to PRE delay intra-bank *)
- T_RTP : nat; (* RD to PRE delay intra-bank *)
- T_WR : nat; (* WR end to PRE delay intra-bank *)
-
- T_RTW : nat; (* RD to WR delay intra- + inter-bank *)
- T_WTR : nat; (* WR to RD delay intra- + inter-bank *)
- T_CCD : nat; (* RD/WR to RD/WR delay intra- + inter-bank *)
-
- (* POs *)
-
- BANKS_pos : BANKS != 0;
-
- T_RRD_pos : T_RRD != 0;
- T_FAW_pos : T_FAW != 0;
-
- T_RC_pos : T_RC != 0;
- T_RP_pos : T_RP != 0;
- T_RCD_pos : T_RCD != 0;
- T_RAS_pos : T_RAS != 0;
- T_RTP_pos : T_RTP != 0;
- T_WR_pos : T_WR != 0;
-
- T_RTW_pos : T_RTW != 0;
- T_WTR_pos : T_WTR != 0;
- T_CCD_pos : T_CCD != 0
-}.
-
-End System.
\ No newline at end of file
diff --git a/framework/DDR4/TDM.v b/framework/DDR4/TDM.v
deleted file mode 100644
index cfb3036cd3694e6281985e7315eb75e79ffd3df6..0000000000000000000000000000000000000000
--- a/framework/DDR4/TDM.v
+++ /dev/null
@@ -1,1510 +0,0 @@
-Set Warnings "-notation-overridden,-parsing".
-Set Printing Projections.
-From sdram Require Export Arbiter Requests.
-From mathcomp Require Export fintype div.
-Require Import Program.
-(* Require Import Coq.Logic.Classical_Pred_Type. *)
-
-Section TDM.
- Context {BANK_CFG : Bank_configuration}.
-
- Local Definition ACT_date := T_RP.+1.
- Local Definition CAS_date := ACT_date + T_RCD.+1.
-
- Class TDM_configuration :=
- {
- SL : nat;
- SN : nat;
-
- SN_pos : 0 < SN;
- SN_one : 1 < SN;
- SL_pos : 0 < SL;
- SL_ACT : ACT_date < SL;
- SL_CASS : CAS_date.+1 < SL;
-
- T_RRD_SL : T_RRD < SL;
- T_FAW_3SL : T_FAW < SL + SL + SL
- }.
-
- Context {TDM_CFG : TDM_configuration}.
-
- Lemma Last_cycle:
- SL.-1 < SL.
- Proof.
- rewrite ltn_predL. apply SL_pos.
- Qed.
-
- Lemma SL_CAS:
- CAS_date < SL.
- Proof.
- specialize SL_CASS as H.
- apply ltn_trans with (m := CAS_date) in H.
- - exact H.
- - apply ltnSn.
- Qed.
-
- Lemma SL_one:
- 1 < SL.
- Proof.
- specialize SL_CAS as H.
- unfold CAS_date, ACT_date in H.
- apply ltn_trans with (m := 1) in H.
- - exact H. clear H.
- - rewrite ltn_addr.
- - trivial.
- - rewrite ltnS.
- specialize T_RP_pos as H.
- by rewrite <- lt0n in H.
- Qed.
-
- Lemma CAS_pos:
- 0 < CAS_date.
- Proof.
- unfold CAS_date, ACT_date.
- rewrite addn_gt0. apply /orP. left.
- apply ltn0Sn.
- Qed.
-
- Lemma SL_ACTS:
- ACT_date.+1 < SL.
- Proof.
- specialize SL_CAS as H.
- unfold CAS_date, ACT_date in *.
- apply ltn_trans with (m := T_RP.+2) in H.
- - exact H.
- - rewrite <- (addn1 T_RP.+1), ltn_add2l, ltnS, lt0n.
- exact T_RCD_pos.
- Qed.
-
- Lemma ACT_pos:
- 0 < ACT_date.
- Proof.
- by rewrite /ACT_date -[T_RP.+1]addn1 addn_gt0 ltn0Sn orbT.
- Qed.
-
- Local Definition OZCycle := Ordinal SL_pos.
- Local Definition OACT_date := Ordinal SL_ACT.
- Local Definition OCAS_date := Ordinal SL_CAS.
- Local Definition OLastCycle := Ordinal Last_cycle.
-
- Local Definition OZSlot := Ordinal SN_pos.
-
- Definition Slot_t :=
- ordinal_eqType SN.
-
- Instance REQESTOR_CFG : Requestor_configuration :=
- {
- Requestor_t := Slot_t
- }.
-
- Context {AF : Arrival_function_t}.
-
- Definition Counter_t := ordinal SL.
-
- (* Track whether a request is processed (RUNNING) or not (IDLE), the owner of
- the current slot, the cycle offset within the slot, as well as the set of
- pending requests. *)
- Variant TDM_state_t :=
- | IDLE : Slot_t -> Counter_t -> Requests_t -> TDM_state_t
- | RUNNING : Slot_t -> Counter_t -> Requests_t -> Request_t-> TDM_state_t.
-
- Local Definition TDM_state_eqdef (a b : TDM_state_t) :=
- match a, b with
- | IDLE sa ca Pa, IDLE sb cb Pb => (sa == sb) && (ca == cb) && (Pa == Pb)
- | RUNNING sa ca Pa ra, IDLE sb cb Pb => false
- | IDLE sa ca Pa, RUNNING sb cb Pb rb => false
- | RUNNING sa ca Pa ra, RUNNING sb cb Pb rb => (sa == sb) && (ca == cb) && (Pa == Pb) && (ra == rb)
- end.
-
- Lemma TDM_state_eqn : Equality.axiom TDM_state_eqdef.
- Proof.
- unfold Equality.axiom. intros. destruct TDM_state_eqdef eqn:H; unfold TDM_state_eqdef in *.
- {
- destruct x, y; apply ReflectT;
- try (contradict H; discriminate).
- 1: move: H => /andP [/andP [/eqP S /eqP C /eqP P]].
- 2: move: H => /andP [/andP [/andP [/eqP S /eqP C /eqP P /eqP R]]].
- all: subst; reflexivity.
- }
- destruct x, y; apply negbT in H; apply ReflectF;
- try discriminate.
-
- all: unfold not; intro BUG.
- 1: rewrite 2! negb_and in H.
- 2: rewrite 3! negb_and in H.
- 2: move: H => /orP [H | /eqP R].
- 1,2: move: H => /orP [H | /eqP P].
- 1,3: move: H => /orP [/eqP S | /eqP C].
- all: try (by apply S; inversion BUG).
- all: try (by apply C; inversion BUG).
- all: try (by apply P; inversion BUG).
- all: try (by apply R; inversion BUG).
- Qed.
-
- Canonical TDM_state_eqMixin := EqMixin TDM_state_eqn.
- Canonical TDM_state_eqType := Eval hnf in EqType TDM_state_t TDM_state_eqMixin.
-
- Global Instance ARBITER_CFG : Arbiter_configuration :=
- {
- State_t := TDM_state_t;
- }.
-
- (*************************************************************************************************)
- (** ARBITER IMPLEMENTATION ***********************************************************************)
- (*************************************************************************************************)
-
- (* Increment counter for cycle offset (with wrap-arround). *)
- Definition Next_cycle (c : Counter_t) :=
- let nextc := c.+1 < SL in
- (if nextc as X return (nextc = X -> Counter_t) then
- fun (P : nextc = true) => Ordinal (P : nextc)
- else
- fun _ => OZCycle) Logic.eq_refl.
-
- (* Increment the slot counter (with wrap-arround) *)
- Local Definition Next_slot (s : Slot_t) (c : Counter_t) : Slot_t :=
- if (c.+1 < SL) then
- s
- else
- let nexts := s.+1 < SN in
- (if nexts as X return (nexts = X -> Slot_t) then
- fun (P : nexts = true) => Ordinal (P : nexts)
- else
- fun _ => OZSlot) Logic.eq_refl.
-
- (* Enqueue newly arriving requests in the pending queue. *)
- Local Definition Enqueue (R P : Requests_t) :=
- P ++ R.
-
- (* Remove a request from the pending queue that is about to be processed. *)
- Local Definition Dequeue r (P : Requests_t) :=
- rem r P.
-
- (* The set of pending requests of a slot *)
- Local Definition Pending_of s (P : Requests_t) :=
- [seq r <- P | r.(Requestor) == s].
-
- Local Definition Init_state R :=
- IDLE OZSlot OZCycle (Enqueue R [::]).
-
- Local Hint Unfold PRE_of_req : core.
- Local Hint Unfold ACT_of_req : core.
- Local Hint Unfold CAS_of_req : core.
-
- Axiom ACommand_t : Command_t.
-
- Local Definition nullreq :=
- mkReq OZSlot 0 RD 0 (Nat_to_bank 0) 0.
-
- (* The next-state function of the arbiter *)
- Local Definition Next_state R (AS : TDM_state_t) : (TDM_state_t * (Command_kind_t * Request_t)) :=
- match AS return (TDM_state_t * (Command_kind_t * Request_t)) with
- | IDLE s c P => (* Currently no request is processed *)
- let P' := Enqueue R P in (* enqueue newly arriving requests *)
- let s' := Next_slot s c in (* advance slot counter (if needed) *)
- let c' := Next_cycle c in (* advance slot counter (if needed) *)
- if (c == OZCycle) then
- match Pending_of s P with (* Check if a request is pending *)
- | [::] => (* No? Continue with IDLE *)
- (IDLE s' c' P', (NOP, nullreq))
- | r::_ => (* Yes? Emit PRE, dequeue request, and continue with RUNNING *)
- (RUNNING s' c' (Enqueue R (Dequeue r P)) r, (PRE,r))
- end
- else (IDLE s' c' P', (NOP, nullreq))
- | RUNNING s c P r => (* Currently a request is processed *)
- let P' := Enqueue R P in (* enqueue newly arriving requests *)
- let s' := Next_slot s c in (* advance slot counter (if needed) *)
- let c' := Next_cycle c in (* advance slot counter (if needed) *)
- if c == OACT_date then (* need to emit the ACT command *)
- (RUNNING s' c' P' r, (ACT, r))
- else if c == OCAS_date then (* need to emit the CAS command *)
- (RUNNING s' c' P' r, (Kind_of_req r, r))
- else if c == OLastCycle then (* return to IDLE state *)
- (IDLE s' c' P', (NOP, nullreq))
- else
- (RUNNING s' c' P' r, (NOP, nullreq))
- end.
-
- (*************************************************************************************************)
- (** UTILITY FUNCTIONS AND PROOFS *****************************************************************)
- (*************************************************************************************************)
-
- Definition TDM_counter (AS : State_t) :=
- match AS with
- | IDLE _ c _ => c
- | RUNNING _ c _ _ => c
- end.
-
- Definition TDM_pending (AS : State_t) :=
- match AS with
- | IDLE _ _ P => P
- | RUNNING _ _ P _ => P
- end.
-
- Definition TDM_request (AS : State_t) :=
- match AS with
- | IDLE _ _ _ => None
- | RUNNING _ _ _ r => Some r
- end.
-
- Definition TDM_slot (AS : State_t) :=
- match AS with
- | IDLE s _ _ => s
- | RUNNING s _ _ _ => s
- end.
-
- (* Instantiation of Arbiter_trace_t class *)
- Local Instance TDM_arbiter_trace : Implementation_t :=
- mkImplementation Init_state Next_state.
-
- Lemma ACT_neq_ZCycle:
- (OACT_date == OZCycle) = false.
- Proof.
- unfold OACT_date, OZCycle, ACT_date.
- rewrite eqE. simpl.
- apply /negP /negP. rewrite <- addn1, addn_eq0, negb_and.
- apply /orP. by right.
- Qed.
-
- Lemma ACT_neq_CAS:
- (OACT_date == OCAS_date) = false.
- Proof.
- unfold OACT_date, OCAS_date.
- rewrite eqE //= -[ACT_date]addn0 /CAS_date.
- apply /negbTE.
- rewrite eqn_add2l -addn1 eq_sym addn_eq0 negb_and.
- apply /orP. by right.
- Qed.
-
- Lemma Next_ZCycle_neq_ZCycle:
- Next_cycle OZCycle == OZCycle = false.
- Proof.
- unfold OZCycle, Next_cycle, nat_of_ord.
- set (X := 1 < SL).
- dependent destruction X;
- apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; intro; simpl.
- - by rewrite eqE.
- - contradict x. rewrite SL_one. discriminate.
- Qed.
-
- Lemma Next_ACT_neq_ZCycle:
- Next_cycle OACT_date == OZCycle = false.
- Proof.
- unfold OZCycle, OACT_date, Next_cycle, nat_of_ord.
- set (X := ACT_date.+1 < SL).
- dependent destruction X;
- apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; intro; simpl.
- - by rewrite eqE.
- - contradict x. rewrite SL_ACTS. discriminate.
- Qed.
-
- Lemma Next_CAS_neq_ZCycle:
- Next_cycle OCAS_date == OZCycle = false.
- Proof.
- unfold OZCycle, OCAS_date, Next_cycle, nat_of_ord.
- set (X := CAS_date.+1 < SL).
- dependent destruction X;
- apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; intro; simpl.
- - by rewrite eqE.
- - contradict x. rewrite SL_CASS. discriminate.
- Qed.
-
- Lemma Next_cycle_inc (c : Counter_t):
- c < SL.-1
- -> nat_of_ord (Next_cycle c) == c.+1.
- Proof.
- intros H.
- rewrite /Next_cycle //=.
- set x := c.+1 < SL.
- dependent destruction x;
- apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; intro; simpl.
- - trivial.
- - contradict x; rewrite ltn_predRL in H; by rewrite H.
- Qed.
-
- Lemma nat_of_counter_eq (ca cb : Counter_t) :
- (nat_of_ord ca == nat_of_ord cb) = (ca == cb).
- Proof.
- apply inj_eq.
- exact (ord_inj (n := SL)).
- Qed.
-
- Lemma nat_of_ACT c :
- nat_of_ord c == ACT_date -> c == OACT_date.
- Proof.
- intros H.
- move : H => /eqP H.
- by rewrite -nat_of_counter_eq H.
- Qed.
-
- Lemma nat_of_CAS c :
- nat_of_ord c == CAS_date -> c == OCAS_date.
- Proof.
- intros H.
- move : H => /eqP H.
- by rewrite -nat_of_counter_eq H.
- Qed.
-
- Lemma nat_of_slot_eq (sa sb : Slot_t) :
- (nat_of_ord sa == nat_of_ord sb) = (sa == sb).
- Proof.
- apply inj_eq.
- exact (ord_inj (n := SN)).
- Qed.
-
- Lemma TDM_next_cycle_modulo (c : Counter_t) t:
- (t %% SL) = c -> (t.+1 %% SL) = (Next_cycle c).
- Proof.
- intros.
- unfold Next_cycle.
- destruct c as [c Hc]. simpl in *.
- set (nc := c.+1 < SL).
- dependent destruction nc;
- apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro.
- - apply modn_small in x.
- by rewrite -x -(addn1 c) -H modnDml addn1.
- - rewrite -ltn_predRL in x.
- move : x => /ltP /ltP x.
- rewrite -leqNgt leq_eqVlt in x.
- move : x => /orP [/eqP x | x].
- - rewrite -H in x.
- rewrite -add1n -modnDmr -x add1n prednK.
- 2: exact SL_pos.
- by rewrite modnn.
- - apply nat_ltlt_empty in Hc.
- - by contradict Hc.
- - exact SL_pos.
- - exact x.
- Qed.
-
- Lemma Time_counter_modulo t:
- (t %% SL) = TDM_counter (Default_arbitrate t).(Implementation_State).
- Proof.
- induction t.
- - specialize SL_pos as H. apply lt0n_neq0 in H.
- move : H => /eqP H.
- by rewrite mod0n.
- - simpl in *. unfold Next_state, TDM_counter in *. simpl in *.
- destruct (Default_arbitrate t).(Implementation_State), (c == OZCycle), (c == OACT_date), (c == OCAS_date), (c == OLastCycle);
- try destruct (Pending_of _ _); simpl.
- all: by apply TDM_next_cycle_modulo in IHt.
- Qed.
-
- Lemma Exists_time_multiple t:
- (TDM_counter (Default_arbitrate t).(Implementation_State)) == OZCycle
- -> exists d, t = d * SL.
- Proof.
- intros Hc.
- apply /dvdnP.
- rewrite -nat_of_counter_eq -Time_counter_modulo /OZCycle //= in Hc.
- Qed.
-
- Lemma TDM_next_slot_modulo (s : Slot_t) t:
- ((t %/ SL) %% SN) = s -> ((t.+1 %/ SL) %% SN) = (Next_slot s (TDM_counter (Default_arbitrate t).(Implementation_State))).
- Proof.
- intros.
- unfold Next_slot.
- destruct s as [s Hs].
- specialize (Time_counter_modulo t) as Hm.
- destruct (TDM_counter (Default_arbitrate t).(Implementation_State)) as [c Hc]; simpl in *.
- destruct (c.+1 < SL) eqn:HcS; simpl.
- - rewrite <- (addn0 (t %/ SL)) in H.
- rewrite <- addn1, divnD, (divn_small (m := 1)), (modn_small (m := 1)), addn0, addn1, Hm, <- H.
- 4: exact SL_pos.
- 2-3: exact SL_one.
- rewrite ltnNge in HcS. move : HcS => /negPf HcS.
- apply /eqP.
- by rewrite eqn_modDl HcS eq_refl.
- - set (ns := s.+1 < SN).
- dependent destruction ns;
- apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; intro; simpl.
- - apply modn_small in x.
- rewrite <- addn1, divnD, (divn_small (m := 1)), (modn_small (m := 1)), addn0, addn1, Hm, <- x, <- H.
- 4: exact SL_pos.
- 2-3: exact SL_one.
- rewrite ltnNge in HcS. move : HcS => /negPn HcS.
- apply /eqP.
- by rewrite <- (addn1 (_ %% SN)), modnDml, eqn_modDl, HcS.
- - rewrite <- ltn_predRL in x.
- move : x => /ltP /ltP x.
- rewrite <- leqNgt, leq_eqVlt in x.
- move : x => /orP [He | Hlt].
- - rewrite <- H, <- (modn_small (m := SN.-1) (d := SN)) in He.
- rewrite <- (eqn_modDr 1), !addn1, prednK, modnn in He.
- 3: rewrite ltn_predL.
- 2-3: exact SN_pos.
- move : He => /eqP He. rewrite He.
- apply /eqP.
- rewrite divnS. unfold dvdn.
- 2: exact SL_pos.
- rewrite <- ltn_predRL in HcS.
- move : HcS => /ltP /ltP HcS.
- rewrite <- leqNgt, leq_eqVlt in HcS.
- move : HcS => /orP [HcE | HcL].
- - rewrite <- Hm, <- (modn_small (m := SL.-1) (d := SL)), <- (eqn_modDr 1), !addn1, prednK in HcE.
- 3: rewrite ltn_predL.
- 2-3: exact SL_pos.
- move : HcE => /eqP HcE.
- by rewrite <- HcE, modnn, eq_refl.
- - apply nat_ltlt_empty in Hc.
- - by contradict Hc.
- - exact SL_pos.
- - exact HcL.
- - apply nat_ltlt_empty in Hs.
- - by contradict Hs.
- - exact SN_pos.
- - exact Hlt.
- Qed.
-
- Lemma Time_slot_modulo t:
- ((t %/ SL) %% SN) = TDM_slot (Default_arbitrate t).(Implementation_State).
- Proof.
- induction t.
- - specialize SN_pos as H. apply lt0n_neq0 in H.
- move : H => /eqP H.
- by rewrite div0n mod0n.
- - apply TDM_next_slot_modulo in IHt.
- simpl in *. unfold Next_state, TDM_slot, TDM_counter in *. simpl in *.
- destruct (Default_arbitrate t).(Implementation_State), (c == OZCycle), (c == OACT_date), (c == OCAS_date), (c == OLastCycle);
- try destruct (Pending_of _ _); simpl.
- all: exact IHt.
- Qed.
-
- (*************************************************************************************************)
- (** COMMAND TIMING PROOFS ************************************************************************)
- (*************************************************************************************************)
-
- Lemma Modulo_time_distance t t':
- TDM_counter (Default_arbitrate t).(Implementation_State) == TDM_counter (Default_arbitrate t').(Implementation_State)
- -> t' < t
- -> t' + SL <= t.
- Proof.
- intros Hc Ht.
- rewrite <- nat_of_counter_eq in Hc.
- rewrite <- 2 Time_counter_modulo in Hc. rewrite eqn_mod_dvd in Hc.
- - move : Hc => /dvdnP Hc. destruct Hc.
- rewrite <- leq_subRL, H.
- - apply leq_pmull. rewrite <- subn_gt0, H, muln_gt0 in Ht. by move : Ht => /andP [He _].
- all: by apply ltnW.
- Qed.
-
- Ltac isCommand :=
- unfold isPRE, isACT, isCAS, PRE_of_req, ACT_of_req, CAS_of_req, Kind_of_req;
- match goal with
- | |- context G [?r.(Kind)] => destruct (r.(Kind)); discriminate
- | |- (_) => discriminate
- end.
-
- Lemma PRE_modulo_date t cmd:
- cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isPRE cmd ->
- cmd.(CDate) %% SL == Next_cycle OZCycle.
- Proof.
- induction t.
- - done.
- - intros Hi Hp.
- simpl in *. unfold Next_state in *.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (c == OZCycle) eqn:Hz, (c == OACT_date), (c == OCAS_date), (c == OLastCycle);
- try destruct (Pending_of _ _) eqn:HP; simpl in Hi.
- all: try (rewrite in_cons in Hi; move : Hi => /orP [/eqP He | Hi]; subst).
- all: try by apply IHt in Hi. (* if no new command generated *)
- all: try by (contradict Hp; isCommand). (* if a command other than a PRE is generated *)
- (* a PRE command is generated *)
- all: simpl; rewrite Time_counter_modulo //= /Next_state Hs HP Hz /TDM_counter //=.
- all: move : Hz => /eqP Hz; by subst.
- Qed.
-
- Lemma ACT_modulo_date t cmd:
- cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isACT cmd ->
- cmd.(CDate) %% SL == Next_cycle OACT_date.
- Proof.
- induction t.
- - done.
- - intros Hi Hp.
- simpl in *. unfold Next_state in *.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (c == OZCycle), (c == OACT_date) eqn:Ha, (c == OCAS_date), (c == OLastCycle);
- try destruct (Pending_of _ _) eqn:HP; simpl in Hi.
- all: try (rewrite in_cons in Hi; move : Hi => /orP [/eqP He | Hi]; subst).
- all: try by apply IHt in Hi. (* if no new command generated *)
- all: try by (contradict Hp; isCommand). (* if a command other than an ACT is generated *)
- (* an ACT command is generated *)
- all: simpl; rewrite Time_counter_modulo //= /Next_state Hs Ha /TDM_counter //=.
- all: move : Ha => /eqP Ha; by subst.
- Qed.
-
- Lemma CAS_modulo_date t cmd:
- cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isCAS cmd ->
- cmd.(CDate) %% SL == Next_cycle OCAS_date.
- Proof.
- induction t.
- - done.
- - intros Hi Hp.
- simpl in *. unfold Next_state in *.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (c == OZCycle), (c == OACT_date) eqn:Ha, (c == OCAS_date) eqn:Hc, (c == OLastCycle);
- try destruct (Pending_of _ _) eqn:HP; simpl in Hi.
- all: try (rewrite in_cons in Hi; move : Hi => /orP [/eqP He | Hi]; subst).
- all: try by apply IHt in Hi. (* if no new command generated *)
- all: try by (contradict Hp; isCommand). (* if a command other than a CAS is generated *)
- (* a CAS command is generated *)
- all: simpl; rewrite Time_counter_modulo //= /Next_state Hs Ha Hc /TDM_counter //=.
- all: move : Hc => /eqP Hc; by subst.
- Qed.
-
- Lemma Cmds_T_RRD_ok t a b:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- ACT_to_ACT a b -> ~~ Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RRD.
- Proof.
- intros Ha Hb AtA _ aBb.
- move : AtA => /andP [Aa Ab].
- apply ACT_modulo_date in Ha.
- 2: exact Aa. clear Aa.
- apply ACT_modulo_date in Hb.
- 2: exact Ab. clear Ab.
- move : Ha => /eqP Ha.
- rewrite <- Ha, !Time_counter_modulo, nat_of_counter_eq in Hb. clear Ha.
- apply Modulo_time_distance in Hb as H.
- 2: by unfold Before. clear Hb aBb.
- unfold Apart_at_least.
- apply leq_trans with (n := a.(CDate) + SL).
- 2: exact H.
- rewrite leq_add2l.
- by rewrite leq_eqVlt T_RRD_SL orbT.
- Qed.
-
- Lemma Cmds_T_FAW_ok t a b c d:
- a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- c \in (Default_arbitrate t).(Arbiter_Commands) -> d \in (Default_arbitrate t).(Arbiter_Commands) ->
- isACT a -> isACT b -> isACT c -> isACT d -> Diff_Bank [::a;b;c;d] ->
- Before a b -> Before b c -> Before c d ->
- Apart_at_least a d T_FAW.
- Proof.
- intros Ha Hb Hc Hd Aa Ab Ac Ad _ aBb bBc cBd.
- apply ACT_modulo_date in Ha.
- 2: exact Aa. clear Aa.
- apply ACT_modulo_date in Hb.
- 2: exact Ab. clear Ab.
- apply ACT_modulo_date in Hc.
- 2: exact Ac. clear Ac.
- apply ACT_modulo_date in Hd.
- 2: exact Ad. clear Ad.
- move : Ha Hb Hc Hd => /eqP Ha /eqP Hb /eqP Hc /eqP Hd.
- rewrite <- Hc, !Time_counter_modulo in Hd.
- rewrite <- Hb, !Time_counter_modulo in Hc.
- rewrite <- Ha, !Time_counter_modulo in Hb. clear Ha.
-
- move : Hb Hc Hd => /eqP Hb /eqP Hc /eqP Hd.
-
- rewrite nat_of_counter_eq in Hb.
- rewrite nat_of_counter_eq in Hc.
- rewrite nat_of_counter_eq in Hd.
-
- apply Modulo_time_distance in Hb as aLb.
- 2: by unfold Before. clear Hb aBb.
- apply Modulo_time_distance in Hc as bLc.
- 2: by unfold Before. clear Hc bBc.
- apply Modulo_time_distance in Hd as cLd.
- 2: by unfold Before. clear Hd cBd.
-
- rewrite <- (leq_add2r SL), addnCAC, addnC in aLb.
- apply leq_trans with (p := c.(CDate)) in aLb.
- 2: exact bLc. clear bLc.
- rewrite <- (leq_add2r SL), addnCAC, addnC in aLb.
- apply leq_trans with (p := d.(CDate)) in aLb.
- 2: exact cLd. clear cLd.
-
- unfold Apart_at_least.
- apply leq_trans with (n := a.(CDate) + (SL + SL + SL)).
- by rewrite leq_add2l leq_eqVlt T_FAW_3SL orbT.
- by rewrite addnACl.
- Qed.
-
- (*************************************************************************************************)
- (** REQUEST HANDLING PROOFS **********************************************************************)
- (*************************************************************************************************)
-
- (* The time instant when the counter was last zero, i.e., the last slot started.*)
- Definition Last_slot_start ta :=
- ta - TDM_counter (Default_arbitrate ta).(Implementation_State).
-
- Lemma Last_Slot_start_aligned ta :
- ((TDM_counter (Default_arbitrate (Last_slot_start ta)).(Implementation_State)) == OZCycle).
- Proof.
- rewrite /Last_slot_start -!nat_of_counter_eq -!Time_counter_modulo //=.
- rewrite -(mod0n SL) -(eqn_modDr (ta %% SL)) add0n subnK.
- 2: apply leq_mod.
- by rewrite modn_mod eq_refl.
- Qed.
-
- (* The time instant when the counter will become zero next, i.e., the next slot to start.*)
- Definition Next_slot_start ta :=
- (Last_slot_start ta) + SL.
-
- Lemma Next_Slot_start_aligned ta :
- ((TDM_counter (Default_arbitrate (Next_slot_start ta)).(Implementation_State)) == OZCycle).
- Proof.
- rewrite /Next_slot_start /Last_slot_start -!nat_of_counter_eq -!Time_counter_modulo //=.
- rewrite -(mod0n SL) -(eqn_modDr (ta %% SL)) add0n addnACl [ta %% SL + _]addnC subnK.
- 2: apply leq_mod.
- by rewrite modnDl modn_mod eq_refl.
- Qed.
-
- (* The closest time instant when the counter will become zero, i.e., now or the next slot start *)
- Definition Closest_slot_start ta :=
- if ((TDM_counter (Default_arbitrate ta).(Implementation_State)) == OZCycle) then ta
- else (Next_slot_start ta).
-
- Lemma Closest_slot_start_aligned ta :
- ((TDM_counter (Default_arbitrate (Closest_slot_start ta)).(Implementation_State)) == OZCycle).
- Proof.
- rewrite /Closest_slot_start.
- destruct (TDM_counter (Default_arbitrate ta).(Implementation_State) == OZCycle) eqn:Hz.
- - move : Hz => /eqP Hz; by rewrite Hz eq_refl.
- - apply Next_Slot_start_aligned.
- Qed.
-
- Lemma Closest_slot_start_leq ta:
- ta <= Closest_slot_start ta.
- Proof.
- unfold Closest_slot_start.
- destruct (_ == _).
- - apply leqnn.
- - unfold Next_slot_start, Last_slot_start.
- rewrite -addnABC.
- 3: rewrite -Time_counter_modulo; apply ltnW, ltn_pmod; exact SL_pos.
- 2: rewrite -Time_counter_modulo; apply leq_mod.
- by rewrite leq_addr.
- Qed.
-
- Lemma Pending_on_arrival ta ra:
- ra \in Arrival_at ta
- -> ra \in (TDM_pending ((Default_arbitrate ta).(Implementation_State))).
- Proof.
- intros HA.
- destruct ta.
- - by rewrite /TDM_pending.
- - rewrite /TDM_pending //= /Next_state.
- destruct (Default_arbitrate ta).(Implementation_State) as [s c P | s c P rb] eqn:HSS,
- (c == OZCycle) eqn:Hz, (c == OACT_date) eqn:Ha, (c == OCAS_date) eqn:Hc, (c == OLastCycle) eqn:Hl;
- try (destruct (Pending_of s P) as [ | rb] eqn:HPP); simpl in *.
- all: by rewrite /Enqueue mem_cat HA orbT.
- Qed.
-
- Definition Requestor_slot_start ta (s : Slot_t) :=
- let aligned_ta := Closest_slot_start ta in
- let current_slot := TDM_slot (Default_arbitrate aligned_ta).(Implementation_State) in
- if current_slot <= s then aligned_ta + ((s - current_slot) * SL)
- else aligned_ta + (((SN - current_slot) + s) * SL).
-
- Lemma Requestor_slot_start_aligned ta s:
- (TDM_counter (Default_arbitrate (Requestor_slot_start ta s)).(Implementation_State)) == OZCycle.
- Proof.
- rewrite -nat_of_counter_eq -Time_counter_modulo -(modn_small (m := OZCycle) (d := SL)).
- 2: trivial.
- rewrite /Requestor_slot_start.
- destruct (TDM_slot (Default_arbitrate (Closest_slot_start ta)).(Implementation_State) <= s);
- rewrite addnC modnMDl (modn_small (m := OZCycle) (d := SL));
- (trivial || by rewrite Time_counter_modulo nat_of_counter_eq Closest_slot_start_aligned).
- Qed.
-
- Lemma Slots_equals_last_slot ta:
- (TDM_slot (Default_arbitrate ta).(Implementation_State)) =
- (TDM_slot (Default_arbitrate (Last_slot_start ta)).(Implementation_State)).
- Proof.
- apply /eqP.
- rewrite -nat_of_slot_eq -!Time_slot_modulo.
- rewrite /Last_slot_start -Time_counter_modulo.
- rewrite {2}(divn_eq ta SL) -addnBA.
- 2: apply leqnn.
- rewrite subnn addn0 mulnK.
- 2: exact SL_pos.
- by rewrite eq_refl.
- Qed.
-
- Lemma Requestor_slot_start_match ta s :
- (TDM_slot (Default_arbitrate (Requestor_slot_start ta s)).(Implementation_State)) == s.
- Proof.
- specialize (Requestor_slot_start_aligned ta s) as HC.
- specialize (Closest_slot_start_aligned ta) as HC'.
- rewrite -!nat_of_counter_eq -!Time_counter_modulo /OZCycle //= in HC HC'.
- move : HC HC' => /dvdnP HC /dvdnP HC'; destruct HC as [x HC], HC' as [x' HC'].
-
- unfold Requestor_slot_start.
- destruct (TDM_slot (Default_arbitrate (Closest_slot_start ta)).(Implementation_State) <= s) eqn:HS;
- rewrite -Time_slot_modulo HC' mulnK in HS; try exact SL_pos;
- rewrite HC' -mulnDl -nat_of_slot_eq -!Time_slot_modulo;
- rewrite !mulnK; try exact SL_pos.
- - rewrite nat_add_modn_sub.
- - by rewrite eq_refl.
- - exact SN_pos.
- - destruct s as [s Hs]; exact Hs.
- - exact HS.
- - rewrite -{2}(modn_small (m := s) (d := SN)).
- 2: destruct s as [s Hs]; exact Hs.
- rewrite -{2}(add0n s) -addnACl addnCAC eqn_modDr addnC nat_add_modd_sub.
- 2: exact SN_pos.
- by rewrite mod0n.
- Qed.
-
- Lemma Slots_in_period ta:
- forall i,
- (nat_of_ord (TDM_slot (Default_arbitrate (ta + (i*SL))).(Implementation_State)) = ((TDM_slot (Default_arbitrate ta).(Implementation_State)) + i) %% SN).
- Proof.
- specialize (Last_Slot_start_aligned ta) as HC.
- rewrite -nat_of_counter_eq -Time_counter_modulo //= in HC.
- move : HC => /dvdnP HC; destruct HC as [x HC].
- rewrite Slots_equals_last_slot HC -Time_slot_modulo mulnK.
- 2: exact SL_pos.
- rewrite /Last_slot_start -Time_counter_modulo in HC.
- intros i.
- apply /eqP.
- rewrite modnDml.
- rewrite Slots_equals_last_slot -Time_slot_modulo /Last_slot_start -Time_counter_modulo.
- rewrite [ta + (i * SL)]addnC modnMDl -addnBA.
- 2: apply leq_mod.
- rewrite HC -mulnDl mulnK.
- 2: exact SL_pos.
- by rewrite addnC.
- Qed.
-
- Lemma Requestor_slot_start_distance ta (s : Slot_t):
- (Requestor_slot_start ta s) - ta < SN*SL.
- Proof.
- rewrite /Requestor_slot_start /Closest_slot_start /Next_slot_start /Last_slot_start.
- destruct (_ <= s) eqn:Hs, (_ == OZCycle) eqn:Hc.
- - rewrite ltn_subLR.
- 2: apply leq_addr.
- rewrite ltn_add2l ltn_mul2r SL_pos andTb.
- rewrite ltn_subLR.
- 2: exact Hs.
- by apply ltn_addl.
- - rewrite {1}addnBAC.
- 2: by rewrite -Time_counter_modulo leq_mod.
- rewrite -[ta + _ - _]addnBA.
- 2: rewrite -Time_counter_modulo; apply ltnW, ltn_pmod, SL_pos.
- rewrite ltn_subLR.
- 2: apply nat_leq_addr, nat_leq_addr, leqnn.
- rewrite [ta + _]addnC addnACl ltn_add2l addnBA.
- 2: rewrite -Time_counter_modulo; apply ltnW, ltn_pmod, SL_pos.
- rewrite ltn_subLR.
- 2: apply nat_leq_addl; rewrite -Time_counter_modulo; apply ltnW, ltn_pmod, SL_pos.
- rewrite -mulSnr.
- apply leq_ltn_trans with (n := SN * SL).
- 2: move : Hc => /negbT Hc; rewrite -lt0n in Hc; rewrite addnC; by apply nat_ltnn_add.
- rewrite leq_mul2r; apply /orP; right.
- rewrite -subSn.
- 2: exact Hs.
- rewrite leq_subLR.
- by apply ltn_addl.
- - rewrite ltn_subLR.
- 2: apply nat_leq_addr, leqnn.
- rewrite ltn_add2l ltn_mul2r SL_pos andTb.
- rewrite addnBAC.
- 2: by apply ltnW.
- rewrite ltn_subLR.
- 2: by apply nat_leq_addr, ltnW.
- by rewrite addnC ltn_add2r ltnNge Hs.
- - rewrite {1}addnBAC.
- 2: by rewrite -Time_counter_modulo leq_mod.
- rewrite -[ta + _ - _]addnBA.
- 2: rewrite -Time_counter_modulo; apply ltnW, ltn_pmod, SL_pos.
- rewrite ltn_subLR.
- 2: apply nat_leq_addr, nat_leq_addr, leqnn.
- rewrite [ta + _]addnC addnACl ltn_add2l addnBA.
- 2: rewrite -Time_counter_modulo; apply ltnW, ltn_pmod, SL_pos.
- rewrite ltn_subLR.
- 2: apply nat_leq_addl; rewrite -Time_counter_modulo; apply ltnW, ltn_pmod, SL_pos.
- rewrite -mulSnr.
- apply leq_ltn_trans with (n := SN * SL).
- 2: move : Hc => /negbT Hc; rewrite -lt0n in Hc; rewrite addnC; by apply nat_ltnn_add.
- rewrite leq_mul2r; apply /orP; right.
- rewrite addnBAC.
- 2: rewrite -Time_slot_modulo; apply ltnW, ltn_pmod, SN_pos.
- rewrite ltn_subLR.
- 2: rewrite -Time_slot_modulo; apply ltnW, ltn_addr, ltn_pmod, SN_pos.
- by rewrite addnC ltn_add2r ltnNge Hs.
- Qed.
-
- (* TODO: merge No_requestor_periodX and No_requestor_periodY *)
- Lemma No_requestor_periodY ta tb s:
- ta < tb -> tb < (Requestor_slot_start ta s)
- -> ((TDM_counter (Default_arbitrate tb).(Implementation_State)) != OZCycle) || ((TDM_slot (Default_arbitrate tb).(Implementation_State)) != s).
- Proof.
- intros HL HU.
- apply /orP.
- destruct (TDM_counter (Default_arbitrate tb).(Implementation_State) != OZCycle) eqn:HC.
- - by left.
- - right; move : HC => /negPn HC.
- destruct tb.
- - contradict HL; by rewrite ltn0.
- - specialize (Requestor_slot_start_distance ta s) as HB.
- specialize (Requestor_slot_start_aligned ta s) as HUC.
- specialize (Requestor_slot_start_match ta s) as HUS.
-
- apply Exists_time_multiple in HUC; destruct HUC as [u HUC].
- rewrite HUC in HU HB.
-
- rewrite -nat_of_slot_eq -Time_slot_modulo HUC mulnK in HUS.
- 2: exact SL_pos.
- move : HUS => /eqP HUS.
-
- apply ltn_trans with (m := u * SL - tb.+1) in HB .
- 2: apply ltn_sub2l; exact HL ||
- (apply ltn_trans with (n := tb.+1); exact HL || exact HU).
-
- apply Exists_time_multiple in HC as Htb; destruct Htb as [b Htb].
- rewrite -nat_of_slot_eq -Time_slot_modulo.
- rewrite !Htb in HB HU *.
- rewrite -HUS mulnK.
- 2: exact SL_pos.
-
- rewrite ltn_subLR in HB.
- 2: apply ltnW; exact HU.
- rewrite -mulnDl in HB.
- rewrite !ltn_mul2r in HB, HU; move : HB HU => /andP [_ HB] /andP [_ HU].
-
- rewrite eq_sym eqn_mod_dvd.
- 2: apply ltnW; exact HU.
- rewrite /dvdn modn_small.
- 2: rewrite -ltn_subLR in HB; exact HB || apply ltnW; exact HU.
-
- by rewrite -lt0n subn_gt0.
- Qed.
-
- Lemma No_requestor_periodX a s:
- TDM_slot (Default_arbitrate (a * SL)).(Implementation_State) == s
- -> forall tb, a * SL < tb -> tb < a * SL + SN * SL
- -> (TDM_counter (Default_arbitrate tb).(Implementation_State) != OZCycle) || (TDM_slot (Default_arbitrate tb).(Implementation_State) != s).
- Proof.
- intros HS tb HL HU.
- apply /orP.
- destruct (TDM_counter (Default_arbitrate tb).(Implementation_State) != OZCycle) eqn:HC.
- - by left.
- - right; move : HC => /negPn HC.
- destruct tb.
- - contradict HL; by rewrite ltn0.
- - rewrite -nat_of_slot_eq -Time_slot_modulo mulnK in HS.
- 2: exact SL_pos.
- move : HS => /eqP HS.
-
- apply Exists_time_multiple in HC as Htb; destruct Htb as [b Htb].
- rewrite -nat_of_slot_eq -Time_slot_modulo.
- rewrite !Htb in HL HU *.
- rewrite -HS mulnK.
- 2: exact SL_pos.
-
- rewrite -mulnDl in HU.
- rewrite !ltn_mul2r in HU, HL; move : HL HU => /andP [_ HL] /andP [_ HU].
- rewrite -ltn_subLR in HU.
- 2: apply ltnW; exact HL.
- rewrite eqn_mod_dvd.
- 2: apply ltnW; exact HL.
- rewrite /dvdn modn_small.
- 2: exact HU.
- by rewrite -lt0n subn_gt0.
- Qed.
-
- Lemma Request_slot_start_aligned ta s i:
- TDM_counter (Default_arbitrate (Requestor_slot_start ta s + (i*SN*SL))).(Implementation_State) == OZCycle.
- Proof.
- specialize (Requestor_slot_start_aligned ta s) as H.
- rewrite -!nat_of_counter_eq -!Time_counter_modulo in H *.
- rewrite addnC modnMDl.
- exact H.
- Qed.
-
- Lemma Request_slot_start_match ta s i:
- (TDM_slot (Default_arbitrate ((Requestor_slot_start ta s) + (i*SN*SL))).(Implementation_State)) == s.
- Proof.
- specialize (Requestor_slot_start_match ta s) as HS.
- rewrite -nat_of_slot_eq in HS; move : HS => /eqP HS.
- specialize (Slots_in_period (Requestor_slot_start ta s) (i * SN)) as HS'.
- rewrite HS [s + _]addnC modnMDl in HS'.
- by rewrite -nat_of_slot_eq HS' modn_small.
- Qed.
-
- Lemma Requestor_slot_start_leq ta ra:
- ta <= Requestor_slot_start ta ra.(Requestor).
- Proof.
- unfold Requestor_slot_start.
- destruct (_ <= ra.(Requestor)).
- all: apply leq_trans with (n := Closest_slot_start ta) ; apply leq_addr || apply Closest_slot_start_leq.
- Qed.
-
- Lemma Pending_requestor ta ra:
- is_true (ra \in TDM_pending (Default_arbitrate ta).(Implementation_State))
- -> ((TDM_counter (Default_arbitrate ta).(Implementation_State) != OZCycle) || (TDM_slot (Default_arbitrate ta).(Implementation_State) != ra.(Requestor)))
- -> is_true (ra \in TDM_pending (Default_arbitrate ta.+1).(Implementation_State)).
- Proof.
- intros HP HCS.
- move : HCS => /orP [HC | HS].
-
- all: unfold TDM_counter, TDM_pending, TDM_slot in *.
- all: simpl; unfold Next_state.
- all: destruct (Default_arbitrate ta).(Implementation_State) as [s' c P | s' c P rb] eqn:HSS,
- (c == OZCycle) eqn:Hz, (c == OACT_date) eqn:Ha, (c == OCAS_date) eqn:Hc, (c == OLastCycle) eqn:Hl;
- try (destruct (Pending_of s' P) as [ | rb] eqn:HPP); simpl in *.
-
- all: try by contradict HC.
-
- (* cases within a slot *)
- all: try (by rewrite /Enqueue mem_cat HP).
-
- all: apply seq_filter_eq_cons_p in HPP; move : HPP => /eqP HPP; subst.
- all: rewrite /Enqueue /Dequeue mem_cat seq_rem_id.
- all: try trivial.
-
- all: try (rewrite mem_cat; apply /orP; by left).
- all: move : HS => /negPf HS; rewrite eq_sym in HS.
- all: by rewrite eqE //= /Requests.Request_eqdef HS !andFb.
- Qed.
-
- Lemma Requestor_slot_start_lt ta s:
- (ta < Requestor_slot_start ta s) -> ((TDM_counter (Default_arbitrate ta).(Implementation_State)) != OZCycle) || ((TDM_slot (Default_arbitrate ta).(Implementation_State)) != s).
- Proof.
- intros H.
- rewrite /Requestor_slot_start /Closest_slot_start /Next_slot_start /Last_slot_start in H.
- destruct (TDM_counter (Default_arbitrate ta).(Implementation_State) == OZCycle) eqn:Hc, (TDM_slot (Default_arbitrate ta).(Implementation_State) == s) eqn:HS,
- (_ <= s) eqn:Hs; trivial; move : HS => /eqP HS.
- - contradict H; subst; by rewrite subnn mul0n addn0 ltnn.
- - contradict Hs; subst; by rewrite leqnn.
- Qed.
-
- Lemma Pending_requestor_slot_start ta ra:
- ra \in (TDM_pending (Default_arbitrate ta).(Implementation_State))
- -> forall tb, ta <= tb -> tb <= (Requestor_slot_start ta ra.(Requestor))
- -> ra \in (TDM_pending (Default_arbitrate tb).(Implementation_State)).
- Proof.
- intros HP.
- destruct (ta == (Requestor_slot_start ta ra.(Requestor))) eqn:Ht.
- - intros tb HL HU.
- move : Ht => /eqP Ht; rewrite Ht in HL HP.
- rewrite leq_eqVlt in HU; rewrite leq_eqVlt in HL.
- move : HL HU => /orP [/eqP HL | HL] /orP [/eqP HU | HU]; subst.
- - exact HP.
- - contradict HU; by rewrite ltnn.
- - contradict HL; by rewrite ltnn.
- - contradict HL; apply /negP; rewrite -leqNgt; apply ltnW, HU.
- - move : Ht => /negbT Ht. rewrite neq_ltn in Ht; move : Ht => /orP [Ht | Ht].
- 2: specialize (Requestor_slot_start_leq ta ra) as H;
- contradict H; apply /negP; by rewrite leqNgt Ht.
-
- induction tb; intros HL HU.
- - rewrite leqn0 in HL; move : HL => /eqP HL; subst; exact HP.
- - rewrite leq_eqVlt in HL; move : HL => /orP [/eqP HL | HL].
- - subst; exact HP.
- - rewrite ltnS in HL.
- apply IHtb in HL as IH; clear IHtb.
- 2: by apply ltnW in HU.
-
- rewrite leq_eqVlt in HL; move : HL => /orP [/eqP HL | HL].
- - subst; apply Requestor_slot_start_lt in Ht; by apply Pending_requestor.
- - apply No_requestor_periodY with (s := ra.(Requestor)) in HL as HCS.
- 2: exact HU.
- by apply Pending_requestor.
- Qed.
-
- Lemma Not_Running_ZCycle t P s r:
- (Default_arbitrate t).(Implementation_State) <> RUNNING s OZCycle P r.
- Proof.
- induction t.
- - discriminate.
- - apply /eqP.
- simpl. unfold Next_state.
- destruct (Default_arbitrate t).(Implementation_State), (c == OZCycle) eqn:Hz, (c == OACT_date) eqn:Ha, (c == OCAS_date) eqn:Hc, (c == OLastCycle) eqn:Hl;
- try destruct (Pending_of _ _).
- all: try (exact isT); simpl.
- all: move : Hz Ha Hc => /eqP Hz /eqP Ha /eqP Hc; subst.
- all: rewrite eqE !negb_and; simpl.
- all: apply /orP; left.
- all: apply /orP; left.
- all: apply /orP; right.
- all: try (by rewrite Next_ZCycle_neq_ZCycle).
- all: try (by rewrite Next_ACT_neq_ZCycle).
- all: try (by rewrite Next_CAS_neq_ZCycle).
-
- clear Hz Ha Hc.
- move : Hl => /negbT Hl.
- unfold Next_cycle.
- set (X := c.+1 < SL).
- dependent destruction X;
- apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; intro; simpl.
- - exact isT.
- - contradict x.
- destruct c as [c H];
- rewrite ltn_neqAle //=.
- apply Bool.not_false_iff_true. apply /andP. split.
- - rewrite <- nat_of_counter_eq, <- eqSS in Hl. simpl in Hl. rewrite prednK in Hl.
- - exact Hl.
- - exact SL_pos.
- - exact H.
- Qed.
-
- Lemma Request_index_decrements_within_period ta ra:
- let S := (Default_arbitrate ta).(Implementation_State) in
- (ra \in (TDM_pending S))
- -> (TDM_counter S) == OZCycle
- -> (TDM_slot S) == ra.(Requestor)
- -> (0 < index ra (Pending_of ra.(Requestor) (TDM_pending S)))
- -> forall tb, ta < tb
- -> tb <= ta + SN * SL
- -> let S' := (Default_arbitrate tb).(Implementation_State) in
- (ra \in (TDM_pending S')) && ((index ra (Pending_of ra.(Requestor) (TDM_pending S))) == (index ra (Pending_of ra.(Requestor) (TDM_pending S'))).+1).
- Proof.
- intros S HP HC HS HI.
- unfold S in *; clear S.
- induction tb; intros HL HU.
- - contradict HL.
- by rewrite ltn0.
- - rewrite leq_eqVlt in HL; move : HL => /orP [HL | HL].
- - clear IHtb.
- rewrite eqSS in HL; move : HL => /eqP HL; subst.
- simpl; unfold TDM_counter, TDM_pending, TDM_slot, Next_state in *.
- destruct (Default_arbitrate tb).(Implementation_State) as [s' c P | s' c P rb] eqn:HSS;
- move : HC HS => /eqP HC /eqP HS; subst.
- - rewrite eq_refl.
- apply seq_in_filer_in with (p := fun r => r.(Requestor) == ra.(Requestor)) in HP as HF.
- 2: trivial.
- destruct (Pending_of _ P) as [ | rb] eqn:HPP; simpl; unfold Pending_of in HPP; rewrite HPP in HF.
- - contradict HF; by rewrite in_nil.
- - simpl in HI.
- destruct (rb == ra) eqn:He.
- - contradict HI; by rewrite ltnn.
- - rewrite in_cons in HF; move : HF => /orP [/eqP HF | HF].
- - contradict He; by rewrite HF eq_refl.
- - rewrite /Enqueue /Dequeue /Pending_of filter_cat seq_filter_rem HPP //= eq_refl index_cat HF.
- rewrite mem_cat seq_rem_id.
- 3: apply /negPf; by rewrite eq_sym.
- 2: exact HP.
- by rewrite orTb eq_refl.
- - contradict HSS; by apply Not_Running_ZCycle.
- - rewrite ltnS in HL.
- apply IHtb in HL as IH; clear IHtb.
- 2: by apply ltnW in HU.
-
- move : IH => /andP [HP' /eqP HI'].
- rewrite HI'.
-
- apply Exists_time_multiple in HC. destruct HC as [a HC]. subst.
- apply No_requestor_periodX with (tb := tb) in HS.
- 3: exact HU.
- 2: exact HL.
-
- apply Pending_requestor in HP' as HP''.
- 2: exact HS.
- rewrite HP'' andTb.
- clear HL HU HI HP HI' HP''.
-
- simpl in *; unfold TDM_counter, TDM_pending, TDM_slot, Next_state in *.
-
- destruct (Default_arbitrate tb).(Implementation_State) as [s' c P | s' c P rb] eqn:HSS,
- (c == OZCycle), (c == OACT_date), (c == OCAS_date), (c == OLastCycle);
- try (destruct (Pending_of s' P) as [ | rb] eqn:HPP); simpl in *.
-
- all: apply seq_in_filer_in with (p := fun r => r.(Requestor) == ra.(Requestor)) in HP' as HF; trivial.
- all: try (by rewrite /Pending_of /Enqueue filter_cat index_cat HF eq_refl).
-
- all: rewrite /Pending_of in HPP;
- rewrite /Pending_of /Enqueue /Dequeue filter_cat seq_filter_rem_id;
- (by rewrite index_cat HF eq_refl) ||
- (apply seq_filter_eq_cons_p in HPP; move : HPP => /eqP HPP; rewrite -HPP in HS; by apply /negbTE).
- Qed.
-
- Lemma Request_index_decrements_over_periods ta ra:
- let S := (Default_arbitrate (Requestor_slot_start ta ra.(Requestor))).(Implementation_State) in
- ra \in (TDM_pending S)
- -> forall i, let S' := (Default_arbitrate (Requestor_slot_start ta ra.(Requestor) + i * SN * SL)).(Implementation_State) in
- i <= (index ra (Pending_of ra.(Requestor) (TDM_pending S)))
- -> (ra \in (TDM_pending S')) && ((index ra (Pending_of ra.(Requestor) (TDM_pending S))) == (index ra (Pending_of ra.(Requestor) (TDM_pending S'))) + i).
- Proof.
- intros S HP.
- induction i; intros S' Hi;
- unfold S, S' in *; clear S S'.
- - by rewrite /Pending_of !mul0n !addn0 eq_refl HP.
- - apply ltnW in Hi as IH.
- apply IHi in IH; clear IHi; move : IH => /andP [HP' /eqP IH'].
-
- apply Request_index_decrements_within_period with (tb := (Requestor_slot_start ta ra.(Requestor) + i.+1 * SN * SL)) in HP'.
- - move : HP' => /andP [HP'' /eqP IH''].
- by rewrite HP'' IH' IH'' addnS addSn eq_refl.
- - rewrite -nat_of_counter_eq -Time_counter_modulo addnC modnMDl Time_counter_modulo.
- apply Requestor_slot_start_aligned.
- - rewrite -nat_of_slot_eq -Time_slot_modulo divnDMl.
- 2: exact SL_pos.
- rewrite addnC modnMDl Time_slot_modulo.
- apply Requestor_slot_start_match.
- - rewrite IH' -{1}[i]add0n ltn_add2r in Hi; exact Hi.
- - by rewrite ltn_add2l !ltn_mul2r SL_pos SN_pos !andTb ltnSn.
- - rewrite addnCAC [i*_]mulnC -[_ * i * _]mulnAC -mulnS addnC leq_add2r.
- by rewrite [_ * i.+1]mulnAC [_ * i.+1]mulnC leqnn.
- Qed.
-
- Lemma Request_index_zero ta ra:
- let S := (Default_arbitrate (Requestor_slot_start ta ra.(Requestor))).(Implementation_State) in
- let i := (index ra (Pending_of ra.(Requestor) (TDM_pending S))) in
- ra \in (TDM_pending S)
- -> let S' := (Default_arbitrate (Requestor_slot_start ta ra.(Requestor) + i * SN * SL)).(Implementation_State) in
- (ra \in (TDM_pending S')) && ((index ra (Pending_of ra.(Requestor) (TDM_pending S'))) == 0).
- Proof.
- intros S i HP; simpl.
-
- apply Request_index_decrements_over_periods with (i := i) in HP.
- 2: unfold i, S; by rewrite leqnn.
- move : HP => /andP [HP HI].
-
- rewrite HP andTb.
- by rewrite -[index _ _]add0n eqn_add2r eq_sym in HI.
- Qed.
-
- Lemma Request_starts ta ra:
- let S := (Default_arbitrate ta).(Implementation_State) in
- (TDM_counter S) == OZCycle
- -> (TDM_slot S) == ra.(Requestor)
- -> (ra \in (TDM_pending S))
- -> index ra (Pending_of ra.(Requestor) (TDM_pending S)) == 0
- -> let S' := (Default_arbitrate ta.+1).(Implementation_State) in
- ((TDM_counter S') == Next_cycle OZCycle) && ((TDM_request S') == Some ra).
- Proof.
- intros S HC HS HP Hi; unfold S in *; clear S.
- unfold TDM_counter, TDM_pending, TDM_request, TDM_slot in *.
- simpl; unfold Next_state.
- destruct (Default_arbitrate ta).(Implementation_State) as [s' c P | s' c P rb] eqn:HSS;
- move : HC HS => /eqP HC /eqP HS; subst; simpl in *.
- - destruct (Pending_of ra.(Requestor) P) as [ | rb] eqn:HPP; simpl.
- - apply seq_in_filer_in with (p := fun r => r.(Requestor) == ra.(Requestor)) in HP as HF.
- 2: trivial.
- contradict HF.
- rewrite /Pending_of in HPP.
- by rewrite HPP in_nil.
- - simpl in Hi.
- destruct (rb == ra) eqn:He.
- - move : He => /eqP He; subst; by rewrite !eq_refl.
- - contradict Hi.
- apply /negPn.
- rewrite lt0n_neq0.
- - trivial.
- - apply ltn0Sn.
- - contradict HSS; apply Not_Running_ZCycle.
- Qed.
-
- Lemma Request_running_in_slot ta ra:
- let S := (Default_arbitrate ta).(Implementation_State) in
- (TDM_request S) == Some ra
- -> (TDM_counter S) == Next_cycle OZCycle
- -> forall d, d < SL.-1
- -> let S' := (Default_arbitrate (ta + d)).(Implementation_State) in
- (nat_of_ord (TDM_counter S') == d.+1) && ((TDM_request S') == Some ra).
- Proof.
- intros S HR HC.
- unfold S in *; clear S; simpl.
- induction d; intros Hd.
- - rewrite -nat_of_counter_eq in HC; move : HC => /eqP HC.
- rewrite addn0 HR HC /Next_cycle //=.
- set x := 1 < SL.
- dependent destruction x;
- apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; intro; simpl.
- - trivial.
- - contradict x; by rewrite SL_one.
- - apply ltn_trans with (m := d) in Hd as Hd'.
- 2: apply ltnSn.
- apply IHd in Hd' as IH; clear Hd' IHd HC HR.
-
- unfold TDM_counter, TDM_request in *.
- move : IH => /andP [/eqP HC HR].
-
- rewrite addnS //= /Next_state.
- destruct (Default_arbitrate (ta + d)).(Implementation_State) as [s' c P | s' c P rb] eqn:HSS.
- - by contradict HR.
- - rewrite -HC.
- destruct (c == OZCycle) eqn:Hz, (c == OACT_date) eqn:Ha, (c == OCAS_date) eqn:Hc, (c == OLastCycle) eqn:Hl; simpl.
- all: rewrite -HC in Hd; apply Next_cycle_inc in Hd as HC'.
- all: try by rewrite HC' HR andbT.
-
- all: move : Hl => /eqP Hl; subst.
- all: contradict Hd; by rewrite /OLastCycle //= ltnn.
- Qed.
-
- Lemma Request_processing_starts ta ra:
- ra \in (Arrival_at ta)
- -> let S := (Default_arbitrate (Requestor_slot_start ta ra.(Requestor) + index ra (Pending_of ra.(Requestor) (TDM_pending (Default_arbitrate (Requestor_slot_start ta ra.(Requestor))).(Implementation_State))) * SN * SL)).(Implementation_State) in
- (ra \in TDM_pending S) && (index ra (Pending_of ra.(Requestor) (TDM_pending S)) == 0).
- Proof.
- intros HP.
- (* An arriving request always becomes pending *)
- apply Pending_on_arrival in HP.
-
- (* Any pending request at least remains pending until its requestors slot is reached *)
- apply Pending_requestor_slot_start with (tb := (Requestor_slot_start ta ra.(Requestor))) in HP.
- 3: apply leqnn.
- 2: apply Requestor_slot_start_leq.
-
- (* Any pending request ultimately gets to the head of the pending queue (index zero) *)
- apply Request_index_zero in HP; simpl in HP.
- exact HP.
- Qed.
-
- Lemma Request_processing ta ra d:
- ra \in (Arrival_at ta)
- -> d < SL.-1
- -> let i := index ra (Pending_of ra.(Requestor) (TDM_pending (Default_arbitrate (Requestor_slot_start ta ra.(Requestor))).(Implementation_State))) in
- let S' := (Default_arbitrate ((Requestor_slot_start ta ra.(Requestor) + i * SN * SL).+1 + d)).(Implementation_State) in
- (nat_of_ord (TDM_counter S') == d.+1) && ((TDM_request S') == Some ra).
- Proof.
- intros HA Hd.
-
- (* Any request eventually gets to the head of the pending queue *)
- apply Request_processing_starts in HA as HP; move : HP => /andP [HP HI].
-
- (* fold complex terms *)
- set i := index _ _ in HP.
- set t := Requestor_slot_start ta ra.(Requestor) + _ in HP.
- specialize (Request_slot_start_aligned ta ra.(Requestor) i) as HC.
- specialize (Request_slot_start_match ta ra.(Requestor) i) as HS.
-
- (* Any request at the head of the pending queue eventually starts to be processed *)
- apply Request_starts with (ra := ra) in HC as HR.
- 4: unfold i; exact HI.
- 3: exact HP.
- 2: exact HS.
- move : HR => /andP [HC' HR'].
-
- (* Any request is processed until the CAS date is reached *)
- apply Request_running_in_slot with (d := d) in HR' as HR''.
- 3: exact Hd.
- 2: exact HC'.
- exact HR''.
- Qed.
-
- Lemma Request_PRE ta ra:
- ra \in (Arrival_at ta)
- -> let i := index ra (Pending_of ra.(Requestor) (TDM_pending (Default_arbitrate (Requestor_slot_start ta ra.(Requestor))).(Implementation_State))) * SN * SL in
- let tc := ((Requestor_slot_start ta ra.(Requestor)) + i).+1 in
- (PRE_of_req ra tc) \in (Default_arbitrate tc).(Arbiter_Commands).
- Proof.
- intros HA.
-
- (* Any request eventually gets to the head of the pending queue *)
- apply Request_processing_starts in HA as HP; move : HP => /andP [HP HI].
-
- (* fold complex terms *)
- set i := index _ _ in HP.
- set t := Requestor_slot_start ta ra.(Requestor) + _ in HP.
- specialize (Request_slot_start_aligned ta ra.(Requestor) i) as HC.
- specialize (Request_slot_start_match ta ra.(Requestor) i) as HS.
- simpl; fold t in HC, HS; fold i t.
-
- rewrite /TDM_counter /TDM_slot /TDM_pending /Next_state in HC HS HP HI *.
- destruct (Default_arbitrate t).(Implementation_State) as [s' c P | s' c P rb] eqn:HSS;
- move : HC HS => /eqP HC /eqP HS; subst; simpl in *.
- - destruct (Pending_of ra.(Requestor) P) as [ | rb] eqn:HPP; simpl.
- - apply seq_in_filer_in with (p := fun r => r.(Requestor) == ra.(Requestor)) in HP as HF.
- 2: trivial.
- contradict HF.
- rewrite /Pending_of in HPP.
- by rewrite HPP in_nil.
- - rewrite in_cons.
- simpl in HI.
- destruct (rb == ra) eqn:He.
- - move : He => /eqP He; subst; by rewrite !eq_refl.
- - contradict HI.
- apply /negPn.
- rewrite lt0n_neq0.
- - trivial.
- - apply ltn0Sn.
- - contradict HSS; apply Not_Running_ZCycle.
- Qed.
-
- Lemma Request_ACT ta ra:
- ra \in (Arrival_at ta)
- -> let i:= index ra (Pending_of ra.(Requestor) (TDM_pending (Default_arbitrate (Requestor_slot_start ta ra.(Requestor))).(Implementation_State))) * SN * SL in
- let tc := (Requestor_slot_start ta ra.(Requestor) + i + ACT_date).+1 in
- (ACT_of_req ra tc) \in (Default_arbitrate tc).(Arbiter_Commands).
- Proof.
- intros HA.
-
- (* Any request is processed until the ACT date is reached *)
- apply Request_processing with (d := ACT_date.-1) in HA as HR.
- 2: rewrite ltn_predRL prednK; exact SL_ACT || exact ACT_pos.
- move : HR => /andP [HC HR].
- clear HA.
-
- (* fold +1/-1s *)
- rewrite addSn -addnS in HC HR.
- rewrite prednK in HC HR.
- 2: exact ACT_pos.
-
- (* get the actual command *)
- simpl; set tc := _ + ACT_date.
- rewrite //= /Next_state /TDM_counter /TDM_request in HC HR *.
- destruct (Default_arbitrate tc).(Implementation_State) as [s' c P | s' c P rb] eqn:HSS;
- apply nat_of_ACT in HC; move : HC => /eqP HC; subst.
- - by contradict HR.
- - rewrite eq_refl //=.
- rewrite inj_eq in HR; exact ssrfun.Some_inj || move : HR => /eqP HR; subst.
- rewrite in_cons; apply /orP; by left.
- Qed.
-
- Lemma Request_CAS ta ra:
- ra \in (Arrival_at ta)
- -> let tc := (Requestor_slot_start ta ra.(Requestor) + index ra (Pending_of ra.(Requestor) (TDM_pending (Default_arbitrate (Requestor_slot_start ta ra.(Requestor))).(Implementation_State))) * SN * SL + CAS_date).+1 in
- (CAS_of_req ra tc) \in (Default_arbitrate tc).(Arbiter_Commands).
- Proof.
- intros HA.
-
- (* Any request is processed until the CAS date is reached *)
- apply Request_processing with (d := CAS_date.-1) in HA as HR.
- 2: rewrite ltn_predRL prednK; exact SL_CAS || exact CAS_pos.
- move : HR => /andP [HC HR].
- clear HA.
-
- (* fold +1/-1s *)
- rewrite addSn -addnS in HC HR.
- rewrite prednK in HC HR.
- 2: exact CAS_pos.
-
- (* get the actual command *)
- simpl; set tc := _ + CAS_date.
- rewrite //= /Next_state /TDM_counter /TDM_request in HC HR *.
- destruct (Default_arbitrate tc).(Implementation_State) as [s' c P | s' c P rb] eqn:HSS;
- apply nat_of_CAS in HC; move : HC => /eqP HC; subst.
- - by contradict HR.
- - rewrite eq_sym ACT_neq_CAS eq_refl //=.
- rewrite inj_eq in HR; exact ssrfun.Some_inj || move : HR => /eqP HR; subst.
- rewrite in_cons; apply /orP; by left.
- Qed.
-
- Lemma Requests_handled ta ra:
- ra \in (Arrival_at ta)
- -> exists tc, (CAS_of_req ra tc) \in ((Default_arbitrate tc).(Arbiter_Commands)).
- Proof.
- intros HA.
-
- (* get the CAS command *)
- apply Request_CAS in HA as H.
-
- (* finish the proof *)
- set tc := _.+1 in H.
- exists (tc).
- exact H.
- Qed.
-
- (* ------------------------------------------------------------------ *)
- (* --------------------- UNUSED LEMMAS ------------------------------ *)
- (* ------------------------------------------------------------------ *)
-
- (* TODO: remove *)
- Lemma TDM_PRE_distance t cmda cmdb:
- cmda.(CDate) < cmdb.(CDate) -> isPRE cmda -> isPRE cmdb
- -> cmda \in (Default_arbitrate t).(Arbiter_Commands)
- -> cmdb \in (Default_arbitrate t).(Arbiter_Commands)
- -> cmda.(CDate) + SL <= cmdb.(CDate).
- Proof.
- intros Hd Ha Hb Ia Ib.
- apply PRE_modulo_date in Ia as Hma.
- 2: exact Ha.
- apply PRE_modulo_date in Ib as Hmb. move : Hmb => /eqP Hmb.
- 2: exact Hb.
- rewrite <- Hmb, !Time_counter_modulo, eq_sym, nat_of_counter_eq in Hma.
- by apply Modulo_time_distance in Hma.
- Qed.
-
- (* TODO: remove *)
- Lemma TDM_ACT_distance t cmda cmdb:
- cmda.(CDate) < cmdb.(CDate) -> isACT cmda -> isACT cmdb ->
- cmda \in (Default_arbitrate t).(Arbiter_Commands) ->
- cmdb \in (Default_arbitrate t).(Arbiter_Commands)
- -> cmda.(CDate) + SL <= cmdb.(CDate).
- Proof.
- intros Hd Ha Hb Ia Ib.
- apply ACT_modulo_date in Ia as Hma.
- 2: exact Ha.
- apply ACT_modulo_date in Ib as Hmb. move : Hmb => /eqP Hmb.
- 2: exact Hb.
- rewrite <- Hmb, !Time_counter_modulo, eq_sym, nat_of_counter_eq in Hma.
- by apply Modulo_time_distance in Hma.
- Qed.
-
- (* TODO: remove *)
- Lemma TDM_CAS_distance t cmda cmdb:
- cmda.(CDate) < cmdb.(CDate) -> isCAS cmda -> isCAS cmdb ->
- cmda \in (Default_arbitrate t).(Arbiter_Commands) ->
- cmdb \in (Default_arbitrate t).(Arbiter_Commands)
- -> cmda.(CDate) + SL <= cmdb.(CDate).
- Proof.
- intros Hd Ha Hb Ia Ib.
- apply CAS_modulo_date in Ia as Hma.
- 2: exact Ha.
- apply CAS_modulo_date in Ib as Hmb. move : Hmb => /eqP Hmb.
- 2: exact Hb.
- rewrite <- Hmb, !Time_counter_modulo, eq_sym, nat_of_counter_eq in Hma.
- by apply Modulo_time_distance in Hma.
- Qed.
-
- (* TODO: remove *)
- Obligation Tactic := simpl.
-
- (* Define the arbitration function which creates the actual trace -- used to instantiate the arbiter *)
- Program Definition TDM_arbitrate t :=
- mkTrace
- (Default_arbitrate t).(Arbiter_Commands)
- (Default_arbitrate t).(Arbiter_Time)
- _ _ (* uniqueness and time *)
- _ _ _ _ _ _ _ _ _ _
- (Cmds_T_FAW_ok t)
- (Cmds_T_RRD_ok t)
- _ _ _ _ _ _ _ _ (* DDR4 proofs *)
- _ _.
- Admit Obligations.
-
- (* Instantiate the TDM arbiter *)
- Global Instance TDM_arbiter : Arbiter_t :=
- mkArbiter AF TDM_arbitrate Requests_handled Default_arbitrate_time_match.
-End TDM.
-
-Section Test.
- Program Instance BANK_CFG : Bank_configuration :=
- {
- BANKS := 2;
-
- T_BURST := 1;
- T_WL := 1;
-
- T_RRD := 3;
- T_FAW := 20;
-
- T_RC := 3;
- T_RP := 7;
- T_RCD := 2;
- T_RAS := 4;
- T_RTP := 2;
- T_WR := 1;
-
- T_RTW := 10;
- T_WTR := 10;
- T_CCD := 12;
-
- T_WTR_s := 10;
- T_WTR_l := 10;
- T_CCD_s := 10;
- T_CCD_l := 10;
- T_RRD_s := 10;
- T_RRD_l := 10;
- }.
-
- Program Instance TDM_CFG : TDM_configuration :=
- {
- SL := 100;
- SN := 3
- }.
-
- Existing Instance REQESTOR_CFG.
-
- Program Definition Req1 := mkReq (Ordinal (_ : 0 < SN)) 0 RD 0 0 0.
- Program Definition Req2 := mkReq (Ordinal (_ : 1 < SN)) 4 WR 0 1 0.
-
- Definition Input := [:: Req2; Req1].
-
- Program Instance AF : Arrival_function_t :=
- Default_arrival_function_t Input.
-
- (* Compute Arbitrate 300. *)
-End Test.
diff --git a/framework/DDR4/Trace.v b/framework/DDR4/Trace.v
deleted file mode 100644
index 07d1bb9a00149bd72bae1d753d7443c6905483a0..0000000000000000000000000000000000000000
--- a/framework/DDR4/Trace.v
+++ /dev/null
@@ -1,244 +0,0 @@
-Set Warnings "-notation-overridden,-parsing".
-Set Printing Projections.
-From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
-From sdram Require Export Commands Bank.
-
-Section Trace.
- Context {REQESTOR_CFG : Requestor_configuration}.
- Context {BANK_CFG : Bank_configuration}.
-
- Definition Same_Row (a b : Command_t) :=
- a.(Request).(Row) == b.(Request).(Row).
-
- Definition Same_Bank (a b : Command_t) :=
- a.(Request).(Bank) == b.(Request).(Bank).
-
- Definition Same_Bankgroup (a b : Command_t) :=
- a.(Request).(Bankgroup) == b.(Request).(Bankgroup).
-
- Fixpoint Diff_Bank_ a (S : seq Command_t) :=
- match S with
- | [::] => true
- | b::S' => (a != b) && (Diff_Bank_ a S')
- end.
-
- Fixpoint Diff_Bank (S : seq Command_t) :=
- match S with
- | [::] => true
- | a::S' => Diff_Bank_ a S' && Diff_Bank S'
- end.
-
- Definition ACT_to_ACT (a b : Command_t) :=
- isACT a && isACT b.
-
- Definition ACT_to_CAS (a b : Command_t) :=
- isACT a && isCAS b.
-
- Definition ACT_to_PRE (a b : Command_t) :=
- isACT a && isPRE b.
-
- Definition CRD_to_CRD (a b : Command_t) :=
- isCRD a && isCRD b.
-
- Definition CRD_to_CWR (a b : Command_t) :=
- isCRD a && isCWR b.
-
- Definition CRD_to_PRE (a b : Command_t) :=
- isCRD a && isPRE b.
-
- Definition CWR_to_CRD (a b : Command_t) :=
- isCWR a && isCRD b.
-
- Definition CWR_to_CWR (a b : Command_t) :=
- isCWR a && isCWR b.
-
- Definition CWR_to_PRE (a b : Command_t) :=
- isCWR a && isPRE b.
-
- Definition PRE_to_ACT (a b : Command_t) :=
- isPRE a && isACT b.
-
- Definition PRE_to_PRE (a b : Command_t) :=
- isPRE a && isPRE b.
-
- Definition isACT_or_PRE cmd :=
- (isACT cmd || isPRE cmd).
-
- Definition Before (a b : Command_t) :=
- a.(CDate) < b.(CDate).
-
- Definition Before_at (a b : Command_t) :=
- a.(CDate) <= b.(CDate).
-
- Definition Apart (a b : Command_t) t :=
- a.(CDate) + t < b.(CDate).
-
- Definition Apart_at_least (a b : Command_t) t :=
- a.(CDate) + t <= b.(CDate).
-
- Definition Between (l : Commands_t) (a b : Command_t) : Commands_t :=
- [seq cmds <- l | (cmds.(CDate) > a.(CDate)) && (cmds.(CDate) < b.(CDate))].
-
- Definition isPREtoBank cmd bank :=
- match cmd.(CKind) with
- | PREA => true
- | PRE => cmd.(Request).(Bank) == bank
- | _ => false
- end.
-
- Record Trace_t := mkTrace
- {
- Commands : Commands_t;
- Time : nat;
-
- (* All commands must be uniq *)
- Cmds_uniq : uniq Commands;
-
- (* All commands have to occur before the current time instant *)
- Cmds_time_ok : forall cmd, cmd \in Commands -> cmd.(CDate) <= Time;
-
- (* ------------------------------------------------------------------------- *)
- (* -------------------Timing constraints ----------------------------------- *)
- (* ------------------------------------------------------------------------- *)
-
- (* Ensure that the time between an ACT and a CAS commands respects T_RCD *)
- Cmds_T_RCD_ok : forall a b, a \in Commands -> b \in Commands ->
- ACT_to_CAS a b -> Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RCD;
-
- (* Ensure that the time between a PRE and an ACT commands respects T_RP *)
- Cmds_T_RP_ok : forall a b, a \in Commands -> b \in Commands ->
- PRE_to_ACT a b -> Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RP;
-
- (* 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_at_least a b T_RC;
-
- (* Maximum interval between ACT and PRE is T_RAS *)
- Cmds_T_RAS_ok : forall a b, a \in Commands -> b \in Commands ->
- isACT a -> isPRE b \/ isPREA b -> Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RAS;
-
- (* RL *)
- (* WL *)
-
- (* Ensure that the time between a CRD and a PRE commands respects T_RTP *)
- Cmds_T_RTP_ok : forall a b, a \in Commands -> b \in Commands ->
- CRD_to_PRE a b -> Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RTP;
-
- (* Ensure that the time between a CWR and a PRE commands respects T_WR + T_WL + T_BURST *)
- Cmds_T_WTP_ok : forall a b, a \in Commands -> b \in Commands ->
- CWR_to_PRE a b -> Same_Bank a b -> Before a b ->
- Apart_at_least a b (T_WR + T_WL + T_BURST);
-
- (* ---------------------------------------------------------------------------------- *)
-
- (* Where is the RTW value this is a sum of different values *)
- Cmds_T_RtoW_ok : forall a b, a \in Commands -> b \in Commands ->
- CRD_to_CWR a b -> Before a b ->
- Apart_at_least a b T_RTW;
-
- (* Ensure that the time between a CWR and a CRD commands respects T_WTR + T_WL + T_BURST *)
- Cmds_T_WtoR_ok : forall a b, a \in Commands -> b \in Commands ->
- CWR_to_CRD a b -> Before a b ->
- Apart_at_least a b (T_WTR + T_WL + T_BURST);
-
- (* Ensure that the time between a CAS and a CAS commands respects T_CCD *)
- Cmds_T_CCD_RD_ok : forall a b, a \in Commands -> b \in Commands ->
- CRD_to_CRD a b -> Before a b ->
- Apart_at_least a b T_CCD;
-
- Cmds_T_CCD_WR_ok : forall a b, a \in Commands -> b \in Commands ->
- CWR_to_CWR a b -> Before a b ->
- Apart_at_least a b T_CCD;
-
- (* ---------------------------------------------------------------------------------- *)
-
- (* Ensure that the time between four ACT commands respects T_FAW *)
- Cmds_T_FAW_ok : forall a b c d,
- a \in Commands -> b \in Commands -> c \in Commands -> d \in Commands ->
- isACT a -> isACT b -> isACT c -> isACT d -> Diff_Bank [::a;b;c;d] ->
- Before a b -> Before b c -> Before c d ->
- Apart_at_least a d T_FAW;
-
- (* Ensure that the time between two ACT commands respects T_RRD *)
- Cmds_T_RRD_ok : forall a b, a \in Commands -> b \in Commands ->
- ACT_to_ACT a b -> ~~ Same_Bank a b -> Before a b ->
- Apart_at_least a b T_RRD;
-
- (* ------------------------------------------------------------------------- *)
- (* ------------------- REFRESH specifics ------------------------------------ *)
- (* ------------------------------------------------------------------------- *)
-
- (*
- Cmds_T_RFC_ok : forall a b, a \in Commands -> b \in Commands ->
- isREF a -> Before a b -> Apart_at_least a b T_RFC;
-
- Cmds_T_REFI_ok: forall a, a \in Commands -> isREF a -> exists (b : Command_t),
- (b \in Commands /\ Before a b /\ isREF b /\ b.(CDate) <= a.(CDate) + 9 * T_REFI);
- *)
-
- (* Write POs limiting pull ins & postponing *)
-
- (* ------------------------------------------------------------------------- *)
- (* ------------------- DDR4 specifics -------------------------------------- *)
- (* ------------------------------------------------------------------------- *)
-
- (* If the device is DDR3, then these constraints are the same as the ones defined above
- since all requests target the same bank-group and the constraints only admit one value *)
-
- Cmds_T_WtoR_DBG_ok : forall a b, a \in Commands -> b \in Commands ->
- CWR_to_CRD a b -> Same_Bankgroup a b -> Before a b ->
- Apart_at_least a b (T_WTR_s + T_WL + T_BURST);
-
- Cmds_T_WtoR_SBG_ok : forall a b, a \in Commands -> b \in Commands ->
- CWR_to_CRD a b -> ~~ Same_Bankgroup a b -> Before a b ->
- Apart_at_least a b (T_WTR_l + T_WL + T_BURST);
-
- Cmds_T_CCD_RD_short_ok :forall a b, a \in Commands -> b \in Commands ->
- CRD_to_CRD a b -> Same_Bankgroup a b -> Before a b ->
- Apart_at_least a b T_CCD_s;
-
- Cmds_T_CCD_WR_short_ok :forall a b, a \in Commands -> b \in Commands ->
- CWR_to_CWR a b -> Same_Bankgroup a b -> Before a b ->
- Apart_at_least a b T_CCD_s;
-
- Cmds_T_CCD_RD_long_ok : forall a b, a \in Commands -> b \in Commands ->
- ACT_to_ACT a b -> ~~ Same_Bankgroup a b -> Before a b ->
- Apart_at_least a b T_CCD_l;
-
- Cmds_T_CCD_WR_long_ok : forall a b, a \in Commands -> b \in Commands ->
- ACT_to_ACT a b -> ~~ Same_Bankgroup a b -> Before a b ->
- Apart_at_least a b T_CCD_l;
-
- Cmds_T_RRD_short_ok : forall a b, a \in Commands -> b \in Commands ->
- CWR_to_CRD a b -> ~~ Same_Bank a b -> Same_Bankgroup a b -> Before a b ->
- Apart_at_least a b T_RRD_s;
-
- Cmds_T_RRD_long_ok : forall a b, a \in Commands -> b \in Commands ->
- CWR_to_CRD a b -> ~~ Same_Bank a b -> ~~ Same_Bankgroup a b -> Before a b ->
- Apart_at_least a b T_RRD_l;
-
- (* ------------------------------------------------------------------------- *)
- (* ------------------------Correctness of the command protocol ------------- *)
- (* ------------------------------------------------------------------------- *)
-
- Cmds_ACT_ok: forall a b, a \in Commands -> b \in Commands ->
- isACT a \/ isCAS a -> isACT b -> Same_Bank a b -> Before a b ->
- exists c, (c \in Commands /\ isPRE c /\ Same_Bank a c /\ Before c b /\ ~ Before_at c a);
-
- (* All banks are precharged before a refresh *)
-
- (* Cmds_REF_ok : forall (banks : Bank_t) ref, ref \in Commands -> isREF ref ->
- exists pre, (forall act, act \in Commands -> isACT act -> (Before act pre \/ Before ref act)) /\
- pre \in Commands /\ (isPREtoBank pre banks) /\ Apart_at_least pre ref T_RP; *)
-
- (* Every CAS command is preceded by a matching ACT without another ACT or PRE in between *)
- Cmds_row_ok : forall b c, b \in Commands -> c \in Commands -> isCAS b -> isACT_or_PRE c ->
- Same_Bank b c -> Before c b ->
- exists a, a \in Commands /\ isACT a /\ Same_Bank a b /\ Same_Row a b /\ Before a b /\ Before_at c a
- }.
-End Trace.
diff --git a/framework/DDR4/Util.v b/framework/DDR4/Util.v
deleted file mode 100644
index 6b4088d4adea47a2e70d6fbb29d04871fa6188fa..0000000000000000000000000000000000000000
--- a/framework/DDR4/Util.v
+++ /dev/null
@@ -1,444 +0,0 @@
-Set Warnings "-notation-overridden,-parsing".
-Set Printing Projections.
-From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype div.
-
-Lemma nat_ltn_leq_pred m n :
- (m < n) -> (m <= n.-1).
-Proof.
-Admitted.
-
-Lemma nat_add_pred m n :
- (m + n).-1 = m + n.-1.
-Proof.
-Admitted.
-
-Lemma nat_ltn_add_rev m p:
- m < m + p -> p > 0.
-Proof.
- intros.
- induction p.
- { by rewrite addn0 ltnn in H. }
- { rewrite addnS leq_eqVlt in H.
- move: H => /orP [/eqP H | H].
- { move: H => /eqP H. rewrite eqSS in H.
- rewrite -{1}[m]add0n addnC eqn_add2l in H.
- move: H => /eqP H.
- by rewrite -H.
- }
- rewrite -[m.+1]addn1 -[(m + p).+1]addn1 ltn_add2r in H.
- apply IHp in H.
- apply ltn_trans with (n := p).
- exact H.
- done.
- }
-Qed.
-
-Lemma Queue_non_empty [T : eqType] (ra : T) (s : seq T):
- ra \in s -> s != [::].
-Proof.
- intros H.
- induction s.
- { discriminate H. }
- auto.
-Qed.
-
-Lemma nat_ltn_add n m:
- m > 0 -> n < n + m.
-Proof.
- intros.
- induction n.
- { by rewrite add0n. }
- rewrite -addnC !addnS.
- rewrite -[(m + n).+1]addn1 -[n.+1]addn1.
- rewrite ltn_add2r.
- by rewrite addnC.
-Qed.
-
-Lemma nat_add_ltn m n p:
- m > 0 -> m + n < p -> n < p.
-Proof.
- intros.
- induction n.
- { rewrite addn0 in H0; apply ltn_trans with (m := 0) in H0; (exact H0 || exact H). }
- apply ltn_trans with (m := n.+1) in H0.
- 2: {
- rewrite addnC.
- apply nat_ltn_add.
- exact H.
- }
- exact H0.
-Qed.
-
-Lemma nat_leq_addl m n p:
- m <= n -> m <= p + n.
-Proof.
- intros H.
- induction p.
- - by rewrite add0n.
- - rewrite addSn.
- apply ltnW.
- by rewrite ltnS.
-Qed.
-
-Lemma nat_leq_addr m n p:
- m <= n -> m <= n + p.
-Proof.
- intros H.
- induction p.
- - by rewrite addn0.
- - rewrite addnS.
- apply ltnW.
- by rewrite ltnS.
-Qed.
-
-Lemma nat_add_modn_sub n d s:
- 0 < d -> s < d -> n %% d <= s -> (n + (s - n %% d)) %% d = s.
-Proof.
- intros Hd Hs Hl.
- apply /eqP.
- rewrite -{2}(modn_small (m := s) (d := d)).
- 2: exact Hs.
- rewrite addnBCA.
- 3: exact Hl.
- 2: apply leq_mod.
- rewrite -{2}(addn0 s) eqn_modDl -(eqn_modDr (n %% d)) subnK.
- 2: apply leq_mod.
- rewrite add0n modn_mod eq_refl. exact isT.
-Qed.
-
-Lemma nat_add_modd_sub n d:
- 0 < d -> (n + (d - n %% d)) %% d = 0.
-Proof.
- intros H.
- apply /eqP.
- rewrite -(mod0n d) addnBCA.
- 3: apply ltnW; rewrite ltn_mod; exact H.
- 2: apply leq_mod.
- rewrite modnDl -(eqn_modDr (n %% d)) subnK.
- 2: apply leq_mod.
- rewrite add0n modn_mod eq_refl. exact isT.
-Qed.
-
-Lemma nat_add_modd_sub_div n d:
- 0 < d -> (n + (d - n %% d)) %/ d = (n %/ d).+1.
-Proof.
- intros H.
- apply /eqP.
- rewrite eq_sym eqn_div.
- 3: rewrite /dvdn nat_add_modd_sub;
- (exact H || rewrite eq_refl; exact isT).
- 2: exact H.
- rewrite addnBA.
- 2: apply ltnW; rewrite ltn_mod; exact H.
- rewrite -(eqn_add2l (n %% d)) addnBCA.
- 3: apply leq_trans with (n := n);
- (rewrite leq_mod || rewrite leq_addr); exact isT.
- 2: rewrite leqnn; exact isT.
-rewrite subnn addn0 mulSn -addnACl -divn_eq eq_refl. exact isT.
-Qed.
-
-Lemma nat_add_gt_1 m n:
- m > 0 -> n > 0 -> 1 < m + n.
-Proof.
- intros Hm Hn.
- induction (m).
- { discriminate Hm. }
- induction (n).
- { discriminate Hn. }
- rewrite addnS addnC addnS -ltn_predRL.
- by simpl.
-Qed.
-
-Lemma nat_ltlt_empty m n:
- 0 < m -> m.-1 < n -> n < m -> false.
-Proof.
- intros Hz Ha Hb.
- contradict Hb.
- apply /negP.
- rewrite <- leqNgt.
- by rewrite <- (prednK (n := m)).
-Qed.
-
-Lemma nat_eq_ltS m n :
- m = n -> m < n.+1.
-Proof.
- intros.
- induction n.
- { by rewrite H. }
- rewrite H; simpl. rewrite <- ltn_predRL; by simpl.
-Qed.
-
-Lemma nat_maxn_add m n x: ((maxn m n) + x) = (maxn (m + x) (n + x)).
-Proof.
- unfold maxn.
- destruct (m < n) eqn:Hlt, (m + x < n + x) eqn:Hltp; auto;
- contradict Hltp; by rewrite ltn_add2r Hlt.
-Qed.
-
-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_add_lt_add m1 m2 n1 n2: is_true ((m1 < m2) && (n1 < n2)) -> is_true (m1 + n1 < m2 + n2).
-Proof.
- intros.
- rewrite <- addn1. rewrite addnACl addnC.
- apply leq_add.
- - rewrite addnC addn1. by move : H => /andP /proj1 H.
- - apply ltnW. by move : H => /andP /proj2 H.
-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_lt_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.
- - rewrite <- (ltn_add2r x m o) in Hlt.
- by apply ltn_trans with (n := m + x) (m := n) (p := o + x) in Hlt.
- - done.
-Qed.
-
-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.
- - 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 seq_rem_id {T : eqType} (x y : T) S:
- x \in S -> x != y
- -> x \in rem y S.
-Proof.
- induction S; intros Hi He.
- - contradict Hi; by rewrite in_nil.
- - rewrite in_cons in Hi; move : Hi => /orP [/eqP Hi | Hi].
- - subst.
- move : He => /negPf He.
- by rewrite //= He in_cons eq_refl.
- - rewrite //=.
- destruct (a == y).
- - exact Hi.
- - apply IHS in Hi as IH.
- - by rewrite in_cons IH orbT.
- - exact He.
-Qed.
-
-Lemma seq_eq_cons_in {T : eqType} (x :T) S S':
- S = x::S' -> x \in S.
-Proof.
- intros He.
- rewrite He.
- by rewrite in_cons eq_refl orTb.
-Qed.
-
-Lemma seq_in_filer_in {T : eqType} (x : T) S p:
- is_true (p x) -> x \in S -> x \in (filter p S).
-Proof.
- intros Hp Hi.
- by rewrite mem_filter Hp Hi.
-Qed.
-
-Lemma seq_filter_eq_cons_p {T : eqType} (x :T) S S' p:
- filter p S = x::S' -> p x.
-Proof.
- induction S; intros Hf.
- - contradict Hf; discriminate.
- - destruct (a == x) eqn:He, (p a) eqn:Hp'.
- - move : He => /eqP He; by subst.
- - rewrite //= Hp' in Hf; apply IHS in Hf.
- contradict Hf.
- move : He => /eqP He; subst; by rewrite Hp'.
- - rewrite //= Hp' in Hf.
- move : Hf => /eqP Hf; rewrite eqseq_cons in Hf; move : Hf => /andP [He' _].
- contradict He'; by rewrite He.
- - rewrite //= Hp' in Hf; apply IHS in Hf; exact Hf.
-Qed.
-
-Lemma seq_filter_rem_id {T : eqType} (x : T) S p :
- p x = false -> filter p (rem x S) = filter p S.
-Proof.
- induction S; intros Hp.
- - done.
- - simpl.
- destruct (a == x) eqn:He, (p a) eqn:Hp'.
- - contradict Hp'; move : He => /eqP He; subst; by rewrite Hp.
- - move : He => /eqP He; subst; reflexivity.
- all: by rewrite //= Hp' IHS.
-Qed.
-
-Lemma seq_filter_rem {T : eqType} (x : T) S p:
- filter p (rem x S) = rem x (filter p S).
-Proof.
- induction S.
- - simpl. reflexivity.
- - simpl.
- destruct (a == x) eqn:He, (p a) eqn:Hp.
- - rewrite //= He. reflexivity.
- - rewrite -IHS seq_filter_rem_id //=; move : He => /eqP He; subst; exact Hp.
- - rewrite //= He Hp IHS. reflexivity.
- - rewrite //= Hp IHS. reflexivity.
-Qed.
-
-Lemma seq_index_zero_head {T : eqType} (x : T) S:
- x \in S -> index x S == 0 -> exists S', S = x :: S'.
-Proof.
- intros Hi HI.
- induction S.
- - contradict Hi. rewrite in_nil. exact notF.
- - rewrite in_cons in Hi. move : Hi => /orP [/eqP Hi | Hi]; exists S.
- - subst. reflexivity.
- - simpl in Hi.
- destruct (a == x) eqn:He.
- - move : He => /eqP He. subst. reflexivity.
- - contradict HI.
- simpl. rewrite He eqE. exact notF.
-Qed.
-
-Lemma eq_seq_consr {T : eqType} (s : seq T):
- forall x, (s != x::s).
-Proof.
- induction s; intros.
- - done.
- - rewrite eqseq_cons.
- specialize IHs with (x := a).
- move : IHs => /negbTE IHs.
- by rewrite IHs Bool.andb_false_r.
-Qed.
-
-Definition seq_sorted_pred T := T -> T -> bool.
-
-Local Fixpoint seq_sorted_rec {T : Type} (P : seq_sorted_pred T) x s :=
- match s with
- | [::] => true
- | x'::s' => if (P x x') then seq_sorted_rec P x' s'
- else false
- end.
-
-Definition seq_sorted {T : Type} (P : seq_sorted_pred T) s :=
- match s with
- | [::] => true
- | x'::s' => seq_sorted_rec P x' s'
- end.
-
-Lemma seq_sorted_tail {T : eqType} (P : seq_sorted_pred T) s x:
- (seq_sorted P (x::s)) -> (seq_sorted P s).
-Proof.
- intros Hs. simpl in Hs.
- induction s.
- - done.
- - simpl in *.
- destruct (P x a).
- - done.
- - by contradict Hs.
-Qed.
-
-Lemma seq_sorted_cons {T : eqType} (P : seq_sorted_pred T) s x:
- (seq_sorted P s) -> (forall y, y \in s -> P x y) -> (seq_sorted P (x::s)).
-Proof.
- induction s; intros Hs Hip.
- - done.
- - specialize Hip with (y := a).
- rewrite in_cons eq_refl orTb in Hip.
- by rewrite /= Hip //=.
-Qed.
-
-Lemma all_filter [T : eqType] a (p : pred T) S:
- all a S -> all a [seq x <- S | p x].
-Proof.
- intros.
- induction S.
- auto.
- simpl in *.
- destruct (p a0).
- simpl. apply /andP.
- split.
- move : H => /andP /proj1 H. auto.
- move : H => /andP /proj2 H. apply IHS in H. auto.
- move : H => /andP /proj2 H. apply IHS in H. auto.
-Qed.
-
-(* TODO replace by generic definition *)
-(* Definition pred2_t (T : eqType) := T -> T -> bool.
-
-Definition all_pred2 [T : eqType] (p : pred2_t T) S x :=
- all (p x) S.
-
-Lemma all_pred2_filter [T : eqType] (p2 : pred2_t T) (p : pred T) S (x : T):
- all_pred2 p2 S x -> all_pred2 p2 [seq y <- S | p y] x.
-Proof.
- unfold pred2_t.
- intros.
- by apply all_filter.
-Qed.
-
-Fixpoint all_pred2_recursive [T : eqType] (p2 : pred2_t T) S :=
- match S with
- | [::] => true
- | x::S' => all_pred2 p2 S' x &&
- all_pred2_recursive p2 S'
- end.
-
-Lemma all_pred2_recursive_filter [T : eqType] (p2 : pred2_t T) (p : pred T) S:
- all_pred2_recursive p2 S -> all_pred2_recursive p2 [seq x <- S | p x].
-Proof.
- induction S; intros; auto.
- simpl in *. move : H => /andP H.
- destruct (p a); simpl.
- apply /andP. split.
- apply proj1 in H. by apply all_filter.
- apply proj2 in H. by apply IHS in H.
- apply proj2 in H. by apply IHS in H.
-Qed. *)
-
-(* Lemma filter_forall_pred [T : eqType] S (p : pred T): forall z , z \in [seq y <- S | p y ] -> p z.
- intros.
- rewrite (mem_filter p z S) in H. by move : H => /andP /proj1.
-Qed.
- *)
diff --git a/framework/DDR4/_CoqProject b/framework/DDR4/_CoqProject
deleted file mode 100644
index ed8669089baa7f94ed053041c0285b0a38d1b155..0000000000000000000000000000000000000000
--- a/framework/DDR4/_CoqProject
+++ /dev/null
@@ -1,11 +0,0 @@
-INSTALLDEFAULTROOT = DDR4
--Q . DDR4
-
-Util.v
-System.v
-Requestor.v
-Bank.v
-Requests.v
-Commands.v
-Trace.v
-Arbiter.v
diff --git a/framework/DDR4/makefile b/framework/DDR4/makefile
deleted file mode 100644
index a7496e22df777de3ce60a5dc037845b942007ffe..0000000000000000000000000000000000000000
--- a/framework/DDR4/makefile
+++ /dev/null
@@ -1,870 +0,0 @@
-##########################################################################
-## # The Coq Proof Assistant / The Coq Development Team ##
-## v # Copyright INRIA, CNRS and contributors ##
-## <O___,, # (see version control and CREDITS file for authors & dates) ##
-## \VV/ ###############################################################
-## // # This file is distributed under the terms of the ##
-## # GNU Lesser General Public License Version 2.1 ##
-## # (see LICENSE file for the text of the license) ##
-##########################################################################
-## GNUMakefile for Coq 8.13.2
-
-# For debugging purposes (must stay here, don't move below)
-INITIAL_VARS := $(.VARIABLES)
-# To implement recursion we save the name of the main Makefile
-SELF := $(lastword $(MAKEFILE_LIST))
-PARENT := $(firstword $(MAKEFILE_LIST))
-
-# This file is generated by coq_makefile and contains many variable
-# definitions, like the list of .v files or the path to Coq
-include makefile.conf
-
-# Put in place old names
-VFILES := $(COQMF_VFILES)
-MLIFILES := $(COQMF_MLIFILES)
-MLFILES := $(COQMF_MLFILES)
-MLGFILES := $(COQMF_MLGFILES)
-MLPACKFILES := $(COQMF_MLPACKFILES)
-MLLIBFILES := $(COQMF_MLLIBFILES)
-CMDLINE_VFILES := $(COQMF_CMDLINE_VFILES)
-INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
-OTHERFLAGS := $(COQMF_OTHERFLAGS)
-COQ_SRC_SUBDIRS := $(COQMF_COQ_SRC_SUBDIRS)
-OCAMLLIBS := $(COQMF_OCAMLLIBS)
-SRC_SUBDIRS := $(COQMF_SRC_SUBDIRS)
-COQLIBS := $(COQMF_COQLIBS)
-COQLIBS_NOML := $(COQMF_COQLIBS_NOML)
-CMDLINE_COQLIBS := $(COQMF_CMDLINE_COQLIBS)
-LOCAL := $(COQMF_LOCAL)
-COQLIB := $(COQMF_COQLIB)
-DOCDIR := $(COQMF_DOCDIR)
-OCAMLFIND := $(COQMF_OCAMLFIND)
-CAMLFLAGS := $(COQMF_CAMLFLAGS)
-HASNATDYNLINK := $(COQMF_HASNATDYNLINK)
-OCAMLWARN := $(COQMF_WARN)
-
-makefile.conf: _CoqProject
- coq_makefile -f _CoqProject -o makefile
-
-# This file can be created by the user to hook into double colon rules or
-# add any other Makefile code he may need
--include makefile.local
-
-# Parameters ##################################################################
-#
-# Parameters are make variable assignments.
-# They can be passed to (each call to) make on the command line.
-# They can also be put in makefile.local once and for all.
-# For retro-compatibility reasons they can be put in the _CoqProject, but this
-# practice is discouraged since _CoqProject better not contain make specific
-# code (be nice to user interfaces).
-
-# Print shell commands (set to non empty)
-VERBOSE ?=
-
-# Time the Coq process (set to non empty), and how (see default value)
-TIMED?=
-TIMECMD?=
-# Use command time on linux, gtime on Mac OS
-TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)"
-ifneq (,$(TIMED))
-ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?))
-STDTIME?=command time -f $(TIMEFMT)
-else
-ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?))
-STDTIME?=gtime -f $(TIMEFMT)
-else
-STDTIME?=command time
-endif
-endif
-else
-STDTIME?=command time -f $(TIMEFMT)
-endif
-
-ifneq (,$(COQBIN))
-# add an ending /
-COQBIN:=$(COQBIN)/
-endif
-
-# Coq binaries
-COQC ?= "$(COQBIN)coqc"
-COQTOP ?= "$(COQBIN)coqtop"
-COQCHK ?= "$(COQBIN)coqchk"
-COQDEP ?= "$(COQBIN)coqdep"
-COQDOC ?= "$(COQBIN)coqdoc"
-COQPP ?= "$(COQBIN)coqpp"
-COQMKFILE ?= "$(COQBIN)coq_makefile"
-OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep"
-
-# Timing scripts
-COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py"
-COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py"
-COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py"
-BEFORE ?=
-AFTER ?=
-
-# FIXME this should be generated by Coq (modules already linked by Coq)
-CAMLDONTLINK=str,unix,dynlink,threads,zarith
-
-# OCaml binaries
-CAMLC ?= "$(OCAMLFIND)" ocamlc -c
-CAMLOPTC ?= "$(OCAMLFIND)" opt -c
-CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkpkg -dontlink $(CAMLDONTLINK)
-CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkpkg -dontlink $(CAMLDONTLINK)
-CAMLDOC ?= "$(OCAMLFIND)" ocamldoc
-CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack
-
-# DESTDIR is prepended to all installation paths
-DESTDIR ?=
-
-# Debug builds, typically -g to OCaml, -debug to Coq.
-CAMLDEBUG ?=
-COQDEBUG ?=
-
-# Extra packages to be linked in (as in findlib -package)
-CAMLPKGS ?=
-
-# Option for making timing files
-TIMING?=
-# Option for changing sorting of timing output file
-TIMING_SORT_BY ?= auto
-# Option for changing the fuzz parameter on the output file
-TIMING_FUZZ ?= 0
-# Option for changing whether to use real or user time for timing tables
-TIMING_REAL?=
-# Option for including the memory column(s)
-TIMING_INCLUDE_MEM?=
-# Option for sorting by the memory column
-TIMING_SORT_BY_MEM?=
-# Output file names for timed builds
-TIME_OF_BUILD_FILE ?= time-of-build.log
-TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log
-TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log
-TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log
-TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log
-TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
-
-TGTS ?=
-
-# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
-ifdef DSTROOT
-DESTDIR := $(DSTROOT)
-endif
-
-# Substitution of the path by appending $(DESTDIR) if needed.
-# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments.
-windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1))
-destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1))
-
-# Installation paths of libraries and documentation.
-COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib)
-COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/user-contrib)
-COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable?
-
-########## End of parameters ##################################################
-# What follows may be relevant to you only if you need to
-# extend this Makefile. If so, look for 'Extension point' here and
-# put in makefile.local double colon rules accordingly.
-# E.g. to perform some work after the all target completes you can write
-#
-# post-all::
-# echo "All done!"
-#
-# in makefile.local
-#
-###############################################################################
-
-
-
-
-# Flags #######################################################################
-#
-# We define a bunch of variables combining the parameters.
-# To add additional flags to coq, coqchk or coqdoc, set the
-# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add.
-# To overwrite the default choice and set your own flags entirely, set the
-# {COQ,COQCHK,COQDOC}FLAGS variable.
-
-SHOW := $(if $(VERBOSE),@true "",@echo "")
-HIDE := $(if $(VERBOSE),,@)
-
-TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
-
-OPT?=
-
-# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d
-ifeq '$(OPT)' '-byte'
-USEBYTE:=true
-DYNOBJ:=.cma
-DYNLIB:=.cma
-else
-USEBYTE:=
-DYNOBJ:=.cmxs
-DYNLIB:=.cmxs
-endif
-
-# these variables are meant to be overridden if you want to add *extra* flags
-COQEXTRAFLAGS?=
-COQCHKEXTRAFLAGS?=
-COQDOCEXTRAFLAGS?=
-
-# these flags do NOT contain the libraries, to make them easier to overwrite
-COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS)
-COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS)
-COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS)
-
-COQDOCLIBS?=$(COQLIBS_NOML)
-
-# The version of Coq being run and the version of coq_makefile that
-# generated this makefile
-COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.13.2
-
-COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
-
-CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
-# ocamldoc fails with unknown argument otherwise
-CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
-CAMLFLAGS+=$(OCAMLWARN)
-
-ifneq (,$(TIMING))
-TIMING_ARG=-time
-ifeq (after,$(TIMING))
-TIMING_EXT=after-timing
-else
-ifeq (before,$(TIMING))
-TIMING_EXT=before-timing
-else
-TIMING_EXT=timing
-endif
-endif
-else
-TIMING_ARG=
-endif
-
-# Files #######################################################################
-#
-# We here define a bunch of variables about the files being part of the
-# Coq project in order to ease the writing of build target and build rules
-
-VDFILE := .makefile.d
-
-ALLSRCFILES := \
- $(MLGFILES) \
- $(MLFILES) \
- $(MLPACKFILES) \
- $(MLLIBFILES) \
- $(MLIFILES)
-
-# helpers
-vo_to_obj = $(addsuffix .o,\
- $(filter-out Warning: Error:,\
- $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1))))
-strip_dotslash = $(patsubst ./%,%,$(1))
-
-# without this we get undefined variables in the expansion for the
-# targets of the [deprecated,use-mllib-or-mlpack] rule
-with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1)))
-
-VO = vo
-VOS = vos
-
-VOFILES = $(VFILES:.v=.$(VO))
-GLOBFILES = $(VFILES:.v=.glob)
-HTMLFILES = $(VFILES:.v=.html)
-GHTMLFILES = $(VFILES:.v=.g.html)
-BEAUTYFILES = $(addsuffix .beautified,$(VFILES))
-TEXFILES = $(VFILES:.v=.tex)
-GTEXFILES = $(VFILES:.v=.g.tex)
-CMOFILES = \
- $(MLGFILES:.mlg=.cmo) \
- $(MLFILES:.ml=.cmo) \
- $(MLPACKFILES:.mlpack=.cmo)
-CMXFILES = $(CMOFILES:.cmo=.cmx)
-OFILES = $(CMXFILES:.cmx=.o)
-CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma)
-CMXAFILES = $(CMAFILES:.cma=.cmxa)
-CMIFILES = \
- $(CMOFILES:.cmo=.cmi) \
- $(MLIFILES:.mli=.cmi)
-# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just
-# a .mlg file
-CMXSFILES = \
- $(MLPACKFILES:.mlpack=.cmxs) \
- $(CMXAFILES:.cmxa=.cmxs) \
- $(if $(MLPACKFILES)$(CMXAFILES),,\
- $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs))
-
-# files that are packed into a plugin (no extension)
-PACKEDFILES = \
- $(call strip_dotslash, \
- $(foreach lib, \
- $(call strip_dotslash, \
- $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib))))
-# files that are archived into a .cma (mllib)
-LIBEDFILES = \
- $(call strip_dotslash, \
- $(foreach lib, \
- $(call strip_dotslash, \
- $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib))))
-CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES))
-CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES))
-OBJFILES = $(call vo_to_obj,$(VOFILES))
-ALLNATIVEFILES = \
- $(OBJFILES:.o=.cmi) \
- $(OBJFILES:.o=.cmx) \
- $(OBJFILES:.o=.cmxs)
-# trick: wildcard filters out non-existing files, so that `install` doesn't show
-# warnings and `clean` doesn't pass to rm a list of files that is too long for
-# the shell.
-NATIVEFILES = $(wildcard $(ALLNATIVEFILES))
-FILESTOINSTALL = \
- $(VOFILES) \
- $(VFILES) \
- $(GLOBFILES) \
- $(NATIVEFILES) \
- $(CMIFILESTOINSTALL)
-BYTEFILESTOINSTALL = \
- $(CMOFILESTOINSTALL) \
- $(CMAFILES)
-ifeq '$(HASNATDYNLINK)' 'true'
-DO_NATDYNLINK = yes
-FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx)
-else
-DO_NATDYNLINK =
-endif
-
-ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE)
-
-# Compilation targets #########################################################
-
-all:
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
-.PHONY: all
-
-all.timing.diff:
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES=""
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
-.PHONY: all.timing.diff
-
-ifeq (0,$(TIMING_REAL))
-TIMING_REAL_ARG :=
-TIMING_USER_ARG := --user
-else
-ifeq (1,$(TIMING_REAL))
-TIMING_REAL_ARG := --real
-TIMING_USER_ARG :=
-else
-TIMING_REAL_ARG :=
-TIMING_USER_ARG :=
-endif
-endif
-
-ifeq (0,$(TIMING_INCLUDE_MEM))
-TIMING_INCLUDE_MEM_ARG := --no-include-mem
-else
-TIMING_INCLUDE_MEM_ARG :=
-endif
-
-ifeq (1,$(TIMING_SORT_BY_MEM))
-TIMING_SORT_BY_MEM_ARG := --sort-by-mem
-else
-TIMING_SORT_BY_MEM_ARG :=
-endif
-
-make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE)
-make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE)
-make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
- $(HIDE)rm -f pretty-timed-success.ok
- $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE)
- $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed
-print-pretty-timed::
- $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
-print-pretty-timed-diff::
- $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
-ifeq (,$(BEFORE))
-print-pretty-single-time-diff::
- @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
- $(HIDE)false
-else
-ifeq (,$(AFTER))
-print-pretty-single-time-diff::
- @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
- $(HIDE)false
-else
-print-pretty-single-time-diff::
- $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
-endif
-endif
-pretty-timed:
- $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed
-.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff
-
-# Extension points for actions to be performed before/after the all target
-pre-all::
- @# Extension point
- $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\
- echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\
- echo "W: while the current Coq version is $(COQ_VERSION)";\
- fi
-.PHONY: pre-all
-
-post-all::
- @# Extension point
-.PHONY: post-all
-
-real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles)
-.PHONY: real-all
-
-real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff)
-.PHONY: real-all.timing.diff
-
-bytefiles: $(CMOFILES) $(CMAFILES)
-.PHONY: bytefiles
-
-optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
-.PHONY: optfiles
-
-# FIXME, see Ralf's bugreport
-# quick is deprecated, now renamed vio
-vio: $(VOFILES:.vo=.vio)
-.PHONY: vio
-quick: vio
- $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files")
-.PHONY: quick
-
-vio2vo:
- $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
- -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
-.PHONY: vio2vo
-
-# quick2vo is undocumented
-quick2vo:
- $(HIDE)make -j $(J) vio
- $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \
- viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \
- if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \
- done); \
- echo "VIO2VO: $$VIOFILES"; \
- if [ -n "$$VIOFILES" ]; then \
- $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \
- fi
-.PHONY: quick2vo
-
-checkproofs:
- $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
- -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
-.PHONY: checkproofs
-
-vos: $(VOFILES:%.vo=%.vos)
-.PHONY: vos
-
-vok: $(VOFILES:%.vo=%.vok)
-.PHONY: vok
-
-validate: $(VOFILES)
- $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^
-.PHONY: validate
-
-only: $(TGTS)
-.PHONY: only
-
-# Documentation targets #######################################################
-
-html: $(GLOBFILES) $(VFILES)
- $(SHOW)'COQDOC -d html $(GAL)'
- $(HIDE)mkdir -p html
- $(HIDE)$(COQDOC) \
- -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES)
-
-mlihtml: $(MLIFILES:.mli=.cmi)
- $(SHOW)'CAMLDOC -d $@'
- $(HIDE)mkdir $@ || rm -rf $@/*
- $(HIDE)$(CAMLDOC) -html \
- -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
-
-all-mli.tex: $(MLIFILES:.mli=.cmi)
- $(SHOW)'CAMLDOC -latex $@'
- $(HIDE)$(CAMLDOC) -latex \
- -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
-
-all.ps: $(VFILES)
- $(SHOW)'COQDOC -ps $(GAL)'
- $(HIDE)$(COQDOC) \
- -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \
- -o $@ `$(COQDEP) -sort $(VFILES)`
-
-all.pdf: $(VFILES)
- $(SHOW)'COQDOC -pdf $(GAL)'
- $(HIDE)$(COQDOC) \
- -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \
- -o $@ `$(COQDEP) -sort $(VFILES)`
-
-# FIXME: not quite right, since the output name is different
-gallinahtml: GAL=-g
-gallinahtml: html
-
-all-gal.ps: GAL=-g
-all-gal.ps: all.ps
-
-all-gal.pdf: GAL=-g
-all-gal.pdf: all.pdf
-
-# ?
-beautify: $(BEAUTYFILES)
- for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
- @echo 'Do not do "make clean" until you are sure that everything went well!'
- @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
-.PHONY: beautify
-
-# Installation targets ########################################################
-#
-# There rules can be extended in makefile.local
-# Extensions can't assume when they run.
-
-install:
- $(HIDE)code=0; for f in $(FILESTOINSTALL); do\
- if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
- done; exit $$code
- $(HIDE)for f in $(FILESTOINSTALL); do\
- df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
- if [ "$$?" != "0" -o -z "$$df" ]; then\
- echo SKIP "$$f" since it has no logical path;\
- else\
- install -d "$(COQLIBINSTALL)/$$df" &&\
- install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
- echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
- fi;\
- done
- $(HIDE)$(MAKE) install-extra -f "$(SELF)"
-install-extra::
- @# Extension point
-.PHONY: install install-extra
-
-install-byte:
- $(HIDE)for f in $(BYTEFILESTOINSTALL); do\
- df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\
- if [ "$$?" != "0" -o -z "$$df" ]; then\
- echo SKIP "$$f" since it has no logical path;\
- else\
- install -d "$(COQLIBINSTALL)/$$df" &&\
- install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\
- echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
- fi;\
- done
-
-install-doc:: html mlihtml
- @# Extension point
- $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
- $(HIDE)for i in html/*; do \
- dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
- install -m 0644 "$$i" "$$dest";\
- echo INSTALL "$$i" "$$dest";\
- done
- $(HIDE)install -d \
- "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
- $(HIDE)for i in mlihtml/*; do \
- dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
- install -m 0644 "$$i" "$$dest";\
- echo INSTALL "$$i" "$$dest";\
- done
-.PHONY: install-doc
-
-uninstall::
- @# Extension point
- $(HIDE)for f in $(FILESTOINSTALL); do \
- df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\
- instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
- rm -f "$$instf" &&\
- echo RM "$$instf" &&\
- (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \
- done
-.PHONY: uninstall
-
-uninstall-doc::
- @# Extension point
- $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html'
- $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
- $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml'
- $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
- $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true
-.PHONY: uninstall-doc
-
-# Cleaning ####################################################################
-#
-# There rules can be extended in makefile.local
-# Extensions can't assume when they run.
-
-clean::
- @# Extension point
- $(SHOW)'CLEAN'
- $(HIDE)rm -f $(CMOFILES)
- $(HIDE)rm -f $(CMIFILES)
- $(HIDE)rm -f $(CMAFILES)
- $(HIDE)rm -f $(CMOFILES:.cmo=.cmx)
- $(HIDE)rm -f $(CMXAFILES)
- $(HIDE)rm -f $(CMXSFILES)
- $(HIDE)rm -f $(CMOFILES:.cmo=.o)
- $(HIDE)rm -f $(CMXAFILES:.cmxa=.a)
- $(HIDE)rm -f $(MLGFILES:.mlg=.ml)
- $(HIDE)rm -f $(ALLDFILES)
- $(HIDE)rm -f $(NATIVEFILES)
- $(HIDE)find . -name .coq-native -type d -empty -delete
- $(HIDE)rm -f $(VOFILES)
- $(HIDE)rm -f $(VOFILES:.vo=.vio)
- $(HIDE)rm -f $(VOFILES:.vo=.vos)
- $(HIDE)rm -f $(VOFILES:.vo=.vok)
- $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
- $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
- $(HIDE)rm -f $(VFILES:.v=.glob)
- $(HIDE)rm -f $(VFILES:.v=.tex)
- $(HIDE)rm -f $(VFILES:.v=.g.tex)
- $(HIDE)rm -f pretty-timed-success.ok
- $(HIDE)rm -rf html mlihtml
-.PHONY: clean
-
-cleanall:: clean
- @# Extension point
- $(SHOW)'CLEAN *.aux *.timing'
- $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)
- $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE)
- $(HIDE)rm -f $(VOFILES:.vo=.v.timing)
- $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing)
- $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing)
- $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff)
- $(HIDE)rm -f .lia.cache .nia.cache
-.PHONY: cleanall
-
-archclean::
- @# Extension point
- $(SHOW)'CLEAN *.cmx *.o'
- $(HIDE)rm -f $(NATIVEFILES)
- $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx)
-.PHONY: archclean
-
-
-# Compilation rules ###########################################################
-
-$(MLIFILES:.mli=.cmi): %.cmi: %.mli
- $(SHOW)'CAMLC -c $<'
- $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
-
-$(MLGFILES:.mlg=.ml): %.ml: %.mlg
- $(SHOW)'COQPP $<'
- $(HIDE)$(COQPP) $<
-
-# Stupid hack around a deficient syntax: we cannot concatenate two expansions
-$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml
- $(SHOW)'CAMLC -c $<'
- $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
-
-# Same hack
-$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml
- $(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
- $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
-
-
-$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
- $(SHOW)'CAMLOPT -shared -o $@'
- $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
- -linkall -shared -o $@ $<
-
-$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
- $(SHOW)'CAMLC -a -o $@'
- $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
-
-$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
- $(SHOW)'CAMLOPT -a -o $@'
- $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^
-
-
-$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
- $(SHOW)'CAMLOPT -shared -o $@'
- $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
- -shared -linkall -o $@ $<
-
-$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx
- $(SHOW)'CAMLOPT -a -o $@'
- $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $<
-
-$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack
- $(SHOW)'CAMLC -a -o $@'
- $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
-
-$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
- $(SHOW)'CAMLC -pack -o $@'
- $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
-
-$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
- $(SHOW)'CAMLOPT -pack -o $@'
- $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
-
-# This rule is for _CoqProject with no .mllib nor .mlpack
-$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx
- $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
- $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
- -shared -o $@ $<
-
-ifneq (,$(TIMING))
-TIMING_EXTRA = > $<.$(TIMING_EXT)
-else
-TIMING_EXTRA =
-endif
-
-$(VOFILES): %.vo: %.v
- $(SHOW)COQC $<
- $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA)
-
-# FIXME ?merge with .vo / .vio ?
-$(GLOBFILES): %.glob: %.v
- $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
-
-$(VFILES:.v=.vio): %.vio: %.v
- $(SHOW)COQC -vio $<
- $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
-
-$(VFILES:.v=.vos): %.vos: %.v
- $(SHOW)COQC -vos $<
- $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
-
-$(VFILES:.v=.vok): %.vok: %.v
- $(SHOW)COQC -vok $<
- $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
-
-$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing
- $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing
- $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@"
-
-$(BEAUTYFILES): %.v.beautified: %.v
- $(SHOW)'BEAUTIFY $<'
- $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $<
-
-$(TEXFILES): %.tex: %.v
- $(SHOW)'COQDOC -latex $<'
- $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
-
-$(GTEXFILES): %.g.tex: %.v
- $(SHOW)'COQDOC -latex -g $<'
- $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
-
-$(HTMLFILES): %.html: %.v %.glob
- $(SHOW)'COQDOC -html $<'
- $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
-
-$(GHTMLFILES): %.g.html: %.v %.glob
- $(SHOW)'COQDOC -html -g $<'
- $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@
-
-# Dependency files ############################################################
-
-ifndef MAKECMDGOALS
- -include $(ALLDFILES)
-else
- ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),)
- -include $(ALLDFILES)
- endif
-endif
-
-.SECONDARY: $(ALLDFILES)
-
-redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV )
-
-GENMLFILES:=$(MLGFILES:.mlg=.ml)
-$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES)
-
-$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli
- $(SHOW)'CAMLDEP $<'
- $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
-
-$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml
- $(SHOW)'CAMLDEP $<'
- $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
-
-$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml
- $(SHOW)'CAMLDEP $<'
- $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
-
-$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib
- $(SHOW)'OCAMLLIBDEP $<'
- $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok)
-
-$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
- $(SHOW)'OCAMLLIBDEP $<'
- $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok)
-
-# If this makefile is created using a _CoqProject we have coqdep get
-# options from it. This avoids argument length limits for pathological
-# projects. Note that extra options might be on the command line.
-VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES)
-
-$(VDFILE): _CoqProject $(VFILES)
- $(SHOW)'COQDEP VFILES'
- $(HIDE)$(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
-
-# Misc ########################################################################
-
-byte:
- $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)"
-.PHONY: byte
-
-opt:
- $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)"
-.PHONY: opt
-
-# This is deprecated. To extend this makefile use
-# extension points and makefile.local
-printenv::
- $(warning printenv is deprecated)
- $(warning write extensions in makefile.local or include makefile.conf)
- @echo 'LOCAL = $(LOCAL)'
- @echo 'COQLIB = $(COQLIB)'
- @echo 'DOCDIR = $(DOCDIR)'
- @echo 'OCAMLFIND = $(OCAMLFIND)'
- @echo 'HASNATDYNLINK = $(HASNATDYNLINK)'
- @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)'
- @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)'
- @echo 'OCAMLFIND = $(OCAMLFIND)'
- @echo 'PP = $(PP)'
- @echo 'COQFLAGS = $(COQFLAGS)'
- @echo 'COQLIB = $(COQLIBS)'
- @echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
- @echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
-.PHONY: printenv
-
-# Generate a .merlin file. If you need to append directives to this
-# file you can extend the merlin-hook target in makefile.local
-.merlin:
- $(SHOW)'FILL .merlin'
- $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin
- $(HIDE)echo 'B $(COQLIB)' >> .merlin
- $(HIDE)echo 'S $(COQLIB)' >> .merlin
- $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
- echo 'B $(COQLIB)$(d)' >> .merlin;)
- $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
- echo 'S $(COQLIB)$(d)' >> .merlin;)
- $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;)
- $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;)
- $(HIDE)$(MAKE) merlin-hook -f "$(SELF)"
-.PHONY: merlin
-
-merlin-hook::
- @# Extension point
-.PHONY: merlin-hook
-
-# prints all variables
-debug:
- $(foreach v,\
- $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\
- $(.VARIABLES))),\
- $(info $(v) = $($(v))))
-.PHONY: debug
-
-.DEFAULT_GOAL := all
-
-# Local Variables:
-# mode: makefile-gmake
-# End:
diff --git a/framework/DDR3/Arbiter.v b/framework/DRAM/Arbiter.v
similarity index 97%
rename from framework/DDR3/Arbiter.v
rename to framework/DRAM/Arbiter.v
index e67251213091108fec8ccddee89dfee6e5b38184..b27d6b86cb120723881e3ffc24a2ef33031a9185 100644
--- a/framework/DDR3/Arbiter.v
+++ b/framework/DRAM/Arbiter.v
@@ -1,7 +1,7 @@
Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
-From DDR3 Require Export Trace.
+From DRAM Require Export Trace.
Section Arbiter.
diff --git a/framework/DDR3/Bank.v b/framework/DRAM/Bank.v
similarity index 97%
rename from framework/DDR3/Bank.v
rename to framework/DRAM/Bank.v
index 2d869eea442146c20f641d8cd0b661ff04f95ea0..d5fed31c19ffe528b7163d8519c575cd0ba5e579 100644
--- a/framework/DDR3/Bank.v
+++ b/framework/DRAM/Bank.v
@@ -1,7 +1,7 @@
Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
-From DDR3 Require Export System.
+From DRAM Require Export System.
Section Banks.
diff --git a/framework/DDR3/Commands.v b/framework/DRAM/Commands.v
similarity index 98%
rename from framework/DDR3/Commands.v
rename to framework/DRAM/Commands.v
index f6d001f3d1b34962c13dbebffc916a1ee053bf8f..6ad725801b71943260a9b7521183bdd582d0b8ae 100644
--- a/framework/DDR3/Commands.v
+++ b/framework/DRAM/Commands.v
@@ -1,6 +1,6 @@
Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
-From DDR3 Require Export Requests.
+From DRAM Require Export Requests.
Section Commands.
diff --git a/framework/DDR3/FIFO.v b/framework/DRAM/FIFO.v
similarity index 98%
rename from framework/DDR3/FIFO.v
rename to framework/DRAM/FIFO.v
index aac58469c3a0423355dde510cfdf346389919474..03fa9e4b6327eca424d6fc2a5ec708215061ac1f 100644
--- a/framework/DDR3/FIFO.v
+++ b/framework/DRAM/FIFO.v
@@ -3,7 +3,7 @@ Set Printing Projections.
From mathcomp Require Export fintype div.
Require Import Program.
-From DDR3 Require Export ImplementationInterface.
+From DRAM Require Export ImplementationInterface.
Section FIFO.
diff --git a/framework/DDR3/FIFO_extraction.v b/framework/DRAM/FIFO_extraction.v
similarity index 93%
rename from framework/DDR3/FIFO_extraction.v
rename to framework/DRAM/FIFO_extraction.v
index 4ee4a45ecb3f17279d918a4cad31a2227e888909..0327eccf0d5ebe7e4b46dd2c39c27ad464c7829e 100644
--- a/framework/DDR3/FIFO_extraction.v
+++ b/framework/DRAM/FIFO_extraction.v
@@ -1,7 +1,7 @@
Set Warnings "-notation-overridden,-parsing".
Unset Extraction Optimize.
-From DDR3 Require Export FIFO.
+From DRAM Require Export FIFO.
From Coq Require Extraction.
From Coq Require Import Arith.
diff --git a/framework/DDR3/FIFO_proofs.v b/framework/DRAM/FIFO_proofs.v
similarity index 99%
rename from framework/DDR3/FIFO_proofs.v
rename to framework/DRAM/FIFO_proofs.v
index 8d8a9b8dd0a41555d909f52daba5d13885b2ccb5..075fa262cf9a1a905318f3ae5adb2f45d0197264 100644
--- a/framework/DDR3/FIFO_proofs.v
+++ b/framework/DRAM/FIFO_proofs.v
@@ -3,7 +3,7 @@ Set Printing Projections.
From mathcomp Require Export fintype div.
Require Import Program.
-From DDR3 Require Export FIFO.
+From DRAM Require Export FIFO.
Section FIFOPROOFS.
diff --git a/framework/DDR3/FIFO_sim.v b/framework/DRAM/FIFO_sim.v
similarity index 96%
rename from framework/DDR3/FIFO_sim.v
rename to framework/DRAM/FIFO_sim.v
index 203e9d9cbfba5ea3350844b59fea0e0018c8ac46..46c9789cfbccc90fde7a0cda31caaa2f56a2960f 100644
--- a/framework/DDR3/FIFO_sim.v
+++ b/framework/DRAM/FIFO_sim.v
@@ -3,7 +3,7 @@ Set Printing Projections.
From mathcomp Require Export fintype div.
Require Import Program.
-From DDR3 Require Export FIFO_proofs.
+From DRAM Require Export FIFO_proofs.
Section FIFOsim.
diff --git a/framework/DDR3/ImplementationInterface.v b/framework/DRAM/ImplementationInterface.v
similarity index 98%
rename from framework/DDR3/ImplementationInterface.v
rename to framework/DRAM/ImplementationInterface.v
index 7eb0389f19ceb7a9d880df0615301cfaf6c3d803..0a0904f8f62374e285c5dc539b4962d4232818e1 100644
--- a/framework/DDR3/ImplementationInterface.v
+++ b/framework/DRAM/ImplementationInterface.v
@@ -1,6 +1,6 @@
Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
-From DDR3 Require Export Arbiter.
+From DRAM Require Export Arbiter.
Section ImplementationInterface.
@@ -8,7 +8,7 @@ Section ImplementationInterface.
Class Arbiter_configuration :=
{
State_t : Type;
- }.
+ }.gi
Context {REQESTOR_CFG : Requestor_configuration}.
Context {ARBITER_CFG : Arbiter_configuration}.
diff --git a/framework/DDR3/README.md b/framework/DRAM/README.md
similarity index 100%
rename from framework/DDR3/README.md
rename to framework/DRAM/README.md
diff --git a/framework/DDR3/Requestor.v b/framework/DRAM/Requestor.v
similarity index 100%
rename from framework/DDR3/Requestor.v
rename to framework/DRAM/Requestor.v
diff --git a/framework/DDR3/Requests.v b/framework/DRAM/Requests.v
similarity index 97%
rename from framework/DDR3/Requests.v
rename to framework/DRAM/Requests.v
index ce2b344c9ebeffb002400fbc3bf125299c53d672..f4e28e20ff2ef2d022d83f96a60df29807702704 100644
--- a/framework/DDR3/Requests.v
+++ b/framework/DRAM/Requests.v
@@ -1,7 +1,7 @@
Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
From mathcomp Require Export ssreflect eqtype.
-From DDR3 Require Export Util System Requestor Bank.
+From DRAM Require Export Util System Requestor Bank.
Section Requests.
diff --git a/framework/DDR3/System.v b/framework/DRAM/System.v
similarity index 100%
rename from framework/DDR3/System.v
rename to framework/DRAM/System.v
diff --git a/framework/DDR3/TDM.v b/framework/DRAM/TDM.v
similarity index 99%
rename from framework/DDR3/TDM.v
rename to framework/DRAM/TDM.v
index 6ddc974c805442c0fed4adb9fba6b3cc8de69038..e2413ea9236df75db7e1820c4d265ffb160e256a 100644
--- a/framework/DDR3/TDM.v
+++ b/framework/DRAM/TDM.v
@@ -1,6 +1,6 @@
Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
-From DDR3 Require Export ImplementationInterface.
+From DRAM Require Export ImplementationInterface.
From mathcomp Require Export fintype div.
Require Import Program.
diff --git a/framework/DDR3/TDM_extraction.v b/framework/DRAM/TDM_extraction.v
similarity index 100%
rename from framework/DDR3/TDM_extraction.v
rename to framework/DRAM/TDM_extraction.v
diff --git a/framework/DDR3/TDM_proofs.v b/framework/DRAM/TDM_proofs.v
similarity index 99%
rename from framework/DDR3/TDM_proofs.v
rename to framework/DRAM/TDM_proofs.v
index 9874586d650482114a95e0424bd27b0220b9aa06..bd3d75d20e82e204722300ff605843b76694e981 100644
--- a/framework/DDR3/TDM_proofs.v
+++ b/framework/DRAM/TDM_proofs.v
@@ -4,7 +4,7 @@ Set Printing Projections.
From mathcomp Require Export fintype div.
Require Import Program.
Require Import Psatz Lia.
-From DDR3 Require Export TDM.
+From DRAM Require Export TDM.
Section TDMPROOFS.
diff --git a/framework/DDR3/TDM_sim.v b/framework/DRAM/TDM_sim.v
similarity index 96%
rename from framework/DDR3/TDM_sim.v
rename to framework/DRAM/TDM_sim.v
index 0fefeefbab335d974ac71b250c42c0ddce8c3941..c017d5f71b5e5e2216d1500672b7ab1352b87170 100644
--- a/framework/DDR3/TDM_sim.v
+++ b/framework/DRAM/TDM_sim.v
@@ -3,7 +3,7 @@ Set Printing Projections.
From mathcomp Require Export fintype div.
Require Import Program.
-From DDR3 Require Export TDM_proofs.
+From DRAM Require Export TDM_proofs.
Section Test.
diff --git a/framework/DDR3/Trace.v b/framework/DRAM/Trace.v
similarity index 99%
rename from framework/DDR3/Trace.v
rename to framework/DRAM/Trace.v
index 6253615dc6f0f3ebc591cedb690ee8be479de44b..6b249e526abdd3c80977491a46368882ea7f0010 100644
--- a/framework/DDR3/Trace.v
+++ b/framework/DRAM/Trace.v
@@ -1,7 +1,7 @@
Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
-From DDR3 Require Export Commands.
+From DRAM Require Export Commands.
Section Trace.
diff --git a/framework/DDR3/Util.v b/framework/DRAM/Util.v
similarity index 100%
rename from framework/DDR3/Util.v
rename to framework/DRAM/Util.v
diff --git a/framework/DDR3/_CoqProject b/framework/DRAM/_CoqProject
similarity index 79%
rename from framework/DDR3/_CoqProject
rename to framework/DRAM/_CoqProject
index 39a16ce2bac6251eb0959905f981d51484c9403c..315c72c67f5b6d6042d6afa51bf7164998dd40e7 100644
--- a/framework/DDR3/_CoqProject
+++ b/framework/DRAM/_CoqProject
@@ -1,5 +1,5 @@
-INSTALLDEFAULTROOT = DDR3
--Q . DDR3
+INSTALLDEFAULTROOT = DRAM
+-Q . DRAM
Util.v
System.v
diff --git a/framework/DDR3/haskell_gencode_fifo/App.hs b/framework/DRAM/haskell_gencode_fifo/App.hs
similarity index 100%
rename from framework/DDR3/haskell_gencode_fifo/App.hs
rename to framework/DRAM/haskell_gencode_fifo/App.hs
diff --git a/framework/DDR3/haskell_gencode_fifo/ForeignCommand.hsc b/framework/DRAM/haskell_gencode_fifo/ForeignCommand.hsc
similarity index 100%
rename from framework/DDR3/haskell_gencode_fifo/ForeignCommand.hsc
rename to framework/DRAM/haskell_gencode_fifo/ForeignCommand.hsc
diff --git a/framework/DDR3/haskell_gencode_fifo/ForeignCommand_t.h b/framework/DRAM/haskell_gencode_fifo/ForeignCommand_t.h
similarity index 100%
rename from framework/DDR3/haskell_gencode_fifo/ForeignCommand_t.h
rename to framework/DRAM/haskell_gencode_fifo/ForeignCommand_t.h
diff --git a/framework/DDR3/haskell_gencode_fifo/ForeignRequest.hsc b/framework/DRAM/haskell_gencode_fifo/ForeignRequest.hsc
similarity index 100%
rename from framework/DDR3/haskell_gencode_fifo/ForeignRequest.hsc
rename to framework/DRAM/haskell_gencode_fifo/ForeignRequest.hsc
diff --git a/framework/DDR3/haskell_gencode_fifo/ForeignRequest_t.h b/framework/DRAM/haskell_gencode_fifo/ForeignRequest_t.h
similarity index 100%
rename from framework/DDR3/haskell_gencode_fifo/ForeignRequest_t.h
rename to framework/DRAM/haskell_gencode_fifo/ForeignRequest_t.h
diff --git a/framework/DDR3/haskell_gencode_fifo/MCsimRequest.h b/framework/DRAM/haskell_gencode_fifo/MCsimRequest.h
similarity index 100%
rename from framework/DDR3/haskell_gencode_fifo/MCsimRequest.h
rename to framework/DRAM/haskell_gencode_fifo/MCsimRequest.h
diff --git a/framework/DDR3/haskell_gencode_fifo/README.md b/framework/DRAM/haskell_gencode_fifo/README.md
similarity index 100%
rename from framework/DDR3/haskell_gencode_fifo/README.md
rename to framework/DRAM/haskell_gencode_fifo/README.md
diff --git a/framework/DDR3/haskell_gencode_fifo/main.cpp b/framework/DRAM/haskell_gencode_fifo/main.cpp
similarity index 100%
rename from framework/DDR3/haskell_gencode_fifo/main.cpp
rename to framework/DRAM/haskell_gencode_fifo/main.cpp
diff --git a/framework/DDR3/haskell_gencode_fifo/makefile b/framework/DRAM/haskell_gencode_fifo/makefile
similarity index 100%
rename from framework/DDR3/haskell_gencode_fifo/makefile
rename to framework/DRAM/haskell_gencode_fifo/makefile
diff --git a/framework/DDR3/haskell_gencode_tdm/App.hs b/framework/DRAM/haskell_gencode_tdm/App.hs
similarity index 99%
rename from framework/DDR3/haskell_gencode_tdm/App.hs
rename to framework/DRAM/haskell_gencode_tdm/App.hs
index 6f20afd1915b68263b14e87765f40feccfd97551..0c4776a690ce8ca0c31bc042528d4228fc3f5f27 100644
--- a/framework/DDR3/haskell_gencode_tdm/App.hs
+++ b/framework/DRAM/haskell_gencode_tdm/App.hs
@@ -61,7 +61,7 @@ tdm_init_state_genstate :: [ForeignRequest.ForeignRequest_t] -> IO (TDM.TDM_stat
tdm_init_state_genstate reqlist = do
coq_list <- convertReqList reqlist
-- this should be arguments eventually
- -- using values from DDR3 800E
+ -- using values From DRAM 800E
let bkcfg = Bank.Build_Bank_configuration 2 4 5 4 20 21 6 6 15 4 6 7 4 4 10 10 10 10 10 10
-- let reqcfg = (TDM.unsafeCoerce CInt)
let tdmcfg = TDM.Build_TDM_configuration 24 2
diff --git a/framework/DDR3/haskell_gencode_tdm/ForeignCommand.hsc b/framework/DRAM/haskell_gencode_tdm/ForeignCommand.hsc
similarity index 100%
rename from framework/DDR3/haskell_gencode_tdm/ForeignCommand.hsc
rename to framework/DRAM/haskell_gencode_tdm/ForeignCommand.hsc
diff --git a/framework/DDR3/haskell_gencode_tdm/ForeignCommand_t.h b/framework/DRAM/haskell_gencode_tdm/ForeignCommand_t.h
similarity index 100%
rename from framework/DDR3/haskell_gencode_tdm/ForeignCommand_t.h
rename to framework/DRAM/haskell_gencode_tdm/ForeignCommand_t.h
diff --git a/framework/DDR3/haskell_gencode_tdm/ForeignRequest.hsc b/framework/DRAM/haskell_gencode_tdm/ForeignRequest.hsc
similarity index 100%
rename from framework/DDR3/haskell_gencode_tdm/ForeignRequest.hsc
rename to framework/DRAM/haskell_gencode_tdm/ForeignRequest.hsc
diff --git a/framework/DDR3/haskell_gencode_tdm/ForeignRequest_t.h b/framework/DRAM/haskell_gencode_tdm/ForeignRequest_t.h
similarity index 100%
rename from framework/DDR3/haskell_gencode_tdm/ForeignRequest_t.h
rename to framework/DRAM/haskell_gencode_tdm/ForeignRequest_t.h
diff --git a/framework/DDR3/haskell_gencode_tdm/MCsimRequest.h b/framework/DRAM/haskell_gencode_tdm/MCsimRequest.h
similarity index 100%
rename from framework/DDR3/haskell_gencode_tdm/MCsimRequest.h
rename to framework/DRAM/haskell_gencode_tdm/MCsimRequest.h
diff --git a/framework/DDR3/haskell_gencode_tdm/README.md b/framework/DRAM/haskell_gencode_tdm/README.md
similarity index 100%
rename from framework/DDR3/haskell_gencode_tdm/README.md
rename to framework/DRAM/haskell_gencode_tdm/README.md
diff --git a/framework/DDR3/haskell_gencode_tdm/main.cpp b/framework/DRAM/haskell_gencode_tdm/main.cpp
similarity index 100%
rename from framework/DDR3/haskell_gencode_tdm/main.cpp
rename to framework/DRAM/haskell_gencode_tdm/main.cpp
diff --git a/framework/DDR3/haskell_gencode_tdm/makefile b/framework/DRAM/haskell_gencode_tdm/makefile
similarity index 100%
rename from framework/DDR3/haskell_gencode_tdm/makefile
rename to framework/DRAM/haskell_gencode_tdm/makefile