Neven Villani · Ralf Jung · e4813c39 · e4813c39 · e4813c39 · e4813c39
--- a/theories/tree_borrows/logical_state.v
+++ b/theories/tree_borrows/logical_state.v
 Global Instance subG_bor_stateΣ Σ :
  subG bor_stateΣ Σ → bor_stateGpreS Σ.
 Proof. solve_inG. Qed.

+Section utils.
+
+  Record item_for_loc : Type := {
+    lperm : lazy_permission;
+    tg : tag;
+    cid : option protector;
+  }.
+
+  Inductive item_for_loc_in_tree (i : item_for_loc) (tree : tree item) (l' : Z) : Prop :=
+    is_in_tree item :
+        exists_node (IsTag i.(tg)) tree →
+        every_node (λ i', i.(tg) = i'.(itag) → i' = item) tree →
--- a/theories/tree_borrows/logical_state.v
+++ b/theories/tree_borrows/logical_state.v
+    tg : tag;
+    cid : option protector;
+  }.
+
+  Inductive item_for_loc_in_tree (i : item_for_loc) (tree : tree item) (l' : Z) : Prop :=
+    is_in_tree item :
+        exists_node (IsTag i.(tg)) tree →
+        every_node (λ i', i.(tg) = i'.(itag) → i' = item) tree →
+        i.(cid) = item.(iprot) →
+        i.(lperm) = default {| initialized := PermLazy; perm := item.(initp) |}
+                           (item.(iperm) !! l') →
+        item_for_loc_in_tree i tree l'.
+
+  Inductive item_for_loc_in_trees (i : item_for_loc) (t : trees) (l : loc) : Prop :=
+    is_in_trees tree :
+        t !! (fst l) = Some tree → item_for_loc_in_tree i tree (snd l) → item_for_loc_in_trees i t l.
--- a/theories/tree_borrows/logical_state.v
+++ b/theories/tree_borrows/logical_state.v
+        t !! (fst l) = Some tree → item_for_loc_in_tree i tree (snd l) → item_for_loc_in_trees i t l.
+
+  Context (C : gset call_id).
+
+  Inductive protected_by: option protector → Prop := 
+    is_protected_by p :
+        p.(call) ∈ C → protected_by (Some p).
+
+  Inductive pseudo_conflicted (tr : tree item) (l : Z) (tg1 : tag) : res_conflicted → option protector → Prop :=
+    pseudo_conflicted_conflicted c :
+        protected_by c →
+        pseudo_conflicted tr l tg1 ResConflicted c
+  | pseudo_conflicted_cousin_init conf c it :
+        protected_by c →
+        item_for_loc_in_tree it tr l →
+        rel_dec tr it.(tg) tg1 = Uncle →
--- a/theories/tree_borrows/logical_state.v
+++ b/theories/tree_borrows/logical_state.v
  Section defs.
    (* We need all the maps from the tag interpretation here....
     TODO: can we make that more beautiful? all the different invariants are interleaved in subtle ways, which makes modular reasoning really hard... *)
-    Context (M_tag : gmap ptr_id (tag_kind * unit)) (M_t M_s : gmap (ptr_id * loc) scalar) (Mcall_t : gmap call_id (gmap ptr_id (gset loc))).
+    Context (M_tag : gmap nat (tag_kind * unit)) (M_t M_s : gmap (nat * loc) scalar) (Mcall_t : gmap call_id (gmap nat (gset loc))).
--- a/theories/tree_borrows/logical_state.v
+++ b/theories/tree_borrows/logical_state.v
    state_rel M_tag M_t Mcall σ_t σ_s -∗
    pub_loc sc_rel σ_t σ_s l ∨ ⌜∃ t, priv_loc M_tag M_t Mcall t l⌝.
  Proof.
+From simuliris.stacked_borrows Require Import steps_progress steps_retag.
--- a/theories/tree_borrows/logical_state.v
+++ b/theories/tree_borrows/logical_state.v
  Lemma loc_controlled_local_authoritative l t t' tk' sc sc' σ f :
    loc_controlled l t tk_local sc (state_upd_mem f σ) →
    loc_controlled l t' tk' sc' σ →
+From simuliris.stacked_borrows Require Import steps_progress steps_retag.