From 23b6f0413868fc877490b3c4295635ff5ed20f6b Mon Sep 17 00:00:00 2001
From: Florian Brandner <florian.brandner@telecom-paris.fr>
Date: Sun, 16 May 2021 12:25:28 +0200
Subject: [PATCH] entirely rework proofs for FIFO
* less direct proofs
* instead use general properties of the FIFO implementation
---
coq/FIFO.v | 673 ++++++++++++++++++++++++++++++++-----------------
coq/Requests.v | 16 ++
2 files changed, 453 insertions(+), 236 deletions(-)
diff --git a/coq/FIFO.v b/coq/FIFO.v
index 18d4d2e..a7f2b0d 100644
--- a/coq/FIFO.v
+++ b/coq/FIFO.v
@@ -14,11 +14,9 @@ Section FIFO.
FIFO_wait : nat;
(* have to issue at least 3 commands *)
- FIFO_cmds : 3 < FIFO_wait;
- (* have to respect T_RC *)
+ (* have to respect T_RC, T_RAS, T_RP *)
FIFO_T_RC : T_RC < FIFO_wait;
- FIFO_T_RAS : 1 + T_RP + T_RAS < FIFO_wait;
- FIFO_T_RAS' : T_RAS < FIFO_wait;
+ FIFO_T_RAS : T_RAS + (1 + T_RP) < FIFO_wait;
FIFO_T_PRE : FIFO_PRE_date <= FIFO_wait;
FIFO_T_ACT : FIFO_ACT_date <= FIFO_wait;
@@ -33,8 +31,11 @@ Section FIFO.
Time : nat;
}.
+ Local Definition FIFO_next_time req State :=
+ maxn State.(Time) req.(Date).
+
Local Definition FIFO_req req State : FIFO_state_t :=
- let time := maxn State.(Time) req.(Date) in
+ let time := FIFO_next_time req State in
let PRE_date := time + FIFO_PRE_date in
let ACT_date := time + FIFO_ACT_date in
let CMD_date := time + FIFO_CMD_date in
@@ -50,60 +51,270 @@ Section FIFO.
| req::Reqs' => FIFO_req req (FIFO_trace Reqs')
end.
+ Local Fixpoint FIFO_Req_before (req' req : Request_t) Reqs :=
+ match Reqs with
+ | [::] => false
+ | x::Reqs' => if req == x then true
+ else if req' == x then false
+ else FIFO_Req_before req' req Reqs'
+ end.
+
+ Local Fixpoint FIFO_Reqs_before (req : Request_t) Reqs :=
+ if req \notin Reqs then Reqs
+ else
+ match Reqs with
+ | [::] => [::]
+ | req'::Reqs' => if (req' == req) then Reqs'
+ else FIFO_Reqs_before req Reqs'
+ end.
+
+ Local Definition FIFO_trace_base_date req Reqs :=
+ FIFO_next_time req (FIFO_trace (FIFO_Reqs_before req Reqs)).
+
Ltac decompose_FIFO_cmds H suffix :=
let cmd := fresh suffix in
move : H => /orP [ /eqP cmd | /orP [ /eqP cmd | /orP [ /eqP cmd | H]] ].
- Lemma lt_FIFO_wait n: n < 3 -> n < FIFO_wait.
+ Lemma FIFO_Req_before_in o req' req Reqs:
+ uniq (o::Reqs) -> req \in Reqs -> req' \in Reqs ->
+ (FIFO_Req_before req' req (o::Reqs)) = (FIFO_Req_before req' req Reqs).
Proof.
- specialize FIFO_cmds as H.
- intros.
- by apply ltn_trans with (m := n) in H.
+ intros Hu Ir Ir'.
+ decompose_Reqs_uniq Hu Nio.
+ simpl. destruct (req == o) eqn:Heq, (req' == o) eqn:Heq';
+ move : Heq Heq' => /eqP Heq /eqP Heq'; subst; auto;
+ contradict Nio; by (rewrite Ir + rewrite Ir').
Qed.
- Lemma FIFO_T_RP : T_RP < FIFO_wait.
+ Lemma FIFO_Reqs_before_head req Reqs:
+ FIFO_Reqs_before req (req::Reqs) = Reqs.
Proof.
- specialize FIFO_T_ACT as H.
- unfold FIFO_ACT_date in H.
- rewrite addn1 in H.
- apply ltn_trans with (n := FIFO_PRE_date + T_RP).
- - rewrite addnC. by apply nat_ltnn_add.
- - done.
+ simpl. by rewrite eq_refl mem_head.
Qed.
- Lemma FIFO_T_RCD : T_RCD < FIFO_wait.
+ Lemma FIFO_trace_base_date_head req Reqs:
+ req \notin Reqs ->
+ FIFO_trace_base_date req (req::Reqs) = FIFO_next_time req (FIFO_trace Reqs).
Proof.
- specialize FIFO_T_CMD as H.
- unfold FIFO_CMD_date in H.
- rewrite addn1 in H.
- apply ltn_trans with (n := FIFO_ACT_date + T_RCD).
- - rewrite addnC. by apply nat_ltnn_add.
- - done.
+ intros Ni.
+ by rewrite /FIFO_trace_base_date FIFO_Reqs_before_head.
Qed.
- Lemma FIFO_trace_time_monotone req Reqs:
- (FIFO_trace Reqs).(Time) < (FIFO_trace (req::Reqs)).(Time).
+ Lemma FIFO_Reqs_before_in req' req Reqs:
+ req \notin Reqs -> req' \in Reqs ->
+ FIFO_Reqs_before req' (req::Reqs) = FIFO_Reqs_before req' Reqs.
Proof.
- simpl.
- specialize FIFO_cmds as H.
- apply ltn_trans with (m := 0) in H.
- - by move : H => /nat_ltmaxn_l_add H.
- - auto.
+ intros Ni Ir.
+ simpl. rewrite in_cons Ir Bool.orb_true_r. simpl.
+ destruct (req == req') eqn:Heq;
+ move : Heq => /eqP Heq; auto.
+ contradict Ni. subst. by rewrite Ir.
+ Qed.
+
+ Lemma FIFO_trace_base_date_in req' req Reqs:
+ req \notin Reqs -> req' \in Reqs ->
+ FIFO_trace_base_date req' (req::Reqs) = FIFO_trace_base_date req' Reqs.
+ Proof.
+ intros Ni Ir'.
+ by rewrite /FIFO_trace_base_date FIFO_Reqs_before_in.
+ Qed.
+
+ Lemma FIFO_trace_Req_Before_date x y req Reqs:
+ Reqs_sorted_ok Reqs -> uniq Reqs -> req \in Reqs -> x < y + FIFO_wait ->
+ req.(Date) + x < (FIFO_trace Reqs).(Time) + y.
+ Proof.
+ induction Reqs; auto.
+ intros Hs Hu Ir Hltw.
+ simpl. unfold FIFO_next_time.
+ decompose_Reqs_in Ir Heq; subst; auto.
+ - unfold maxn.
+ destruct ((FIFO_trace Reqs).(Time) < a.(Date)) eqn:Hlt.
+ - by rewrite addnCAC addnC ltn_add2r.
+ - move : Hlt => /ltP /ltP Hlt. rewrite <- leqNgt in Hlt.
+ rewrite <- (leq_add2l x) in Hlt.
+ apply leq_ltn_trans with (p := (FIFO_trace Reqs).(Time) + FIFO_wait + y) in Hlt.
+ - by rewrite addnC.
+ - by rewrite addnCAC ltn_add2r.
+ - apply Reqs_sorted_cons in Hs.
+ decompose_Reqs_uniq Hu Nia.
+ rewrite addnACl [y + _]addnC nat_maxn_add [FIFO_wait + _]addnC.
+ apply nat_le_lemaxn_add.
+ by apply IHReqs.
+ Qed.
+
+ Lemma FIFO_trace_Req_Before_date_offs x y req req' Reqs:
+ Reqs_sorted_ok Reqs -> uniq Reqs -> req \in Reqs -> req' \in Reqs ->
+ req != req' -> FIFO_Req_before req' req Reqs -> x < y + FIFO_wait ->
+ req'.(Date) + x < (FIFO_trace (FIFO_Reqs_before req Reqs)).(Time) + y.
+ Proof.
+ induction Reqs; auto.
+ intros Hs Hu Ir Ir' Hneq Rb Hltw.
+ decompose_Reqs_in Ir Heq; decompose_Reqs_in Ir' Heq'; subst; auto.
+ - contradict Hneq. by rewrite eq_refl.
+ - rewrite FIFO_Reqs_before_head.
+ apply Reqs_sorted_cons in Hs.
+ decompose_Reqs_uniq Hu Nia.
+ by apply (FIFO_trace_Req_Before_date x y req').
+ - contradict Rb.
+ move : Hneq => /negPf Hneq.
+ simpl. by rewrite Hneq eq_refl.
+ - apply Reqs_sorted_cons in Hs.
+ rewrite FIFO_Req_before_in in Rb; auto.
+ decompose_Reqs_uniq Hu Nia.
+ rewrite FIFO_Reqs_before_in; auto.
+ Qed.
+
+ Lemma FIFO_Reqs_Before_Reqs_trace_offs x y req Reqs:
+ Reqs_sorted_ok Reqs -> uniq Reqs -> req \in Reqs -> x < y + FIFO_wait ->
+ (FIFO_trace (FIFO_Reqs_before req Reqs)).(Time) + x < (FIFO_trace Reqs).(Time) + y.
+ Proof.
+ induction Reqs; auto.
+ intros Hs Hu Ir Hltw.
+ decompose_Reqs_in Ir Heq; subst; auto.
+ - rewrite FIFO_Reqs_before_head.
+ simpl. rewrite /FIFO_next_time addnACl [y + _]addnC [FIFO_wait + _]addnC nat_maxn_add.
+ apply nat_lt_add_lemaxn_add.
+ by rewrite addnCAC addnC ltn_add2r addnC.
+ - decompose_Reqs_uniq Hu Nia.
+ apply Reqs_sorted_cons in Hs.
+ rewrite FIFO_Reqs_before_in; auto.
+ simpl. rewrite /FIFO_next_time addnACl [y + _]addnC addnC [FIFO_wait + _]addnC nat_maxn_add addnC.
+ apply nat_le_lemaxn_add.
+ by apply IHReqs.
+ Qed.
+
+ Lemma FIFO_Reqs_Before_trace_offs x y req' req Reqs:
+ Reqs_sorted_ok Reqs -> uniq Reqs -> req \in Reqs -> req' \in Reqs -> req != req' ->
+ FIFO_Req_before req' req Reqs -> x < y + FIFO_wait ->
+ (FIFO_trace (FIFO_Reqs_before req' Reqs)).(Time) + x < (FIFO_trace (FIFO_Reqs_before req Reqs)).(Time) + y.
+ Proof.
+ induction Reqs; auto.
+ intros Hs Hu Ir Ir' Hneq Rb Hltw.
+ decompose_Reqs_in Ir Heq; decompose_Reqs_in Ir' Heq'; subst; auto.
+ - contradict Hneq. by rewrite eq_refl.
+ - decompose_Reqs_uniq Hu Nia.
+ rewrite FIFO_Reqs_before_in; auto.
+ rewrite FIFO_Reqs_before_head; auto.
+ apply Reqs_sorted_cons in Hs.
+ by apply FIFO_Reqs_Before_Reqs_trace_offs.
+ - contradict Rb. simpl.
+ destruct (req == a) eqn:Heq.
+ - move : Heq => /eqP Heq. subst.
+ decompose_Reqs_uniq Hu Nia.
+ contradict Nia. by rewrite Ir.
+ - by rewrite eq_refl.
+ - apply Reqs_sorted_cons in Hs.
+ rewrite FIFO_Req_before_in in Rb; auto.
+ decompose_Reqs_uniq Hu Nia.
+ rewrite -> 2 FIFO_Reqs_before_in; auto.
+ Qed.
+
+ Lemma FIFO_trace_base_date_dist x y req' req Reqs:
+ Reqs_sorted_ok Reqs -> uniq Reqs -> req \in Reqs -> req' \in Reqs -> req != req' ->
+ FIFO_Req_before req' req Reqs -> x < y + FIFO_wait ->
+ ((FIFO_trace_base_date req' Reqs) + x) < (FIFO_trace_base_date req Reqs) + y.
+ Proof.
+ intros Hs Hu Ir Ir' Hneq Rb Hltw.
+ rewrite /FIFO_trace_base_date /FIFO_next_time [_ + y]nat_maxn_add.
+ apply nat_le_lemaxn.
+ unfold maxn.
+ destruct (Time (FIFO_trace (FIFO_Reqs_before req' Reqs)) < Date req').
+ - by apply FIFO_trace_Req_Before_date_offs.
+ - by apply FIFO_Reqs_Before_trace_offs.
+ Qed.
+
+ Lemma FIFO_trace_base_date_dist0 x req' req Reqs:
+ Reqs_sorted_ok Reqs -> uniq Reqs -> req \in Reqs -> req' \in Reqs -> req != req' ->
+ FIFO_Req_before req' req Reqs -> x < FIFO_wait ->
+ ((FIFO_trace_base_date req' Reqs) + x) < (FIFO_trace_base_date req Reqs).
+ Proof.
+ intros Hs Hu Ir Ir' Hneq Rb Hltw.
+ rewrite <- (addn0 (FIFO_trace_base_date req Reqs)).
+ by apply FIFO_trace_base_date_dist.
Qed.
- Lemma FIFO_trace_dist req Reqs:
- (FIFO_trace Reqs).(Time) + FIFO_wait <= (FIFO_trace (req::Reqs)).(Time).
+ Lemma FIFO_cmd_req_in cmd Reqs:
+ cmd \in (FIFO_trace Reqs).(Cmds) ->
+ cmd.(Request) \in Reqs.
Proof.
+ induction Reqs; auto.
+ intros Ic.
simpl.
- apply nat_le_add_lemaxn_add.
- apply leqnn.
+ rewrite in_cons. apply /orP.
+ destruct (cmd.(Request) == a) eqn:Heqn.
+ - by left.
+ - right.
+ simpl in Ic. decompose_FIFO_cmds Ic c; subst; simpl in Heqn.
+ - 1,2,3: contradict Heqn; by rewrite eq_refl.
+ - by apply IHReqs.
+ Qed.
+
+ Ltac FIFO_contradict_isCmd H :=
+ contradict H;
+ unfold isACT, isPRE, isCMD,
+ ACT_of_req, PRE_of_req, Cmd_of_req, Kind_of_req;
+ by (simpl + destruct (Kind _)).
+
+ Lemma FIFO_ACT_at_Reqs_before cmd Reqs:
+ uniq Reqs -> cmd \in (FIFO_trace Reqs).(Cmds) -> isACT cmd ->
+ cmd.(CDate) = FIFO_trace_base_date cmd.(Request) Reqs + FIFO_ACT_date.
+ Proof.
+ induction Reqs;
+ intros Hu Ic iA.
+ - contradict Ic. by rewrite in_nil.
+ - decompose_FIFO_cmds Ic c; subst.
+ - FIFO_contradict_isCmd iA.
+ - move : Hu => /andP [Nia Hu].
+ fold FIFO_trace.
+ by rewrite FIFO_trace_base_date_head.
+ - FIFO_contradict_isCmd iA.
+ - move : Hu => /andP [Nia Hu].
+ rewrite FIFO_trace_base_date_in; auto.
+ by apply FIFO_cmd_req_in.
+ Qed.
+
+ Lemma FIFO_PRE_at_Reqs_before cmd Reqs:
+ uniq Reqs -> cmd \in (FIFO_trace Reqs).(Cmds) -> isPRE cmd ->
+ cmd.(CDate) = FIFO_trace_base_date cmd.(Request) Reqs + FIFO_PRE_date.
+ Proof.
+ induction Reqs;
+ intros Hu Ic iP.
+ - contradict Ic. by rewrite in_nil.
+ - decompose_FIFO_cmds Ic c; subst.
+ - FIFO_contradict_isCmd iP.
+ - FIFO_contradict_isCmd iP.
+ - move : Hu => /andP [Nia Hu].
+ fold FIFO_trace.
+ by rewrite FIFO_trace_base_date_head.
+ - move : Hu => /andP [Nia Hu].
+ rewrite FIFO_trace_base_date_in; auto.
+ fold FIFO_trace in Ic. fold mem_seq in Ic. simpl in Ic.
+ by apply FIFO_cmd_req_in.
+ Qed.
+
+ Lemma FIFO_CMD_at_Reqs_before cmd Reqs:
+ uniq Reqs -> cmd \in (FIFO_trace Reqs).(Cmds) -> isCMD cmd ->
+ cmd.(CDate) = FIFO_trace_base_date cmd.(Request) Reqs + FIFO_CMD_date.
+ Proof.
+ induction Reqs;
+ intros Hu Ic iC.
+ - contradict Ic. by rewrite in_nil.
+ - decompose_FIFO_cmds Ic c; subst.
+ - move : Hu => /andP [Nia Hu].
+ fold FIFO_trace.
+ by rewrite FIFO_trace_base_date_head.
+ - FIFO_contradict_isCmd iC.
+ - FIFO_contradict_isCmd iC.
+ - move : Hu => /andP [Nia Hu].
+ rewrite FIFO_trace_base_date_in; auto.
+ fold FIFO_trace in Ic. fold mem_seq in Ic. simpl in Ic.
+ by apply FIFO_cmd_req_in.
Qed.
Lemma FIFO_trace_time_ok Reqs:
forall cmd, cmd \in (FIFO_trace Reqs).(Cmds) -> cmd.(CDate) <= (FIFO_trace Reqs).(Time).
Proof.
intros.
- specialize FIFO_cmds as Hc.
induction Reqs; auto.
simpl in *.
rewrite -> 3 in_cons in H.
@@ -116,6 +327,71 @@ Section FIFO.
by apply nat_le_lemaxn_add with (x := FIFO_wait) (o := a.(Date)) in H.
Qed.
+ Lemma FIFO_next_time_lt_cmd x req' c Reqs :
+ x > 0 -> c \in (FIFO_trace Reqs).(Cmds) ->
+ (CDate c < FIFO_next_time req' (FIFO_trace Reqs) + x).
+ Proof.
+ intros gt1 Ic.
+ apply FIFO_trace_time_ok in Ic.
+ apply leq_ltn_trans with (p := (FIFO_trace Reqs).(Time) + x) in Ic.
+ - unfold FIFO_next_time.
+ by apply nat_lt_add_lemaxn_add with (o := req'.(Date)) in Ic.
+ - by apply nat_ltnn_add.
+ Qed.
+
+ Lemma FIFO_trace_head_in c req Reqs:
+ uniq (req::Reqs) -> c.(Request) \in Reqs ->
+ c \in Cmds (FIFO_trace (req :: Reqs)) ->
+ c \in Cmds (FIFO_trace (Reqs)).
+ Proof.
+ intros Hu Ir Ic.
+ simpl in Hu; move : Hu => /andP [Nia Hu].
+ decompose_FIFO_cmds Ic cmd; subst.
+ 1,2,3: simpl in Ir; contradict Nia; by rewrite Ir.
+ exact Ic.
+ Qed.
+
+ Lemma FIFO_Before_Req_before a b Reqs:
+ uniq Reqs -> a \in (FIFO_trace Reqs).(Cmds) ->
+ b \in (FIFO_trace Reqs).(Cmds) -> Before a b ->
+ FIFO_Req_before a.(Request) b.(Request) Reqs.
+ Proof.
+ intros Hu Ia Ib aBb.
+ apply FIFO_cmd_req_in in Ia as Ir'.
+ apply FIFO_cmd_req_in in Ib as Ir.
+ induction Reqs; auto.
+ rewrite -> in_cons in Ir, Ir'.
+ move : Ir => /orP [/eqP Heq | Ir]; move : Ir' => /orP [/eqP Heq' | Ir']; subst.
+ - simpl. by rewrite eq_refl.
+ - simpl. by rewrite eq_refl.
+ - contradict aBb. unfold Before.
+ simpl in Ia, Ib.
+ simpl in Hu; move : Hu => /andP [Nia Hu].
+ decompose_FIFO_cmds Ia cmda; decompose_FIFO_cmds Ib cmdb; subst;
+ try (simpl in Ir; contradict Nia; by rewrite Ir).
+ - rewrite cmda. simpl.
+ apply FIFO_next_time_lt_cmd with (x := FIFO_CMD_date) (req' := a.(Request)) in Ib; auto.
+ by apply /negP /ltP /PeanoNat.Nat.lt_asymm /ltP.
+ - rewrite cmda. simpl.
+ apply FIFO_next_time_lt_cmd with (x := FIFO_ACT_date) (req' := a.(Request)) in Ib; auto.
+ by apply /negP /ltP /PeanoNat.Nat.lt_asymm /ltP.
+ - rewrite cmda. simpl.
+ apply FIFO_next_time_lt_cmd with (x := FIFO_PRE_date) (req' := a.(Request)) in Ib; auto.
+ by apply /negP /ltP /PeanoNat.Nat.lt_asymm /ltP.
+ - contradict Nia.
+ apply /negP. rewrite Bool.negb_involutive.
+ by apply FIFO_cmd_req_in.
+ - simpl.
+ destruct (Request b == a0) eqn:Heqb, (Request a == a0) eqn:Heqa; auto;
+ move : Heqa Heqb => /eqP Heqa /eqP Heqb; subst.
+ - simpl in Hu; move : Hu => /andP [Nia Hu].
+ contradict Nia. by rewrite Ir'.
+ - apply FIFO_trace_head_in in Ia; auto.
+ apply FIFO_trace_head_in in Ib; auto.
+ simpl in Hu; move : Hu => /andP [Nia Hu].
+ apply IHReqs; auto.
+ Qed.
+
Lemma FIFO_trace_cmd_notin cmd Reqs:
is_true ((FIFO_trace Reqs).(Time) < cmd.(CDate)) -> is_true (cmd \notin (FIFO_trace Reqs).(Cmds)).
Proof.
@@ -126,226 +402,156 @@ Section FIFO.
contradict Hin. rewrite -> leqNgt. by apply /negP /negPn.
Qed.
- Lemma FIFO_trace_uniq req Reqs:
- is_true (uniq (FIFO_trace Reqs).(Cmds)) -> is_true (uniq (FIFO_trace (req::Reqs)).(Cmds)).
+ Lemma FIFO_trace_uniq:
+ uniq (FIFO_trace Requests).(Cmds).
Proof.
- intros.
- simpl.
+ induction Requests; auto.
+ intros. simpl.
apply /andP; split.
- rewrite in_cons negb_or. apply /andP. split.
- - apply Command_neq_CMD_ACT.
+ - by apply Command_neq_CMD_ACT.
+ - rewrite in_cons negb_or. apply /andP. split.
+ - by apply Command_neq_CMD_PRE.
+ - apply FIFO_trace_cmd_notin. by apply nat_ltmaxn_l_add.
+ - apply /andP; split.
- rewrite in_cons negb_or. apply /andP. split.
- - apply Command_neq_CMD_PRE.
+ - by apply Command_neq_ACT_PRE.
+ - apply FIFO_trace_cmd_notin. by apply nat_ltmaxn_l_add.
+ - apply /andP; split.
- apply FIFO_trace_cmd_notin.
by apply nat_ltmaxn_l_add.
- apply /andP; split.
- - rewrite in_cons negb_or. apply /andP. split.
- - apply Command_neq_ACT_PRE.
- - apply FIFO_trace_cmd_notin.
- by apply nat_ltmaxn_l_add.
- apply /andP; split.
- - apply FIFO_trace_cmd_notin.
- by apply nat_ltmaxn_l_add.
- - auto.
+ - done.
Qed.
- Lemma FIFO_trace_T_RC_ok Reqs:
- forall a b, a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
+ Lemma FIFO_trace_T_RC_ok:
+ forall a b, a \in (FIFO_trace Requests).(Cmds) -> b \in (FIFO_trace Requests).(Cmds) ->
ACT_to_ACT a b -> Same_Bank a b -> Before a b ->
Apart a b T_RC.
Proof.
- induction Reqs as [| req Reqs']; auto.
intros a b Ia Ib AtA SB aBb.
- decompose_FIFO_cmds Ib Cmdb; decompose_FIFO_cmds Ia Cmda;
- try contradict_AtoA AtA req.
- - contradict aBb. subst. unfold Before. apply /negP. by rewrite ltnn.
- - destruct Reqs'.
- - by contradict Ia.
- - decompose_FIFO_cmds Ia Cmda;
- try contradict_AtoA AtA req; try contradict_AtoA AtA r;
- subst; unfold Apart, ACT_of_req; simpl.
- - set T := maxn (FIFO_trace Reqs').(Time) r.(Date).
- unfold maxn. simpl.
- destruct (T + FIFO_wait < req.(Date)) eqn:Hlt.
- 1 : rewrite <- (ltn_add2r FIFO_ACT_date) in Hlt.
- 1 : apply ltn_trans with (n := T + FIFO_wait + FIFO_ACT_date); auto.
- 1,2: rewrite addnCAC [T + FIFO_wait + FIFO_ACT_date]addnCAC.
- 1,2: rewrite [FIFO_ACT_date + _]addnC.
- 1,2: rewrite ltn_add2r ltn_add2r.
- 1,2: by specialize FIFO_T_RC.
- - set T := maxn (FIFO_trace (r :: Reqs')).(Time) req.(Date).
- set Tf := (FIFO_trace Reqs').(Time) + FIFO_wait.
- specialize (FIFO_trace_dist r Reqs') as Hdist.
- apply leq_trans with (p := T) in Hdist.
- - rewrite <- (leq_add2r FIFO_ACT_date) in Hdist.
- rewrite addnS in Hdist.
- apply FIFO_trace_time_ok in Ia as H.
- rewrite <- (leq_add2r T_RC) in H.
- apply leq_ltn_trans with (p := Tf) in H.
- - apply ltn_trans with (p := Tf + (T_RP + 1)) in H.
- - by apply ltn_trans with (p := T + FIFO_ACT_date) in H.
- - apply nat_ltnn_add. rewrite addn_gt0. apply /orP. by right.
- - rewrite ltn_add2l. by specialize FIFO_T_RC.
- - unfold T. by apply leq_maxl.
- - contradict aBb. subst a.
- apply /negP.
- unfold Before, ACT_of_req. rewrite <- leqNgt. apply nat_le_lemaxn_add.
- by apply (FIFO_trace_time_ok Reqs') in Ib.
- - by apply (IHReqs' a b) in Ia.
- Qed.
-
- Lemma FIFO_trace_T_RP_ok Reqs:
- forall a b, a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
+ destruct Input.
+ move : AtA => /andP [iAa iAb].
+ apply FIFO_ACT_at_Reqs_before in Ia as Da;
+ apply FIFO_ACT_at_Reqs_before in Ib as Db; try exact.
+ apply FIFO_Before_Req_before with (Reqs := Requests) in aBb as RB; auto.
+ apply FIFO_cmd_req_in in Ia as Ir.
+ apply FIFO_cmd_req_in in Ib as Ir'.
+ rewrite /Apart Da Db addnACl addnC ltn_add2r addnC.
+ destruct (Request b == Request a) eqn:Heq;
+ move : Heq => /eqP Heq.
+ - contradict aBb. rewrite -> Heq in *.
+ by rewrite /Before Da Db ltnn.
+ - move : Heq => /eqP Heq. specialize FIFO_T_RC.
+ by apply FIFO_trace_base_date_dist0.
+ Qed.
+
+ Lemma FIFO_T_RP_neq:
+ T_RP + FIFO_PRE_date < FIFO_ACT_date + FIFO_wait.
+ Proof.
+ rewrite /FIFO_ACT_date addnC addnCAC [_ + (FIFO_PRE_date + T_RP)]addnC.
+ apply nat_ltnn_add. rewrite addn1. by apply ltn0Sn.
+ Qed.
+
+ Lemma FIFO_T_RP_eq:
+ (T_RP + FIFO_PRE_date) < FIFO_ACT_date.
+ Proof.
+ rewrite /FIFO_ACT_date addnCAC ltn_add2r addnC addn1. by apply ltnSn.
+ Qed.
+
+ Lemma FIFO_trace_T_RP_ok:
+ forall a b, a \in (FIFO_trace Requests).(Cmds) -> b \in (FIFO_trace Requests).(Cmds) ->
PRE_to_ACT a b -> Same_Bank a b -> Before a b ->
Apart a b T_RP.
Proof.
- induction Reqs as [| req Reqs']; auto.
- intros a b Ia Ib PtA SB aBb.
- decompose_FIFO_cmds Ib Cmdb; decompose_FIFO_cmds Ia Cmda;
- try (contradict_PtoA PtA req).
- - unfold Apart. subst. simpl.
- unfold FIFO_ACT_date.
- rewrite addnCAC addnC ltn_add2l addnC. by apply nat_ltnn_add.
- - destruct Reqs'.
- - by contradict Ia.
- - decompose_FIFO_cmds Ia Cmda;
- try contradict_PtoA PtA req; try contradict_PtoA PtA r;
- subst; unfold Apart, ACT_of_req, PRE_of_req; simpl.
- - set T := maxn (FIFO_trace Reqs').(Time) r.(Date).
- unfold maxn. simpl.
- destruct (T + FIFO_wait < req.(Date)) eqn:Hlt.
- 1 : rewrite <- (ltn_add2r FIFO_ACT_date) in Hlt.
- 1 : apply ltn_trans with (n := T + FIFO_wait + FIFO_ACT_date); auto.
- 1,2: rewrite addnCAC [T + FIFO_wait + FIFO_ACT_date]addnCAC.
- 1,2: rewrite [FIFO_ACT_date + _]addnC.
- 1,2: rewrite ltn_add2r.
- 1,2: apply nat_add_lt_add.
- 1,2: apply /andP; split.
- 1,3: by specialize FIFO_T_RP.
- 1,2: unfold FIFO_ACT_date.
- 1,2: rewrite addnCAC addnC; apply nat_ltnn_add.
- 1,2: rewrite addn_gt0; apply /orP; by left.
- - set T := maxn (FIFO_trace (r :: Reqs')).(Time) req.(Date).
- set Tf := (FIFO_trace Reqs').(Time) + FIFO_wait.
- specialize (FIFO_trace_dist r Reqs') as Hdist.
- apply leq_trans with (p := T) in Hdist.
- - rewrite <- (leq_add2r FIFO_ACT_date) in Hdist.
- rewrite addnS in Hdist.
- apply FIFO_trace_time_ok in Ia as H.
- rewrite <- (leq_add2r T_RP) in H.
- apply leq_ltn_trans with (p := Tf) in H.
- - apply ltn_trans with (p := Tf + (T_RP + 1)) in H.
- - by apply ltn_trans with (p := T + FIFO_ACT_date) in H.
- - apply nat_ltnn_add. rewrite addn_gt0. apply /orP. by right.
- - rewrite ltn_add2l. by specialize FIFO_T_RP.
- - unfold T. by apply leq_maxl.
- - contradict aBb. subst a.
- apply /negP.
- unfold Before, ACT_of_req. rewrite <- leqNgt. apply nat_le_lemaxn_add.
- by apply (FIFO_trace_time_ok Reqs') in Ib.
- - by apply (IHReqs' a b) in Ia.
- Qed.
-
- Lemma FIFO_trace_T_RCD_ok Reqs:
- forall a b, a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
+ intros a b Ia Ib AtA SB aBb.
+ destruct Input.
+ move : AtA => /andP [iAa iAb].
+ apply FIFO_PRE_at_Reqs_before in Ia as Da; auto.
+ apply FIFO_ACT_at_Reqs_before in Ib as Db; auto.
+ apply FIFO_Before_Req_before with (Reqs := Requests) in aBb as RB; auto.
+ apply FIFO_cmd_req_in in Ia as Ir.
+ apply FIFO_cmd_req_in in Ib as Ir'.
+ rewrite /Apart Da Db addnCAC addnC.
+ destruct (Request b == Request a) eqn:Heq;
+ move : Heq => /eqP Heq.
+ - rewrite Heq ltn_add2l. by apply FIFO_T_RP_eq.
+ - move : Heq => /eqP Heq. specialize FIFO_T_RP_neq.
+ by apply FIFO_trace_base_date_dist.
+ Qed.
+
+ Lemma FIFO_trace_T_RCD_eq:
+ (T_RCD + FIFO_ACT_date) < FIFO_CMD_date.
+ Proof.
+ rewrite /FIFO_CMD_date addn1 addnC. by apply ltnSn.
+ Qed.
+
+ Lemma FIFO_trace_T_RCD_neq:
+ (T_RCD + FIFO_ACT_date) < (FIFO_CMD_date + FIFO_wait).
+ Proof.
+ rewrite /FIFO_CMD_date addnC addnCAC. rewrite [(_+_) + (_+_)]addnC addn1.
+ apply nat_ltnn_add. by apply ltn0Sn.
+ Qed.
+
+ Lemma FIFO_trace_T_RCD_ok:
+ forall a b, a \in (FIFO_trace Requests).(Cmds) -> b \in (FIFO_trace Requests).(Cmds) ->
ACT_to_CMD a b -> Same_Bank a b -> Before a b ->
Apart a b T_RCD.
Proof.
- induction Reqs as [| req Reqs']; auto.
- intros a b Ia Ib AtC SB aBb.
- decompose_FIFO_cmds Ib Cmdb; decompose_FIFO_cmds Ia Cmda;
- try (contradict_AtoC AtC req).
- - unfold Apart. subst. simpl.
- unfold FIFO_CMD_date.
- rewrite addnCAC addnC ltn_add2l addnC. by apply nat_ltnn_add.
- - destruct Reqs'.
- - by contradict Ia.
- - decompose_FIFO_cmds Ia Cmda;
- try contradict_AtoC CtA req; try contradict_AtoC AtC r;
- subst; unfold Apart, ACT_of_req, Cmd_of_req; simpl.
- - set T := maxn (FIFO_trace Reqs').(Time) r.(Date).
- unfold maxn. simpl.
- destruct (T + FIFO_wait < req.(Date)) eqn:Hlt.
- 1 : rewrite <- (ltn_add2r FIFO_CMD_date) in Hlt.
- 1 : apply ltn_trans with (n := T + FIFO_wait + FIFO_CMD_date); auto.
- 1,2: rewrite addnCAC [T + FIFO_wait + FIFO_CMD_date]addnCAC.
- 1,2: rewrite [FIFO_CMD_date + _]addnC.
- 1,2: rewrite ltn_add2r.
- 1,2: apply nat_add_lt_add.
- 1,2: apply /andP; split.
- 1,3: by specialize FIFO_T_RCD.
- 1,2: unfold FIFO_CMD_date.
- 1,2: rewrite addnCAC addnC; apply nat_ltnn_add.
- 1,2: rewrite addn_gt0; apply /orP; by left.
- - set T := maxn (FIFO_trace (r :: Reqs')).(Time) req.(Date).
- Opaque FIFO_CMD_date.
- set Tf := (FIFO_trace Reqs').(Time) + FIFO_wait.
- specialize (FIFO_trace_dist r Reqs') as Hdist.
- apply leq_trans with (p := T) in Hdist.
- fold Tf in Hdist.
- - rewrite <- (leq_add2r FIFO_CMD_date) in Hdist.
- rewrite addnC addnACl addnC addn1 in Hdist.
- apply FIFO_trace_time_ok in Ia as H.
- rewrite <- (leq_add2r T_RCD) in H.
- apply leq_ltn_trans with (p := Tf) in H.
- - apply ltn_trans with (p := Tf + (FIFO_ACT_date + T_RCD)) in H.
- - by apply ltn_trans with (p := T + FIFO_CMD_date) in H.
- - apply nat_ltnn_add. rewrite addn_gt0. apply /orP. by left.
- - rewrite ltn_add2l. by specialize FIFO_T_RCD.
- - unfold T. by apply leq_maxl.
- - contradict aBb. subst a.
- apply /negP.
- unfold Before, ACT_of_req. rewrite <- leqNgt. apply nat_le_lemaxn_add.
- by apply (FIFO_trace_time_ok Reqs') in Ib.
- - by apply (IHReqs' a b) in Ia.
+ intros a b Ia Ib AtA SB aBb.
+ destruct Input.
+ move : AtA => /andP [iAa iAb].
+ apply FIFO_ACT_at_Reqs_before in Ia as Da; auto.
+ apply FIFO_CMD_at_Reqs_before in Ib as Db; auto.
+ apply FIFO_Before_Req_before with (Reqs := Requests) in aBb as RB; auto.
+ apply FIFO_cmd_req_in in Ia as Ir.
+ apply FIFO_cmd_req_in in Ib as Ir'.
+ rewrite /Apart Da Db addnCAC addnC.
+ destruct (Request b == Request a) eqn:Heq;
+ move : Heq => /eqP Heq.
+ - rewrite Heq ltn_add2l. by apply FIFO_trace_T_RCD_eq.
+ - move : Heq => /eqP Heq. specialize FIFO_trace_T_RCD_neq.
+ by apply FIFO_trace_base_date_dist.
Qed.
Ltac contradict_AtoP H req :=
(contradict H; subst; unfold ACT_to_PRE, isACT, PRE_of_req, Cmd_of_req, Kind_of_req; simpl; destruct (Kind req));
(done + apply /negP; rewrite negb_and; apply /orP; by right).
+ Lemma FIFO_trace_T_RAS_eq:
+ ~ FIFO_ACT_date < FIFO_PRE_date.
+ Proof.
+ apply /negP. rewrite <- leqNgt.
+ rewrite /FIFO_ACT_date addnCAC addnC add1n. by apply leq_addr.
+ Qed.
- Lemma FIFO_trace_T_RAS_ok Reqs:
- forall a b, a \in (FIFO_trace Reqs).(Cmds) -> b \in (FIFO_trace Reqs).(Cmds) ->
+ Lemma FIFO_trace_T_RAS_neq:
+ (T_RAS + FIFO_ACT_date) < (FIFO_PRE_date + FIFO_wait).
+ Proof.
+ rewrite /FIFO_ACT_date [FIFO_PRE_date + _]addnC addnACl addnC addnCAC addnC ltn_add2l.
+ by apply FIFO_T_RAS.
+ Qed.
+
+ Lemma FIFO_trace_T_RAS_ok:
+ forall a b, a \in (FIFO_trace Requests).(Cmds) -> b \in (FIFO_trace Requests).(Cmds) ->
ACT_to_PRE a b -> Same_Bank a b -> Before a b ->
Apart a b T_RAS.
Proof.
- induction Reqs as [| req Reqs']; auto.
- intros a b Ia Ib AtC SB aBb.
- decompose_FIFO_cmds Ib Cmdb; decompose_FIFO_cmds Ia Cmda;
- try (contradict_AtoP AtC req).
- - contradict aBb. subst.
- apply /negP.
- unfold Before, ACT_of_req, PRE_of_req. rewrite <- leqNgt. simpl.
- apply leq_add.
- - by apply leqnn.
- - unfold FIFO_ACT_date.
- rewrite addnC. rewrite <- addnACl. rewrite addnC.
- by apply leq_addr.
- - destruct Reqs'.
- - by contradict Ia.
- - decompose_FIFO_cmds Ia Cmda;
- try contradict_AtoP AtC req; try contradict_AtoC AtC r;
- subst; unfold Apart, ACT_of_req, PRE_of_req, FIFO_ACT_date; simpl.
- - set T := maxn (FIFO_trace Reqs').(Time) r.(Date).
- apply nat_lt_add_lemaxn_add.
- clear SB aBb AtC.
- rewrite [(_ + _) + 1]addnCAC 2![_ + FIFO_PRE_date]addnC. rewrite <- addnACl.
- rewrite [_ + FIFO_PRE_date]addnC addnCAC [_ + FIFO_PRE_date]addnC ltn_add2l.
- rewrite [_ + T]addnC. rewrite <- addnACl. rewrite addnC ltn_add2l.
- by specialize FIFO_T_RAS as H.
- - fold FIFO_trace. apply nat_lt_add_lemaxn_add. rewrite nat_maxn_add. apply nat_lt_add_lemaxn_add.
- apply FIFO_trace_time_ok in Ia as H.
- rewrite <- (leq_add2r T_RAS) in H.
- apply leq_ltn_trans with (p := (FIFO_trace Reqs').(Time) + FIFO_wait + FIFO_PRE_date) in H.
- - done.
- - rewrite addnCAC [_ + (FIFO_trace Reqs').(Time)]addnC ltn_add2l.
- specialize FIFO_T_RAS' as Hlt. by apply ltn_addl.
- - contradict aBb. subst a.
- apply /negP.
- unfold Before, ACT_of_req. rewrite <- leqNgt. apply nat_le_lemaxn_add.
- by apply (FIFO_trace_time_ok Reqs') in Ib.
- - by apply (IHReqs' a b) in Ia.
+ intros a b Ia Ib AtA SB aBb.
+ destruct Input.
+ move : AtA => /andP [iAa iAb].
+ apply FIFO_ACT_at_Reqs_before in Ia as Da; auto.
+ apply FIFO_PRE_at_Reqs_before in Ib as Db; auto.
+ apply FIFO_Before_Req_before with (Reqs := Requests) in aBb as RB; auto.
+ apply FIFO_cmd_req_in in Ia as Ir.
+ apply FIFO_cmd_req_in in Ib as Ir'.
+ rewrite /Apart Da Db addnCAC addnC.
+ destruct (Request b == Request a) eqn:Heq;
+ move : Heq => /eqP Heq.
+ - contradict aBb. rewrite -> Heq in *.
+ rewrite /Before Da Db ltn_add2l.
+ by apply FIFO_trace_T_RAS_eq.
+ - move : Heq => /eqP Heq. specialize FIFO_trace_T_RAS_neq.
+ by apply FIFO_trace_base_date_dist.
Qed.
Lemma Between_cons req Reqs a b:
@@ -393,16 +599,11 @@ Ltac contradict_AtoP H req :=
- rewrite <- Between_cons. apply IHReqs in Ia. apply Ia. all : auto.
Admitted.
- Program Definition FIFO_arbitrate :=
+ Definition FIFO_arbitrate :=
let State := FIFO_trace Requests in
- mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests)
- (FIFO_trace_Cmds_PRE_ok Requests) (FIFO_trace_T_RC_ok Requests) (FIFO_trace_T_RP_ok Requests)
- (FIFO_trace_T_RCD_ok Requests) (FIFO_trace_T_RAS_ok Requests).
- Next Obligation.
- induction Requests.
- - auto.
- - by apply (FIFO_trace_uniq a) in IHl.
- Qed.
+ mkTrace State.(Cmds) State.(Time) FIFO_trace_uniq (FIFO_trace_time_ok Requests)
+ (FIFO_trace_Cmds_PRE_ok Requests) FIFO_trace_T_RC_ok FIFO_trace_T_RP_ok
+ FIFO_trace_T_RCD_ok FIFO_trace_T_RAS_ok.
Lemma FIFO_trace_Req_handled Reqs:
forall req, req \in Reqs ->
diff --git a/coq/Requests.v b/coq/Requests.v
index 80a68bf..60cb28b 100644
--- a/coq/Requests.v
+++ b/coq/Requests.v
@@ -95,4 +95,20 @@ Section Requests.
Reqs_issue : forall a b, a \in Requests -> b \in Requests -> a != b ->
a.(Date) == b.(Date) -> a.(Bank) != b.(Bank);
}.
+
+ Lemma Reqs_sorted_cons req Reqs:
+ Reqs_sorted_ok (req::Reqs) -> Reqs_sorted_ok Reqs.
+ Proof.
+ intros Hs.
+ induction Reqs; auto.
+ simpl in *. by move : Hs => /andP [Hleq Hs].
+ Qed.
End Requests.
+
+Ltac decompose_Reqs_in H suffix :=
+ let Heq := fresh suffix in
+ rewrite -> in_cons in H; move : H => /orP [/eqP Heq | H].
+
+Ltac decompose_Reqs_uniq H suffix :=
+ let Nia := fresh suffix in
+ rewrite cons_uniq in H; move : H => /andP [Nia H].
--
GitLab