diff --git a/README.md b/README.md
index e890844b5a7129415186ede5efa0b9cf7cb1fb71..3db18f2fcf54fd7ade4cfe0b2dba4391be0ab6ea 100644
--- a/README.md
+++ b/README.md
@@ -44,6 +44,8 @@ This repository contains the following case studies:
* Binary logical relations for proving contextual refinements
- Proof of refinement for a pair of fine-grained/coarse-grained concurrent counter implementations
- Proof of refinement for a pair of fine-grained/coarse-grained concurrent stack implementations
+* [spanning-tree](theories/spanning_tree): Proof of partial functional
+ correctness of a concurrent spanning tree algorithm.
## For Developers: How to update the Iris dependency
diff --git a/_CoqProject b/_CoqProject
index 5d8f4075f5f4e8bfb8767168c1f118b2a9456488..fca71553a94a302343f6b62863da91331436b197 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -48,3 +48,8 @@ theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
+
+theories/spanning_tree/graph.v
+theories/spanning_tree/mon.v
+theories/spanning_tree/spanning.v
+theories/spanning_tree/proof.v
diff --git a/theories/spanning_tree/graph.v b/theories/spanning_tree/graph.v
new file mode 100644
index 0000000000000000000000000000000000000000..b48efab4bd31332625b4bfc3261103398bc5d108
--- /dev/null
+++ b/theories/spanning_tree/graph.v
@@ -0,0 +1,114 @@
+From iris.algebra Require Import base gmap.
+From stdpp Require Import gmap mapset.
+
+Section Graphs.
+ Context {T : Type} {HD : EqDecision T} {HC : @Countable T HD}.
+
+ Definition graph := gmap T (option T * option T).
+
+ Identity Coercion graph_to_gmap : graph >-> gmap.
+
+ Definition get_left (g : graph) x : option T := g !! x ≫= fst.
+ Definition get_right (g : graph) x : option T := g !! x ≫= snd.
+
+ Definition strict_sub_child (ch ch' : option T) :=
+ match ch, ch' with
+ | Some c, Some c' => c = c'
+ | Some c, None => True
+ | None, Some _ => False
+ | None, None => True
+ end.
+
+ Definition strict_sub_children (ch ch' : option T * option T) : Prop :=
+ strict_sub_child (ch.1) (ch'.1) ∧ strict_sub_child (ch.2) (ch'.2).
+
+ Definition strict_subgraph (g g' : graph) : Prop :=
+ ∀ x, strict_sub_children (get_left g x, get_right g x)
+ (get_left g' x, get_right g' x).
+
+(* A path is a list of booleans true for left child and false for the right *)
+(* The empty list is the identity trace (from x to x). *)
+ Definition path := list bool.
+
+ Identity Coercion path_to_list : path >-> list.
+
+ Inductive valid_path (g : graph) (x y : T) : path → Prop :=
+ | valid_path_E : x ∈ dom (gset _) g → x = y → valid_path g x y []
+ | valid_path_l (xl : T) p : get_left g x = Some xl → valid_path g xl y p →
+ valid_path g x y (true :: p)
+ | valid_path_r (xr : T) p : get_right g x = Some xr → valid_path g xr y p →
+ valid_path g x y (false :: p).
+
+ Definition connected (g : graph) (x : T) :=
+ ∀ z, z ∈ dom (gset _) g → ∃ p, valid_path g x z p.
+
+ Definition front (g : graph) (t t' : gset T) := t ⊆ dom (gset _) g ∧
+ ∀ x v, x ∈ t → (get_left g x = Some v) ∨ (get_right g x = Some v) →
+ v ∈ t'.
+
+ Definition maximal (g : graph) := front g (dom (gset _) g) (dom (gset _) g).
+
+ Definition tree (g : graph) (x : T) :=
+ ∀ z, z ∈ dom (gset _) g → exists !p, valid_path g x z p.
+
+ (* graph facts *)
+
+ Lemma front_t_t_dom g z t :
+ z ∈ t → connected g z → front g t t → t = dom (gset _) g.
+ Proof.
+ intros Hz Hc [Hsb Hdt].
+ apply collection_equiv_spec_L; split; trivial.
+ apply elem_of_subseteq => x Hx. destruct (Hc x Hx) as [p pv].
+ clear Hc Hx; revert z Hz pv.
+ induction p => z Hz pv.
+ - by inversion pv; subst.
+ - inversion pv as [|? ? Hpv1 Hpv2 Hpv3|? ? Hpv1 Hpv2 Hpv3]; subst.
+ + eapply IHp; [eapply Hdt|apply Hpv2]; eauto.
+ + eapply IHp; [eapply Hdt|apply Hpv2]; eauto.
+ Qed.
+
+ Lemma front_mono g t t' s : front g t t' → t' ⊆ s → front g t s.
+ Proof. intros [Htd Hf] Hts; split; eauto. Qed.
+
+ Lemma front_empty g : front g ∅ ∅.
+ Proof. split; auto. intros ? Hcn; inversion Hcn. Qed.
+
+ Lemma strict_sub_children_refl v : strict_sub_children v v.
+ Proof. by destruct v as [[] []]. Qed.
+
+ Lemma strict_sub_children_trans v1 v2 v3 : strict_sub_children v1 v2 →
+ strict_sub_children v2 v3 → strict_sub_children v1 v3.
+ Proof.
+ destruct v1 as [[] []]; destruct v2 as [[] []];
+ destruct v3 as [[] []]; cbv; by intuition subst.
+ Qed.
+
+ Lemma strict_sub_children_None v : strict_sub_children v (None, None).
+ Proof. by destruct v as[[] []]. Qed.
+
+ Lemma strict_subgraph_empty g : strict_subgraph g ∅.
+ Proof.
+ intros i.
+ rewrite /get_left /get_right /strict_sub_child lookup_empty //=.
+ by destruct (g !! i) as [[[] []]|].
+ Qed.
+
+ Lemma get_left_dom g x y : get_left g x = Some y → x ∈ dom (gset _) g.
+ Proof.
+ rewrite /get_left elem_of_dom. case _ : (g !! x); inversion 1; eauto.
+ Qed.
+
+ Lemma get_right_dom g x y : get_right g x = Some y → x ∈ dom (gset _) g.
+ Proof.
+ rewrite /get_right elem_of_dom. case _ : (g !! x); inversion 1; eauto.
+ Qed.
+
+ Lemma path_start g x y p : valid_path g x y p → x ∈ dom (gset _) g.
+ Proof. inversion 1; subst; eauto using get_left_dom, get_right_dom. Qed.
+
+ Lemma path_end g x y p : valid_path g x y p → y ∈ dom (gset _) g.
+ Proof. induction 1; subst; eauto. Qed.
+
+End Graphs.
+
+Arguments graph _ {_ _}.
\ No newline at end of file
diff --git a/theories/spanning_tree/mon.v b/theories/spanning_tree/mon.v
new file mode 100644
index 0000000000000000000000000000000000000000..df249ab3b5f19db6109d10bef7fb66ccfcfc437a
--- /dev/null
+++ b/theories/spanning_tree/mon.v
@@ -0,0 +1,784 @@
+From iris.heap_lang Require Export lifting notation.
+From iris.algebra Require Import auth frac gset gmap excl.
+From iris.base_logic Require Export invariants.
+From iris.proofmode Require Import tactics.
+Import uPred.
+
+From iris.base_logic Require Import cancelable_invariants.
+
+From stdpp Require Import gmap mapset.
+
+From iris_examples.spanning_tree Require Import graph.
+
+(* children cofe *)
+Canonical Structure chlC := leibnizC (option loc * option loc).
+(* The graph monoid. *)
+Definition graphN : namespace := nroot .@ "SPT_graph".
+Definition graphUR : ucmraT :=
+ optionUR (prodR fracR (gmapR loc (exclR chlC))).
+(* The monoid for talking about which nodes are marked.
+These markings are duplicatable. *)
+Definition markingUR : ucmraT := gsetUR loc.
+
+(** The CMRA we need. *)
+Class graphG Σ := GraphG
+ {
+ graph_marking_inG :> inG Σ (authR markingUR);
+ graph_marking_name : gname;
+ graph_inG :> inG Σ (authR graphUR);
+ graph_name : gname
+ }.
+(** The Functor we need. *)
+(*Definition graphΣ : gFunctors := #[authΣ graphUR].*)
+
+Section marking_definitions.
+ Context `{irisG heap_lang Σ, graphG Σ}.
+
+ Definition is_marked (l : loc) : iProp Σ :=
+ own graph_marking_name (â—¯ {[ l ]}).
+
+ Global Instance marked_persistentP x : Persistent (is_marked x).
+ Proof. apply _. Qed.
+
+ Lemma dup_marked l : is_marked l ⊣⊢ is_marked l ∗ is_marked l.
+ Proof. by rewrite /is_marked -own_op -auth_frag_op idemp_L. Qed.
+
+ Lemma new_marked {E} (m : markingUR) l :
+ own graph_marking_name (◠m) ={E}=∗
+ own graph_marking_name (◠(m ⋅ ({[l]} : gset loc))) ∗ is_marked l.
+ Proof.
+ iIntros "H". rewrite -own_op (comm _ m).
+ iMod (@own_update with "H") as "Y"; eauto.
+ apply auth_update_alloc.
+ setoid_replace ({[l]} : gset loc) with (({[l]} : gset loc) ⋅ ∅) at 2
+ by (by rewrite right_id).
+ apply op_local_update_discrete; auto.
+ Qed.
+
+ Lemma already_marked {E} (m : gset loc) l : l ∈ m →
+ own graph_marking_name (◠m) ={E}=∗
+ own graph_marking_name (◠m) ∗ is_marked l.
+ Proof.
+ iIntros (Hl) "Hm". iMod (new_marked with "Hm") as "[H1 H2]"; iFrame.
+ rewrite gset_op_union (comm _ m) (subseteq_union_1_L {[l]} m); trivial.
+ by apply elem_of_subseteq_singleton.
+ Qed.
+
+End marking_definitions.
+
+(* The monoid representing graphs *)
+Definition Gmon := gmapR loc (exclR chlC).
+
+Definition excl_chlC_chl (ch : exclR chlC) : option (option loc * option loc) :=
+ match ch with
+ | Excl w => Some w
+ | Excl_Bot => None
+ end.
+
+Definition Gmon_graph (G : Gmon) : graph loc := omap excl_chlC_chl G.
+
+Definition Gmon_graph_dom (G : Gmon) :
+ ✓ G → dom (gset loc) (Gmon_graph G) = dom (gset _) G.
+Proof.
+ intros Hvl; apply mapset_eq => i. rewrite ?elem_of_dom lookup_omap.
+ specialize (Hvl i). split.
+ - revert Hvl; case _ : (G !! i) => [[]|] //=; eauto.
+ intros _ [? Hgi]; inversion Hgi.
+ - intros Hgi; revert Hgi Hvl. intros [[] Hgi]; rewrite Hgi; inversion 1; eauto.
+Qed.
+
+Definition child_to_val (c : option loc) : val :=
+ match c with
+ | None => NONEV
+ | Some l => SOMEV #l
+ end.
+
+(* convert the data of a node to a value in the heap *)
+Definition children_to_val (ch : option loc * option loc) : val :=
+ (child_to_val (ch.1), child_to_val (ch.2)).
+
+Lemma children_to_val_is_val (c c' : option loc) :
+ to_val (child_to_val c, child_to_val c') =
+ Some (child_to_val c, child_to_val c')%V.
+Proof. by destruct c; destruct c'. Qed.
+
+Definition marked_graph := gmap loc (bool * (option loc * option loc)).
+Identity Coercion marked_graph_gmap: marked_graph >-> gmap.
+
+Definition of_graph_elem (G : Gmon) i v
+ : option (bool * (option loc * option loc)) :=
+ match Gmon_graph G !! i with
+ | Some w => Some (true, w)
+ | None => Some (false,v)
+ end.
+
+Definition of_graph (g : graph loc) (G : Gmon) : marked_graph :=
+ map_imap (of_graph_elem G) g.
+
+(* facts *)
+
+Global Instance Gmon_graph_proper : Proper ((≡) ==> (=)) Gmon_graph.
+Proof. solve_proper. Qed.
+
+Lemma new_Gmon_dom (G : Gmon) x w :
+ dom (gset loc) (G ⋅ {[x := w]}) = dom (gset loc) G ∪ {[x]}.
+Proof. by rewrite dom_op dom_singleton_L. Qed.
+
+Definition of_graph_empty (g : graph loc) :
+ of_graph g ∅ = fmap (λ x, (false, x)) g.
+Proof.
+ apply: map_eq => i.
+ rewrite lookup_imap /of_graph_elem lookup_fmap lookup_omap //.
+Qed.
+
+Lemma of_graph_dom_eq g G :
+ ✓ G → dom (gset loc) g = dom (gset loc) (Gmon_graph G) →
+ of_graph g G = fmap (λ x, (true, x) )(Gmon_graph G).
+Proof.
+ intros HGvl. rewrite Gmon_graph_dom // => Hd. apply map_eq => i.
+ assert (Hd' : i ∈ dom (gset _) g ↔ i ∈ dom (gset _) G) by (by rewrite Hd).
+ revert Hd'; clear Hd. specialize (HGvl i); revert HGvl.
+ rewrite /of_graph /of_graph_elem /Gmon_graph lookup_imap lookup_fmap
+ lookup_omap ?elem_of_dom.
+ case _ : (g !! i); case _ : (G !! i) => [[]|] /=; inversion 1; eauto;
+ intros [? ?];
+ match goal with
+ H : _ → @is_Some ?A None |- _ =>
+ assert (Hcn : @is_Some A None) by eauto;
+ destruct Hcn as [? Hcn]; inversion Hcn
+ end.
+Qed.
+
+Section definitions.
+ Context `{heapG Σ, graphG Σ}.
+
+ Definition own_graph (q : frac) (G : Gmon) : iProp Σ :=
+ own graph_name (â—¯ (Some (q, G) : graphUR)).
+
+ Global Instance own_graph_proper q : Proper ((≡) ==> (⊣⊢)) (own_graph q).
+ Proof. solve_proper. Qed.
+
+ Definition heap_owns (M : marked_graph) (markings : gmap loc loc) : iProp Σ :=
+ ([∗ map] l ↦ v ∈ M, ∃ (m : loc), ⌜markings !! l = Some mâŒ
+ ∗ l ↦ (#m, children_to_val (v.2)) ∗ m ↦ #(LitBool (v.1)))%I.
+
+ Definition graph_inv (g : graph loc) (markings : gmap loc loc) : iProp Σ :=
+ (∃ (G : Gmon), own graph_name (◠Some (1%Qp, G))
+ ∗ own graph_marking_name (◠dom (gset _) G)
+ ∗ heap_owns (of_graph g G) markings ∗ ⌜strict_subgraph g (Gmon_graph G)âŒ
+ )%I.
+
+ Global Instance graph_inv_timeless g Mrk : Timeless (graph_inv g Mrk).
+ Proof. apply _. Qed.
+
+ Context `{cinvG Σ}.
+ Definition graph_ctx κ g Mrk : iProp Σ := cinv graphN κ (graph_inv g Mrk).
+
+ Global Instance graph_ctx_persistent κ g Mrk : Persistent (graph_ctx κ g Mrk).
+ Proof. apply _. Qed.
+
+End definitions.
+
+Notation "l [↦] v" := ({[l := Excl v]}) (at level 70, format "l [↦] v").
+
+Typeclasses Opaque graph_ctx graph_inv own_graph.
+
+Section graph_ctx_alloc.
+ Context `{heapG Σ, cinvG Σ, inG Σ (authR markingUR), inG Σ (authR graphUR)}.
+
+ Lemma graph_ctx_alloc (E : coPset) (g : graph loc) (markings : gmap loc loc)
+ (HNE : (nclose graphN) ⊆ E)
+ : ([∗ map] l ↦ v ∈ g, ∃ (m : loc), ⌜markings !! l = Some mâŒ
+ ∗ l ↦ (#m, children_to_val v) ∗ m ↦ #false)
+ ={E}=∗ ∃ (Ig : graphG Σ) (κ : gname), cinv_own κ 1 ∗ graph_ctx κ g markings
+ ∗ own_graph 1%Qp ∅.
+ Proof.
+ iIntros "H1".
+ iMod (own_alloc (◠(∅ : markingUR))) as (mn) "H2"; first done.
+ iMod (own_alloc (◠(Some (1%Qp, ∅ : Gmon) : graphUR)
+ ⋅ ◯ (Some (1%Qp, ∅ : Gmon) : graphUR))) as (gn) "H3".
+ { done. }
+ iDestruct "H3" as "[H31 H32]".
+ set (Ig := GraphG _ _ mn _ gn).
+ iExists Ig.
+ iAssert (graph_inv g markings) with "[H1 H2 H31]" as "H".
+ { unfold graph_inv. iExists ∅. rewrite dom_empty_L. iFrame "H2 H31".
+ iSplitL; [|iPureIntro].
+ - rewrite /heap_owns of_graph_empty big_sepM_fmap; eauto.
+ - rewrite /Gmon_graph omap_empty; apply strict_subgraph_empty. }
+ iMod (cinv_alloc _ graphN with "[H]") as (κ) "[Hinv key]".
+ { iNext. iExact "H". }
+ iExists κ.
+ rewrite /own_graph /graph_ctx //=; by iFrame.
+ Qed.
+
+End graph_ctx_alloc.
+
+Lemma marked_was_unmarked (G : Gmon) x v :
+ ✓ ({[x := Excl v]} ⋅ G) → G !! x = None.
+Proof.
+ intros H2; specialize (H2 x).
+ revert H2; rewrite lookup_op lookup_singleton. intros H2.
+ by rewrite (excl_validN_inv_l O _ _ (proj1 (cmra_valid_validN _) H2 O)).
+Qed.
+
+Lemma mark_update_lookup_base (G : Gmon) x v :
+ ✓ ({[x := Excl v]} ⋅ G) → ({[x := Excl v]} ⋅ G) !! x = Some (Excl v).
+Proof.
+ intros H2; rewrite lookup_op lookup_singleton.
+ erewrite marked_was_unmarked; eauto.
+Qed.
+
+Lemma mark_update_lookup_ne_base (G : Gmon) x i v :
+ i ≠x → ({[x := Excl v]} ⋅ G) !! i = G !! i.
+Proof. intros H. by rewrite lookup_op lookup_singleton_ne //= left_id_L. Qed.
+
+Lemma of_graph_dom g G : dom (gset loc) (of_graph g G) = dom (gset _) g.
+Proof.
+ apply mapset_eq=>i.
+ rewrite ?elem_of_dom lookup_imap /of_graph_elem lookup_omap.
+ case _ : (g !! i) => [x|]; case _ : (G !! i) => [[]|] //=; split;
+ intros [? Hcn]; inversion Hcn; eauto.
+Qed.
+
+Lemma in_dom_of_graph (g : graph loc) (G : Gmon) x (b : bool) v :
+ ✓ G → of_graph g G !! x = Some (b, v) → b ↔ x ∈ dom (gset _) G.
+Proof.
+ rewrite /of_graph /of_graph_elem lookup_imap lookup_omap elem_of_dom.
+ intros Hvl; specialize (Hvl x); revert Hvl;
+ case _ : (g !! x) => [?|]; case _ : (G !! x) => [[] ?|] //=;
+ intros Hvl; inversion Hvl; try (inversion 1; subst); split;
+ try (inversion 1; fail); try (intros [? Hcn]; inversion Hcn; fail);
+ subst; eauto.
+Qed.
+
+Global Instance of_graph_proper g : Proper ((≡) ==> (=)) (of_graph g).
+Proof. solve_proper. Qed.
+
+
+Lemma mark_update_lookup (g : graph loc) (G : Gmon) x v :
+ x ∈ dom (gset loc) g →
+ ✓ ((x [↦] v) ⋅ G) → of_graph g ((x [↦] v) ⋅ G) !! x = Some (true, v).
+Proof.
+ rewrite elem_of_dom /is_Some. intros [w H1] H2.
+ rewrite /of_graph /of_graph_elem lookup_imap H1 lookup_omap; simpl.
+ rewrite mark_update_lookup_base; trivial.
+Qed.
+
+Lemma mark_update_lookup_ne (g : graph loc) (G : Gmon) x i v :
+ i ≠x → of_graph g ((x [↦] v) ⋅ G) !! i = (of_graph g G) !! i.
+Proof.
+ intros H. rewrite /of_graph /of_graph_elem ?lookup_imap ?lookup_omap; simpl.
+ rewrite mark_update_lookup_ne_base //=.
+Qed.
+
+Section graph.
+ Context `{heapG Σ, graphG Σ}.
+
+ Lemma own_graph_valid q G : own_graph q G ⊢ ✓ G.
+ Proof.
+ iIntros "H". unfold own_graph.
+ by iDestruct (own_valid with "H") as %[_ ?].
+ Qed.
+
+ Lemma auth_own_graph_valid q G : own graph_name (◠Some (q, G)) ⊢ ✓ G.
+ Proof.
+ iIntros "H". unfold own_graph.
+ by iDestruct (own_valid with "H") as %[_ [_ ?]].
+ Qed.
+
+ Lemma whole_frac (G G' : Gmon):
+ own graph_name (â— Some (1%Qp, G)) ∗ own_graph 1 G' ⊢ ⌜G = G'âŒ.
+ Proof.
+ iIntros "[H1 H2]". rewrite /own_graph.
+ iCombine "H1" "H2" as "H".
+ iDestruct (own_valid with "H") as %[H1 H2]; cbn in *.
+ iPureIntro.
+ specialize (H1 O).
+ apply cmra_discrete_included_iff in H1.
+ apply option_included in H1; destruct H1 as [H1|H1]; [inversion H1|].
+ destruct H1 as (u1 & u2 & Hu1 & Hu2 & H3);
+ inversion Hu1; inversion Hu2; subst.
+ destruct H3 as [[_ H31%leibniz_equiv]|H32]; auto.
+ inversion H32 as [[q x] H4].
+ inversion H4 as [H41 H42]; simpl in *.
+ assert (✓ (1 ⋅ q)%Qp) by (rewrite -H41; done).
+ exfalso; eapply exclusive_l; eauto; typeclasses eauto.
+ Qed.
+
+ Lemma graph_divide q G G' :
+ own_graph q (G ⋅ G') ⊣⊢ own_graph (q / 2) G ∗ own_graph (q / 2) G'.
+ Proof.
+ replace q with ((q / 2) + (q / 2))%Qp at 1 by (by rewrite Qp_div_2).
+ by rewrite /own_graph -own_op.
+ Qed.
+
+ Lemma mark_graph {E} (G : Gmon) q x w : G !! x = None →
+ own graph_name (◠Some (1%Qp, G)) ∗ own_graph q ∅
+ ={E}=∗
+ own graph_name (◠Some (1%Qp, {[x := Excl w]} ⋅ G)) ∗ own_graph q (x [↦] w).
+ Proof.
+ iIntros (Hx) "H". rewrite -?own_op.
+ iMod (own_update with "H") as "H'"; eauto.
+ apply auth_update, option_local_update, prod_local_update;
+ first done; simpl.
+ rewrite -{2}[(x [↦] w)]right_id.
+ apply op_local_update_discrete; auto.
+ rewrite -insert_singleton_op; trivial. apply insert_valid; done.
+ Qed.
+
+ Lemma update_graph {E} (G : Gmon) q x w m :
+ G !! x = None →
+ own graph_name (â— Some (1%Qp, {[x := Excl m]} â‹… G))
+ ∗ own_graph q (x [↦] m)
+ ⊢ |={E}=> own graph_name (◠Some (1%Qp, {[x := Excl w]} ⋅ G))
+ ∗ own_graph q (x [↦] w).
+ Proof.
+ iIntros (Hx) "H". rewrite -?own_op.
+ iMod (own_update with "H") as "H'"; eauto.
+ apply auth_update, option_local_update, prod_local_update;
+ first done; simpl.
+ rewrite -!insert_singleton_op; trivial.
+ replace (<[x:=Excl w]> G) with (<[x:=Excl w]> (<[x:=Excl m]> G))
+ by (by rewrite insert_insert).
+ eapply singleton_local_update; first (by rewrite lookup_insert);
+ apply exclusive_local_update; done.
+ Qed.
+
+ Lemma graph_pointsto_marked (G : Gmon) q x w :
+ own graph_name (◠Some (1%Qp, G)) ∗ own_graph q (x [↦] w)
+ ⊢ ⌜G = {[x := Excl w]} â‹… (delete x G)âŒ.
+ Proof.
+ rewrite /own_graph -?own_op. iIntros "H".
+ iDestruct (@own_valid with "H") as %[H1 H2]; simpl in *.
+ iPureIntro.
+ specialize (H1 O).
+ apply cmra_discrete_included_iff in H1.
+ apply option_included in H1; destruct H1 as [H1|H1]; [inversion H1|].
+ destruct H1 as (u1 & u2 & Hu1 & Hu2 & H1);
+ inversion Hu1; inversion Hu2; subst.
+ destruct H1 as [[_ H11%leibniz_equiv]|H12]; simpl in *.
+ + by rewrite -H11 delete_singleton right_id_L.
+ + apply prod_included in H12; destruct H12 as [_ H12]; simpl in *.
+ rewrite -insert_singleton_op ?insert_delete; last by rewrite lookup_delete.
+ apply: map_eq => i. apply leibniz_equiv, equiv_dist => n.
+ destruct (decide (x = i)); subst;
+ rewrite ?lookup_insert ?lookup_insert_ne //.
+ apply singleton_included in H12. destruct H12 as [y [H31 H32]].
+ rewrite H31 (Some_included_exclusive _ _ H32); try done.
+ destruct H2 as [H21 H22]; simpl in H22.
+ specialize (H22 i); revert H22; rewrite H31; done.
+ Qed.
+
+ Lemma graph_open (g :graph loc) (markings : gmap loc loc) (G : Gmon) x
+ : x ∈ dom (gset _) g →
+ own graph_name (◠Some (1%Qp, G)) ∗ heap_owns (of_graph g G) markings ⊢
+ own graph_name (â— Some (1%Qp, G))
+ ∗ heap_owns (delete x (of_graph g G)) markings
+ ∗ (∃ u : bool * (option loc * option loc), ⌜of_graph g G !! x = Some uâŒ
+ ∗ ∃ (m : loc), ⌜markings !! x = Some m⌠∗ x ↦ (#m, children_to_val (u.2))
+ ∗ m ↦ #(u.1)).
+ Proof.
+ iIntros (Hx) "(Hg & Ha)".
+ assert (Hid : x ∈ dom (gset _) (of_graph g G)) by (by rewrite of_graph_dom).
+ revert Hid; rewrite elem_of_dom /is_Some. intros [y Hy].
+ rewrite /heap_owns -{1}(insert_id _ _ _ Hy) -insert_delete.
+ rewrite big_sepM_insert; [|apply lookup_delete_None; auto].
+ iDestruct "Ha" as "[H $]". iFrame "Hg". iExists _; eauto.
+ Qed.
+
+ Lemma graph_close g markings G x :
+ heap_owns (delete x (of_graph g G)) markings
+ ∗ (∃ u : bool * (option loc * option loc), ⌜of_graph g G !! x = Some uâŒ
+ ∗ ∃ (m : loc), ⌜markings !! x = Some m⌠∗ x ↦ (#m, children_to_val (u.2))
+ ∗ m ↦ #(u.1))
+ ⊢ heap_owns (of_graph g G) markings.
+ Proof.
+ iIntros "[Ha Hl]". iDestruct "Hl" as (u) "[Hu Hl]". iDestruct "Hu" as %Hu.
+ rewrite /heap_owns -{2}(insert_id _ _ _ Hu) -insert_delete.
+ rewrite big_sepM_insert; [|apply lookup_delete_None; auto]. by iFrame "Ha".
+ Qed.
+
+ Lemma marked_is_marked_in_auth (mr : gset loc) l :
+ own graph_marking_name (â— mr) ∗ is_marked l ⊢ ⌜l ∈ mrâŒ.
+ Proof.
+ iIntros "H". unfold is_marked. rewrite -own_op.
+ iDestruct (own_valid with "H") as %Hvl.
+ iPureIntro. destruct Hvl as [Hvl _]. destruct (Hvl O) as [z Hvl'].
+ rewrite Hvl' /= !gset_op_union !elem_of_union elem_of_singleton; tauto.
+ Qed.
+
+ Lemma marked_is_marked_in_auth_sepS (mr : gset loc) m :
+ own graph_marking_name (â— mr) ∗ ([∗ set] l ∈ m, is_marked l) ⊢ ⌜m ⊆ mrâŒ.
+ Proof.
+ iIntros "[Hmr Hm]". rewrite big_sepS_forall pure_forall.
+ iIntros (x). rewrite pure_impl. iIntros (Hx).
+ iApply marked_is_marked_in_auth.
+ iFrame. by iApply "Hm".
+ Qed.
+
+End graph.
+
+(* Graph properties *)
+
+Lemma delete_marked g G x w :
+ delete x (of_graph g G) = delete x (of_graph g ((x [↦] w) ⋅ G)).
+Proof.
+ apply: map_eq => i. destruct (decide (i = x)).
+ - subst; by rewrite ?lookup_delete.
+ - rewrite ?lookup_delete_ne //= /of_graph /of_graph_elem ?lookup_imap
+ ?lookup_omap; case _ : (g !! i) => [v|] //=.
+ by rewrite lookup_op lookup_singleton_ne //= left_id_L.
+Qed.
+
+Lemma in_dom_conv (G G' : Gmon) x : ✓ (G ⋅ G') → x ∈ dom (gset loc) (Gmon_graph G)
+ → (Gmon_graph (G ⋅ G')) !! x = (Gmon_graph G) !! x.
+Proof.
+ intros HGG. specialize (HGG x). revert HGG.
+ rewrite /get_left /Gmon_graph elem_of_dom /is_Some ?lookup_omap lookup_op.
+ case _ : (G !! x) => [[]|]; case _ : (G' !! x) => [[]|]; do 2 inversion 1;
+ simpl in *; auto; congruence.
+Qed.
+Lemma in_dom_conv' (G G' : Gmon) x: ✓(G ⋅ G') → x ∈ dom (gset loc) (Gmon_graph G')
+ → (Gmon_graph (G ⋅ G')) !! x = (Gmon_graph G') !! x.
+Proof. rewrite comm; apply in_dom_conv. Qed.
+Lemma get_left_conv (G G' : Gmon) x xl : ✓ (G ⋅ G') →
+ x ∈ dom (gset _) (Gmon_graph G) → get_left (Gmon_graph (G ⋅ G')) x = Some xl
+ ↔ get_left (Gmon_graph G) x = Some xl.
+Proof. intros. rewrite /get_left in_dom_conv; auto. Qed.
+Lemma get_left_conv' (G G' : Gmon) x xl : ✓ (G ⋅ G') →
+ x ∈ dom (gset _) (Gmon_graph G') → get_left (Gmon_graph (G ⋅ G')) x = Some xl
+ ↔ get_left (Gmon_graph G') x = Some xl.
+Proof. rewrite comm; apply get_left_conv. Qed.
+Lemma get_right_conv (G G' : Gmon) x xl : ✓ (G ⋅ G') →
+ x ∈ dom (gset _) (Gmon_graph G) → get_right (Gmon_graph (G ⋅ G')) x = Some xl
+ ↔ get_right (Gmon_graph G) x = Some xl.
+Proof. intros. rewrite /get_right in_dom_conv; auto. Qed.
+Lemma get_right_conv' (G G' : Gmon) x xl : ✓ (G ⋅ G') →
+ x ∈ dom (gset _) (Gmon_graph G') → get_right (Gmon_graph (G ⋅ G')) x = Some xl
+ ↔ get_right (Gmon_graph G') x = Some xl.
+Proof. rewrite comm; apply get_right_conv. Qed.
+
+Lemma in_op_dom (G G' : Gmon) y : ✓(G ⋅ G') →
+ y ∈ dom (gset loc) (Gmon_graph G) → y ∈ dom (gset loc) (Gmon_graph (G ⋅ G')).
+Proof. refine (λ H x, _ x); rewrite ?elem_of_dom ?in_dom_conv ; eauto. Qed.
+Lemma in_op_dom' (G G' : Gmon) y : ✓(G ⋅ G') →
+ y ∈ dom (gset loc) (Gmon_graph G') → y ∈ dom (gset loc) (Gmon_graph (G ⋅ G')).
+Proof. rewrite comm; apply in_op_dom. Qed.
+
+Local Hint Resolve cmra_valid_op_l cmra_valid_op_r in_op_dom in_op_dom'.
+
+Lemma in_op_dom_alt (G G' : Gmon) y : ✓(G ⋅ G') →
+ y ∈ dom (gset loc) G → y ∈ dom (gset loc) (G ⋅ G').
+Proof. intros HGG; rewrite -?Gmon_graph_dom; eauto. Qed.
+Lemma in_op_dom_alt' (G G' : Gmon) y : ✓(G ⋅ G') →
+ y ∈ dom (gset loc) G' → y ∈ dom (gset loc) (G ⋅ G').
+Proof. intros HGG; rewrite -?Gmon_graph_dom; eauto. Qed.
+
+Local Hint Resolve in_op_dom_alt in_op_dom_alt'.
+Local Hint Extern 1 => eapply get_left_conv + eapply get_left_conv' +
+ eapply get_right_conv + eapply get_right_conv'.
+
+Local Hint Extern 1 (_ ∈ dom (gset loc) (Gmon_graph _)) =>
+ erewrite Gmon_graph_dom.
+
+Local Hint Resolve path_start path_end.
+
+Lemma path_conv (G G' : Gmon) x y p :
+ ✓ (G ⋅ G') → maximal (Gmon_graph G) → x ∈ dom (gset _) G →
+ valid_path (Gmon_graph (G ⋅ G')) x y p → valid_path (Gmon_graph G) x y p.
+Proof.
+ intros Hv Hm. rewrite -Gmon_graph_dom //=; eauto. revert x y.
+ induction p as [|[] p]; inversion 2; subst; econstructor; eauto;
+ try eapply IHp; try eapply Hm; eauto.
+Qed.
+Lemma path_conv_back (G G' : Gmon) x y p :
+ ✓ (G ⋅ G') → x ∈ dom (gset _) G →
+ valid_path (Gmon_graph G) x y p → valid_path (Gmon_graph (G ⋅ G')) x y p.
+Proof.
+ intros Hv. rewrite -Gmon_graph_dom //=; eauto. revert x y.
+ induction p as [|[] p]; inversion 2; subst; econstructor; eauto;
+ try eapply IHp; eauto.
+Qed.
+Lemma path_conv' (G G' : Gmon) x y p :
+ ✓ (G ⋅ G') → maximal (Gmon_graph G') → x ∈ dom (gset _) G' →
+ valid_path (Gmon_graph (G ⋅ G')) x y p → valid_path (Gmon_graph G') x y p.
+Proof. rewrite comm; eapply path_conv. Qed.
+Lemma path_conv_back' (G G' : Gmon) x y p :
+ ✓ (G ⋅ G') → x ∈ dom (gset _) G' →
+ valid_path (Gmon_graph G') x y p → valid_path (Gmon_graph (G ⋅ G')) x y p.
+Proof. rewrite comm; apply path_conv_back. Qed.
+
+Local Ltac in_dom_Gmon_graph :=
+ rewrite Gmon_graph_dom //= ?dom_op ?elem_of_union ?dom_singleton
+ ?elem_of_singleton.
+
+Lemma get_left_singleton x vl vr :
+ get_left (Gmon_graph (x [↦] (vl, vr))) x = vl.
+Proof. rewrite /get_left /Gmon_graph lookup_omap lookup_singleton; done. Qed.
+Lemma get_right_singleton x vl vr :
+ get_right (Gmon_graph (x [↦] (vl, vr))) x = vr.
+Proof. rewrite /get_right /Gmon_graph lookup_omap lookup_singleton; done. Qed.
+
+Lemma graph_in_dom_op (G G' : Gmon) x :
+ ✓ (G ⋅ G') → x ∈ dom (gset loc) G → x ∉ dom (gset _) G'.
+Proof.
+ intros HGG. specialize (HGG x). revert HGG. rewrite ?elem_of_dom lookup_op.
+ case _ : (G !! x) => [[]|]; case _ : (G' !! x) => [[]|]; inversion 1;
+ do 2 (intros [? Heq]; inversion Heq; clear Heq).
+Qed.
+Lemma graph_in_dom_op' (G G' : Gmon) x :
+ ✓ (G ⋅ G') → x ∈ dom (gset loc) G' → x ∉ dom (gset _) G.
+Proof. rewrite comm; apply graph_in_dom_op. Qed.
+Lemma graph_op_path (G G' : Gmon) x z p :
+ ✓ (G ⋅ G') → x ∈ dom (gset _) G → valid_path (Gmon_graph G') z x p → False.
+Proof.
+ intros ?? Hp%path_end; rewrite Gmon_graph_dom in Hp; eauto.
+ eapply graph_in_dom_op; eauto.
+Qed.
+Lemma graph_op_path' (G G' : Gmon) x z p :
+ ✓ (G ⋅ G') → x ∈ dom (gset _) G' → valid_path (Gmon_graph G) z x p → False.
+Proof. rewrite comm; apply graph_op_path. Qed.
+
+Lemma in_dom_singleton (x : loc) (w : chlC) :
+ x ∈ dom (gset loc) (x [↦] w : gmap loc _).
+Proof. by rewrite dom_singleton elem_of_singleton. Qed.
+
+
+Local Hint Resolve graph_op_path graph_op_path' in_dom_singleton.
+
+Lemma maximal_op (G G' : Gmon) : ✓ (G ⋅ G') → maximal (Gmon_graph G)
+ → maximal (Gmon_graph G') → maximal (Gmon_graph (G ⋅ G')).
+Proof.
+ intros Hvl [_ HG] [_ HG']. split; trivial => x v.
+ rewrite Gmon_graph_dom ?dom_op ?elem_of_union -?Gmon_graph_dom; eauto.
+ intros [Hxl|Hxr].
+ - erewrite get_left_conv, get_right_conv; eauto.
+ - erewrite get_left_conv', get_right_conv'; eauto.
+Qed.
+
+Lemma maximal_op_singleton (G : Gmon) x vl vr :
+ ✓ ((x [↦] (vl, vr)) ⋅ G) → maximal(Gmon_graph G) →
+ match vl with | Some xl => xl ∈ dom (gset _) G | None => True end →
+ match vr with | Some xr => xr ∈ dom (gset _) G | None => True end →
+ maximal (Gmon_graph ((x [↦] (vl, vr)) ⋅ G)).
+Proof.
+ intros HGG [_ Hmx] Hvl Hvr; split; trivial => z v. in_dom_Gmon_graph.
+ intros [Hv|Hv]; subst.
+ - erewrite get_left_conv, get_right_conv, get_left_singleton,
+ get_right_singleton; eauto.
+ destruct vl as [xl|]; destruct vr as [xr|]; intros [Hl|Hr];
+ try inversion Hl; try inversion Hr; subst; eauto.
+ - erewrite get_left_conv', get_right_conv', <- Gmon_graph_dom; eauto.
+Qed.
+
+Local Hint Resolve maximal_op_singleton maximal_op get_left_singleton
+ get_right_singleton.
+
+Lemma maximally_marked_tree_both (G G' : Gmon) x xl xr :
+ ✓ ((x [↦] (Some xl, Some xr)) ⋅ (G ⋅ G')) →
+ xl ∈ dom (gset _) G → tree (Gmon_graph G) xl → maximal (Gmon_graph G) →
+ xr ∈ dom (gset _) G' → tree (Gmon_graph G') xr → maximal (Gmon_graph G') →
+ tree (Gmon_graph ((x [↦] (Some xl, Some xr)) ⋅ (G ⋅ G'))) x ∧
+ maximal (Gmon_graph ((x [↦] (Some xl, Some xr)) ⋅ (G ⋅ G'))).
+Proof.
+ intros Hvl Hxl tl ml Hxr tr mr; split.
+ - intros l. in_dom_Gmon_graph. intros [?|[HlG|HlG']]; first subst.
+ + exists []; split.
+ { constructor 1; trivial. in_dom_Gmon_graph; auto. }
+ { intros p Hp. destruct p; inversion Hp as [| ? ? Hl Hpv| ? ? Hl Hpv];
+ trivial; subst.
+ - exfalso. apply get_left_conv in Hl; [| |in_dom_Gmon_graph]; eauto.
+ rewrite get_left_singleton in Hl; inversion Hl; subst.
+ apply path_conv' in Hpv; eauto.
+ - exfalso. apply get_right_conv in Hl; [| |in_dom_Gmon_graph]; eauto.
+ rewrite get_right_singleton in Hl; inversion Hl; subst.
+ apply path_conv' in Hpv; eauto. }
+ + edestruct tl as [q [qv Hq]]; eauto.
+ exists (true :: q). split; [econstructor; eauto|].
+ { eapply path_conv_back'; eauto; eapply path_conv_back; eauto. }
+ { intros p Hp. destruct p; inversion Hp as [| ? ? Hl Hpv| ? ? Hl Hpv];
+ trivial; subst.
+ - exfalso; eapply path_conv_back in qv; eauto.
+ - apply get_left_conv in Hl; eauto.
+ rewrite get_left_singleton in Hl. inversion Hl; subst.
+ apply path_conv', path_conv in Hpv; eauto. erewrite Hq; eauto.
+ - exfalso. apply get_right_conv in Hl; eauto.
+ rewrite get_right_singleton in Hl; inversion Hl; subst.
+ do 2 apply path_conv' in Hpv; eauto. }
+ + edestruct tr as [q [qv Hq]]; eauto.
+ exists (false :: q). split; [econstructor; eauto|].
+ { eapply path_conv_back'; eauto; eapply path_conv_back'; eauto. }
+ { intros p Hp. destruct p; inversion Hp as [| ? ? Hl Hpv| ? ? Hl Hpv];
+ trivial; subst.
+ - exfalso; eapply path_conv_back' in qv; eauto.
+ - exfalso. apply get_left_conv in Hl; eauto.
+ rewrite get_left_singleton in Hl; inversion Hl; subst.
+ apply path_conv', path_conv in Hpv; eauto.
+ - apply get_right_conv in Hl; eauto.
+ rewrite get_right_singleton in Hl. inversion Hl; subst.
+ apply path_conv', path_conv' in Hpv; eauto. erewrite Hq; eauto. }
+ - apply maximal_op_singleton; eauto.
+Qed.
+
+Lemma maximally_marked_tree_left (G : Gmon) x xl :
+ ✓ ((x [↦] (Some xl, None)) ⋅ G) →
+ xl ∈ dom (gset _) G → tree (Gmon_graph G) xl → maximal (Gmon_graph G) →
+ tree (Gmon_graph ((x [↦] (Some xl, None)) ⋅ G)) x ∧
+ maximal (Gmon_graph ((x [↦] (Some xl, None)) ⋅ G)).
+Proof.
+ intros Hvl Hxl tl ml; split.
+ - intros l. in_dom_Gmon_graph. intros [?|HlG]; first subst.
+ + exists []; split.
+ { constructor 1; trivial. in_dom_Gmon_graph; auto. }
+ { intros p Hp. destruct p; inversion Hp as [| ? ? Hl Hpv| ? ? Hl Hpv];
+ trivial; subst.
+ - exfalso. apply get_left_conv in Hl; [| |in_dom_Gmon_graph]; eauto.
+ rewrite get_left_singleton in Hl; inversion Hl; subst.
+ apply path_conv' in Hpv; eauto.
+ - exfalso. apply get_right_conv in Hl; [| |in_dom_Gmon_graph]; eauto.
+ rewrite get_right_singleton in Hl; inversion Hl. }
+ + edestruct tl as [q [qv Hq]]; eauto.
+ exists (true :: q). split; [econstructor; eauto|].
+ { eapply path_conv_back'; eauto; eapply path_conv_back; eauto. }
+ { intros p Hp. destruct p; inversion Hp as [| ? ? Hl Hpv| ? ? Hl Hpv];
+ trivial; subst.
+ - exfalso; eauto.
+ - apply get_left_conv in Hl; eauto.
+ rewrite get_left_singleton in Hl. inversion Hl; subst.
+ apply path_conv' in Hpv; eauto. erewrite Hq; eauto.
+ - exfalso. apply get_right_conv in Hl; eauto.
+ rewrite get_right_singleton in Hl; inversion Hl. }
+ - apply maximal_op_singleton; eauto.
+Qed.
+
+Lemma maximally_marked_tree_right (G : Gmon) x xr :
+ ✓ ((x [↦] (None, Some xr)) ⋅ G) →
+ xr ∈ dom (gset _) G → tree (Gmon_graph G) xr → maximal (Gmon_graph G) →
+ tree (Gmon_graph ((x [↦] (None, Some xr)) ⋅ G)) x ∧
+ maximal (Gmon_graph ((x [↦] (None, Some xr)) ⋅ G)).
+Proof.
+ intros Hvl Hxl tl ml; split.
+ - intros l. in_dom_Gmon_graph. intros [?|HlG]; first subst.
+ + exists []; split.
+ { constructor 1; trivial. in_dom_Gmon_graph; auto. }
+ { intros p Hp. destruct p; inversion Hp as [| ? ? Hl Hpv| ? ? Hl Hpv];
+ trivial; subst.
+ - exfalso. apply get_left_conv in Hl; [| |in_dom_Gmon_graph]; eauto.
+ rewrite get_left_singleton in Hl; inversion Hl.
+ - exfalso. apply get_right_conv in Hl; [| |in_dom_Gmon_graph]; eauto.
+ rewrite get_right_singleton in Hl; inversion Hl; subst.
+ apply path_conv' in Hpv; eauto. }
+ + edestruct tl as [q [qv Hq]]; eauto.
+ exists (false :: q). split; [econstructor; eauto|].
+ { eapply path_conv_back'; eauto; eapply path_conv_back; eauto. }
+ { intros p Hp. destruct p; inversion Hp as [| ? ? Hl Hpv| ? ? Hl Hpv];
+ trivial; subst.
+ - exfalso; eauto.
+ - exfalso. apply get_left_conv in Hl; eauto.
+ rewrite get_left_singleton in Hl; inversion Hl.
+ - apply get_right_conv in Hl; eauto.
+ rewrite get_right_singleton in Hl. inversion Hl; subst.
+ apply path_conv' in Hpv; eauto. erewrite Hq; eauto. }
+ - apply maximal_op_singleton; eauto.
+Qed.
+
+Lemma maximally_marked_tree_none (x : loc) :
+ ✓ ((x [↦] (None, None)) : Gmon) →
+ tree (Gmon_graph (x [↦] (None, None))) x ∧
+ maximal (Gmon_graph (x [↦] (None, None))).
+Proof.
+ intros Hvl; split.
+ - intros l. in_dom_Gmon_graph. intros ?; subst.
+ + exists []; split.
+ { constructor 1; trivial. in_dom_Gmon_graph; auto. }
+ { intros p Hp. destruct p; inversion Hp as [| ? ? Hl Hpv| ? ? Hl Hpv];
+ trivial; subst.
+ - rewrite get_left_singleton in Hl; inversion Hl.
+ - rewrite get_right_singleton in Hl; inversion Hl. }
+ - split; trivial. intros z v. in_dom_Gmon_graph. intros ? [Hl|Hl]; subst.
+ + rewrite get_left_singleton in Hl; inversion Hl.
+ + rewrite get_right_singleton in Hl; inversion Hl.
+Qed.
+
+Lemma update_valid (G : Gmon) x v w : ✓ ((x [↦] v) ⋅ G) → ✓ ((x [↦] w) ⋅ G).
+Proof.
+ intros Hvl i; specialize (Hvl i); revert Hvl.
+ rewrite ?lookup_op. destruct (decide (i = x)).
+ - subst; rewrite ?lookup_singleton; case _ : (G !! x); done.
+ - rewrite ?lookup_singleton_ne //=.
+Qed.
+
+Lemma of_graph_unmarked (g : graph loc) (G : Gmon) x v :
+ of_graph g G !! x = Some (false, v) → g !! x = Some v.
+Proof.
+ rewrite lookup_imap /of_graph_elem lookup_omap.
+ case _ : (g !! x); case _ : (G !! x) => [[]|]; by inversion 1.
+Qed.
+Lemma get_lr_disj (G G' : Gmon) i : ✓ (G ⋅ G') →
+ (get_left (Gmon_graph (G ⋅ G')) i = get_left (Gmon_graph G) i ∧
+ get_right (Gmon_graph (G ⋅ G')) i = get_right (Gmon_graph G) i ∧
+ get_left (Gmon_graph G') i = None ∧
+ get_right (Gmon_graph G') i = None) ∨
+ (get_left (Gmon_graph (G ⋅ G')) i = get_left (Gmon_graph G') i ∧
+ get_right (Gmon_graph (G ⋅ G')) i = get_right (Gmon_graph G') i ∧
+ get_left (Gmon_graph G) i = None ∧
+ get_right (Gmon_graph G) i = None).
+Proof.
+ intros Hvl. specialize (Hvl i). revert Hvl.
+ rewrite /get_left /get_right /Gmon_graph ?lookup_omap ?lookup_op.
+ case _ : (G !! i) => [[]|]; case _ : (G' !! i) => [[]|]; inversion 1;
+ simpl; auto.
+Qed.
+Lemma mark_update_strict_subgraph (g : graph loc) (G G' : Gmon) : ✓ (G ⋅ G') →
+ strict_subgraph g (Gmon_graph G) ∧ strict_subgraph g (Gmon_graph G') ↔
+ strict_subgraph g (Gmon_graph (G â‹… G')).
+Proof.
+ intros Hvl; split.
+ - intros [HG HG'] i.
+ destruct (get_lr_disj G G' i) as [(-> & -> & _ & _)|(-> & -> & _ & _)]; eauto.
+ - intros HGG; split => i.
+ + destruct (get_lr_disj G G' i) as [(<- & <- & _ & _)|(_ & _ & -> & ->)];
+ eauto using strict_sub_children_None.
+ + destruct (get_lr_disj G G' i) as [(_ & _ & -> & ->)|(<- & <- & _ & _)];
+ eauto using strict_sub_children_None.
+Qed.
+Lemma strinct_subgraph_singleton (g : graph loc) x v :
+ x ∈ dom (gset loc) g → (∀ w, g !! x = Some w → strict_sub_children w v)
+ ↔ strict_subgraph g (Gmon_graph (x [↦] v)).
+Proof.
+ rewrite elem_of_dom; intros [u Hu]; split.
+ - move => /(_ _ Hu) Hgw i.
+ rewrite /get_left /get_right /Gmon_graph lookup_omap.
+ destruct (decide (i = x)); subst.
+ + by rewrite Hu lookup_singleton; simpl.
+ + rewrite lookup_singleton_ne; auto. by case _ : (g !! i) => [[[?|] [?|]]|].
+ - intros Hg w Hw; specialize (Hg x). destruct v as [v1 v2]; simpl. revert Hg.
+ rewrite Hu in Hw; inversion Hw; subst.
+ by rewrite get_left_singleton get_right_singleton /get_left /get_right Hu.
+Qed.
+Lemma mark_strict_subgraph (g : graph loc) (G : Gmon) x v :
+ ✓ ((x [↦] v) ⋅ G) → x ∈ dom (gset positive) g →
+ of_graph g G !! x = Some (false, v) → strict_subgraph g (Gmon_graph G) →
+ strict_subgraph g (Gmon_graph ((x [↦] v) ⋅ G)).
+Proof.
+ intros Hvl Hdx Hx Hsg. apply mark_update_strict_subgraph; try split; eauto.
+ eapply strinct_subgraph_singleton; erewrite ?of_graph_unmarked; eauto.
+ inversion 1; auto using strict_sub_children_refl.
+Qed.
+Lemma update_strict_subgraph (g : graph loc) (G : Gmon) x v w :
+ ✓ ((x [↦] v) ⋅ G) → x ∈ dom (gset positive) g →
+ strict_subgraph g (Gmon_graph ((x [↦] w) ⋅ G)) →
+ strict_sub_children w v →
+ strict_subgraph g (Gmon_graph ((x [↦] v) ⋅ G)).
+Proof.
+ intros Hvl Hdx Hx Hsc1 Hsc2.
+ apply mark_update_strict_subgraph in Hx; eauto using update_valid.
+ destruct Hx as [Hx1 Hx2].
+ apply mark_update_strict_subgraph; try split; try tauto.
+ pose proof (proj1 (elem_of_dom _ _) Hdx) as [u Hu].
+ eapply strinct_subgraph_singleton in Hx1; eauto.
+ apply strinct_subgraph_singleton; trivial.
+ intros u' Hu'; rewrite Hu in Hu'; inversion Hu'; subst.
+ intuition eauto using strict_sub_children_trans.
+Qed.
diff --git a/theories/spanning_tree/proof.v b/theories/spanning_tree/proof.v
new file mode 100644
index 0000000000000000000000000000000000000000..81098608287f6187f1a8869213a9181da0e099bc
--- /dev/null
+++ b/theories/spanning_tree/proof.v
@@ -0,0 +1,69 @@
+From iris.algebra Require Import frac gmap auth.
+From iris.base_logic Require Export invariants.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Export lifting notation.
+From iris.heap_lang.lib Require Import par.
+From iris.base_logic Require Import cancelable_invariants.
+Import uPred.
+
+From iris_examples.spanning_tree Require Import graph mon spanning.
+
+Section wp_span.
+ Context `{heapG Σ, cinvG Σ, inG Σ (authR markingUR),
+ inG Σ (authR graphUR), spawnG Σ}.
+
+ Lemma wp_span g (markings : gmap loc loc) (x : val) (l : loc) :
+ l ∈ dom (gset loc) g → maximal g → connected g l →
+ ([∗ map] l ↦ v ∈ g,
+ ∃ (m : loc), ⌜markings !! l = Some m⌠∗ l ↦ (#m, children_to_val v)
+ ∗ m ↦ #false) ⊢
+ WP span (SOME #l)
+ {{ _, ∃ g',
+ ([∗ map] l ↦ v ∈ g',
+ ∃ m : loc, ⌜markings !! l = Some m⌠∗ l ↦ (#m, children_to_val v)
+ ∗ m ↦ #true)
+ ∗ ⌜dom (gset loc) g = dom (gset loc) g'âŒ
+ ∗ ⌜strict_subgraph g g'⌠∗ ⌜tree g' lâŒ
+ }}.
+ Proof.
+ iIntros (Hgl Hgmx Hgcn) "Hgr".
+ iMod (graph_ctx_alloc _ g markings with "[Hgr]") as (Ig κ) "(key & #Hgr & Hg)";
+ eauto.
+ iApply wp_fupd.
+ iApply wp_wand_l; iSplitR;
+ [|iApply ((rec_wp_span κ g markings 1 1 (SOMEV #l)) with "[Hg key]");
+ eauto; iFrame "#"; iFrame].
+ iIntros (v) "[H key]".
+ unfold graph_ctx.
+ iMod (cinv_cancel ⊤ graphN κ (graph_inv g markings) with "[#] [key]")
+ as ">Hinv"; first done; try by iFrame.
+ iClear "Hgr". unfold graph_inv.
+ iDestruct "Hinv" as (G) "(Hi1 & Hi2 & Hi3 & Hi4)".
+ iDestruct "Hi4" as %Hi4.
+ iDestruct "H" as "[H|H]".
+ - iDestruct "H" as "(_ & H)". iDestruct "H" as (l') "(H1 & H2 & Hl')".
+ iDestruct "H1" as %Hl; inversion Hl; subst.
+ iDestruct "H2" as (G' gmr gtr) "(Hl1 & Hl2 & Hl3 & Hl4 & Hl5)".
+ iDestruct "Hl2" as %Hl2. iDestruct "Hl3" as %Hl3. iDestruct "Hl4" as %Hl4.
+ iDestruct (whole_frac with "[Hi1 Hl1]") as %Heq; [by iFrame|]; subst.
+ iDestruct (marked_is_marked_in_auth_sepS with "[Hi2 Hl5]") as %Hmrk;
+ [by iFrame|].
+ iDestruct (own_graph_valid with "Hl1") as %Hvl.
+ iExists (Gmon_graph G').
+ assert (dom (gset positive) g = dom (gset positive) (Gmon_graph G')).
+ { erewrite front_t_t_dom; eauto.
+ - by rewrite Gmon_graph_dom.
+ - eapply front_mono; rewrite Gmon_graph_dom; eauto. }
+ iModIntro. repeat iSplitL; try by iPureIntro.
+ rewrite /heap_owns of_graph_dom_eq //=. by rewrite big_sepM_fmap /=.
+ - iDestruct "H" as "(_ & [H|H] & Hx)".
+ + iDestruct "H" as %Heq. inversion Heq.
+ + iDestruct "H" as (l') "(_ & Hl)".
+ iDestruct (marked_is_marked_in_auth with "[Hi2 Hl]") as %Hmrk;
+ [by iFrame|].
+ iDestruct (whole_frac with "[Hx Hi1]") as %Heq; [by iFrame|]; subst.
+ exfalso; revert Hmrk. rewrite dom_empty. inversion 1.
+ Qed.
+
+End wp_span.
\ No newline at end of file
diff --git a/theories/spanning_tree/spanning.v b/theories/spanning_tree/spanning.v
new file mode 100644
index 0000000000000000000000000000000000000000..ff71d3b675bb62341d4e3b973706edd20c3ac4ef
--- /dev/null
+++ b/theories/spanning_tree/spanning.v
@@ -0,0 +1,493 @@
+From iris.algebra Require Import frac gmap gset excl.
+From iris.base_logic Require Export invariants.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Export lifting notation.
+From iris.heap_lang.lib Require Import par.
+From iris.base_logic Require Import cancelable_invariants.
+Import uPred.
+
+From iris_examples.spanning_tree Require Import graph mon.
+
+Definition try_mark : val :=
+ λ: "y", let: "e" := Fst (!"y") in CAS "e" #false #true.
+
+Definition unmark_fst : val :=
+ λ: "y",
+ let: "e" := ! "y" in "y" <- (Fst "e", (NONE, Snd (Snd "e"))).
+
+Definition unmark_snd : val :=
+ λ: "y",
+ let: "e" := ! "y" in "y" <- (Fst "e", (Fst (Snd "e"), NONE)).
+
+Definition span : val :=
+ rec: "span" "x" :=
+ match: "x" with
+ NONE => # false
+ | SOME "y" =>
+ if: try_mark "y" then
+ let: "e" := ! "y" in
+ let: "rs" := "span" (Fst (Snd "e")) ||| "span" (Snd (Snd "e")) in
+ ((if: ~ (Fst "rs") then unmark_fst "y" else #())
+ ;; if: ~ (Snd "rs") then unmark_snd "y" else #());; #true
+ else
+ #false
+ end.
+
+Section Helpers.
+ Context `{heapG Σ, cinvG Σ, graphG Σ, spawnG Σ} (κ : gname).
+
+ Lemma wp_try_mark g Mrk k q (x : loc) : x ∈ dom (gset _) g →
+ graph_ctx κ g Mrk ∗ own_graph q ∅ ∗ cinv_own κ k
+ ⊢ WP (try_mark #x) {{ v,
+ (⌜v = #true⌠∗ (∃ u, ⌜(g !! x) = Some u⌠∗ own_graph q (x [↦] u))
+ ∗ is_marked x ∗ cinv_own κ k)
+ ∨ (⌜v = #false⌠∗ own_graph q ∅ ∗ is_marked x ∗ cinv_own κ k)
+ }}.
+ Proof.
+ iIntros (Hgx) "(#Hgr & Hx & key)".
+ wp_let; wp_bind (! _)%E. unfold graph_ctx.
+ iMod (cinv_open with "Hgr key") as "(>Hinv & key & Hcl)"; first done.
+ unfold graph_inv at 2.
+ iDestruct "Hinv" as (G) "(Hi1 & Hi2 & Hi3 & Hi4)".
+ iDestruct (graph_open with "[Hi1 Hi3]") as
+ "(Hi1 & Hi3 & Hil)"; eauto; [by iFrame|].
+ iDestruct "Hil" as (u) "[Hil1 Hil2]".
+ iDestruct "Hil2" as (m) "[Hil2 [Hil3 Hil4]]".
+ wp_load.
+ iDestruct "Hil1" as %Hil1. iDestruct "Hil2" as %Hil2.
+ iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3"; eauto.
+ { iFrame. iExists _; eauto. iSplitR; eauto. iExists _; by iFrame. }
+ iMod ("Hcl" with "[Hi1 Hi2 Hi3 Hi4]") as "_".
+ { iNext. unfold graph_inv at 2. iExists _; iFrame; auto. }
+ iModIntro. wp_proj. wp_let.
+ destruct u as [u1 u2]; simpl.
+ iMod (cinv_open _ graphN with "Hgr key")
+ as "(>Hinv & key & Hclose)"; first done.
+ unfold graph_inv at 2.
+ iDestruct "Hinv" as (G') "(Hi1 & Hi2 & Hi3 & Hi4)".
+ iDestruct (graph_open with "[Hi1 Hi3]") as
+ "(Hi1 & Hi3 & Hil)"; eauto; [by iFrame|].
+ iDestruct "Hil" as (u) "[Hil1 Hil2]".
+ iDestruct "Hil2" as (m') "[Hil2 [Hil3 Hil4]]".
+ iDestruct "Hil2" as %Hil2'. iDestruct "Hil1" as %Hil1'.
+ iDestruct "Hi4" as %Hi4.
+ rewrite Hil2' in Hil2; inversion Hil2; subst.
+ iDestruct (auth_own_graph_valid with "Hi1") as %Hvl.
+ destruct u as [[] uch].
+ - wp_cas_fail; first done.
+ iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3";
+ eauto.
+ { iFrame. iExists _; eauto. iSplitR; eauto. by iExists _; iFrame. }
+ iMod (already_marked with "Hi2") as "[Hi2 Hxm]"; [|iFrame "Hxm"].
+ { by eapply in_dom_of_graph. }
+ iMod ("Hclose" with "[Hi1 Hi2 Hi3]") as "_".
+ { iNext. unfold graph_inv at 2. iExists _; iFrame; auto. }
+ iModIntro. iFrame. iRight; by iFrame.
+ - (* CAS succeeds *)
+ wp_cas_suc; first done.
+ iMod (mark_graph _ _ x uch with "[Hi1 Hx]") as "[Hi1 Hx]"; try by iFrame.
+ { apply (proj1 (not_elem_of_dom (D := gset loc) G' x)).
+ intros Hid. eapply in_dom_of_graph in Hid; eauto; tauto. }
+ iMod (new_marked with "Hi2") as "[Hi2 Hm]". iFrame "key Hm".
+ erewrite delete_marked.
+ iDestruct (auth_own_graph_valid with "Hi1") as %Hvl'.
+ iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3".
+ { iFrame. iExists (_, _). iSplitR; [| iExists _; iFrame]; trivial.
+ rewrite mark_update_lookup; eauto. }
+ iMod ("Hclose" with "[Hi1 Hi2 Hi3]") as "_".
+ + iNext; unfold graph_inv at 2. iExists _; iFrame.
+ rewrite dom_op dom_singleton_L ?gset_op_union (comm union); iFrame.
+ iPureIntro.
+ { by apply mark_strict_subgraph. }
+ + iModIntro. iLeft; iSplit; trivial. iExists _; iFrame.
+ iPureIntro; eapply of_graph_unmarked; eauto.
+ Qed.
+
+ Lemma laod_strict_sub_children g G x w u : g !! x = Some u →
+ strict_subgraph g (Gmon_graph ((x [↦] w) ⋅ delete x G)) →
+ strict_sub_children u w.
+ Proof.
+ move => Hgx /(_ x).
+ rewrite /get_left /get_right /Gmon_graph Hgx ?lookup_omap ?lookup_op
+ ?lookup_delete ?right_id_L ?lookup_singleton /=;
+ destruct w; destruct u; done.
+ Qed.
+
+ Lemma wp_load_graph g markings k q (x : loc) u w :
+ (g !! x) = Some u →
+ (graph_ctx κ g markings ∗ own_graph q (x [↦] w) ∗ cinv_own κ k)
+ ⊢
+ WP (! #x)
+ {{ v, (∃ m : loc, ⌜markings !! x = Some m⌠∧
+ ⌜v = (#m, children_to_val w)âŒ%V) ∗ ⌜strict_sub_children u wâŒ
+ ∗ own_graph q (x [↦] w) ∗ cinv_own κ k }}.
+ Proof.
+ iIntros (Hgx) "(#Hgr & Hx & key)".
+ assert (Hgx' : x ∈ dom (gset _) g).
+ { rewrite elem_of_dom Hgx; eauto. }
+ unfold graph_ctx.
+ iMod (cinv_open _ graphN with "Hgr key")
+ as "(>Hinv & key & Hclose)"; first done.
+ unfold graph_inv at 2.
+ iDestruct "Hinv" as (G) "(Hi1 & Hi2 & Hi3 & Hi4)".
+ iDestruct (graph_open with "[Hi1 Hi3]") as
+ "(Hi1 & Hi3 & Hil)"; eauto; [by iFrame|].
+ iDestruct "Hil" as (u') "[Hil1 Hil2]".
+ iDestruct "Hil2" as (m) "[Hil2 [Hil3 Hil4]]".
+ wp_load. iDestruct "Hil1" as %Hil1.
+ iDestruct "Hil2" as %Hil2. iDestruct "Hi4" as %Hi4.
+ iDestruct (auth_own_graph_valid with "Hi1") as %Hvl.
+ iDestruct (graph_pointsto_marked with "[Hi1 Hx]")
+ as %Heq; try by iFrame.
+ pose proof Hil1 as Hil1'. rewrite Heq in Hil1' Hvl.
+ rewrite mark_update_lookup in Hil1'; trivial.
+ iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3"; [iFrame|].
+ { iExists _; iSplitR; auto. iExists _; by iFrame. }
+ iMod ("Hclose" with "[Hi1 Hi2 Hi3]") as "_".
+ { iNext. unfold graph_inv at 2. iExists _; iFrame; auto. }
+ iFrame. inversion Hil1'; subst u'; simpl.
+ iModIntro. iSplit; [|iPureIntro]. iExists _; iSplit; iPureIntro; eauto.
+ { rewrite Heq in Hi4. eapply laod_strict_sub_children; eauto. }
+ Qed.
+
+ Lemma wp_store_graph {g markings k q} {x : loc} {v}
+ (w w' : option loc * option loc) {m : loc} :
+ strict_sub_children w w' → (markings !! x) = Some m →
+ (g !! x) = Some v →
+ (graph_ctx κ g markings ∗ own_graph q (x [↦] w) ∗ cinv_own κ k)
+ ⊢
+ WP (#x <- (#m, children_to_val w'))
+ {{ v, own_graph q (x [↦] w') ∗ cinv_own κ k }}.
+ Proof.
+ iIntros (Hagree Hmrk Hgx) "(#Hgr & Hx & key)".
+ assert (Hgx' : x ∈ dom (gset _) g).
+ { rewrite elem_of_dom Hgx; eauto. }
+ unfold graph_ctx.
+ iMod (cinv_open _ graphN with "Hgr key")
+ as "(>Hinv & key & Hclose)"; first done.
+ unfold graph_inv at 2.
+ iDestruct "Hinv" as (G) "(Hi1 & Hi2 & Hi3 & Hi4)".
+ iDestruct (graph_open with "[Hi1 Hi3]") as
+ "(Hi1 & Hi3 & Hil)"; eauto; [by iFrame|].
+ iDestruct "Hil" as (u') "[Hil1 Hil2]".
+ iDestruct "Hil2" as (m') "[Hil2 [Hil3 Hil4]]".
+ wp_store.
+ iDestruct "Hil2" as %Hil2.
+ rewrite Hmrk in Hil2. inversion Hil2; subst; clear Hil2.
+ iDestruct "Hil1" as %Hil1. iDestruct "Hi4" as %Hi4.
+ iDestruct (auth_own_graph_valid with "Hi1") as %Hvl.
+ iDestruct (graph_pointsto_marked with "[Hi1 Hx]") as %Heq; try by iFrame.
+ pose proof Hil1 as Hil1'. rewrite Heq in Hil1' Hvl Hi4.
+ rewrite mark_update_lookup in Hil1'; trivial. inversion Hil1'; subst u'.
+ clear Hil1'. simpl. rewrite Heq.
+ iMod (update_graph _ _ _ w' with "[Hi1 Hx]") as
+ "[Hi1 Hx]"; try by iFrame. by rewrite lookup_delete.
+ rewrite -delete_marked. erewrite (delete_marked _ _ _ w').
+ assert (HvG : ✓ ({[x := Excl w']} ⋅ delete x G)).
+ { eapply update_valid; eauto. }
+ iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3".
+ { iFrame. iExists _. iSplitR.
+ - rewrite ?mark_update_lookup; eauto. - iExists _; by iFrame. }
+ iMod ("Hclose" with "[Hi1 Hi2 Hi3]") as "_"; [|by iFrame].
+ unfold graph_inv at 2.
+ iNext. iExists _; iFrame. rewrite !dom_op !dom_singleton_L. iFrame.
+ iPureIntro.
+ { eapply update_strict_subgraph; eauto. }
+ Qed.
+
+ Lemma wp_unmark_fst g markings k q (x : loc) v w1 w2 :
+ (g !! x) = Some v →
+ (graph_ctx κ g markings ∗ own_graph q (x [↦] (w1, w2))
+ ∗ cinv_own κ k) ⊢
+ WP (unmark_fst #x)
+ {{ _, own_graph q (x [↦] (None, w2)) ∗ cinv_own κ k }}.
+ Proof.
+ iIntros (Hgx) "(#Hgr & Hx & key)".
+ wp_let. wp_bind (! _)%E.
+ iApply wp_wand_l; iSplitR;
+ [|iApply wp_load_graph; eauto; iFrame "Hgr"; by iFrame].
+ iIntros (u) "(H1 & Hagree & Hx & key)". iDestruct "H1" as (m) "[Hmrk Hu]".
+ iDestruct "Hagree" as %Hagree.
+ iDestruct "Hmrk" as %Hmrk; iDestruct "Hu" as %Hu; subst.
+ wp_let. wp_bind (Fst _). do 3 wp_proj.
+ iApply (wp_store_graph _ (None, w2) with "[Hx key]"); eauto;
+ [|iFrame "Hgr"; by iFrame].
+ { by destruct w1; destruct w2; destruct v; inversion Hagree; subst. }
+ Qed.
+
+ Lemma wp_unmark_snd g markings k q (x : loc) v w1 w2 :
+ (g !! x) = Some v →
+ (graph_ctx κ g markings ∗ own_graph q (x [↦] (w1, w2))
+ ∗ cinv_own κ k) ⊢
+ WP (unmark_snd #x)
+ {{ _, own_graph q (x [↦] (w1, None)) ∗ cinv_own κ k }}.
+ Proof.
+ iIntros (Hgx) "(#Hgr & Hx & key)".
+ wp_let. wp_bind (! _)%E.
+ iApply wp_wand_l; iSplitR;
+ [|iApply wp_load_graph; eauto; iFrame "Hgr"; by iFrame].
+ iIntros (u) "(H1 & Hagree & Hx & key)". iDestruct "H1" as (m) "[Hmrk Hu]".
+ iDestruct "Hagree" as %Hagree.
+ iDestruct "Hmrk" as %Hmrk; iDestruct "Hu" as %Hu; subst.
+ wp_let. wp_bind (Fst _). do 3 wp_proj.
+ iApply (wp_store_graph _ (w1, None) with "[Hx key]"); eauto;
+ [|iFrame "Hgr"; by iFrame].
+ { by destruct w1; destruct w2; destruct v; inversion Hagree; subst. }
+ Qed.
+
+ Lemma front_op (g : graph loc) (G G' : Gmon) (t : gset loc) :
+ front g (dom (gset _) G) t → front g (dom (gset _) G') t →
+ front g (dom (gset _) (G â‹… G')) t.
+ Proof.
+ rewrite dom_op. intros [HGd HGf] [HGd' HGf']; split.
+ - intros x; rewrite elem_of_union; intuition.
+ - intros x y; rewrite elem_of_union; intuition eauto.
+ Qed.
+ Lemma front_singleton (g : graph loc) (t : gset loc) l (w : chlC) u1 u2 :
+ g !! l = Some (u1, u2) →
+ match u1 with |Some l1 => l1 ∈ t | None => True end →
+ match u2 with |Some l2 => l2 ∈ t | None => True end →
+ front g (dom (gset loc) (l [↦] w : gmap loc _)) t.
+ Proof.
+ intros Hgl Hu1 Hu2.
+ split => [x |x y]; rewrite ?dom_singleton ?elem_of_singleton => ?; subst.
+ - rewrite elem_of_dom Hgl; eauto.
+ - rewrite /get_left /get_right Hgl /=.
+ destruct u1; destruct u2; simpl; intros [Heq|Heq]; by inversion Heq; subst.
+ Qed.
+ Lemma empty_graph_divide q :
+ own_graph q ∅ ⊢ own_graph (q / 2) ∅ ∗ own_graph (q / 2) ∅.
+ Proof.
+ setoid_replace (∅ : gmapR loc (exclR chlC)) with
+ (∅ ⋅ ∅ : gmapR loc (exclR chlC)) at 1 by (by rewrite ucmra_unit_left_id).
+ by rewrite graph_divide.
+ Qed.
+
+ Lemma front_marked (g : graph loc) (l : loc) u1 u2 w mr1 mr2 (G1 G2 : Gmon) :
+ g !! l = Some (u1, u2) →
+ (front g (dom (gset _) G1) mr1) → (front g (dom (gset _) G2) mr2) →
+ ([∗ set] l ∈ mr1, is_marked l) ∗ ([∗ set] l ∈ mr2, is_marked l) ∗
+ match u1 with |Some l1 => is_marked l1 | None => True end ∗
+ match u2 with |Some l2 => is_marked l2 | None => True end ⊢
+ ∃ (mr : gset loc), ⌜front g (dom (gset loc) ((l [↦] w) â‹… (G1 â‹… G2))) mrâŒ
+ ∗ ([∗ set] l ∈ mr, is_marked l).
+ Proof.
+ iIntros (Hgl Hfr1 Hfr2) "(Hmr1 & Hmr2 & Hu1 & Hu2)".
+ iExists (match u1 with |Some l1 => {[l1]} | None => ∅ end ∪
+ match u2 with |Some l2 => {[l2]} | None => ∅ end ∪ mr1 ∪ mr2).
+ iSplitR; [iPureIntro|].
+ - repeat apply front_op.
+ + eapply front_singleton; eauto; simpl; destruct u1; destruct u2; trivial;
+ rewrite ?elem_of_union ?elem_of_singleton; intuition.
+ + eapply front_mono; eauto => x. rewrite ?elem_of_union; intuition.
+ + eapply front_mono; eauto => x. rewrite ?elem_of_union; intuition.
+ - rewrite ?big_sepS_forall. iIntros (x); destruct u1; destruct u2;
+ rewrite ?elem_of_union ?elem_of_empty ?elem_of_singleton; iIntros (Hx);
+ intuition; subst; auto; solve [iApply "Hmr1"; auto|iApply "Hmr2"; auto].
+ Qed.
+
+ Lemma rec_wp_span g markings k q (x : val) :
+ maximal g →
+ (x = NONEV ∨ ∃ l : loc,
+ x = SOMEV #l ∧ l ∈ dom (gset _) g) →
+ (graph_ctx κ g markings ∗ own_graph q ∅ ∗ cinv_own κ k)
+ ⊢
+ WP (span x)
+ {{ v, ((⌜v = # true⌠∗
+ (∃ l : loc, ⌜x = SOMEV #l⌠∗
+ (∃ (G : Gmon) mr (tr : tree (Gmon_graph G) l),
+ own_graph q G ∗ ⌜l ∈ dom (gset _) G⌠∗
+ ⌜maximal (Gmon_graph G)⌠∗ ⌜front g (dom (gset _) G) mr⌠∗
+ ([∗ set] l ∈ mr , is_marked l)) ∗ is_marked l)) ∨
+ (⌜v = # false⌠∗
+ (⌜x = NONEV⌠∨ (∃ l : loc, ⌜x = SOMEV #l⌠∗ is_marked l))
+ ∗ own_graph q ∅))
+ ∗ cinv_own κ k
+ }}.
+ Proof.
+ intros [_ Hgmx] Hxpt. iIntros "(#Hgr & Hx & key)".
+ iRevert (x Hxpt k q) "key Hx". iLöb as "IH".
+ iIntros (x Hxpt k q) "key Hx".
+ wp_rec.
+ destruct Hxpt as [|[l [? Hgsl]]]; subst.
+ { wp_match.
+ iFrame; iRight; iFrame; repeat iSplit; trivial; by iLeft. }
+ wp_match. wp_bind (try_mark _).
+ iDestruct (empty_graph_divide with "Hx") as "[Hx1 Hx2]".
+ iApply wp_wand_l; iSplitL "Hx1";
+ [|iApply wp_try_mark; try iFrame]; eauto; simpl.
+ iIntros (v) "[(% & Hv & Hm & key)|(% & Hx2 & Hm & key)]"; subst;
+ [|iCombine "Hx1" "Hx2" as "Hx"; rewrite -graph_divide ucmra_unit_right_id;
+ wp_if; iFrame; iRight; iFrame; iSplit; trivial; iRight;
+ iExists _; eauto].
+ iDestruct "Hv" as (u) "[Hgl Hl]". iDestruct "Hgl" as %Hgl.
+ wp_if.
+ (* reading the reference. This part is very similar to unmark lemmas! *)
+ wp_bind (! _)%E.
+ iApply wp_wand_l; iSplitR "Hl key";
+ [|iApply wp_load_graph; eauto; iFrame "Hgr"; by iFrame].
+ iIntros (v) "(H1 & Hagree & Hx & key)". iDestruct "H1" as (m) "[Hmrk Hv]".
+ iDestruct "Hagree" as %Hagree. iDestruct "Hv" as %Hv; subst v.
+ wp_let. wp_bind (par _).
+ iDestruct "key" as "[K1 K2]".
+ iDestruct (empty_graph_divide with "Hx1") as "[Hx11 Hx12]".
+ destruct u as [u1 u2]. iApply (par_spec with "[Hx11 K1] [Hx12 K2]").
+ (* symbolically executing the left part of the par. *)
+ wp_lam; repeat wp_proj.
+ assert ((child_to_val u1) = NONEV
+ ∨ (∃ l : loc,
+ (child_to_val u1) = SOMEV #l ∧ l ∈ dom (gset _) g)) as Hlf.
+ { destruct u1 as [l1|]; [right |by left].
+ exists l1; split; trivial. eapply (Hgmx l); rewrite // /get_left Hgl; auto. }
+ iApply ("IH" with "[#] * [K1] [Hx11]"); auto.
+ (* symbolically executing the left part of the par. *)
+ wp_lam; repeat wp_proj.
+ assert ((child_to_val u2) = NONEV
+ ∨ (∃ l : loc,
+ (child_to_val u2) = SOMEV #l ∧ l ∈ dom (gset _) g)) as Hrh.
+ { destruct u2 as [l2|]; [right |by left].
+ exists l2; split; trivial. eapply (Hgmx l); rewrite // /get_right Hgl; auto. }
+ iApply ("IH" with "[#] * [K2] [Hx12]"); auto.
+ (* continuing after both children are processed *)
+ iNext.
+ iIntros (vl vr) "([Hvl K1] & Hvr & K2 & K2')".
+ iCombine "K2" "K2'" as "K2". iCombine "K1" "K2" as "key".
+ iNext. wp_let.
+ (* We don't need the huge induction hypothesis anymore. *)
+ iClear "IH".
+ (* separating all four cases *)
+ iDestruct "Hvl" as "[[% Hvll]|[% Hvlr]]"; subst;
+ iDestruct "Hvr" as "[[% Hvrl]|[% Hvrr]]"; subst.
+ - wp_proj. wp_op. wp_if; wp_seq. wp_proj. wp_op. wp_if. wp_seq.
+ iDestruct "Hvll" as (l1) "(Hl1eq & Hg1 & ml1)".
+ iDestruct "Hg1" as (G1 mr1 tr1) "(Hxl & Hl1im & Hmx1 & Hfr1 & Hfml)".
+ iDestruct "Hfr1" as %Hfr1. iDestruct "Hmx1" as %Hmx1.
+ iDestruct "Hl1eq" as %Hl1eq. iDestruct "Hl1im" as %Hl1im.
+ iDestruct "Hvrl" as (l2) "(Hl2eq & Hg2 & ml2)".
+ iDestruct "Hg2" as (G2 mr2 tr2) "(Hxr & Hl2im & Hmx2 & Hfr2 & Hfmr)".
+ iDestruct "Hfr2" as %Hfr2. iDestruct "Hmx2" as %Hmx2.
+ iDestruct "Hl2eq" as %Hl2eq. iDestruct "Hl2im" as %Hl2im.
+ iCombine "Hxl" "Hxr" as "Hxlr". rewrite -graph_divide.
+ iCombine "Hx" "Hxlr" as "Hx". rewrite -graph_divide.
+ destruct u1; destruct u2; inversion Hl1eq; inversion Hl2eq; subst.
+ iFrame; iLeft. iSplit; [trivial|].
+ iExists _; iSplit; [trivial|]. iFrame.
+ iDestruct (own_graph_valid with "Hx") as %Hvl.
+ iExists ({[l := Excl (Some l1, Some l2)]} â‹… (G1 â‹… G2)).
+ iDestruct (front_marked _ _ _ _ (Some l1, Some l2) _ _ G1 G2 with
+ "[ml1 ml2 Hfml Hfmr]") as (mr)"[Hfr Hfm]"; eauto. iDestruct "Hfr" as %Hfr.
+ iExists mr.
+ unshelve iExists _; [eapply maximally_marked_tree_both; eauto|].
+ iFrame. iSplit; try iPureIntro; eauto.
+ { rewrite dom_op dom_singleton elem_of_union elem_of_singleton; by left. }
+ split; auto.
+ { eapply maximally_marked_tree_both; eauto. }
+ - wp_proj. wp_op. wp_if. wp_seq. wp_proj. wp_op. wp_if.
+ iDestruct "Hvll" as (l1) "(Hl1eq & Hg1 & ml1)".
+ iDestruct "Hg1" as (G1 mr1 tr1) "(Hxl & Hl1im & Hmx1 & Hfr1 & Hfml)".
+ iDestruct "Hfr1" as %Hfr1. iDestruct "Hmx1" as %Hmx1.
+ iDestruct "Hl1eq" as %Hl1eq. iDestruct "Hl1im" as %Hl1im.
+ iDestruct "Hvrr" as "(Hvr & Hxr)".
+ iCombine "Hxl" "Hxr" as "Hxlr". rewrite -graph_divide ucmra_unit_right_id.
+ wp_bind (unmark_snd _).
+ iApply wp_wand_l; iSplitR "Hx key";
+ [|iApply wp_unmark_snd; eauto; by iFrame "Hgr"; iFrame].
+ iIntros (v) "[Hx key]".
+ iCombine "Hx" "Hxlr" as "Hx". rewrite -graph_divide.
+ wp_seq.
+ iFrame; iLeft. iSplit; [trivial|].
+ iExists _; iSplit; [trivial|]. iFrame.
+ iDestruct (own_graph_valid with "Hx") as %Hvld.
+ iExists ({[l := Excl (u1, None)]} â‹… G1).
+ destruct u1; inversion Hl1eq; subst.
+ iDestruct (front_marked _ _ _ _ (Some l1, None) _ ∅ G1 ∅ with
+ "[ml1 Hvr Hfml]") as (mr)"[Hfr Hfm]"; eauto.
+ { rewrite dom_empty_L; apply front_empty. }
+ { rewrite big_sepS_empty. iFrame.
+ destruct u2; iDestruct "Hvr" as "[Hvr|Hvr]"; trivial;
+ [iDestruct "Hvr" as %Hvr; inversion Hvr|
+ iDestruct "Hvr" as (l2) "[Hvreq Hvr]"; iDestruct "Hvreq" as %Hvreq;
+ by inversion Hvreq]. }
+ iDestruct "Hfr" as %Hfr. rewrite right_id_L in Hfr.
+ iExists mr.
+ unshelve iExists _; [eapply maximally_marked_tree_left; eauto|].
+ iFrame. iSplit; try iPureIntro; eauto.
+ { rewrite dom_op dom_singleton elem_of_union elem_of_singleton; by left. }
+ split; auto.
+ { eapply maximally_marked_tree_left; eauto. }
+ - wp_proj. wp_op. wp_if.
+ iDestruct "Hvlr" as "(Hvl & Hxl)".
+ iDestruct "Hvrl" as (l2) "(Hl2eq & Hg2 & ml2)".
+ iDestruct "Hg2" as (G2 mr2 tr2) "(Hxr & Hl2im & Hmx2 & Hfr2 & Hfmr)".
+ iDestruct "Hfr2" as %Hfr2. iDestruct "Hmx2" as %Hmx2.
+ iDestruct "Hl2eq" as %Hl2eq. iDestruct "Hl2im" as %Hl1im.
+ iCombine "Hxl" "Hxr" as "Hxlr". rewrite -graph_divide left_id.
+ wp_bind (unmark_fst _).
+ iApply wp_wand_l; iSplitR "Hx key";
+ [|iApply wp_unmark_fst; eauto; by iFrame "Hgr"; iFrame].
+ iIntros (v) "[Hx key]".
+ iCombine "Hx" "Hxlr" as "Hx". rewrite -graph_divide.
+ wp_seq. wp_proj. wp_op. wp_if. wp_seq.
+ iFrame; iLeft. iSplit; [trivial|].
+ iExists _; iSplit; [trivial|]. iFrame.
+ iDestruct (own_graph_valid with "Hx") as %Hvld.
+ iExists ({[l := Excl (None, u2)]} â‹… G2).
+ destruct u2; inversion Hl2eq; subst.
+ iDestruct (front_marked _ _ _ _ (None, Some l2) ∅ _ ∅ G2 with
+ "[ml2 Hvl Hfmr]") as (mr)"[Hfr Hfm]"; eauto.
+ { rewrite dom_empty_L; apply front_empty. }
+ { rewrite big_sepS_empty. iFrame.
+ destruct u1; iDestruct "Hvl" as "[Hvl|Hvl]"; trivial;
+ [iDestruct "Hvl" as %Hvl; inversion Hvl|
+ iDestruct "Hvl" as (l1) "[Hvleq Hvl]"; iDestruct "Hvleq" as %Hvleq;
+ by inversion Hvleq]. }
+ iDestruct "Hfr" as %Hfr. rewrite left_id_L in Hfr.
+ iExists mr.
+ unshelve iExists _; [eapply maximally_marked_tree_right; eauto|].
+ iFrame. iSplit; try iPureIntro; eauto.
+ { rewrite dom_op dom_singleton elem_of_union elem_of_singleton; by left. }
+ split; auto.
+ { eapply maximally_marked_tree_right; eauto. }
+ - iDestruct "Hvlr" as "(Hvl & Hxl)".
+ iDestruct "Hvrr" as "(Hvr & Hxr)".
+ iCombine "Hxl" "Hxr" as "Hxlr". rewrite -graph_divide ucmra_unit_right_id.
+ wp_proj. wp_op. wp_if. wp_bind(unmark_fst _).
+ iApply wp_wand_l; iSplitR "Hx key";
+ [|iApply wp_unmark_fst; eauto; by iFrame "Hgr"; iFrame].
+ iIntros (v) "[Hx key]".
+ wp_seq. wp_proj. wp_op. wp_if. wp_bind(unmark_snd _).
+ iApply wp_wand_l; iSplitR "Hx key";
+ [|iApply wp_unmark_snd; eauto; by iFrame "Hgr"; iFrame].
+ clear v. iIntros (v) "[Hx key]".
+ iCombine "Hx" "Hxlr" as "Hx". rewrite -graph_divide.
+ wp_seq.
+ iFrame; iLeft. iSplit; [trivial|].
+ iExists _; iSplit; [trivial|]. iFrame.
+ iDestruct (own_graph_valid with "Hx") as %Hvld.
+ iExists ({[l := Excl (None, None)]} ⋅ ∅).
+ iDestruct (front_marked _ _ _ _ (None, None) ∅ ∅ ∅ ∅ with
+ "[Hvr Hvl]") as (mr)"[Hfr Hfm]"; eauto.
+ { rewrite dom_empty_L; apply front_empty. }
+ { rewrite dom_empty_L; apply front_empty. }
+ { rewrite big_sepS_empty.
+ destruct u1; iDestruct "Hvl" as "[Hvl|Hvl]";
+ destruct u2; iDestruct "Hvr" as "[Hvr|Hvr]";
+ try (iDestruct "Hvl" as %Hvl; inversion Hvl);
+ try (iDestruct "Hvr" as %Hvr; inversion Hvr);
+ try (iDestruct "Hvl" as (ll) "[Hvleq Hvl]";
+ iDestruct "Hvleq" as %Hvleq; inversion Hvleq);
+ try (iDestruct "Hvr" as (lr) "[Hvreq Hvr]";
+ iDestruct "Hvreq" as %Hvreq; inversion Hvreq);
+ iFrame; by repeat iSplit. }
+ iDestruct "Hfr" as %Hfr. rewrite left_id_L in Hfr.
+ iExists mr.
+ rewrite right_id_L. rewrite right_id_L in Hvld Hfr.
+ unshelve iExists _; [eapply maximally_marked_tree_none; eauto|].
+ iFrame. iSplit; try iPureIntro; eauto.
+ { by rewrite dom_singleton elem_of_singleton. }
+ split; auto.
+ { eapply maximally_marked_tree_none; eauto. }
+ Qed.
+
+End Helpers.
\ No newline at end of file