Update TB-specific Readme

_CoqProject

@@ -164,7 +164,6 @@ theories/tree_borrows/steps_all.v
 theories/tree_borrows/primitive_laws.v
 theories/tree_borrows/proofmode.v
 theories/tree_borrows/early_proofmode.v
-theories/tree_borrows/wishlist.v
 theories/tree_borrows/tree_access_laws.v
 theories/tree_borrows/tag_protected_laws.v
 theories/tree_borrows/loc_controlled_laws.v

theories/tree_borrows/README.md

@@ -4,12 +4,23 @@ Forked and adapted from the sibling folder `../stacked_borrows` with the same st
 
 * `tree.v`, `locations.v` contain preliminary definitions.
 * `lang_base.v`, `expr_semantics.v`, `bor_semantics.v`, and `lang.v` contain the language definition.
-* `tree_lemmas.v`, `bor_lemmas.v` and `steps_wf.v` contain basic lemmas to help with the manipulation of trees.
-* [WIP] `logical_state.v` defines the invariants and instantiates the simulation relation.
-* [WIP] `steps_refl.v` and `steps_opt.v` prove the main execution lemmas.
-* [WIP] `behavior.v` defines the notion of contextual refinement and expression well-formedness.
-* [WIP] `adequacy.v` contains the resulting adequacy proof.
-* [WIP] `examples` contains example optimizations.
+* `tree_lemmas.v`, `bor_lemmas.v`, `steps_wf.v` and `steps_preserve.v` contain basic lemmas to help with the manipulation of trees.
+* `defs.v` defines well-formedness invariants for trees.
+* `logical_state.v` defines the invariants and instantiates the simulation relation,
+  using among others a notion of when trees are similar in `trees_equal/`.
+* `steps_refl.v` and `steps_opt.v` prove the main execution lemmas.
+* `behavior.v` defines the notion of contextual refinement and expression well-formedness.
+* `adequacy.v` contains the resulting adequacy proof.
+* `examples/` contains example optimizations, further subdivided into
+  - `unprotected/` optimizations, which are program transformations that can be applied even in the absence of protectors,
+  - `protected/` optimizations, which require a protector to hold,
+  - `impossible/` optimizations used to hold under Stacked Borrows,
+    but we know of counter-examples under Tree Borrows.
 
-In addition, `disjoint.v` provides proofs of simple reorderings (swapping adjacent operations in
-a sequential setting) directly against the operational semantics.
+In addition, `read_read_reorder/` provides proofs of simple reorderings
+(swapping adjacent operations in a sequential setting)
+directly against the operational semantics.
+It is subdivided into
+ * `refinement_def.v`: definition of a bisimulation relation for a sequential setting.
+ * `low_level.v`: lemmas against the operational semantics.
+ * `refinement.v`: actual proof of bisimulation between two programs in which adjacent reads have been swapped.

theories/tree_borrows/wishlist.v

-From iris.proofmode Require Export proofmode.
-From simuliris.tree_borrows Require Export tree_access_laws tag_protected_laws loc_controlled_laws.
-From iris.base_logic.lib Require Import ghost_map.
-From simuliris.base_logic Require Export gen_sim_prog.
-From simuliris.simulation Require Export slsls.
-From simuliris.simulation Require Import lifting.
-From simuliris.tree_borrows Require Import tkmap_view.
-From simuliris.tree_borrows Require Export defs class_instances.
-From simuliris.tree_borrows Require Import steps_progress steps_inv.
-From simuliris.tree_borrows Require Import logical_state inv_accessors.
-From simuliris.tree_borrows.trees_equal Require Import trees_equal_base random_lemmas.
-From iris.prelude Require Import options.
-
-
-
-
-