Commit 79f3c265 authored by Hai Dang's avatar Hai Dang
Browse files

Reuse more proofs (stack LIFO)

parent 5b75db74
......@@ -975,6 +975,7 @@ Proof.
apply lookup_app_1 in Eqee as [?|[-> <-]]; [done|].
exfalso. apply FRT. by apply elem_of_list_lookup_2 in EqT. }
(* StackProps *)
iDestruct "CASE" as "[[F EL]|[F CASE]]".
{ (* exchange fails *)
iDestruct "F" as %(-> & Eqsox' & ? & ? & ? & ->).
......@@ -1734,34 +1735,10 @@ Proof.
- (* 5 *) by apply stack_empty_unmatched_push_insert_edge.
- by rewrite /G' /= SCSO.
- (* stack_LIFO *)
(* the pair comes from exchanger, we may want to require that if one
sees a push it must also have seen the matching pop. *)
(* TODO: remove some dups here *)
intros u1 o1 oV1 u2 o2 uV2 oV2. rewrite 2!elem_of_union 2!elem_of_singleton.
intros In1 In2 NEqu Eqo1 Equ2 Eqo2.
destruct In1 as [Eq1|In1]; [apply pair_inj in Eq1 as [-> ->]|];
(destruct In2 as [Eq2|In2]; [apply pair_inj in Eq2 as [-> ->]|]); [done|..].
+ rewrite lookup_app_1_eq in Eqo1. inversion Eqo1. clear Eqo1. subst oV1.
destruct (NI _ _ In2). rewrite lookup_app_1_ne in Eqo2; [|done].
intros _ Lt'%(egcons_logview_closed _ EGCs _ _ Eqo2)%lookup_lt_is_Some _.
clear -Lt'; lia.
+ clear NEqu Equ2 Eqo2.
rewrite lookup_app_1_ne in Eqo1; [|apply (NI _ _ In1)].
simpl. intros _ _ InpsId.
assert (Leo1 := SCMO _ _ _ Eqo1 InpsId).
assert (NEqo1: psId o1).
{ clear -SCMA EqeVps EqeVs In1. intros <-.
specialize (SCMA _ _ In1) as [_ (_ & dV1 & v' & _ & EqdV1 & _ & Eqv' & _)].
rewrite EqeVps in EqdV1. apply Some_inj in EqdV1 as <-.
by rewrite EqeVs in Eqv'. }
(* we know that psId is the biggest in G, so it cannot be in o1's view *)
apply NEqo1, (anti_symm Nat.le); [exact Leo1|]. clear -Eqo1.
apply lookup_lt_Some in Eqo1. subst psId. lia.
+ destruct (NI _ _ In1), (NI _ _ In2).
rewrite lookup_app_1_ne in Eqo1; [|done].
rewrite lookup_app_1_ne in Equ2; [|done].
rewrite lookup_app_1_ne in Eqo2; [|done].
revert In1 In2 NEqu Eqo1 Equ2 Eqo2. by apply SCLIFO.
apply (stack_LIFO_insert_edge _ _ _ _ _ _ EqeVps EqeVs); [|done..]. clear.
intros u1 o1 [_ In1]%gcons_com_included [_ Lto1] _.
(* we know that psId is the biggest in G, so it cannot be smaller than o1 *)
simpl in In1. subst psId. lia.
- clear -SubM' SCMO. by apply graph_insert_xo_eco.
}
......
......@@ -1848,44 +1848,16 @@ Proof.
- (* 5 *) by apply stack_empty_unmatched_push_insert_edge.
- by rewrite /G' /= SC2SO.
- (* LIFO *)
intros u1 o1 oV1 u2 o2 uV2 oV2. rewrite 2!elem_of_union 2!elem_of_singleton.
intros In1 In2 NEqu Eqo1 Equ2 Eqo2.
destruct In1 as [Eq1|In1]; [inversion Eq1; subst u1 o1; clear Eq1|];
(destruct In2 as [Eq2|In2]; [inversion Eq2; subst u2 o2; clear Eq2|]); [done|..].
+ rewrite lookup_app_1_eq in Eqo1. inversion Eqo1. clear Eqo1. subst oV1.
destruct (NI _ _ In2). rewrite lookup_app_1_ne in Eqo2; [|done].
intros _ ?%(egcons_logview_closed _ EGCs2 _ _ Eqo2)%lookup_lt_is_Some _. lia.
+ rewrite lookup_app_1_ne in Equ2; [|done].
rewrite lookup_app_1_eq in Eqo2. inversion Eqo2. clear Eqo2. subst oV2.
destruct (NI _ _ In1). rewrite lookup_app_1_ne in Eqo1; [|done].
rewrite Eqep in Equ2. inversion Equ2. clear Equ2. subst uV2.
simpl. intros Inu1. rewrite 2!elem_of_union elem_of_singleton.
intros InM InpsId.
assert (Leo1 := SC2MO _ _ _ Eqo1 InpsId).
assert (NEqo1: o1 psId).
{ clear -SC2MA Eqep Eqvp In1. intros ->.
specialize (SC2MA _ _ In1) as
[_ (_ & dV1 & v' & _ & EqdV1 & _ & Eqv' & _)]. rewrite Eqep in EqdV1.
inversion EqdV1. subst dV1. by rewrite Eqvp in Eqv'. }
destruct InM as [InM|[->|InM']]; [|done|].
* (* psId ∈ o1.logview => psId ≤ o1 ∧ u1 ∈ psId.logview => u1 ≤ psId ≤ o1 *)
destruct (egcons_logview_closed _ EGCs2 _ _ Eqep _ Inu1) as [uV1 EquV1].
destruct (SP2ORD2 _ _ (ltac:(by left)) EqTn u1 o1) as [[Leu Leo]|[Geu Geo]].
{ by rewrite SC2SO. }
{ (* o1 = psId, Pop = Push *)
apply NEqo1. clear -Leo1 Leo. by apply (anti_symm Nat.le). }
{ (* u1 = psId *)
assert (Leu1 := SC2MO _ _ _ Eqep Inu1).
apply NEqu. clear -Leu1 Geu. by apply (anti_symm Nat.le). }
* (* psId ∈ o1.logview => psId ≤ o1 ∧ o1 ∈ psId.logview => o1 ≤ psId
=> o1 = psId => Pop = Push => contradiction *)
apply NEqo1. apply (SC2MO _ _ _ Eqep) in InM'.
clear -InM' Leo1. by apply (anti_symm Nat.le).
+ destruct (NI _ _ In1), (NI _ _ In2).
rewrite lookup_app_1_ne in Eqo1; [|done].
rewrite lookup_app_1_ne in Equ2; [|done].
rewrite lookup_app_1_ne in Eqo2; [|done].
revert In1 In2 NEqu Eqo1 Equ2 Eqo2. by apply SC2LIFO.
apply (stack_LIFO_insert_edge _ _ _ _ _ _ Eqep Eqvp); [|done..].
clear -SP2ORD2 SC2SO SC2MO Eqep EqTn NI.
intros u1 o1 In1 [Ltu1 Lto1]. rewrite 2!elem_of_union elem_of_singleton.
destruct (NI _ _ In1).
intros [InM|[->|InM']]; [|done|].
* (* psId is still in the stack, so it cannot get in between u1 and o1 *)
rewrite -SC2SO in In1.
destruct (SP2ORD2 _ _ (ltac:(by left)) EqTn _ _ In1) as [[]|[]]; lia.
* (* psId < o1 ∧ o1 ≤ psId => contradiction *)
apply (SC2MO _ _ _ Eqep) in InM'. lia.
- clear -SubM' SC2MO. by apply graph_insert_xo_eco.
- intros u1 o1 oV1 u2 uV2. rewrite elem_of_union elem_of_singleton.
intros [Equo1|In1].
......
......@@ -584,3 +584,47 @@ Proof.
+ intros ?. subst d1. exfalso. move : (NI _ _ InG1). clear; lia.
+ move : InG1 InG2. by apply CO.
Qed.
Lemma stack_LIFO_insert_edge G e egV
(Lt: bool_decide (e < length G.(Es))%nat) eV v :
let G' := graph_insert_edge e egV G Lt in
G.(Es) !! e = Some eV eV.(ge_event) = Push v
( u1 o1, (u1, o1) G.(com) (u1 < e < o1)%nat o1 egV.(ge_lview) False)
eventgraph_consistent G
graph_xo_eco G.(Es)
stack_matches_value G
stack_LIFO G stack_LIFO G'.
Proof.
intros G' Eqe Eqv LF' EGCs MO MA LF u1 o1 oV1 u2 o2 uV2 oV2.
rewrite 2!elem_of_union 2!elem_of_singleton.
intros In1 In2 NEqu Eqo1 Equ2 Eqo2.
set e' := length G.(Es).
have NI: e1 e2, (e1, e2) G.(com) e1 e' e2 e'.
{ move => ?? /(gcons_com_included G) [/= ??]. lia. }
have NEqe' : e e'.
{ clear -Lt. apply bool_decide_unpack in Lt. intros ->. lia. }
destruct In1 as [Eq1|In1]; [apply pair_inj in Eq1 as [-> ->]|];
(destruct In2 as [Eq2|In2]; [apply pair_inj in Eq2 as [-> ->]|]); [done|..].
- rewrite lookup_app_1_eq in Eqo1. inversion Eqo1. clear Eqo1. subst oV1.
destruct (NI _ _ In2). rewrite lookup_app_1_ne in Eqo2; [|done].
intros _ Lt'%(egcons_logview_closed _ EGCs _ _ Eqo2)%lookup_lt_is_Some _.
clear -Lt'; lia.
- rewrite lookup_app_1_ne in Eqo1; [|apply (NI _ _ In1)].
rewrite lookup_app_1_eq in Eqo2. apply Some_inj in Eqo2 as <-.
rewrite lookup_app_1_ne in Equ2; [|done].
rewrite Eqe in Equ2. apply Some_inj in Equ2 as <-.
intros Inu1 InM Ino1.
assert (Leu1 := MO _ _ _ Eqe Inu1).
assert (Leo1 := MO _ _ _ Eqo1 Ino1). clear Ino1.
assert (NEqo1: e o1).
{ clear -MA Eqe Eqv In1. intros <-.
specialize (MA _ _ In1) as [_ (_ & dV1 & v' & _ & EqdV1 & _ & Eqv' & _)].
rewrite Eqe in EqdV1. apply Some_inj in EqdV1 as <-.
by rewrite Eqv in Eqv'. }
apply (LF' _ _ In1); [|done]. split; lia.
- destruct (NI _ _ In1), (NI _ _ In2).
rewrite lookup_app_1_ne in Eqo1; [|done].
rewrite lookup_app_1_ne in Equ2; [|done].
rewrite lookup_app_1_ne in Eqo2; [|done].
revert In1 In2 NEqu Eqo1 Equ2 Eqo2. by apply LF.
Qed.
Markdown is supported
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