Merge branch 'amin/spanning' into 'master'

Add the spanning tree algorithm.

Closes #3

See merge request FP/iris-examples!3

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
 

_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

theories/spanning_tree/graph.v

+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

theories/spanning_tree/mon.v

+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.

theories/spanning_tree/proof.v

+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

theories/spanning_tree/spanning.v

+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