From 2894a20f4d996edec8a56789aa50bf2b18a8c311 Mon Sep 17 00:00:00 2001
From: Johannes Hostert <jhostert@ethz.ch>
Date: Fri, 14 Mar 2025 14:54:34 +0100
Subject: [PATCH] huge TB cleanup

---
 _CoqProject                                   |   3 +-
 theories/tree_borrows/bor_semantics.v         |   5 +-
 theories/tree_borrows/defs.v                  |   4 -
 .../protected/mutable_reorder_read_down.v     |   4 -
 .../protected/mutable_reorder_read_up.v       |   4 -
 .../mutable_reorder_write_down_activated.v    |   4 -
 .../mutable_reorder_write_up_activated.v      |   4 -
 ...mutable_reorder_write_up_activated_paper.v |   4 -
 .../examples/protected/shared_insert_read.v   |   4 -
 .../shared_reorder_read_down_escaped.v        |   4 -
 .../shared_reorder_read_up_escaped.v          |   4 -
 .../unprotected/mutable_delete_read.v         |   4 -
 .../unprotected/shared_delete_read_escaped.v  |   4 -
 theories/tree_borrows/expr_semantics.v        |   4 -
 theories/tree_borrows/helpers.v               |   4 -
 theories/tree_borrows/lang.v                  |   4 -
 theories/tree_borrows/locations.v             |   4 -
 theories/tree_borrows/notation.v              |   4 -
 theories/tree_borrows/steps_access.v          | 109 ------------------
 theories/tree_borrows/steps_foreach.v         | 106 ++++++++++++++++-
 theories/tree_borrows/steps_progress.v        |   4 -
 theories/tree_borrows/steps_wf.v              |  55 +--------
 theories/tree_borrows/tkmap_view.v            |  10 +-
 theories/tree_borrows/tree_lemmas.v           |  59 +---------
 .../trees_equal/disabled_in_practice.v        |   1 -
 .../tree_borrows/trees_equal/random_lemmas.v  |   1 -
 .../trees_equal/trees_equal_asymmetric_prot.v |   1 -
 .../trees_equal/trees_equal_base.v            |   1 -
 .../trees_equal/trees_equal_create_child.v    |   1 -
 .../trees_equal/trees_equal_initcall.v        |   1 -
 .../trees_equal/trees_equal_more_access.v     |   1 -
 .../trees_equal_preserved_by_access.v         |   1 -
 .../trees_equal_preserved_by_access_base.v    |   1 -
 .../trees_equal/trees_equal_source_read.v     |   1 -
 .../trees_equal/trees_equal_transitivity.v    |   1 -
 35 files changed, 120 insertions(+), 306 deletions(-)
 delete mode 100755 theories/tree_borrows/steps_access.v

diff --git a/_CoqProject b/_CoqProject
index 45e51474..3f81f7a4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -124,7 +124,7 @@ theories/stacked_borrows/examples/coinductive.v
 
 
 ## Tree Borrows
-theories/tree_borrows/helpers.v
+# theories/tree_borrows/helpers.v
 theories/tree_borrows/locations.v
 theories/tree_borrows/lang_base.v
 theories/tree_borrows/notation.v
@@ -139,7 +139,6 @@ theories/tree_borrows/lang.v
 # Actual Simuliris proof content for TB
 theories/tree_borrows/defs.v
 theories/tree_borrows/steps_foreach.v
-theories/tree_borrows/steps_access.v
 theories/tree_borrows/steps_preserve.v
 theories/tree_borrows/steps_wf.v
 theories/tree_borrows/steps_progress.v
diff --git a/theories/tree_borrows/bor_semantics.v b/theories/tree_borrows/bor_semantics.v
index 4fba6c16..79a8ea91 100755
--- a/theories/tree_borrows/bor_semantics.v
+++ b/theories/tree_borrows/bor_semantics.v
@@ -17,7 +17,7 @@ From Equations Require Import Equations.
 From iris.prelude Require Import prelude options.
 From stdpp Require Export gmap.
 
-From simuliris.tree_borrows Require Export lang_base notation tree tree_lemmas.
+From simuliris.tree_borrows Require Export lang_base notation tree  locations.
 From iris.prelude Require Import options.
 
 (*** TREE BORROWS SEMANTICS ---------------------------------------------***)
@@ -995,6 +995,7 @@ Inductive bor_steps trs cids nxtp nxtc
         trs2 cids2 nxtp2 nxtc2
   .
 
+(** Unit test for the tree relation definition, showing how it works *)
 (* conversion is magic *)
 Local Definition unpack_option {A:Type} (o : option A) {oo : A} (Heq : o = Some oo) : A := oo.
 Local Notation unwrap K := (unpack_option K eq_refl).
@@ -1016,6 +1017,8 @@ Local Definition with_three_children :=
 In particular, 4 is a non-immediate child of 1, but all other child relations are immediate.
 
 *)
+
+(** Having constructed the above tree, we can now check that all relations are computed correctly *)
 (* conversion keeps being magical *)
 Succeed Example foo : rel_dec with_three_children 1 1 = Child This                   := eq_refl.
 Succeed Example foo : rel_dec with_three_children 1 2 = Foreign (Parent Immediate)   := eq_refl.
diff --git a/theories/tree_borrows/defs.v b/theories/tree_borrows/defs.v
index e9f1a8c8..8f8c276b 100755
--- a/theories/tree_borrows/defs.v
+++ b/theories/tree_borrows/defs.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From iris.prelude Require Export prelude.
 From simuliris.tree_borrows Require Export tactics notation lang bor_semantics bor_lemmas.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_read_down.v b/theories/tree_borrows/examples/protected/mutable_reorder_read_down.v
index 2c49abb3..e9b73792 100755
--- a/theories/tree_borrows/examples/protected/mutable_reorder_read_down.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_read_down.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import primitive_laws proofmode examples.lib adequacy.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_read_up.v b/theories/tree_borrows/examples/protected/mutable_reorder_read_up.v
index 39171b47..fce0c9e8 100755
--- a/theories/tree_borrows/examples/protected/mutable_reorder_read_up.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_read_up.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import primitive_laws proofmode examples.lib adequacy.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v b/theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v
index ae4933d0..1ad1d78a 100755
--- a/theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v b/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v
index a12caee7..5e02c635 100755
--- a/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v b/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v
index 78508609..dc7f4e69 100644
--- a/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/shared_insert_read.v b/theories/tree_borrows/examples/protected/shared_insert_read.v
index 207ddd86..3cec5d57 100644
--- a/theories/tree_borrows/examples/protected/shared_insert_read.v
+++ b/theories/tree_borrows/examples/protected/shared_insert_read.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v b/theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v
index ffa0acf2..3aef4400 100755
--- a/theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v
+++ b/theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang examples.lib adequacy.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v b/theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v
index 303d4c54..8b1634f4 100755
--- a/theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v
+++ b/theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/unprotected/mutable_delete_read.v b/theories/tree_borrows/examples/unprotected/mutable_delete_read.v
index 910a6bb0..09d2f2e2 100644
--- a/theories/tree_borrows/examples/unprotected/mutable_delete_read.v
+++ b/theories/tree_borrows/examples/unprotected/mutable_delete_read.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v b/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v
index 74a81dc4..a82d996b 100644
--- a/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v
+++ b/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/expr_semantics.v b/theories/tree_borrows/expr_semantics.v
index a2a97289..d658e991 100755
--- a/theories/tree_borrows/expr_semantics.v
+++ b/theories/tree_borrows/expr_semantics.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From Equations Require Import Equations.
 From iris.prelude Require Import prelude options.
 From stdpp Require Export gmap.
diff --git a/theories/tree_borrows/helpers.v b/theories/tree_borrows/helpers.v
index 7e2a01e0..2da99c05 100755
--- a/theories/tree_borrows/helpers.v
+++ b/theories/tree_borrows/helpers.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From Coq Require Import ssreflect.
 From stdpp Require Export list gmap.
 From iris.prelude Require Export prelude.
diff --git a/theories/tree_borrows/lang.v b/theories/tree_borrows/lang.v
index 8afd7c3a..89d58619 100755
--- a/theories/tree_borrows/lang.v
+++ b/theories/tree_borrows/lang.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 (** This file manages the interface between the expression semantics and
    the borrow semantics. *)
 
diff --git a/theories/tree_borrows/locations.v b/theories/tree_borrows/locations.v
index b8ce6b0a..c2feb533 100755
--- a/theories/tree_borrows/locations.v
+++ b/theories/tree_borrows/locations.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 (** Internal representation of memory.
     We opt for a view in which a location is composed of
     an allocation id and an offset into that allocation. *)
diff --git a/theories/tree_borrows/notation.v b/theories/tree_borrows/notation.v
index d150892e..d3bb1ec7 100755
--- a/theories/tree_borrows/notation.v
+++ b/theories/tree_borrows/notation.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From iris.prelude Require Import prelude options.
 From simuliris.tree_borrows Require Export lang_base.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/steps_access.v b/theories/tree_borrows/steps_access.v
deleted file mode 100755
index 6d2bad74..00000000
--- a/theories/tree_borrows/steps_access.v
+++ /dev/null
@@ -1,109 +0,0 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
-From simuliris.tree_borrows Require Export defs steps_foreach.
-From iris.prelude Require Import options.
-
-Lemma free_mem_lookup l n h :
-  (∀ (i: nat), (i < n)%nat → free_mem l n h !! (l +ₗ i) = None) ∧
-  (∀ (l': loc), (∀ (i: nat), (i < n)%nat → l' ≠ l +ₗ i) →
-    free_mem l n h !! l' = h !! l').
-Proof.
-  revert l. induction n as [|n IH]; intros l; simpl.
-  { split; intros ??; by [lia|]. } split.
-  - intros i Lt. destruct i as [|i].
-    + rewrite shift_loc_0 lookup_delete //.
-    + rewrite lookup_delete_ne.
-      * specialize (IH (l +â‚— 1))as [IH _].
-        rewrite (_: l +â‚— S i = l +â‚— 1 +â‚— i).
-        { apply IH. lia. }
-        { rewrite shift_loc_assoc. f_equal. lia. }
-      * rewrite -{1}(shift_loc_0 l).
-        move => /shift_loc_inj ?. lia.
-  - intros l' Lt.
-    rewrite lookup_delete_ne.
-    + apply IH. intros i Lti.
-      rewrite (_: l +â‚— 1 +â‚— i = l +â‚— S i).
-      * apply Lt. lia.
-      * rewrite shift_loc_assoc. f_equal. lia.
-    + rewrite -(shift_loc_0_nat l). intros ?. subst l'. apply (Lt O); [lia|done].
-Qed.
-
-Lemma free_mem_lookup_case l' l n h :
-  (∀ i : nat, (i < n)%nat → l' ≠ l +ₗ i) ∧ free_mem l n h !! l' = h !! l' ∨
-  ∃ i : nat, (i < n)%nat ∧ l' = l +ₗ i ∧ free_mem l n h !! (l +ₗ i) = None.
-Proof.
-  destruct (free_mem_lookup l n h) as [EQ1 EQ2].
-  destruct (block_case l l' n) as [NEql|Eql].
-  - left. rewrite -EQ2 //.
-  - right. destruct Eql as (i & Lt & ?). exists i. do 2 (split; [done|]).
-    subst l'. by apply EQ1.
-Qed.
-
-Lemma free_mem_dom_inv l' l n h:
-  l' ∈ dom (free_mem l n h) →
-  l' ∈ dom h ∧
-  (∀ i : nat, (i < n)%nat → l' ≠ l +ₗ i) ∧ free_mem l n h !! l' = h !! l'.
-Proof.
-  intros [? EqD]%elem_of_dom.
-  destruct (free_mem_lookup_case l' l n h) as [Eqn|(i & Lt & ? & EqN)].
-  - split; [|done]. apply elem_of_dom. destruct Eqn as [? Eqn].
-    rewrite -Eqn. by eexists.
-  - exfalso. subst l'. by rewrite EqD in EqN.
-Qed.
-
-
-
-Lemma init_mem_lookup_fresh_poison blk off (n:nat) h :
-  0 ≤ off ∧ off < n →
-  init_mem (blk, 0) n h !! (blk, off) = Some ScPoison.
-Proof.
-  intros (Hpos & Hlt).
-  pose proof (init_mem_lookup (blk, 0) n h) as (Hinit1&_).
-  ospecialize (Hinit1 (Z.to_nat off) _); first lia.
-  rewrite /= /shift_loc /= Z.add_0_l Z2Nat.id // in Hinit1.
-Qed.
-
-Lemma init_mem_lookup_fresh_None blk off (n:nat) h :
-  (forall off, (blk, off) ∉ dom h) →
-  (off < 0 ∨ n ≤ off) →
-  init_mem (blk, 0) n h !! (blk, off) = None.
-Proof.
-  intros Hfresh Hout.
-  pose proof (init_mem_lookup (blk, 0) n h) as (_&Hinit2).
-  rewrite (Hinit2 (blk, off)).
-  + eapply not_elem_of_dom, Hfresh.
-  + intros i Hlt.
-    rewrite /= /shift_loc /= Z.add_0_l.
-    intros [= ->]. destruct Hout as [Hout|Hout]; lia.
-Qed.
-
-Lemma init_mem_lookup_fresh_old blk blk' off (n:nat) h :
-  blk ≠ blk' →
-  init_mem (blk, 0) n h !! (blk', off) = h !! (blk', off).
-Proof.
-  intros Hfresh.
-  pose proof (init_mem_lookup (blk, 0) n h) as (_&Hinit2).
-  apply Hinit2.
-  intros ? _ [=]. done.
-Qed.
-
-
-Lemma init_mem_lookup_fresh_inv blk blk' off (n:nat) h k :
-  (forall off, (blk, off) ∉ dom h) →
-  init_mem (blk, 0) n h !! (blk', off) = k →
-  (k = Some ScPoison ∧ blk = blk' ∧ 0 ≤ off ∧ off < n)
-∨ (k = None ∧ blk = blk' ∧ (off < 0 ∨ n ≤ off))
-∨ (k = h !! (blk', off) ∧ blk ≠ blk').
-Proof.
-  intros Hfresh Hinit.
-  destruct (decide (blk = blk')) as [Heqblk|Hne].
-  1: subst blk'; destruct (decide (0 ≤ off)) as [Hpos|Hneg].
-  1: destruct (decide (off < n)) as [Hlt|Hge].
-  { left. subst k. split_and!; try done. by rewrite init_mem_lookup_fresh_poison. }
-  1-2: right; left; split_and!; try done; last lia.
-  1-2: subst k; rewrite init_mem_lookup_fresh_None; try done; lia.
-  { right. right. split; last done. subst k. by apply init_mem_lookup_fresh_old. }
-Qed.
-
diff --git a/theories/tree_borrows/steps_foreach.v b/theories/tree_borrows/steps_foreach.v
index fd2b1206..ba77c310 100755
--- a/theories/tree_borrows/steps_foreach.v
+++ b/theories/tree_borrows/steps_foreach.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.tree_borrows Require Export defs.
 From iris.prelude Require Import options.
 
@@ -139,3 +135,105 @@ Lemma extend_trees_lookup_ne trs tg off sz blk blk' :
 Proof. apply lookup_insert_ne. Qed.
 
 
+Lemma free_mem_lookup l n h :
+  (∀ (i: nat), (i < n)%nat → free_mem l n h !! (l +ₗ i) = None) ∧
+  (∀ (l': loc), (∀ (i: nat), (i < n)%nat → l' ≠ l +ₗ i) →
+    free_mem l n h !! l' = h !! l').
+Proof.
+  revert l. induction n as [|n IH]; intros l; simpl.
+  { split; intros ??; by [lia|]. } split.
+  - intros i Lt. destruct i as [|i].
+    + rewrite shift_loc_0 lookup_delete //.
+    + rewrite lookup_delete_ne.
+      * specialize (IH (l +â‚— 1))as [IH _].
+        rewrite (_: l +â‚— S i = l +â‚— 1 +â‚— i).
+        { apply IH. lia. }
+        { rewrite shift_loc_assoc. f_equal. lia. }
+      * rewrite -{1}(shift_loc_0 l).
+        move => /shift_loc_inj ?. lia.
+  - intros l' Lt.
+    rewrite lookup_delete_ne.
+    + apply IH. intros i Lti.
+      rewrite (_: l +â‚— 1 +â‚— i = l +â‚— S i).
+      * apply Lt. lia.
+      * rewrite shift_loc_assoc. f_equal. lia.
+    + rewrite -(shift_loc_0_nat l). intros ?. subst l'. apply (Lt O); [lia|done].
+Qed.
+
+Lemma free_mem_lookup_case l' l n h :
+  (∀ i : nat, (i < n)%nat → l' ≠ l +ₗ i) ∧ free_mem l n h !! l' = h !! l' ∨
+  ∃ i : nat, (i < n)%nat ∧ l' = l +ₗ i ∧ free_mem l n h !! (l +ₗ i) = None.
+Proof.
+  destruct (free_mem_lookup l n h) as [EQ1 EQ2].
+  destruct (block_case l l' n) as [NEql|Eql].
+  - left. rewrite -EQ2 //.
+  - right. destruct Eql as (i & Lt & ?). exists i. do 2 (split; [done|]).
+    subst l'. by apply EQ1.
+Qed.
+
+Lemma free_mem_dom_inv l' l n h:
+  l' ∈ dom (free_mem l n h) →
+  l' ∈ dom h ∧
+  (∀ i : nat, (i < n)%nat → l' ≠ l +ₗ i) ∧ free_mem l n h !! l' = h !! l'.
+Proof.
+  intros [? EqD]%elem_of_dom.
+  destruct (free_mem_lookup_case l' l n h) as [Eqn|(i & Lt & ? & EqN)].
+  - split; [|done]. apply elem_of_dom. destruct Eqn as [? Eqn].
+    rewrite -Eqn. by eexists.
+  - exfalso. subst l'. by rewrite EqD in EqN.
+Qed.
+
+
+
+Lemma init_mem_lookup_fresh_poison blk off (n:nat) h :
+  0 ≤ off ∧ off < n →
+  init_mem (blk, 0) n h !! (blk, off) = Some ScPoison.
+Proof.
+  intros (Hpos & Hlt).
+  pose proof (init_mem_lookup (blk, 0) n h) as (Hinit1&_).
+  ospecialize (Hinit1 (Z.to_nat off) _); first lia.
+  rewrite /= /shift_loc /= Z.add_0_l Z2Nat.id // in Hinit1.
+Qed.
+
+Lemma init_mem_lookup_fresh_None blk off (n:nat) h :
+  (forall off, (blk, off) ∉ dom h) →
+  (off < 0 ∨ n ≤ off) →
+  init_mem (blk, 0) n h !! (blk, off) = None.
+Proof.
+  intros Hfresh Hout.
+  pose proof (init_mem_lookup (blk, 0) n h) as (_&Hinit2).
+  rewrite (Hinit2 (blk, off)).
+  + eapply not_elem_of_dom, Hfresh.
+  + intros i Hlt.
+    rewrite /= /shift_loc /= Z.add_0_l.
+    intros [= ->]. destruct Hout as [Hout|Hout]; lia.
+Qed.
+
+Lemma init_mem_lookup_fresh_old blk blk' off (n:nat) h :
+  blk ≠ blk' →
+  init_mem (blk, 0) n h !! (blk', off) = h !! (blk', off).
+Proof.
+  intros Hfresh.
+  pose proof (init_mem_lookup (blk, 0) n h) as (_&Hinit2).
+  apply Hinit2.
+  intros ? _ [=]. done.
+Qed.
+
+
+Lemma init_mem_lookup_fresh_inv blk blk' off (n:nat) h k :
+  (forall off, (blk, off) ∉ dom h) →
+  init_mem (blk, 0) n h !! (blk', off) = k →
+  (k = Some ScPoison ∧ blk = blk' ∧ 0 ≤ off ∧ off < n)
+∨ (k = None ∧ blk = blk' ∧ (off < 0 ∨ n ≤ off))
+∨ (k = h !! (blk', off) ∧ blk ≠ blk').
+Proof.
+  intros Hfresh Hinit.
+  destruct (decide (blk = blk')) as [Heqblk|Hne].
+  1: subst blk'; destruct (decide (0 ≤ off)) as [Hpos|Hneg].
+  1: destruct (decide (off < n)) as [Hlt|Hge].
+  { left. subst k. split_and!; try done. by rewrite init_mem_lookup_fresh_poison. }
+  1-2: right; left; split_and!; try done; last lia.
+  1-2: subst k; rewrite init_mem_lookup_fresh_None; try done; lia.
+  { right. right. split; last done. subst k. by apply init_mem_lookup_fresh_old. }
+Qed.
+
diff --git a/theories/tree_borrows/steps_progress.v b/theories/tree_borrows/steps_progress.v
index 81bacaf5..2fca45fb 100755
--- a/theories/tree_borrows/steps_progress.v
+++ b/theories/tree_borrows/steps_progress.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 (** Statements of success conditions for borrow steps.
     The goal is to be able to prove a [bor_step] statement. *)
 
diff --git a/theories/tree_borrows/steps_wf.v b/theories/tree_borrows/steps_wf.v
index d3b65255..4a2644ab 100755
--- a/theories/tree_borrows/steps_wf.v
+++ b/theories/tree_borrows/steps_wf.v
@@ -1,65 +1,22 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 (** The core idea of this file is to prove that all borrow steps preserve
     well-formedness of trees. *)
 
-From simuliris.tree_borrows Require Import helpers.
-From simuliris.tree_borrows Require Export defs steps_foreach steps_access steps_preserve bor_lemmas.
+From simuliris.tree_borrows Require Export defs tree_lemmas steps_foreach steps_preserve bor_lemmas.
 From iris.prelude Require Import options.
 
 (* weird GMAP stuff *)
 
-Lemma gmap_dep_fold_ind_strong {B A P} (f : positive → A → B → B) (Q : B → gmap_dep A P → Prop) (b : B) j :
-  Q b GEmpty →
-  (∀ i p x mt r, gmap.gmap_dep_lookup i mt = None →
-    r = gmap.gmap_dep_fold f j b mt →
-    (∀ B' f' (b':B'), (f' (Pos.reverse_go i j) x (gmap.gmap_dep_fold f' j b' mt)) = gmap.gmap_dep_fold f' j b' (gmap.gmap_dep_partial_alter (λ _, Some x) i p mt)) →
-    Q r mt →
-    Q (f (Pos.reverse_go i j) x r) (gmap.gmap_dep_partial_alter (λ _, Some x) i p mt)) →
-  ∀ mt, Q (gmap.gmap_dep_fold f j b mt) mt.
-Proof.
-  intros Hemp Hinsert mt. revert Q b j Hemp Hinsert.
-  induction mt as [|P ml mx mr ? IHl IHr] using gmap.gmap_dep_ind;
-    intros Q b j Hemp Hinsert; [done|].
-  rewrite gmap.gmap_dep_fold_GNode; try done.
-  apply (IHr (λ y mt, Q y (gmap.GNode ml mx mt))).
-  { apply (IHl (λ y mt, Q y (gmap.GNode mt mx GEmpty))).
-    { destruct mx as [[p x]|]; [|done].
-      replace (gmap.GNode gmap.GEmpty (Some (p,x)) gmap.GEmpty) with
-        (gmap.gmap_dep_partial_alter (λ _, Some x) 1 p gmap.GEmpty) by done.
-      by apply Hinsert. }
-    intros i p x mt r H1 H2 H3 H4.
-    replace (gmap.GNode (gmap.gmap_dep_partial_alter (λ _, Some x) i p mt) mx gmap.GEmpty)
-      with (gmap.gmap_dep_partial_alter (λ _, Some x) (i~0) p (gmap.GNode mt mx gmap.GEmpty))
-      by (by destruct mt, mx as [[]|]).
-    apply Hinsert. 1,4: by rewrite ?gmap.gmap_dep_lookup_GNode.
-    1: by destruct mt, mx as [[]|]; done.
-    intros B' f' b'. destruct mt, mx as [[]|]; simpl in *.
-    1: done. 1: done. all: rewrite H3; by destruct gmap.gmap_dep_ne_partial_alter. }
-  intros i p x mt r H1 H2 H3 H4.
-  replace (gmap.GNode ml mx (gmap.gmap_dep_partial_alter (λ _, Some x) i p mt))
-    with (gmap.gmap_dep_partial_alter (λ _, Some x) (i~1) p (gmap.GNode ml mx mt))
-    by (by destruct ml, mx as [[]|], mt).
-  apply Hinsert. all: rewrite ?gmap.gmap_dep_lookup_GNode; try done.
-  1: destruct ml, mx as [[]|], mt; simpl in *; done.
-  intros B' f' b'. destruct ml, mx as [[]|], mt; simpl in *.
-  1,3,5,7: done. all: rewrite H3; by destruct gmap.gmap_dep_ne_partial_alter.
-Qed.
 
 Lemma map_fold_ind_strong {K V B} `{Countable K} (P : B → gmap K V → Prop) (f : K → V → B → B) (b:B) (M : gmap K V) :
   P b ∅ →
   (∀ k v M, M !! k = None → (∀ B' f' (b':B'), map_fold f' b' (<[k:=v]> M) = f' k v (map_fold f' b' M)) → P (map_fold f b M) M → P (f k v (map_fold f b M)) (<[k:=v]> M)) →
   P (map_fold f b M) M.
 Proof.
-  intros H1 H2. destruct M as [M]. rewrite /map_fold /=.
-  apply (gmap_dep_fold_ind_strong _ (λ r M, P r (GMap M))); clear M; [done|].
-  intros i [Hk] x mt r H0 -> H3; simpl. destruct (fmap_Some_1 _ _ _ Hk) as (k&Hk1&Hk2). subst i.
-  rewrite Hk1.
-  assert (GMapKey Hk = gmap_key_encode k) as Hk3 by (apply proof_irrel). rewrite Hk3.
-  apply (H2 _ _ (GMap mt)). 1: done.
-  intros ???. simpl. rewrite /map_fold /gmap_fold /= -Hk3 -H3 /= Hk1 //.
+  intros Hbase Hstep. eapply (map_first_key_ind (fun mm => P (map_fold f b mm) mm)).
+  - rewrite map_fold_empty. apply Hbase.
+  - intros k v m Hnone Hfirstkey HIH.
+    rewrite map_fold_insert_first_key //. eapply Hstep; [done| |done].
+    intros B' f' b'. rewrite map_fold_insert_first_key //.
 Qed.
 
 
diff --git a/theories/tree_borrows/tkmap_view.v b/theories/tree_borrows/tkmap_view.v
index 0e0ff280..51c4c5fc 100755
--- a/theories/tree_borrows/tkmap_view.v
+++ b/theories/tree_borrows/tkmap_view.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Iris development, available at 
-  https://gitlab.mpi-sws.org/iris/iris
-*)
-
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export view gmap frac dfrac.
 From iris.algebra Require Import local_updates proofmode_classes big_op.
@@ -13,10 +9,10 @@ From simuliris.tree_borrows Require Export defs.
 (gmap_view has since been updated so we could now use it directly, but this code predates the generalized gmap_view for arbitrary CRMA.) *)
 
 (* Currently, we place a strong restriction on the shape of a location's stack:
-  A tag can be of one of two kinds:
+  A tag can be of one of several kinds:
   - tk_pub: the tag is public (can be shared, assertion is persistent)
-  - tk_unq: the tag is unique (cannot be shared, assertion is not persistent).
-  - tk_loc: the tag is local
+  - tk_unq: the tag is unique (cannot be shared, assertion is not persistent). This is further parameterized by whether it is reserved or activated.
+  - tk_loc: the tag is local (a local variable whose address has not been taken)
  *)
 
 Definition tagKindR := csumR (exclR unitO) (csumR (csumR (exclR unitO) (exclR unitO)) unitR).
diff --git a/theories/tree_borrows/tree_lemmas.v b/theories/tree_borrows/tree_lemmas.v
index b0470ca7..2eb5bf0d 100644
--- a/theories/tree_borrows/tree_lemmas.v
+++ b/theories/tree_borrows/tree_lemmas.v
@@ -1,7 +1,7 @@
 From Equations Require Import Equations.
 From iris.prelude Require Import prelude options.
 From stdpp Require Export gmap.
-From simuliris.tree_borrows Require Export lang_base notation tree.
+From simuliris.tree_borrows Require Export tree.
 From iris.prelude Require Import options.
 
 Implicit Type (V W X Y:Type).
@@ -246,42 +246,6 @@ Proof.
     all: simpl; auto.
 Qed.
 
-(*
-Lemma exists_child_transitive {X} (search search':Tprop X) :
-  forall tr,
-  exists_node search tr ->
-  tree_AtNode search (tree_ChildExists search') tr ->
-  exists_node search' tr.
-Proof.
-  intros tr Exists Search.
-  induction tr; simpl; auto.
-  destruct Search as [Search0 [Search1 Search2]].
-  destruct Exists as [Exists0 | [Exists1 | Exists2]]; auto.
-  destruct (Search0 Exists0); auto.
-Qed.
-
-Lemma AtNodeExists_transitive {X} (search search' search'':Tprop X) :
-  forall tr,
-  tree_AtNode search (tree_ChildExists search') tr ->
-  tree_AtNode search' (tree_ChildExists search'') tr ->
-  tree_AtNode search (tree_ChildExists search'') tr.
-Proof.
-  intros tr Search Search'.
-  induction tr; auto.
-  destruct Search' as [Search' [Search'1 Search'2]].
-  destruct Search as [Search [Search1 Search2]].
-  pose Found1 := (IHtr1 Search1 Search'1).
-  pose Found2 := (IHtr2 Search2 Search'2).
-  simpl; try repeat split; auto.
-  clear Found1; clear Found2; clear IHtr1; clear IHtr2.
-  intro Found; destruct (Search Found) as [Found' | FoundSub].
-  - destruct (Search' Found') as [Found'' | Found'Sub]; auto.
-  - right; clear Found; clear Search; clear Search1; clear Search2.
-    clear Search'.
-    apply (ExistsAtNode_transitive search'); auto.
-Qed.
-*)
-
 Lemma insert_true_preserves_every {X} (tr:tree X) (ins:X) (search prop:X -> Prop)
   {search_dec:forall x, Decision (search x)} :
   prop ins ->
@@ -370,21 +334,6 @@ Proof.
     * right; right; auto.
 Qed.
 
-(*
-Lemma insert_preserves_ChildExists {X} (ins:X) (tr:tree X) (search prop:Tprop X)
-  {search_dec:forall x, Decision (search x)} :
-  tree_ChildExists prop tr -> tree_ChildExists prop (insert_child_at tr ins search).
-Proof.
-  intro Exists.
-  destruct tr; simpl; auto.
-  destruct (decide (search data)) eqn:Found; simpl; auto.
-  all: simpl in Exists.
-  all: inversion Exists as [Ex0 | Ex2]; auto.
-  1: right; right; left; apply insert_preserves_Exists; auto.
-  right; apply insert_preserves_Exists; auto.
-Qed.
-*)
-
 Lemma exists_insert_requires_parent {X} (ins:X) (search prop:X -> Prop)
   {search_dec:forall x, Decision (search x)} :
   forall tr,
@@ -414,7 +363,7 @@ Proof.
   right; right. destruct Hyp2 as [Contra | [Hyp2Sub | Hyp2Empty]]; auto; contradiction.
 Qed.
 
-Lemma exists_subtree_transitive br prop (tr:tree item) :
+Lemma exists_subtree_transitive T br prop (tr:tree T) :
   exists_subtree (eq br) tr ->
   exists_subtree prop (of_branch br) ->
   exists_subtree prop tr.
@@ -428,7 +377,7 @@ Proof.
   - right; right. apply IHtr2; auto.
 Qed.
 
-Lemma every_subtree_transitive br prop (tr:tree item) :
+Lemma every_subtree_transitive T br prop (tr:tree T) :
   every_subtree (eq br) tr ->
   every_subtree prop (of_branch br) ->
   every_subtree prop tr.
@@ -442,7 +391,7 @@ Proof.
   try repeat split; auto.
 Qed.
 
-Lemma exists_node_transitive br prop (tr:tree item) :
+Lemma exists_node_transitive T br prop (tr:tree T) :
   exists_subtree (eq br) tr ->
   exists_node prop (of_branch br) ->
   exists_node prop tr.
diff --git a/theories/tree_borrows/trees_equal/disabled_in_practice.v b/theories/tree_borrows/trees_equal/disabled_in_practice.v
index 6bdb6d5b..9e635cd1 100644
--- a/theories/tree_borrows/trees_equal/disabled_in_practice.v
+++ b/theories/tree_borrows/trees_equal/disabled_in_practice.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/random_lemmas.v b/theories/tree_borrows/trees_equal/random_lemmas.v
index 2ae7810b..7abccdfb 100644
--- a/theories/tree_borrows/trees_equal/random_lemmas.v
+++ b/theories/tree_borrows/trees_equal/random_lemmas.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_asymmetric_prot.v b/theories/tree_borrows/trees_equal/trees_equal_asymmetric_prot.v
index f4342eef..4c081cee 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_asymmetric_prot.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_asymmetric_prot.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_base.v b/theories/tree_borrows/trees_equal/trees_equal_base.v
index 4ac52f8d..8c0500b1 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_base.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_base.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_create_child.v b/theories/tree_borrows/trees_equal/trees_equal_create_child.v
index efda218a..e9b0cb19 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_create_child.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_create_child.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_initcall.v b/theories/tree_borrows/trees_equal/trees_equal_initcall.v
index 10c03dc2..dbb1a888 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_initcall.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_initcall.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_more_access.v b/theories/tree_borrows/trees_equal/trees_equal_more_access.v
index d8fb9630..c6382850 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_more_access.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_more_access.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access.v b/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access.v
index d2124075..17f81ed1 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access_base.v b/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access_base.v
index f02f2c20..b0e6444a 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access_base.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access_base.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_source_read.v b/theories/tree_borrows/trees_equal/trees_equal_source_read.v
index 0cbe36a4..902f3963 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_source_read.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_source_read.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_transitivity.v b/theories/tree_borrows/trees_equal/trees_equal_transitivity.v
index e619696a..9ebf91f1 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_transitivity.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_transitivity.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
-- 
GitLab