Skip to content
Snippets Groups Projects
Commit 23b6f041 authored by Florian Brandner's avatar Florian Brandner
Browse files

entirely rework proofs for FIFO 

* less direct proofs
* instead use general properties of the FIFO implementation
parent 476778e3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
coq/FIFO.v
+ 437
− 236
View file @ 23b6f041
......@@ -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 ->
......
coq/Requests.v
+ 16
− 0
View file @ 23b6f041
......@@ -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].
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment