From f6e00a2b9cfe06e6c92fd7b370407ac44e7f452b Mon Sep 17 00:00:00 2001
From: Neven Villani <vanille@crans.org>
Date: Fri, 9 Feb 2024 17:01:06 +0100
Subject: [PATCH] fixing the dealloc semantics

---
 theories/tree_borrows/bor_semantics.v | 43 ++++++++++++++-------------
 1 file changed, 22 insertions(+), 21 deletions(-)

diff --git a/theories/tree_borrows/bor_semantics.v b/theories/tree_borrows/bor_semantics.v
index 030c4966..62c1ff2f 100755
--- a/theories/tree_borrows/bor_semantics.v
+++ b/theories/tree_borrows/bor_semantics.v
@@ -5,6 +5,7 @@ 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.
+
 From simuliris.tree_borrows Require Export lang_base notation tree tree_lemmas.
 From iris.prelude Require Import options.
 
@@ -340,13 +341,13 @@ Global Instance protector_is_strong_dec prot : Decision (protector_is_strong pro
 Proof. rewrite /protector_is_strong. try repeat case_match; solve_decision. Qed.
 
 (* State machine including protector UB *)
-Definition apply_access_perm kind rel (isprot:bool) (protector_relevant:bool)
+Definition apply_access_perm kind rel (isprot:bool)
   : app lazy_permission := fun operm =>
   let old := operm.(perm) in
   new โ† apply_access_perm_inner kind rel isprot old;
   validated โ† if operm.(initialized) then (
     (* only if the permission is initialized do we possibly trigger protector UB *)
-    if isprot && protector_relevant && bool_decide (new = Disabled) then (
+    if isprot && bool_decide (new = Disabled) then (
         None
     ) else Some new
   ) else Some new;
@@ -354,32 +355,31 @@ Definition apply_access_perm kind rel (isprot:bool) (protector_relevant:bool)
     (most_init operm.(initialized) (requires_init rel)) (* can only become more initialized *)
     validated.
 
-Definition item_apply_access (fn : rel_pos -> bool -> bool -> app lazy_permission) strong cids rel range
+Definition item_apply_access (fn : rel_pos -> bool -> app lazy_permission) cids rel range
   : app item := fun it =>
   let oldps := it.(iperm) in
   let protected := bool_decide (protector_is_active it.(iprot) cids) in
-  let protector_relevant := bool_decide (strong = ProtStrong \/ protector_is_strong it.(iprot)) in
   newps โ† permissions_apply_range' (mkPerm PermLazy it.(initp)) range
-    (fn rel protected protector_relevant) oldps;
+    (fn rel protected) oldps;
   Some $ mkItem it.(itag) it.(iprot) it.(initp) newps.
 
 (* FIXME: share code *)
 Definition tree_apply_access
   (fn:rel_pos -> bool -> bool -> app lazy_permission)
-  strong cids (access_tag:tag) range (tr:tree item)
+  cids (access_tag:tag) range (tr:tree item)
   : option (tree item) :=
   let app : item -> option item := fun it => (
-    item_apply_access fn strong cids (rel_dec tr access_tag it.(itag)) range it
+    item_apply_access fn cids (rel_dec tr access_tag it.(itag)) range it
   ) in
   join_nodes (map_nodes app tr).
 
 Definition tree_apply_access_nonchildren_only
   (fn:rel_pos -> bool -> bool -> app lazy_permission)
-  strong cids (access_tag:tag) range (tr:tree item)
+  cids (access_tag:tag) range (tr:tree item)
   : option (tree item) :=
   let app : item -> option item := fun it => (
     (* FIXME This does not skip children *)
-    item_apply_access fn strong cids (rel_dec tr access_tag it.(itag)) range it
+    item_apply_access fn cids (rel_dec tr access_tag it.(itag)) range it
   ) in
   join_nodes (map_nodes app tr).
 
@@ -395,16 +395,19 @@ Definition extend_trees t blk
 
 (* Perform the access check on a block of continuous memory.
  * This implements Tree::before_memory_{read,write,deallocation}. *)
-Definition memory_access kind strong cids tg range
+Definition memory_access kind cids tg range
   : app (tree item) := fun tr =>
-  tree_apply_access (apply_access_perm kind) strong cids tg range tr.
-Definition memory_access_nonchildren_only kind strong cids tg range
+  tree_apply_access (apply_access_perm kind) cids tg range tr.
+Definition memory_access_nonchildren_only kind cids tg range
   : app (tree item) := fun tr =>
-  tree_apply_access_nonchildren_only (apply_access_perm kind) strong cids tg range tr.
+  tree_apply_access_nonchildren_only (apply_access_perm kind) cids tg range tr.
 
 Definition memory_deallocate cids t range
   : app (tree item) := fun tr =>
-  tree_apply_access (apply_access_perm AccessWrite) ProtWeak cids t range tr.
+  tree_apply_access (apply_access_perm AccessWrite) cids t range tr
+  ยป= fun tr' -> tree_apply_access (fun it =>
+    if bool_decide (protector_is_strong it.(iprot) then None else Some it
+  ) cids t range tr
 
 (* Normal reachability definition is not easily destructable, so we're defining it
    manually and proving it's equivalent to the reflexive transitive closuse of one step.
@@ -532,12 +535,11 @@ Lemma IsTag_reverse it it' :
 Proof. unfold IsTag. auto. Qed.
 
 Lemma apply_access_idempotent
-  {kind rel} (isprot isstrong isprot' isstrong':bool) {perm perm'}
+  {kind rel} (isprot isprot' : bool) {perm perm'}
   (ProtIncr : if isprot then True else isprot' = false)
-  (StongIncr : if isstrong then True else isstrong' = false)
-  (Acc1 : apply_access_perm kind rel isprot isstrong perm = Some perm')
-  (Witness : exists x, x = (kind, rel, perm, perm', isprot, isstrong, isprot', isstrong'))
-  : apply_access_perm kind rel isprot' isstrong' perm' = Some perm'.
+  (Acc1 : apply_access_perm kind rel isprot perm = Some perm')
+  (Witness : exists x, x = (kind, rel, perm, perm', isprot, isprot'))
+  : apply_access_perm kind rel isprot' perm' = Some perm'.
 Proof.
   destruct perm as [init perm]; destruct perm' as [init' perm'].
   unfold apply_access_perm in *.
@@ -545,11 +547,10 @@ Proof.
      everything. Still, let's try to do it in a smart order otherwise it'll generate
      upwards of 2000 cases *)
   destruct kind, rel.
-  all: destruct isprot, isstrong.
+  all: destruct isprot.
   all: destruct init, perm as [[][]| | |]; simpl in *; inversion Acc1; subst.
   all: simpl; try auto.
   all: destruct isprot'; simpl; try auto.
-  all: destruct isstrong'; simpl; try auto.
 Qed.
 
 Definition tree_contains tg tr
-- 
GitLab