diff --git a/framework/DRAM/Core/Arbiter.v b/framework/DRAM/Core/Arbiter.v
index 8c56d19e52cc94fdf4c8d2d8fc4e14f32f1259d3..035e18b9521e1e01b0653cfd281f19c63555c934 100644
--- a/framework/DRAM/Core/Arbiter.v
+++ b/framework/DRAM/Core/Arbiter.v
@@ -52,9 +52,9 @@ Section Arbiter.
the completion date of reqb *)
-> exists txa txb, (CAS_of_req reqa txa \in (Arbitrate txa).(Commands))
&& (CAS_of_req reqb txb \in (Arbitrate txb).(Commands)) && (txa < txb)
-}.
+ }.
-Class W_SequentialConsistent_Arbiter {AF : Arrival_function_t} {AR : Arbiter_t} := mkWSeqARbiter {
+ Class W_SequentialConsistent_Arbiter {AF : Arrival_function_t} {AR : Arbiter_t} := mkWSeqARbiter {
R2_relaxed : forall ta reqa tb reqb,
reqa \in (Arrival_at ta) -> (* reqa arrives at ta *)
reqb \in (Arrival_at tb) -> (* reqb arrives at tb *)
@@ -67,7 +67,7 @@ Class W_SequentialConsistent_Arbiter {AF : Arrival_function_t} {AR : Arbiter_t}
exists txa txb,
(CAS_of_req reqa txa \in (Arbitrate txa).(Commands)) &&
(CAS_of_req reqb txb \in (Arbitrate txb).(Commands)) && (txa < txb)
-}.
+ }.
Definition Default_arrival_at Input t :=
[seq x <- Input | x.(Date) == t].
diff --git a/framework/DRAM/Core/BankMachine.v b/framework/DRAM/Core/BankMachine.v
index ad3e5e4f6cb3a6cca541c795c5108ea671bb1c6a..fda1b460df0f304cc65ad5ccec29adb85e485f8a 100644
--- a/framework/DRAM/Core/BankMachine.v
+++ b/framework/DRAM/Core/BankMachine.v
@@ -182,6 +182,8 @@ Section BankMachine.
) true (proj1_sig SS.(Banks)).
(* check if all banks are OK to be pre-charged *)
+ (* If alreadu IDLE ok ? *)
+ (* Some logic to not allow commands to be issued if PREA or REF are due -> already there ! *)
Definition checkPREA SS :=
@fold_right bool BankState_t
(fun bs r => if r then
diff --git a/framework/DRAM/Core/ImplementationInterface.v b/framework/DRAM/Core/ImplementationInterface.v
index 595b4ef69a57f5666fa9ab3ea012bfdb941f6a86..a4f52b759b0d5e772433772f5b958c093cddadad 100644
--- a/framework/DRAM/Core/ImplementationInterface.v
+++ b/framework/DRAM/Core/ImplementationInterface.v
@@ -25,8 +25,6 @@ Section ImplementationInterface.
Arbiter_Commands : Commands_t;
Arbiter_Time : nat;
Implementation_State : State_t;
-
-
}.
(* Computes the t_th state *)
diff --git a/framework/DRAM/Core/InterfaceSubLayer.v b/framework/DRAM/Core/InterfaceSubLayer.v
index 491fc3e62b65e256a58e1e3467ab234f12739bc2..2c8dd8f8218fee8e0e514737394d1c7ef13b3682 100644
--- a/framework/DRAM/Core/InterfaceSubLayer.v
+++ b/framework/DRAM/Core/InterfaceSubLayer.v
@@ -55,8 +55,14 @@ Section InterfaceSubLayer.
(* Schedule_In : forall m SYS_ST SCH_ST, m <> [] -> Schedule m SYS_ST SCH_ST \in m; *)
InitSchState : SchState_t;
- UpdatSchState : Command_kind_t -> ReqCmdMap_t -> SystemState_t -> SchState_t -> SchState_t;
+
+ (* UpdateSchState : forall reqmap SS SCH_ST,
+ let sch_cmd := Schedule reqmap SS SCH_ST in SchState_t; *)
+
+ UpdateSchState : ReqCmdMap_t -> SystemState_t -> SchState_t -> SchState_t;
}.
+
+ Check UpdateSchState.
Context {SCH : Scheduler_t}.
@@ -135,7 +141,7 @@ Section InterfaceSubLayer.
match SS' with
| None => (None,NOP)
| Some SS'valid =>
- let new_SchState := UpdatSchState sch_cmd cmdmap'' SS SchS in
+ let new_SchState := UpdateSchState cmdmap'' SS SchS in
let new_ImplSubLayerState := mkImplSubLayerState SS'valid updated_map new_SchState in
(Some new_ImplSubLayerState, sch_cmd)
end
diff --git a/framework/DRAM/Implementations/BM/FIFOimpSL/FIFOimpSL.v b/framework/DRAM/Implementations/BM/FIFOimpSL/FIFOimpSL.v
index 4347d7d91a07cad0a3ce66a482f678a2c7a93882..a99fe46397a212c96e5ad36a9a10abe5caae35d8 100644
--- a/framework/DRAM/Implementations/BM/FIFOimpSL/FIFOimpSL.v
+++ b/framework/DRAM/Implementations/BM/FIFOimpSL/FIFOimpSL.v
@@ -31,7 +31,7 @@ Section FIFOimpSL.
| None => NOP
end.
- Definition UpdatSchState (cmd : Command_kind_t) (cmd_map : ReqCmdMap_t) (SS : SystemState_t)
+ Definition UpdatSchState (cmd_map : ReqCmdMap_t) (SS : SystemState_t)
(FIFO_st : FIFO_internal_state) : FIFO_internal_state := tt.
#[global] Program Instance FIFO : Scheduler_t :=
diff --git a/framework/DRAM/Implementations/BM/RRimpSL/RRimpSL.v b/framework/DRAM/Implementations/BM/RRimpSL/RRimpSL.v
index ad5933061792a42f237fce8f24b04cc6fe130182..aba9629a2433a079ae8f66fc6bd12f60e18769d6 100644
--- a/framework/DRAM/Implementations/BM/RRimpSL/RRimpSL.v
+++ b/framework/DRAM/Implementations/BM/RRimpSL/RRimpSL.v
@@ -64,15 +64,16 @@ Section RRimpSL.
(* Can't update when the CAS is seen on the structure, but rather issued to the device *)
(* Maybe look at counters to detect a CWR or RD ?! *)
(* Give up slot if no pending request *)
- Definition UpdatSchState cmd cmd_map (SS : SystemState_t) (slot : Slot_t) : Slot_t :=
+ Definition UpdatSchState cmd_map (SS : SystemState_t) (slot : Slot_t) : Slot_t :=
+ let sch_cmd := RR_schedule cmd_map SS slot in
let cond1 := (* no commands belonging to the current slot owner *)
- ((find (fun cmd =>
- match cmd with
+ ((find (fun sch_cmd =>
+ match sch_cmd with
| CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r => r.(Requestor) == slot
| _ => false
end) cmd_map) == seq.size cmd_map) in
let cond2 := (* scheduled command is a CAS *)
- (match cmd with
+ (match sch_cmd with
| CRD _ | CRDA _ | CWR _ | CWRA _ => true
| _ => false
end) in
diff --git a/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL.v b/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL.v
index a0d9bd07526d312125203d1641ac309439e7f2dc..057edb298e31a3acff959eb6d2ec8bf2267ae50e 100644
--- a/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL.v
+++ b/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL.v
@@ -14,7 +14,23 @@ Section TDMimpSL.
SN_gt_1 : SN > 1;
SL : nat;
- SL_pos : SL > 0
+ SL_pos : SL > 0;
+
+ (* Necessary for TDM guarantees *)
+
+ (* -------------- Intra bank constraints ---------------- *)
+ (* SL is big enough to accomodate a PRE-ACT-CAS sequence *)
+ SL_enough : T_RP + T_RCD + 1 <= SL;
+ SL_WR_to_RD : T_WL + T_BURST + T_WTR_l <= SL;
+ SL_RD_to_WR : T_RTW <= SL;
+ SL_CAS_to_CAS : T_CCD_l <= SL;
+ SL_ACT_to_ACT_SB : T_RRD_l <= SL;
+
+ (* ------------- Inter-bank constraints ------------------ *)
+ SL_ACT_to_PRE : T_RAS - 1 <= SL;
+ SL_ACT_to_ACT_DB : T_RC - T_RP - 1 <= SL;
+ SL_RD_to_PRE : T_RTP - 1 <= SL;
+ SL_WR_to_PRE : T_WL + T_BURST + T_WR - 1 <= SL;
}.
Context {TDM_CFG : TDM_configuration}.
@@ -46,10 +62,9 @@ Section TDMimpSL.
(SS : SystemState_t)
(TDM_st : TDM_internal_state) : Command_kind_t :=
let slot := fst TDM_st in
- let cmd := seq.ohead (filter_cmd slot map) in
- match cmd with
- | Some cmd => cmd
- | None => NOP
+ match seq.ohead (filter_cmd slot map) with
+ | Some cmd => cmd
+ | None => NOP
end.
Lemma SN_pos : SN > 0.
@@ -74,8 +89,9 @@ Section TDMimpSL.
fun (P : nexts = true) => Ordinal (P : nexts)
else fun _ => OZSlot) Logic.eq_refl.
- Definition UpdatSchState (cmd : Command_kind_t) (cmd_map : ReqCmdMap_t) (SS : SystemState_t)
+ Definition UpdatSchState (cmd_map : ReqCmdMap_t) (SS : SystemState_t)
(TDM_st : TDM_internal_state) : TDM_internal_state :=
+ let cmd := TDM_schedule cmd_map SS TDM_st in
let '(s,c) := TDM_st in
((Next_slot s c),(Next_cycle c)).
diff --git a/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL_proofs.v b/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL_proofs.v
new file mode 100644
index 0000000000000000000000000000000000000000..7374eec7b5c6deb24f520686f453a269a07a5d13
--- /dev/null
+++ b/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL_proofs.v
@@ -0,0 +1,173 @@
+Set Printing Projections.
+
+From Hammer Require Import Hammer.
+From mathcomp Require Import ssreflect eqtype ssrbool ssrnat fintype div ssrZ zify tuple.
+From Coq Require Import Program List.
+From DRAM Require Import TDMimpSL.
+
+Set Hammer ReconstrLimit 15.
+
+Section TDMimpSL_proofs.
+
+ Context {SYS_CFG : System_configuration}.
+
+ (* Defined in InterfaceSubLayer *)
+ Existing Instance ARBITER_CFG.
+ Existing Instance ImplementationSubLayer.
+
+ (* Defined in TDMimpSL *)
+ Existing Instance REQUESTOR_CFG.
+ Existing Instance SCH_ST.
+
+ Context {SCH_OPT : SchedulingOptions_t}.
+ Context {TDM_CFG : TDM_configuration}.
+ Context {AF : Arrival_function_t}.
+
+ Notation "# t" := (Default_arbitrate t) (at level 0).
+
+ Fixpoint request_list (cmds : seq.seq Command_kind_t) :=
+ match cmds with
+ | [::] => [::]
+ | hd :: tl =>
+ match hd with
+ | CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r => r :: request_list tl
+ | _ => request_list tl
+ end
+ end.
+
+ (* Returns the list of pending requests *)
+ Definition TDM_pending t : seq.seq Request_t :=
+ request_list
+ (match # (t).(Implementation_State) with
+ | Some st => st.(CMap)
+ | None => [::]
+ end).
+
+ Definition get_req_from_cmdkind (cmd : Command_kind_t) :=
+ match cmd with
+ | CRD r | CRDA r | CWR r | CWRA r | ACT r | PRE r => Some r
+ | _ => None
+ end.
+
+ (* ------------------------------ PROOFS -------------------------------------- *)
+ Lemma request_list_rcons r x a :
+ r \in request_list x -> r \in request_list (x ++ [:: a]).
+ Proof.
+ induction x; simpl; intro H; [ discriminate H | ];
+ destruct a0; try by apply IHx in H.
+ all:
+ rewrite in_cons in H; move: H => /orP [/eqP H | H];
+ try (by subst r; rewrite in_cons eq_refl orTb).
+ all:
+ apply IHx in H as IH; clear IHx;
+ by rewrite in_cons IH orbT.
+ Qed.
+
+ Lemma request_list_id a i : request_list [:: cmdGEN a i] = [:: a].
+ Proof.
+ simpl; unfold cmdGEN; destruct SCH_OPT.(pP);
+ [ unfold cmdGEN_opage | unfold cmdGEN_cpage ];
+ set nth_bk := nth _ _ _;
+ destruct nth_bk; try reflexivity; [ destruct (_ == r) | ]; try reflexivity;
+ destruct a.(Kind); reflexivity.
+ Qed.
+
+ Lemma request_in_queue : forall r l tl I,
+ r \in l -> r \in request_list (map_arriving_req_to_cmd l tl I).
+ Proof.
+ intros r l tl i H.
+ induction l; [ discriminate H | ].
+ rewrite in_cons in H; move: H => /orP [/eqP H | H].
+ { subst r; clear IHl; simpl.
+ set ll := map_arriving_req_to_cmd _ _ _.
+ induction ll;
+ [ by rewrite app_nil_l request_list_id mem_seq1 eq_refl | ].
+ simpl; destruct a0; try (by rewrite in_cons IHll orbT);
+ assumption.
+ }
+ apply IHl in H as IH; clear IHl.
+ simpl. set ll := map_arriving_req_to_cmd _ _ _; fold ll in IH.
+ by apply request_list_rcons.
+ Qed.
+
+ Lemma request_in_queue_rem r ra l cmd :
+ get_req_from_cmdkind cmd == Some ra ->
+ r <> ra -> r \in request_list l -> r \in request_list (rem cmd l).
+ Proof.
+ intros Hreq Hdiff H.
+ induction l; simpl in *; [ discriminate H | ].
+ unfold get_req_from_cmdkind in Hreq.
+ destruct a, cmd; simpl; try discriminate Hreq.
+ all: rewrite inj_eq in Hreq; [ | exact ssrfun.Some_inj ]; move: Hreq => /eqP Hreq; subst.
+ all: try (apply IHl in H; clear IHl); try (by rewrite H).
+ all: rewrite in_cons in H; move: H => /orP [/eqP H | H ]; try subst;
+ try (by rewrite in_cons eq_refl orTb).
+ all: try (rewrite in_cons; apply IHl in H; clear IHl; by rewrite H orbT).
+ all: destruct (_ == _) eqn:Heq; simpl;
+ try (move: Heq => /eqP Heq; injection Heq as Hbug; rewrite Hbug in Hdiff; done);
+ try (by rewrite in_cons eq_refl orTb);
+ try assumption;
+ rewrite in_cons; apply IHl in H; by rewrite H orbT.
+ Qed.
+
+ Lemma request_in_queue_rem_ r ra l :
+ r <> ra -> r \in request_list l -> r \in request_list (rem (CRD ra) l).
+ Proof.
+ intros Hdiff H.
+ induction l; simpl in *; [ discriminate H | ].
+ destruct a; simpl.
+ { rewrite in_cons in H; move: H => /orP [/eqP H | H]; [ subst r | ].
+ { destruct (_ == _) eqn:Heq;
+ [ move: Heq => /eqP Heq; injection Heq as Hbug; rewrite Hbug in Hdiff; done | ].
+ simpl; by rewrite in_cons eq_refl orTb.
+ }
+ apply IHl in H as IH; clear IHl;
+ destruct (_ == _) eqn:Heq; [ assumption | ].
+ simpl; by rewrite in_cons IH orbT.
+ }
+ all:
+ try (rewrite in_cons in H; move: H => /orP [/eqP H | H]);
+ try subst r;
+ try rewrite in_cons; try (by rewrite eq_refl orTb); apply IHl in H as IH; clear IHl;
+ rewrite IH; try rewrite orbT; done.
+ Qed.
+
+ Lemma arriving_request_is_not_scheduled ra ta i :
+ let SS := i.(SystemState) in
+ let R := Arrival_at ta in
+ let sch_cmd := Schedule
+ (replace_nonrdy_cmds
+ (IssueREF (map_arriving_req_to_cmd R (map_running_req_to_cmd i.(CMap) SS) SS) SS) SS) SS i.(SchState) in
+ ra \in R -> get_req_from_cmdkind sch_cmd <> Some ra.
+ Proof.
+ cbv zeta; intros Hin; unfold get_req_from_cmdkind.
+ Admitted.
+
+ (* It either goes into the queue OR
+ starts being processed immediatly *)
+
+ (* Opt 1 : Change the algorithm such that arriving requests cannot
+ start being processed immediatly ? *)
+ Lemma Pending_on_arrival ta ra:
+ ra \in Arrival_at ta -> ra \in (TDM_pending ta).
+ Proof.
+ intros H; unfold TDM_pending.
+ destruct ta; simpl; [ by apply request_in_queue | ].
+ unfold Next_SL_state.
+ destruct # (ta).(Implementation_State) eqn:HS.
+ 2: { simpl. admit. (* Invalid state ... *) }
+ set SS' := SystemUpdate _ _; destruct SS' eqn:HS'; simpl.
+ 2: { simpl. admit. (* Invalid state ... *) }
+ set sch_cmd := TDM_schedule _ _ _; destruct sch_cmd eqn:Hcmd; simpl.
+ 5-9:
+ unfold IssueREF; destruct SCH_OPT.(pP);
+ destruct (_ == _); simpl; [ | destruct (_ == _) | | ]; by apply request_in_queue.
+ all:
+ apply request_in_queue_rem with (r := ra) (ra := r);
+ [ by unfold get_req_from_cmdkind; rewrite eq_refl | admit | ].
+ all:
+ unfold IssueREF; destruct SCH_OPT.(pP);
+ destruct (_ == _); simpl; [ | destruct (_ == _) | | ]; by apply request_in_queue.
+ Admitted.
+
+End TDMimpSL_proofs.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL_sim.v b/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL_sim.v
index dbc0ebb8efa161b0f348fc98f2367c30b0d9bcce..ef6b31edd26faf8e8edc37c358b9dfdbdfc2335a 100644
--- a/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL_sim.v
+++ b/framework/DRAM/Implementations/BM/TDMimpSL/TDMimpSL_sim.v
@@ -6,9 +6,14 @@ From DRAM Require Import TDMimpSL.
Section TDMimpSL_sim.
- Program Instance SYS_CFG : System_configuration := {
+ (* Try to reproduce the TDM example from Farouk's paper ? *)
+ (* Any advantages to start at 0 ? Yes, the proof of advancement, but quite hard ... *)
+ (* Try to do some progress with the advancement proof *)
+ (*
+
+ Program Instance SYS_CFG : System_configuration := {
BANKGROUPS := 1;
- BANKS := 2;
+ BANKS := 3;
T_BURST := 2;
T_WL := 2;
T_RRD_s := 1;
@@ -22,11 +27,68 @@ Section TDMimpSL_sim.
T_WR := 1;
T_RTW := 10;
T_WTR_s := 1;
- T_WTR_l := 10;
+ T_WTR_l := 2;
T_CCD_s := 1;
T_CCD_l := 12;
T_REFI := 100;
T_RFC := 6
+ }.
+ *)
+
+ Program Instance SYS_CFG : System_configuration :=
+ {
+ BANKGROUPS := 4;
+ BANKS := 16;
+
+ (* [Figure 105] always the same *)
+ T_BURST := 4; (* INTRA/INTER *)
+
+ (* [Figure 105] 1tCK write preamble mode, AL = 0
+ -- independent of BC4 or BL8
+ -- depends on write preamble mode (1tCK or 2tCK)
+ -- depends on AL (what is AL ?) *)
+ T_WL := 9;
+
+ (* ACT to ACT, same and different bank groups, exclusevely inter-bank
+ -- depends on page size, which depends on device density (total size) and configuration
+ see (https://www.micron.com/-/media/client/global/documents/products/data-sheet/dram/ddr4/16gb_ddr4_sdram.pdf)
+ *)
+ T_RRD_s := 4; (* [Page 189] Max (4nCK, 5 ns) -> 4nCK = 1/800MHz * 4 = 5ns -> max is 5 -> 4 cycles at 800MHz*)
+ T_RRD_l := 5; (* [Page 189] Max (4nCK, 6 ns) -> 4nCK = 1/800MHz * 4 = 5ns -> max is 6 -> 4.8 ~ 5 cyles at 800MHz *)
+
+ (* Intra/inter-bank: Four ACT delay window *)
+ T_FAW := 20; (* [Page 189] 25ns *)
+
+ (* ACT to ACT, intra bank *)
+ T_RC := 38; (* [Page 163] 47.5 ns *)
+
+ (* PRE to ACT, intra bank *)
+ T_RP := 10; (* [Page 163] 12.5 ns *)
+
+ (* ACT to CAS, intra bank *)
+ T_RCD := 10; (* [Page 163] 12.5 ns *)
+
+ (* ACT to PRE, intra bank *)
+ T_RAS := 28; (* [Page 163] 35.0 ns *)
+
+ (* RD to PRE, intra bank *)
+ T_RTP := 6; (* [Page 189] Max (4nCK, 7.5ns) -> 4nCK = 1/800MHz * 4 = 5ns -> max is 7 -> 5.6 ~ 6 cycles at 800MHz *)
+
+ (* Write recovery time: R data to PRE *)
+ T_WR := 12; (* [Page 189] 15 ns *)
+
+ (* Read to write, inter and intra bank *)
+ T_RTW := 8; (* [Page 94] T_RTW = RL + BL/2 - WL + 2tCK = 11 + 8/2 - 9 + 2 = 8 *)
+
+ (* End of write operation to read *)
+ T_WTR_s := 2; (* [Page 189] Max (2nCK,2.5ns) -> 2nCK = 1/800MHz * 2 = 2.5ns -> max is 2.5ns -> 2 cycles at 800MHz *)
+ T_WTR_l := 6; (* [Page 189] Nax (4nCK,7.5ns) -> 4nCK = 5ns -> max is 7.5ns -> 6 cycles at 800MHz *)
+
+ T_CCD_s := 4;
+ T_CCD_l := 5;
+
+ T_REFI := 2000; (* 6240 [Page 36] Refresh average time*)
+ T_RFC := 280; (* 280 [Page 36] *)
}.
(* The one defined in TDMimpSL *)
@@ -44,15 +106,57 @@ Section TDMimpSL_sim.
Instance SCH_OPT : SchedulingOptions_t := mkSCH_OPT opage.
(* There has to be at least two requestors *)
- Program Instance TDM_CFG : TDM_configuration := mkTDMCFG 2 _ 15 _.
+ Program Instance TDM_CFG : TDM_configuration := mkTDMCFG
+ 3 (* SN *)
+ _(* SN_gt 1*)
+ 27 (* SL *)
+ _ (* SL_pos *)
+ _ _ _ _ _ _
+ _ _ _.
+
+ Program Definition A0 := mkReq
+ (Ordinal (_ : 0 < SN)) (* Requestor *)
+ 4 (* Date *)
+ RD (* Kind *)
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 0) 50).
+
+ Program Definition B0 := mkReq
+ (Ordinal (_ : 1 < SN)) (* Requestor *)
+ 50 (* Date *)
+ WR (* Kind *)
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 1) 10).
- Program Definition Req1 := mkReq (Ordinal (_ : 0 < SN)) 1 RD
+ Program Definition C0 := mkReq
+ (Ordinal (_ : 2 < SN)) (* Requestor *)
+ 85 (* Date *)
+ RD (* Kind *)
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 2) 20).
+
+ Program Definition B1 := mkReq
+ (Ordinal (_ : 1 < SN)) (* Requestor *)
+ 145 (* Date *)
+ RD (* Kind *)
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 1) 10).
+
+ Program Definition C1 := mkReq
+ (Ordinal (_ : 2 < SN)) (* Requestor *)
+ 180 (* Date *)
+ WR (* Kind *)
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 2) 30).
+
+ Program Definition A1 := mkReq
+ (Ordinal (_ : 0 < SN)) (* Requestor *)
+ 190 (* Date *)
+ RD (* Kind *)
(mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 0) 5).
- Program Definition Req2 := mkReq (Ordinal (_ : 1 < SN)) 1 RD
- (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 1) 10).
+ Program Definition B2 := mkReq
+ (Ordinal (_ : 1 < SN)) (* Requestor *)
+ 220 (* Date *)
+ WR (* Kind *)
+ (mkAddress (Nat_to_bankgroup 0) (Nat_to_bank 1) 15).
- Definition Input := [:: Req1;Req2].
+ Definition Input := [:: A0;B0;C0;B1;C1;A1;B2].
Program Instance AF : Arrival_function_t := Default_arrival_function_t Input.
@@ -61,7 +165,9 @@ Section TDMimpSL_sim.
(* But it will keep waiting forever if the slot owner has no CAS *)
Instance TDM_arbiter : TestArbiter_t := mkTestArbiter AF TDM_arbitrate.
- Definition inst := 30.
+ Definition inst := 300.
+
+ Eval vm_compute in (Default_arbitrate inst).(Arbiter_Commands).
(* At 9 see the CRD from Req1 -> Change slot owner to 1 *)
(* At 11 see the CRD from Req2 -> Change slot owner to 0 *)
@@ -69,18 +175,16 @@ Section TDMimpSL_sim.
(* A (C)| A (C)| | C *)
(* 1 2 3 4 5 6 7 8 | 9 10 11 |12| 13 14 15 16 17 18 19 20*)
(* 0 0 0 0 0 0 0 0 | 1 1 1 | 0| 1 0 0 0 0 0 0 0*)
- Eval vm_compute in
+
+ (* Eval vm_compute in
map (fun '(a,b) => (nat_of_ord a, nat_of_ord b))
(map (fun x => (match (Default_arbitrate x).(Implementation_State) with
| Some st => (fst st.(SchState),snd st.(SchState))
| None => (Ordinal (_ : 0 < SN),Ordinal (_ : 0 < SL))
- end)) (seq.iota 1 30)).
-
- (* Still have a problem : Why ACT is only issued at cycle 7 ?! *)
- Eval vm_compute in (Default_arbitrate inst).(Arbiter_Commands).
+ end)) (seq.iota 1 30)). *)
Eval vm_compute in
- proj1_sig (match (Default_arbitrate inst).(Implementation_State) with
+ proj1_sig (match (Default_arbitrate 189).(Implementation_State) with
| Some st => st.(SystemState).(Banks)
| None => (exist _ (repeat InitBank BANKS) (repeat_size InitBank BANKS))
end).
diff --git a/framework/DRAM/Implementations/TS/FIFO/FIFO_proofs.v b/framework/DRAM/Implementations/TS/FIFO/FIFO_proofs.v
index 6b97ee80a7bd55887836493ece84a1732d18f05b..d65b901bd8cfb7050f07ca8ed6d10857a129e22b 100644
--- a/framework/DRAM/Implementations/TS/FIFO/FIFO_proofs.v
+++ b/framework/DRAM/Implementations/TS/FIFO/FIFO_proofs.v
@@ -1179,6 +1179,7 @@ Section Proofs.
&& isACT a && Same_Row a b && After a c && Before a b.
Proof.
intros Hb Hc iCb iPc SB cBb.
+
apply FIFO_CAS_date in Hb as H; [ | done ].
destruct H as [Hcb [Hrun_b Hreq_b]].
@@ -2198,15 +2199,15 @@ Section Proofs.
(Cmds_T_WtoR_DBG_ok t)
(Cmds_T_CCD_SBG_ok t)
(Cmds_T_CCD_DBG_ok t)
- _
- _
+ _ (* REFRESH *)
+ _ (* REFRESH *)
(Cmds_T_FAW_ok t)
(Cmds_T_RRD_SBG_ok t)
(Cmds_T_RRD_DBG_ok t)
(Cmds_ACT_ok t)
(Cmds_row_ok t)
(Cmds_initial t)
- _.
+ _. (* REFRESH *)
Admit Obligations.
diff --git a/framework/DRAM/Implementations/TS/TDM/TDM_proofs.v b/framework/DRAM/Implementations/TS/TDM/TDM_proofs.v
index 8b8fa9ee0493133ee6da73bf28c864557002a3fd..8f19dbe32808212b973e66270b06d67b05d147d2 100644
--- a/framework/DRAM/Implementations/TS/TDM/TDM_proofs.v
+++ b/framework/DRAM/Implementations/TS/TDM/TDM_proofs.v
@@ -2,8 +2,8 @@ Set Warnings "-notation-overridden,-parsing".
Set Printing Projections.
From mathcomp Require Export fintype div ssrZ zify.
-Require Import Program.
-From DRAM Require Export TDM.
+From Coq Require Import Program.
+From DRAM Require Export Util TDM.
Section TDMPROOFS.
@@ -19,7 +19,7 @@ Section TDMPROOFS.
(*************************************************************************************************)
(** UTILITY PROOFS *******************************************************************************)
(*************************************************************************************************)
-
+
Lemma ACT_neq_ZCycle:
(OACT_date == OZCycle) = false.
Proof.
@@ -149,8 +149,7 @@ Section TDMPROOFS.
cmd.(CDate) <= t.
Proof.
intros H.
- induction t.
- { by simpl in H. }
+ induction t; [ by simpl in H | ].
simpl in H; rewrite /Next_state in H.
destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (c == OZCycle) eqn:Hz, (c == OACT_date) eqn:Hact, (c == OCAS_date) eqn:Hcas,
(c == OLastCycle) eqn:Hlast; try destruct (Pending_of _ _) eqn:HP; simpl in H.
@@ -161,16 +160,14 @@ Section TDMPROOFS.
Lemma Date_gt_counter t:
TDM_counter (Default_arbitrate t).(Implementation_State) <= t.
Proof.
- induction t.
- { by simpl. }
- { simpl; rewrite /Next_state;
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (c == OZCycle) eqn:Hz,
- (c == OACT_date) eqn:Hact, (c == OCAS_date) eqn:Hcas, (c == OLastCycle) eqn:Hend; try destruct (Pending_of _ _) eqn:HP; simpl.
- all: rewrite /TDM_counter in IHt.
- all: try (rewrite /Next_cycle; set (Hc := c.+1 < SL); dependent destruction Hc).
- all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
- all: done.
- }
+ induction t; [ by simpl | ].
+ simpl; rewrite /Next_state;
+ destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (c == OZCycle) eqn:Hz,
+ (c == OACT_date) eqn:Hact, (c == OCAS_date) eqn:Hcas, (c == OLastCycle) eqn:Hend; try destruct (Pending_of _ _) eqn:HP; simpl.
+ all: rewrite /TDM_counter in IHt.
+ all: try (rewrite /Next_cycle; set (Hc := c.+1 < SL); dependent destruction Hc).
+ all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
+ all: done.
Qed.
Lemma TDM_next_cycle_modulo (c : Counter_t) t:
@@ -192,11 +189,8 @@ Section TDMPROOFS.
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.
+ - lia.
+ Qed.
Lemma Time_counter_modulo t:
(t %% SL) = TDM_counter (Default_arbitrate t).(Implementation_State).
@@ -267,14 +261,10 @@ Section TDMPROOFS.
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.
+ - 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:
@@ -334,18 +324,17 @@ Section TDMPROOFS.
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.
+ 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:
@@ -353,7 +342,7 @@ Section TDMPROOFS.
cmd.(CDate) %% SL == Next_cycle OACT_date.
Proof.
induction t.
- - done.
+ - 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);
@@ -497,11 +486,10 @@ Section TDMPROOFS.
Theorem Cmds_T_RCD_ok t a b:
a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- ACT_to_CAS a b -> Same_Bank a b -> Before a b ->
+ isACT a -> isCAS b -> Same_Bank a b -> Before a b ->
Apart_at_least a b T_RCD.
Proof.
- intros Ha Hb AtC SB aBb; rewrite /Apart_at_least.
- move : AtC => /andP [Aa Cb].
+ intros Ha Hb Aa Cb SB aBb; rewrite /Apart_at_least.
apply ACT_modulo_date in Ha as Ha'.
2: exact Aa. clear Aa.
apply CAS_modulo_date in Hb as Hb'.
@@ -560,11 +548,10 @@ Section TDMPROOFS.
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 ->
+ isPRE a -> isACT 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].
+ intros Ha Hb iPa iAb SB aBb.
apply PRE_modulo_date in Ha as Ha'.
2: exact iPa. clear iPa.
apply ACT_modulo_date in Hb as Hb'.
@@ -592,11 +579,10 @@ Section TDMPROOFS.
Theorem Cmds_T_RC_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 ->
+ isACT a -> isACT b -> Same_Bank a b -> Before a b ->
Apart_at_least a b T_RC.
Proof.
- intros Ha Hb AtA _ aBb.
- move : AtA => /andP [Aa Ab].
+ intros Ha Hb Aa Ab _ aBb.
apply ACT_modulo_date in Ha.
2: exact Aa. clear Aa.
apply ACT_modulo_date in Hb.
@@ -614,11 +600,10 @@ Section TDMPROOFS.
Theorem Cmds_T_RAS_ok t a b:
a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- ACT_to_PRE a b -> Same_Bank a b -> Before a b ->
+ isACT a -> isPRE b -> Same_Bank a b -> Before a b ->
Apart_at_least a b T_RAS.
Proof.
- intros Ha Hb Hty SB aBb; rewrite /Apart_at_least.
- rewrite /ACT_to_PRE in Hty; move : Hty => /andP [iAa iPb].
+ intros Ha Hb iAa iPb SB aBb; rewrite /Apart_at_least.
apply ACT_modulo_date in Ha.
2: exact iAa. clear iAa.
apply PRE_modulo_date in Hb.
@@ -677,8 +662,7 @@ Section TDMPROOFS.
specialize leq_add2r with (m := tb) (n := ta) (p := 0) as HH.
by rewrite -HH addn0 -leq_subLR H.
}
- rewrite -mulnA leq_pmull.
- all: done.
+ rewrite -mulnA leq_pmull; done.
Qed.
Lemma TDM_counter_last t:
@@ -713,8 +697,7 @@ Section TDMPROOFS.
all: rewrite /Next_slot; destruct (c0.+1 < SL) eqn:Hbug.
all: try (apply IHd in Hlt' as IH; by rewrite /TDM_slot in IH).
all: rewrite /TDM_counter in Hc'; move: Hc' => /eqP Hc'; rewrite Hc' in Hbug.
- all: rewrite addnS in Hlt; rewrite Hlt in Hbug.
- all: done.
+ all: rewrite addnS in Hlt; rewrite Hlt in Hbug; done.
Qed.
Lemma TDM_counter_same ta tb:
@@ -753,8 +736,7 @@ Section TDMPROOFS.
TDM_slot (Default_arbitrate (tb + d)).(Implementation_State) ==
TDM_slot (Default_arbitrate (ta + d)).(Implementation_State).
Proof.
- intros Hc Hs d; induction d.
- 1: by rewrite !addn0.
+ intros Hc Hs d; induction d; [ by rewrite !addn0 | ].
apply TDM_counter_same with (d := d) in Hc as Hc'.
rewrite !addnS; simpl; rewrite /Next_state.
destruct (Default_arbitrate (ta + d)).(Implementation_State) eqn:HSa,
@@ -777,14 +759,13 @@ Section TDMPROOFS.
Theorem Cmds_T_RTP_ok (t : nat) 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.
+ isCRD a -> isPRE b -> Same_Bank a b -> Before a b -> Apart_at_least a b T_RTP.
Proof.
- intros Ha_in Hb_in Htype sB aBb; rewrite /Apart_at_least.
- rewrite /CRD_to_PRE in Htype; move: Htype => /andP [iCa iPb].
+ intros Ha_in Hb_in iCa iPb sB aBb; rewrite /Apart_at_least.
apply CAS_modulo_date in Ha_in as Ha.
- 2: by unfold isCRD in iCa; unfold isCAS; rewrite iCa orTb. clear iCa.
+ 2: by unfold isCRD in iCa; unfold isCAS,isCRD,isCWR; rewrite iCa orTb; clear iCa.
apply PRE_modulo_date in Hb_in as Hb.
- 2: exact iPb. clear iPb.
+ 2: exact iPb; clear iPb.
rewrite !Time_counter_modulo in Hb,Ha.
apply TDM.Private_Mapping in sB.
@@ -854,15 +835,14 @@ Section TDMPROOFS.
Theorem Cmds_T_WTP_ok t a b:
a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CWR_to_PRE a b -> Same_Bank a b -> Before a b ->
+ isCWR a -> isPRE b -> Same_Bank a b -> Before a b ->
Apart_at_least a b (T_WR + T_WL + T_BURST).
Proof.
- intros Ha_in Hb_in Htype sB aBb; rewrite /Apart_at_least.
- rewrite /CRD_to_PRE in Htype; move: Htype => /andP [iCa iPb].
+ intros Ha_in Hb_in iCa iPb sB aBb; rewrite /Apart_at_least.
apply CAS_modulo_date in Ha_in as Ha.
- 2: by unfold isCWR in iCa; unfold isCAS; rewrite iCa orbT. clear iCa.
+ 2: by unfold isCWR in iCa; unfold isCAS,isCWR,isCRD; rewrite iCa orbT; clear iCa.
apply PRE_modulo_date in Hb_in as Hb.
- 2: exact iPb. clear iPb.
+ 2: exact iPb; clear iPb.
rewrite !Time_counter_modulo in Hb,Ha.
apply TDM.Private_Mapping in sB.
@@ -933,70 +913,75 @@ Section TDMPROOFS.
Theorem Cmds_T_RtoW_ok t a b:
a \in (Default_arbitrate t).(Arbiter_Commands) ->
b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CRD_to_CWR a b -> Before a b ->
+ isCRD a -> isCWR b -> Before a b ->
Apart_at_least a b T_RTW.
Proof.
- intros Ha Hb Htype aBb; unfold Apart_at_least.
- rewrite /CWR_to_PRE in Htype; move: Htype => /andP [iCRa iCWb].
+ intros Ha Hb iCRa iCWb aBb; unfold Apart_at_least.
apply CAS_modulo_date in Ha.
- 2: by unfold isCRD in iCRa; unfold isCAS; rewrite iCRa orTb. clear iCRa.
+ 2: by unfold isCRD in iCRa; unfold isCAS, isCRD, isCWR; rewrite iCRa orTb. clear iCRa.
apply CAS_modulo_date in Hb.
- 2: by unfold isCWR in iCWb; unfold isCAS; rewrite iCWb orbT. clear iCWb.
+ 2: by unfold isCWR in iCWb; unfold isCAS, isCRD, isCWR; rewrite iCWb orbT. clear iCWb.
rewrite !Time_counter_modulo in Hb,Ha.
move: Hb => /eqP Hb; rewrite -Hb in Ha; move: Ha => /eqP Ha; apply Logic.eq_sym in Ha; move: Ha => /eqP Ha.
apply Modulo_time_distance in Ha.
2: by unfold Before in aBb.
- apply leq_trans with (n := a.(CDate) + SL).
- 2: exact Ha.
+ apply leq_trans with (n := a.(CDate) + SL); [ | assumption ].
by rewrite leq_add2l leq_eqVlt T_RTW_SL orbT.
Qed.
Theorem Cmds_T_WtoR_SBG_ok t a b:
a \in (Default_arbitrate t).(Arbiter_Commands) ->
b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CWR_to_CRD a b -> Before a b -> Same_Bankgroup a b ->
+ isCWR a -> isCRD b -> Before a b -> Same_Bankgroup a b ->
Apart_at_least a b (T_WTR_l + T_WL + T_BURST).
Proof.
- intros Ha Hb Htype aBb sBG; unfold Apart_at_least.
- rewrite /CWR_to_PRE in Htype; move: Htype => /andP [iA iB].
+ intros Ha Hb iA iB aBb sBG; unfold Apart_at_least.
apply CAS_modulo_date in Ha.
- 2: by unfold isCWR in iA; unfold isCAS; rewrite iA orbT. clear iA.
+ 2: by unfold isCWR in iA; unfold isCAS,isCRD,isCWR; rewrite iA orbT; clear iA.
apply CAS_modulo_date in Hb.
- 2: by unfold isCRD in iB; unfold isCAS; rewrite iB orTb. clear iB.
+ 2: by unfold isCRD in iB; unfold isCAS,isCRD,isCWR; rewrite iB orTb; clear iB.
rewrite !Time_counter_modulo in Hb,Ha.
move: Hb => /eqP Hb; rewrite -Hb in Ha; move: Ha => /eqP Ha; apply Logic.eq_sym in Ha; move: Ha => /eqP Ha.
apply Modulo_time_distance in Ha.
2: by unfold Before in aBb.
- apply leq_trans with (n := a.(CDate) + SL).
- 2: exact Ha.
+ apply leq_trans with (n := a.(CDate) + SL); [ | assumption ].
by rewrite leq_add2l leq_eqVlt WTR_SL orbT.
Qed.
- Theorem Cmds_T_WtoR_DBG_ok t:
- BANKGROUPS > 1 -> forall (a b : Command_t),
+ Theorem Cmds_T_WtoR_DBG_ok t a b:
a \in (Default_arbitrate t).(Arbiter_Commands) ->
b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CWR_to_CRD a b -> Before a b -> ~~ Same_Bankgroup a b ->
+ isCWR a -> isCRD b -> Before a b -> ~~ Same_Bankgroup a b ->
Apart_at_least a b (T_WTR_s + T_WL + T_BURST).
Proof.
- intros H. specialize TDM.DDR3 as Hbug. by rewrite Hbug in H.
- Qed.
+ intros Ha Hb iA iB aBb sBG; unfold Apart_at_least.
+ apply CAS_modulo_date in Ha.
+ 2: by unfold isCWR in iA; unfold isCAS,isCRD,isCWR; rewrite iA orbT; clear iA.
+ apply CAS_modulo_date in Hb.
+ 2: by unfold isCRD in iB; unfold isCAS,isCRD,isCWR; rewrite iB orTb; clear iB.
+ rewrite !Time_counter_modulo in Hb,Ha.
+ move: Hb => /eqP Hb; rewrite -Hb in Ha; move: Ha => /eqP Ha; apply Logic.eq_sym in Ha; move: Ha => /eqP Ha.
+ apply Modulo_time_distance in Ha.
+ 2: by unfold Before in aBb.
+ apply leq_trans with (n := a.(CDate) + SL); [ | assumption ].
+ specialize T_WTR_bgs; specialize WTR_SL; lia.
+ Qed.
Theorem Cmds_T_CCD_SBG_ok t a b:
a \in (Default_arbitrate t).(Arbiter_Commands) ->
b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CRD_to_CRD a b \/ CWR_to_CWR a b -> Before a b -> Same_Bankgroup a b ->
+ (isCRD a /\ isCRD b) \/ (isCWR a /\ isCWR b) -> Before a b -> Same_Bankgroup a b ->
Apart_at_least a b T_CCD_l.
Proof.
intros Ha Hb Htype aBb sBG; unfold Apart_at_least.
destruct Htype as [Htype | Htype].
- 2: unfold CWR_to_CWR in Htype; move: Htype => /andP [iWa iWb].
- 1: unfold CRD_to_CRD in Htype; move: Htype => /andP [iRa iRb].
+ 2: destruct Htype as [iWa iWb].
+ 1: destruct Htype as [iRa iRb].
all: apply CAS_modulo_date in Ha,Hb.
- 2: by unfold isCAS; unfold isCRD in iRb; rewrite iRb orTb.
- 2: by unfold isCAS; unfold isCRD in iRa; rewrite iRa orTb.
- 3: by unfold isCAS; unfold isCWR in iWb; rewrite iWb orbT.
- 3: by unfold isCAS; unfold isCWR in iWa; rewrite iWa orbT.
+ 2: by unfold isCAS,isCWR,isCRD; unfold isCRD in iRb; rewrite iRb orTb.
+ 2: by unfold isCAS,isCWR,isCRD; unfold isCRD in iRa; rewrite iRa orTb.
+ 3: by unfold isCAS,isCWR,isCRD; unfold isCWR in iWb; rewrite iWb orbT.
+ 3: by unfold isCAS,isCWR,isCRD; unfold isCWR in iWa; rewrite iWa orbT.
all: rewrite !Time_counter_modulo in Hb,Ha.
all: move: Hb => /eqP Hb; rewrite -Hb in Ha; move: Ha => /eqP Ha; apply Logic.eq_sym in Ha; move: Ha => /eqP Ha.
all: apply Modulo_time_distance in Ha.
@@ -1006,15 +991,29 @@ Section TDMPROOFS.
all: by rewrite leq_add2l leq_eqVlt T_CCD_SL orbT.
Qed.
- Theorem Cmds_T_CCD_DBG_ok t:
- BANKGROUPS > 1 -> forall a b,
+ Theorem Cmds_T_CCD_DBG_ok t a b :
a \in (Default_arbitrate t).(Arbiter_Commands) ->
b \in (Default_arbitrate t).(Arbiter_Commands) ->
- CRD_to_CRD a b \/ CWR_to_CWR a b -> Before a b -> ~~ Same_Bankgroup a b ->
+ (isCRD a /\ isCRD b) \/ (isCWR a /\ isCWR b) -> Before a b -> ~~ Same_Bankgroup a b ->
Apart_at_least a b T_CCD_s.
Proof.
- intros H. specialize TDM.DDR3 as Hbug. by rewrite Hbug in H.
- Qed.
+ intros Ha Hb Htype aBb sBG; unfold Apart_at_least.
+ destruct Htype as [Htype | Htype].
+ 2: destruct Htype as [iWa iWb].
+ 1: destruct Htype as [iRa iRb].
+ all: apply CAS_modulo_date in Ha,Hb.
+ 2: by unfold isCAS,isCWR,isCRD; unfold isCRD in iRb; rewrite iRb orTb.
+ 2: by unfold isCAS,isCWR,isCRD; unfold isCRD in iRa; rewrite iRa orTb.
+ 3: by unfold isCAS,isCWR,isCRD; unfold isCWR in iWb; rewrite iWb orbT.
+ 3: by unfold isCAS,isCWR,isCRD; unfold isCWR in iWa; rewrite iWa orbT.
+ all: rewrite !Time_counter_modulo in Hb,Ha.
+ all: move: Hb => /eqP Hb; rewrite -Hb in Ha; move: Ha => /eqP Ha; apply Logic.eq_sym in Ha; move: Ha => /eqP Ha.
+ all: apply Modulo_time_distance in Ha.
+ all: try done.
+ all: apply leq_trans with (n := a.(CDate) + SL).
+ all: try exact Ha.
+ all: specialize T_CCD_bgs; specialize T_CCD_SL; lia.
+ 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) ->
@@ -1065,11 +1064,10 @@ Section TDMPROOFS.
Theorem Cmds_T_RRD_SBG_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 -> Same_Bankgroup a b ->
+ isACT a -> isACT b -> ~~ Same_Bank a b -> Before a b -> Same_Bankgroup a b ->
Apart_at_least a b T_RRD_l.
Proof.
- intros Ha Hb AtA _ aBb sBG.
- move : AtA => /andP [Aa Ab].
+ intros Ha Hb Aa Ab _ aBb sBG.
apply ACT_modulo_date in Ha.
2: exact Aa. clear Aa.
apply ACT_modulo_date in Hb.
@@ -1085,19 +1083,31 @@ Section TDMPROOFS.
by rewrite leq_eqVlt T_RRD_SL orbT.
Qed.
- Theorem Cmds_T_RRD_DBG_ok t: BANKGROUPS > 1 -> forall a b,
+ Theorem Cmds_T_RRD_DBG_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 -> ~~ Same_Bankgroup a b ->
+ isACT a -> isACT b -> ~~ Same_Bank a b -> Before a b -> ~~ Same_Bankgroup a b ->
Apart_at_least a b T_RRD_s.
Proof.
- intros H. specialize TDM.DDR3 as Hbug. by rewrite Hbug in H.
- Qed.
+ intros Ha Hb Aa Ab _ aBb sBG.
+ 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.
+ specialize T_RRD_SL; specialize T_RRD_bgs; lia.
+ 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).
@@ -1111,8 +1121,7 @@ Section TDMPROOFS.
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.
+ 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).
@@ -1150,19 +1159,19 @@ Section TDMPROOFS.
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.
+ 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 *;
+ by rewrite /Enqueue mem_cat HA orbT.
+ Qed.
Definition Requestor_slot_start ta (s : Slot_t) :=
let aligned_ta := Closest_slot_start ta in
@@ -1173,9 +1182,8 @@ Section TDMPROOFS.
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.
+ rewrite -nat_of_counter_eq -Time_counter_modulo -(modn_small (m := OZCycle) (d := SL)); [ | done ].
+ 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).
@@ -1696,7 +1704,7 @@ Section TDMPROOFS.
all: try by rewrite HC' HR andbT.
all: move : Hl => /eqP Hl; subst.
- all: contradict Hd; by rewrite /OLastCycle //= ltnn.
+ all: contradict Hd; by rewrite /OLastCycle //= ltnn.Request_slot_start_aligned
Qed.
Lemma Request_processing_starts ta ra:
@@ -1863,6 +1871,8 @@ Section TDMPROOFS.
exact H.
Qed.
+ (* ------------------------------------------------------------------------------------------ *)
+
Lemma TDM_inc_counter t:
TDM_counter (Default_arbitrate t).(Implementation_State) < SL.-1 ->
nat_of_ord (TDM_counter (Default_arbitrate t.+1).(Implementation_State)) =
@@ -2024,43 +2034,45 @@ Section TDMPROOFS.
Lemma TDM_ACT_date cmd t:
cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isACT cmd ->
TDM_counter (Default_arbitrate cmd.(CDate)).(Implementation_State) == Next_cycle OACT_date /\
- TDM_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 (c == OZCycle) eqn:Hz; try destruct (Pending_of _ _) eqn:HP; simpl in *.
- all: rewrite in_cons in Hi; move: Hi => /orP [/eqP H | H]; try by rewrite H in Hp.
- all: apply IHt in H; try (exact Hp || exact H). }
- { destruct (c == OACT_date) eqn:Hact, (c == OCAS_date) eqn:Hcas, (c == OLastCycle) eqn:Hend; simpl in *.
- all: rewrite in_cons in Hi; move: Hi => /orP [/eqP H | H]; try by rewrite H in Hp.
- all: try (rewrite H //= /TDM_counter !Hs //= Hact //=; move: Hact => /eqP Hact; by rewrite Hact).
- all: try apply IHt in H; try exact Hp; try exact H.
- all: rewrite H /isACT /Kind_of_req //= in Hp; contradict Hp; by case r0.(Kind). }
+ TDM_request (Default_arbitrate cmd.(CDate)).(Implementation_State) == get_req cmd.
+ 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 (c == OZCycle) eqn:Hz; try destruct (Pending_of _ _) eqn:HP; simpl in *.
+ all: rewrite in_cons in Hi; move: Hi => /orP [/eqP H | H]; try by rewrite H in Hp.
+ all: apply IHt in H; try (exact Hp || exact H). }
+ { destruct (c == OACT_date) eqn:Hact, (c == OCAS_date) eqn:Hcas, (c == OLastCycle) eqn:Hend; simpl in *.
+ all: rewrite in_cons in Hi; move: Hi => /orP [/eqP H | H]; try by rewrite H in Hp.
+ all: try (rewrite H //= /TDM_counter !Hs //= Hact //=; move: Hact => /eqP Hact; by rewrite Hact).
+ all: try apply IHt in H; try exact Hp; try exact H.
+ all: rewrite H /isACT /Kind_of_req //= in Hp; contradict Hp; by case r0.(Kind). }
Qed.
Lemma TDM_CAS_date cmd t:
cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isCAS cmd ->
TDM_counter (Default_arbitrate cmd.(CDate)).(Implementation_State) == Next_cycle OCAS_date /\
- TDM_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 (c == OZCycle) eqn:Hz; try destruct (Pending_of _ _) eqn:HP; simpl in *.
- all: rewrite in_cons in Hi; move: Hi => /orP [/eqP H | H]; try by rewrite H in Hp.
- all: apply IHt in H; try (exact Hp || exact H). }
- { destruct (c == OACT_date) eqn:Hact, (c == OCAS_date) eqn:Hcas, (c == OLastCycle) eqn:Hend; simpl in *.
- all: rewrite in_cons in Hi; move: Hi => /orP [/eqP H | H]; try by rewrite H in Hp.
- (* all: try (rewrite H //= /TDM_counter !Hs //= Hact //=; move: Hact => /eqP Hact; by rewrite Hact). *)
- all: try apply IHt in H; try exact Hp; try exact H.
- all: rewrite H //= Hs //= Hact Hcas //=.
- all: move: Hcas => /eqP Hcas; by rewrite Hcas !eq_refl. }
- Qed.
+ (isRUNNING (Default_arbitrate cmd.(CDate)).(Implementation_State)) /\
+ TDM_request (Default_arbitrate cmd.(CDate)).(Implementation_State) == get_req cmd.
+ 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 (c == OZCycle) eqn:Hz; try destruct (Pending_of _ _) eqn:HP; simpl in *.
+ all: rewrite in_cons in Hi; move: Hi => /orP [/eqP H | H]; try by rewrite H in Hp.
+ all: apply IHt in H; try (exact Hp || exact H). }
+ { destruct (c == OACT_date) eqn:Hact, (c == OCAS_date) eqn:Hcas, (c == OLastCycle) eqn:Hend; simpl in *.
+ all: rewrite in_cons in Hi; move: Hi => /orP [/eqP H | H]; try by rewrite H in Hp.
+ (* all: try (rewrite H //= /TDM_counter !Hs //= Hact //=; move: Hact => /eqP Hact; by rewrite Hact). *)
+ all: try apply IHt in H; try exact Hp; try exact H.
+ all:
+ rewrite H //= Hs //= Hact Hcas //=;
+ move: Hcas => /eqP Hcas; rewrite Hcas !eq_refl /get_req /Kind_of_req //=; split; [trivial | ];
+ destruct r0.(Kind); by rewrite eq_refl.
+ }
+ Qed.
Lemma TDM_SL_gt_nc_act_p1 :
Next_cycle OACT_date +1 < SL.
@@ -2079,24 +2091,25 @@ Section TDMPROOFS.
Proof.
intros Ha Hb iA iAb SB aBb.
(* info about b's counter *)
- apply ACT_modulo_date in Hb as Hb'. rewrite Time_counter_modulo in Hb'.
- 2: done.
+ apply ACT_modulo_date in Hb as Hb'; [ | done].
+ rewrite Time_counter_modulo in Hb'.
(* other info *)
- apply TDM_ACT_date in Hb as H. destruct H as [Hc_b Hreq_b].
- 2: exact iAb.
+ apply TDM_ACT_date in Hb as H; [ | assumption ]. destruct H as [Hc_b Hreq_b].
apply TDM_add_counter with (d := 1) in Hc_b as Hc_b'.
2: exact TDM_SL_gt_nc_act_p1.
rewrite !addn1 in Hc_b'; move: Hc_b' => /eqP Hc_b'.
+ unfold get_req in Hreq_b; destruct b.(CKind) eqn:H_kind;
+ try (by unfold isACT in iAb; rewrite H_kind in iAb).
+
(* get the PRE *)
apply Request_PRE_bounded in Hreq_b.
move: Hc_b => /eqP Hc_b. rewrite /Last_slot_start Hc_b in Hreq_b.
- exists (PRE_of_req b.(Request) (b.(CDate) - Next_cycle OACT_date).+1).
- rewrite /Same_Bank in SB; move: SB => /eqP SB.
- rewrite /isPRE /Same_Bank //= eq_refl andbT SB eq_refl andbT andbT /Before /After //=.
- clear SB.
-
+ exists (PRE_of_req r (b.(CDate) - Next_cycle OACT_date).+1).
+ rewrite /Same_Bank in SB; move: SB => /eqP SB; rewrite /Same_Bank SB.
+ rewrite /isPRE /PRE_of_req //= andbT /get_bank H_kind //= eq_refl !andbT /Before /After.
+
(* solve Before c b*)
apply /andP; split.
2: {
@@ -2104,9 +2117,9 @@ Section TDMPROOFS.
2: specialize Date_gt_counter with (t := b.(CDate)) as HH; rewrite Hc_b in HH; exact HH.
rewrite ltn_subLR.
2: specialize Date_gt_counter with (t := b.(CDate).+1) as HH; rewrite Hc_b' in HH; by rewrite leq_eqVlt HH orbT.
- rewrite -ltn_predRL addnC nat_add_pred; apply nat_ltn_add.
- by rewrite TDM_nextcycle_act_eq_actS -pred_Sn /ACT_date.
- }
+ assert (Next_cycle OACT_date > 1); [ | lia ].
+ rewrite TDM_nextcycle_act_eq_actS /ACT_date; lia.
+ }
(* solve ~~ Before_at a c, i.e., After c a *)
apply /andP; split; clear Hb'.
@@ -2220,6 +2233,19 @@ Section TDMPROOFS.
exact Hreq_b.
Qed.
+ Lemma Request_exists b c0 r r0 s0 :
+ isCAS b ->
+ (Default_arbitrate b.(CDate)).(Implementation_State) = RUNNING s0 c0 r r0 ->
+ TDM_request (Default_arbitrate b.(CDate)).(Implementation_State) == get_req b ->
+ TDM_request (Default_arbitrate b.(CDate)).(Implementation_State) == Some r0.
+ Proof.
+ intros iCb H Hreq_b.
+ unfold get_req, TDM_request in *; rewrite H in Hreq_b.
+ destruct b.(CKind) eqn:Hkind;
+ try (by unfold isCAS,isCRD,isCWR in iCb; rewrite Hkind in iCb);
+ by rewrite H eq_refl.
+ Qed.
+
Theorem Cmds_row_ok t b c:
b \in (Default_arbitrate t).(Arbiter_Commands) -> c \in (Default_arbitrate t).(Arbiter_Commands) ->
isCAS b -> isPRE c -> Same_Bank b c -> Before c b ->
@@ -2228,24 +2254,42 @@ Section TDMPROOFS.
Proof.
intros Hb Hc iCb iPc SB cBb.
- apply TDM_CAS_date in Hb as H. destruct H as [Hc_b Hreq_b].
- 2: exact iCb.
+ apply TDM_CAS_date in Hb as H; [ | assumption].
+ destruct H as [Hc_b [Hrun_b Hreq_b]].
- apply Request_ACT_bounded in Hreq_b.
- move: Hc_b => /eqP Hc_b; rewrite /Last_slot_start Hc_b in Hreq_b.
+ destruct (Default_arbitrate b.(CDate)).(Implementation_State) eqn:Hsb; [ done | ].
- rewrite TDM_nextcycle_cas_eq_casS subnSK in Hreq_b.
- 2: specialize Date_gt_counter with (t := b.(CDate)) as HH; by rewrite Hc_b TDM_nextcycle_cas_eq_casS in HH.
+ apply Request_exists in Hsb as H; try assumption; [ | by rewrite <- Hsb in Hreq_b].
+
+ apply Request_ACT_bounded in H.
+ rewrite /TDM_counter in Hc_b; move: Hc_b => /eqP Hc_b; cbv zeta in H.
+ rewrite /Last_slot_start Hsb /TDM_counter Hc_b in H.
- exists (ACT_of_req b.(Request) (b.(CDate) - CAS_date + ACT_date)).
- rewrite /Same_Bank in SB; move: SB => /eqP SB.
- rewrite /isACT //= eq_refl andbT /Before /After //= /Same_Row eq_refl //= andbT.
+ rewrite TDM_nextcycle_cas_eq_casS subnSK in H.
+ 2:
+ specialize Date_gt_counter with (t := b.(CDate)) as HH;
+ by rewrite Hsb /TDM_counter Hc_b TDM_nextcycle_cas_eq_casS in HH.
- apply /andP; split.
- 2: {
+ exists (ACT_of_req r0 (b.(CDate) - CAS_date + ACT_date)).
+
+ rewrite /Same_Bank in SB; move: SB => /eqP SB;
+ rewrite /isACT //= andbT /Before /After //= /Same_Row /get_row //=.
+
+ apply /andP; split; [ apply /andP; split; [ apply /andP; split | ] | ].
+
+ 2: {
+ unfold TDM_request, get_req in *.
+ destruct b.(CKind) eqn:Hkind;
+ try (by unfold isCAS,isCRD,isCWR in iCb; rewrite Hkind in iCb);
+ rewrite inj_eq in Hreq_b; try rewrite inj_eq; try (exact ssrfun.Some_inj);
+ move: Hreq_b => /eqP Hreq_b; subst r0; by rewrite eq_refl.
+ }
+
+ 3: {
rewrite -subnA.
- 3: {
- specialize Date_gt_counter with (t := b.(CDate)) as H.
+ 3: { clear H.
+ specialize Date_gt_counter with (t := b.(CDate)) as H.
+ rewrite Hsb //= in H.
rewrite Hc_b TDM_nextcycle_cas_eq_casS in H.
by rewrite leq_eqVlt H orbT. }
2: by rewrite /CAS_date leq_addr.
@@ -2254,7 +2298,6 @@ Section TDMPROOFS.
by apply nat_ltn_add.
}
- apply /andP; split.
2: {
apply PRE_modulo_date in Hc as Hc_c. rewrite Time_counter_modulo in Hc_c.
2: exact iPc.
@@ -2265,6 +2308,10 @@ Section TDMPROOFS.
move: Hc_b => /eqP Hc_b; rewrite -nat_of_counter_eq TDM_nextcycle_cas_eq_casS in Hc_b.
move: Hc_b => /eqP Hc_b; rewrite -Hc_b in Hc_c'.
move: Hc_c' => /eqP Hc_c'; apply Logic.eq_sym in Hc_c'; move: Hc_c' => /eqP Hc_c'.
+
+ assert (H0: TDM_counter (Default_arbitrate b.(CDate)).(Implementation_State) = c0);
+ [ rewrite Hsb //= | rewrite <- H0 in Hc_c' ].
+
apply Modulo_time_distance_or in Hc_c'; destruct Hc_c' as [Hc_c' | [Hc_c' | Hc_c']].
3: {
rewrite Hc_c' -subnA.
@@ -2290,7 +2337,11 @@ Section TDMPROOFS.
apply nat_ltn_add.
by rewrite addn_gt0 SL_pos orTb. }
{ rewrite -subnA.
- 3: by specialize Date_gt_counter with (t := b.(CDate)) as H; rewrite Hc_b in H; rewrite leq_eqVlt H orbT.
+ 3: {
+ clear H; specialize Date_gt_counter with (t := b.(CDate)) as H.
+ rewrite Hsb //= in H.
+ by rewrite Hc_b in H; rewrite leq_eqVlt H orbT.
+ }
2: by rewrite /CAS_date leq_addr.
rewrite ltn_subRL addnC.
apply ltn_trans with (m := c.(CDate) + (CAS_date - ACT_date)) in Hc_c'.
@@ -2308,12 +2359,14 @@ Section TDMPROOFS.
{ rewrite -subnA.
3: {
move: Hc_b => /eqP Hc_b; rewrite -nat_of_counter_eq TDM_nextcycle_cas_eq_casS in Hc_b; move: Hc_b => /eqP Hc_b.
- by specialize Date_gt_counter with (t := b.(CDate)) as H; rewrite Hc_b in H; rewrite leq_eqVlt H orbT.
+ clear H; specialize Date_gt_counter with (t := b.(CDate)) as H;
+ rewrite Hsb //= in H;
+ rewrite Hc_b in H; by rewrite leq_eqVlt H orbT.
}
2: by rewrite /CAS_date leq_addr.
by rewrite leq_subr.
}
- exact Hreq_b.
+ exact H.
Qed.
Lemma Default_arbitrate_notin_cmd t (c : Command_t):
@@ -2329,22 +2382,14 @@ Section TDMPROOFS.
Lemma Default_arbitrate_cmds_uniq t:
uniq ((Default_arbitrate t).(Arbiter_Commands)).
Proof.
- induction t; simpl.
- { done. }
+ induction t; simpl; [ done | ].
rewrite /Next_state //=.
- destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (c == OZCycle), (c == OACT_date),
- (c == OCAS_date), (c == OLastCycle); try destruct (Pending_of _ _); simpl.
- all: rewrite IHt andbT.
- all: assert (t < t.+1) as H0; try trivial.
- all: try (specialize Default_arbitrate_notin_cmd with (c := mkCmd t.+1 NOP nullreq) (t := t) as H; simpl in H;
- apply H in H0; by rewrite H0).
- all: try (specialize Default_arbitrate_notin_cmd with (c := mkCmd t.+1 PRE r0) (t := t) as H; simpl in H;
- apply H in H0; by rewrite H0).
- all: try (specialize Default_arbitrate_notin_cmd with (c := mkCmd t.+1 ACT r0) (t := t) as H; simpl in H;
- apply H in H0; by rewrite H0).
- all: try (specialize Default_arbitrate_notin_cmd with (c := mkCmd t.+1 (Kind_of_req r0) r0) (t := t) as H; simpl in H;
- apply H in H0; by rewrite H0).
- Qed.
+ destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (c == OZCycle), (c == OACT_date),
+ (c == OCAS_date), (c == OLastCycle); try destruct (Pending_of _ _); simpl;
+ rewrite IHt andbT;
+ assert (t < t.+1) as H0; try trivial;
+ apply Default_arbitrate_notin_cmd; simpl; lia.
+ Qed.
Lemma Default_arbitrate_cmds_date t cmd:
cmd \in (Default_arbitrate t).(Arbiter_Commands) ->
@@ -2371,12 +2416,18 @@ Section TDMPROOFS.
(Cmds_T_WtoR_DBG_ok t)
(Cmds_T_CCD_SBG_ok t)
(Cmds_T_CCD_DBG_ok t)
+ _ (* REF *)
+ _ (* REF *)
(Cmds_T_FAW_ok t)
(Cmds_T_RRD_SBG_ok t)
(Cmds_T_RRD_DBG_ok t)
(Cmds_ACT_ok t)
- (Cmds_row_ok t).
+ (Cmds_row_ok t)
+ _ (* Initial *)
+ _ (* REF *).
+ Admit Obligations.
Global Instance TDM_arbiter : Arbiter_t :=
mkArbiter AF TDM_arbitrate Requests_handled Default_arbitrate_time_match.
-End TDMPROOFS.
+
+End TDMPROOFS.
diff --git a/framework/DRAM/Implementations/TS/DynTDM/TDMds.v b/framework/DRAM/Implementations/old_imps/DynTDM/TDMds.v
similarity index 100%
rename from framework/DRAM/Implementations/TS/DynTDM/TDMds.v
rename to framework/DRAM/Implementations/old_imps/DynTDM/TDMds.v
diff --git a/framework/DRAM/Implementations/TS/DynTDM/TDMes.v b/framework/DRAM/Implementations/old_imps/DynTDM/TDMes.v
similarity index 100%
rename from framework/DRAM/Implementations/TS/DynTDM/TDMes.v
rename to framework/DRAM/Implementations/old_imps/DynTDM/TDMes.v
diff --git a/framework/DRAM/Implementations/TS/DynTDM/TDMesREF.v b/framework/DRAM/Implementations/old_imps/DynTDM/TDMesREF.v
similarity index 100%
rename from framework/DRAM/Implementations/TS/DynTDM/TDMesREF.v
rename to framework/DRAM/Implementations/old_imps/DynTDM/TDMesREF.v
diff --git a/framework/DRAM/Implementations/TS/DynTDM/TDMesREFpg.v b/framework/DRAM/Implementations/old_imps/DynTDM/TDMesREFpg.v
similarity index 100%
rename from framework/DRAM/Implementations/TS/DynTDM/TDMesREFpg.v
rename to framework/DRAM/Implementations/old_imps/DynTDM/TDMesREFpg.v
diff --git a/framework/DRAM/Implementations/TS/FIFOImp2/FIFOImp2.v b/framework/DRAM/Implementations/old_imps/FIFOImp2/FIFOImp2.v
similarity index 100%
rename from framework/DRAM/Implementations/TS/FIFOImp2/FIFOImp2.v
rename to framework/DRAM/Implementations/old_imps/FIFOImp2/FIFOImp2.v
diff --git a/framework/DRAM/Implementations/TS/FIFOImp2/FIFOImp2Properties.v b/framework/DRAM/Implementations/old_imps/FIFOImp2/FIFOImp2Properties.v
similarity index 100%
rename from framework/DRAM/Implementations/TS/FIFOImp2/FIFOImp2Properties.v
rename to framework/DRAM/Implementations/old_imps/FIFOImp2/FIFOImp2Properties.v
diff --git a/framework/DRAM/Implementations/TS/FIFOImp2/FIFOImp2Test.v b/framework/DRAM/Implementations/old_imps/FIFOImp2/FIFOImp2Test.v
similarity index 100%
rename from framework/DRAM/Implementations/TS/FIFOImp2/FIFOImp2Test.v
rename to framework/DRAM/Implementations/old_imps/FIFOImp2/FIFOImp2Test.v
diff --git a/framework/DRAM/Implementations/old_imps/TDMREF/TDMREF.v b/framework/DRAM/Implementations/old_imps/TDMREF/TDMREF.v
new file mode 100644
index 0000000000000000000000000000000000000000..fe6858da531c35a01601d215ce7eee723e72d5eb
--- /dev/null
+++ b/framework/DRAM/Implementations/old_imps/TDMREF/TDMREF.v
@@ -0,0 +1,353 @@
+Set Warnings "-notation-overridden,-parsing".
+Set Printing Projections.
+From DRAM Require Export ImplementationInterface.
+From mathcomp Require Export fintype div ssrZ zify.
+From Coq Require Import Program.
+
+Section TDMREF.
+
+ Context {SYS_CFG : System_configuration}.
+
+ (* Implementing everything with just one counter *)
+ (* Definition REF_cycle := T_REFI. *)
+ Definition REF_start_date := T_REFI.
+ Definition PREA_date := T_REFI - T_RP.
+
+ Definition REF_date := T_RP.
+ Definition PRE_date := REF_date + T_RFC.
+ Definition ACT_date := PRE_date + T_RP.
+ Definition CAS_date := ACT_date + T_RCD.
+
+ (* Definition ENDREF_date := REF_date + T_RFC. *)
+
+ (* Need an axiom saying that:
+ T_RP + T_RFC > T_RTP
+ T_RP + T_RFC > T_WL + T_BURST + T_WR
+ Then, in this case, I won't need an hypothesis of disjoint banks *)
+
+ Class TDMREF_configuration :=
+ {
+ SN : nat;
+ SN_one : 1 < SN;
+
+ SL : nat;
+ SL_pos : 0 < SL;
+
+ (* There has to be enough time to complete a full PRE - ACT - CAS sequence, plus one extra
+ IDLE cycle *)
+ SL_CASS : CAS_date.+1 < SL;
+
+ (* SL has to be large enough to acomodate bus changing directions *)
+ SL_BUS_RD_TO_WR : T_RTW < SL;
+ SL_BUS_WR_TO_RD : T_WTR_l + T_WL + T_BURST < SL;
+
+ (* Other axioms about SL *)
+ T_RTP_SN_SL : T_RTP < SN * SL - CAS_date;
+ T_WTP_SN_SL : (T_WR + T_WL + T_BURST) < SN * SL - CAS_date;
+
+ T_RAS_SL : T_RP.+1 + T_RAS < SL;
+ T_RC_SL : T_RC < SL;
+ T_RRD_SL : T_RRD_l < SL;
+ T_CCD_SL : T_CCD_l < SL;
+ T_FAW_3SL : T_FAW < SL + SL + SL;
+
+ (* Axiom A1: SL needs to be a divider of T_REFI *)
+ SL_REF_aligned : T_REFI %% SL == 0;
+
+ (* No need for disjoint banks if this is satisfied -- initial REF delay is big enough
+ to acomodate the write recovery time. This should always be the case, since T_RFC is big enough *)
+ SL_REF_cycle : (T_RP + T_RFC).+1 > (T_WL + T_BURST + T_WR);
+ }.
+
+ Context {TDMREF_CFG : TDMREF_configuration}.
+
+ (* -------------------- Additional Lemmas about SN ------------------------ *)
+ Lemma SN_pos : SN > 0.
+ specialize SN_one; lia.
+ Qed.
+
+ (* --------------------- Additional Lemmas about PREA_date ---------------- *)
+ (* Lemma PREA_date_GT_REF_date : REF_date < PREA_date.
+ specialize PREA_date_GT_ENDREF_date; unfold ENDREF_date; lia.
+ Qed. *)
+
+ Lemma REF_start_date_pos : 0 < REF_start_date.
+ unfold REF_start_date; specialize T_REFI_GT_T_RP; lia.
+ Qed.
+
+ (* ---------------------- Additional Lemmas about SL ---------------------- *)
+ Lemma SL_PRE : PRE_date < SL.
+ specialize SL_CASS; unfold PRE_date, CAS_date, ACT_date, PRE_date, REF_date; lia.
+ Qed.
+
+ Lemma SL_REF : REF_date < SL.
+ unfold REF_date; specialize T_RAS_SL; lia.
+ Qed.
+
+ Lemma SL_ACT : ACT_date < SL.
+ specialize SL_CASS; unfold CAS_date, ACT_date; lia.
+ Qed.
+
+ Lemma Last_cycle: SL.-1 < SL.
+ rewrite ltn_predL; apply SL_pos.
+ Qed.
+
+ Lemma SL_CAS: CAS_date < SL.
+ specialize SL_CASS as H; lia.
+ Qed.
+
+ Lemma SL_one: 1 < SL.
+ specialize SL_CASS; lia.
+ Qed.
+
+ Lemma SL_ACTS: ACT_date.+1 < SL.
+ specialize SL_CASS; unfold CAS_date, ACT_date; lia.
+ Qed.
+
+ (* ------------------------ Additional Lemmas about ACT_date & CAS_date ---- *)
+ Lemma ACT_pos: 0 < ACT_date.
+ unfold ACT_date; specialize T_RP_pos; lia.
+ Qed.
+
+ Lemma CAS_pos: 0 < CAS_date.
+ unfold CAS_date; specialize T_RCD_pos; lia.
+ Qed.
+
+ (* ------------------------ Controller implementation ---------------------- *)
+
+ (* Normal counter *)
+ Definition Counter_t := ordinal SL.
+ Definition OZCycle := Ordinal SL_pos.
+ Definition OREF_date := Ordinal SL_REF.
+ Definition OPRE_date := Ordinal SL_PRE.
+ Definition OACT_date := Ordinal SL_ACT.
+ Definition OCAS_date := Ordinal SL_CAS.
+ Definition OLastCycle := Ordinal Last_cycle.
+
+ 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.
+
+ (* Slot counter *)
+ Definition Slot_t := ordinal_eqType SN.
+ Definition OZSlot := Ordinal SN_pos.
+
+ 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.
+
+ (* Refresh counter *)
+ Definition Counter_ref_t := ordinal REF_start_date.
+
+ Lemma REF_start_date_GT_PREA_date : PREA_date < REF_start_date.
+ unfold PREA_date, REF_start_date; specialize T_RP_pos; specialize T_REFI_pos; lia.
+ Qed.
+
+ Definition OPREA_date := Ordinal REF_start_date_GT_PREA_date.
+ Definition OCycle0REF := Ordinal T_REFI_pos.
+
+ Definition Next_cycle_ref (c : Counter_ref_t) : Counter_ref_t :=
+ let nextcref := c.+1 < REF_start_date in
+ (if nextcref as X return (nextcref = X -> Counter_ref_t) then
+ (fun (P : nextcref = true) => Ordinal (P : nextcref))
+ else (fun _ => OCycle0REF)) Logic.eq_refl.
+
+ Instance REQUESTOR_CFG : Requestor_configuration :=
+ {
+ Requestor_t := Slot_t
+ }.
+
+ Context {AF : Arrival_function_t}.
+
+ Inductive TDM_state_t :=
+ | IDLE : Slot_t -> Counter_t -> Counter_ref_t -> Requests_t -> TDM_state_t
+ | RUNNING : Slot_t -> Counter_t -> Counter_ref_t -> Requests_t -> Request_t -> TDM_state_t
+ | REFRESH : Slot_t -> Counter_t -> Counter_ref_t -> Requests_t -> Request_t -> TDM_state_t.
+
+ Global Instance ARBITER_CFG : Arbiter_configuration :=
+ {
+ State_t := TDM_state_t;
+ }.
+
+ Definition Enqueue (R P : Requests_t) := P ++ R.
+
+ Definition Dequeue r (P : Requests_t) := rem r P.
+
+ (* The set of pending requests of a slot *)
+ Definition Pending_of s (P : Requests_t) := [seq r <- P | r.(Requestor) == s].
+
+ (* Definition OREF_TRP := Ordinal T_REFI_GT_T_RP. *)
+
+ (* Start the refresh counter at T_RP, so that the first refresh you happen at
+ (T_REFI - T_RP) + T_RP cycles *)
+ Definition Init_state R := IDLE OZSlot OZCycle OPREA_date (Enqueue R [::]).
+
+ Definition nullreq :=
+ mkReq OZSlot 0 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ (* The next-state function of the arbiter *)
+ 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 cref P =>
+ let P' := Enqueue R P in
+ let s' := Next_slot s c in
+ let c' := Next_cycle c in
+ let cref' := Next_cycle_ref cref in
+ if (c == OZCycle) then (
+ (* Only need to test for refresh date here, since it can only happen here -- alignment *)
+ (* Will start with a REFRESH cycle *)
+ if (cref == OPREA_date) then (
+ match Pending_of s P with
+ | [::] => (REFRESH s' c' cref' P' nullreq, (PREA,nullreq))
+ | r :: _ => (REFRESH s' c' cref' P' r, (PREA,nullreq))
+ end
+ )
+ else (
+ match Pending_of s P with
+ | [::] => (IDLE s' c' cref' P', (NOP,nullreq))
+ | r :: _ => (RUNNING s' c' cref' (Enqueue R (Dequeue r P)) r, (NOP,r))
+ end
+ )
+ ) else (IDLE s' c' cref' P', (NOP, nullreq))
+ | RUNNING s c cref P r =>
+ let P' := Enqueue R P in
+ let s' := Next_slot s c in
+ let c' := Next_cycle c in
+ let cref' := Next_cycle_ref cref in
+ if (c == OPRE_date) then (RUNNING s' c' cref' P' r, (PRE,r))
+ else if (c == OACT_date) then (RUNNING s' c' cref' P' r, (ACT, r))
+ else if (c == OCAS_date) then (RUNNING s' c' cref' P' r, (Kind_of_req r, r))
+ else if (c == OLastCycle) then (IDLE s' c' cref' P', (NOP, nullreq))
+ else (RUNNING s' c' cref' P' r, (NOP, nullreq))
+ | REFRESH s c cref P r =>
+ let P' := Enqueue R P in
+ let s' := Next_slot s c in
+ let c' := Next_cycle c in
+ let cref' := Next_cycle_ref cref in
+ (* Could use cref as well to issue *)
+ if (c == OREF_date) then (REFRESH s' c' cref' P' r, (REF,nullreq))
+ (* No scheduling decisions while REFRESHING *)
+ else if (c == OPRE_date) then
+ (if (r == nullreq) then (IDLE s' c' cref' P', (NOP,nullreq)) else (RUNNING s' c' cref' P' r, (PRE,r)))
+ else (REFRESH s' c' cref' P' r, (NOP,nullreq))
+ end.
+
+ Global Instance TDMREF_implementation : Implementation_t :=
+ mkImplementation Init_state Next_state.
+
+ Program Definition TDMREF_arbitrate t :=
+ mkTrace
+ (Default_arbitrate t).(Arbiter_Commands)
+ (Default_arbitrate t).(Arbiter_Time)
+ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _.
+ Admit Obligations.
+
+ Program Instance TDMREF_arbiter : Arbiter_t :=
+ mkArbiter AF TDMREF_arbitrate _ _.
+ Admit Obligations.
+
+End TDMREF.
+
+Section TDMREF_sim.
+
+ (* DDR4-1600J *)
+ (* Density : 8Gb *)
+ (* Page Size : 1K (1G8 adressing) *)
+ (* 1tCK write preamble mode *)
+ (* 1tCK read preamble mode *)
+ (* AL = 0 *)
+ (* 1X Refresh mode *)
+ Program Instance SYS_CFG : System_configuration :=
+ {
+ BANKGROUPS := 4;
+ BANKS := 16;
+
+ (* [Figure 105] always the same *)
+ T_BURST := 4; (* INTRA/INTER *)
+
+ (* [Figure 105] 1tCK write preamble mode, AL = 0
+ -- independent of BC4 or BL8
+ -- depends on write preamble mode (1tCK or 2tCK)
+ -- depends on AL (what is AL ?) *)
+ T_WL := 9;
+
+ (* ACT to ACT, same and different bank groups, exclusevely inter-bank
+ -- depends on page size, which depends on device density (total size) and configuration
+ see (https://www.micron.com/-/media/client/global/documents/products/data-sheet/dram/ddr4/16gb_ddr4_sdram.pdf)
+ *)
+ T_RRD_s := 4; (* [Page 189] Max (4nCK, 5 ns) -> 4nCK = 1/800MHz * 4 = 5ns -> max is 5 -> 4 cycles at 800MHz*)
+ T_RRD_l := 5; (* [Page 189] Max (4nCK, 6 ns) -> 4nCK = 1/800MHz * 4 = 5ns -> max is 6 -> 4.8 ~ 5 cyles at 800MHz *)
+
+ (* Intra/inter-bank: Four ACT delay window *)
+ T_FAW := 20; (* [Page 189] 25ns *)
+
+ (* ACT to ACT, intra bank *)
+ T_RC := 38; (* [Page 163] 47.5 ns *)
+
+ (* PRE to ACT, intra bank *)
+ T_RP := 10; (* [Page 163] 12.5 ns *)
+
+ (* ACT to CAS, intra bank *)
+ T_RCD := 10; (* [Page 163] 12.5 ns *)
+
+ (* ACT to PRE, intra bank *)
+ T_RAS := 28; (* [Page 163] 35.0 ns *)
+
+ (* RD to PRE, intra bank *)
+ T_RTP := 6; (* [Page 189] Max (4nCK, 7.5ns) -> 4nCK = 1/800MHz * 4 = 5ns -> max is 7 -> 5.6 ~ 6 cycles at 800MHz *)
+
+ (* Write recovery time: R data to PRE *)
+ T_WR := 12; (* [Page 189] 15 ns *)
+
+ (* Read to write, inter and intra bank *)
+ T_RTW := 8; (* [Page 94] T_RTW = RL + BL/2 - WL + 2tCK = 11 + 8/2 - 9 + 2 = 8 *)
+
+ (* End of write operation to read *)
+ T_WTR_s := 2; (* [Page 189] Max (2nCK,2.5ns) -> 2nCK = 1/800MHz * 2 = 2.5ns -> max is 2.5ns -> 2 cycles at 800MHz *)
+ T_WTR_l := 6; (* [Page 189] Nax (4nCK,7.5ns) -> 4nCK = 5ns -> max is 7.5ns -> 6 cycles at 800MHz *)
+
+ T_CCD_s := 4;
+ T_CCD_l := 5;
+
+ T_REFI := 100; (* 6240 [Page 36] Refresh average time*)
+ T_RFC := 15; (* 280 [Page 36] *)
+ }.
+
+ Program Instance TDMREF_CFG : TDMREF_configuration :=
+ {
+ SN := 2;
+ SL := 50
+ }.
+
+ Existing Instance REQUESTOR_CFG.
+ Existing Instance TDMREF_implementation.
+ Existing Instance TDMREF_arbiter.
+
+ Axiom SN1 : 1 < SN.
+ Definition Slot1 := Ordinal SN1.
+
+ Program Definition ReqA0 := mkReq
+ OZSlot 10 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 5.
+
+ Program Definition ReqB0 := mkReq (* 3 instead of 14 *)
+ Slot1 20 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 10.
+
+ Definition test_req_seq := [:: ReqA0;ReqB0].
+
+ Program Instance AF : Arrival_function_t := Default_arrival_function_t test_req_seq.
+
+ (* Compute (Default_arbitrate 100).(Implementation_State). *)
+ Compute (Arbitrate 150).(Commands).
+
+ (* Next: introduce the concepts of page open / closed *)
+ (* Do proofs about TDMes ? *)
+
+End TDMes_sim.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/old_imps/TDMREF/TDMesREF.v b/framework/DRAM/Implementations/old_imps/TDMREF/TDMesREF.v
new file mode 100644
index 0000000000000000000000000000000000000000..eecae58708c85f8b828df8035705480fd1071235
--- /dev/null
+++ b/framework/DRAM/Implementations/old_imps/TDMREF/TDMesREF.v
@@ -0,0 +1,443 @@
+Set Warnings "-notation-overridden,-parsing".
+Set Printing Projections.
+
+From DRAM Require Export ImplementationInterface.
+From mathcomp Require Import fintype div ssrZ zify.
+From mathcomp Require Import ssreflect seq.
+
+From Coq Require Import Program FMapList OrderedTypeEx.
+
+(* FMapList.Make expects an instance of the OrderedType module, which we define as Nat_as_OT *)
+Module Import NatMap := FMapList.Make(Nat_as_OT).
+
+Section TDMesREF.
+
+ Context {SYS_CFG : System_configuration}.
+
+ Definition REF_start_date := T_REFI.
+ Definition PREA_date := T_REFI - T_RP.
+
+ Definition REF_date := T_RP.
+ Definition PRE_date := REF_date + T_RFC.
+ Definition ACT_date := PRE_date + T_RP.
+ Definition CAS_date := ACT_date + T_RCD.
+
+ Class TDMesREF_configuration :=
+ {
+ SN : nat;
+ SN_one : 1 < SN;
+
+ SL : nat;
+ SL_pos : 0 < SL;
+
+ (* There has to be enough time to complete a full PRE - ACT - CAS sequence *)
+ SL_CASS : CAS_date.+1 < SL;
+
+ (* SL has to be large enough to acomodate bus changing directions *)
+ SL_BUS_RD_TO_WR : T_RTW < SL;
+ SL_BUS_WR_TO_RD : T_WTR_l + T_WL + T_BURST < SL;
+
+ (* Other axioms about SL *)
+ T_RTP_SN_SL : T_RTP < SN * SL - CAS_date;
+ T_WTP_SN_SL : (T_WR + T_WL + T_BURST) < SN * SL - CAS_date;
+
+ T_RAS_SL : T_RP.+1 + T_RAS < SL;
+ T_RC_SL : T_RC < SL;
+ T_RRD_SL : T_RRD_l < SL;
+ T_CCD_SL : T_CCD_l < SL;
+ T_FAW_3SL : T_FAW < SL + SL + SL;
+ T_RCD_SL : T_RCD < SL;
+
+ (* Axiom A1: SL needs to be a divider of T_REFI *)
+ SL_REF_aligned : T_REFI %% SL == 0;
+
+ (* No need for disjoint banks if this is satisfied -- initial REF delay is big enough
+ to acomodate the write recovery time. This should always be the case, since T_RFC is big enough *)
+ SL_REF_cycle : (T_RP + T_RFC).+1 > (T_WL + T_BURST + T_WR);
+ }.
+
+ Context {TDMesREF_CFG : TDMesREF_configuration}.
+
+ (* -------------------- Additional Lemmas about SN ------------------------ *)
+ Lemma SN_pos : SN > 0.
+ specialize SN_one; lia.
+ Qed.
+
+ (* --------------------- Additional Lemmas about PREA_date ---------------- *)
+ (* Lemma PREA_date_GT_REF_date : REF_date < PREA_date.
+ specialize PREA_date_GT_ENDREF_date; unfold ENDREF_date; lia.
+ Qed. *)
+
+ Lemma REF_start_date_pos : 0 < REF_start_date.
+ unfold REF_start_date; specialize T_REFI_GT_T_RP; lia.
+ Qed.
+
+ (* ---------------------- Additional Lemmas about SL ---------------------- *)
+ Lemma SL_PRE : PRE_date < SL.
+ specialize SL_CASS; unfold PRE_date, CAS_date, ACT_date, PRE_date, REF_date; lia.
+ Qed.
+
+ Lemma SL_REF : REF_date < SL.
+ unfold REF_date; specialize T_RAS_SL; lia.
+ Qed.
+
+ Lemma SL_ACT : ACT_date < SL.
+ specialize SL_CASS; unfold CAS_date, ACT_date; lia.
+ Qed.
+
+ Lemma Last_cycle: SL.-1 < SL.
+ rewrite ltn_predL; apply SL_pos.
+ Qed.
+
+ Lemma SL_CAS: CAS_date < SL.
+ specialize SL_CASS as H; lia.
+ Qed.
+
+ Lemma SL_one: 1 < SL.
+ specialize SL_CASS; lia.
+ Qed.
+
+ Lemma SL_ACTS: ACT_date.+1 < SL.
+ specialize SL_CASS; unfold CAS_date, ACT_date; lia.
+ Qed.
+
+ Lemma CAS_ACT_SL : CAS_date - ACT_date < SL.
+ unfold CAS_date; specialize T_RCD_SL; lia.
+ Qed.
+
+ (* ------------------------ Additional Lemmas about ACT_date & CAS_date ---- *)
+ Lemma ACT_pos: 0 < ACT_date.
+ unfold ACT_date; specialize T_RP_pos; lia.
+ Qed.
+
+ Lemma CAS_pos: 0 < CAS_date.
+ unfold CAS_date; specialize T_RCD_pos; lia.
+ Qed.
+
+ (* ------------------------ Requestor ------------------------------------- *)
+ Record Requestor_t_def := mkRequestorSlack
+ {
+ nb : nat; (* the id of the requestor : no longer bounded by slot number *)
+ crit : bool; (* criticality *)
+
+ (* critical requests are bounded by the number of slots *)
+ crit_req : crit == true <-> nb < SN;
+ }.
+
+ Definition Same_Requestor (a b : Requestor_t_def) :=
+ a.(nb) == b.(nb).
+
+ Definition Requestor_t_def_eqdef (a b : Requestor_t_def) :=
+ (a.(nb) == b.(nb)) && (a.(crit) == b.(crit)).
+
+ Lemma Requestor_t_def_eqn : Equality.axiom Requestor_t_def_eqdef.
+ Admitted.
+
+ Canonical Requestor_t_def_eqMixin := EqMixin Requestor_t_def_eqn.
+ Canonical Requestor_t_def_eqType := Eval hnf in EqType Requestor_t_def Requestor_t_def_eqMixin.
+
+ Instance REQUESTOR_CFG : Requestor_configuration := {
+ Requestor_t := Requestor_t_def_eqType
+ }.
+
+ Context {AF : Arrival_function_t}.
+
+ (* ------------------------ Counter Types -------------------------------- *)
+ Definition Counter_t := ordinal SL.
+ Definition OZCycle := Ordinal SL_pos.
+ Definition OSlot1 := Ordinal SL_one.
+ Definition OREF_date := Ordinal SL_REF.
+ Definition OPRE_date := Ordinal SL_PRE.
+ Definition OACT_date := Ordinal SL_ACT.
+ Definition OCAS_date := Ordinal SL_CAS.
+ Definition OLastCycle := Ordinal Last_cycle.
+
+ 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.
+
+ (* Slot counter *)
+ Definition Slot_t := ordinal_eqType SN.
+ Definition OZSlot := Ordinal SN_pos.
+
+ 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.
+
+ (* Refresh counter *)
+ Definition Counter_ref_t := ordinal REF_start_date.
+
+ Lemma REF_start_date_GT_PREA_date : PREA_date < REF_start_date.
+ unfold PREA_date, REF_start_date; specialize T_RP_pos; specialize T_REFI_pos; lia.
+ Qed.
+
+ Definition OPREA_date := Ordinal REF_start_date_GT_PREA_date.
+ Definition OCycle0REF := Ordinal T_REFI_pos.
+
+ Definition Next_cycle_ref (c : Counter_ref_t) : Counter_ref_t :=
+ let nextcref := c.+1 < REF_start_date in
+ (if nextcref as X return (nextcref = X -> Counter_ref_t) then
+ (fun (P : nextcref = true) => Ordinal (P : nextcref))
+ else (fun _ => OCycle0REF)) Logic.eq_refl.
+
+ Definition Slack_t := NatMap.t nat.
+ Definition empty_nat_map := NatMap.empty nat.
+
+ (* ------------------------ State -------------------------------------- *)
+ Inductive TDM_state_t :=
+ | IDLE : Slot_t -> Slack_t -> Counter_t -> Counter_ref_t ->
+ Requests_t -> TDM_state_t
+ | RUNNING : Slot_t -> Slack_t -> Counter_t -> Counter_ref_t ->
+ Counter_t -> Requests_t -> Request_t-> TDM_state_t
+ | REFRESH : Slot_t -> Slack_t -> Counter_t -> Counter_ref_t ->
+ Requests_t -> Request_t -> TDM_state_t.
+
+ Global Instance ARBITER_CFG : Arbiter_configuration := {
+ State_t := TDM_state_t;
+ }.
+
+ (* ------------------------ Arbitration functions ----------------------- *)
+ Definition p_transform (x cs : nat) : nat :=
+ match (cs > 0) as X with
+ | true => if (x < cs) then (cs - 1) - x else (SN - 1 + cs) - x
+ | _ => (SN - 1) - x
+ end.
+
+ Definition egt (cs a b : nat) :=
+ gtn (p_transform a cs) (p_transform b cs).
+
+ Definition lp (cs : Slot_t) := if (nat_of_ord cs == 0) then (SN.-1) else cs.-1.
+
+ Definition dist (max a b : nat) : nat :=
+ if (b < a) then (a - b) else (if (b == a) then 0 else (max - (b - a))).
+
+ (* This function iterates over a list of request to choose the next one to be serviced *)
+ Program Definition edf_slack_crit (cs : Slot_t) (smap : Slack_t) := foldr (fun r_it r_saved =>
+ let cs_nat := nat_of_ord cs in
+ let r_it_crit := r_it.(Requestor).(crit) in
+ let r_it_id := r_it.(Requestor).(nb) in
+ let r_saved_crit := r_saved.(Requestor).(crit) in
+ let r_saved_id := r_saved.(Requestor).(nb) in
+ (* If request is non-critical *)
+ if ~~ (r_it_crit) then
+ (* safe to choose the non-critical request when the saved
+ request is not the upcoming one, which has the most priority *)
+ (if (r_saved_id != cs_nat) then r_it else r_saved)
+ else (
+ (* choose the request if:
+ a) r_it[i] > r_saved[i] , i.e., r_it has more priority than r_saved
+ b) r_it[i] is the due for the upcoming slot (most priority), this condition
+ is useful to overwrite previously selected non-critical requests
+ c) overwrite the default request, which has special date 0 *)
+ let cond := (egt cs_nat r_it_id r_saved_id) || (r_it_id == cs_nat) || (r_saved.(Date) == 0) in
+ let slack := find r_it.(Requestor).(nb) smap in
+ match slack with
+ | None => (* if there is no slack, then only consider cond *)
+ if cond then r_it else r_saved
+ | Some sl => (* if there is enough slack, then don't choose that request *)
+ let t := (r_it.(Date) %% (SL * SN)) in
+ if (sl > t) then r_saved else
+ (* if there is enough slack, then the
+ associated request is not priority, don't update variables *)
+ (if cond then r_it else r_saved)
+ end
+ )) (mkReq (mkRequestorSlack (lp cs) true _) 0 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0).
+ Next Obligation.
+ split; [ intros H; clear H | trivial ]; unfold lp.
+ destruct (nat_of_ord cs == 0); [ rewrite ltn_predL; exact SN_pos | ].
+ destruct cs; simpl; lia.
+ Qed.
+
+ Check edf_slack_crit.
+
+ Definition early_start cs cnt cref smap req :=
+ let ncs := nat_of_ord (Next_slot cs OLastCycle) in
+ (* if a refresh is scheduled, then early start is not allowed *)
+ if (OPREA_date - cref < SL) then false else (
+ if (ncs == req.(Requestor).(nb)) then true
+ else (let slack := find ncs smap in
+ match slack with
+ | None => false
+ | Some sl => SL.-1 - cnt < sl (* if next slot owner has enough slack, it is safe to early start *)
+ end
+ )).
+
+ Definition Enqueue (R P : Requests_t) := P ++ R.
+ Definition Dequeue r (P : Requests_t) := rem r P.
+
+ Program Definition nullreq := mkReq
+ (mkRequestorSlack 0 true _) 0 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+ Next Obligation.
+ split; [ intros _; exact SN_pos | trivial].
+ Qed.
+
+ Program Definition Next_state (R : Requests_t) (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 slmap c cref P =>
+ let P' := Enqueue R P in
+ let s' := Next_slot s c in
+ let c' := Next_cycle c in
+ let cref' := Next_cycle_ref cref in
+ if (c == OZCycle) then (
+ (* can only happen at OZCycle, because refresh cycles are aligned with slots *)
+ if (cref == OPREA_date) then (
+ match P with
+ | [::] =>
+ (REFRESH s' slmap c' cref' P' nullreq, (PREA,nullreq))
+ | _ => let req := edf_slack_crit s slmap P in
+ (REFRESH s' slmap c' cref' P' req, (PREA,nullreq))
+ end
+ ) else (
+ match P withL
+ | [::] => (IDLE s' slmap c' cref' P',(NOP,nullreq))
+ | _ => let req := edf_slack_crit s slmap P in
+ (* both counters will be equal in this case -> no offset *)
+ (RUNNING s' slmap c' cref' OZCycle (Enqueue R (Dequeue req P)) req, (NOP,req))
+ end
+ )
+ ) else ( (* early start *)
+ (* if arbitrating in the middle of slot, then priority rules chance, hence
+ the different argument sent to the scheduling function *)
+ let req := edf_slack_crit (Next_slot s OLastCycle) slmap P in
+ if (early_start s c cref slmap req) then
+ (* if early start will happen, then the counter offset should be the counter value *)
+ (RUNNING s' slmap c' cref' c (Enqueue R (Dequeue req P)) req, (NOP,req))
+ else (IDLE s' slmap c' cref' P', (NOP,nullreq))
+ )
+ | RUNNING s slmap c cref cnt_offset P r =>
+ let P' := Enqueue R P in
+ let s' := Next_slot s c in
+ let c' := Next_cycle c in
+ let cref' := Next_cycle_ref cref in
+ let pre_cond := Ordinal (@ltn_pmod (cnt_offset + PRE_date) SL SL_pos) in
+ let act_cond := Ordinal (@ltn_pmod (cnt_offset + ACT_date) SL SL_pos) in
+ let cas_cond := Ordinal (@ltn_pmod (cnt_offset + CAS_date) SL SL_pos) in
+ let end_cond := Ordinal (@ltn_pmod (cnt_offset + SL.-1) SL SL_pos) in
+ (* let cnt_cmd := nat_of_ord c + nat_of_ord cnt_offset in *)
+ if (c == pre_cond) then (RUNNING s' slmap c' cref' cnt_offset P' r, (PRE,r))
+ else if (c == act_cond) then (RUNNING s' slmap c' cref' cnt_offset P' r, (ACT, r))
+ else if (c == cas_cond) then (RUNNING s' slmap c' cref' cnt_offset P' r, (Kind_of_req r, r))
+ else if (c == end_cond) then ( (* calculate new slack *)
+ let req_id := r.(Requestor).(nb) in
+ let slack' := if r.(Requestor).(crit) then
+ (SL.-1 - c) + ((dist SN (nat_of_ord s) req_id) * SL) else 0 in
+ let slmap' := NatMap.add req_id slack' slmap in
+ (IDLE s' slmap' c' cref' P', (NOP, nullreq))
+ ) else (RUNNING s' slmap c' cref' cnt_offset P' r, (NOP, nullreq))
+ | REFRESH s slmap c cref P r =>
+ let P' := Enqueue R P in
+ let s' := Next_slot s c in
+ let c' := Next_cycle c in
+ let cref' := Next_cycle_ref cref in
+ if (c == OREF_date) then (REFRESH s' slmap c' cref' P' r, (REF,nullreq))
+ else if (c == OPRE_date) then (
+ if (r == nullreq) then (IDLE s' slmap c' cref' P', (NOP,nullreq))
+ (* IN this case the two running counters will be equal *)
+ else (RUNNING s' slmap c' cref' c' P' r, (PRE,r))
+ ) else (REFRESH s' slmap c' cref' P' r, (NOP,nullreq))
+ end.
+
+ Definition Init_state R :=
+ IDLE OZSlot empty_nat_map OZCycle OPREA_date (Enqueue R [::]).
+
+ Instance TDMesREF_implementation : Implementation_t :=
+ mkImplementation Init_state Next_state.
+
+ (* Start proving *)
+ Program Definition TDMesREF_arbitrate t :=
+ mkTrace
+ (Default_arbitrate t).(Arbiter_Commands)
+ (Default_arbitrate t).(Arbiter_Time)
+ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _.
+ Admit Obligations.
+
+ Program Instance TDMesREF_arbiter : Arbiter_t :=
+ mkArbiter AF TDMesREF_arbitrate _ _.
+ Admit Obligations.
+
+End TDMesREF.
+
+Section TDMesREF_sim.
+
+ Program Instance SYS_CFG : System_configuration :=
+ {
+ BANKGROUPS := 1;
+ BANKS := 8;
+
+ T_BURST := 1;
+ T_WL := 1;
+ T_RRD_s := 1;
+ T_RRD_l := 2;
+ T_FAW := 20;
+ T_RC := 3;
+ T_RP := 2;
+ T_RCD := 2;
+ T_RAS := 1;
+ T_RTP := 1;
+ T_WR := 1;
+ T_RTW := 1;
+ T_WTR_s := 1;
+ T_WTR_l := 2;
+ T_CCD_s := 1;
+ T_CCD_l := 2;
+
+ T_REFI := 48;
+ T_RFC := 4;
+ }.
+
+ Program Instance TDMdsREF_CFG : TDMesREF_configuration :=
+ {
+ SN := 3;
+ SL := 12;
+ }.
+
+ Existing Instance REQUESTOR_CFG.
+ Existing Instance TDMesREF_implementation.
+ Existing Instance TDMesREF_arbiter.
+
+ Hint Extern 1 => split; [intro H; lia | trivial] : core.
+
+ Program Definition ReqA0 := mkReq
+ (mkRequestorSlack 0 true _) 6 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 5.
+
+ Program Definition ReqB0 := mkReq (* 3 instead of 14 *)
+ (mkRequestorSlack 1 true _) 15 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 10.
+
+ Program Definition ReqC0 := mkReq
+ (mkRequestorSlack 2 true _) 39 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqB1 := mkReq
+ (mkRequestorSlack 1 true _) 28 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqA1 := mkReq
+ (mkRequestorSlack 0 true _) 40 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqC1 := mkReq
+ (mkRequestorSlack 2 true _) 40 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqB2 := mkReq
+ (mkRequestorSlack 1 true _) 44 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Program Definition ReqA2 := mkReq
+ (mkRequestorSlack 0 true _) 62 RD (Nat_to_bankgroup 0) (Nat_to_bank 0) 0.
+
+ Definition test_req_seq := [:: ReqA0;ReqB0;ReqC0].
+
+ Program Instance AF : Arrival_function_t := Default_arrival_function_t test_req_seq.
+
+ (* Compute (Default_arbitrate 36).(Implementation_State). *)
+ Compute seq.map (fun cmd => (cmd.(CKind),cmd.(CDate),cmd.(Request).(Requestor).(nb))) (Arbitrate 64).(Commands).
+
+ (* Next: introduce the concepts of page open / closed *)
+ (* Do proofs about TDMes ? *)
+
+End TDMesREF_sim.
\ No newline at end of file
diff --git a/framework/DRAM/Implementations/old_imps/TDMREF/TDMesREF_proofs.v b/framework/DRAM/Implementations/old_imps/TDMREF/TDMesREF_proofs.v
new file mode 100644
index 0000000000000000000000000000000000000000..7f2ed2a3b0080981f6874b755c1e0516d72a975d
--- /dev/null
+++ b/framework/DRAM/Implementations/old_imps/TDMREF/TDMesREF_proofs.v
@@ -0,0 +1,2873 @@
+Set Warnings "-notation-overridden,-parsing".
+Set Printing Projections.
+
+From mathcomp Require Export fintype div.
+From Coq Require Import Program Psatz Lia ZArith Zify.
+(* Require Import Psatz Lia. *)
+From DRAM Require Export TDMesREF.
+
+(* From Hammer Require Import Tactics. *)
+
+Section TDMesREF_proofs.
+
+ Context {SYS_CFG : System_configuration}.
+ Context {TDMesREF_CFG : TDMesREF_configuration}.
+
+ Existing Instance REQUESTOR_CFG.
+ Context {AF : Arrival_function_t}.
+
+ Existing Instance ARBITER_CFG.
+ Existing Instance TDMesREF_implementation.
+
+ Notation "# t" := (Default_arbitrate t) (at level 0).
+
+ Definition TDM_counter (AS : TDM_state_t) :=
+ match AS with
+ | IDLE _ _ c _ _ => c
+ | RUNNING _ _ c _ _ _ _ => c
+ | REFRESH _ _ c _ _ _ => c
+ end.
+
+ Ltac destruct_state t :=
+ let x := fresh "Hs" in destruct # (t).(Implementation_State) eqn:x;
+ repeat lazymatch goal with
+ | |- context [?c == OZCycle] =>
+ let x := fresh "Hc0" in destruct (c == OZCycle) eqn:x
+ | |- context [?c == OPREA_date] =>
+ let x := fresh "Hprea" in destruct (c == OPREA_date) eqn:x
+ | |- context [match ?r with | [::] => _ | _ => _ end] =>
+ let x := fresh "Hr" in destruct r eqn:x
+ | |- context [early_start _ _ _ _] =>
+ let x := fresh "Hes" in destruct (early_start _ _ _ _) eqn:x
+ | |- context [?c == Ordinal (n:=SL) (m :=(?c1 + PRE_date) %% SL) _] =>
+ let x := fresh "Hpre" in destruct (c == Ordinal (n:=SL) (m :=(c1 + PRE_date) %% SL) _) eqn:x
+ | |- context [?c == Ordinal (n:=SL) (m :=(?c1 + ACT_date) %% SL) _] =>
+ let x := fresh "Hact" in destruct (c == Ordinal (n:=SL) (m :=(c1 + ACT_date) %% SL) _) eqn:x
+ | |- context [?c == Ordinal (n:=SL) (m :=(?c1 + CAS_date) %% SL) _] =>
+ let x := fresh "Hcas" in destruct (c == Ordinal (n:=SL) (m :=(c1 + CAS_date) %% SL) _) eqn:x
+ | |- context [?c == Ordinal (n:=SL) (m :=(?c1 + SL.-1) %% SL) _] =>
+ let x := fresh "end" in destruct (c == Ordinal (n:=SL) (m :=(c1 + SL.-1) %% SL) _) eqn:x
+ | |- context [?c == OPRE_date] =>
+ let x := fresh "Hpre_ref" in destruct (c == OPRE_date) eqn:x
+ | |- context [?c == OREF_date] =>
+ let x := fresh "Href" in destruct (c == OREF_date) eqn:x
+ | |- context [?r == nullreq] =>
+ let x := fresh "Href_r" in destruct (r == nullreq) eqn:x
+ end; simpl.
+
+
+ (* ---------------------------------------------------------------------- *)
+ (* ------------- Arithmetic Lemmas -------------------------------------- *)
+ (* ---------------------------------------------------------------------- *)
+
+ Lemma add_sub a b c : a = b + c -> c = a - b.
+ Proof. by move=> ->; rewrite addnC -subnBA // subnn subn0. Qed.
+
+ Lemma dvdS_modnS d m:
+ d > 0 -> (d %| m.+1) -> (m %% d).+1 = d.
+ Proof.
+ move => lt0d /dvdnP [k] mlk.
+ move/eqP: (divn_eq m d).
+ set m' := m %/ d; set m'' := m %% d.
+ rewrite -eqSS -addnS mlk => /eqP /add_sub.
+ rewrite -mulnBl => m''l.
+ move: (ltn_pmod m lt0d).
+ rewrite {}m''l -{2}(mul1n d) leq_mul2r eqn0Ngt lt0d //= leq_eqVlt => /orP [/eqP -> | ];
+ first by rewrite mul1n.
+ (* rewrite /add_sub. *)
+ by rewrite ltnS leqn0 subn_eq0 leqNgt ltn_divLR // mlk leqnn.
+ Qed.
+
+ (* ---------------------------------------------------------------------- *)
+ (* ------------- Auxiliary Lemmas / Basic Statements -------------------- *)
+ (* ---------------------------------------------------------------------- *)
+
+ Lemma NextCycle_inj c c0 :
+ c = c0 -> Next_cycle c = Next_cycle c0.
+ Proof.
+ intros H; rewrite H; reflexivity.
+ Qed.
+
+ Lemma NextCycle_inj_nat c c0 :
+ nat_of_ord c = nat_of_ord c0 ->
+ nat_of_ord (Next_cycle c) = nat_of_ord (Next_cycle c0).
+ Proof.
+ intros H;
+ unfold Next_cycle at 1; set (Hc := c.+1 < SL);
+ dependent destruction Hc;
+ apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro;
+ unfold Next_cycle; set (Hc := c0.+1 < SL);
+ dependent destruction Hc;
+ apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; lia.
+ 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.
+
+ (* ---------------------------------------------------------------------- *)
+ (* ------------- Counter proofs ----------------------------------------- *)
+ (* ---------------------------------------------------------------------- *)
+
+ 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; [ by rewrite modnn | exact SL_pos]. }
+ { apply nat_ltlt_empty in Hc; [ done | exact SL_pos | exact x]. }
+ Qed.
+
+ Lemma Time_counter_modulo t:
+ (t %% SL) = TDM_counter (Default_arbitrate t).(Implementation_State).
+ Proof.
+ induction t; simpl.
+ { specialize SL_pos as H; apply lt0n_neq0 in H;
+ move : H => /eqP H; by rewrite mod0n. }
+ { unfold Next_state, TDM_counter in *; simpl in *;
+ destruct_state t; by apply TDM_next_cycle_modulo in IHt. }
+ Qed.
+
+ Lemma ACT_modulo_date t cmd:
+ cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isACT cmd ->
+ (exists d, d < SL /\
+ cmd.(CDate) %% SL == Next_cycle (Ordinal (@ltn_pmod (d + ACT_date) SL SL_pos))).
+ Proof.
+ induction t; [ done | ].
+ simpl; unfold Next_state.
+ destruct_state t; rewrite in_cons; intros H iACT;
+ move: H => /orP [/eqP H | H];
+ try rewrite H /isACT //= in iACT;
+ try apply IHt in H; try exact iACT; try exact H.
+ 2: unfold Kind_of_req in iACT; destruct (r0.(Kind)); done.
+ exists c1; split; [ destruct c1; done | ].
+ rewrite H //= Time_counter_modulo //= /Next_state Hs Hpre Hact /TDM_counter //=.
+ clear iACT H Hs IHt Hpre c0 r r0 s s0.
+ move: Hact => /eqP Hact; by rewrite Hact.
+ Qed.
+
+ (* finish this one, should be like the one above *)
+ Lemma CAS_modulo_date t cmd:
+ cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isCAS cmd ->
+ (exists d, d < SL /\
+ cmd.(CDate) %% SL == Next_cycle (Ordinal (@ltn_pmod (d + CAS_date) SL SL_pos))).
+ Admitted.
+
+ (*
+ Lemma TDMes_inc_counter t x :
+ let c := Ordinal (@ltn_pmod x SL SL_pos) in
+ TDM_counter (# t).(Implementation_State) = c ->
+ let c' := Ordinal (@ltn_pmod x.+1 SL SL_pos) in
+ TDM_counter (# (t.+1)).(Implementation_State) = c'.
+ Admitted.
+
+ Lemma TDMes_add_counter t x d:
+ let c := Ordinal (@ltn_pmod x SL SL_pos) in
+ TDM_counter (# t).(Implementation_State) = c ->
+ let c' := Ordinal (@ltn_pmod (x + d) SL SL_pos) in
+ TDM_counter (# (t + d)).(Implementation_State) = c'.
+ Proof.
+ cbv zeta; intros H; induction d; [ rewrite !addn0; exact H | ];
+ rewrite addnS; simpl; unfold Next_state; destruct_state (t + d);
+ rewrite -Hs in IHd.
+ { specialize (TDMes_inc_counter (t + d) (x + d)) as Hinc; cbv zeta in Hinc;
+ apply Hinc in IHd; clear Hinc;
+ rewrite /TDM_counter //= /Next_state Hs Hc0 Hprea //= in IHd.
+ (* hard because of proofs ... do the same but with the nat version *)
+ admit.
+ }
+ Admitted.
+
+ Lemma TDMes_inc_counter_nat t x :
+ let c := Ordinal (@ltn_pmod x SL SL_pos) in
+ nat_of_ord (TDM_counter (# t).(Implementation_State)) = nat_of_ord c ->
+ let c' := Ordinal (@ltn_pmod x.+1 SL SL_pos) in
+ nat_of_ord (TDM_counter (# (t.+1)).(Implementation_State)) = nat_of_ord c'.
+ Admitted.
+
+ Lemma TDMes_add_counter_nat t x d:
+ let c := Ordinal (@ltn_pmod x SL SL_pos) in
+ nat_of_ord (TDM_counter (# t).(Implementation_State)) = nat_of_ord c ->
+ let c' := Ordinal (@ltn_pmod (x + d) SL SL_pos) in
+ nat_of_ord (TDM_counter (# (t + d)).(Implementation_State)) = nat_of_ord c'.
+ Proof.
+ cbv zeta; induction d; [ rewrite !addn0; done | ];
+ move: IHd; rewrite addnS; simpl;
+ unfold Next_state; destruct_state (t + d); intros IHd H;
+ apply IHd in H; clear IHd;
+ specialize (TDMes_inc_counter_nat (t + d) (x + d)) as Hinc; cbv zeta in Hinc;
+ rewrite Hs //= in Hinc; apply Hinc in H; clear Hinc;
+ rewrite /TDM_counter /Next_state Hs in H;
+ try rewrite Hc0 in H; try rewrite Hprea in H;
+ try rewrite Hes in H; try rewrite Hpre in H;
+ try rewrite Hact in H; try rewrite Hcas in H;
+ try rewrite Hcas end0 in H; try rewrite end0 in H;
+ try rewrite Href in H; try rewrite Hpre_ref in H;
+ try rewrite Href_r in H; try rewrite -addnS //= in H;
+ rewrite -addnS //= in H.
+ Qed.
+
+ *)
+
+ Lemma TDMes_inc_counter_nat_NC t x :
+ let c := Next_cycle (Ordinal (@ltn_pmod x SL SL_pos)) in
+ nat_of_ord (TDM_counter (# t).(Implementation_State)) = nat_of_ord c ->
+ let c' := Next_cycle (Ordinal (@ltn_pmod x.+1 SL SL_pos)) in
+ nat_of_ord (TDM_counter (# (t.+1)).(Implementation_State)) = nat_of_ord c'.
+ Proof.
+ cbv zeta; simpl; unfold Next_state; destruct_state t; intros H;
+ apply NextCycle_inj_nat; rewrite H; clear H;
+ simpl; unfold Next_cycle; simpl; set (Hc := (x %% SL).+1 < SL);
+ dependent destruction Hc;
+ apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro;
+ try (
+ specialize (modnS x0 SL) as HmodnS;
+ destruct (SL %| x0.+1) eqn:HH; [ by rewrite HmodnS | ];
+ rewrite -HmodnS in x; clear HmodnS e;
+ contradict x; apply Bool.not_false_iff_true;
+ apply (ltn_pmod); exact SL_pos ).
+ all:
+ specialize (modnS x0 SL) as HmodnS;
+ destruct (SL %| x0.+1) eqn:HH; [ | rewrite -HmodnS; reflexivity];
+ apply dvdS_modnS in HH; [ | exact SL_pos ];
+ rewrite HH ltnn in x; done.
+ Qed.
+
+ Lemma TDMes_add_counter_nat_NC t x d:
+ let c := Ordinal (@ltn_pmod x SL SL_pos) in
+ nat_of_ord (TDM_counter (# t).(Implementation_State)) = nat_of_ord (Next_cycle c) ->
+ let c' := Ordinal (@ltn_pmod (x + d) SL SL_pos) in
+ nat_of_ord (TDM_counter (# (t + d)).(Implementation_State)) = nat_of_ord (Next_cycle c').
+ Proof.
+ cbv zeta; induction d; [ rewrite !addn0; done | ];
+ move: IHd; rewrite addnS; simpl;
+ specialize (TDMes_inc_counter_nat_NC (t + d) (x + d)); cbv zeta;
+ simpl; unfold Next_state; destruct_state (t + d); intros;
+ apply IHd in H0; clear IHd;
+ apply H in H0; clear H;
+ rewrite addnS; done.
+ Qed.
+
+ 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.
+
+ Lemma Modulo_time_distance_or t t':
+ TDM_counter (Default_arbitrate t).(Implementation_State) == TDM_counter (Default_arbitrate t').(Implementation_State)
+ -> t' + SL <= t \/ t + SL <= t' \/ t = t'.
+ Proof.
+ intros H; destruct (t' < t) eqn:Hlt.
+ { apply Modulo_time_distance in H; [ by left | exact Hlt]. }
+ rewrite ltnNge in Hlt; apply negbFE in Hlt.
+ rewrite leq_eqVlt in Hlt; move: Hlt => /orP [/eqP Heq | Hlt]; [ right; by right | ].
+ move: H => /eqP H; apply Logic.eq_sym in H; move: H => /eqP H.
+ apply Modulo_time_distance in H; [ right; by left | exact Hlt ].
+ Qed.
+
+ Lemma TDM_date_gt_0 cmd t:
+ cmd \in (Default_arbitrate t).(Arbiter_Commands) -> cmd.(CDate) > 0.
+ Proof.
+ induction t; [ done | ].
+ simpl; unfold Next_state; destruct_state t.
+ all: intros H; try (rewrite in_cons in H; move: H => /orP [/eqP H | H]).
+ all: (by rewrite H || by apply IHt in H).
+ Qed.
+
+ (* ------------------------------------------------------------------------ *)
+ (* Trying to get my proof to go ------------------------------------------- *)
+
+ Definition Early_start_trigger t : bool :=
+ match (# t).(Implementation_State) with
+ | IDLE s slmap c cref P => (c != OZCycle) &&
+ let req := edf_slack_crit (Next_slot s slmap P in
+ (early_start s c cref slmap req)
+ | _ => false
+ end.
+
+ Definition Normal_start_trigger t :=
+ match (# t).(Implementation_State) with
+ | IDLE s slmap c cref P => (c == OZCycle) && (cref != OPREA_date) && (P != [::])
+ | _ => false
+ end.
+
+ Definition Start_trigger t := Early_start_trigger t || Normal_start_trigger t.
+
+ (* This one could be maybe proved by induction on t' *)
+ Lemma No_starts_for_a_while_aux t:
+ (Start_trigger t) -> forall t', t < t' -> t' < t + SL ->
+ ~~ (Start_trigger t').
+ Proof.
+ intros Hstart t' Hlb Hub; unfold Start_trigger, Early_start_trigger, Normal_start_trigger in *;
+ induction t'; [ done | ].
+ destruct (# t).(Implementation_State) eqn:Hs_t; try done.
+ rename s into s_t, s0 into slack_t, c into cnt_t, c0 into cref_t, r into r_t.
+ destruct (cnt_t != OZCycle) eqn:Hc0.
+ { (* first consider an early start trigger at t *)
+ assert ((cnt_t == OZCycle) = false) as Hc0_; [ lia | ]; rewrite Hc0_ in Hstart.
+ cbn in Hstart; rewrite Bool.orb_false_r in Hstart.
+ simpl; unfold Next_state.
+ destruct (# t').(Implementation_State) eqn:Hs_t';
+ rename s into s_t', s0 into slack_t', c into cnt_t', c0 into cref_t', r into r_t'.
+ rewrite ltnS leq_eqVlt in Hlb; move: Hlb => /orP [/eqP Heq |Hlt].
+ { clear IHt'; subst t'.
+ rewrite Hs_t' in Hs_t;
+ injection Hs_t as Hinj; subst r_t' s_t' slack_t' cnt_t' cref_t'.
+ rewrite Hc0_. Hstart.
+ }
+
+ }
+
+ destruct_state t'.
+
+ rewrite andb_false_r.
+ 2: { }
+
+ destruct_state t.
+
+
+ simpl; unfold Next_state; destruc
+
+ destruct Hlt as [Hlt_ Hlt].
+ Admitted.
+
+ (* if t and t' are the time instants where to requests starts being processed, they have to be separated by
+ at least SL *)
+ Lemma No_starts_for_a_while t t' :
+ t != t' -> (Start_trigger t) -> (Start_trigger t') -> t + SL <= t' \/ t' <= t - SL.
+ Proof.
+ intros Hdiff Hs Hs';
+ rewrite neq_ltn in Hdiff; move: Hdiff => /orP [Hlt | Hlt]; [ left | right].
+ {
+ (* specialize (No_starts_for_a_while_aux t Hs t') as H. *)
+ unfold Start_trigger, Early_start_trigger, Normal_start_trigger in Hs.
+ }
+
+
+
+ Admitted.
+
+ (* only important to say that a start condition has been triggered, not necessarily the one related to the command *)
+ (* not sure I can prove this though ... *)
+ Lemma Request_from_CAS a t :
+ a \in (# t).(Arbiter_Commands) -> isCAS a ->
+ exists t', t' = a.(CDate) - CAS_date /\ (Start_trigger t').
+ Admitted.
+
+ (* Have to generalize this to any two equal types of commands *)
+ Lemma CAS_separation a b t:
+ a \in (# t).(Arbiter_Commands) -> isCAS a ->
+ b \in (# t).(Arbiter_Commands) -> isCAS b ->
+ Before a b -> Apart_at_least a b SL.
+ Admitted.
+
+ (* --------------------------------------------------------------------- *)
+ Definition TDM_offset t : option Counter_t :=
+ match (# t).(Implementation_State) with
+ | IDLE _ _ _ _ _ => None
+ | RUNNING _ _ _ _ a_ofs _ _ => Some a_ofs
+ | REFRESH _ _ _ _ _ _ => None
+ end.
+
+ Definition Aligned ta tb :=
+ match (TDM_offset ta),(TDM_offset tb) with
+ | Some a, Some b => (a == b)
+ | _,_ => true
+ end.
+
+ Definition diff (a b : option Counter_t) : nat :=
+ match a,b with
+ | Some a', Some b' =>
+ let an := nat_of_ord a' in
+ let bn := nat_of_ord b' in
+ if (an > bn) then (an - bn) else (bn - an)
+ | _,_ => 0
+ end.
+
+ Lemma CAS_after_ACT a t :
+ a \in (# t).(Arbiter_Commands) -> isACT a ->
+ exists b, b \in (# t).(Arbiter_Commands)
+ /\ isCAS b
+ /\ b.(CDate) = a.(CDate) + T_RCD.
+ Admitted.
+
+
+ Lemma CMD_separation ta tb :
+ let a_ofs := TDM_offset ta in
+ let b_ofs := TDM_offset tb in
+ TDM_counter (# ta).(Implementation_State) == Next_cycle (Ordinal (@ltn_pmod (a_ofs + x) SL SL_pos)) ->
+ TDM_counter (# tb).(Implementation_State) == Next_cycle (Ordinal (@ltn_pmod (b_ofs + x) SL SL_pos)) ->
+ ta +
+
+
+ (* This is incorrect, need to go from commands rather than equal counters ... *)
+ Lemma Counter_Alignment ta tb:
+ let ca := TDM_counter (# ta).(Implementation_State) in
+ let cb := TDM_counter (# tb).(Implementation_State) in
+ let a_ofs := TDM_offset ta in
+ let b_ofs := TDM_offset tb in
+ ca == cb -> ~~ Aligned ta tb ->
+ (ta + SL + (diff a_ofs b_ofs) <= tb) \/ (tb + SL + (diff a_ofs b_ofs) <= ta).
+ Proof.
+ unfold Aligned, TDM_offset, TDM_counter;
+ destruct_state ta; destruct_state tb; try done; intros Hceq Halign.
+ rename s into s_a, s0 into sl_a, c into cnt_a, c0 into cref_a,
+ c1 into ofs_a, r into P_a, r0 into r_a;
+ rename s1 into s_b, s2 into sl_b, c2 into cnt_b, c3 into cref_b,
+ c4 into ofs_b, r1 into P_b, r2 into r_b.
+ destruct (ta < tb) eqn:Hdate.
+ { left.
+ destruct (ofs_b < ofs_a) eqn:Hltn.
+ Admitted.
+
+ (* ---------------------------------------------------------------------- *)
+ (* ------------Proofs about Timing Constraints -------------------------- *)
+ (* ---------------------------------------------------------------------- *)
+
+ Theorem Cmds_T_RCD_ok t a b:
+ a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
+ ACT_to_CAS a b -> Same_Bank a b -> Before a b ->
+ Apart_at_least a b T_RCD.
+ Proof.
+ intros Ha Hb AtC SB aBb; rewrite /Apart_at_least;
+ unfold ACT_to_CAS in AtC; move: AtC => /andP [Aa Cb].
+
+ apply ACT_modulo_date in Ha as Haux; [ | exact Aa ];
+ destruct Haux as [a_offset [a_offset_ub Ha']];
+ apply CAS_modulo_date in Hb as Haux; [ | exact Cb ];
+ destruct Haux as [b_offset [b_offset_ub Hb']].
+
+ apply CAS_after_ACT in Ha as Haux; [ | exact Aa];
+ destruct Haux as [cas [Hcas [iC cdate]]].
+
+
+
+
+ rewrite Time_counter_modulo in Ha'; move: Ha'; set (ca := Next_cycle _); intros Ha';
+ rewrite Time_counter_modulo in Hb'; move: Hb'; set (cb := Next_cycle _); intros Hb'.
+ destruct (a_offset == b_offset) eqn:Hof.
+ { (* equal offset *)
+ move: Hof => /eqP Hof; subst a_offset; clear a_offset_ub;
+ set (d := CAS_date - ACT_date); unfold ca in Ha'; move: Ha' => /eqP Ha'.
+ (* move the (a) counter *)
+ apply TDMes_add_counter_nat_NC with (d := d) in Ha'; unfold d in Ha'.
+ assert (ACT_date <= CAS_date) as Hact_cas; [ unfold CAS_date; lia | ];
+ apply subnKC in Hact_cas; unfold cb in Hb'; rewrite -Hact_cas addnA in Hb'.
+ (* counters are finally equal *)
+ rewrite -Ha' in Hb'.
+ apply Modulo_time_distance_or in Hb'; destruct Hb' as [H0 | [H1 | H2]].
+ { (* the correct case *)
+ assert ((CAS_date - ACT_date) + SL > T_RCD); [ unfold CAS_date; lia | lia ]. }
+ { (* incorrect case *)
+ contradict aBb; unfold Before; apply /negP; rewrite -leqNgt.
+ rewrite addnC in H1; rewrite -leq_psubRL in H1; [ | by apply TDM_date_gt_0 in Hb ].
+ apply leq_trans with (p := a.(CDate)) in H1; [ exact H1 | ].
+ rewrite -subnBA; [ | by rewrite leq_eqVlt CAS_ACT_SL orbT ].
+ by apply leq_subr. }
+ { (* incorrect case *)
+ rewrite H2 leq_add2l; unfold CAS_date; lia. }}
+ { (* different offsets *)
+ move: Hof => /eqP Hof; assert (a_offset != b_offset); [ lia | ]; clear Hof; rename H into Hof.
+ move: Hof; rewrite neq_ltn => /orP [Hof | Hof].
+ { (* a_offset < b_offset *)
+ set (d := CAS_date - ACT_date); unfold ca in Ha'; move: Ha' => /eqP Ha'.
+ (* move the (a) counter *)
+ apply TDMes_add_counter_nat_NC with (d := d) in Ha'; unfold d in Ha'.
+ apply TDMes_add_counter_nat_NC with (d := b_offset - a_offset) in Ha'.
+ assert ((a_offset + ACT_date + (CAS_date - ACT_date) + (b_offset - a_offset)) = b_offset + CAS_date).
+ { assert (ACT_date <= CAS_date) as Hact_cas; [ unfold CAS_date; lia | ].
+ apply subnKC in Hact_cas; rewrite -{2}Hact_cas.
+ assert (a_offset <= b_offset) as H_aof_bof; [ lia | ].
+ apply subnKC in H_aof_bof; rewrite -{2}H_aof_bof. lia.
+ }
+ rewrite H in Ha'; clear H; unfold cb in Hb'.
+ rewrite -Ha' in Hb'.
+
+ (* apply Modulo_time_distance in Hb'. *)
+
+ (* move: Hb' => /eqP Hb'; apply Logic.eq_sym in Hb'; move: Hb' => /eqP Hb'. *)
+ apply Modulo_time_distance_or in Hb'; destruct Hb' as [H0 | [H1 | H2]].
+ (* apply Modulo_time_distance in Hb'. destruct Hb' as [H0 | [H1 | H2]]. *)
+ { have: (CAS_date - ACT_date) + (b_offset - a_offset) + SL > T_RCD;
+ [ unfold CAS_date; lia | ]; lia. }
+ { contradict aBb; unfold Before; apply /negP; rewrite -leqNgt.
+ rewrite addnC in H1; rewrite -leq_psubRL in H1; [ | by apply TDM_date_gt_0 in Hb ].
+ apply leq_trans with (p := a.(CDate)) in H1; [ exact H1 | ].
+ admit. }
+ { rewrite H2 -addnA leq_add2l; unfold CAS_date; lia. }}
+ { (* a_offset > b_offset *)
+
+ }
+ }
+
+ (*************************************************************************************************)
+ (** UTILITY PROOFS *******************************************************************************)
+ (*************************************************************************************************)
+
+ 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 TDM_nextcycle_ozcycle : nat_of_ord (Next_cycle OZCycle) = 1.
+ Proof.
+ rewrite /OZCycle /Next_cycle //=; set (Hc := 1 < SL); dependent destruction Hc.
+ all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
+ 2: by rewrite SL_one in x.
+ 1: reflexivity.
+ 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_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), (c == OZCycle), (c == OACT_date), (c == OCAS_date),
+ (c == OLastCycle); try destruct (Pending_of _ _); 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 //=.
+ simpl; rewrite /Next_state //=;
+ destruct (Default_arbitrate t').(Implementation_State), (c == OZCycle), (c == OACT_date), (c == OCAS_date),
+ (c == OLastCycle); try destruct (Pending_of _ _); simpl.
+ all: try (rewrite in_cons; apply /orP; right; exact H). }
+ Qed.
+
+ Lemma Cmd_in_trace cmd t:
+ cmd \in (Default_arbitrate t).(Arbiter_Commands) ->
+ cmd.(CDate) <= t.
+ Proof.
+ intros H.
+ induction t.
+ { by simpl in H. }
+ simpl in H; rewrite /Next_state in H.
+ destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (c == OZCycle) eqn:Hz, (c == OACT_date) eqn:Hact, (c == OCAS_date) eqn:Hcas,
+ (c == OLastCycle) eqn:Hlast; try destruct (Pending_of _ _) eqn:HP; simpl in H.
+ all: try (rewrite in_cons in H; move: H => /orP [/eqP H | H]); try (subst cmd; by simpl).
+ all: try (apply IHt in H; by apply ltnW).
+ Qed.
+
+ Lemma Date_gt_counter t:
+ TDM_counter (Default_arbitrate t).(Implementation_State) <= t.
+ Proof.
+ induction t.
+ { by simpl. }
+ { simpl; rewrite /Next_state;
+ destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (c == OZCycle) eqn:Hz,
+ (c == OACT_date) eqn:Hact, (c == OCAS_date) eqn:Hcas, (c == OLastCycle) eqn:Hend; try destruct (Pending_of _ _) eqn:HP; simpl.
+ all: rewrite /TDM_counter in IHt.
+ all: try (rewrite /Next_cycle; set (Hc := c.+1 < SL); dependent destruction Hc).
+ all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
+ all: done.
+ }
+ 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.
+
+ 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.
+
+ Lemma Modulo_time_distance_or t t':
+ TDM_counter (Default_arbitrate t).(Implementation_State) == TDM_counter (Default_arbitrate t').(Implementation_State)
+ -> t' + SL <= t \/ t + SL <= t' \/ t = t'.
+ Proof.
+ intros H.
+ destruct (t' < t) eqn:Hlt.
+ { apply Modulo_time_distance in H.
+ 2: exact Hlt.
+ by left. }
+ rewrite ltnNge in Hlt; apply negbFE in Hlt.
+ rewrite leq_eqVlt in Hlt; move: Hlt => /orP [/eqP Heq | Hlt].
+ { right; by right. }
+ move: H => /eqP H; apply Logic.eq_sym in H; move: H => /eqP H.
+ apply Modulo_time_distance in H.
+ 2: exact Hlt.
+ right; by left.
+ 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 TDM_add_counter (c : Counter_t) t:
+ TDM_counter (Default_arbitrate t).(Implementation_State) == c ->
+ forall (d : nat), c + d < SL ->
+ nat_of_ord (TDM_counter (Default_arbitrate (t + d)).(Implementation_State)) == c + d.
+ Proof.
+ intros Hc d Hbound.
+ induction d.
+ 1: rewrite !addn0; by rewrite nat_of_counter_eq.
+ rewrite addnS in Hbound.
+ apply ltn_trans with (m := c+d) in Hbound as H.
+ 2: done.
+ apply IHd in H as IH; clear IHd.
+ rewrite -Time_counter_modulo.
+ set (HH := Ordinal H : Counter_t); simpl in HH.
+ assert (c + d.+1 = Next_cycle HH).
+ { unfold Next_cycle. set (H0 := HH.+1 < SL).
+ dependent destruction H0.
+ all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
+ 1: by rewrite addnS.
+ contradict x; unfold HH; simpl; apply Bool.not_false_iff_true; by rewrite Hbound.
+ }
+ specialize TDM_next_cycle_modulo with (c := HH) (t := (t + d)) as H1.
+ rewrite H0; rewrite addnS; apply /eqP; apply H1.
+ by rewrite Time_counter_modulo; unfold HH; simpl; apply /eqP.
+ Qed.
+
+ Lemma TDM_nextcycle_act_eq_actS:
+ nat_of_ord (Next_cycle OACT_date) = ACT_date.+1.
+ Proof.
+ unfold Next_cycle.
+ set (Hc := OACT_date.+1 < SL).
+ 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 SL_ACTS.
+ Qed.
+
+ Lemma TDM_nextcycle_cas_eq_casS:
+ nat_of_ord (Next_cycle OCAS_date) = CAS_date.+1.
+ Proof.
+ unfold Next_cycle.
+ set (Hc := OCAS_date.+1 < SL).
+ 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 SL_CASS.
+ Qed.
+
+ Lemma TDM_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, (c == OZCycle), (c == OACT_date) eqn:Ha, (c == OCAS_date) eqn:Hc, (c == OLastCycle);
+ try destruct (Pending_of _ _) eqn:HP.
+ all: intros H; try (rewrite in_cons in H; move: H => /orP [/eqP H | H]).
+ all: (by rewrite H || by apply IHt in H).
+ Qed.
+
+ Lemma Next_cycke_OZ_pl_ACT :
+ Next_cycle OZCycle + OACT_date = Next_cycle OACT_date.
+ Proof.
+ rewrite TDM_nextcycle_act_eq_actS.
+ unfold Next_cycle; set (Hc := OZCycle.+1 < SL); dependent destruction Hc.
+ all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
+ 2: { contradict x; apply Bool.not_false_iff_true; unfold OZCycle; simpl.
+ by rewrite SL_one. }
+ rewrite addnC addn1; reflexivity.
+ Qed.
+
+ Lemma Next_cycke_OZ_pl_CAS :
+ Next_cycle OZCycle + OCAS_date = Next_cycle OCAS_date.
+ Proof.
+ rewrite TDM_nextcycle_cas_eq_casS.
+ unfold Next_cycle; set (Hc := OZCycle.+1 < SL); dependent destruction Hc.
+ all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
+ 2: { contradict x; apply Bool.not_false_iff_true; unfold OZCycle; simpl.
+ by rewrite SL_one. }
+ rewrite addnC addn1; reflexivity.
+ Qed.
+
+ Lemma Next_cycle_OZ_pl_ACT_lt_SL :
+ Next_cycle OZCycle + OACT_date < SL.
+ Proof.
+ unfold Next_cycle; set (Hc := OZCycle.+1 < SL); dependent destruction Hc.
+ all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
+ 2: rewrite add0n; exact SL_ACT.
+ rewrite addnC addn1; exact SL_ACTS.
+ Qed.
+
+ Lemma Next_cycle_OZ_pl_CAS_lt_SL :
+ Next_cycle OZCycle + OCAS_date < SL.
+ Proof.
+ unfold Next_cycle; set (Hc := OZCycle.+1 < SL); dependent destruction Hc.
+ all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e.
+ 2: rewrite add0n; exact SL_CAS.
+ rewrite addnC addn1; exact SL_CASS.
+ Qed.
+
+ (*************************************************************************************************)
+ (** COMMAND TIMING PROOFS ************************************************************************)
+ (*************************************************************************************************)
+
+ Theorem Cmds_T_RCD_ok t a b:
+ a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
+ ACT_to_CAS a b -> Same_Bank a b -> Before a b ->
+ Apart_at_least a b T_RCD.
+ Proof.
+ intros Ha Hb AtC SB aBb; rewrite /Apart_at_least.
+ move : AtC => /andP [Aa Cb].
+ apply ACT_modulo_date in Ha as Ha'.
+ 2: exact Aa. clear Aa.
+ apply CAS_modulo_date in Hb as Hb'.
+ 2: exact Cb. clear Cb.
+ rewrite !Time_counter_modulo in Ha',Hb'.
+ set (d := Next_cycle OCAS_date - Next_cycle OACT_date).
+ assert (Next_cycle OACT_date + d = Next_cycle OCAS_date) as H.
+ { unfold d; rewrite subnKC. reflexivity.
+ rewrite TDM_nextcycle_cas_eq_casS TDM_nextcycle_act_eq_actS /CAS_date.
+ rewrite -addnS; apply nat_ltn_add; done. }
+ apply TDM_add_counter with (d := d) in Ha'. move: Ha' => /eqP Ha'.
+ 2: { unfold d; rewrite subnKC.
+ 1: by rewrite TDM_nextcycle_cas_eq_casS SL_CASS.
+ rewrite TDM_nextcycle_cas_eq_casS TDM_nextcycle_act_eq_actS /CAS_date.
+ rewrite -addnS; apply nat_ltn_add; done. }
+ rewrite H in Ha'. rewrite -Ha' in Hb'.
+ apply Modulo_time_distance_or in Hb' as HH. destruct HH as [H0 | [H1 | H2]].
+ { apply leq_trans with (m := a.(CDate) + T_RCD) in H0. exact H0.
+ rewrite -addnA leq_add2l.
+ assert (T_RCD <= SL).
+ { specialize SL_CASS as HH; unfold CAS_date in HH.
+ rewrite addnS -addn2 in HH.
+ apply leq_trans with (n := (ACT_date + T_RCD).+1 + 2).
+ 2: exact HH.
+ rewrite addn2 -addn3 addnACl. apply leq_addr.
+ }
+ apply nat_leq_addl; done. }
+ { rewrite /Before in aBb; contradict aBb.
+ apply /negP; rewrite -leqNgt.
+ rewrite addnC in H1. rewrite -leq_psubRL in H1.
+ 2: by apply TDM_date_gt_0 in Hb.
+ apply leq_trans with (p := a.(CDate)) in H1.
+ exact H1.
+ rewrite -subnBA.
+ 2: { unfold d. rewrite TDM_nextcycle_act_eq_actS TDM_nextcycle_cas_eq_casS.
+ apply leq_trans with (n := CAS_date.+1).
+ 1: apply leq_subr.
+ apply ltn_trans with (n := CAS_date.+1).
+ 1: apply leqnn.
+ exact SL_CASS. }
+ apply leq_subr. }
+ { rewrite H2 leq_add2l.
+ unfold d; rewrite TDM_nextcycle_act_eq_actS TDM_nextcycle_cas_eq_casS /CAS_date.
+ rewrite subnS predn_sub -pred_Sn leq_subRL.
+ 2: apply leq_addr.
+ by rewrite leq_add2l leqnSn. }
+ 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 PRE_modulo_date in Ha as Ha'.
+ 2: exact iPa. clear iPa.
+ apply ACT_modulo_date in Hb as Hb'.
+ 2: exact iAb. clear iAb.
+ unfold Apart_at_least.
+ rewrite !Time_counter_modulo in Ha',Hb'.
+ apply TDM_add_counter with (d := OACT_date) in Ha' as H.
+ 2: exact Next_cycle_OZ_pl_ACT_lt_SL.
+ specialize Next_cycke_OZ_pl_ACT as H0; rewrite H0 in H.
+ move: H => /eqP H; rewrite -H in Hb'; clear H0.
+ apply Modulo_time_distance_or in Hb'; destruct Hb' as [H0 | [H1 | H2]].
+ { apply leq_trans with (m := a.(CDate) + T_RP) in H0. exact H0.
+ rewrite -addnA leq_add2l; unfold OACT_date; simpl; unfold ACT_date.
+ rewrite -addn1 -addnA; apply leq_addr. }
+ { rewrite /Before in aBb; contradict aBb; apply /negP; rewrite -leqNgt.
+ rewrite addnC -leq_psubRL in H1.
+ 2: by apply TDM_date_gt_0 in Hb.
+ apply leq_trans with (p := a.(CDate)) in H1.
+ 1: exact H1.
+ rewrite -subnBA.
+ 2: by rewrite leq_eqVlt /OACT_date //= SL_ACT orbT.
+ apply leq_subr. }
+ { by rewrite H2 leq_add2l /OACT_date //= /ACT_date. }
+ Qed.
+
+ Theorem Cmds_T_RC_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_RC.
+ 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_RC_SL orbT.
+ Qed.
+
+ Theorem Cmds_T_RAS_ok t a b:
+ a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
+ ACT_to_PRE a b -> Same_Bank a b -> Before a b ->
+ Apart_at_least a b T_RAS.
+ Proof.
+ intros Ha Hb Hty SB aBb; rewrite /Apart_at_least.
+ rewrite /ACT_to_PRE in Hty; move : Hty => /andP [iAa iPb].
+ apply ACT_modulo_date in Ha.
+ 2: exact iAa. clear iAa.
+ apply PRE_modulo_date in Hb.
+ 2: exact iPb. clear iPb.
+ rewrite !Time_counter_modulo in Hb,Ha.
+ apply TDM_add_counter with (d := OACT_date) in Hb.
+ 2: exact Next_cycle_OZ_pl_ACT_lt_SL.
+ specialize Next_cycke_OZ_pl_ACT as H0; rewrite H0 in Hb.
+ move: Hb => /eqP Hb; rewrite -Hb in Ha;
+ move: Ha => /eqP Ha; apply Logic.eq_sym in Ha; move: Ha => /eqP Ha.
+ apply Modulo_time_distance in Ha.
+ 2: { unfold Before in aBb; apply ltn_trans with (p := b.(CDate) + OACT_date) in aBb.
+ 1: exact aBb.
+ apply nat_ltn_add; rewrite /OACT_date //=. }
+ rewrite [b.(CDate) + _]addnC -leq_subLR in Ha.
+ apply leq_trans with (m := a.(CDate) + T_RAS) in Ha.
+ 1: exact Ha.
+ rewrite -addnBA.
+ 2: by rewrite /OACT_date //= leq_eqVlt SL_ACT orbT.
+ rewrite leq_add2l leq_subRL.
+ 2: by rewrite /OACT_date //= leq_eqVlt SL_ACT orbT.
+ by rewrite /OACT_date //= /ACT_date leq_eqVlt T_RAS_SL orbT.
+ Qed.
+
+ Lemma Private_Bank_Separation_at_NZero (ta tb o : nat) :
+ TDM_counter (Default_arbitrate (ta + o)).(Implementation_State) == OZCycle ->
+ TDM_counter (Default_arbitrate (tb + o)).(Implementation_State) ==
+ TDM_counter (Default_arbitrate (ta + o)).(Implementation_State) ->
+ TDM_slot (Default_arbitrate (tb + o)).(Implementation_State) ==
+ TDM_slot (Default_arbitrate (ta + o)).(Implementation_State) ->
+ ta < tb -> ta + (SN * SL) <= tb.
+ Proof.
+ intros Hz Hc Hsl Hlt.
+ rewrite -!nat_of_slot_eq -!Time_slot_modulo eqn_mod_dvd in Hsl.
+ 2: by apply leq_div2r; rewrite leq_add2r leq_eqVlt Hlt orbT.
+ move: Hsl => /dvdnP Hsl; destruct Hsl.
+ rewrite -divnBr in H.
+ 2: {
+ apply Exists_time_multiple in Hz as H; destruct H as [d H].
+ rewrite H dvdn_mull.
+ 1: trivial.
+ by rewrite dvdnn.
+ }
+ move: H => /eqP H; rewrite -eqn_mul in H.
+ 3: {
+ rewrite -nat_of_counter_eq -!Time_counter_modulo eqn_mod_dvd in Hc. exact Hc.
+ by rewrite leq_add2r leq_eqVlt Hlt orbT.
+ }
+ 2: exact SL_pos.
+ rewrite subnDr in H; move: H => /eqP H; rewrite -leq_subRL.
+ 2: by rewrite leq_eqVlt Hlt orbT.
+ rewrite H.
+ destruct x.
+ { rewrite !mul0n in H; contradict Hlt.
+ apply /negP; rewrite -leqNgt.
+ specialize leq_add2r with (m := tb) (n := ta) (p := 0) as HH.
+ by rewrite -HH addn0 -leq_subLR H.
+ }
+ rewrite -mulnA leq_pmull.
+ all: done.
+ Qed.
+
+ Lemma TDM_counter_last t:
+ TDM_counter (Default_arbitrate t).(Implementation_State) == OLastCycle ->
+ TDM_counter (Default_arbitrate t.+1).(Implementation_State) == OZCycle.
+ Proof.
+ simpl; rewrite /Next_state; intros.
+ destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (c == OZCycle), (c == OACT_date),
+ (c == OCAS_date), (c == OLastCycle); try destruct (Pending_of _ _); simpl.
+ all: rewrite /TDM_counter in H.
+ all: move : H => /eqP H; rewrite H; unfold Next_cycle; set (Hc := OLastCycle.+1 < SL).
+ all: dependent destruction Hc.
+ all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; intro; simpl; try reflexivity.
+ all: unfold OLastCycle in x; simpl in x; rewrite prednK in x; try exact SL_pos.
+ all: by rewrite ltnn in x.
+ Qed.
+
+ Lemma TDM_slot_bound t s c:
+ TDM_counter (Default_arbitrate t).(Implementation_State) == c ->
+ TDM_slot (Default_arbitrate t).(Implementation_State) == s ->
+ forall (d : nat), c + d < SL ->
+ TDM_slot (Default_arbitrate (t + d)).(Implementation_State) == s.
+ Proof.
+ intros Hc Hs d Hlt; induction d.
+ { rewrite addn0; exact Hs. }
+ rewrite addnS; simpl; rewrite /Next_state.
+ apply TDM_add_counter with (d := d) in Hc as Hc'.
+ 2: { apply ltn_trans with (m := c + d) in Hlt as Hlt'. exact Hlt'. by rewrite addnS. }
+ destruct (Default_arbitrate (t + d)).(Implementation_State), (c0 == OZCycle), (c0 == OACT_date),
+ (c0 == OCAS_date), (c0 == OLastCycle); try destruct (Pending_of _ _); simpl.
+ all: apply ltn_trans with (m := c + d) in Hlt as Hlt'; try by rewrite addnS.
+ all: rewrite /Next_slot; destruct (c0.+1 < SL) eqn:Hbug.
+ all: try (apply IHd in Hlt' as IH; by rewrite /TDM_slot in IH).
+ all: rewrite /TDM_counter in Hc'; move: Hc' => /eqP Hc'; rewrite Hc' in Hbug.
+ all: rewrite addnS in Hlt; rewrite Hlt in Hbug.
+ all: done.
+ Qed.
+
+ Lemma TDM_counter_same ta tb:
+ TDM_counter (Default_arbitrate ta).(Implementation_State) ==
+ TDM_counter (Default_arbitrate tb).(Implementation_State) ->
+ forall d,
+ TDM_counter (Default_arbitrate (ta + d)).(Implementation_State) ==
+ TDM_counter (Default_arbitrate (tb + d)).(Implementation_State).
+ Proof.
+ intros; induction d.
+ { by rewrite !addn0. }
+ rewrite !addnS; simpl; rewrite /Next_state.
+ destruct (Default_arbitrate (ta + d)).(Implementation_State) eqn:HSa,
+ (Default_arbitrate (tb + d)).(Implementation_State) eqn:HSb.
+ all: rewrite /TDM_counter in IHd; move: IHd => /eqP IH.
+ { destruct (c == OZCycle),(c0 == OZCycle); try destruct (Pending_of _ _); simpl;
+ try destruct (Pending_of s0 r0); simpl.
+ all: rewrite IH; done. }
+ { destruct (c == OZCycle), (c0 == OACT_date),(c0 == OCAS_date), (c0 == OLastCycle);
+ try destruct (Pending_of _ _); simpl.
+ all: rewrite IH; done. }
+ { destruct (c == OACT_date), (c == OCAS_date), (c == OLastCycle), (c0 == OZCycle);
+ try destruct (Pending_of _ _); simpl.
+ all: rewrite IH; done. }
+ { destruct (c == OACT_date), (c == OCAS_date), (c == OLastCycle),
+ (c0 == OACT_date),(c0 == OCAS_date), (c0 == OLastCycle); simpl.
+ all: rewrite IH; done. }
+ Qed.
+
+ Lemma TDM_slot_same ta tb:
+ TDM_counter (Default_arbitrate tb).(Implementation_State) ==
+ TDM_counter (Default_arbitrate ta).(Implementation_State) ->
+ TDM_slot (Default_arbitrate tb).(Implementation_State) ==
+ TDM_slot (Default_arbitrate ta).(Implementation_State) ->
+ forall d,
+ TDM_slot (Default_arbitrate (tb + d)).(Implementation_State) ==
+ TDM_slot (Default_arbitrate (ta + d)).(Implementation_State).
+ Proof.
+ intros Hc Hs d; induction d.
+ 1: by rewrite !addn0.
+ apply TDM_counter_same with (d := d) in Hc as Hc'.
+ rewrite !addnS; simpl; rewrite /Next_state.
+ destruct (Default_arbitrate (ta + d)).(Implementation_State) eqn:HSa,
+ (Default_arbitrate (tb + d)).(Implementation_State) eqn:HSb.
+ all: rewrite /TDM_counter in Hc'; move: Hc' => /eqP Hc'.
+ all: rewrite /TDM_slot in IHd; move: IHd => /eqP IH.
+ { destruct (c == OZCycle),(c0 == OZCycle); try destruct (Pending_of _ _); simpl;
+ try destruct (Pending_of s r); simpl.
+ all: rewrite Hc' IH; done. }
+ { destruct (c == OZCycle), (c0 == OACT_date),(c0 == OCAS_date), (c0 == OLastCycle);
+ try destruct (Pending_of _ _); simpl.
+ all: rewrite Hc' IH; done. }
+ { destruct (c == OACT_date), (c == OCAS_date), (c == OLastCycle), (c0 == OZCycle);
+ try destruct (Pending_of _ _); simpl.
+ all: rewrite Hc' IH; done. }
+ { destruct (c == OACT_date), (c == OCAS_date), (c == OLastCycle),
+ (c0 == OACT_date),(c0 == OCAS_date), (c0 == OLastCycle); simpl.
+ all: rewrite Hc' IH; done. }
+ Qed.
+
+ Theorem Cmds_T_RTP_ok (t : nat) 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_in Hb_in Htype sB aBb; rewrite /Apart_at_least.
+ rewrite /CRD_to_PRE in Htype; move: Htype => /andP [iCa iPb].
+ apply CAS_modulo_date in Ha_in as Ha.
+ 2: by unfold isCRD in iCa; unfold isCAS; rewrite iCa orTb. clear iCa.
+ apply PRE_modulo_date in Hb_in as Hb.
+ 2: exact iPb. clear iPb.
+ rewrite !Time_counter_modulo in Hb,Ha.
+ apply TDM.Private_Mapping in sB.
+
+ set (d := SL.-1 - Next_cycle OCAS_date).
+ set (q := (Next_cycle OCAS_date - Next_cycle OZCycle)).
+ set (s := TDM_slot (Default_arbitrate a.(CDate)).(Implementation_State)); fold s in sB.
+
+ (* (b) slot is still (s) at (b + q) *)
+ apply TDM_slot_bound with (s := s) (d := q) in Hb as Hsb.
+ 3: {
+ unfold q. rewrite subnKC.
+ 2: by rewrite TDM_nextcycle_ozcycle TDM_nextcycle_cas_eq_casS.
+ by rewrite TDM_nextcycle_cas_eq_casS SL_CASS.
+ }
+ 2: by rewrite -nat_of_slot_eq sB.
+
+ (* (b) counter is (Next_cycle OCAS_date) at (b + q) *)
+ apply TDM_add_counter with (d := q) in Hb.
+ 2: {
+ unfold q. rewrite subnKC.
+ by rewrite TDM_nextcycle_cas_eq_casS SL_CASS.
+ by rewrite TDM_nextcycle_ozcycle TDM_nextcycle_cas_eq_casS.
+ }
+ rewrite {2}/q in Hb. rewrite subnKC in Hb.
+ 2: by rewrite TDM_nextcycle_ozcycle TDM_nextcycle_cas_eq_casS.
+
+ unfold s in Hsb.
+ apply TDM_slot_same with (d := d.+1) in Hsb as HSL.
+ 2: {
+ fold q in Hb; move: Hb => /eqP Hb; rewrite -Hb in Ha.
+ move: Ha => /eqP Ha; apply Logic.eq_sym in Ha; move: Ha => /eqP Ha. exact Ha.
+ }
+
+ move: Ha => /eqP Ha; rewrite -Ha in Hb.
+ apply TDM_counter_same with (d := d.+1) in Hb as HCL.
+ apply Private_Bank_Separation_at_NZero in HCL.
+ 4: {
+ unfold Before in aBb; apply ltn_trans with (p := b.(CDate) + q) in aBb. exact aBb.
+ apply nat_ltnn_add; unfold q; rewrite TDM_nextcycle_cas_eq_casS TDM_nextcycle_ozcycle.
+ by rewrite subn1 -pred_Sn CAS_pos. }
+ 3: exact HSL.
+ 2: {
+ move: Ha => /eqP Ha. apply TDM_add_counter with (d := d) in Ha as Ha'.
+ 2: {
+ unfold d. rewrite subnKC. by rewrite ltn_predL SL_pos.
+ by rewrite TDM_nextcycle_cas_eq_casS ltn_predRL SL_CASS.
+ }
+ rewrite {2}/d subnKC in Ha'.
+ 2: by rewrite TDM_nextcycle_cas_eq_casS ltn_predRL SL_CASS.
+ apply TDM_counter_last in Ha'; by rewrite -addnS in Ha'.
+ }
+
+ assert (CAS_date <= SN * SL).
+ { specialize SN_one as H1; specialize SL_CAS as H2.
+ apply ltnW in H1,H2; apply leq_mul with (m1 := 1) (n1 := SN) in H2.
+ rewrite mul1n in H2; exact H2. exact SN_pos.
+ }
+
+ unfold q in HCL; rewrite TDM_nextcycle_cas_eq_casS TDM_nextcycle_ozcycle subn1 -pred_Sn in HCL.
+ rewrite [_ + CAS_date]addnC -leq_subLR in HCL.
+ apply leq_trans with (m := a.(CDate) + T_RTP) in HCL.
+ 1: exact HCL.
+ rewrite -addnBA.
+ 2: exact H.
+ by rewrite leq_add2l leq_eqVlt T_RTP_SN_SL orbT.
+ Qed.
+
+ Theorem Cmds_T_WTP_ok t a b:
+ a \in (Default_arbitrate t).(Arbiter_Commands) -> b \in (Default_arbitrate t).(Arbiter_Commands) ->
+ CWR_to_PRE a b -> Same_Bank a b -> Before a b ->
+ Apart_at_least a b (T_WR + T_WL + T_BURST).
+ Proof.
+ intros Ha_in Hb_in Htype sB aBb; rewrite /Apart_at_least.
+ rewrite /CRD_to_PRE in Htype; move: Htype => /andP [iCa iPb].
+ apply CAS_modulo_date in Ha_in as Ha.
+ 2: by unfold isCWR in iCa; unfold isCAS; rewrite iCa orbT. clear iCa.
+ apply PRE_modulo_date in Hb_in as Hb.
+ 2: exact iPb. clear iPb.
+ rewrite !Time_counter_modulo in Hb,Ha.
+ apply TDM.Private_Mapping in sB.
+
+ set (d := SL.-1 - Next_cycle OCAS_date).
+ set (q := (Next_cycle OCAS_date - Next_cycle OZCycle)).
+ set (s := TDM_slot (Default_arbitrate a.(CDate)).(Implementation_State)); fold s in sB.
+
+ (* (b) slot is still (s) at (b + q) *)
+ apply TDM_slot_bound with (s := s) (d := q) in Hb as Hsb.
+ 3: {
+ unfold q. rewrite subnKC.
+ 2: by rewrite TDM_nextcycle_ozcycle TDM_nextcycle_cas_eq_casS.
+ by rewrite TDM_nextcycle_cas_eq_casS SL_CASS.
+ }
+ 2: by rewrite -nat_of_slot_eq sB.
+
+ (* (b) counter is (Next_cycle OCAS_date) at (b + q) *)
+ apply TDM_add_counter with (d := q) in Hb.
+ 2: {
+ unfold q. rewrite subnKC.
+ by rewrite TDM_nextcycle_cas_eq_casS SL_CASS.
+ by rewrite TDM_nextcycle_ozcycle TDM_nextcycle_cas_eq_casS.
+ }
+ rewrite {2}/q in Hb. rewrite subnKC in Hb.
+ 2: by rewrite TDM_nextcycle_ozcycle TDM_nextcycle_cas_eq_casS.
+
+ unfold s in Hsb.
+ apply TDM_slot_same with (d := d.+1) in Hsb as HSL.
+ 2: {
+ fold q in Hb; move: Hb => /eqP Hb; rewrite -Hb in Ha.
+ move: Ha => /eqP Ha; apply Logic.eq_sym in Ha; move: Ha => /eqP Ha. exact Ha.
+ }
+
+ move: Ha => /eqP Ha; rewrite -Ha in Hb.
+ apply TDM_counter_same with (d := d.+1) in Hb as HCL.
+ apply Private_Bank_Separation_at_NZero in HCL.
+ 4: {
+ unfold Before in aBb; apply ltn_trans with (p := b.(CDate) + q) in aBb. exact aBb.
+ apply nat_ltnn_add; unfold q; rewrite TDM_nextcycle_cas_eq_casS TDM_nextcycle_ozcycle.
+ by rewrite subn1 -pred_Sn CAS_pos. }
+ 3: exact HSL.
+ 2: {
+ move: Ha => /eqP Ha. apply TDM_add_counter with (d := d) in Ha as Ha'.
+ 2: {
+ unfold d. rewrite subnKC. by rewrite ltn_predL SL_pos.
+ by rewrite TDM_nextcycle_cas_eq_casS ltn_predRL SL_CASS.
+ }
+ rewrite {2}/d subnKC in Ha'.
+ 2: by rewrite TDM_nextcycle_cas_eq_casS ltn_predRL SL_CASS.
+ apply TDM_counter_last in Ha'; by rewrite -addnS in Ha'.
+ }
+
+ assert (CAS_date <= SN * SL).
+ { specialize SN_one as H1; specialize SL_CAS as H2.
+ apply ltnW in H1,H2; apply leq_mul with (m1 := 1) (n1 := SN) in H2.
+ rewrite mul1n in H2; exact H2. exact SN_pos.
+ }
+
+ unfold q in HCL; rewrite TDM_nextcycle_cas_eq_casS TDM_nextcycle_ozcycle subn1 -pred_Sn in HCL.
+ rewrite [_ + CAS_date]addnC -leq_subLR in HCL.
+ apply leq_trans with (m := a.(CDate) + (T_WR + T_WL + T_BURST)) in HCL.
+ 1: exact HCL.
+ rewrite -addnBA.
+ 2: exact H.
+ by rewrite leq_add2l leq_eqVlt T_WTP_SN_SL orbT.
+ Qed.
+
+ Theorem Cmds_T_RtoW_ok t a b:
+ a \in (Default_arbitrate t).(Arbiter_Commands) ->
+ b \in (Default_arbitrate t).(Arbiter_Commands) ->
+ CRD_to_CWR a b -> Before a b ->
+ Apart_at_least a b T_RTW.
+ Proof.
+ intros Ha Hb Htype aBb; unfold Apart_at_least.
+ rewrite /CWR_to_PRE in Htype; move: Htype => /andP [iCRa iCWb].
+ apply CAS_modulo_date in Ha.
+ 2: by unfold isCRD in iCRa; unfold isCAS; rewrite iCRa orTb. clear iCRa.
+ apply CAS_modulo_date in Hb.
+ 2: by unfold isCWR in iCWb; unfold isCAS; rewrite iCWb orbT. clear iCWb.
+ rewrite !Time_counter_modulo in Hb,Ha.
+ move: Hb => /eqP Hb; rewrite -Hb in Ha; move: Ha => /eqP Ha; apply Logic.eq_sym in Ha; move: Ha => /eqP Ha.
+ apply Modulo_time_distance in Ha.
+ 2: by unfold Before in aBb.
+ apply leq_trans with (n := a.(CDate) + SL).
+ 2: exact Ha.
+ by rewrite leq_add2l leq_eqVlt T_RTW_SL orbT.
+ Qed.
+
+ Theorem Cmds_T_WtoR_SBG_ok t a b:
+ a \in (Default_arbitrate t).(Arbiter_Commands) ->
+ b \in (Default_arbitrate t).(Arbiter_Commands) ->
+ CWR_to_CRD a b -> Before a b -> Same_Bankgroup a b ->
+ Apart_at_least a b (T_WTR_l + T_WL + T_BURST).
+ Proof.
+ intros Ha Hb Htype aBb sBG; unfold Apart_at_least.
+ rewrite /CWR_to_PRE in Htype; move: Htype => /andP [iA iB].
+ apply CAS_modulo_date in Ha.
+ 2: by unfold isCWR in iA; unfold isCAS; rewrite iA orbT. clear iA.
+ apply CAS_modulo_date in Hb.
+ 2: by unfold isCRD in iB; unfold isCAS; rewrite iB orTb. clear iB.
+ rewrite !Time_counter_modulo in Hb,Ha.
+ move: Hb => /eqP Hb; rewrite -Hb in Ha; move: Ha => /eqP Ha; apply Logic.eq_sym in Ha; move: Ha => /eqP Ha.
+ apply Modulo_time_distance in Ha.
+ 2: by unfold Before in aBb.
+ apply leq_trans with (n := a.(CDate) + SL).
+ 2: exact Ha.
+ by rewrite leq_add2l leq_eqVlt WTR_SL orbT.
+ Qed.
+
+ Theorem Cmds_T_WtoR_DBG_ok t:
+ BANKGROUPS > 1 -> forall (a b : Command_t),
+ a \in (Default_arbitrate t).(Arbiter_Commands) ->
+ b \in (Default_arbitrate t).(Arbiter_Commands) ->
+ CWR_to_CRD a b -> Before a b -> ~~ Same_Bankgroup a b ->
+ Apart_at_least a b (T_WTR_s + T_WL + T_BURST).
+ Proof.
+ intros H. specialize TDM.DDR3 as Hbug. by rewrite Hbug in H.
+ Qed.
+
+ Theorem Cmds_T_CCD_SBG_ok t a b:
+ a \in (Default_arbitrate t).(Arbiter_Commands) ->
+ b \in (Default_arbitrate t).(Arbiter_Commands) ->
+ CRD_to_CRD a b \/ CWR_to_CWR a b -> Before a b -> Same_Bankgroup a b ->
+ Apart_at_least a b T_CCD_l.
+ Proof.
+ intros Ha Hb Htype aBb sBG; unfold Apart_at_least.
+ destruct Htype as [Htype | Htype].
+ 2: unfold CWR_to_CWR in Htype; move: Htype => /andP [iWa iWb].
+ 1: unfold CRD_to_CRD in Htype; move: Htype => /andP [iRa iRb].
+ all: apply CAS_modulo_date in Ha,Hb.
+ 2: by unfold isCAS; unfold isCRD in iRb; rewrite iRb orTb.
+ 2: by unfold isCAS; unfold isCRD in iRa; rewrite iRa orTb.
+ 3: by unfold isCAS; unfold isCWR in iWb; rewrite iWb orbT.
+ 3: by unfold isCAS; unfold isCWR in iWa; rewrite iWa orbT.
+ all: rewrite !Time_counter_modulo in Hb,Ha.
+ all: move: Hb => /eqP Hb; rewrite -Hb in Ha; move: Ha => /eqP Ha; apply Logic.eq_sym in Ha; move: Ha => /eqP Ha.
+ all: apply Modulo_time_distance in Ha.
+ all: try done.
+ all: apply leq_trans with (n := a.(CDate) + SL).
+ all: try exact Ha.
+ all: by rewrite leq_add2l leq_eqVlt T_CCD_SL orbT.
+ Qed.
+
+ Theorem Cmds_T_CCD_DBG_ok t:
+ BANKGROUPS > 1 -> forall a b,
+ a \in (Default_arbitrate t).(Arbiter_Commands) ->
+ b \in (Default_arbitrate t).(Arbiter_Commands) ->
+ CRD_to_CRD a b \/ CWR_to_CWR a b -> Before a b -> ~~ Same_Bankgroup a b ->
+ Apart_at_least a b T_CCD_s.
+ Proof.
+ intros H. specialize TDM.DDR3 as Hbug. by rewrite Hbug in H.
+ 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.
+
+ Theorem Cmds_T_RRD_SBG_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 -> Same_Bankgroup a b ->
+ Apart_at_least a b T_RRD_l.
+ Proof.
+ intros Ha Hb AtA _ aBb sBG.
+ 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.
+
+ Theorem Cmds_T_RRD_DBG_ok t: BANKGROUPS > 1 -> forall 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 -> ~~ Same_Bankgroup a b ->
+ Apart_at_least a b T_RRD_s.
+ Proof.
+ intros H. specialize TDM.DDR3 as Hbug. by rewrite Hbug in H.
+ 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).
+ rewrite -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.
+
+ Lemma TDM_inc_counter t:
+ TDM_counter (Default_arbitrate t).(Implementation_State) < SL.-1 ->
+ nat_of_ord (TDM_counter (Default_arbitrate t.+1).(Implementation_State)) =
+ (nat_of_ord (TDM_counter (Default_arbitrate t).(Implementation_State))).+1.
+ Proof.
+ intros H; simpl; rewrite /Next_state.
+ 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.
+ all: try (rewrite /TDM_counter //= Hs //= Hz HP //= in H).
+ all: unfold Next_cycle; set (Hc := c.+1 < SL); dependent destruction Hc.
+ all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; intro; simpl; clear e; try reflexivity.
+ all: try (by move: Hz => /eqP Hz; rewrite Hz /OZCycle //= SL_one in x).
+ all: try (by rewrite /TDM_counter //= ltn_predRL in H; rewrite H in x).
+ Qed.
+
+ Lemma Counter_is_bounded (c: Counter_t) :
+ (c == OLastCycle) = false -> nat_of_ord c < SL.-1.
+ Proof.
+ intros H.
+ rewrite -nat_of_counter_eq in H.
+ destruct c; simpl in *.
+ rewrite leq_eqVlt in i; move: i => /orP [/eqP i | i].
+ 2: by rewrite ltn_predRL.
+ by rewrite -i -pred_Sn eq_refl in H.
+ Qed.
+
+ Lemma Request_PRE_bounded t ra:
+ TDM_request (Default_arbitrate t).(Implementation_State) == Some ra ->
+ (PRE_of_req ra ((Last_slot_start t).+1)) \in (Default_arbitrate ((Last_slot_start t).+1)).(Arbiter_Commands).
+ Proof.
+ intros Hreq.
+ induction t.
+ { by simpl in Hreq. }
+ rewrite /Last_slot_start; simpl in Hreq; unfold Next_state in Hreq.
+ destruct (Default_arbitrate t).(Implementation_State) eqn:Hs.
+ { destruct (c == OZCycle) eqn:Hc.
+ { destruct (Pending_of _ _) eqn:Hp; simpl in Hreq.
+ 1: inversion Hreq.
+ simpl; rewrite Hs //= Hc Hp //=.
+ rewrite /Next_state.
+ move: Hc => /eqP Hc.
+ assert (nat_of_ord (Next_cycle c) = 1).
+ { unfold Next_cycle; set (HH := c.+1 < SL); dependent destruction HH.
+ all: apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; intro; simpl; clear e.
+ 2: rewrite Hc /OZCycle //= in x; contradict x; by rewrite SL_one.
+ rewrite Hc /OZCycle //=. }
+ move: Hc => /eqP Hc.
+ rewrite H subn1 -pred_Sn Hs Hc Hp //=.
+ rewrite in_cons /PRE_of_req.
+ rewrite inj_eq in Hreq. move: Hreq => /eqP Hreq.
+ 2: exact ssrfun.Some_inj.
+ by rewrite Hreq eq_refl orTb. }
+ by simpl in Hreq. }
+ { destruct (c == OACT_date) eqn:Hact, (c == OCAS_date) eqn:Hcas, (c == OLastCycle) eqn:Hlast; simpl in Hreq.
+ all: rewrite /TDM_request in IHt.
+ all: try done. (* Case where c == OLast_cycle, None == Some *)
+ all: apply IHt in Hreq as IH; clear IHt.
+ all: rewrite /Last_slot_start Hs /TDM_counter in IH.
+ 7: {
+ apply Counter_is_bounded in Hlast.
+ assert (TDM_counter (Default_arbitrate t).(Implementation_State) = c) as Hc; try by rewrite Hs.
+ rewrite -Hc in Hlast; apply TDM_inc_counter in Hlast.
+ rewrite Hlast /TDM_counter Hs subSS. exact IH.
+ }
+ all: assert (c < SL.-1).
+ all: try (move: Hact => /eqP Hact; by rewrite Hact /OACT_date //= ltn_predRL SL_ACTS).
+ all: try (move: Hcas => /eqP Hcas; by rewrite Hcas /OCAS_date //= ltn_predRL SL_CASS).
+ all: assert (TDM_counter (Default_arbitrate t).(Implementation_State) = c) as Hc; try by rewrite Hs.
+ all: try (rewrite -Hc in H; apply TDM_inc_counter in H).
+ all: try (rewrite H /TDM_counter Hs subSS; exact IH).
+ }
+ Qed.
+
+ Definition req_pred (s : Slot_t): pred Request_t :=
+ fun '(x) => x.(Requestor) == s.
+
+ Lemma filter_in p s (r0 : Request_t) l:
+ filter p s = r0 :: l ->
+ r0 \in s.
+ Proof.
+ intros.
+ induction s.
+ { done. }
+ rewrite in_cons.
+ destruct (p a) eqn:Hp.
+ { (* use H *)
+ rewrite /filter Hp in H; move: H => /eqP H.
+ rewrite eqseq_cons in H; move: H => /andP [/eqP Heq H].
+ by rewrite Heq eq_refl orTb. }
+ { (* use IH*)
+ unfold filter in H; rewrite Hp in H.
+ apply IHs in H; by rewrite H orbT. }
+ Qed.
+
+ Lemma Request_ACT_bounded t ra:
+ TDM_request (Default_arbitrate t).(Implementation_State) == Some ra ->
+ let tact := (Last_slot_start t).+1 + ACT_date in
+ (ACT_of_req ra tact) \in (Default_arbitrate tact).(Arbiter_Commands).
+ Proof.
+ intros Hreq; simpl.
+ induction t.
+ { by simpl in Hreq. }
+ unfold Last_slot_start in *; simpl in *.
+ destruct (Default_arbitrate t).(Implementation_State) eqn:Hs; simpl in *.
+ { destruct (c == OZCycle) eqn:Hz; try destruct (Pending_of _ _) eqn:HP; simpl in *.
+ all: try inversion Hreq; clear IHt.
+ move: Hz => /eqP Hz; rewrite Hz.
+ rewrite TDM_nextcycle_ozcycle subn1 -pred_Sn /ACT_of_req; clear H0.
+ assert (TDM_counter (Default_arbitrate t).(Implementation_State) == OZCycle) as Hcounter.
+ { by rewrite /TDM_counter Hs Hz. }
+ apply seq_filter_eq_cons_p in HP as HP'; move: HP' => /eqP HP'.
+ apply Request_starts with (ta := t) (ra := r0) in Hcounter.
+ 4: by rewrite /TDM_pending Hs //= HP' HP index_head.
+ 3: apply filter_in in HP; rewrite /TDM_pending Hs; exact HP.
+ 2: by rewrite /TDM_slot Hs HP'.
+ move: Hcounter => /andP [Hc' Hreq'].
+ specialize Request_running_in_slot with (ta := t.+1) (ra := r0) as H.
+ apply H with (d := ACT_date.-1) in Hreq' as HH. clear H.
+ 3: { rewrite -!subn1. apply ltn_sub2r. exact SL_one. exact SL_ACT. }
+ 2: exact Hc'.
+ move: HH => /andP [Hc'' Hreq''].
+ assert (t.+1 + ACT_date.-1 = t + ACT_date) as Haux.
+ { rewrite -addn1 -addnA [1 + ACT_date.-1]addnC addn1 prednK. reflexivity. exact ACT_pos. }
+ rewrite Haux in Hc'', Hreq''; rewrite prednK in Hc''.
+ 2: exact ACT_pos.
+ rewrite /Next_state.
+ destruct (Default_arbitrate (t + ACT_date)).(Implementation_State) eqn:Hss.
+ 1: discriminate Hreq''.
+ rewrite /TDM_counter in Hc''.
+ rewrite -nat_of_counter_eq /OACT_date //= Hc'' //=.
+ assert ((t + ACT_date)%Nrec.+1 = t.+1 + ACT_date).
+ { rewrite -[t.+1]addn1. rewrite -addnA [1 + ACT_date]addnC addnA addn1. reflexivity. }
+ rewrite H.
+ rewrite /TDM_request in Hreq''; move: Hreq'' => /eqP Hreq''; rewrite -Hreq'' inj_eq in Hreq.
+ 2: exact ssrfun.Some_inj.
+ move: Hreq => /eqP Hreq;
+ by rewrite Hreq in_cons eq_refl orTb. }
+ { destruct (c == OACT_date) eqn:Hact, (c == OCAS_date) eqn:Hcas, (c == OLastCycle) eqn:Hlast; simpl in *.
+ all: try inversion Hreq; clear H0.
+ all: apply IHt in Hreq as IH; clear IHt.
+ all: rewrite -{1}addn1 -addnA [1 + ACT_date]addnC addn1 addnS.
+ all: assert ((t.+1 - Next_cycle c + ACT_date)%Nrec = (t.+1 - Next_cycle c + ACT_date)) as H0; try reflexivity.
+ all: assert ((t.+1 - Next_cycle c + ACT_date) = (t - c + ACT_date)).
+ all: try(
+ unfold Next_cycle; set (Hc := c.+1 < SL); dependent destruction Hc;
+ apply Logic.eq_sym in x; move : Logic.eq_refl; rewrite {2 3} x; simpl; intro; clear e
+ ).
+ all: try by (rewrite subSS; reflexivity).
+ all: try by (move: Hact => /eqP Hact; rewrite Hact /OACT_date //= SL_ACTS in x).
+ all: try (by move: Hcas => /eqP Hcas; rewrite Hcas /OCAS_date //= SL_CASS in x).
+ all: try (by apply Counter_is_bounded in Hlast; rewrite ltn_predRL in Hlast; rewrite Hlast in x).
+ all: rewrite H0 H.
+ all: assert (((t - c).+1 + ACT_date) = (t - c + ACT_date).+1); try by rewrite -addn1 -addnA [1 + ACT_date]addnC addn1 addnS.
+ all: rewrite H1 in IH.
+ all: exact IH.
+ }
+ Qed.
+
+ Lemma TDM_ACT_date cmd t:
+ cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isACT cmd ->
+ TDM_counter (Default_arbitrate cmd.(CDate)).(Implementation_State) == Next_cycle OACT_date /\
+ TDM_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 (c == OZCycle) eqn:Hz; try destruct (Pending_of _ _) eqn:HP; simpl in *.
+ all: rewrite in_cons in Hi; move: Hi => /orP [/eqP H | H]; try by rewrite H in Hp.
+ all: apply IHt in H; try (exact Hp || exact H). }
+ { destruct (c == OACT_date) eqn:Hact, (c == OCAS_date) eqn:Hcas, (c == OLastCycle) eqn:Hend; simpl in *.
+ all: rewrite in_cons in Hi; move: Hi => /orP [/eqP H | H]; try by rewrite H in Hp.
+ all: try (rewrite H //= /TDM_counter !Hs //= Hact //=; move: Hact => /eqP Hact; by rewrite Hact).
+ all: try apply IHt in H; try exact Hp; try exact H.
+ all: rewrite H /isACT /Kind_of_req //= in Hp; contradict Hp; by case r0.(Kind). }
+ Qed.
+
+ Lemma TDM_CAS_date cmd t:
+ cmd \in (Default_arbitrate t).(Arbiter_Commands) -> isCAS cmd ->
+ TDM_counter (Default_arbitrate cmd.(CDate)).(Implementation_State) == Next_cycle OCAS_date /\
+ TDM_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 (c == OZCycle) eqn:Hz; try destruct (Pending_of _ _) eqn:HP; simpl in *.
+ all: rewrite in_cons in Hi; move: Hi => /orP [/eqP H | H]; try by rewrite H in Hp.
+ all: apply IHt in H; try (exact Hp || exact H). }
+ { destruct (c == OACT_date) eqn:Hact, (c == OCAS_date) eqn:Hcas, (c == OLastCycle) eqn:Hend; simpl in *.
+ all: rewrite in_cons in Hi; move: Hi => /orP [/eqP H | H]; try by rewrite H in Hp.
+ (* all: try (rewrite H //= /TDM_counter !Hs //= Hact //=; move: Hact => /eqP Hact; by rewrite Hact). *)
+ all: try apply IHt in H; try exact Hp; try exact H.
+ all: rewrite H //= Hs //= Hact Hcas //=.
+ all: move: Hcas => /eqP Hcas; by rewrite Hcas !eq_refl. }
+ Qed.
+
+ Lemma TDM_SL_gt_nc_act_p1 :
+ Next_cycle OACT_date +1 < SL.
+ Proof.
+ rewrite TDM_nextcycle_act_eq_actS.
+ apply ltn_trans with (n := CAS_date.+1).
+ 2: exact SL_CASS.
+ rewrite ltnS /CAS_date addn1 -[ACT_date.+1]addn1 addnC -ltn_subRL subn1 addnS-pred_Sn.
+ apply nat_ltn_add; by rewrite lt0n T_RCD_pos.
+ Qed.
+
+ Theorem Cmds_ACT_ok t a b:
+ 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 && After c a && Before c b.
+ Proof.
+ intros Ha Hb iA iAb SB aBb.
+ (* info about b's counter *)
+ apply ACT_modulo_date in Hb as Hb'. rewrite Time_counter_modulo in Hb'.
+ 2: done.
+
+ (* other info *)
+ apply TDM_ACT_date in Hb as H. destruct H as [Hc_b Hreq_b].
+ 2: exact iAb.
+ apply TDM_add_counter with (d := 1) in Hc_b as Hc_b'.
+ 2: exact TDM_SL_gt_nc_act_p1.
+ rewrite !addn1 in Hc_b'; move: Hc_b' => /eqP Hc_b'.
+
+ (* get the PRE *)
+ apply Request_PRE_bounded in Hreq_b.
+ move: Hc_b => /eqP Hc_b. rewrite /Last_slot_start Hc_b in Hreq_b.
+ exists (PRE_of_req b.(Request) (b.(CDate) - Next_cycle OACT_date).+1).
+ rewrite /Same_Bank in SB; move: SB => /eqP SB.
+ rewrite /isPRE /Same_Bank //= eq_refl andbT SB eq_refl andbT andbT /Before /After //=.
+ clear SB.
+
+ (* solve Before c b*)
+ apply /andP; split.
+ 2: {
+ rewrite -subSn.
+ 2: specialize Date_gt_counter with (t := b.(CDate)) as HH; rewrite Hc_b in HH; exact HH.
+ rewrite ltn_subLR.
+ 2: specialize Date_gt_counter with (t := b.(CDate).+1) as HH; rewrite Hc_b' in HH; by rewrite leq_eqVlt HH orbT.
+ rewrite -ltn_predRL addnC nat_add_pred; apply nat_ltn_add.
+ by rewrite TDM_nextcycle_act_eq_actS -pred_Sn /ACT_date.
+ }
+
+ (* solve ~~ Before_at a c, i.e., After c a *)
+ apply /andP; split; clear Hb'.
+ 2: {
+ destruct iA as [iAa | iCa].
+ { apply ACT_modulo_date in Ha as Hc_a. rewrite Time_counter_modulo in Hc_a.
+ 2: exact iAa.
+ apply TDM_add_counter with (d := 1) in Hc_a as Hc_a'. rewrite !addn1 in Hc_a'.
+ 2: exact TDM_SL_gt_nc_act_p1.
+ specialize Modulo_time_distance with (t' := a.(CDate).+1) (t := b.(CDate).+1) as Heq.
+ rewrite -Hc_b' in Hc_a'. rewrite nat_of_counter_eq in Hc_a'.
+ move: Hc_a' => /eqP Hc_a'; apply Logic.eq_sym in Hc_a'; move: Hc_a' => /eqP Hc_a'.
+ apply Heq in Hc_a'.
+ 2: by unfold Before in aBb.
+ clear Heq; rename Hc_a' into Hlt.
+ rewrite leq_eqVlt in Hlt; move: Hlt => /orP [/eqP H0 | H1].
+ { assert (b.(CDate) = a.(CDate) + SL).
+ { rewrite -addn1 addnACl addnC addn1 in H0; apply eq_add_S in H0; by rewrite -H0 addnC. }
+ clear H0; rename H into H0.
+ rewrite H0 TDM_nextcycle_act_eq_actS ltnS -addnBA.
+ 2: exact SL_ACT.
+ by rewrite leq_addr. }
+ { apply ltn_trans with (n := b.(CDate) - SL);
+ assert (a.(CDate) + SL < b.(CDate)).
+ 1,3: rewrite -[a.(CDate).+1]addn1 -[b.(CDate).+1]addn1 addnC in H1;
+ rewrite addnA in H1; rewrite ltn_add2r addnC in H1; exact H1.
+ all: clear H1.
+ 1 : rewrite ltn_subRL addnC; exact H.
+ rewrite TDM_nextcycle_act_eq_actS subnSK.
+ 2: {
+ specialize Date_gt_counter with (t := b.(CDate)) as H0; rewrite Hc_b in H0.
+ rewrite TDM_nextcycle_act_eq_actS in H0. exact H0.
+ }
+ apply ltn_sub2l.
+ 2: exact SL_ACT.
+ 1: specialize Date_gt_counter with (t := b.(CDate)) as H0; rewrite Hc_b in H0;
+ rewrite TDM_nextcycle_act_eq_actS in H0; exact H0. }}
+ { apply CAS_modulo_date in Ha. rewrite Time_counter_modulo in Ha.
+ 2: exact iCa.
+
+ set (d := Next_cycle OCAS_date - Next_cycle OACT_date); move: Hc_b => /eqP Hc_b.
+ apply TDM_add_counter with (d := d) in Hc_b as Hc_b''.
+ 2: {
+ unfold d; rewrite subnKC.
+ 1: by rewrite TDM_nextcycle_cas_eq_casS SL_CASS.
+ rewrite TDM_nextcycle_cas_eq_casS TDM_nextcycle_act_eq_actS /CAS_date.
+ rewrite -addnS; by apply nat_ltn_add.
+ }
+
+ assert (Next_cycle OACT_date + d = Next_cycle OCAS_date).
+ { unfold d; rewrite subnKC. reflexivity.
+ rewrite TDM_nextcycle_cas_eq_casS TDM_nextcycle_act_eq_actS /CAS_date /ACT_date -addnS.
+ by apply nat_ltn_add.
+ }
+ move: Hc_b'' => /eqP Hc_b''; rewrite H in Hc_b''; rewrite -Hc_b'' in Ha.
+
+ specialize Modulo_time_distance with (t' := a.(CDate)) (t := b.(CDate) + d) as HH.
+ move: Ha => /eqP Ha; apply Logic.eq_sym in Ha; move: Ha => /eqP Ha.
+ apply HH in Ha; clear HH.
+ 2: {
+ unfold Before in aBb. apply ltn_trans with (p := b.(CDate) + d) in aBb. exact aBb.
+ apply nat_ltn_add; unfold d;
+ rewrite subn_gt0 TDM_nextcycle_cas_eq_casS TDM_nextcycle_act_eq_actS
+ -[ACT_date.+1]addn1 -[CAS_date.+1]addn1 ltn_add2r /CAS_date.
+ by apply nat_ltn_add.
+ }
+
+ rewrite TDM_nextcycle_act_eq_actS subnSK; move: Hc_b => /eqP Hc_b.
+ 2: {
+ specialize Date_gt_counter with (t := b.(CDate)) as H0; rewrite Hc_b in H0.
+ rewrite TDM_nextcycle_act_eq_actS in H0. exact H0.
+ }
+
+ assert ((a.(CDate) < b.(CDate) - ACT_date) == (a.(CDate) + SL < b.(CDate) - ACT_date + SL)) as H0.
+ { apply /eqP; by rewrite ltn_add2r. }
+
+ move: H0 => /eqP H0; rewrite H0; clear H0; rename Ha into Hlt.
+ rewrite leq_eqVlt in Hlt; move: Hlt => /orP [/eqP Hlt | Hlt].
+ { rewrite Hlt addnBAC.
+ 2: {
+ specialize Date_gt_counter with (t := b.(CDate)) as HH;
+ rewrite Hc_b TDM_nextcycle_act_eq_actS in HH;
+ by rewrite leq_eqVlt HH orbT.
+ }
+ rewrite -addnBA.
+ 2: by rewrite leq_eqVlt SL_ACT orbT.
+ rewrite ltn_add2l /d TDM_nextcycle_cas_eq_casS TDM_nextcycle_act_eq_actS ltn_subRL subSS subnKC.
+ 2: by rewrite /CAS_date ltn_addr.
+ exact SL_CAS. }
+ { apply ltn_trans with (n := b.(CDate) + d). exact Hlt.
+ rewrite addnBAC.
+ 2: {
+ specialize Date_gt_counter with (t := b.(CDate)) as HH;
+ rewrite Hc_b TDM_nextcycle_act_eq_actS in HH;
+ by rewrite leq_eqVlt HH orbT.
+ }
+ rewrite -addnBA.
+ 2: by rewrite leq_eqVlt SL_ACT orbT.
+ rewrite ltn_add2l /d TDM_nextcycle_cas_eq_casS TDM_nextcycle_act_eq_actS ltn_subRL subSS subnKC.
+ 2: by rewrite /CAS_date ltn_addr.
+ exact SL_CAS. }
+ }
+ }
+ apply TDM_in_the_past with (t := b.(CDate)).
+ { by apply Cmd_in_trace. }
+ apply TDM_in_the_past with (t := (b.(CDate) - Next_cycle OACT_date).+1).
+ { rewrite TDM_nextcycle_act_eq_actS -addn1 -subnA. by rewrite leq_subr.
+ 1: done.
+ specialize Date_gt_counter with (t := b.(CDate)) as HH; rewrite Hc_b TDM_nextcycle_act_eq_actS in HH; exact HH.
+ }
+ exact Hreq_b.
+ Qed.
+
+ Theorem Cmds_row_ok t b c:
+ b \in (Default_arbitrate t).(Arbiter_Commands) -> c \in (Default_arbitrate t).(Arbiter_Commands) ->
+ isCAS b -> isPRE c -> Same_Bank b c -> Before c b ->
+ exists a, (a \in (Default_arbitrate t).(Arbiter_Commands))
+ && isACT a && Same_Row a b && After a c && Before a b.
+ Proof.
+ intros Hb Hc iCb iPc SB cBb.
+
+ apply TDM_CAS_date in Hb as H. destruct H as [Hc_b Hreq_b].
+ 2: exact iCb.
+
+ apply Request_ACT_bounded in Hreq_b.
+ move: Hc_b => /eqP Hc_b; rewrite /Last_slot_start Hc_b in Hreq_b.
+
+ rewrite TDM_nextcycle_cas_eq_casS subnSK in Hreq_b.
+ 2: specialize Date_gt_counter with (t := b.(CDate)) as HH; by rewrite Hc_b TDM_nextcycle_cas_eq_casS in HH.
+
+ exists (ACT_of_req b.(Request) (b.(CDate) - CAS_date + ACT_date)).
+ rewrite /Same_Bank in SB; move: SB => /eqP SB.
+ rewrite /isACT //= eq_refl andbT /Before /After //= /Same_Row eq_refl //= andbT.
+
+ apply /andP; split.
+ 2: {
+ rewrite -subnA.
+ 3: {
+ specialize Date_gt_counter with (t := b.(CDate)) as H.
+ rewrite Hc_b TDM_nextcycle_cas_eq_casS in H.
+ by rewrite leq_eqVlt H orbT. }
+ 2: by rewrite /CAS_date leq_addr.
+ rewrite ltn_subrL subn_gt0 /CAS_date.
+ apply TDM_date_gt_0 in Hb; rewrite Hb andbT.
+ by apply nat_ltn_add.
+ }
+
+ apply /andP; split.
+ 2: {
+ apply PRE_modulo_date in Hc as Hc_c. rewrite Time_counter_modulo in Hc_c.
+ 2: exact iPc.
+ apply TDM_add_counter with (d := CAS_date) in Hc_c as Hc_c'.
+ 2: by rewrite addnC TDM_nextcycle_ozcycle addn1 SL_CASS.
+ rewrite TDM_nextcycle_ozcycle [1 + _]addnC addn1 in Hc_c'.
+ (* this should be optimzed *)
+ move: Hc_b => /eqP Hc_b; rewrite -nat_of_counter_eq TDM_nextcycle_cas_eq_casS in Hc_b.
+ move: Hc_b => /eqP Hc_b; rewrite -Hc_b in Hc_c'.
+ move: Hc_c' => /eqP Hc_c'; apply Logic.eq_sym in Hc_c'; move: Hc_c' => /eqP Hc_c'.
+ apply Modulo_time_distance_or in Hc_c'; destruct Hc_c' as [Hc_c' | [Hc_c' | Hc_c']].
+ 3: {
+ rewrite Hc_c' -subnA.
+ 3: by rewrite addnC leq_addr.
+ 2: by rewrite /CAS_date leq_addr.
+ by rewrite ltn_subRL addnC ltn_add2l ltn_subrL ACT_pos CAS_pos.
+ }
+ 2: {
+ contradict Hc_c'; apply /negP; rewrite -ltnNge; unfold Before in cBb.
+ rewrite addnC -ltn_subRL.
+ apply ltn_trans with (n := b.(CDate)). exact cBb.
+ by rewrite ltn_subRL addnC ltn_add2l SL_CAS.
+ }
+ rewrite leq_eqVlt in Hc_c'; move: Hc_c' => /orP [/eqP Hc_c' | Hc_c'].
+ { rewrite -Hc_c' -addnA -subnA.
+ 3: by rewrite addnC -addnA leq_addr.
+ 2: by rewrite /CAS_date leq_addr.
+ rewrite leq_subRL.
+ 2: by rewrite leq_subLR addnA addnC -addnA leq_addr.
+ rewrite addnC -addn1 -addnA leq_add2l addnC addn1 ltn_subLR.
+ 2: by rewrite /CAS_date leq_addr.
+ rewrite addnC -addnA.
+ apply nat_ltn_add.
+ by rewrite addn_gt0 SL_pos orTb. }
+ { rewrite -subnA.
+ 3: by specialize Date_gt_counter with (t := b.(CDate)) as H; rewrite Hc_b in H; rewrite leq_eqVlt H orbT.
+ 2: by rewrite /CAS_date leq_addr.
+ rewrite ltn_subRL addnC.
+ apply ltn_trans with (m := c.(CDate) + (CAS_date - ACT_date)) in Hc_c'.
+ exact Hc_c'.
+ rewrite -addnA ltn_add2l ltn_subLR.
+ 2: by rewrite /CAS_date leq_addr.
+ rewrite addnA addnC [ACT_date + _]addnC [SL + _]addnC -addnA.
+ apply nat_ltn_add; by rewrite addn_gt0 SL_pos orbT.
+ }
+ }
+
+ apply TDM_in_the_past with (t := b.(CDate)).
+ { by apply Cmd_in_trace. }
+ apply TDM_in_the_past with (t := (b.(CDate) - CAS_date + ACT_date)).
+ { rewrite -subnA.
+ 3: {
+ move: Hc_b => /eqP Hc_b; rewrite -nat_of_counter_eq TDM_nextcycle_cas_eq_casS in Hc_b; move: Hc_b => /eqP Hc_b.
+ by specialize Date_gt_counter with (t := b.(CDate)) as H; rewrite Hc_b in H; rewrite leq_eqVlt H orbT.
+ }
+ 2: by rewrite /CAS_date leq_addr.
+ by rewrite leq_subr.
+ }
+ exact Hreq_b.
+ Qed.
+
+ Lemma Default_arbitrate_notin_cmd t (c : Command_t):
+ c.(CDate) > t -> c \notin (Default_arbitrate t).(Arbiter_Commands).
+ Proof.
+ intros.
+ destruct (c \notin (Default_arbitrate t).(Arbiter_Commands)) eqn:Hni.
+ { done. }
+ { move : Hni => /negPn Hni. apply Cmd_in_trace in Hni.
+ contradict Hni; apply /negP; by rewrite -ltnNge. }
+ Qed.
+
+ Lemma Default_arbitrate_cmds_uniq t:
+ uniq ((Default_arbitrate t).(Arbiter_Commands)).
+ Proof.
+ induction t; simpl.
+ { done. }
+ rewrite /Next_state //=.
+ destruct (Default_arbitrate t).(Implementation_State) eqn:Hs, (c == OZCycle), (c == OACT_date),
+ (c == OCAS_date), (c == OLastCycle); try destruct (Pending_of _ _); simpl.
+ all: rewrite IHt andbT.
+ all: assert (t < t.+1) as H0; try trivial.
+ all: try (specialize Default_arbitrate_notin_cmd with (c := mkCmd t.+1 NOP nullreq) (t := t) as H; simpl in H;
+ apply H in H0; by rewrite H0).
+ all: try (specialize Default_arbitrate_notin_cmd with (c := mkCmd t.+1 PRE r0) (t := t) as H; simpl in H;
+ apply H in H0; by rewrite H0).
+ all: try (specialize Default_arbitrate_notin_cmd with (c := mkCmd t.+1 ACT r0) (t := t) as H; simpl in H;
+ apply H in H0; by rewrite H0).
+ all: try (specialize Default_arbitrate_notin_cmd with (c := mkCmd t.+1 (Kind_of_req r0) r0) (t := t) as H; simpl in H;
+ apply H in H0; by rewrite H0).
+ Qed.
+
+ Lemma Default_arbitrate_cmds_date t cmd:
+ cmd \in (Default_arbitrate t).(Arbiter_Commands) ->
+ cmd.(CDate) <= (Default_arbitrate t).(Arbiter_Time).
+ Proof.
+ rewrite Default_arbitrate_time; apply Cmd_in_trace.
+ Qed.
+
+ (* Define the arbitration function which creates the actual trace -- used to instantiate the arbiter *)
+ Program Definition TDM_arbitrate (t : nat) :=
+ mkTrace
+ (Default_arbitrate t).(Arbiter_Commands)
+ (Default_arbitrate t).(Arbiter_Time)
+ (Default_arbitrate_cmds_uniq t)
+ (Default_arbitrate_cmds_date t)
+ (Cmds_T_RCD_ok t)
+ (Cmds_T_RP_ok t)
+ (Cmds_T_RC_ok t)
+ (Cmds_T_RAS_ok t)
+ (Cmds_T_RTP_ok t)
+ (Cmds_T_WTP_ok t)
+ (Cmds_T_RtoW_ok t)
+ (Cmds_T_WtoR_SBG_ok t)
+ (Cmds_T_WtoR_DBG_ok t)
+ (Cmds_T_CCD_SBG_ok t)
+ (Cmds_T_CCD_DBG_ok t)
+ (Cmds_T_FAW_ok t)
+ (Cmds_T_RRD_SBG_ok t)
+ (Cmds_T_RRD_DBG_ok t)
+ (Cmds_ACT_ok t)
+ (Cmds_row_ok t).
+
+ Global Instance TDM_arbiter : Arbiter_t :=
+ mkArbiter AF TDM_arbitrate Requests_handled Default_arbitrate_time_match.
+End TDMPROOFS.
diff --git a/framework/DRAM/_CoqProject b/framework/DRAM/_CoqProject
index 77ada9de5ff680d8a7265665d7939cec5916ddd7..30445672a4b92c0e65d4e63324c2eb830164b6dd 100644
--- a/framework/DRAM/_CoqProject
+++ b/framework/DRAM/_CoqProject
@@ -13,6 +13,7 @@ Core/BankMachine.v
Core/InterfaceSubLayer.v
Implementations/TS/FIFO/FIFO.v
+Implementations/TS/TDM/TDM.v
Implementations/BM/FIFOimpSL/FIFOimpSL.v
Implementations/BM/RRimpSL/RRimpSL.v