logsem · fresheed · Jun 3, 2025 · Jun 10, 2025 · Jun 13, 2025 · Jun 13, 2025
diff --git a/.gitmodules b/.gitmodules
@@ -1,9 +0,0 @@
-[submodule "external/stdpp"]
-	path = external/stdpp
-	url = https://gitlab.mpi-sws.org/iris/stdpp.git
-[submodule "external/iris"]
-	path = external/iris
-	url = https://gitlab.mpi-sws.org/iris/iris.git
-[submodule "external/paco"]
-	path = external/paco
-	url = https://github.com/snu-sf/paco.git

diff --git a/Makefile b/Makefile
@@ -1,10 +1,10 @@
 TRILLIUM_DIR := 'trillium'
+HL_DIR := 'heap_lang'
+FAIRNESS_DIR := 'fairness'
 FAIRIS_DIR := 'fairis'
-LOCAL_SRC_DIRS := $(TRILLIUM_DIR) $(FAIRIS_DIR)
-SRC_DIRS := $(LOCAL_SRC_DIRS) 'external'
+SRC_DIRS := $(TRILLIUM_DIR) $(FAIRNESS_DIR) $(HL_DIR) $(FAIRIS_DIR)
 
-ALL_VFILES := $(shell find $(SRC_DIRS) -name "*.v")
-VFILES := $(shell find $(LOCAL_SRC_DIRS) -name "*.v")
+VFILES := $(shell find $(SRC_DIRS) -name "*.v")
 
 COQC := coqc
 Q:=@
@@ -14,9 +14,9 @@ COQPROJECT_ARGS := $(shell sed -E -e '/^\#/d' -e 's/-arg ([^ ]*)/\1/g' _CoqProje
 
 all: $(VFILES:.v=.vo)
 
-.coqdeps.d: $(ALL_VFILES) _CoqProject
+.coqdeps.d: $(VFILES) _CoqProject
 	@echo "COQDEP $@"
-	$(Q)coqdep -vos -f _CoqProject $(ALL_VFILES) > $@
+	$(Q)coqdep -vos -f _CoqProject $(VFILES) > $@
 
 # do not try to build dependencies if cleaning or just building _CoqProject
 ifeq ($(filter clean,$(MAKECMDGOALS)),)
@@ -43,26 +43,33 @@ clean:
 	rm -f .coqdeps.d
 
 # project-specific targets
-.PHONY: build clean-trillium clean-fairis trillium fairis
+.PHONY: build clean-trillium trillium clean-fairness fairness clean-heap-lang heap-lang clean-fairis fairis
 
-VPATH= $(TRILLIUM_DIR) $(FAIRIS_DIR)
+VPATH= $(TRILLIUM_DIR) $(FAIRNESS_DIR) $(HL_DIR) $(FAIRIS_DIR)
 VPATH_FILES := $(shell find $(VPATH) -name "*.v")
 
 build: $(VPATH_FILES:.v=.vo)
 
-fairis :
-	@$(MAKE) build VPATH=$(FAIRIS_DIR)
-
 trillium :
 	@$(MAKE) build VPATH=$(TRILLIUM_DIR)
 
-clean-local:
-	@echo "CLEAN vo glob aux"
-	$(Q)find $(LOCAL_SRC_DIRS) \( -name "*.vo" -o -name "*.vo[sk]" \
-		-o -name ".*.aux" -o -name ".*.cache" -o -name "*.glob" \) -delete
+fairness :
+	@$(MAKE) build VPATH=$(FAIRNESS_DIR)
+
+heap-lang :
+	@$(MAKE) build VPATH=$(HL_DIR)
+
+fairis :
+	@$(MAKE) build VPATH=$(FAIRIS_DIR)
 
 clean-trillium:
-	@$(MAKE) clean-local LOCAL_SRC_DIRS=$(TRILLIUM_DIR)
+	@$(MAKE) clean SRC_DIRS=$(TRILLIUM_DIR)
+
+clean-fairness:
+	@$(MAKE) clean SRC_DIRS=$(FAIRNESS_DIR)
+
+clean-heap-lang:
+	@$(MAKE) clean SRC_DIRS=$(HL_DIR)
 
 clean-fairis:
-	@$(MAKE) clean-local LOCAL_SRC_DIRS=$(FAIRIS_DIR)
+	@$(MAKE) clean SRC_DIRS=$(FAIRIS_DIR)
diff --git a/README.md b/README.md
@@ -3,65 +3,69 @@
 Trillium is a higher-order concurrent separation logic for proving trace
 refinements between programs and models. The logic is
 built using the [Iris](https://iris-project.org) program logic framework and
-mechanized in the [Coq proof assistant](https://coq.inria.fr/).
+mechanized in the [Rocq proof assistant](https://rocq-prover.org/).
 
 ## Directory Structure
 
 - [`trillium/`](trillium/): The Trillium program logic framework
 
-- [`fairis/`](fairis/): The Fairis instantiation of Trillium for reasoning
-  about fair termination of concurrent programs.
-  + [`heap_lang/`](fairis/heap_lang/): HeapLang instantiation with fuel model
-    * [`examples/`](fairis/heap_lang/examples/): Examples and case studies
+- [`heap_lang/`](heap_lang/) - a variation of HeapLang language (most notably - enriched with locales)
 
-- [`external/`](external/): External dependencies
+- [`fairness/`](fairness/) - a number of various trace and model utilities; most notably - a uniform definition of trace and model fairness.
 
-## Compiling
-
-The project maintains compatibility with Coq 8.17 and relies on `coqc` being
-available in your shell. Clone the external git submodule dependencies using
-
-    git submodule update --init --recursive
-
-Alternatively, clone the repository using the `--recurse-submodules` flag.
-
-Run `make -jN` to build the full development, where `N` is the number of your
-CPU cores.
-
-Note that the compilation of the external dependencies is known to print
-a lot of warning messages when compiled with Coq 8.17.
+- [`fairis/`](fairis/) - The Fairis program logic - an instantiation of Trillium for reasoning about fair termination of HeapLang programs.
 
-## Git submodule dependencies
 
-This project uses git submodules to manage dependencies with other Coq
-libraries. By default, when working with a repository that uses submodules, the
-submodules will *not* be populated and updated automatically, and it is often
-necessary to invoke `git submodule update --init --recursive` or use the
-`--recurse-submodules` flag. However, this can be automated by setting the
-`submodule.recurse` setting to `true` in your git config by running
-
-    git config --global submodule.recurse true
-
-This will make `git clone`, `git checkout`, `git pull`, etc. work as you would
-expect and it should rarely be necessary to invoke any `git submodule update`
-commands.
-
-A git submodule is pinned to a particular commit of an external (remote)
-repository. If new commits have been pushed to the remote repository and you
-wish to integrate these in to the development, invoke
-
-    git submodule update --remote
-
-to fetch the new commits and apply them to your local repository. This changes
-which commit your *local* submodule is pinned to. Remember to commit and push
-the submodule update to make it visible to other users of the repository.
+## Compiling
 
-Read more about git submodules in [this
-tutorial](https://git-scm.com/book/en/v2/Git-Tools-Submodules).
+    # create a new opam environment
+    opam switch create trillium_env 5.2.0
+    # switch into the new environment
+    eval $(opam env --switch=trillium_env)
+
+    # set up repository for Rocq packages
+    opam repo add rocq-released https://rocq-prover.github.io/opam/released/
+
+    # install all dependencies of Trillium
+    opam install . --deps-only
+    # build Trillium; adjust the number of jobs as needed
+    make -j 5
+
+## Using Trillium in your project
+
+The instruction below applies until Trillium is released as a publicly available opam package.
+
+Your project should be set up as an opam package. 
+With that, add the Trillium dependency to its `.opam` file:
+
+    depends: [
+      # ...
+      "trillium" { (= "2.2.0") }
+    ]
+
+Then, clone the Trillium repo at some local path TRILLIUM_PATH.
+After that, execute the following in the root of your project:
+
+    # create a new opam environment for your project
+    opam switch create project-env 5.2.0
+    # switch into the new environment
+    eval $(opam env --switch=project-env)
+
+    # set up repository for Rocq packages
+    opam repo add rocq-released https://rocq-prover.github.io/opam/released/
+    # set up the local repository for Trillium
+    opam pin add trillium TRILLIUM_PATH --no-action
+
+    # install all dependencies of your project; Trillium will be installed as a part of it
+    opam install . --deps-only
+    # build your project
+    make -j 5	
+
 
 ## Publications
 
-A [preprint](https://iris-project.org/pdfs/2021-submitted-trillium.pdf) is
-available describing Trillium, a program logic framework for both proving
-partial correctness properties and trace properties; Aneris is now an
-instantiation of the Trillium framework.
+- Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement.
+
+  Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, Lars Birkedal.
+
+  In POPL 2024: ACM SIGPLAN Symposium on Principles of Programming Languages
diff --git a/_CoqProject b/_CoqProject
@@ -1,13 +1,7 @@
 -Q trillium trillium
--Q fairis trillium.fairness
-
--Q external/stdpp/stdpp stdpp
--Q external/stdpp/stdpp_unstable stdpp.unstable
--Q external/iris/iris iris
--Q external/iris/iris_deprecated iris.deprecated
--Q external/iris/iris_unstable iris.unstable
--Q external/iris/iris_heap_lang iris.heap_lang
--Q external/paco/src Paco
+-Q heap_lang heap_lang
+-Q fairness fairness
+-Q fairis fairis
 
 -arg -w -arg -notation-overridden
 -arg -w -arg -redundant-canonical-projection

diff --git a/external/iris b/external/iris
diff --git a/external/paco b/external/paco
diff --git a/external/stdpp b/external/stdpp
diff --git a/fairis/heap_lang/adequacy.v → fairis/adequacy.v b/fairis/heap_lang/adequacy.v → fairis/adequacy.v
@@ -4,94 +4,15 @@ From iris.algebra Require Import auth gmap gset excl.
 From iris.base_logic Require Export gen_heap.
 From trillium.prelude Require Import classical_instances.
 From trillium.program_logic Require Import weakestpre adequacy.
-From trillium.fairness Require Export fairness fair_termination fairness_finiteness fuel fuel_termination map_included_utils resources.
+From fairness Require Export fairness.
+From fairis Require Import fair_termination fairness_finiteness fuel fuel_termination map_included_utils resources heap_lang_lm destuttering.
 From trillium.program_logic Require Import ectx_lifting.
-From trillium.fairness.heap_lang Require Import lang.
-From trillium.fairness.heap_lang Require Import tactics notation.
-From trillium.fairness.heap_lang Require Import lifting.
-Set Default Proof Using "Type".
-
-Section adequacy.
-
-Lemma posts_of_empty_mapping `{heapGS Σ M} (e1 e: expr) v (tid : nat) (tp : list expr):
-  tp !! tid = Some e ->
-  to_val e = Some v ->
-  posts_of tp ((λ (_ : val), 0%nat ↦M ∅) ::  (map (λ '(tnew, e), fork_post (locale_of tnew e)) (prefixes_from [e1] (drop (length [e1]) tp)))) -∗
-  tid ↦M ∅.
-Proof.
-  intros Hsome Hval. simpl.
-  rewrite (big_sepL_elem_of (λ x, x.2 x.1) _ (v, (λ _: val, tid ↦M ∅)%I) _);
-    first by auto.
-  apply elem_of_list_omap.
-  exists (e, (λ _: val, tid ↦M ∅)%I); split; last first.
-  - simpl. apply fmap_Some. exists v. split; done.
-  - destruct tp as [|e1' tp]; first set_solver. simpl.
-    apply elem_of_cons.
-    destruct tid as [|tid]; [left|right]; first by simpl in Hsome; simplify_eq.
-    apply elem_of_lookup_zip_with. eexists tid, e, _. do 2 split =>//.
-    rewrite /locale_of /=.
-    rewrite list_lookup_fmap fmap_Some. simpl in Hsome.
-    exists (e1 :: take tid tp, e). rewrite drop_0. split.
-    + erewrite prefixes_from_lookup =>//.
-    + rewrite /locale_of /= take_length_le //.
-      assert (tid < length tp)%nat; last lia. by eapply lookup_lt_Some.
-Qed.
-
-Lemma from_locale_from_lookup tp0 tp tid e :
-  from_locale_from tp0 tp tid = Some e <-> (tp !! (tid - length tp0)%nat = Some e ∧ (length tp0 <= tid)%nat).
-Proof.
-  split.
-  - revert tp0 tid. induction tp as [| e1 tp1 IH]; intros tp0 tid.
-    { unfold from_locale. simpl. done. }
-    unfold from_locale. simpl.
-    destruct (decide (locale_of tp0 e1 = tid)).
-    + intros ?; simplify_eq. rewrite /locale_of /= Nat.sub_diag.
-      split; [done|lia].
-    + intros [H Hlen]%IH. rewrite app_length /= in H.
-      rewrite app_length /= in Hlen.
-      destruct tid as [|tid]; first lia.
-      assert (Heq1 : (length tp0 + 1 = S (length tp0))%nat) by lia.
-      rewrite Heq1 in Hlen.
-      assert (length tp0 ≤ tid)%nat by lia.
-      assert (Heq : (S tid - length tp0)%nat = (S ((tid - (length tp0))))%nat) by lia.
-      rewrite Heq /=. split.
-      * rewrite -H. f_equal. lia.
-      * transitivity tid; try lia. assumption.
-  - revert tp0 tid. induction tp as [|e1 tp1 IH]; intros tp0 tid.
-    { set_solver. }
-    destruct (decide (tid = length tp0)) as [-> | Hneq].
-    + rewrite Nat.sub_diag /=. intros  [? _]. simplify_eq.
-      rewrite decide_True //.
-    + intros [Hlk Hlen]. assert (length tp0 < tid)%nat as Hle by lia.
-      simpl. rewrite decide_False //. apply IH. split.
-      * assert (tid - length tp0 = S ((tid - 1) - length tp0))%nat as Heq by lia.
-        rewrite Heq /= in Hlk. rewrite -Hlk app_length /=. f_equal; lia.
-      * rewrite app_length /=. apply Nat.le_succ_l in Hle. rewrite Nat.add_comm //.
-Qed.
-
-Lemma from_locale_lookup tp tid e :
-  from_locale tp tid = Some e <-> tp !! tid = Some e.
-Proof.
-  assert (from_locale tp tid = Some e <-> (tp !! tid = Some e ∧ 0 ≤ tid)%nat) as H; last first.
-  { split; intros ?; apply H; eauto. split; [done|lia]. }
-  unfold from_locale. replace (tid) with (tid - length (A := expr) [])%nat at 2;
-    first apply from_locale_from_lookup. simpl; lia.
-Qed.
+From heap_lang Require Import locales_helpers_hl.
 
-Definition indexes {A} (xs : list A) := imap (λ i _, i) xs.
 
-Lemma locales_of_list_from_indexes (es' es : list expr) :
-  locales_of_list_from es' es = imap (λ i _, length es' + i)%nat es.
-Proof.
-  revert es'. induction es; [done|]; intros es'.
-  rewrite locales_of_list_from_cons=> /=. rewrite /locale_of.
-  f_equiv; [lia|]. rewrite IHes. apply imap_ext.
-  intros x ? Hin. rewrite app_length=> /=. lia.
-Qed.
+Set Default Proof Using "Type".
 
-Lemma locales_of_list_indexes (es : list expr) :
-  locales_of_list es = indexes es.
-Proof. apply locales_of_list_from_indexes. Qed.
+Section adequacy.
 
 Theorem heap_lang_continued_simulation_fair_termination {FM : FairModel}
         `{FairTerminatingModel FM} {LM:LiveModel heap_lang FM} ξ a1 r1 extr :
@@ -131,13 +52,14 @@ Proof.
   iMod (model_state_init s1) as (γmod) "[Hmoda Hmodf]".
   iMod (model_fuel_mapping_init s1) as (γmap) "[Hmapa Hmapf]".
   iMod (model_free_roles_init s1 (FR ∖ live_roles _ s1)) as (γfr) "[HFR Hfr]".
+  set (hG := {| heap1_gen_heapGS := genheap |}). 
   set (distG :=
          {|
           heap_fairnessGS := {|
                               fairness_model_name := γmod;
                               fairness_model_fuel_mapping_name := γmap;
                               fairness_model_free_roles_name := γfr;
-                              |}
+                              |};
          |}).
   iMod (H distG) as "Hwp". clear H.
   iExists state_interp, (λ _, 0%nat ↦M ∅)%I, fork_post.