Merge branch 'master' into ci/tree-borrows

README.md

 # Simuliris Coq development
+
 This repository contains the Coq development of Simuliris (paper presented at POPL22: https://iris-project.org/pdfs/2022-popl-simuliris.pdf).
 
-## Setup 
-This project is known to build with [Coq](https://coq.inria.fr/) 8.18.0.
-It depends on recent development versions of [std++](https://gitlab.mpi-sws.org/iris/stdpp) and [Iris](https://gitlab.mpi-sws.org/iris/iris), as well as [coq-equations](https://github.com/mattam82/Coq-Equations).
+## Prerequisites
+
+This version is known to compile with:
+
+ - Coq 8.18.0
+ - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
+ - A recent version of [Coq-Equations](https://github.com/mattam82/Coq-Equations)
 
+## Building from source
 
-We recommend using [opam](https://opam.ocaml.org/) (version >= 2.0, tested on 2.0.8) for the installation.
+When building from source, we recommend to use opam (2.0.0 or newer) for
+installing the dependencies.  This requires the following two repositories:
 
-Please execute the following instructions in the folder containing this README, replacing `N` with the number of jobs you'd like to use for compilation.
-```
-opam switch create simuliris 4.11.1
-opam switch link simuliris .
-opam repo add coq-released https://coq.inria.fr/opam/released
-opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
-make -jN builddep
-make -jN
+    opam repo add coq-released https://coq.inria.fr/opam/released
+    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
 
-```
+Once you got opam set up, run `make build-dep` to install the right versions
+of the dependencies.
 
 ## Structure
+
 The project follows the following structure below the `theories` folder:
 - `logic` and `base_logic` contain libraries for defining fixpoints as well as general ghost state constructions.
 - `simulation` contains the language-generic parts of the framework, in particular the definition of the simulation relation and the general adequacy proof.
@@ -64,9 +67,11 @@ The project follows the following structure below the `theories` folder:
 
 
 ## Theorems, definitions, and examples referenced in the paper
+
 We list the relevant theorems and definitions mentioned in the paper by section.
 
 ### Section 2
+
 | Paper | Coq file | Coq name |
 | ------ | ------ | ------ |
 | SimuLang grammar (Figure 2) | `theories/simulang/lang.v` | `expr`, `val`, `prog`, `ectx_item`, `ectx` |
@@ -85,6 +90,7 @@ We list the relevant theorems and definitions mentioned in the paper by section.
 | Rule `while-paco` (2.4) | `theories/simulang/simple_inv/examples/derived.v` | `sim_while` |
 
 ### Section 3
+
 | Paper | Coq file | Coq name |
 | ------ | ------ | ------ |
 | Rule `exploit-store` (Figure 7) | `theories/simulang/na_inv/examples/derived.v` | `sim_exploit_store` |
@@ -97,6 +103,7 @@ We list the relevant theorems and definitions mentioned in the paper by section.
 | Rules in Figure 8| `theories/simulang/na_inv/examples/derived.v` | `sim_load_sc_public`, `sim_load_na_public`, `sim_store_sc_public`, `sim_call` |
 
 ### Section 4
+
 The definition of contextual refinement is language-specific as the contexts are language-specific.
 Similarly, the specific logical relation is specific to the different program logics
 (although we have factored out a common structure and other common components that can be re-used in a language-generic way,
@@ -114,6 +121,7 @@ They are instantiated for the fundamental theorems.
 | Theorem 4.3 (for SimuLang, non-atomic logic) | `theories/simulang/na_inv/adequacy.v` | `log_rel_adequacy` |
 
 ### Section 5
+
 | Paper | Coq file | Coq name |
 | ------ | ------ | ------ |
 | Simulation relation (Figure 11) (full version) | `theories/simulation/slsls.v` | `greatest_def`, `sim_expr_inner` |
@@ -127,6 +135,7 @@ They are instantiated for the fundamental theorems.
 | Theorem 5.2 (for SimuLang, simple logic) | `theories/simulang/simple_inv/adequacy.v` | `log_rel_adequacy` |
 
 ### Section 6
+
 | Paper | Coq file | Coq name |
 | ------ | ------ | ------ |
 | heapbij (simplified) | `theories/simulang/heapbij.v` | `heapbij_interp` |
@@ -138,6 +147,7 @@ They are instantiated for the fundamental theorems.
 | preservation for sim-store-sc (Maintaining the state interpretation) | `theories/simulang/na_inv/na_locs.v` | `na_locs_wf_store` |
 
 ### Section 7
+
 | Paper | Coq file | Coq name |
 | ------ | ------ | ------ |
 | Adequacy (Theorem 5.2 for Stacked Borrows) | `theories/stacked_borrows/adequacy.v` | `log_rel_adequacy` |
@@ -153,5 +163,6 @@ The optimizations ported and extended to concurrency from the original Stacked B
 * `theories/stacked_borrows/examples/opt3_down.v`
 
 ### Section 8
+
 As mentioned in the related work section, we have verified the reorderings and eliminations by [Ševčík, 2011]. They can be found in file `theories/simulang/na_inv/examples/program_transformations_in_weak_memory_models.v`.
 For further information on this, we refer to Section 5 of the technical appendix.

_CoqProject

@@ -4,6 +4,8 @@
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
+# Fixing this one requires Coq 8.19
+-arg -w -arg -argument-scope-delimiter
 
 theories/logic/satisfiable.v
 theories/simulation/language.v
@@ -160,13 +162,13 @@ theories/tree_borrows/logical_state.v
 theories/tree_borrows/inv_accessors.v # needs stuff
 theories/tree_borrows/steps_refl.v # needs tkmap_view
 #theories/tree_borrows/steps_opt.v # needs tkmap_view
-#theories/tree_borrows/primitive_laws.v # needs logical_state
-#theories/tree_borrows/proofmode.v # needs primitive_laws
+theories/tree_borrows/primitive_laws.v # needs logical_state
+theories/tree_borrows/proofmode.v # needs primitive_laws
 
 theories/tree_borrows/wf.v # builds almost as-is
 theories/tree_borrows/parallel_subst.v
-#theories/tree_borrows/log_rel_structural.v # needs proofmode
-#theories/tree_borrows/refl.v # needs proofmode
+theories/tree_borrows/log_rel_structural.v
+theories/tree_borrows/refl.v
 theories/tree_borrows/behavior.v # builds almost as-is
 #theories/tree_borrows/adequacy.v # needs proofmode
 

theories/tree_borrows/bor_semantics.v

@@ -560,6 +560,8 @@ Definition tree_unique tg it tr
   : Prop :=
   every_node (fun it' => IsTag tg it' -> it' = it) tr.
 
+
+(* TODO change to thing below *)
 Definition trees_at_block prop trs blk
   : Prop :=
   match trs !! blk with
@@ -567,6 +569,17 @@ Definition trees_at_block prop trs blk
   | Some tr => prop tr
   end.
 
+Lemma trees_at_block_char prop trs blk :
+  trees_at_block prop trs blk ↔ ∃ tr, trs !! blk = Some tr ∧ prop tr.
+Proof.
+  rewrite /trees_at_block. 
+  destruct (trs !! blk) as [tr|]; split; intros H.
+  - by eexists.
+  - by destruct H as (? & [= ->] & H).
+  - done.
+  - by destruct H as (? & [=] & _).
+Qed.
+
 Definition trees_contain tg trs blk :=
   trees_at_block (tree_contains tg) trs blk.
 

theories/tree_borrows/class_instances.v

@@ -254,8 +254,9 @@ Section safe_reach.
   Global Instance safe_implies_free_val P σ r :
     SafeImplies (∃ l tg T, r = PlaceR l tg T) P (Free r) σ.
   Proof. prove_safe_implies. Qed.
+
   Global Instance safe_implies_free P σ l t (sz:nat) :
-    SafeImplies ((∀ m, is_Some (σ.(shp) !! (l +ₗ m)) ↔ 0 ≤ m < sz) ∧ True) P (Free (Place l t sz)) σ.
+    SafeImplies (∃ trs', (∀ m, is_Some (σ.(shp) !! (l +ₗ m)) ↔ 0 ≤ m < sz) ∧ (sz > 0)%nat ∧ trees_contain t σ.(strs) l.1 ∧ apply_within_trees (memory_deallocate σ.(scs) t (l.2, sz)) l.1 σ.(strs) = Some trs') P (Free (Place l t sz)) σ.
   Proof. prove_safe_implies. Qed.
 
   (* Doesn't build because we don't have typees anymore

theories/tree_borrows/expr_semantics.v

@@ -523,9 +523,10 @@ Inductive mem_expr_step (h: mem) : expr → event → mem → expr → list expr
     (* FIXME: This is wrong because it allows double-free of zero-sized allocations
               Possible solutions:
               - Change the heap from `gmap loc scalar` to `gmap blk (gmap Z scalar)`
-              - Require `sz > 0`      <- probably this
+              - Require `sz > 0`      <- probably this (implementing it)
               - special case for TB where if the size is zero we don't add a new tree
     *)
+    (sz > 0)%nat →
     (∀ m, is_Some (h !! ((blk,l) +ₗ m)) ↔ 0 ≤ m < sz) →
     mem_expr_step
               h (Free (Place (blk,l) lbor sz))

theories/tree_borrows/primitive_laws.v

@@ -3,5 +3,7 @@ From iris.proofmode Require Export proofmode.
 From simuliris.base_logic Require Export gen_sim_heap gen_sim_prog.
 From simuliris.simulation Require Export slsls.
 From simuliris.tree_borrows Require Export class_instances tactics notation
-  defs logical_state steps_refl steps_opt.
+  defs logical_state steps_refl (* steps_opt *).
 From iris.prelude Require Import options.
+
+(** TODO XXX TODO re-add the above import *)

theories/tree_borrows/refl.v

@@ -98,7 +98,7 @@ Section log_rel.
       iPoseProof (rrel_value_source with H) as (? ->) H'
     ];
     try iClear H; try iRename H' into H.
-
+(*
   Lemma log_rel_call e1_t e1_s e2_t e2_s :
     log_rel e1_t e1_s -∗ log_rel e2_t e2_s -∗ log_rel (Call e1_t e2_t) (Call e1_s e2_s).
   Proof.
@@ -136,7 +136,7 @@ Section log_rel.
     iApply (sim_endcall with "Hv").
     sim_finish. sim_val. iModIntro. iSplit; first done. iApply value_rel_poison.
   Qed.
-
+*)
 
   (** a bit of work for eqop *)
   Lemma bor_interp_scalar_eq_source σ_t σ_s sc1_t sc1_s sc2_t sc2_s :
@@ -319,7 +319,7 @@ Section log_rel.
     discr_source. val_discr_source "Hv".
     sim_pures. solve_rrel_refl.
   Qed.
-
+(*
   Lemma log_rel_copy e_t e_s :
     log_rel e_t e_s -∗ log_rel (Copy e_t) (Copy e_s).
   Proof.
@@ -367,7 +367,7 @@ Section log_rel.
     discr_source. val_discr_source "Hv1". val_discr_source "Hv2".
     iApply (sim_retag_public with "[-]"). { by iApply value_rel_ptr. }
     iIntros (t) "Hv". sim_val. eauto.
-  Qed.
+  Qed. *)
 
   (* TODO: this can be useful elsewhere. It's here because I'm relying on the
     several useful tactics defined here. *)
@@ -482,11 +482,11 @@ Section refl.
     - (* Var *)
       by iApply log_rel_var.
     - (* Call *)
-      by iApply (log_rel_call with "IH IH1").
+      admit; by iApply (log_rel_call with "IH IH1").
     - (* InitCall *)
-      by iApply log_rel_initcall.
+      admit; by iApply log_rel_initcall.
     - (* EndCall *)
-      by iApply (log_rel_endcall with "IH").
+      admit; by iApply (log_rel_endcall with "IH").
     - (* Proj *)
       by iApply (log_rel_proj with "IH IH1").
     - (* Conc *)
@@ -498,15 +498,15 @@ Section refl.
     - (* Ref *)
       by iApply (log_rel_ref with "IH").
     - (* Copy *)
-      by iApply (log_rel_copy with "IH").
+      admit; by iApply (log_rel_copy with "IH").
     - (* Write *)
-      by iApply (log_rel_write with "IH IH1").
+      admit; by iApply (log_rel_write with "IH IH1").
     - (* Alloc *)
       by iApply log_rel_alloc.
     - (* Free *)
-      by iApply log_rel_free.
+      admit; by iApply log_rel_free.
     - (* Retag *)
-      by iApply (log_rel_retag with "IH IH1").
+      admit; by iApply (log_rel_retag with "IH IH1").
     - (* Let *)
       by iApply (log_rel_let with "IH IH1").
     - (* Case *)
@@ -515,7 +515,7 @@ Section refl.
       by iApply (log_rel_fork with "IH").
     - (* While *)
       by iApply (log_rel_while with "IH IH1").
-  Qed.
+  Admitted.
 
   Corollary log_rel_refl e :
     expr_wf e →

theories/tree_borrows/steps_progress.v

@@ -183,16 +183,41 @@ Proof.
   rewrite /item_inactive_protector /is_active_protector /is_active.
   case protector; naive_solver.
 Qed.
-
-Lemma dealloc_base_step' P (σ: state) l bor T α (WF: state_wf σ) :
-  (∀ m : Z, is_Some (σ.(shp) !! (l +ₗ m)) ↔ 0 ≤ m ∧ m < tsize T) →
-  memory_deallocated σ.(sst) σ.(scs) l bor (tsize T) = Some α →
-  let σ' := mkState (free_mem l (tsize T) σ.(shp)) α σ.(scs) σ.(snp) σ.(snc) in
-  base_step P (Free (Place l bor T)) σ #[☠] σ' [].
+*)
+(*
+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 →
+  trees_contain tg (strs σ) l.1 →
+  apply_within_trees (memory_deallocate σ.(scs) tg (l.2, sz)) l.1 σ.(strs) = Some α' →
+  let σ' := mkState (free_mem l sz σ.(shp)) (delete l.1 α') σ.(scs) σ.(snp) σ.(snc) in
+  base_step P (Free (Place l tg sz)) σ #[☠] σ' [].
 Proof.
-  intros DOM MD. econstructor; econstructor; eauto.
+  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)

theories/tree_borrows/steps_refl.v

@@ -223,22 +223,27 @@ Proof.
   - iPureIntro. by eapply base_step_wf.
   - iPureIntro. by eapply base_step_wf.
 Qed. 
-(*
-Lemma sim_free_public T_t T_s l_t l_s bor_t bor_s Φ π :
-  rrel (PlaceR l_t bor_t T_t) (PlaceR l_s bor_s T_s) -∗
+
+Lemma sim_free_public sz sz' l_t l_s bor_t bor_s Φ π :
+  rrel (PlaceR l_t bor_t sz') (PlaceR l_s bor_s sz) -∗
   #[☠] ⪯{π} #[☠] [{ Φ }] -∗
-  Free (Place l_t bor_t T_t) ⪯{π} Free (Place l_s bor_s T_s) [{ Φ }].
+  Free (Place l_t bor_t sz') ⪯{π} Free (Place l_s bor_s sz) [{ Φ }].
 Proof.
   iIntros "[#Hscrel ->] Hsim".
   iPoseProof (sc_rel_ptr_source with "Hscrel") as "[%Heq Hpub]". injection Heq as [= -> ->].
   iApply sim_lift_base_step_both. iIntros (P_t P_s σ_t σ_s ??) "[(HP_t & HP_s & Hbor) %Hsafe]".
   iModIntro.
   destruct Hsafe as [Hpool Hsafe].
-  specialize (pool_safe_implies Hsafe Hpool) as (Hdealloc_s & []).
+  specialize (pool_safe_implies Hsafe Hpool) as (trs & Hdealloc_s & Hpos & Hcontain & Hdealloc).
   iPoseProof (bor_interp_get_pure with "Hbor") as "%Hp".
   destruct Hp as (Hsst_eq & Hsnp_eq & Hsnc_eq & Hscs_eq & Hwf_s & Hwf_t & Hdom_eq).
-  iSplitR.
-  { iPureIntro. do 3 eexists. econstructor. eapply dealloc_base_step'; [done | |].
+  iSplitR. (*
+  { iPureIntro. do 3 eexists. eapply dealloc_base_step'; try done.
+    - setoid_rewrite <- elem_of_dom. setoid_rewrite <- elem_of_dom in Hdealloc_s. rewrite -Hdom_eq //.
+    - rewrite - trees_equal_same_tags //.
+    - 
+    - Print memory_deallocate. Search trees_equal trees_contain. Print trees_contain. , trees_at_block. Search is_Some lookup dom. intros m; destruct (Hdealloc_s m) as (H1&H2); split; intros H.
+      + apply H1. destruct H as [x Hx]. exists x. rewrite -Hx. f_equal. exact H.
     - intros m. rewrite -Hdealloc_s. rewrite -!elem_of_dom Hdom_eq. done.
     - instantiate (1 := α'). rewrite -Hsst_eq -Hscs_eq. done.
   }
@@ -323,8 +328,9 @@ Proof.
       intros [-> _]. rewrite Hpub in Ht. congruence.
   - iPureIntro. by eapply base_step_wf.
   - iPureIntro. by eapply base_step_wf.
-Qed.
+Qed. *) Admitted.
 
+(*
 (** TODO: generalize, move, and use it for the opt lemmas too *)
 Lemma sim_copy_public_controlled_update σ l l' (bor : tag) (T : type) (α' : stacks) (t : ptr_id) (tk : tag_kind) sc :
   memory_read σ.(sst) σ.(scs) l bor (tsize T) = Some α' →
@@ -1000,7 +1006,7 @@ Lemma sim_call fn (r_t r_s : result) π Φ :
 Proof.
   iIntros "Hval Hsim". iApply (sim_lift_call _ fn r_t r_s with "[Hval]"); first done. by iApply "Hsim".
 Qed.
-
+*)
 (** Coinduction on while loops *)
 Lemma sim_while_while inv c_t c_s b_t b_s π Ψ :
   inv -∗
@@ -1030,7 +1036,6 @@ Proof.
   simpl. iFrame. iSplitL; last done.
   iApply "Hsim".
 Qed.
-*)
 
 End lifting.