From 10d7bb4b901a3f1ffce30da7b88c129b40936dc7 Mon Sep 17 00:00:00 2001 From: Neven Villani <vanille@crans.org> Date: Wed, 13 Nov 2024 15:40:26 +0100 Subject: [PATCH] Update TB-specific Readme --- _CoqProject | 1 - theories/tree_borrows/README.md | 27 +++++++++++++++++++-------- theories/tree_borrows/wishlist.v | 17 ----------------- 3 files changed, 19 insertions(+), 26 deletions(-) delete mode 100644 theories/tree_borrows/wishlist.v diff --git a/_CoqProject b/_CoqProject index 91b31f44..efe981db 100644 --- a/_CoqProject +++ b/_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 diff --git a/theories/tree_borrows/README.md b/theories/tree_borrows/README.md index 83aeafaa..bb1c7659 100644 --- a/theories/tree_borrows/README.md +++ b/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. diff --git a/theories/tree_borrows/wishlist.v b/theories/tree_borrows/wishlist.v deleted file mode 100644 index e5ea6c2b..00000000 --- a/theories/tree_borrows/wishlist.v +++ /dev/null @@ -1,17 +0,0 @@ -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. - - - - - -- GitLab