Commit 776c5a0a authored by Hai Dang's avatar Hai Dang
Browse files

Use mono_list instead; remove olist

parent 27eecdc3
......@@ -98,7 +98,6 @@ theories/examples/uniq_token.v
theories/examples/nat_tokens.v
theories/examples/map_seq.v
theories/examples/list_helper.v
theories/examples/list_cmra.v
theories/examples/loc_helper.v
theories/examples/set_helper.v
theories/examples/big_op.v
......
From iris.algebra Require Import cmra auth.
From gpfsl.examples Require Import list_helper.
From orc11 Require Import base.
Require Import iris.prelude.options.
(* TODO: remove this once mono_list is unstaged in Iris :
https://gitlab.mpi-sws.org/iris/iris/-/blob/0fc3d8cc4a4c1dc55de3238c8c5b319f43cac90a/iris_staging/algebra/mono_list.v
*)
(** A list cmra that can only grow at the end, as defined by its [sqsubseteq] (⊑)
relation, which in turn is only used as a convenient notation for [prefix_of]. *)
(** A similar implementation is here
https://github.com/jtassarotti/iris-inv-hierarchy/blob/fupd-split-level/iris/algebra/mlist.v.
Both are inspired by the original iGPS RCU proof. *)
(** Another possibly equivalent implementation is
listUR (optionUR (agreeR (leibnizO A))).
See https://gitlab.mpi-sws.org/FCS/lang-sandbox-coq/-/blob/master/theories/lang/heap.v#L18. *)
(** Another implementation is to use an equivalent gmap lattice representation.
See https://gitlab.mpi-sws.org/iris/iris/-/issues/244#note_55782. *)
(* We box the type to avoid ambiguous instances. *)
(* We wrap the list in an option to allow for partial composition. *)
Record olistT A := to_olistT { of_olistT :> (option (list A)) }.
Arguments to_olistT {_} _.
Arguments of_olistT {_} _.
Notation to_olistT' l := (to_olistT (Some l)).
Section list.
Context (A: Type) `{EqDecision A}.
Notation olist := (option (list A)).
Notation olistT := (olistT A).
Implicit Type (l : list A).
Instance list_equiv : Equiv (list A) := eq.
Instance olistT_equiv : Equiv olistT := λ x y, of_olistT x = y.
Instance olistT_equiv_equivalence : @Equivalence olistT ().
Proof.
constructor.
- intros []; auto.
- intros [] []; auto.
- intros [] [] []. cbv; intros; by subst.
Qed.
Canonical Structure olistO := discreteO olistT.
Instance olist_valid : Valid olistT :=
λ x, if of_olistT x is None then False else True.
Instance olist_pcore : PCore olistT := Some.
(* The composition is partial *)
Instance olist_op : Op olistT :=
λ x y, to_olistT (
match of_olistT x, of_olistT y with
| Some l1, Some l2 =>
if decide (l1 l2)
then Some l2
else
if decide (l2 l1)
then Some l1
else None
| _, _ => None
end).
Global Instance olist_op_idemp : IdemP eq (op: Op olistT).
Proof.
intros [[|]]; rewrite /op /olist_op /=; [by simpl; rewrite decide_True|auto].
Qed.
Global Instance olist_op_assoc: Assoc equiv (op: Op olistT).
Proof.
intros [[l1|]] [[l2|]] [[l3|]]; eauto; rewrite {1}/op /olist_op; cbn.
- repeat (case_decide; auto); rewrite {1}/op /olist_op; cbn; do 2 f_equal.
+ case_decide; first by rewrite decide_True //.
destruct (prefix_weak_total l1 l2 l3); auto.
* naive_solver.
* by rewrite decide_True // decide_True //.
+ assert (l2 l1). { by etrans. } rewrite decide_False.
* by rewrite decide_True // decide_False // decide_True //.
* intros ?. assert (l1 l3). { by etrans. } naive_solver.
+ case_decide.
* assert (l1 l3). { by etrans. } naive_solver.
* case_decide; [|done]. rewrite decide_False // decide_False //.
+ rewrite decide_True // decide_False // decide_True //.
+ assert (l3 l1). { by etrans. }
rewrite decide_False // decide_True // decide_False //.
* by rewrite decide_True //.
* intros ?. assert (l2 l3). { by etrans. } naive_solver.
+ rewrite decide_False // decide_False //.
+ case_decide.
* rewrite decide_False // decide_False //.
* case_decide; [|done]. rewrite decide_False.
{ rewrite decide_False //. intros ?.
destruct (prefix_weak_total l2 l3 l1); auto. }
{ intros ?. assert (l2 l3). { by etrans. } naive_solver. }
- rewrite /op /olist_op; cbn. repeat case_decide; auto.
Qed.
Definition olist_ra_mixin : RAMixin olistT.
Proof.
apply ra_total_mixin; try apply _; try done.
- intros [[?|]] [[?|]] [[?|]]; eauto;
rewrite /op /olist_op /=; by inversion 1.
- by intros [[?|]] [[?|]].
- intros [[?|]] [[?|]]; eauto. rewrite /op /olist_op /=. do 2 f_equal.
case_decide; auto. case_decide; auto.
f_equal. by apply : (anti_symm prefix).
- intros. by rewrite idemp_L.
- by intros [[?|]] [[?|]].
Qed.
Canonical Structure olistR := discreteR olistT olist_ra_mixin.
Global Instance olistR_cmra_discrete : CmraDiscrete olistR.
Proof. apply discrete_cmra_discrete. Qed.
Instance olistR_unit : Unit olistT := to_olistT' nil.
Lemma olistT_ucmra_mixin : UcmraMixin olistT.
Proof. constructor; eauto; try done; by intros [[|]]. Qed.
Canonical Structure olistUR : ucmra := Ucmra olistT olistT_ucmra_mixin.
Global Instance of_olistT_inj : Inj () () (of_olistT).
Proof.
intros [[?|]] [[?|]]; simpl; try done; try by inversion 1.
inversion 1 as [?? Eq|]. rewrite -> leibniz_equiv_iff in Eq. by subst.
Qed.
Global Instance to_olistT_inj : Inj () () (to_olistT).
Proof. intros [?|] [?|]; simpl; try done. by inversion 1. Qed.
Lemma of_to_olistT (x : olist) : of_olistT (to_olistT x) = x.
Proof. done. Qed.
Lemma to_of_olistT (x : olistT) : to_olistT (of_olistT x) = x.
Proof. by destruct x. Qed.
Global Instance of_olistT_Proper : Proper (() ==> ()) (of_olistT).
Proof. intros [[?|]] [[?|]]; simpl; try done. by inversion 1. Qed.
Global Instance to_olistT_Proper : Proper (() ==> ()) (to_olistT).
Proof. solve_proper. Qed.
Global Instance olistT_core_id (x : olistT) : CoreId x.
Proof. by unfold CoreId. Qed.
Lemma olistT_equiv_iff (x y : olistT) : x y of_olistT x of_olistT y.
Proof. split; first by inversion 1. apply inj, _. Qed.
Global Instance olistT_leinbniz : LeibnizEquiv olistT.
Proof. intros [[?|]] [[?|]]; simpl; try done. by inversion 1. Qed.
Lemma olist_op_prefix l1 l2 :
l1 l2 to_olistT' l1 to_olistT' l2 = to_olistT' l2.
Proof. intros; rewrite /op /olist_op /=. f_equal. by rewrite decide_True. Qed.
Lemma olist_included l1 l2 : to_olistT' l1 to_olistT' l2 l1 l2.
Proof.
split.
- move => [[[?|]]]; cbn; last by inversion 1. rewrite /op /olist_op /=.
case_decide; first by (inversion 1; subst).
by case_decide; inversion 1.
- intros. exists (to_olistT' l2). by rewrite olist_op_prefix.
Qed.
Lemma olist_op_join (x y : olistT) (VL: x) :
of_olistT x of_olistT y x y = y.
Proof.
destruct x as [[x|]], y as [[y|]];
simpl; auto; intros; rewrite /op /olist_op /=.
- rewrite decide_True //.
- done.
Qed.
Lemma olistT_included (x y : olistT) (VLx: x) (VLy: y) :
x y of_olistT x of_olistT y.
Proof.
split=>[[z Eqy]|?].
- rewrite Eqy. move : Eqy.
destruct x as [[x|]], y as [[y|]], z as [[z|]]; simpl; try done.
case_decide.
+ rewrite olist_op_prefix //.
+ rewrite /op /olist_op /= decide_False //. case_decide; [done|inversion 1].
- exists y. by rewrite olist_op_join //.
Qed.
Lemma olistT_absorb (x y : olistT) (VLx: x) (VLy: y) :
x y x y x.
Proof.
split; first by move => <-; apply : cmra_included_r.
move => /(olistT_included _ _ VLy VLx) ?.
by rewrite comm olist_op_join.
Qed.
Lemma olistT_local_unit_update (x x' y : olistUR)
(Ext: of_olistT x of_olistT x') (VLx': x') (VLx: x) :
(x, y) ~l~> (x', x').
Proof.
apply local_update_unital_discrete => z Val Eq. split; [done|].
symmetry. apply olistT_absorb; [done|..].
- eapply cmra_valid_included; first exact VLx. exists y. by rewrite comm.
- etrans; last by apply olistT_included, Ext.
rewrite Eq. apply : cmra_included_r.
Qed.
Lemma olistT_local_unit_update' (l l': list A) y (Ext: l l') :
(to_olistT' l, y) ~l~> (to_olistT' l', to_olistT' l').
Proof. by apply olistT_local_unit_update. Qed.
Lemma olistT_valid_op l1 l2 :
(to_olistT' l1 to_olistT' l2) l1 l2 l2 l1.
Proof.
rewrite /op /olist_op /=. case_decide; first by left. case_decide; [by right|done].
Qed.
End list.
From iris.algebra Require Import auth gset gmap agree.
From iris.proofmode Require Import tactics.
From gpfsl.algebra Require Import to_agree.
From gpfsl.algebra Require Import to_agree mono_list.
From gpfsl.logic Require Import logatom atomics invariants.
From gpfsl.examples Require Import list_helper list_cmra.
From gpfsl.examples Require Import list_helper.
From gpfsl.logic Require Import repeat_loop new_delete.
From gpfsl.examples Require Import map_seq.
......@@ -43,7 +43,7 @@ Definition LinkState: Type := option node.
#[local] Notation msq_qmapUR' := (gmapUR gname (agreeR (leibnizO event_id))).
#[local] Notation msq_qmapUR := (authUR msq_qmapUR').
(* an append-only list of nodes *)
#[local] Notation msq_linkUR := (authUR $ (olistUR node)).
#[local] Notation msq_linkUR := (mono_listUR (leibnizO node)).
#[local] Notation msq_queueR := (prodR (prodUR msq_linkUR msq_linkUR) msq_qmapUR).
Class msqueueG Σ := MSQueueG {
......@@ -409,19 +409,24 @@ Definition LTM_snapv γq T : vProp := ⎡ LTM_snap γq T ⎤.
Definition LTM_ssnap γq η e : iProp := LTM_snap γq {[η := e]}.
Definition LTM_ssnapv γq η e : vProp := LTM_ssnap γq η e .
Definition LEL_snap γq L : iProp := own γq (LEGhost ( to_olistT' L)).
Definition LEL_snap γq L : iProp :=
own γq (LEGhost (ML (L : listO (leibnizO node)))).
Definition LEL_snapv γq L : vProp := LEL_snap γq L .
Definition LDL_snap γq D : iProp := own γq (LDGhost ( to_olistT' D)).
Definition LDL_snap γq D : iProp :=
own γq (LDGhost (ML (D : listO (leibnizO node)))).
Definition LDL_snapv γq D : vProp := LDL_snap γq D .
(* LTM_master and LEL_master track the enqueues *)
Definition LTM_master γq T : iProp := own γq (LTGhost ( (to_agreeM T))).
Definition LTM_auth T : msq_qmapUR := (to_agreeM T) (to_agreeM T).
Definition LTM_master γq T : iProp := own γq (LTGhost (LTM_auth T)).
Definition LTM_masterv γq T : vProp := LTM_master γq T .
Definition LEL_master γq L : iProp := own γq (LEGhost ( (to_olistT' L))).
Definition LEL_master γq L : iProp :=
own γq (LEGhost (ML ((L : listO (leibnizO node))))).
Definition LEL_masterv γq L : vProp := LEL_master γq L .
(* LDL_master track the dequeues *)
Definition LDL_master γq D : iProp := own γq (LDGhost ( (to_olistT' D))).
Definition LDL_master γq D : iProp :=
own γq (LDGhost (ML ((D : listO (leibnizO node))))).
Definition LDL_masterv γq D : vProp := LDL_master γq D .
End ghost.
......@@ -1146,15 +1151,16 @@ Lemma Maps_master_alloc CL D T :
|==> γ, LEL_master γ CL LDL_master γ D LTM_master γ T.
Proof.
do 2 setoid_rewrite <-own_op. apply own_alloc.
rewrite /= -!pair_op /= !left_id !right_id.
split; first split; apply auth_auth_valid; by eauto using to_agreeM_valid.
rewrite /= -!pair_op /= !left_id !right_id !pair_valid.
split; [split; apply mono_list_auth_valid|].
apply auth_both_valid_discrete. split; [done|apply to_agreeM_valid].
Qed.
(* lnode-event_id map T *)
Lemma LTM_master_snap_included γ T T' :
LTM_master γ T - LTM_snap γ T' - T' T.
Proof.
iIntros "o1 o2".
iIntros "[o1 ?] o2".
iDestruct (own_valid_2 with "o1 o2") as %[_ [INCL _]%auth_both_valid_discrete].
iPureIntro. by move : INCL => /to_agreeM_included.
Qed.
......@@ -1164,18 +1170,27 @@ Proof.
iIntros "LTm VMs". by iDestruct (LTM_master_snap_included with "LTm VMs")
as %SUB%map_singleton_subseteq_l.
Qed.
Lemma LTM_update γ T T' (SUB: T T'):
LTM_master γ T == LTM_master γ T' LTM_snap γ T'.
Proof.
rewrite -own_op -2!pair_op !left_id.
apply own_update, prod_update; [done|].
by apply auth_update_alloc, to_agreeM_local_update.
Qed.
Lemma LTM_snap_sub γ T T' (Le: T T') : LTM_snap γ T' LTM_snap γ T.
Proof.
apply own_mono, prod_included. split; [done|]. simpl.
by apply auth_frag_mono, to_agreeM_included.
Qed.
Lemma LTM_master_fork γ T : LTM_master γ T LTM_snap γ T.
Proof. by iIntros "[? $]". Qed.
Lemma LTM_update' γ T T' (SUB: T T') :
LTM_master γ T == LTM_master γ T'.
Proof.
apply own_update, prod_update; [done|]. simpl.
by apply auth_update, to_agreeM_local_update.
Qed.
Lemma LTM_update γ T T' (SUB: T T') :
LTM_master γ T == LTM_master γ T' LTM_snap γ T'.
Proof.
iIntros "T". iMod (LTM_update' _ _ _ SUB with "T") as "T".
iDestruct (LTM_master_fork with "T") as "#$". by iFrame.
Qed.
Lemma LTM_update_insert γ T η eid (FR: η dom (gset lnode) T):
LTM_master γ T == LTM_master γ (<[η := eid]>T) LTM_ssnap γ η eid.
Proof.
......@@ -1185,72 +1200,81 @@ Proof.
iIntros "!>". iApply (LTM_snap_sub with "Snap").
by apply insert_mono, gmap_subseteq_empty.
Qed.
Lemma LTM_master_fork γ T :
LTM_master γ T == LTM_master γ T LTM_snap γ T.
Proof. by apply LTM_update. Qed.
(* Authoritative complete list L *)
Lemma LEL_update γ L L' (SUB: L L'):
LEL_master γ L == LEL_master γ L' LEL_snap γ L'.
Proof.
rewrite -own_op -2!pair_op !left_id.
apply own_update, prod_update; [|done]. apply prod_update; [|done]. simpl.
by apply auth_update_alloc, olistT_local_unit_update'.
Qed.
Lemma LEL_update_app γ L L':
LEL_master γ L == LEL_master γ (L ++ L') LEL_snap γ (L ++ L').
Lemma LEL_master_snap_included γ L L' :
LEL_master γ L - LEL_snap γ L' - L' L.
Proof.
apply LEL_update. rewrite -{1}(app_nil_r L). by apply prefix_app, prefix_nil.
iIntros "o1 o2". by iDestruct (own_valid_2 with "o1 o2")
as %[[?%mono_list_both_valid_L _] _].
Qed.
Lemma LEL_snap_sub γ L L' (Le: L L') : LEL_snap γ L' LEL_snap γ L.
Proof.
apply own_mono, prod_included. split; [|done].
apply prod_included. split; [|done]. simpl.
by apply auth_frag_mono, olist_included.
apply prod_included. split; [|done]. simpl. by apply mono_list_lb_mono.
Qed.
Lemma LEL_master_fork γ L :
LEL_master γ L == LEL_master γ L LEL_snap γ L.
LEL_master γ L LEL_snap γ L.
Proof.
rewrite -own_op -2!pair_op !left_id. apply own_update, prod_update; [|done].
apply prod_update; [|done]. apply auth_update_dfrac_alloc; [by apply _|done].
apply own_mono, prod_included. split; [|done].
apply prod_included. split; [|done]. simpl. by apply mono_list_included.
Qed.
Lemma LEL_master_snap_included γ L L' :
LEL_master γ L - LEL_snap γ L' - L' L.
Lemma LEL_update' γ L L' (SUB: L L') :
LEL_master γ L == LEL_master γ L'.
Proof.
iIntros "o1 o2". by iDestruct (own_valid_2 with "o1 o2")
as %[[[?%olist_included _]%auth_both_valid_discrete _] _].
apply own_update, prod_update; [|done]. apply prod_update; [|done]. simpl.
by apply mono_list_update.
Qed.
(* Dequeued list D *)
Lemma LDL_update γ D D' (SUB: D D'):
LDL_master γ D == LDL_master γ D' LDL_snap γ D'.
Lemma LEL_update γ L L' (SUB: L L') :
LEL_master γ L == LEL_master γ L' LEL_snap γ L'.
Proof.
rewrite -own_op -2!pair_op !left_id.
apply own_update, prod_update; [|done]. apply prod_update; [done|]. simpl.
by apply auth_update_alloc, olistT_local_unit_update'.
iIntros "L". iMod (LEL_update' _ _ _ SUB with "L") as "L".
iDestruct (LEL_master_fork with "L") as "#$". by iFrame.
Qed.
Lemma LDL_update_app γ D D':
LDL_master γ D == LDL_master γ (D ++ D') LDL_snap γ (D ++ D').
Lemma LEL_update_app γ L L':
LEL_master γ L == LEL_master γ (L ++ L') LEL_snap γ (L ++ L').
Proof.
apply LDL_update. rewrite -{1}(app_nil_r D). by apply prefix_app, prefix_nil.
apply LEL_update. rewrite -{1}(app_nil_r L). by apply prefix_app, prefix_nil.
Qed.
(* Dequeued list D *)
Lemma LDL_master_snap_included γ D D' :
LDL_master γ D - LDL_snap γ D' - D' D.
Proof.
iIntros "o1 o2". by iDestruct (own_valid_2 with "o1 o2")
as %[[_ ?%mono_list_both_valid_L] _].
Qed.
Lemma LDL_snap_sub γ D D' (Le: D D') : LDL_snap γ D' LDL_snap γ D.
Proof.
apply own_mono, prod_included. split; [|done].
apply prod_included. split; [done|]. simpl.
by apply auth_frag_mono, olist_included.
apply prod_included. split; [done|]. simpl. by apply mono_list_lb_mono.
Qed.
Lemma LDL_master_fork γ D :
LDL_master γ D == LDL_master γ D LDL_snap γ D.
LDL_master γ D LDL_snap γ D.
Proof.
rewrite -own_op -2!pair_op !left_id. apply own_update, prod_update; [|done].
apply prod_update; [done|]. apply auth_update_dfrac_alloc; [by apply _|done].
apply own_mono, prod_included. split; [|done].
apply prod_included. split; [done|]. simpl. by apply mono_list_included.
Qed.
Lemma LDL_master_snap_included γ D D' :
LDL_master γ D - LDL_snap γ D' - D' D.
Lemma LDL_update' γ D D' (SUB: D D') :
LDL_master γ D == LDL_master γ D'.
Proof.
iIntros "o1 o2". by iDestruct (own_valid_2 with "o1 o2")
as %[[_ [?%olist_included _]%auth_both_valid_discrete] _].
apply own_update, prod_update; [|done]. apply prod_update; [done|]. simpl.
by apply mono_list_update.
Qed.
Lemma LDL_update γ D D' (SUB: D D') :
LDL_master γ D == LDL_master γ D' LDL_snap γ D'.
Proof.
iIntros "D". iMod (LDL_update' _ _ _ SUB with "D") as "D".
iDestruct (LDL_master_fork with "D") as "#$". by iFrame.
Qed.
Lemma LDL_update_app γ D D':
LDL_master γ D == LDL_master γ (D ++ D') LDL_snap γ (D ++ D').
Proof.
apply LDL_update. rewrite -{1}(app_nil_r D). by apply prefix_app, prefix_nil.
Qed.
End ghost_rules.
......@@ -1304,17 +1328,15 @@ Proof.
Qed.
Lemma QueueInv_no_exist_snapshot γg q G γ γh γl η s D L T :
QueueInv_no_exist γg q G γ γh γl η s D L T ==
QueueInv_no_exist γg q G γ γh γl η s D L T
QueueInv_no_exist γg q G γ γh γl η s D L T
LEL_snapv γ ((η,s) :: D ++ L)
LDL_snapv γ D
LTM_snapv γ T.
Proof.
iDestruct 1 as "(LEL & LD & LT & ?)".
iMod (LEL_master_fork with "LEL") as "[LEL $]".
iMod (LDL_master_fork with "LD") as "[LD $]".
iMod (LTM_master_fork with "LT") as "[LT $]".
iIntros "!>". rewrite /QueueInv_no_exist. by iFrame.
iDestruct (LEL_master_fork with "LEL") as "$".
iDestruct (LDL_master_fork with "LD") as "$".
by iDestruct (LTM_master_fork with "LT") as "$".
Qed.
Lemma QueueInv_no_exist_QueueLocs_access γg q G γ γh γl η s D L T :
......@@ -1395,7 +1417,7 @@ Proof.
(* get a snapshot *)
iDestruct (graph_master_snap with "GM") as "#GS0".
iMod (QueueInv_no_exist_snapshot with "QBI") as "(QBI & #LS & _ & #LTs)".
iDestruct (QueueInv_no_exist_snapshot with "QBI") as "#(LS & _ & LTs)".
(* get Tail *)
iDestruct (QueueInv_no_exist_tail_immut_access with "QBI")
......@@ -1439,7 +1461,7 @@ Proof.
(* get another snapshot *)
iDestruct (graph_master_snap with "GM") as "#GS1".
iMod (QueueInv_no_exist_snapshot with "QBI") as "(QBI & #LS1 & _ & #LT1)".
iDestruct (QueueInv_no_exist_snapshot with "QBI") as "#(LS1 & _ & LT1)".
(* get permission of η *)
set E1 := G1.(Es).
......@@ -1605,9 +1627,9 @@ Proof.
iMod (AtomicPtsTo_CON_from_na with "Hs") as (ηs ts Vs) "(#sVs & #SNs & ATs)".
(* allocate ghost graphs *)
iMod (Maps_master_alloc [(ηs,s)] [] ) as (γ) "(LELm & LDLm & LTm)".
iMod (LEL_master_fork with "LELm") as "[LELm #LELs]".
iMod (LDL_master_fork with "LDLm") as "[LDLm #LDLs]".
iMod (LTM_master_fork with "LTm") as "[LTm #LTs]".
iDestruct (LEL_master_fork with "LELm") as "#LELs".
iDestruct (LDL_master_fork with "LDLm") as "#LDLs".
iDestruct (LTM_master_fork with "LTm") as "#LTs".
iMod graph_master_alloc_empty as (γg) "([GM1 GM2] & #Gs)".
iAssert (link_val ηs s Vs 0) as "#LVs0".
......@@ -1767,17 +1789,17 @@ Proof.
iDestruct "F" as %(-> & NEq & ->).
iDestruct (graph_master_snap with "GM") as "#Gs'".
iMod (LEL_master_fork with "LM") as "[LM Ls']".
iMod (LDL_master_fork with "LD") as "[LD LD']".
iMod (LTM_master_fork with "LTm") as "[LTm LTs']".
iDestruct (LEL_master_fork with "LM") as "#Ls'".
iDestruct (LDL_master_fork with "LD") as "#LD'".
iDestruct (LTM_master_fork with "LTm") as "#LTs'".
assert (SYE2 := SyncEnqueues_mono _ _ _ SubD1 InE1 SYE1).
(* Close without updating. TODO: can be more a interesting FAIL *)
rewrite bi.and_elim_r.
iMod ("HClose" $! false V'' G2 dummy_eid dummy_qevt Venq M
with "[GM' Gs' Ls' LD' LTs']") as "HΦ".
with "[GM']") as "HΦ {Gs' Ls' LD' LTs'}".
{ iSplitL "GM'". { iNext. iFrame (CON) "GM'". }
iFrame "SnV''". iSplitL; [|by iPureIntro]. iSplitL "Gs'".
iFrame "SnV''". iSplitL; [|by iPureIntro]. iSplit.
{ iDestruct "Gs'" as "[$ _]". iFrame "PSV". }
iExists γ, γh, γl. iFrame "QII". iExists ηs, s, D2, L2, D0, T2.
iSplit. { iPureIntro. by etrans. }
......@@ -1840,7 +1862,6 @@ Proof.
iMod ("oD" with "oL") as (η tn Vn FRη) "(%LeVn & oD & #SNn & ATn)".
rewrite ->elem_of_list_to_set in FRη. rewrite view_at_view_at.
set Mη' : gset event_id :=
if T2 !! η' is Some e'
then if E2 !! e' is Some eV' then eV'.(ge_lview) else
......@@ -1907,8 +1928,8 @@ Proof.
iMod (LTM_update_insert _ _ η enqId FRηT with "LTm") as "[LTm' #LTs']".
iMod (LEL_update_app _ _ [(η,n)] with "LM") as "[LM #LS']". rewrite -EqCL2'.