Completeness of Iris-Based Program Logics (Artifact)

This is the artifact for the paper Completeness of Iris-based Program Logics. icfp26-artifact29.tax.xz is the Rocq development. icfp26-artifact29-vm.tar.xz is a QEMU virtual machine containing the Rocq development and all of its dependencies. The VM image takes 10 GiB of disk space. Building the development This Rocq development is known to compile with OCaml 5.4.1 Rocq 9.1.1 std++ 1.13.0 Iris 4.5.0 The case studies require Autosubst dev Hierarchy Builder 1.10.1 Mathematical Components 2.5.0 ELPI 3.4.2 and its Rocq plugin 3.2.0 Coquelicot 3.4.4 The recommended way to install the dependencies is through opam. Users of the VM image should jump to step 6. Step 1. Install opam if not already installed (a version greater than 2.0 is required). Step 2. Install a new switch and link it to the current directory. opam switch create iris-completeness 5.4.1opam switch link iris-completeness .eval $(opam env) Step 3. Add the Rocq and Iris opam repositories. opam repo add rocq-released https://rocq-prover.org/opam/releasedopam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.gitopam update Step 4. Pin non-standard dependencies. ./depends.sh Step 5. Install the right version of the dependencies as specified in the opam file. opam install . --deps-only Step 6. Build the development. eval $(opam env)make Step 7. (Optional) Print axioms. python3 print_axioms.py Using the development as a dependency This repository contains two opam packages: rocq-iris-completeness: language-independent completeness and requisiteness theorems. rocq-iris-completeness-examples: case studies of HeapLang, lambdaRust, time credits, Eris, and relational logic. This package is not expected to be used as a dependency. To use the rocq-iris-completeness package, add this to the depends field of your opam file: "rocq-iris-completeness" { ((= "dev")) } Since this package is not published to the Rocq package manager yet, you also need to add an opam pin to the URL of the repository or a local directory containing the development. For example opam pin add --no-action rocq-iris-completeness.dev "$(pwd)" Code structure All Rocq mechanizations are in the theories/ directory. framework/abstract/abstract_ectx_lang_completeness_classical.v: the language-independent completeness theorem, with the Strong Invariant Opening Lemma (Lemma 15) proven using excluded middle, as described in the paper. There is an alternative proof that does not use the excluded middle law at framework/abstract/abstract_lang_completeness.v, but this proof unfolds the definition of wp. File framework/abstract/abstract_ectx_lang_completeness.v is based on abstract_lang_completeness.v and thus does not use excluded middle. framework/total/lang_total_completeness.v: the language-independent total completeness theorem. It does not depend on the excluded middle law. framework/requisite/lang_requisiteness.v: the language-independent requisiteness theorem. case_studies/heaplang/: the completeness and requisiteness of HeapLang. case_studies/lambda_rust/: the completeness of lambdaRust. case_studies/iris_time/: the completeness of the time credit logic. case_studies/eris/: the completeness of the error credit logic. case_studies/relational/: the completeness of a CaReSL-style relational logic. Links with the paper Section 2: this section is for presentation purposes only. Section 3 Figure 3 (ConcLang): a subset of HeapLang for paper presentation only, not mechanized 3.2 safe-tp: cfg_safe_forking and adequate_tp with ϕ = λ v _, φ v; note that cfg_safe_forking does not have a parameter about φ because the Rocq version of the completeness proof uses a different approach to handle φ, and does not directly put φ into cfg_safe_forking. Remark 11: a simple fact inlined in proofs Remark 12: cfg_safe_step and adequate_tp_erased_step Theorem 13: a standard Iris theorem (part of the dependencies), specifically iris.heap_lang.adequacy.heap_adequacy Lemma 14: a special case of abstract_lang_completeness.weakestpre_completeness Lemma 15: This lemma is proven twice: A generic proof using classical logic: wp_inv_open_maybe_ectxlang_inv; file abstract_ectx_lang_completeness_classical.v is then based on this. A proof in the model: wp_inv_open_maybe; files abstract_lang_completeness.v and abstract_ectx_lang_completeness.v are based on this and thus have the additional assumption that wp satisfies this law. Apart from this, these two files are identical to abstract_ectx_lang_completeness_classical.v. Theorem 16: a special case of Theorem 17 \(I_{compl}\): abstract_lang_completeness.cfg_inv Theorem 17: weakestpre_sem_completeness Condition 18: a special case of the lang_completeness field of typeclass abstract_lang_completeness_gen Section 4 \(S_{\circ}(\sigma)\): heaplang.completeness_generic.heap_inv Completeness result: heap_lang_sem_completeness_intuitionistic Identified completeness gaps have been merged into Iris. Section 5 Theorem 19: a standard Iris theorem, specifically iris.heap_lang.total_adequacy.heap_total Theorem 20: sem_total_completeness The total completeness condition: field lang_total_completeness of typeclass lang_total_completeness_gen Total completeness of HeapLang: heap_lang_sem_total_completeness Section 6 The per-location invariant for exploiting reads: lambda_rust.races.loc_state_inv Lemma for starting non-atomic memory access: loc_state_start_race Lemma for finishing non-atomic memory access: loc_state_end_race \(S_{\circ}(\sigma)\): lambda_rust.completeness.baby_heap_inv Completeness result: lambda_rust.completeness.lrust_completeness Identified completeness gaps are in lambda_rust/fixes.v. The missing laws for non-deterministic comparison make up most of this file. We also need comparisons to be atomic since their behavior depends on memory existing, which they check atomically. The new exclusivity law for the block tokens is heap_freeable_excl. wp_fork_fupd strengthens the fork law to correspond with the one we presented in Figure 3. lambdaRust here had an unnecessarily weak law. Section 7 Theorem 21: a result by Mével et al. [53] \(S_{\circ}(\sigma)\): iris_time.completeness.state_inv Theorem 22: time_credit_sem_completeness Section 8 Theorem 23: a result by Aguirre et al. [1] Theorem 24: eris_total_completeness.tgl_twp_completeness Lemma 25: eris_total_completeness.prob_lang_tgl_sem_completeness Section 9 Theorem 26: relational_noalloc.basic_rel_soundness. As the name “noalloc” indicates, file relational_noalloc.v actually contains a completeness theorem for programs without allocation (and hence does not need the reserved locations set), but the soundness theorem in this file applies to all programs, even with allocations. Theorem 27: relational_alloc1.basic_rel_soundness Theorem 28: relational_alloc1.basic_rel_completeness_empty Section 10 Definition 29: a standard Iris definition, specifically iris.program_logic.weakestpre.wp' Theorem 30: a standard Iris theorem, specifically iris.program_logic.adequacy.wp_adequacy_gen Theorem 31: lang_requisiteness.wp_requisiteness \(I_{compl}\): lang_requisiteness.requisiteInv Requisiteness of HeapLang: heaplang.requisiteness.wp_requisiteness Appendix A Condition 32: the lang_completeness field of typeclass abstract_lang_completeness_gen Appendix B seq: cfg_forking with parameter f = DoesNotFork, and adequate_nofork_nofork field in record adequate_nofork ssafe-tp: cfg_safe_forking and adequate_tp Theorem 33: weakestpre_sem_completeness_nofork Theorem 34: wp_requisiteness_nofork There are also *_nofork variants for case studies in Sections 4 to 7. Appendices C—E and G: external results from the dependencies. Notably, Appendix C corresponds to lemmas in iris.base_logic.upred, ignoring the laws for connectives we do not need. Axioms We use classical logic to prove the Strong Invariant Opening Lemma. Classical_Prop.classic : ∀ P : Prop, P ∨ ¬ P Note that some files like heaplang.completeness_intuitionistic derive the Strong Invariant Opening Lemma in the model, and are thus axiom-free. The rocq-clutch package used by the error credits case study introduces the following axioms: ClassicalDedekindReals.sig_forall_dec : ∀ P : nat → Prop, (∀ n : nat, {P n} + {¬ P n}) → {n : nat | ¬ P n} + {∀ n : nat, P n}ClassicalDedekindReals.sig_not_dec : ∀ P : Prop, {¬ ¬ P} + {¬ P}ClassicalEpsilon.constructive_indefinite_description : ∀ (A : Type) (P : A → Prop), (∃ x : A, P x) → {x : A | P x}Classical_Prop.classic : ∀ P : Prop, P ∨ ¬ PFunctionalExtensionality.functional_extensionality_dep : ∀ (A : Type) (B : A → Type) (f g : ∀ x : A, B x), (∀ x : A, f x = g x) → f = gPropExtensionality.propositional_extensionality : ∀ P Q : Prop, P ↔ Q → P = Q License The Rocq development is licensed under the BSD 3-Clause “New” or “Revised” License. The VM image is an aggregate of several free software under difference licenses.