cleanup the branch and make is_ctx_dep implicit

README.md

@@ -1,10 +1,11 @@
 # Guarded Interaction Trees
 
 This is the Coq formalization of guarded interaction trees, associated examples and case studies.
+Read the [GITrees POPL paper](https://iris-project.org/pdfs/2024-popl-gitrees.pdf) describing our work.
 
 ## Installation instructions
 
-To install the formalization you will need the Iris, std++, and Equations packages.
+To install the formalization you will need Iris and std++ libraries.
 The dependencies can be easily installed using [Opam](https://opam.ocaml.org/) with the following commands:
 
 ```
@@ -24,16 +25,20 @@ All the code lives in the `theories` folder. Below is the quick guide
 to the code structure.
 
 - `gitree/` -- contains the core definitions related to guarded interaction trees
-- `input_lang/` -- formalization of the language with io, the soundness and adequacy
-- `input_lang_callcc/` -- formalization of the language with io, throw and call/cc, the soundness and adequacy
-- `affine_lang/` -- formalization of the affine language, type safety of the language interoperability
-- `examples/` -- some other smaller examples
-- `lang_generic.v` -- generic facts about languages with binders and their interpretations, shared by `input_lang` and `affine_lang`
-- `lang_generic_sem.v` -- generic facts about languages with a different representation of binders and their interpretations, used for `input_lang_callcc`
+- `lib/` -- derived combinators for gitrees
+- `examples/input_lang/` -- formalization of the language with io, the soundness and adequacy
+- `examples/input_lang_callcc/` -- formalization of the language with io, throw and call/cc, the soundness and adequacy
+- `examples/affine_lang/` -- formalization of the affine language, type safety of the language interoperability
+- `effects/` -- concrete effects, their interpretaions, and logics
 - `prelude.v` -- some stuff that is missing from Iris
+- `lang_generic.v` -- generic facts about languages with binders and their interpretations, shared by `input_lang` and `affine_lang`
+- `vendor/Binding/` -- the functorial syntax library used for
 
 ### References from the paper to the code
 
+The version of the formalization that corresponds to the paper can be found under the [tag `popl24`](https://github.com/logsem/gitrees/releases/tag/popl24).
+Below we describe the correspondence per-section.
+
 - **Section 3**
   + Definition of guarded interaction trees, constructors, the
     recursion principle, and the destructors are in `gitree/core.v`

_CoqProject

@@ -31,6 +31,7 @@ theories/program_logic.v
 
 theories/examples/input_lang_delim/lang.v
 theories/examples/input_lang_delim/interp.v
+theories/examples/input_lang_delim/example.v
 
 theories/examples/input_lang_callcc/lang.v
 theories/examples/input_lang_callcc/interp.v
@@ -53,4 +54,4 @@ theories/lib/while.v
 theories/lib/factorial.v
 theories/lib/iter.v
 
-theories/utils/finite_sets.v
+theories/utils/finite_sets.v

coq-gitrees.opam

@@ -2,14 +2,13 @@ opam-version: "2.0"
 name: "coq-gitrees"
 synopsis: "Guarded Interaction Trees"
 version: "dev"
-maintainer: "..."
-authors: "..."
+maintainer: "Logsem"
+authors: "Logsem"
 license: "BSD"
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/gitrees"]
 depends: [
-  "coq-equations" { (= "1.3+8.17") }
   "coq-iris" { (= "4.1.0") }
   "coq-iris-heap-lang" { (= "4.1.0") }
   "coq-stdpp" { (= "1.9.0") }

theories/effects/store.v

@@ -224,10 +224,7 @@ Section wp.
   Proof.
     iIntros (Hee) "#Hcxt H".
     unfold READ. simpl.
-    match goal with
-    | |- context G [Vis ?a ?b ?c] => assert (c ≡ idfun ◎ (subEff_outs ^-1)) as ->
-    end; first solve_proper.
-    iApply wp_subreify_ctx_indep'.
+    iApply wp_subreify_ctx_indep'. simpl.
     iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl".
     iApply (fupd_mask_weaken E1).
     { set_solver. }
@@ -249,16 +246,9 @@ Section wp.
     iFrame "Hs".
     repeat iSplit.
     - assert ((option_bind _ _ (λ x, Some (x, σ)) (σ !! l)) ≡
-                 (option_bind _ _ (λ x, Some (x, σ)) (Some (Next β')))) as H.
-      + f_equiv.
-        * solve_proper.
-        * by rewrite Hx Hb'.
-      + simpl in H.
-        rewrite <-H.
-        unfold mbind.
-        simpl.
-        iPureIntro.
-        f_equiv; last done.
+                (option_bind _ _ (λ x, Some (x, σ)) (Some (Next β')))) as <-.
+      { rewrite Hx /= ; solve_proper. }
+      simpl. iPureIntro. by f_equiv.
     - iPureIntro. apply ofe_iso_21.
     - iNext. iIntros "Hlc Hs".
       iMod ("Hback" with "Hp") as "Hback".
@@ -290,8 +280,7 @@ Section wp.
     WP@{rs} WRITE l β @ s {{ Φ }}.
   Proof.
     iIntros (Hee) "#Hcxt H".
-    unfold READ. simpl.
-    iApply wp_subreify_ctx_indep'.
+    iApply wp_subreify_ctx_indep'. simpl.
     iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl".
     iApply (fupd_mask_weaken E1).
     { set_solver. }
@@ -337,7 +326,7 @@ Section wp.
     WP@{rs} ALLOC α k @ s {{ Φ }}.
   Proof.
     iIntros "Hh H".
-    iApply wp_subreify_ctx_indep'.
+    iApply wp_subreify_ctx_indep'. simpl.
     iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl".
     iApply (lc_fupd_elim_later with "Hlc").
     iModIntro.
@@ -365,8 +354,7 @@ Section wp.
     WP@{rs} DEALLOC l @ s {{ Φ }}.
   Proof.
     iIntros (Hee) "#Hcxt H".
-    unfold DEALLOC. simpl.
-    iApply wp_subreify_ctx_indep'.
+    iApply wp_subreify_ctx_indep'. simpl.
     iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl".
     iApply (fupd_mask_weaken E1).
     { set_solver. }
@@ -404,105 +392,6 @@ Section wp.
     iModIntro. done.
   Qed.
 
-  (** * The logical relation TODO *)
-  (* Definition N := nroot.@"heh". *)
-  (* Definition logrel_expr V (α : IT) : iProp := *)
-  (*   (heap_ctx -∗ WP@{rs} α {{ V }})%I. *)
-
-  (* Context `{!SubOfe natO R, !Inhabited R}. *)
-
-  (* Definition logrel_nat (βv : ITV) : iProp := *)
-  (*   (∃ n : nat, βv ≡ RetV n)%I. *)
-  (* Definition logrel_arr V1 V2 (βv : ITV) : iProp := *)
-  (*   (∃ f, IT_of_V βv ≡ Fun f ∧ □ ∀ αv, V1 αv -∗ *)
-  (*      logrel_expr V2 (APP' (Fun f) (IT_of_V αv)))%I. *)
-  (* Definition logrel_ref V (l : loc) : iProp := *)
-  (*   (inv (N.@l) (∃ βv, pointsto l (IT_of_V βv) ∗ V βv))%I. *)
-
-  (* Lemma logrel_alloc V V2 (αv :ITV) (k : locO -n> IT) `{!forall v, Persistent (V v)} *)
-  (*   `{NonExpansive V2} : *)
-  (*   V αv -∗ *)
-  (*   (∀ l, logrel_ref V l -∗ logrel_expr V2 (k l)) -∗ *)
-  (*   logrel_expr V2 (ALLOC (IT_of_V αv) k). *)
-  (* Proof. *)
-  (*   iIntros "#HV H". *)
-  (*   iIntros "#Hh". *)
-  (*   iApply (wp_alloc with "Hh"). *)
-  (*   iNext. iNext. *)
-  (*   iIntros (l) "Hl". *)
-  (*   iMod (inv_alloc (N.@l) _ (∃ βv, pointsto l (IT_of_V βv) ∗ V βv)%I with "[Hl]") *)
-  (*     as "#Hinv". *)
-  (*   { eauto with iFrame. } *)
-  (*   iSpecialize ("H" with "Hinv"). *)
-  (*   by iApply "H". *)
-  (* Qed. *)
-
-  (* Opaque Ret. (*TODO*) *)
-  (* Lemma logrel_write V αv l `{!forall v, Persistent (V v)} : *)
-  (*   logrel_ref V l -∗ *)
-  (*   V αv -∗ *)
-  (*   logrel_expr logrel_nat (WRITE l (IT_of_V  αv)). *)
-  (* Proof. *)
-  (*   iIntros "#Hl #Hav #Hctx". *)
-  (*   iApply wp_subreify'. *)
-  (*   iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl1". *)
-  (*   iInv (N.@l) as "HH" "Hcl2". *)
-  (*   iDestruct "HH" as (βv) "[Hbv #HV]". *)
-  (*   iApply (lc_fupd_elim_later with "Hlc"). *)
-  (*   iNext. *)
-  (*   iAssert (⌜is_Some (σ !! l)⌝)%I as "%Hdom". *)
-  (*   { iApply (istate_loc_dom with "Hh Hbv"). } *)
-  (*   iExists σ, (),(<[l:=Next (IT_of_V αv)]>σ),(Ret ()). *)
-  (*   iFrame "Hs". *)
-  (*   iSimpl. repeat iSplit; [ done | done | ]. *)
-  (*   iNext. iIntros "Hlc Hs". *)
-  (*   iMod (istate_write _ _ (IT_of_V αv) with "Hh Hbv") as "[Hh Hlav]". *)
-  (*   iMod ("Hcl2" with "[Hlav]") as "_". *)
-  (*   { iNext. iExists _; by iFrame. } *)
-  (*   iMod ("Hcl1" with "[Hlc Hh Hs]") as "_". *)
-  (*   { iNext. iExists _; by iFrame. } *)
-  (*   iModIntro. *)
-  (*   iApply wp_val. iModIntro. *)
-  (*   iExists (). unfold RetV. done. *)
-  (* Qed. *)
-
-  (* Lemma logrel_read V l `{!forall v, Persistent (V v)} : *)
-  (*   logrel_ref V l -∗ *)
-  (*   logrel_expr V (READ l). *)
-  (* Proof. *)
-  (*   iIntros "#Hr #Hctx". *)
-  (*   iApply wp_subreify'. *)
-  (*   iInv (nroot.@"storeE") as (σ) "[>Hlc [Hs Hh]]" "Hcl1". *)
-  (*   iInv (N.@l) as "HH" "Hcl2". *)
-  (*   iDestruct "HH" as (βv) "[Hbv #HV]". *)
-  (*   iAssert (▷ (σ !! l ≡ Some (Next (IT_of_V βv))))%I as "#Hlookup". *)
-  (*   { iNext. iApply (istate_read with "Hh Hbv"). } *)
-  (*   iAssert (▷ ⌜is_Some (σ !! l)⌝)%I as "#Hdom". *)
-  (*   { iNext. iApply (istate_loc_dom with "Hh Hbv"). } *)
-  (*   iDestruct "Hdom" as ">%Hdom". *)
-  (*   destruct Hdom as [x Hx]. *)
-  (*   destruct (Next_uninj x) as [β' Hb']. *)
-  (*   iAssert (▷ ▷ (β' ≡ IT_of_V βv))%I as "#Hbv'". *)
-  (*   { iNext. rewrite Hx. rewrite option_equivI. *)
-  (*     rewrite Hb'. by iNext. } *)
-  (*   iClear "Hlookup". *)
-  (*   iApply (lc_fupd_elim_later with "Hlc"). *)
-  (*   iNext. iSimpl. *)
-  (*   iExists σ,(Next β'),σ,β'. iFrame "Hs". *)
-  (*   repeat iSplit. *)
-  (*   { iPureIntro. rewrite Hx/= Hb'. done. } *)
-  (*   { rewrite ofe_iso_21//. } *)
-  (*   iNext. iIntros "Hlc Hs". *)
-  (*   iMod ("Hcl2" with "[Hbv]") as "_". *)
-  (*   { iNext. eauto with iFrame. } *)
-  (*   iMod ("Hcl1" with "[Hlc Hh Hs]") as "_". *)
-  (*   { iNext. eauto with iFrame. } *)
-  (*   iModIntro. *)
-  (*   iRewrite "Hbv'". *)
-  (*   iApply wp_val. *)
-  (*   iModIntro. done. *)
-  (* Qed. *)
-
 End wp.
 
 Arguments heapG {_} rs R {_} Σ.

theories/examples/affine_lang/lang.v

@@ -3,6 +3,8 @@ From gitrees.examples.input_lang Require Import lang interp.
 From gitrees.effects Require Import store.
 From gitrees.lib Require Import pairs.
 
+Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env.
+
 (* for namespace sake *)
 Module io_lang.
   Definition state := input_lang.lang.state.
@@ -14,8 +16,6 @@ Module io_lang.
     input_lang.interp.interp_expr rs e ı_scope.
 End io_lang.
 
-Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env.
-
 Inductive ty :=
   tBool | tInt | tUnit
 | tArr (τ1 τ2 : ty) | tPair (τ1 τ2 : ty)
@@ -42,7 +42,7 @@ Inductive expr : ∀ (S : Set), Type :=
 | Alloc {S : Set} : expr S → expr S
 | Replace {S1 S2 : Set} : expr S1 → expr S2 → expr (sum S1 S2)
 | Dealloc {S : Set} : expr S → expr S
-| EEmbed {S : Set} {τ1 τ1'} : io_lang.expr Empty_set → ty_conv τ1 τ1' → expr S
+| EEmbed {S : Set} {τ1 τ1'} : io_lang.expr ∅ → ty_conv τ1 τ1' → expr S
 .
 
 Section affine.

theories/examples/affine_lang/logrel1.v

@@ -1,11 +1,11 @@
 (** Unary (Kripke) logical relation for the affine lang *)
-Require Import iris.algebra.gmap.
 From gitrees Require Export gitree program_logic greifiers.
 From gitrees.examples.affine_lang Require Import lang.
 From gitrees.effects Require Import store.
 From gitrees.lib Require Import pairs.
 From gitrees.utils Require Import finite_sets.
 
+
 Inductive typed : forall {S : Set}, (S → ty) → expr S → ty → Prop :=
 (** functions *)
 | typed_Var {S : Set} (Ω : S → ty) (v : S)  :
@@ -525,15 +525,15 @@ Lemma logrel1_adequacy cr Σ R `{!Cofe R, !SubOfe natO R, !SubOfe unitO R, !SubO
   (α : interp_scope ∅ -n>  IT (gReifiers_ops rs) R) (β : IT (gReifiers_ops rs) R) st st' k :
   (∀ `{H1 : !invGS Σ} `{H2: !stateG rs R Σ} `{H3: !heapG rs R Σ},
       (£ cr ⊢ valid1 rs notStuck (λne _: unitO, True)%I □ α τ)%I) →
-  ssteps (gReifiers_sReifier NotCtxDep rs) (α ı_scope) st β st' k →
-  (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1)
+  ssteps (gReifiers_sReifier rs) (α ı_scope) st β st' k →
+  (∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1)
    ∨ (∃ βv, (IT_of_V βv ≡ β)%stdpp).
 Proof.
   intros Hlog Hst.
   destruct (IT_to_V β) as [βv|] eqn:Hb.
   { right. exists βv. apply IT_of_to_V'. rewrite Hb; eauto. }
   left.
-  cut ((∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1)
+  cut ((∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1)
       ∨ (∃ e, (β ≡ Err e)%stdpp ∧ notStuck e)).
   { intros [?|He]; first done.
     destruct He as [? [? []]]. }
@@ -549,9 +549,9 @@ Proof.
   iMod (new_heapG rs σ) as (H3) "H".
   iAssert (has_substate σ ∗ has_substate ios)%I with "[Hst]" as "[Hs Hio]".
   { unfold has_substate, has_full_state.
-    assert (of_state NotCtxDep rs (IT (gReifiers_ops rs) _) st ≡
-            of_idx NotCtxDep rs (IT (gReifiers_ops rs) _) sR_idx (sR_state σ)
-            ⋅ of_idx NotCtxDep rs (IT (gReifiers_ops rs) _) sR_idx (sR_state ios))%stdpp as ->; last first.
+    assert (of_state rs (IT (gReifiers_ops rs) _) st ≡
+            of_idx rs (IT (gReifiers_ops rs) _) sR_idx (sR_state σ)
+            ⋅ of_idx rs (IT (gReifiers_ops rs) _) sR_idx (sR_state ios))%stdpp as ->; last first.
     { rewrite -own_op. done. }
     unfold sR_idx. simpl.
     intro j.
@@ -580,8 +580,8 @@ Definition R := sumO locO (sumO unitO natO).
 
 Lemma logrel1_safety e τ (β : IT (gReifiers_ops rs) R) st st' k :
   typed □ e τ →
-  ssteps (gReifiers_sReifier NotCtxDep rs) (interp_expr rs e ı_scope) st β st' k →
-  (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1)
+  ssteps (gReifiers_sReifier rs) (interp_expr rs e ı_scope) st β st' k →
+  (∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1)
    ∨ (∃ βv, (IT_of_V βv ≡ β)%stdpp).
 Proof.
   intros Hty Hst.

theories/examples/affine_lang/logrel2.v

@@ -1,6 +1,4 @@
-From stdpp Require Import finite.
 From iris.base_logic.lib Require Import na_invariants.
-From iris.algebra Require Import gmap.
 From gitrees Require Export gitree program_logic greifiers.
 From gitrees.examples.input_lang Require Import lang interp logpred.
 From gitrees.examples.affine_lang Require Import lang logrel1.
@@ -478,15 +476,15 @@ Lemma logrel2_adequacy (cr : nat) R `{!Cofe R, !SubOfe locO R, !SubOfe natO R, !
   (τ : ty) (α : interp_scope Empty_set -n> IT (gReifiers_ops rs) R) (β : IT (gReifiers_ops rs) R) st st' k :
   (∀ `{H1 : !invGS Σ} `{H2: !stateG rs R Σ} `{H3: !heapG rs R Σ} p,
       (£ cr ⊢ valid2 rs p □ α τ)%I) →
-  ssteps (gReifiers_sReifier NotCtxDep rs) (α ı_scope) st β st' k →
-  (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1)
+  ssteps (gReifiers_sReifier rs) (α ı_scope) st β st' k →
+  (∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1)
    ∨ (β ≡ Err OtherError)%stdpp
    ∨ (∃ βv, (IT_of_V βv ≡ β)%stdpp).
 Proof.
   intros Hlog Hst.
   destruct (IT_to_V β) as [βv|] eqn:Hb.
   { right. right. exists βv. apply IT_of_to_V'. rewrite Hb; eauto. }
-  cut ((∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1)
+  cut ((∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1)
       ∨ (∃ e, (β ≡ Err e)%stdpp ∧ s e)).
   { intros [?|He]; first eauto. right. left.
     destruct He as [? [? ->]]. done. }
@@ -502,9 +500,9 @@ Proof.
   iMod (new_heapG rs σ) as (H3) "H".
   iAssert (has_substate σ ∗ has_substate ios)%I with "[Hst]" as "[Hs Hio]".
   { unfold has_substate, has_full_state.
-    assert (of_state NotCtxDep rs (IT (gReifiers_ops rs) _) st ≡
-            of_idx NotCtxDep rs (IT (gReifiers_ops rs) _) sR_idx (sR_state σ)
-            ⋅ of_idx NotCtxDep rs (IT (gReifiers_ops rs) _) sR_idx (sR_state ios))%stdpp as ->; last first.
+    assert (of_state rs (IT (gReifiers_ops rs) _) st ≡
+            of_idx rs (IT (gReifiers_ops rs) _) sR_idx (sR_state σ)
+            ⋅ of_idx rs (IT (gReifiers_ops rs) _) sR_idx (sR_state ios))%stdpp as ->; last first.
     { rewrite -own_op. done. }
     unfold sR_idx. simpl.
     intro j.
@@ -535,8 +533,8 @@ Definition R := sumO locO (sumO natO unitO).
 
 Lemma logrel2_safety e τ (β : IT (gReifiers_ops rs) R) st st' k :
   typed_glued □ e τ →
-  ssteps (gReifiers_sReifier NotCtxDep rs) (interp_expr rs e ı_scope) st β st' k →
-  (∃ β1 st1, sstep (gReifiers_sReifier NotCtxDep rs) β st' β1 st1)
+  ssteps (gReifiers_sReifier rs) (interp_expr rs e ı_scope) st β st' k →
+  (∃ β1 st1, sstep (gReifiers_sReifier rs) β st' β1 st1)
    ∨ (β ≡ Err OtherError)%stdpp
    ∨ (∃ βv, (IT_of_V βv ≡ β)%stdpp).
 Proof.