From 24ec44a821ccfd2bef24094eaddffa09cde5119b Mon Sep 17 00:00:00 2001 From: Felipe Lisboa <lisboafelipe5@gmail.com> Date: Thu, 8 Sep 2022 13:22:02 +0200 Subject: [PATCH] Merge DDR4/ and DDR3/ into a single framework --- framework/DDR4/Arbiter.v | 108 - framework/DDR4/Bank.v | 33 - framework/DDR4/Commands.v | 135 - framework/DDR4/ExtractionFIFO.v | 14 - framework/DDR4/ExtractionTDM.v | 14 - framework/DDR4/FIFO.v | 2374 ----------------- framework/DDR4/Requestor.v | 6 - framework/DDR4/Requests.v | 87 - framework/DDR4/System.v | 54 - framework/DDR4/TDM.v | 1510 ----------- framework/DDR4/Trace.v | 244 -- framework/DDR4/Util.v | 444 --- framework/DDR4/_CoqProject | 11 - framework/DDR4/makefile | 870 ------ framework/{DDR3 => DRAM}/Arbiter.v | 2 +- framework/{DDR3 => DRAM}/Bank.v | 2 +- framework/{DDR3 => DRAM}/Commands.v | 2 +- framework/{DDR3 => DRAM}/FIFO.v | 2 +- framework/{DDR3 => DRAM}/FIFO_extraction.v | 2 +- framework/{DDR3 => DRAM}/FIFO_proofs.v | 2 +- framework/{DDR3 => DRAM}/FIFO_sim.v | 2 +- .../{DDR3 => DRAM}/ImplementationInterface.v | 4 +- framework/{DDR3 => DRAM}/README.md | 0 framework/{DDR3 => DRAM}/Requestor.v | 0 framework/{DDR3 => DRAM}/Requests.v | 2 +- framework/{DDR3 => DRAM}/System.v | 0 framework/{DDR3 => DRAM}/TDM.v | 2 +- framework/{DDR3 => DRAM}/TDM_extraction.v | 0 framework/{DDR3 => DRAM}/TDM_proofs.v | 2 +- framework/{DDR3 => DRAM}/TDM_sim.v | 2 +- framework/{DDR3 => DRAM}/Trace.v | 2 +- framework/{DDR3 => DRAM}/Util.v | 0 framework/{DDR3 => DRAM}/_CoqProject | 4 +- .../haskell_gencode_fifo/App.hs | 0 .../haskell_gencode_fifo/ForeignCommand.hsc | 0 .../haskell_gencode_fifo/ForeignCommand_t.h | 0 .../haskell_gencode_fifo/ForeignRequest.hsc | 0 .../haskell_gencode_fifo/ForeignRequest_t.h | 0 .../haskell_gencode_fifo/MCsimRequest.h | 0 .../haskell_gencode_fifo/README.md | 0 .../haskell_gencode_fifo/main.cpp | 0 .../haskell_gencode_fifo/makefile | 0 .../{DDR3 => DRAM}/haskell_gencode_tdm/App.hs | 2 +- .../haskell_gencode_tdm/ForeignCommand.hsc | 0 .../haskell_gencode_tdm/ForeignCommand_t.h | 0 .../haskell_gencode_tdm/ForeignRequest.hsc | 0 .../haskell_gencode_tdm/ForeignRequest_t.h | 0 .../haskell_gencode_tdm/MCsimRequest.h | 0 .../haskell_gencode_tdm/README.md | 0 .../haskell_gencode_tdm/main.cpp | 0 .../haskell_gencode_tdm/makefile | 0 51 files changed, 17 insertions(+), 5921 deletions(-) delete mode 100644 framework/DDR4/Arbiter.v delete mode 100644 framework/DDR4/Bank.v delete mode 100644 framework/DDR4/Commands.v delete mode 100644 framework/DDR4/ExtractionFIFO.v delete mode 100644 framework/DDR4/ExtractionTDM.v delete mode 100644 framework/DDR4/FIFO.v delete mode 100644 framework/DDR4/Requestor.v delete mode 100644 framework/DDR4/Requests.v delete mode 100644 framework/DDR4/System.v delete mode 100644 framework/DDR4/TDM.v delete mode 100644 framework/DDR4/Trace.v delete mode 100644 framework/DDR4/Util.v delete mode 100644 framework/DDR4/_CoqProject delete mode 100644 framework/DDR4/makefile rename framework/{DDR3 => DRAM}/Arbiter.v (97%) rename framework/{DDR3 => DRAM}/Bank.v (97%) rename framework/{DDR3 => DRAM}/Commands.v (98%) rename framework/{DDR3 => DRAM}/FIFO.v (98%) rename framework/{DDR3 => DRAM}/FIFO_extraction.v (93%) rename framework/{DDR3 => DRAM}/FIFO_proofs.v (99%) rename framework/{DDR3 => DRAM}/FIFO_sim.v (96%) rename framework/{DDR3 => DRAM}/ImplementationInterface.v (98%) rename framework/{DDR3 => DRAM}/README.md (100%) rename framework/{DDR3 => DRAM}/Requestor.v (100%) rename framework/{DDR3 => DRAM}/Requests.v (97%) rename framework/{DDR3 => DRAM}/System.v (100%) rename framework/{DDR3 => DRAM}/TDM.v (99%) rename framework/{DDR3 => DRAM}/TDM_extraction.v (100%) rename framework/{DDR3 => DRAM}/TDM_proofs.v (99%) rename framework/{DDR3 => DRAM}/TDM_sim.v (96%) rename framework/{DDR3 => DRAM}/Trace.v (99%) rename framework/{DDR3 => DRAM}/Util.v (100%) rename framework/{DDR3 => DRAM}/_CoqProject (79%) rename framework/{DDR3 => DRAM}/haskell_gencode_fifo/App.hs (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_fifo/ForeignCommand.hsc (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_fifo/ForeignCommand_t.h (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_fifo/ForeignRequest.hsc (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_fifo/ForeignRequest_t.h (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_fifo/MCsimRequest.h (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_fifo/README.md (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_fifo/main.cpp (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_fifo/makefile (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_tdm/App.hs (99%) rename framework/{DDR3 => DRAM}/haskell_gencode_tdm/ForeignCommand.hsc (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_tdm/ForeignCommand_t.h (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_tdm/ForeignRequest.hsc (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_tdm/ForeignRequest_t.h (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_tdm/MCsimRequest.h (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_tdm/README.md (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_tdm/main.cpp (100%) rename framework/{DDR3 => DRAM}/haskell_gencode_tdm/makefile (100%) diff --git a/framework/DDR4/Arbiter.v b/framework/DDR4/Arbiter.v deleted file mode 100644 index 0babd47..0000000 --- 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 e9b52b7..0000000 --- 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 6a0d4ef..0000000 --- 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 4e03ace..0000000 --- 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 307da70..0000000 --- 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 7da65ec..0000000 --- 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 f983405..0000000 --- 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 4aec13d..0000000 --- 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 c60be24..0000000 --- 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 cfb3036..0000000 --- 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 07d1bb9..0000000 --- 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 6b4088d..0000000 --- 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 ed86690..0000000 --- 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 a7496e2..0000000 --- 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 e672512..b27d6b8 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 2d869ee..d5fed31 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 f6d001f..6ad7258 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 aac5846..03fa9e4 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 4ee4a45..0327ecc 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 8d8a9b8..075fa26 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 203e9d9..46c9789 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 7eb0389..0a0904f 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 ce2b344..f4e28e2 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 6ddc974..e2413ea 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 9874586..bd3d75d 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 0fefeef..c017d5f 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 6253615..6b249e5 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 39a16ce..315c72c 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 6f20afd..0c4776a 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 -- GitLab