From a7a6ebb6619702c5c30cc4d9ac7e578715a597d8 Mon Sep 17 00:00:00 2001
From: Neven Villani <vanille@crans.org>
Date: Mon, 10 Mar 2025 13:17:26 +0100
Subject: [PATCH] First wave of extra documentation & cleanup
---
theories/tree_borrows/README.md | 6 +
theories/tree_borrows/behavior.v | 1 +
theories/tree_borrows/bor_lemmas.v | 152 +++++-----
theories/tree_borrows/bor_semantics.v | 54 ++--
theories/tree_borrows/defs.v | 31 +-
theories/tree_borrows/expr_semantics.v | 11 -
theories/tree_borrows/lang.v | 5 +-
theories/tree_borrows/lang_base.v | 35 +--
theories/tree_borrows/locations.v | 4 +
theories/tree_borrows/logical_state.v | 342 -----------------------
theories/tree_borrows/notation.v | 2 -
theories/tree_borrows/steps_access.v | 173 ------------
theories/tree_borrows/steps_preserve.v | 20 +-
theories/tree_borrows/steps_progress.v | 246 +---------------
theories/tree_borrows/steps_wf.v | 3 +
theories/tree_borrows/tree.v | 55 +++-
theories/tree_borrows/tree_access_laws.v | 11 +-
theories/tree_borrows/wf.v | 4 +-
18 files changed, 237 insertions(+), 918 deletions(-)
diff --git a/theories/tree_borrows/README.md b/theories/tree_borrows/README.md
index f6ac526f..97bea348 100644
--- a/theories/tree_borrows/README.md
+++ b/theories/tree_borrows/README.md
@@ -7,9 +7,14 @@ 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`, `steps_wf.v` and `steps_preserve.v` contain basic lemmas to help with the manipulation of trees.
+* `tree_access_laws.v` contains more complex lemmas about the entire memory (`trees`) rather than single allocations (`tree`)
* `defs.v` defines well-formedness invariants for trees.
+* `wf.v` defines well-formedness for expressions.
+* `steps_progress.v` states success conditions for the various borrow steps so that we can prove absence of UB or exploit presence of UB.
+* `tkmap_view.v` defines views (partial ownership) of the global maps we use to remember the kind of each tag
* `logical_state.v` defines the invariants and instantiates the simulation relation,
using among others a notion of when trees are similar in `trees_equal/`.
+* `tag_protected_laws.v` contains reasoning principles about protectors
* `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.
@@ -55,6 +60,7 @@ The proof that the two reads can be reordered is in `read_reorder.v`.
The file `low_level.v` contains low-level lemmas used in `read_reorder.v`
### Other Examples From The Paper
+
Example 1 is similar to the one shown in `examples/unprotected/mutable_delete_read.v`.
The one shown in Coq has two places where arbitrary unknown functions are called, and Example 1 is just a special case of that, if one instantiates these unknown functions correctly.
diff --git a/theories/tree_borrows/behavior.v b/theories/tree_borrows/behavior.v
index 9a27df7d..d22e3758 100755
--- a/theories/tree_borrows/behavior.v
+++ b/theories/tree_borrows/behavior.v
@@ -20,6 +20,7 @@ Definition obs_scalar (sc_t sc_s : scalar) :=
| _, _ => False
end
.
+
Definition obs_value (v_t v_s : value) : Prop := Forall2 obs_scalar v_t v_s.
Definition obs_result (r_t r_s : val bor_lang) : Prop :=
match r_t, r_s with
diff --git a/theories/tree_borrows/bor_lemmas.v b/theories/tree_borrows/bor_lemmas.v
index 61f6e687..773a1fad 100644
--- a/theories/tree_borrows/bor_lemmas.v
+++ b/theories/tree_borrows/bor_lemmas.v
@@ -2,6 +2,13 @@ From iris.prelude Require Import prelude options.
From simuliris.tree_borrows Require Import lang_base notation bor_semantics tree tree_lemmas.
From iris.prelude Require Import options.
+(** A collection of lemmas to reason about the current state of the tree.
+ These are not invariants (you will find those in [steps_wf.v].
+ Rather, consider that this file is to [bor_semantics.v] what
+ [tree_lemmas.v] is to [tree.v]: these are specialized lemmas
+ to reason about the instanciation of trees that is specifically
+ with [item]s containing [tag]s (and some non-tree lemmas also). *)
+
Lemma most_init_comm m1 m2 : most_init m1 m2 = most_init m2 m1.
Proof. by destruct m1, m2. Qed.
@@ -32,6 +39,9 @@ Lemma exists_somewhere
a + b + c ≥ 1 <-> a ≥ 1 \/ b ≥ 1 \/ c ≥ 1.
Proof. lia. Qed.
+(** [tree_unique] is defined by [count_nodes].
+ [tree_contains] is defined by [exists_node].
+ Here are some lemmas that relate the two. *)
Lemma unique_exists {tr tg} :
tree_unique tg tr ->
tree_contains tg tr.
@@ -66,7 +76,6 @@ Proof.
reflexivity.
Qed.
-
Lemma count_0_not_exists tr tg :
tree_count_tg tg tr = 0
<-> ~tree_contains tg tr.
@@ -93,6 +102,8 @@ Proof.
+ apply IHtr2. auto.
Qed.
+(** [tree_item_determined] is defined by a [forall_nodes].
+ We can similarly relate it to predicates derived from [count_nodes]. *)
Lemma absent_determined tr tg :
tree_count_tg tg tr = 0 ->
forall it, tree_item_determined tg it tr.
@@ -148,6 +159,12 @@ Proof.
- right; right; auto.
Qed.
+(** Some of the most important lemmas here.
+ They characterizes insertion of a child node in terms of its relationship
+ with other nodes. If you insert [n'] as a child of [n]...
+ then in the resulting tree [n'] is a child of [n]!
+ Not a groundbreaking statement, but necessary due to our representation
+ of trees. *)
Lemma insert_eqv_strict_rel t t' (ins:item) (tr:tree item) (search:item -> Prop)
{search_dec:forall it, Decision (search it)} :
~IsTag t ins ->
@@ -225,69 +242,6 @@ Proof.
erewrite exists_sibling_insert. eauto.
Qed.
-Lemma join_map_eqv_strict_rel t t' (tr tr':tree item) :
- forall fn,
- (forall it it', fn it = Some it' -> itag it = itag it') ->
- join_nodes (map_nodes fn tr) = Some tr' ->
- StrictParentChildIn t t' tr <-> StrictParentChildIn t t' tr'.
-Proof.
- intros fn FnPreservesTag Success.
- generalize dependent tr'.
- unfold StrictParentChildIn.
- induction tr as [|data ? IHtr1 ? IHtr2]; intros tr' Success; simpl in *.
- - inversion Success; auto.
- - destruct (destruct_joined _ _ _ _ Success) as [data' [tr1' [tr2' [EqTr' [EqData' [EqTr1' EqTr2']]]]]].
- rewrite IHtr1; [|eapply EqTr1'].
- rewrite IHtr2; [|eapply EqTr2'].
- subst; simpl.
- split; intro H; destruct H as [H[??]]; try repeat split; try assumption.
- all: intro Hyp.
- + rewrite <- join_map_preserves_exists.
- * apply H. erewrite FnPreservesTag; eassumption.
- * intros; subst. erewrite FnPreservesTag; eauto.
- * apply EqTr2'.
- + rewrite join_map_preserves_exists.
- * apply H. erewrite <- FnPreservesTag; eassumption.
- * intros; subst. erewrite FnPreservesTag; eauto.
- * apply EqTr2'.
-Qed.
-
-Lemma join_map_eqv_rel
- {t t' tr tr' fn}
- (PreservesTags : forall it it', fn it = Some it' -> itag it = itag it')
- (Success : join_nodes (map_nodes fn tr) = Some tr')
- : ParentChildIn t t' tr <-> ParentChildIn t t' tr'.
-Proof.
- unfold ParentChildIn.
- rewrite join_map_eqv_strict_rel; eauto.
-Qed.
-
-Lemma join_map_eqv_imm_rel
- {t t' tr tr' fn}
- (PreservesTags : forall it it', fn it = Some it' -> itag it = itag it')
- (Success : join_nodes (map_nodes fn tr) = Some tr')
- : ImmediateParentChildIn t t' tr <-> ImmediateParentChildIn t t' tr'.
-Proof.
- generalize dependent tr'.
- unfold ImmediateParentChildIn.
- induction tr as [|data ? IHtr1 ? IHtr2]; intros tr' Success; simpl in *.
- - inversion Success; auto.
- - destruct (destruct_joined _ _ _ _ Success) as [data' [tr1' [tr2' [EqTr' [EqData' [EqTr1' EqTr2']]]]]].
- rewrite IHtr1; [|eapply EqTr1'].
- rewrite IHtr2; [|eapply EqTr2'].
- subst; simpl.
- split; intros (H&?&?); split_and!; try done.
- all: intro Hyp.
- + rewrite <- join_map_preserves_exists_sibling.
- * apply H. erewrite PreservesTags; eassumption.
- * intros; subst. erewrite PreservesTags; eauto.
- * apply EqTr2'.
- + rewrite join_map_preserves_exists_sibling.
- * apply H. erewrite <- PreservesTags; eassumption.
- * intros; subst. erewrite PreservesTags; eauto.
- * apply EqTr2'.
-Qed.
-
Lemma insert_produces_StrictParentChild t (ins:item) (tr:tree item) :
~IsTag t ins ->
StrictParentChildIn t ins.(itag) (insert_child_at tr ins (IsTag t)).
@@ -326,7 +280,6 @@ Proof.
intro H; contradiction.
Qed.
-
Lemma ImmediateParentChild_of_insert_is_parent t t' (ins:item) (tr:tree item) :
¬ exists_node (IsTag (ins.(itag))) tr ->
exists_node (IsTag t') tr ->
@@ -367,7 +320,76 @@ Proof.
eapply IHtr1'; first done. all: simpl in H1tr2,Hnt2; tauto.
Qed.
+(** Recall:
+ [map_nodes : (X -> Y) -> tree X -> tree Y] applies a function to each node.
+ [join_nodes : tree (option X) -> option (tree X)] collects failures.
+
+ Our semantics are mostly expressed as a combination of these two,
+ in the form of [join_nodes (map_nodes faillible_function tree)].
+ Therefore it is not surprising that these characterizations of
+ [join]+[map] are also among the most important lemmas here. *)
+Lemma join_map_eqv_strict_rel t t' (tr tr':tree item) :
+ forall fn,
+ (forall it it', fn it = Some it' -> itag it = itag it') ->
+ join_nodes (map_nodes fn tr) = Some tr' ->
+ StrictParentChildIn t t' tr <-> StrictParentChildIn t t' tr'.
+Proof.
+ intros fn FnPreservesTag Success.
+ generalize dependent tr'.
+ unfold StrictParentChildIn.
+ induction tr as [|data ? IHtr1 ? IHtr2]; intros tr' Success; simpl in *.
+ - inversion Success; auto.
+ - destruct (destruct_joined _ _ _ _ Success) as [data' [tr1' [tr2' [EqTr' [EqData' [EqTr1' EqTr2']]]]]].
+ rewrite IHtr1; [|eapply EqTr1'].
+ rewrite IHtr2; [|eapply EqTr2'].
+ subst; simpl.
+ split; intro H; destruct H as [H[??]]; try repeat split; try assumption.
+ all: intro Hyp.
+ + rewrite <- join_map_preserves_exists.
+ * apply H. erewrite FnPreservesTag; eassumption.
+ * intros; subst. erewrite FnPreservesTag; eauto.
+ * apply EqTr2'.
+ + rewrite join_map_preserves_exists.
+ * apply H. erewrite <- FnPreservesTag; eassumption.
+ * intros; subst. erewrite FnPreservesTag; eauto.
+ * apply EqTr2'.
+Qed.
+
+Lemma join_map_eqv_rel
+ {t t' tr tr' fn}
+ (PreservesTags : forall it it', fn it = Some it' -> itag it = itag it')
+ (Success : join_nodes (map_nodes fn tr) = Some tr')
+ : ParentChildIn t t' tr <-> ParentChildIn t t' tr'.
+Proof.
+ unfold ParentChildIn.
+ rewrite join_map_eqv_strict_rel; eauto.
+Qed.
+Lemma join_map_eqv_imm_rel
+ {t t' tr tr' fn}
+ (PreservesTags : forall it it', fn it = Some it' -> itag it = itag it')
+ (Success : join_nodes (map_nodes fn tr) = Some tr')
+ : ImmediateParentChildIn t t' tr <-> ImmediateParentChildIn t t' tr'.
+Proof.
+ generalize dependent tr'.
+ unfold ImmediateParentChildIn.
+ induction tr as [|data ? IHtr1 ? IHtr2]; intros tr' Success; simpl in *.
+ - inversion Success; auto.
+ - destruct (destruct_joined _ _ _ _ Success) as [data' [tr1' [tr2' [EqTr' [EqData' [EqTr1' EqTr2']]]]]].
+ rewrite IHtr1; [|eapply EqTr1'].
+ rewrite IHtr2; [|eapply EqTr2'].
+ subst; simpl.
+ split; intros (H&?&?); split_and!; try done.
+ all: intro Hyp.
+ + rewrite <- join_map_preserves_exists_sibling.
+ * apply H. erewrite PreservesTags; eassumption.
+ * intros; subst. erewrite PreservesTags; eauto.
+ * apply EqTr2'.
+ + rewrite join_map_preserves_exists_sibling.
+ * apply H. erewrite <- PreservesTags; eassumption.
+ * intros; subst. erewrite PreservesTags; eauto.
+ * apply EqTr2'.
+Qed.
Lemma Immediate_is_StrictChildTag tg tr :
HasImmediateChildTag tg tr →
diff --git a/theories/tree_borrows/bor_semantics.v b/theories/tree_borrows/bor_semantics.v
index 1c7d4a69..4fba6c16 100755
--- a/theories/tree_borrows/bor_semantics.v
+++ b/theories/tree_borrows/bor_semantics.v
@@ -20,14 +20,6 @@ From stdpp Require Export gmap.
From simuliris.tree_borrows Require Export lang_base notation tree tree_lemmas.
From iris.prelude Require Import options.
-Lemma decision_equiv (P Q:Prop) :
- (P <-> Q) ->
- Decision P ->
- Decision Q.
-Proof.
- unfold Decision. tauto.
-Defined.
-
(*** TREE BORROWS SEMANTICS ---------------------------------------------***)
Implicit Type (c:call_id) (cids:call_id_set).
@@ -430,6 +422,14 @@ Proof.
* inversion IsProt.
Defined.
+Lemma decision_equiv (P Q:Prop) :
+ (P <-> Q) ->
+ Decision P ->
+ Decision Q.
+Proof.
+ unfold Decision. tauto.
+Defined.
+
Global Instance protector_is_active_dec prot cids :
Decision (protector_is_active prot cids).
Proof.
@@ -501,7 +501,6 @@ Definition tree_apply_access
(* Initial permissions. *)
Definition init_perms perm off sz
- (* FIXME: simplify to just ø directly ? *)
: permissions := mem_apply_range'_defined (fun _ => mkPerm PermInit perm) (off, sz) ∅.
(* Initial tree is a single root whose default permission is [Active]. *)
@@ -562,7 +561,7 @@ Definition memory_deallocate cids t range
let post_write := memory_access AccessWrite cids t range tr in
(* Then strong protector UB. *)
let find_strong_prot : item -> option item := fun it => (
- (* FIXME: switch to plain [decide] ? *)
+ (* FIXME: consider switching to plain [decide] *)
if bool_decide (protector_is_strong it.(iprot)) && bool_decide (protector_is_active it.(iprot) cids)
then None
else Some it
@@ -589,7 +588,7 @@ Definition witness_transition p p' : Prop :=
| _, _ => False
end.
-(* FIXME: use builtin rtc *)
+(* FIXME: using builtin reflexive transitive closure could simplify some proofs. *)
Inductive witness_reach p p' : Prop :=
| witness_reach_refl : p = p' -> witness_reach p p'
| witness_reach_step p'' : witness_transition p p'' -> witness_reach p'' p' -> witness_reach p p'
@@ -607,11 +606,17 @@ Definition reach p p' : Prop :=
| _, _ => False
end.
+(* Denotes a permission that "acts like Frozen" for the purpose
+ of a later invariant. Concretely this contains
+ [Frozen], [Disabled], [Reserved ResConflicted],
+ which are the 3 permissions that are not affected by a foreign read,
+ so "acts like frozen" can mean "is allowed to coexist with shared references". *)
Definition freeze_like p : Prop :=
reach Frozen p \/ p = Reserved ResConflicted.
-(* Now we check that the two definitions are equivalent, so that the clean definition
- acts as a witness for the easy-to-do-case-analysis definition *)
+(* Now we check that the two definitions of reachability are equivalent,
+ so that the clean definition acts as a witness for the easy-to-do-case-analysis
+ definition *)
Ltac destruct_permission :=
match goal with
@@ -717,20 +722,26 @@ Proof.
all: destruct isprot'; simpl; try auto.
Qed.
+(** Some important predicates on trees. *)
+
+(** There is a node with tag [tg]. *)
Definition tree_contains tg tr
: Prop :=
exists_node (IsTag tg) tr.
+(** All nodes with tag [tg] equal [it].
+ This is often useless on its own if you don't also own a [tree_contains tg]. *)
Definition tree_item_determined tg it tr
: Prop :=
every_node (fun it' => IsTag tg it' -> it' = it) tr.
Notation has_tag tg := (fun it => bool_decide (IsTag tg it)) (only parsing).
+(** Counting how many nodes in a tree have a certain tag. *)
Definition tree_count_tg tg tr : nat := count_nodes (has_tag tg) tr.
Definition tree_unique tg tr : Prop := tree_count_tg tg tr = 1.
-(* TODO change to thing below *)
+(** Capable of lifting any of the above predicates to [trees]. *)
Definition trees_at_block prop trs blk
: Prop :=
match trs !! blk with
@@ -761,7 +772,7 @@ Definition trees_unique tg trs blk it :=
Definition ParentChildInBlk tg tg' trs blk :=
trees_at_block (ParentChildIn tg tg') trs blk.
-(* FIXME: Improve consistency of argument ordering *)
+(* FIXME: Future refactoring: improve consistency of argument ordering *)
(** Reborrow *)
@@ -808,7 +819,6 @@ Definition every_tagged t (P:item -> Prop) tr
: Prop :=
every_node (fun it => IsTag t it -> P it) tr.
-(* FIXME: gmap::partial_alter ? *)
Definition apply_within_trees (fn:tree item -> option (tree item)) blk
: trees -> option trees := fun trs =>
oldtr ↠trs !! blk;
@@ -853,7 +863,7 @@ Definition tree_access_all_protected_initialized (cids : call_id_set) (cid : nat
(* finally we can combine this all *)
set_fold (fun '(tg, init_locs) (tr:option (tree item)) => tr ↠tr; reader_locs tg init_locs tr) (Some tr) init_locs.
-(* WARNING: don't make the access visible to children !
+(* WARNING: don't make the access visible to children!
You can check in `trees_access_all_protected_initialized` that we properly use
`memory_access_nonchildren_only`. *)
(* Finally we read all protected initialized locations on the entire trees by folding it
@@ -870,6 +880,7 @@ Definition trees_access_all_protected_initialized (cids : call_id_set) (cid : na
Inductive bor_step (trs : trees) (cids : call_id_set) (nxtp : nat) (nxtc : call_id)
: event -> trees -> call_id_set -> nat -> call_id -> Prop :=
| AllocIS (blk : block) (off : Z) (sz : nat)
+ (* Memory allocation *)
(FRESH : trs !! blk = None)
(NONZERO : (sz > 0)%nat) :
bor_step
@@ -894,6 +905,10 @@ Inductive bor_step (trs : trees) (cids : call_id_set) (nxtp : nat) (nxtc : call_
trs cids nxtp nxtc
(* | FailedCopyIS (alloc : block) range tg
(* Unsuccessful read access just returns poison instead of causing UB *)
+ (* WARNING: SB works like this, having failed reads return poison
+ instead of triggering UB. We can't do this for Tree Borrows.
+ This was a hack for SB anyway, and not having it gives a stronger result.
+ *)
(EXISTS_TAG : trees_contain tg trs alloc)
(ACC : apply_within_trees (memory_access AccessRead cids tg range) alloc trs = None) :
bor_step
@@ -930,9 +945,8 @@ Inductive bor_step (trs : trees) (cids : call_id_set) (nxtp : nat) (nxtc : call_
(RetagEvt alloc range parentt nxtp pk im cid rk)
trs'' cids (S nxtp) nxtc
| RetagNoopIS parentt (alloc : block) range pk im cid rk
- (* For a retag we require that the parent exists and the introduced tag is fresh, then we do a read access.
- NOTE: create_child does not read, it only inserts, so the read needs to be explicitly added.
- We want to do the read *after* the insertion so that it properly initializes the locations of the range.*)
+ (* This is a noop retag. Some "retagging" operations don't actually do anything,
+ e.g. raw pointer retags. *)
(EL: cid ∈ cids)
(EXISTS_TAG: trees_contain parentt trs alloc)
(IS_NOOP: retag_perm pk im rk = None) :
diff --git a/theories/tree_borrows/defs.v b/theories/tree_borrows/defs.v
index bb15bd95..e9f1a8c8 100755
--- a/theories/tree_borrows/defs.v
+++ b/theories/tree_borrows/defs.v
@@ -16,15 +16,28 @@ Definition wf_mem_tag (h: mem) (nxtp: tag) :=
Definition lazy_perm_wf (lp : lazy_permission) :=
lp.(perm) = Active → lp.(initialized) = PermInit.
+(** Well-formedness constraints on items *)
Record item_wf (it:item) (nxtp:tag) (nxtc:call_id) := {
+ (** Tag is valid *)
item_tag_valid : forall tg, IsTag tg it -> (tg < nxtp)%nat;
+ (** Callid is valid *)
item_cid_valid : forall cid, protector_is_for_call cid (iprot it) -> (cid < nxtc)%nat;
+ (** Permission registered as "default" can't be Active *)
item_default_perm_valid : it.(initp) ≠Active;
+ (** Only protected items can have ReservedIM somewhere in their permissions *)
item_perms_reserved_im_protected : is_Some (it.(iprot)) → ∀ off, (default (mkPerm PermLazy it.(initp)) (it.(iperm) !! off)).(perm) = ReservedIM → False;
+ (** Active implies initialized *)
item_perms_valid : map_Forall (λ _, lazy_perm_wf) it.(iperm);
+ (** Current permission is reachable from initial permission. (This guarantees no Active on shared references) *)
item_perm_reachable : it.(initp) ≠Disabled → map_Forall (λ k v, reach it.(initp) (perm v)) it.(iperm)
}.
+(** Relating the state of the current item with that of its parents.
+ The important properties are:
+ - an initialized item must have initialized parents,
+ - an Active item must have Active parents,
+ - a protected must not have Disabled parents.
+ *)
Definition item_all_more_init itp itc := ∀ l, initialized (item_lookup itc l) = PermInit → initialized (item_lookup itp l) = PermInit.
Definition parents_more_init (tr : tree item) := ∀ tg, every_child tg item_all_more_init tr.
Definition item_all_more_active itp itc := ∀ l, perm (item_lookup itc l) = Active → perm (item_lookup itp l) = Active.
@@ -68,17 +81,11 @@ Definition trees_compat_nexts (trs:trees) (nxtp:tag) (nxtc: call_id) :=
∀ blk tr, trs !! blk = Some tr → tree_items_compat_nexts tr nxtp nxtc.
Definition wf_non_empty (trs:trees) :=
∀ blk tr, trs !! blk = Some tr → tr ≠empty.
-(*
-Definition wf_no_dup (α: stacks) :=
- ∀ l stk, α !! l = Some stk → NoDup stk.
-*)
+
Definition wf_cid_incl (cids: call_id_set) (nxtc: call_id) :=
∀ c : call_id, c ∈ cids → (c < nxtc)%nat.
Definition wf_scalar t sc := ∀ t' l, sc = ScPtr l t' → t' < t.
-(* mem ~ gmap loc scalar
-*)
-
Definition same_blocks (hp:mem) (trs:trees) :=
dom trs =@{gset _} set_map fst (dom hp).
Arguments same_blocks / _ _.
@@ -92,7 +99,6 @@ Definition root_invariant blk it (shp : mem) :=
| Some (mkPerm PermLazy Disabled) | None => shp !! (blk, off) = None
| _ => False end.
-
Definition tree_root_compatible (tr : tree item) blk shp :=
match tr with empty => False | branch it sib _ => root_invariant blk it shp ∧ sib = empty end.
@@ -100,19 +106,28 @@ Definition tree_roots_compatible (trs : trees) shp :=
∀ blk tr, trs !! blk = Some tr → tree_root_compatible tr blk shp.
+(* A State is well-formed if... *)
Record state_wf (s: state) := {
(*state_wf_dom : dom s.(shp) ≡ dom s.(strs);
This was included in SB but we don't care anymore because TB
is very permissive about the range so out-of-bounds UB is *always*
triggered by `expr_semantics` not `bor_semantics`. *)
+
+ (* The heap and the trees talk of the same allocations *)
state_wf_dom : same_blocks s.(shp) s.(strs);
+ (* Every tree is well-formed (includes uniqueness of tags) *)
state_wf_tree_unq : wf_trees s.(strs);
+ (* The child-parent constraints relating to initialization etc. hold *)
state_wf_tree_more_init : each_tree_parents_more_init s.(strs);
state_wf_tree_more_active : each_tree_parents_more_active s.(strs);
state_wf_tree_not_disabled : each_tree_protected_parents_not_disabled s.(scs) s.(strs);
+ (* Some other constraints on relations (cousins can't be simultaneously active) *)
state_wf_tree_no_active_cousins : each_tree_no_active_cousins s.(scs) s.(strs);
+ (* "next fresh tag" is fresh. *)
state_wf_tree_compat : trees_compat_nexts s.(strs) s.(snp) s.(snc);
+ (* Every root pointer is active *)
state_wf_roots_active : tree_roots_compatible s.(strs) s.(shp);
+ (* "next fresh callid" is fresh. *)
state_wf_cid_agree: wf_cid_incl s.(scs) s.(snc);
}.
diff --git a/theories/tree_borrows/expr_semantics.v b/theories/tree_borrows/expr_semantics.v
index 08c03454..a2a97289 100755
--- a/theories/tree_borrows/expr_semantics.v
+++ b/theories/tree_borrows/expr_semantics.v
@@ -27,12 +27,8 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
| Write e1 e2 => Write (subst x es e1) (subst x es e2)
| Alloc T => Alloc T
| Free e => Free (subst x es e)
- (* | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2) *)
- (* | AtomWrite e1 e2 => AtomWrite (subst x es e1) (subst x es e2) *)
- (* | AtomRead e => AtomRead (subst x es e) *)
| Deref e T => Deref (subst x es e) T
| Ref e => Ref (subst x es e)
- (* | Field e path => Field (subst x: es e) path *)
| Retag e1 e2 newp im sz kind => Retag (subst x es e1) (subst x es e2) newp im sz kind
| Let x1 e1 e2 =>
Let x1 (subst x es e1)
@@ -40,7 +36,6 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
| Case e el => Case (subst x es e) (fmap (subst x es) el)
| Fork e => Fork (subst x es e)
| While e1 e2 => While (subst x es e1) (subst x es e2)
- (* | SysCall id => SysCall id *)
end.
(* formal argument list substitution *)
@@ -111,7 +106,6 @@ Inductive ectx_item :=
| FreeEctx
| DerefEctx (sz : nat)
| RefEctx
-(* | FieldEctx (path : list nat) *)
| RetagREctx (e1 : expr) (pk : pointer_kind) (im : interior_mut) (sz : nat) (kind : retag_kind)
| RetagLEctx (r2 : result) (pk : pointer_kind) (im : interior_mut) (sz : nat) (kind : retag_kind)
| LetEctx (x : binder) (e2 : expr)
@@ -136,7 +130,6 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
| FreeEctx => Free e
| DerefEctx T => Deref e T
| RefEctx => Ref e
- (* | FieldEctx path => Field e path *)
| RetagLEctx r2 newp im sz kind => Retag e (of_result r2) newp im sz kind
| RetagREctx e1 newp im sz kind => Retag e1 e newp im sz kind
| LetEctx x e2 => Let x e e2
@@ -542,8 +535,4 @@ Inductive mem_expr_step (h: mem) : expr → event → mem → expr → list expr
h (Retag #[ScPtr l otag] #[ScCallId cid] pk im sz kind)
(RetagEvt l.1 (l.2, sz) otag ntag pk im cid kind)
h #[ScPtr l ntag] []
-
-(* observable behavior *)
-(* | SysCallBS id h:
- expr_step (SysCall id) h (SysCallEvt id) (Lit LitPoison) h [] *)
.
diff --git a/theories/tree_borrows/lang.v b/theories/tree_borrows/lang.v
index 0e10eacf..8afd7c3a 100755
--- a/theories/tree_borrows/lang.v
+++ b/theories/tree_borrows/lang.v
@@ -2,6 +2,9 @@
https://gitlab.mpi-sws.org/FP/stacked-borrows
*)
+(** This file manages the interface between the expression semantics and
+ the borrow semantics. *)
+
From simuliris.simulation Require Export language.
From iris.algebra Require Import ofe.
From iris.prelude Require Import options.
@@ -15,7 +18,7 @@ Module bor_lang.
Record state := mkState {
(* Heap of scalars *)
shp : mem;
- (* Stacked borrows for the heap *)
+ (* Borrow trees for each allocation of the heap *)
strs : trees;
(* Set of active call ids *)
scs : call_id_set;
diff --git a/theories/tree_borrows/lang_base.v b/theories/tree_borrows/lang_base.v
index 9097539f..d522aa9c 100755
--- a/theories/tree_borrows/lang_base.v
+++ b/theories/tree_borrows/lang_base.v
@@ -199,20 +199,9 @@ Inductive retag_kind := FnEntry | Default.
Inductive bin_op :=
| AddOp (* + addition *)
| SubOp (* - subtraction *)
-(* | MulOp (* * multiplication *)
- | DivOp (* / division *)
- | RemOp (* % modulus *)
- | BitXorOp (* ^ bit xor *)
- | BitAndOp (* & bit and *)
- | BitOrOp (* | bit or *)
- | ShlOp (* << shift left *)
- | ShrOp (* >> shift right *) *)
| EqOp (* == equality *)
| LtOp (* < less than *)
| LeOp (* <= less than or equal to *)
-(* | NeOp (* != not equal to *)
- | GeOp (* >= greater than or equal to *)
- | GtOp (* > greater than *) *)
| OffsetOp (* . offset *)
.
@@ -306,18 +295,11 @@ Inductive expr :=
presenting the location that `e` points to.
The location has the kind and size of `ptr`. *)
| Ref (e : expr) (* Turn a place `e` into a pointer value. *)
-(* | Field (e: expr) (path: list nat)(* Create a place that points to a component
- of the place `e`. `path` defines the path
- through the type. *) *)
(* mem op *)
| Copy (e : expr) (* Read from the place `e` *)
| Write (e1 e2 : expr) (* Write the value `e2` to the place `e1` *)
| Alloc (sz : nat) (* Allocate a place of type `T` *)
| Free (e : expr) (* Free the place `e` *)
-(* atomic mem op *)
-(* | CAS (e0 e1 e2 : expr) *) (* CAS the value `e2` for `e1` to the place `e0` *)
-(* | AtomWrite (e1 e2: expr) *)
-(* | AtomRead (e: expr) *)
(* retag *) (* Retag the memory pointed to by `e1` with
retag kind `kind`, for call_id `e2`. The new pointer should have pointer kind pk. *)
| Retag (e1 : expr) (e2 : expr) (pk : pointer_kind) (im : interior_mut) (sz : nat) (kind : retag_kind)
@@ -329,8 +311,6 @@ Inductive expr :=
| Fork (e : expr)
(* While *)
| While (e1 e2 : expr)
-(* observable behavior *)
-(* | SysCall (id: nat) *)
.
Bind Scope expr_scope with expr.
@@ -355,15 +335,15 @@ Arguments While _%_E _%_E.
(** Closedness *)
Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
- | Val _ | Place _ _ _ | Alloc _ | InitCall (* | SysCall _ *) => true
+ | Val _ | Place _ _ _ | Alloc _ | InitCall => true
| Var x => bool_decide (x ∈ X)
| BinOp _ e1 e2 | Write e1 e2 | While e1 e2
| Conc e1 e2 | Proj e1 e2 | Call e1 e2 | Retag e1 e2 _ _ _ _ => is_closed X e1 && is_closed X e2
| Let x e1 e2 => is_closed X e1 && is_closed (x :b: X) e2
| Case e el
=> is_closed X e && forallb (is_closed X) el
- | Fork e | Copy e | Deref e _ | Ref e (* | Field e _ *)
- | Free e | EndCall e (* | AtomRead e | Fork e *)
+ | Fork e | Copy e | Deref e _ | Ref e
+ | Free e | EndCall e
=> is_closed X e
end.
@@ -445,18 +425,11 @@ Qed.
(** Main state: a heap of scalars, each with an associated lock to detect data races. *)
Definition mem := gmap loc scalar.
-(* Events in all their generality.
- We use the point of view adopted by Stacked Borrows and regarded by LLVM
- as acceptable which is to make FAILED READS NOT UB.
- A failed read has its own event [FailedCopyEvt] which returns poison
- instead of triggering immediate UB. This is assumed to be a sound change
- w.r.t. the semantics and is expected to allow proving more optimizations
- (they would still be true, but they wouldn't be *provable* with our means) *)
+(* Arbitrary borrow events. *)
Inductive event :=
| AllocEvt (alloc : block) (lbor : tag) (range : Z * nat)
| DeallocEvt (alloc : block) (lbor: tag) (range : Z * nat)
| CopyEvt (alloc : block) (lbor : tag) (range : Z * nat) (v : value)
-(* | FailedCopyEvt (alloc : block) (lbor : tag) (range : Z * nat) *)
| WriteEvt (alloc : block) (lbor : tag) (range : Z * nat) (v : value)
| InitCallEvt (c : call_id)
| EndCallEvt (c : call_id)
diff --git a/theories/tree_borrows/locations.v b/theories/tree_borrows/locations.v
index 1b91d57c..b8ce6b0a 100755
--- a/theories/tree_borrows/locations.v
+++ b/theories/tree_borrows/locations.v
@@ -2,6 +2,10 @@
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. *)
+
From iris.prelude Require Import prelude.
From iris.prelude Require Import options.
From stdpp Require Import countable numbers gmap.
diff --git a/theories/tree_borrows/logical_state.v b/theories/tree_borrows/logical_state.v
index 6aeab0bf..48e8848e 100755
--- a/theories/tree_borrows/logical_state.v
+++ b/theories/tree_borrows/logical_state.v
@@ -448,38 +448,6 @@ Section heap_defs.
Definition loc_controlled (l : loc) (t : tag) (tk : tag_kind) (sc : scalar) (σ : state) :=
(bor_state_pre l t tk σ → bor_state_own l t tk σ ∧ σ.(shp) !! l = Some sc).
-(* Lemma loc_controlled_local l t sc σ :
- loc_controlled l t tk_local sc σ →
- σ.(sst) !! l = Some [mkItem Unique (Tagged t) None] ∧
- σ.(shp) !! l = Some sc.
- Proof. intros Him. specialize (Him I) as (Hbor & Hmem). split;done. Qed.
-
- Lemma loc_controlled_unq l t sc s σ :
- loc_controlled l t tk_unq sc σ →
- σ.(sst) !! l = Some s →
- (∃ pm opro, mkItem pm (Tagged t) opro ∈ s ∧ pm ≠Disabled) →
- (∃ s' op, s = (mkItem Unique (Tagged t) op) :: s') ∧
- σ.(shp) !! l = Some sc.
- Proof.
- intros Him Hstk (pm & opro & Hpm).
- edestruct Him as (Hown & ?). { rewrite /bor_state_pre. eauto. }
- split; last done.
- destruct Hown as (st' & opro' & st'' & Hst' & ->). simplify_eq. eauto.
- Qed.
-
- Lemma loc_controlled_pub l t sc σ s :
- loc_controlled l t tk_pub sc σ →
- σ.(sst) !! l = Some s →
- (∃ pm opro, mkItem pm (Tagged t) opro ∈ s ∧ pm ≠Disabled) →
- t ∈ active_SRO s ∧
- σ.(shp) !! l = Some sc.
- Proof.
- intros Him Hst (pm & opro & Hin & Hpm).
- edestruct Him as (Hown & ?). { rewrite /bor_state_pre; eauto 8. }
- split; last done. destruct Hown as (st' & Hst' & Hsro).
- simplify_eq. eauto.
- Qed. *)
-
Lemma loc_controlled_mem_insert_ne l l' t tk sc sc' σ :
l ≠l' →
loc_controlled l t tk sc σ →
@@ -496,82 +464,6 @@ Section heap_defs.
intros Him Hpre. apply Him in Hpre as [Hown Hmem]. split; first done.
rewrite lookup_insert; done.
Qed.
-(*
- Section local.
- (** Facts about local tags *)
- Lemma loc_controlled_local_unique l t t' sc sc' σ :
- loc_controlled l t tk_local sc σ →
- loc_controlled l t' tk_local sc' σ →
- t' = t ∧ sc' = sc.
- Proof.
- intros Hcontrol Hcontrol'. specialize (Hcontrol I) as [Hown Hmem].
- specialize (Hcontrol' I) as [Hown' Hmem'].
- split; last by simplify_eq.
- move : Hown Hown'. rewrite /bor_state_own // => -> [=] //.
- Qed.
-
- Lemma loc_controlled_local_pre l t t' tk' sc σ :
- loc_controlled l t tk_local sc σ →
- bor_state_pre l t' tk' σ →
- tk' = tk_local ∨ t' = t.
- Proof.
- intros [Heq _]%loc_controlled_local.
- destruct tk'; last by eauto.
- - intros (st' & pm & opro & Hst & Hin & Hpm).
- move : Hst Hin. rewrite Heq.
- move => [= <-] /elem_of_list_singleton [=]; eauto.
- - intros (st' & pm & opro & Hst & Hin & Hpm).
- move : Hst Hin. rewrite Heq.
- move => [= <-] /elem_of_list_singleton [=]; eauto.
- Qed.
- Lemma bor_state_local_own_exclusive l t t' tk' σ :
- bor_state_own l t tk_local σ →
- bor_state_own l t' tk' σ →
- (tk' = tk_unq ∨ tk' = tk_local) ∧ t = t'.
- Proof.
- intros Heq. destruct tk'.
- - move => [st' []]. rewrite Heq => [= <-] //.
- - move => [st' [Heq' [opro [st'' ]]]]. move : Heq'. rewrite Heq => [= <-] [= ->] //; eauto.
- - rewrite /bor_state_own Heq => [=]; eauto.
- Qed.
- Lemma bor_state_unq_own_exclusive l t t' tk' σ :
- bor_state_own l t tk_unq σ →
- bor_state_own l t' tk' σ →
- (tk' = tk_unq ∨ tk' = tk_local) ∧ t = t'.
- Proof.
- intros (stk & Hstk & (opro & stk' & ->)).
- destruct tk'; simpl.
- - intros (stk'' & Hstk'' & Hact). rewrite Hstk in Hstk''. injection Hstk'' as [= <-].
- simpl in Hact. done.
- - intros (stk'' & Hstk'' & (opro' & stk''' & ->)).
- rewrite Hstk'' in Hstk. injection Hstk as [= -> -> ->]. eauto.
- - rewrite Hstk. intros [= -> -> ->]. eauto.
- Qed.
-
- (* having local ownership of a location is authoritative, in the sense that we can update memory without hurting other tags that control this location. *)
- 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' σ →
- t ≠t' →
- loc_controlled l t' tk' sc' (state_upd_mem f σ).
- Proof.
- intros Hcontrol Hcontrol' Hneq [Hown Hmem]%Hcontrol'. split; first done.
- edestruct (bor_state_local_own_exclusive l t t' tk' (state_upd_mem f σ)) as [_ <-]; [apply Hcontrol |..]; done.
- Qed.
-
- Lemma loc_controlled_protected_authoritative l t t' tk' sc sc' σ f c :
- loc_protected_by (state_upd_mem f σ) t l c →
- loc_controlled l t tk_unq sc (state_upd_mem f σ) →
- loc_controlled l t' tk' sc' σ →
- t ≠t' →
- loc_controlled l t' tk' sc' (state_upd_mem f σ).
- Proof.
- intros Hprot Hcontrol Hcontrol' Hneq [Hown Hmem]%Hcontrol'. split; first done.
- specialize (loc_protected_bor_state_pre _ _ _ _ tk_unq Hprot) as Hpre.
- apply Hcontrol in Hpre as [Hown' Hmem'].
- edestruct (bor_state_unq_own_exclusive l t t' tk' (state_upd_mem f σ)) as [_ <-]; done.
- Qed.
- End local. *)
(** Domain agreement for the two heap views for source and target *)
Definition dom_agree_on_tag (M_t M_s : gmap (tag * block) (gmap Z scalar)) (t : tag) :=
@@ -680,56 +572,6 @@ Section heap_defs.
+ eapply H3r. rewrite /heaplet_lookup HMo /= HH //.
Qed.
-(*
- Lemma dom_agree_on_tag_upd_ne_source M_t M_s t t' l sc :
- t ≠t' →
- dom_agree_on_tag M_t M_s t' →
- dom_agree_on_tag M_t (<[(t, l) := sc]> M_s) t'.
- Proof.
- intros Hneq [Htgt Hsrc]. split => l'' Hsome.
- - apply lookup_insert_is_Some. right. split; first congruence. by apply Htgt.
- - apply Hsrc. move : Hsome. rewrite lookup_insert_is_Some. by intros [[= -> <-] | [_ ?]].
- Qed.
- Lemma dom_agree_on_tag_upd_target M_t M_s t l sc :
- is_Some (M_t !! (t, l)) →
- dom_agree_on_tag M_t M_s t →
- dom_agree_on_tag (<[(t, l) := sc]> M_t) M_s t.
- Proof.
- intros Hs [Htgt Hsrc]. split => l''.
- - rewrite lookup_insert_is_Some. intros [[= <-] | [_ ?]]; by apply Htgt.
- - intros Hsome. rewrite lookup_insert_is_Some'. right; by apply Hsrc.
- Qed.
- Lemma dom_agree_on_tag_upd_source M_t M_s t l sc :
- is_Some (M_s !! (t, l)) →
- dom_agree_on_tag M_t M_s t →
- dom_agree_on_tag M_t (<[(t, l) := sc]> M_s) t.
- Proof.
- intros Hs [Htgt Hsrc]. split => l''.
- - intros Hsome. rewrite lookup_insert_is_Some'. right; by apply Htgt.
- - rewrite lookup_insert_is_Some. intros [[= <-] | [_ ?]]; by apply Hsrc.
- Qed.
- Lemma dom_agree_on_tag_lookup_target M_t M_s t l :
- dom_agree_on_tag M_t M_s t → is_Some (M_t !! (t, l)) → is_Some (M_s !! (t, l)).
- Proof. intros Hag Hsome. apply Hag, Hsome. Qed.
- Lemma dom_agree_on_tag_lookup_source M_t M_s t l :
- dom_agree_on_tag M_t M_s t → is_Some (M_s !! (t, l)) → is_Some (M_t !! (t, l)).
- Proof. intros Hag Hsome. apply Hag, Hsome. Qed.
-
- Lemma dom_agree_on_tag_difference M1_t M1_s M2_t M2_s t :
- dom_agree_on_tag M1_t M1_s t → dom_agree_on_tag M2_t M2_s t →
- dom_agree_on_tag (M1_t ∖ M2_t) (M1_s ∖ M2_s) t.
- Proof.
- intros [H1a H1b] [H2a H2b]. split; intros l.
- all: rewrite !lookup_difference_is_Some !eq_None_not_Some; naive_solver.
- Qed.
-
- Lemma dom_agree_on_tag_union M1_t M1_s M2_t M2_s t :
- dom_agree_on_tag M1_t M1_s t → dom_agree_on_tag M2_t M2_s t →
- dom_agree_on_tag (M1_t ∪ M2_t) (M1_s ∪ M2_s) t.
- Proof.
- intros [H1a H1b] [H2a H2b]. split; intros l; rewrite !lookup_union_is_Some; naive_solver.
- Qed. *)
-
Definition dom_unique_per_tag (M : gmap (tag * block) (gmap Z scalar)) : Prop :=
∀ tg l1 l2, (tg, l1) ∈ dom M → (tg, l2) ∈ dom M → l1 = l2.
@@ -756,12 +598,6 @@ Definition tk_to_frac (tk : tag_kind) :=
| tk_pub => DfracDiscarded
| _ => DfracOwn 1
end.
-(*
-Notation "l '↦t[' tk ']{' t } sc" := (ghost_map_elem heap_view_target_name (t, l) (tk_to_frac tk) sc)
- (at level 20, format "l ↦t[ tk ]{ t } sc") : bi_scope.
-Notation "l '↦s[' tk ']{' t } sc" := (ghost_map_elem heap_view_source_name (t, l) (tk_to_frac tk) sc)
- (at level 20, format "l ↦s[ tk ]{ t } sc") : bi_scope.
-*)
Section public_call_ids.
Context `{bor_stateGS Σ}.
@@ -1384,124 +1220,6 @@ Proof.
rewrite IH. 2: lia. f_equal. f_equal. lia.
Qed.
-
-
-(*
-
-Lemma array_tag_map_lookup1 l t v t' l' r :
- array_tag_map l t v !! (t', l') = Some r →
- t' = t ∧ l.1 = l'.1 ∧ l.2 ≤ l'.2 < l.2 + length v.
-Proof.
- induction v as [ | sc v IH] in l,r |-*.
- - simpl. rewrite lookup_empty. intros [=].
- - simpl. rewrite lookup_insert_Some. move => [[[= <- <-] Heq] | [Hneq Ht]].
- + split; first done. lia.
- + move : (IH (l +â‚— 1) ltac:(eauto) ltac:(eauto)). destruct l. simpl. intros (H1&H2); split; first done; lia.
-Qed.
-Lemma array_tag_map_lookup1_is_Some l t v t' l' :
- is_Some (array_tag_map l t v !! (t', l')) →
- t' = t ∧ l.1 = l'.1 ∧ l.2 ≤ l'.2 < l.2 + length v.
-Proof.
- intros [x Hx]. by eapply array_tag_map_lookup1.
-Qed.
-
-Lemma array_tag_map_lookup2 l t v t' l' :
- is_Some (array_tag_map l t v !! (t', l')) →
- t' = t ∧ ∃ i, (i < length v)%nat ∧ l' = l +ₗ i.
-Proof.
- intros [x (-> & H1 & H2)%array_tag_map_lookup1].
- split; first done. exists (Z.to_nat (l'.2 - l.2)).
- destruct l, l'; rewrite /shift_loc; simpl in *. split.
- - lia.
- - apply pair_equal_spec. split; lia.
-Qed.
-
-Lemma array_tag_map_lookup_Some l t v (i : nat) :
- (i < length v)%nat →
- array_tag_map l t v !! (t, l +â‚— i) = v !! i.
-Proof.
- induction v as [ | sc v IH] in l, i |-*.
- - simpl. lia.
- - simpl. intros Hi. destruct i as [ | i].
- + rewrite shift_loc_0_nat. rewrite lookup_insert. done.
- + rewrite lookup_insert_ne; first last. { destruct l; simpl; intros [= ?]; lia. }
- move : (IH (l +â‚— 1) i ltac:(lia)). rewrite shift_loc_assoc.
- by replace (Z.of_nat (S i)) with (1 + i) by lia.
-Qed.
-
-Lemma array_tag_map_lookup_None t t' l v :
- t ≠t' → ∀ l', array_tag_map l t v !! (t', l') = None.
-Proof.
- intros Hneq l'. destruct (array_tag_map l t v !! (t', l')) eqn:Harr; last done.
- specialize (array_tag_map_lookup1 l t v t' l' ltac:(eauto) ltac:(eauto)) as [Heq _]; congruence.
-Qed.
-
-Lemma array_tag_map_lookup_None' l t v l' :
- (∀ i:nat, (i < length v)%nat → l +ₗ i ≠l') →
- array_tag_map l t v !! (t, l') = None.
-Proof.
- intros Hneq. destruct (array_tag_map _ _ _ !! _) eqn:Heq; last done. exfalso.
- specialize (array_tag_map_lookup2 l t v t l' ltac:(eauto)) as [_ (i & Hi & ->)].
- eapply Hneq; last reflexivity. done.
-Qed.
-
-Lemma array_tag_map_lookup_None2 l t t' v l' :
- array_tag_map l t v !! (t', l') = None →
- t ≠t' ∨ (∀ i: nat, (i < length v)%nat → l +ₗ i ≠l').
-Proof.
- induction v as [ | sc v IH] in l |-*; simpl.
- - intros _. right. intros i Hi; lia.
- - rewrite lookup_insert_None. intros [Ha%IH Hneq].
- destruct Ha; first by eauto. move: Hneq. rewrite pair_equal_spec not_and_l.
- intros [ ? | Hneq]; first by eauto.
- right. intros i Hi. destruct i as [ | i].
- + rewrite shift_loc_0_nat. done.
- + replace (Z.of_nat (S i)) with (1 + i)%Z by lia. rewrite -shift_loc_assoc.
- eauto with lia.
-Qed.
-
-Lemma dom_agree_on_tag_array_tag_map l t v_t v_s :
- length v_t = length v_s →
- dom_agree_on_tag (array_tag_map l t v_t) (array_tag_map l t v_s) t.
-Proof.
- intros Hlen. split; intros l'.
- - intros (_ & (i & Hi & ->))%array_tag_map_lookup2. rewrite array_tag_map_lookup_Some; last lia.
- apply lookup_lt_is_Some_2. lia.
- - intros (_ & (i & Hi & ->))%array_tag_map_lookup2. rewrite array_tag_map_lookup_Some; last lia.
- apply lookup_lt_is_Some_2. lia.
-Qed.
-
-(** Array update lemmas for the heap views *)
-Lemma ghost_map_array_tag_lookup `{!bor_stateGS Σ} (γh : gname) (q : Qp) (M : gmap (tag * block) (gmap Z scalar)) (v : list scalar) (t : tag) (l : loc) dq :
- ghost_map_auth γh q M -∗
- ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +ₗ i) dq sc) -∗
- ⌜∀ i : nat, (i < length v)%nat → M !! (t, l +â‚— i) = v !! iâŒ.
-Proof.
- iIntros "Hauth Helem". iInduction v as [ |sc v ] "IH" forall (l) "Hauth Helem".
- - iPureIntro; cbn. lia.
- - rewrite big_sepL_cons. iDestruct "Helem" as "[Hsc Hscs]".
- iPoseProof (ghost_map_lookup with "Hauth Hsc") as "%Hl".
- iDestruct ("IH" $! (l +â‚— 1) with "Hauth [Hscs]") as "%IH".
- { iApply (big_sepL_mono with "Hscs"). intros i sc' Hs. cbn. rewrite shift_loc_assoc.
- replace (Z.of_nat $ S i) with (1 + i)%Z by lia. done. }
- iPureIntro. intros i Hle. destruct i as [|i]; first done.
- replace (Z.of_nat $ S i) with (1 + i)%Z by lia. cbn in *. rewrite -(IH i); last lia.
- by rewrite shift_loc_assoc.
-Qed.
-
-Lemma array_tag_map_union_commute (l : loc) (sc : scalar) (t : tag) (v : list scalar) (M : gmap (tag * block) (gmap Z scalar)) (i : Z) :
- i > 0 →
- <[(t, l) := sc]> (array_tag_map (l +ₗ i) t v) ∪ M = array_tag_map (l +ₗ i) t v ∪ (<[(t, l) := sc]> M).
-Proof.
- intros Hi. induction v as [ | sc' v IH] in l, i, Hi |-*; simpl.
- - rewrite insert_union_singleton_l. rewrite -map_union_assoc. rewrite !map_empty_union.
- by rewrite insert_union_singleton_l.
- - rewrite insert_commute. 2: { intros [= Heq]. destruct l; simpl in *. injection Heq. lia. }
- rewrite shift_loc_assoc. rewrite -insert_union_l. rewrite (IH l (i + 1)%Z); last lia.
- rewrite -insert_union_l. done.
-Qed.
-*)
-
Lemma ghost_map_array_tag_update `{!bor_stateGS Σ} (γh : gname) (M : gmap (tag * block) (gmap Z scalar)) (v v' : list scalar) (t : tag) (l : loc) :
length v = length v' →
ghost_map_auth γh 1 M -∗
@@ -1528,66 +1246,6 @@ Proof.
all: by iFrame.
Qed.
-(*
-Lemma ghost_map_array_tag_insert `{!bor_stateGS Σ} (γh : gname) (M : gmap (tag * block) (gmap Z scalar)) (v : list scalar) (t : tag) (l : loc) :
- (∀ i : nat, (i < length v)%nat → M !! (t, l +ₗ i) = None) →
- ghost_map_auth γh 1 M ==∗
- ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +ₗ i) (DfracOwn 1) sc) ∗
- ghost_map_auth γh 1 (array_tag_map l t v ∪ M).
-Proof.
- iIntros (Hnone) "Hauth". iInduction v as [ | sc v ] "IH" forall (M l Hnone) "Hauth".
- - rewrite big_sepL_nil. iModIntro. rewrite map_empty_union. iFrame.
- - rewrite big_sepL_cons.
- iMod ("IH" $! M (l +â‚— 1) with "[] Hauth") as "[Helems Hauth]".
- { iPureIntro. intros i Hi. rewrite shift_loc_assoc. replace (1 + i)%Z with (Z.of_nat (S i)) by lia. apply Hnone.
- simpl; lia.
- }
- iMod (ghost_map_insert (t, l +â‚— 0%nat) sc with "Hauth") as "[Hauth Helem]".
- { rewrite lookup_union_None; split.
- - apply array_tag_map_lookup_None'. intros i Hi. destruct l; intros [= ?]. lia.
- - apply Hnone. simpl; lia.
- }
- iModIntro. iFrame "Helem". rewrite shift_loc_0_nat. simpl. rewrite insert_union_l. iFrame "Hauth".
- iApply (big_sepL_mono with "Helems"). intros i sc'' Hs. cbn. rewrite shift_loc_assoc.
- replace (Z.of_nat $ S i) with (1 + i)%Z by lia. done.
-Qed.
-
-Lemma ghost_map_array_tag_delete `{!bor_stateGS Σ} (γh : gname) (M : gmap (tag * block) (gmap Z scalar)) (v : list scalar) (t : tag) (l : loc) :
- ghost_map_auth γh 1 M -∗
- ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +ₗ i) (DfracOwn 1) sc) ==∗
- ghost_map_auth γh 1 (M ∖ array_tag_map l t v).
-Proof.
- iIntros "Hauth Helems".
- iApply (ghost_map_delete_big (array_tag_map l t v) with "Hauth [Helems]").
- iInduction v as [ | sc v] "IH" forall (l); first done.
- simpl. iApply big_sepM_insert.
- { destruct (_ !! _) eqn:Heq; last done.
- specialize (array_tag_map_lookup2 (l +â‚— 1) t v t l ltac:(eauto)) as [_ (i & _ & Hl)].
- destruct l. injection Hl. lia.
- }
- rewrite shift_loc_0_nat. iDestruct "Helems" as "[$ Helems]".
- iApply "IH". iApply (big_sepL_mono with "Helems").
- iIntros (i sc' Hi). simpl.
- rewrite shift_loc_assoc. replace (Z.of_nat (S i)) with (1 + i) by lia; done.
-Qed.
-
-Lemma ghost_map_array_tag_tk `{!bor_stateGS Σ} (γh : gname) (v : list scalar) (t : tag) (l : loc) tk :
- ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +ₗ i) (DfracOwn 1) sc) ==∗
- ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +ₗ i) (tk_to_frac tk) sc).
-Proof.
- destruct tk; cbn; [ | by eauto ..].
- iInduction v as [| sc v] "IH" forall (l); first by eauto.
- rewrite !big_sepL_cons. iIntros "[Hh Hr]".
- iMod (ghost_map_elem_persist with "Hh") as "$".
- iMod ("IH" $! (l +â‚— 1) with "[Hr]") as "Hr".
- - iApply (big_sepL_mono with "Hr"). intros i sc' Hs. simpl. rewrite shift_loc_assoc.
- by replace (Z.of_nat (S i)) with (1 + i) by lia.
- - iModIntro.
- iApply (big_sepL_mono with "Hr"). intros i sc' Hs. simpl. rewrite shift_loc_assoc.
- by replace (Z.of_nat (S i)) with (1 + i) by lia.
-Qed.
-*)
-
Section val_rel.
Context `{bor_stateGS Σ}.
(** Value relation *)
diff --git a/theories/tree_borrows/notation.v b/theories/tree_borrows/notation.v
index f46cea95..d150892e 100755
--- a/theories/tree_borrows/notation.v
+++ b/theories/tree_borrows/notation.v
@@ -89,8 +89,6 @@ Notation "'let:' x := e1 'in' e2" := (Let x%binder e1%E e2%E)
Notation "e1 ;; e2" := (let: <> := e1 in e2)%R
(at level 100, e2 at level 200, format "e1 ;; e2") : result_scope.
-(*Notation "fun: xl , e" := (FunV xl%binder e%E)*)
- (*(at level 102, xl at level 1, e at level 200).*)
Ltac solve_closed :=
match goal with
diff --git a/theories/tree_borrows/steps_access.v b/theories/tree_borrows/steps_access.v
index e894619c..6d2bad74 100755
--- a/theories/tree_borrows/steps_access.v
+++ b/theories/tree_borrows/steps_access.v
@@ -5,179 +5,6 @@
From simuliris.tree_borrows Require Export defs steps_foreach.
From iris.prelude Require Import options.
-(* Kept for now as an easy reference of the lemmas that SB needed
-Lemma access1_in_stack stk kind t cids n stk' :
- access1 stk kind t cids = Some (n, stk') →
- ∃ it, it ∈ stk ∧ it.(tg) = t ∧ it.(perm) ≠Disabled.
-Proof.
- rewrite /access1. case find_granting as [gip|] eqn:Eq1; [|done].
- apply fmap_Some in Eq1 as [[i it] [(IN & [GR Eq] & FR)%list_find_Some EQ]].
- intros ?. exists it. split; last split; [|done|].
- - by eapply elem_of_list_lookup_2.
- - intros Eq1. by rewrite Eq1 in GR.
-Qed.
-
-Lemma access1_tagged_sublist stk kind bor cids n stk' :
- access1 stk kind bor cids = Some (n, stk') → tagged_sublist stk' stk.
-Proof.
- rewrite /access1. case find_granting as [gip|]; [|done]. simpl.
- destruct kind.
- - case replace_check as [stk1|] eqn:Eq; [|done].
- simpl. intros. simplify_eq.
- rewrite -{2}(take_drop gip.1 stk). apply tagged_sublist_app; [|done].
- move : Eq. by apply replace_check_tagged_sublist.
- - case find_first_write_incompatible as [idx|]; [|done]. simpl.
- case remove_check as [stk1|] eqn:Eq; [|done].
- simpl. intros. simplify_eq.
- rewrite -{2}(take_drop gip.1 stk). apply tagged_sublist_app; [|done].
- move : Eq. by apply remove_check_tagged_sublist.
-Qed.
-
-Lemma access1_non_empty stk kind bor cids n stk' :
- access1 stk kind bor cids = Some (n, stk') → stk' ≠[].
-Proof.
- rewrite /access1. case find_granting as [gip|] eqn:Eq1; [|done].
- apply fmap_Some in Eq1 as [[i it] [[IN ?]%list_find_Some EQ]].
- subst gip; simpl.
- have ?: drop i stk ≠[].
- { move => ND. move : IN. by rewrite -(Nat.add_0_r i) -(lookup_drop) ND /=. }
- destruct kind.
- - case replace_check as [stk1|]; [|done].
- simpl. intros ?. simplify_eq => /app_nil [_ ?]. by subst.
- - case find_first_write_incompatible as [?|]; [|done]. simpl.
- case remove_check as [?|]; [|done].
- simpl. intros ?. simplify_eq => /app_nil [_ ?]. by subst.
-Qed.
-
-Lemma for_each_access1 α nxtc l n tg kind α' :
- for_each α l n false
- (λ stk, nstk' ↠access1 stk kind tg nxtc; Some nstk'.2) = Some α' →
- ∀ (l: loc) stk', α' !! l = Some stk' → ∃ stk, α !! l = Some stk ∧
- tagged_sublist stk' stk ∧ (stk ≠[] → stk' ≠[]).
-Proof.
- intros EQ. destruct (for_each_lookup _ _ _ _ _ EQ) as [EQ1 [EQ2 EQ3]].
- intros l1 stk1 Eq1.
- case (decide (l1.1 = l.1)) => [Eql|NEql];
- [case (decide (l.2 ≤ l1.2 < l.2 + n)) => [[Le Lt]|NIN]|].
- - have Eql2: l1 = l +â‚— Z.of_nat (Z.to_nat (l1.2 - l.2)). {
- destruct l, l1. move : Eql Le => /= -> ?.
- rewrite /shift_loc /= Z2Nat.id; [|lia]. f_equal. lia. }
- destruct (EQ2 (Z.to_nat (l1.2 - l.2)) stk1)
- as [stk [Eq [[n1 stk'] [Eq' Eq0]]%bind_Some]];
- [rewrite -(Nat2Z.id n) -Z2Nat.inj_lt; lia|by rewrite -Eql2|].
- exists stk. split; [by rewrite Eql2|]. simplify_eq.
- split; [by eapply access1_tagged_sublist|intros; by eapply access1_non_empty].
- - exists stk1. split; [|done]. rewrite -EQ3; [done|].
- intros i Lt Eq. apply NIN. rewrite Eq /=. lia.
- - exists stk1. split; [|done]. rewrite -EQ3; [done|].
- intros i Lt Eq. apply NEql. by rewrite Eq.
-Qed.
-
-Lemma for_each_access1_non_empty α cids l n tg kind α' :
- for_each α l n false
- (λ stk, nstk' ↠access1 stk kind tg cids; Some nstk'.2) = Some α' →
- wf_non_empty α → wf_non_empty α'.
-Proof.
- move => /for_each_access1 EQ1 WF ?? /EQ1 [? [? [? NE]]]. by eapply NE, WF.
-Qed.
-
-Lemma access1_stack_item_tagged_NoDup stk kind bor cids n stk' :
- access1 stk kind bor cids = Some (n, stk') →
- stack_item_tagged_NoDup stk → stack_item_tagged_NoDup stk'.
-Proof.
- rewrite /access1. case find_granting as [gip|] eqn:Eq1; [|done].
- apply fmap_Some in Eq1 as [[i it] [[IN ?]%list_find_Some EQ]].
- subst gip; simpl.
- destruct kind.
- - case replace_check as [stk1|] eqn:Eqc ; [|done].
- simpl. intros ?. simplify_eq.
- rewrite -{1}(take_drop n stk). move : Eqc.
- by apply replace_check_stack_item_tagged_NoDup_2.
- - case find_first_write_incompatible as [?|]; [|done]. simpl.
- case remove_check as [?|] eqn:Eqc ; [|done].
- simpl. intros ?. simplify_eq.
- rewrite -{1}(take_drop n stk). move : Eqc.
- apply remove_check_stack_item_tagged_NoDup_2.
-Qed.
-
-Lemma access1_read_eq it1 it2 stk tag t cids n stk':
- stack_item_tagged_NoDup stk →
- access1 stk AccessRead tag cids = Some (n, stk') →
- it1 ∈ stk → it2 ∈ stk' →
- it2.(perm) ≠Disabled →
- it1.(tg) = Tagged t → it2.(tg) = Tagged t → it1 = it2.
-Proof.
- intros ND ACC.
- have ND' := access1_stack_item_tagged_NoDup _ _ _ _ _ _ ACC ND.
- move : ACC. rewrite /= /access1 /=.
- case find_granting as [[idx pm]|] eqn:Eq1; [|done]. simpl.
- case replace_check as [stk1|] eqn:Eq2; [|done].
- simpl. intros ?. simplify_eq. intros In1.
- have SUB:= replace_check_tagged_sublist _ _ _ Eq2.
- rewrite elem_of_app. intros In2 ND2.
- destruct In2 as [In2|In2].
- - specialize (SUB _ In2) as (it3 & In3 & Eqt3 & Eqp3 & ND3).
- specialize (ND3 ND2).
- have ?: it3 = it2.
- { destruct it2, it3. simpl in *. by simplify_eq. }
- subst it3.
- apply (stack_item_tagged_NoDup_eq _ _ _ _ ND); [done|].
- rewrite -{1}(take_drop n stk) elem_of_app. by left.
- - apply (stack_item_tagged_NoDup_eq _ _ _ _ ND); [done|].
- rewrite -{1}(take_drop n stk) elem_of_app. by right.
-Qed.
-
-Lemma for_each_access1_stack_item α nxtc cids nxtp l n tg kind α' :
- for_each α l n false
- (λ stk, nstk' ↠access1 stk kind tg cids; Some nstk'.2) = Some α' →
- wf_stacks α nxtp nxtc → wf_stacks α' nxtp nxtc.
-Proof.
- intros ACC WF l' stk' Eq'.
- destruct (for_each_access1 _ _ _ _ _ _ _ ACC _ _ Eq') as [stk [Eq [SUB NN]]].
- split.
- - move => ? /SUB [? [IN [-> [-> ?]]]]. by apply (proj1 (WF _ _ Eq) _ IN).
- - clear SUB NN.
- destruct (for_each_lookup_case _ _ _ _ _ ACC _ _ _ Eq Eq') as [?|[Eqf ?]].
- { subst. by apply (WF _ _ Eq). }
- destruct (access1 stk kind tg cids) as [[]|] eqn:Eqf'; [|done].
- simpl in Eqf. simplify_eq.
- eapply access1_stack_item_tagged_NoDup; eauto. by apply (WF _ _ Eq).
-Qed.
-*)
-
-(** Dealloc *)
-(*
-Lemma for_each_dealloc_lookup α l n f α' :
- for_each α l n true f = Some α' →
- (∀ (i: nat), (i < n)%nat → α' !! (l +ₗ i) = None) ∧
- (∀ (l': loc), (∀ (i: nat), (i < n)%nat → l' ≠l +ₗ i) → α' !! l' = α !! l').
-Proof.
- revert α. induction n as [|n IH]; intros α; simpl.
- { move => [<-]. split; intros ??; by [lia|]. }
- case (α !! (l +ₗ n)) as [stkn|] eqn:Eqn; [|done] => /=.
- case f as [stkn'|] eqn: Eqn'; [|done] => /= /IH [IH1 IH2]. split.
- - intros i Lt. case (decide (i = n)) => Eq'; [subst i|].
- + rewrite IH2; [by apply lookup_delete|].
- move => ?? /shift_loc_inj /Nat2Z.inj ?. by lia.
- + apply IH1. by lia.
- - intros l' Lt. rewrite IH2.
- + rewrite lookup_delete_ne; [done|]. move => Eql'. apply (Lt n); by [lia|].
- + move => ??. apply Lt. lia.
-Qed.
-
-Lemma for_each_dealloc_lookup_Some α l n f α' :
- for_each α l n true f = Some α' →
- ∀ l' stk', α' !! l' = Some stk' →
- (∀ i : nat, (i < n)%nat → l' ≠l +ₗ i) ∧ α !! l' = Some stk'.
-Proof.
- intros EQ. destruct (for_each_dealloc_lookup _ _ _ _ _ EQ) as [EQ1 EQ2].
- intros l1 stk1 Eq1.
- destruct (block_case l l1 n) as [NEql|Eql].
- - rewrite -EQ2 //.
- - destruct Eql as (i & Lt & ?). subst l1. rewrite EQ1 // in Eq1.
-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) →
diff --git a/theories/tree_borrows/steps_preserve.v b/theories/tree_borrows/steps_preserve.v
index d3a20ebe..0bddf4e9 100644
--- a/theories/tree_borrows/steps_preserve.v
+++ b/theories/tree_borrows/steps_preserve.v
@@ -2,9 +2,18 @@ From iris.prelude Require Import prelude options.
From simuliris.tree_borrows Require Import lang_base notation bor_semantics tree tree_lemmas bor_lemmas defs.
From iris.prelude Require Import options.
+(** Lemmas about borrow steps preserving properties of the tree.
+ This is related to [steps_wf.v], but where [steps_wf] states lemmas about
+ preservation of well-formedness by all borrow steps, these are lower-level.
+ Many lemmas here will seem trivial (e.g. if you have a tree in which a tag
+ is unique and you apply a tag-preserving function, the tag is still unique). *)
+
(* Any function that operates only on permissions (which is all transitions steps)
leaves the tag and protector unchanged which means that most of the preservation lemmas
- are trivial once we get to the level of items *)
+ are trivial once we get to the level of items.
+ Preservation of metadata includes preservation of relationships since
+ the parent-child relation is defined by the relative location of tags
+ (which are metadata). *)
Definition preserve_item_metadata (fn:item -> option item) :=
forall it it', fn it = Some it' -> it.(itag) = it'.(itag) /\ it.(iprot) = it'.(iprot) /\ it.(initp) = it'.(initp).
@@ -140,9 +149,10 @@ Proof.
erewrite new_item_has_tag; done.
Qed.
+(** Detailed specification of the effects of one access.
+ This is to trees what [mem_apply_range'_spec] is to ranges. *)
Lemma apply_access_spec_per_node
{tr affected_tag access_tag pre fn cids range tr'}
- (*(ExAcc : tree_contains access_tag tr)*)
(ExAff : tree_contains affected_tag tr)
(UnqAff : tree_item_determined affected_tag pre tr)
(Access : tree_apply_access fn cids access_tag range tr = Some tr')
@@ -182,6 +192,8 @@ Proof.
tauto.
Qed.
+(** Reachability of a state behaves as expected in between applications
+ of functions compatible with [reach]. *)
Lemma apply_access_perm_preserves_backward_reach
{pre post kind rel b p0}
(Access : apply_access_perm kind rel b pre = Some post)
@@ -314,7 +326,7 @@ Proof.
all: intros H H'; inversion H'; inversion H.
Qed.
-
+(** Initialized status is monotonous: an initialized location stays initialized. *)
Lemma memory_access_preserves_perminit
{access_tag affected_tag pre tr post tr' kind cids range z zpre zpost}
(ExAff : tree_contains affected_tag tr)
@@ -344,6 +356,7 @@ Proof.
all: rewrite Lkup; simpl; try exact Apply.
Qed.
+(** Furthermore a child access produces an initialized. *)
Lemma apply_access_perm_child_produces_perminit
{pre post kind b rel}
(CHILD : if rel is Child _ then True else False)
@@ -390,6 +403,7 @@ Proof.
all: simpl; done.
Qed.
+(** Protected + initialized prevents loss of [Active]. *)
Lemma apply_access_perm_protected_initialized_preserves_active
{pre post kind rel}
(Access : apply_access_perm kind rel true pre = Some post)
diff --git a/theories/tree_borrows/steps_progress.v b/theories/tree_borrows/steps_progress.v
index 783fd92e..81bacaf5 100755
--- a/theories/tree_borrows/steps_progress.v
+++ b/theories/tree_borrows/steps_progress.v
@@ -2,6 +2,9 @@
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. *)
+
From simuliris.tree_borrows Require Export steps_wf.
From Equations Require Import Equations.
From iris.prelude Require Import options.
@@ -29,7 +32,7 @@ Proof.
exact Dom.
Qed.
-
+(* Basically, [tree_apply_access] works iff every node accepts the inner function being applied *)
Lemma apply_access_success_condition tr cids access_tag range fn :
every_node (fun it => is_Some (item_apply_access fn cids (rel_dec tr access_tag (itag it)) range it)) tr
<-> is_Some (tree_apply_access fn cids access_tag range tr).
@@ -40,7 +43,6 @@ Proof.
tauto.
Qed.
-
Lemma apply_access_fail_condition tr cids access_tag range fn :
exists_node (fun it => item_apply_access fn cids (rel_dec tr access_tag (itag it)) range it = None) tr
<-> tree_apply_access fn cids access_tag range tr = None.
@@ -51,6 +53,7 @@ Proof.
tauto.
Qed.
+(* [mem_apply_range'] succeeds iff every offset succeeds. *)
Lemma mem_apply_range'_success_condition {X} (map : gmap Z X) fn range :
(forall l, range'_contains range l -> is_Some (fn (map !! l))) <->
is_Some (mem_apply_range' fn range map).
@@ -179,46 +182,6 @@ Proof.
destruct (ProtVulnerable ltac:(reflexivity)); discriminate.
Qed.
-
-
-(*
-Lemma dealloc1_progress stk bor cids
- (PR: Forall (λ it, ¬ is_active_protector cids it) stk)
- (BOR: ∃ it, it ∈ stk ∧ it.(tg) = bor ∧
- it.(perm) ≠Disabled ∧ it.(perm) ≠SharedReadOnly) :
- is_Some (dealloc1 stk bor cids).
-Proof.
- rewrite /dealloc1.
- destruct (find_granting_is_Some stk AccessWrite bor) as [? Eq]; [naive_solver|].
- rewrite Eq /find_top_active_protector list_find_None_inv;
- [by eexists|done].
-Qed.
-
-Lemma for_each_is_Some α l (n: nat) b f :
- (∀ m : Z, 0 ≤ m ∧ m < n → l +ₗ m ∈ dom α) →
- (∀ (m: nat) stk, (m < n)%nat → α !! (l +ₗ m) = Some stk → is_Some (f stk)) →
- is_Some (for_each α l n b f).
-Proof.
- revert α. induction n as [|n IHn]; intros α IN Hf; [by eexists|]. simpl.
- assert (is_Some (α !! (l +ₗ n))) as [stk Eq].
- { apply (elem_of_dom (D:=gset loc)), IN. by lia. }
- rewrite Eq /=. destruct (Hf n stk) as [stk' Eq']; [lia|done|].
- rewrite Eq' /=. destruct b; apply IHn.
- - intros. apply elem_of_dom. rewrite lookup_delete_ne.
- + apply (elem_of_dom (D:=gset loc)), IN. lia.
- + move => /shift_loc_inj. lia.
- - intros ???. rewrite lookup_delete_ne.
- + apply Hf. lia.
- + move => /shift_loc_inj. lia.
- - intros. apply elem_of_dom. rewrite lookup_insert_ne.
- + apply (elem_of_dom (D:=gset loc)), IN. lia.
- + move => /shift_loc_inj. lia.
- - intros ???. rewrite lookup_insert_ne.
- + apply Hf. lia.
- + move => /shift_loc_inj. lia.
-Qed.
-*)
-
(* For a protector to allow deallocation it must be weak or inactive *)
Definition item_deallocateable_protector cids (it: item) :=
match it.(iprot) with
@@ -226,47 +189,6 @@ Definition item_deallocateable_protector cids (it: item) :=
| _ => True
end.
-(* Deallocation progress is going to be a bit more tricky because we need the success of the write *)
-(*
-Lemma memory_deallocated_progress α cids l bor (n: nat) :
- (∀ m : Z, 0 ≤ m ∧ m < n → l +ₗ m ∈ dom α) →
- (∀ (m: nat) stk, (m < n)%nat → α !! (l +ₗ m) = Some stk →
- (∃ it, it ∈ stk ∧ it.(itag) = bor ∧
- it.(perm) ≠Disabled ∧ it.(perm) ≠SharedReadOnly) ∧
- ∀ it, it ∈ stk → item_inactive_protector cids it) →
- is_Some (memory_deallocated α cids l bor n).
-Proof.
- intros IN IT. apply for_each_is_Some; [done|].
- intros m stk Lt Eq. destruct (IT _ _ Lt Eq) as [In PR].
- destruct (dealloc1_progress stk bor cids) as [? Eq1];
- [|done|rewrite Eq1; by eexists].
- apply Forall_forall. move => it /PR.
- rewrite /item_inactive_protector /is_active_protector /is_active.
- case protector; naive_solver.
-Qed.
-*)
-(*
-Lemma memory_deallocate_progress (σ: state) l tg (sz:nat) (WF: state_wf σ) :
- (∀ m : Z, is_Some (σ.(shp) !! (l +ₗ m)) ↔ 0 ≤ m ∧ m < sz) →
- (sz > 0)%nat →
- trees_contain tg (strs σ) l.1 →
- is_Some (apply_within_trees (memory_deallocate σ.(scs) tg (l.2, sz)) l.1 σ.(strs)).
-Proof.
- intros Hfoo Hbar Hcont.
- eexists. Locate trees_contain. unfold trees_contain in Hcont. unfold trees_at_block in Hcont.
- destruct (strs σ !! l.1) as [tr|] eqn:Heqtr; last done.
- rewrite /apply_within_trees /memory_deallocate Heqtr /=.
- unfold tree_apply_access.
- Print join_nodes.
- Print map_nodes.
- Search join_nodes.
- simpl.
- Print apply_within_trees.
- Print memory_deallocate.
- Print tree_apply_access.
- Print item_apply_access.
- Print memory_deallocate.
-*)
Lemma dealloc_base_step' P (σ: state) l tg (sz:nat) α' (WF: state_wf σ) :
(∀ m : Z, is_Some (σ.(shp) !! (l +ₗ m)) ↔ 0 ≤ m ∧ m < sz) →
(sz > 0)%nat →
@@ -278,25 +200,6 @@ Proof.
intros Hdom Hpos Hcont Happly. destruct l as [blk off].
econstructor; econstructor; auto.
Qed.
-(*
-Lemma dealloc_base_step P (σ: state) T l bor
- (WF: state_wf σ)
- (BLK: ∀ m : Z, l +ₗ m ∈ dom σ.(shp) ↔ 0 ≤ m ∧ m < tsize T)
- (BOR: ∀ (n: nat) stk, (n < tsize T)%nat →
- σ.(sst) !! (l +ₗ n) = Some stk →
- (∃ it, it ∈ stk ∧ it.(tg) = bor ∧
- it.(perm) ≠Disabled ∧ it.(perm) ≠SharedReadOnly) ∧
- ∀ it, it ∈ stk → item_inactive_protector σ.(scs) it) :
- ∃ σ',
- base_step P (Free (Place l bor T)) σ #[☠] σ' [].
-Proof.
- destruct (memory_deallocated_progress σ.(sst) σ.(scs) l bor (tsize T))
- as [α' Eq']; [|done|].
- - intros. rewrite -(state_wf_dom _ WF). by apply BLK.
- - eexists. econstructor; econstructor; [|done].
- intros. by rewrite -(elem_of_dom (D:= gset loc) σ.(shp)).
-Qed.
-*)
(* Success of `read_mem` on the heap is unchanged. *)
Lemma read_mem_is_Some' l n h :
@@ -361,147 +264,8 @@ Proof.
rewrite -Hs; last lia. rewrite -Hv'; last lia. intros -> [= ->]. done.
Qed.
-(*
-Lemma replace_check'_is_Some cids acc stk :
- (∀ it, it ∈ stk → it.(perm) = Unique → item_inactive_protector cids it) →
- is_Some (replace_check' cids acc stk).
-Proof.
- revert acc. induction stk as [|si stk IH]; intros acc PR; simpl; [by eexists|].
- case decide => EqU; last by (apply IH; set_solver).
- rewrite (Is_true_eq_true (check_protector cids si)); first by (apply IH; set_solver).
- have IN: si ∈ si :: stk by set_solver. apply PR in IN; [|done].
- move : IN. rewrite /check_protector /item_inactive_protector.
- case si.(protector) => [? /negb_prop_intro|//]. by case is_active.
-Qed.
-
-Lemma replace_check_is_Some cids stk :
- (∀ it, it ∈ stk → it.(perm) = Unique → item_inactive_protector cids it) →
- is_Some (replace_check cids stk).
-Proof. move => /replace_check'_is_Some IS. by apply IS. Qed.
-
-*)
-
-
-(*
-Definition access1_read_pre cids (stk: stack) (bor: tag) :=
- ∃ (i: nat) it, stk !! i = Some it ∧ it.(tg) = bor ∧ it.(perm) ≠Disabled ∧
- ∀ (j: nat) jt, (j < i)%nat → stk !! j = Some jt →
- (jt.(perm) = Disabled ∨ jt.(tg) ≠bor) ∧
- match jt.(perm) with
- | Unique => item_inactive_protector cids jt
- | _ => True
- end.
-
-Definition access1_write_pre cids (stk: stack) (bor: tag) :=
- ∃ (i: nat) it, stk !! i = Some it ∧ it.(perm) ≠Disabled ∧
- it.(perm) ≠SharedReadOnly ∧ it.(tg) = bor ∧
- ∀ (j: nat) jt, (j < i)%nat → stk !! j = Some jt →
- (jt.(perm) = Disabled ∨ jt.(perm) = SharedReadOnly ∨ jt.(tg) ≠bor) ∧
- match find_first_write_incompatible (take i stk) it.(perm) with
- | Some idx =>
- if decide (j < idx)%nat then
- (* Note: if a Disabled item is already in the stack, then its protector
- must have been inactive since its insertion, so this condition is
- unneccessary. *)
- item_inactive_protector cids jt
- else True
- | _ => True
- end.
- *)
-
Definition is_write (access: access_kind) : bool :=
match access with AccessWrite => true | _ => false end.
-(*
-Definition access1_pre
- cids (stk: stack) (access: access_kind) (bor: tag) :=
- ∃ (i: nat) it, stk !! i = Some it ∧ it.(perm) ≠Disabled ∧
- (is_write access → it.(perm) ≠SharedReadOnly) ∧ it.(tg) = bor ∧
- ∀ (j: nat) jt, (j < i)%nat → stk !! j = Some jt →
- (jt.(perm) = Disabled ∨
- (if is_write access then jt.(perm) = SharedReadOnly ∨ jt.(tg) ≠bor
- else jt.(tg) ≠bor)) ∧
- if is_write access then
- match find_first_write_incompatible (take i stk) it.(perm) with
- | Some idx =>
- if decide (j < idx)%nat then
- (* Note: if a Disabled item is already in the stack, then its protector
- must have been inactive since its insertion, so this condition is
- unneccessary. *)
- item_inactive_protector cids jt
- else True
- | _ => True
- end
- else
- match jt.(perm) with
- | Unique => item_inactive_protector cids jt
- | _ => True
- end.
- *)
-
-(*
-Lemma access1_is_Some cids stk kind bor
- (BOR: access1_pre cids stk kind bor) :
- is_Some (access1 stk kind bor cids).
-Proof.
- destruct BOR as (i & it & Eqi & ND & IW & Eqit & Lti).
- rewrite /access1 /find_granting.
- rewrite (_: list_find (matched_grant kind bor) stk = Some (i, it)); last first.
- { apply list_find_Some_not_earlier. split; last split; [done|..].
- - split; [|done].
- destruct kind; [by apply grants_access_all|by apply grants_write_all, IW].
- - intros ?? Lt Eq GR. destruct (Lti _ _ Lt Eq) as [[Eq1|NEq1] NEq2].
- { move : GR. rewrite /matched_grant Eq1 /=. naive_solver. }
- destruct kind; [by apply NEq1, GR|]. destruct NEq1 as [OR|OR].
- + move : GR. rewrite /matched_grant OR /=. naive_solver.
- + by apply OR, GR. } simpl.
- have ?: (i ≤ length stk)%nat. { by eapply Nat.lt_le_incl, lookup_lt_Some. }
- destruct kind.
- - destruct (replace_check_is_Some cids (take i stk)) as [? Eq2];
- [|rewrite Eq2 /=; by eexists].
- intros jt [j Eqj]%elem_of_list_lookup_1 IU.
- have ?: (j < i)%nat.
- { rewrite -(length_take_le stk i); [|done]. by eapply lookup_lt_Some. }
- destruct (Lti j jt) as [Eq1 PR]; [done|..].
- + symmetry. by rewrite -Eqj lookup_take.
- + move : PR. by rewrite /= IU.
- - destruct (find_first_write_incompatible_is_Some (take i stk) it.(perm))
- as [idx Eqx]; [done|by apply IW|]. rewrite Eqx /=.
- destruct (remove_check_is_Some cids (take i stk) idx) as [stk' Eq'];
- [..|rewrite Eq'; by eexists].
- + move : Eqx. apply find_first_write_incompatible_length.
- + intros j jt Lt Eqj.
- have ?: (j < i)%nat.
- { rewrite -(length_take_le stk i); [|done]. by eapply lookup_lt_Some. }
- destruct (Lti j jt) as [Eq1 PR]; [done|..].
- * symmetry. by rewrite -Eqj lookup_take.
- * move : PR. by rewrite /= Eqx decide_True.
-Qed.
-
-Lemma access1_read_is_Some cids stk bor
- (BOR: access1_read_pre cids stk bor) :
- is_Some (access1 stk AccessRead bor cids).
-Proof.
- destruct BOR as (i & it & Eqi & Eqit & ND & Lti).
- apply access1_is_Some. exists i, it. do 4 (split; [done|]).
- intros j jt Lt Eq. by destruct (Lti _ _ Lt Eq).
-Qed.
- *)
-
-(*
-Lemma memory_read_is_Some α cids l bor (n: nat) :
- (∀ m, (m < n)%nat → l +ₗ m ∈ dom α) →
- (∀ (m: nat) stk, (m < n)%nat →
- α !! (l +ₗ m) = Some stk → access1_read_pre cids stk bor) →
- is_Some (memory_read α cids l bor n).
-Proof.
- intros IN STK. apply for_each_is_Some.
- - intros m []. rewrite -(Z2Nat.id m); [|done]. apply IN.
- rewrite -(Nat2Z.id n) -Z2Nat.inj_lt; [done..|lia].
- - intros m stk Lt Eq.
- specialize (STK _ _ Lt Eq).
- destruct (access1_read_is_Some _ _ _ STK) as [? Eq2]. rewrite Eq2. by eexists.
-Qed.
- *)
Lemma apply_within_trees_unchanged fn blk trs trs' :
(∀ tr, trs !! blk = Some tr → fn tr = Some tr) →
diff --git a/theories/tree_borrows/steps_wf.v b/theories/tree_borrows/steps_wf.v
index e78af25a..d3b65255 100755
--- a/theories/tree_borrows/steps_wf.v
+++ b/theories/tree_borrows/steps_wf.v
@@ -2,6 +2,9 @@
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 iris.prelude Require Import options.
diff --git a/theories/tree_borrows/tree.v b/theories/tree_borrows/tree.v
index 72039ac1..400ee57e 100644
--- a/theories/tree_borrows/tree.v
+++ b/theories/tree_borrows/tree.v
@@ -19,30 +19,36 @@ Proof.
Qed.
-(* Generic tree
- Note: we are using the "tilted" representation of n-ary trees
- where the binary children are the next n-ary sibling and
- the first n-ary child.
- This is motivated by the much nicer induction principles
- we get, but requires more careful definition of the
- parent-child relationship.
+(* Generic tree *)
+(* NOTE: we are using the "tilted" representation of n-ary trees
+ where the binary children are the next n-ary sibling and the first n-ary child.
+ This is motivated by the much nicer induction principles we get,
+ but requires more careful definition of the parent-child relationship.
+ In any case anything we do here is abstracted away as far as the more
+ high-level principles are concerned.
*)
Inductive tree X :=
| empty
| branch (data:X) (sibling child:tree X)
.
-(* x
+(* EXAMPLE:
+
+ the n-ary tree of width 4 and height 2
+
+ x
|- y1
|- y2
|- y3
|- y4
+ is encoded by a binary tree of height 5
+
branch x
empty
(branch y1
(branch y2
(branch y3
- (branch y4)
+ (branch y4 empty empty)
empty
empty
empty
@@ -56,6 +62,11 @@ Definition of_branch {X} (br:tbranch X)
: tree X :=
let '(root, lt, rt) := br in branch root lt rt.
+Definition root {X} (br:tbranch X)
+ : X := let '(r, _, _) := br in r.
+
+(** The main traversal operation is the folding. *)
+
Definition fold_subtrees {X Y} (unit:Y) (combine:tbranch X -> Y -> Y -> Y)
: tree X -> Y := fix aux tr : Y :=
match tr with
@@ -63,13 +74,13 @@ Definition fold_subtrees {X Y} (unit:Y) (combine:tbranch X -> Y -> Y -> Y)
| branch data sibling child => combine (data, sibling, child) (aux sibling) (aux child)
end.
-Definition root {X} (br:tbranch X)
- : X := let '(r, _, _) := br in r.
-
Definition fold_nodes {X Y} (unit:Y) (combine:X -> Y -> Y -> Y)
: tree X -> Y := fold_subtrees unit (fun subtree sibling child => combine (root subtree) sibling child).
-Definition map_nodes {X Y} (fn:X -> Y) : tree X -> tree Y := fold_nodes empty (compose branch fn).
+(** From which we define [map] as is standard. *)
+
+Definition map_nodes {X Y} (fn:X -> Y) : tree X -> tree Y :=
+ fold_nodes empty (compose branch fn).
Definition join_nodes {X}
: tree (option X) -> option (tree X) := fix aux tr {struct tr} : option (tree X) :=
@@ -82,6 +93,9 @@ Definition join_nodes {X}
Some $ branch data sibling child
end.
+(** Quantifiers over trees, universal and existential.
+ All of them are of course decidable. *)
+
Definition every_subtree {X} (prop:tbranch X -> Prop) (tr:tree X)
:= fold_subtrees True (fun sub lt rt => prop sub /\ lt /\ rt) tr.
Global Instance every_subtree_dec {X} prop (tr:tree X) : (forall x, Decision (prop x)) -> Decision (every_subtree prop tr).
@@ -100,9 +114,14 @@ Definition exists_node {X} (prop:X -> Prop) (tr:tree X) := fold_nodes False (fun
Global Instance exists_node_dec {X} prop (tr:tree X) : (forall x, Decision (prop x)) -> Decision (exists_node prop tr).
Proof. intro. induction tr; solve_decision. Defined.
+
+(** Alternative to a quantifier, we can state exactly how many nodes
+ satisfy a certain property. From this we derive unique existential quantification. *)
Definition count_nodes {X} (prop:X -> bool) :=
fold_nodes 0 (fun data lt rt => (if prop data then 1 else 0) + lt + rt).
+(* As a consequence of the representation, strict children are all
+ the nodes from the right subtree. *)
Definition exists_strict_child {X} (prop:X -> Prop)
: tbranch X -> Prop := fun '(_, _, child) => exists_node prop child.
Global Instance exists_strict_child_dec {X} prop (tr:tbranch X) :
@@ -114,6 +133,11 @@ Definition empty_children {X} (tr:tbranch X)
let '(_, _, children) := tr in
children = empty.
+(** Other main tree operation is insertion.
+ We use a somewhat nonstandard definition in which insertion occurs
+ as a child of every node that satisfies a certain property.
+ You will need quantifiers about the existence of nodes that satisfy
+ [search_dec] if you want to make sure that the node is actually inserted. *)
Definition insert_child_at {X} (tr:tree X) (ins:X) (search:X -> Prop) {search_dec:forall x, Decision (search x)} : tree X :=
(fix aux tr : tree X :=
match tr with
@@ -128,7 +152,10 @@ Definition insert_child_at {X} (tr:tree X) (ins:X) (search:X -> Prop) {search_de
) tr.
Definition fold_siblings {X Y} (empty:Y) (fn : X -> Y -> Y) (tr : tree X) : Y :=
- fold_nodes empty (λ x tl _, fn x tl) tr.
+ fold_nodes empty (λ this siblings _, fn this siblings) tr.
+
+(** Immediate children are a bit more tricky to reason about.
+ They are the entire leftmost *branch* of the right subtree. *)
Fixpoint fold_immediate_children_at {X Y} (prop:X -> bool) (empty:Y) (fn : X -> Y -> Y) (tr : tree X) : list Y :=
match tr with empty => nil
| branch x tl tr => (if prop x then [fold_siblings empty fn tr] else nil) ++
diff --git a/theories/tree_borrows/tree_access_laws.v b/theories/tree_borrows/tree_access_laws.v
index 3f01f843..b99f619f 100644
--- a/theories/tree_borrows/tree_access_laws.v
+++ b/theories/tree_borrows/tree_access_laws.v
@@ -25,7 +25,7 @@ Proof.
destruct (trs !! blk); [|tauto].
intros Ex Eq. injection Eq; intros; subst. assumption.
Qed.
-(***** not part of the API *****)
+(***** END not part of the API *****)
Lemma trees_contain_trees_lookup_1 trs blk tg :
wf_trees trs →
@@ -329,8 +329,8 @@ Proof.
Qed.
(* Reverse lifting to single trees.
- This is a roundabout of proving these, but we started with the lemmas above and this way there is the least refactoring effort. *)
-
+ This is a roundabout of proving these, but we started with the lemmas above
+ and this way there is the least refactoring effort. *)
Lemma wf_tree_wf_singleton_any z tr : wf_tree tr → wf_trees (singletonM z tr).
Proof.
@@ -427,7 +427,8 @@ Proof.
Qed.
-(* Some more facts about trees. These could be refactored, maybe? *)
+(* Some more facts about trees. *)
+(* TODO: These could be refactored, maybe? *)
Lemma apply_access_perm_access_remains_disabled b acc rel isprot itmo itmn :
maybe_non_children_only b (apply_access_perm acc) rel isprot itmo = Some itmn →
@@ -768,4 +769,4 @@ Proof.
2: done. 2: by eapply Hwf. 2: done. 2: done.
- rewrite /= insert_id //.
- by exists it.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/tree_borrows/wf.v b/theories/tree_borrows/wf.v
index f8e145f6..2926d2d7 100755
--- a/theories/tree_borrows/wf.v
+++ b/theories/tree_borrows/wf.v
@@ -25,7 +25,7 @@ Section expr_wf.
Fixpoint gen_expr_wf (e : expr) : Prop :=
expr_head_wf (expr_split_head e).1 ∧
match e with
- (** [value_wf v] should be part of [expr_head_wf (Val v)] because
+ (** NOTE: [value_wf v] could be part of [expr_head_wf (Val v)] because
[log_rel_structural] only provides [expr_head_wf]. *)
| Val v => True
| Var x => True
@@ -44,7 +44,7 @@ Section expr_wf.
| Case e branches => gen_expr_wf e ∧ Forall id (fmap gen_expr_wf branches)
| While e1 e2 => gen_expr_wf e1 ∧ gen_expr_wf e2
| Fork e => gen_expr_wf e
- (* These should have been handled by [expr_head_wf]. *)
+ (* NOTE: These could also have been handled by [expr_head_wf]. *)
| EndCall e => gen_expr_wf e
| InitCall => True (* administrative *)
| Place _ _ _ => True (* literal pointers *)
--
GitLab