ctx-dependent effects

.github/workflows/build.yml

@@ -4,12 +4,22 @@ name: Docker CI
 on: [push, pull_request]
 
 jobs:
+  build_nix:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+    - uses: cachix/install-nix-action@v24
+      with:
+        github_access_token: ${{ secrets.GITHUB_TOKEN }}
+    - run: nix build .#coq-artifact
+
   build:
     runs-on: ubuntu-latest
     strategy:
       matrix:
         image:
           - 'coqorg/coq:8.17'
+          - 'coqorg/coq:8.18'
       max-parallel: 4
       fail-fast: false
 
@@ -21,7 +31,6 @@ jobs:
           install: |
             startGroup "Install dependencies"
               sudo apt-get update -y -q
-              opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
               opam pin add -n -y -k path $PACKAGE $WORKDIR
               opam update -y
               opam install --confirm-level=unsafe-yes -j 2 $PACKAGE --deps-only

README.md

@@ -1,15 +1,15 @@
 # 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:
 
 ```
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
 opam update
 opam install . --deps-only
 ```
@@ -25,14 +25,24 @@ 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
-- `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`
+- `lib/` -- derived combinators for gitrees
+- `effects/` -- concrete effects, their semantics, and program logic rules
+- `examples/input_lang/` -- formalization of the language with io, the soundness and adequacy
+- `examples/affine_lang/` -- formalization of the affine language, type safety of the language interoperability
+- `examples/input_lang_callcc/` -- formalization of the language with io, throw and call/cc, the soundness and adequacy
+- `examples/delim_lang/` -- formalization shift/reset effects, of a language with delimited continuations and its soundness
 - `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`
+
+For the representation of binders we use a library implemented by
+Filip Sieczkowski and Piotr Polesiuk, located in the `vendor/Binding/`
+folder.
 
 ### 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`
@@ -42,7 +52,7 @@ to the code structure.
   + The factorial example is in `examples/factorial.v`, and
     the pairs example is in `examples/pairs.v`
 - **Section 4**
-  + The definition of reifiers and the reify function are in `gitree/reify.v`
+  + The definition of context-dependent versions of reifiers and the reify function are in `gitree/reify.v`
   + The reduction relation is in `gitree/reductions.v`
   + The specific reifiers for IO and state are in `examples/store.v`
     and `input_lang/interp.v`
@@ -70,12 +80,6 @@ to the code structure.
 
 ## Notes
 
-### Representations of binders
-For the representation of languages with binders, we follow the
-approach of (Benton, Hur, Kennedy, McBride, JAR 2012) with well-scoped
-terms and substitutions/renamings. 
-
-
 ### Disjunction property
 Some results in the formalization make use of the disjunction property
 of Iris: if (P ∨ Q) is provable, then either P or Q are provable on

_CoqProject

@@ -1,6 +1,19 @@
 -Q theories gitrees
+-Q vendor/Binding Binding
 -arg -w -arg -ssr-search-moved
 
+vendor/Binding/Properties.v
+vendor/Binding/Lib.v
+vendor/Binding/Set.v
+vendor/Binding/Auto.v
+vendor/Binding/Core.v
+vendor/Binding/Inc.v
+vendor/Binding/Intrinsic.v
+vendor/Binding/TermSimpl.v
+vendor/Binding/Product.v
+vendor/Binding/Env.v
+vendor/Binding/Resolver.v
+
 theories/prelude.v
 theories/lang_generic.v
 
@@ -15,18 +28,30 @@ theories/gitree.v
 
 theories/program_logic.v
 
-theories/input_lang/lang.v
-theories/input_lang/interp.v
-theories/input_lang/logpred.v
-theories/input_lang/logrel.v
+theories/effects/store.v
+theories/effects/io_tape.v
+
+theories/lib/pairs.v
+theories/lib/while.v
+theories/lib/factorial.v
+theories/lib/iter.v
+
+theories/examples/delim_lang/lang.v
+theories/examples/delim_lang/interp.v
+theories/examples/delim_lang/example.v
+
+theories/examples/input_lang_callcc/lang.v
+theories/examples/input_lang_callcc/interp.v
+theories/examples/input_lang_callcc/hom.v
+theories/examples/input_lang_callcc/logrel.v
 
-theories/affine_lang/lang.v
-theories/affine_lang/logrel1.v
-theories/affine_lang/logrel2.v
+theories/examples/input_lang/lang.v
+theories/examples/input_lang/interp.v
+theories/examples/input_lang/logpred.v
+theories/examples/input_lang/logrel.v
 
-theories/examples/store.v
-theories/examples/pairs.v
-theories/examples/while.v
-theories/examples/factorial.v
-theories/examples/iter.v
+theories/examples/affine_lang/lang.v
+theories/examples/affine_lang/logrel1.v
+theories/examples/affine_lang/logrel2.v
 
+theories/utils/finite_sets.v

check_admits.sh

@@ -0,0 +1,3 @@
+#! /bin/sh
+
+grep -n -e 'admit' -e 'Admitted' $(find . -name '*.v' -type f)

coq-gitrees.opam

@@ -2,16 +2,15 @@ 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" { (= "dev.2023-09-29.0.4f3a385f") }
-  "coq-iris-heap-lang" { (= "dev.2023-09-29.0.4f3a385f") }
-  "coq-stdpp" { (= "dev.2023-09-21.2.7f6df4fa") }
+  "coq-iris" { (= "4.1.0") }
+  "coq-iris-heap-lang" { (= "4.1.0") }
+  "coq-stdpp" { (= "1.9.0") }
   "coq" { (>= "8.17") | (= "dev") }
 ]

flake.nix

@@ -0,0 +1,35 @@
+{
+  description = "gitrees";
+  inputs = {
+    nixpkgs.url = github:NixOS/nixpkgs/nixos-23.11;
+    flake-utils.url = github:numtide/flake-utils;
+  };
+  outputs = { self, nixpkgs, flake-utils }:
+    with flake-utils.lib; eachSystem allSystems (system:
+      let
+        pkgs = nixpkgs.legacyPackages.${system};
+        lib = pkgs.lib;
+        coq = pkgs.coq_8_17;
+        coqPkgs = pkgs.coqPackages_8_17;
+      in {
+        packages = {
+          coq-artifact = coqPkgs.mkCoqDerivation {
+            pname = "coq-artifact";
+            version = "main";
+            src = ./.;
+            buildPhase = "make";
+            propagatedBuildInputs = [
+              coqPkgs.stdpp
+              coqPkgs.iris
+              coqPkgs.equations
+            ];
+          };
+        };
+        devShell = pkgs.mkShell {
+          buildInputs = with pkgs; [
+            coq
+          ];
+          inputsFrom = [ self.packages.${system}.coq-artifact ];
+        };
+      });
+}