Satisfiability Demo

This is a demo how to use the satisfiable-predicate to prove adequacy in Iris. It is accompanying the corresponding Iris workshop talk on Making Adequacy of Iris Satisfying. The demo contains three separate adequacy proofs (explained in more detail below):

1. A standard weakest precondition in ordinary Iris (Section: Standard Iris).
2. A weakest precondition in Transfinite Iris, which allows an arbitrary number of laters per step (Section: Transfinite Iris).
3. A coinductively defined weakest precondition without step-indexing in Iris (Section: Iris Without Step-Indexing).

Getting Started

Installation using Opam. We recommend installing this demo in a new switch to avoid overriding any existing installations of Iris or stdpp. To create a new switch in the demo folder and build the demo, please execute the following:

opam switch create . ocaml-base-compiler.4.14.0 --no-install       # create a new opam switch in this folder
eval $(opam env)                                                   # update the shell environment for the new switch
opam repo add coq-released https://coq.inria.fr/opam/released      # add Coq opam package repositories
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git    # add Iris opam package repositories
make builddep                                                      # install dependencies (e.g., Coq, stdpp, Iris, Transfinite Iris)
make -j4                                                           # build this demo; replace 4 with the number of cores to use

Note on the Iris Version. This demo uses both Transfinite Iris and Standard Iris. To do so, it relies on a version of Iris (from 2022) that is parametric in the type of step-indices. Concretely, this version of Iris contains parametric definitions of algebra, bi, and proofmode. It picks natural numbers as the step-indices for the base_logic. The demo additionally relies on a version of Transfinite Iris, which instantiates this parametric version of Iris. Both versions are pinned in the .opam file and installed automatically when following the above instructions.

Standard Iris

For standard Iris, we prove adequacy of the standard program_logic-weakest precondition, with later credits, laters, concurrency, and fancy updates. The relevant files are contained in the folder theories/iris_standard/:

theories/iris_standard
 |-satisfiable/              # definition of the SAT predicate for satisfiability
 |-base_logic_extension.v    # additional lemmas for "global ghost state" for later credits, fancy updates, ghost_maps, ...
 |-program_logic_adequacy.v  # adequacy proof for the standard program logic weakest precondition
 |-heaplang_adequacy.v       # instantiation of the generic proof for HeapLang (including proof of the initial state-interpretation allocation)

Definition of Satisfiability

For the definition of satisfiability in standard Iris, there are two candidates:

• Candidate 1. The definition sat_global (in theories/iris_standard/satisfiable/satisfiable_standard.v). This definition has almost all the usual properties of satisfiable. The only property we lose is that we cannot pull out disjunctions (i.e., it does not validate sat (P ∨ Q) → sat P ∨ sat Q). In exchange, this definition has the following additional property, which makes allocating global ghost state easy:

  sat_alloc_res:
    ✓ a → sat_global P → ∃ γ, sat_global (own γ a ∗ P)

  In other words, just like in own_alloc, we get to allocate any valid resource a. And in the case of sat_alloc_res, we get access to the ghost name γ immediately outside of Iris.

• Candidate 2. The normal definition sat_standard (in theories/iris_standard/satisfiable/satisfiable_standard.v). This definition allows us to pull out disjunctions with sat_or (using classical logic). However, it makes it difficult to allocate global ghost state, because it does not have the rule sat_alloc_res.

For this demo, we combine both candidates by defining sat m P (in theories/iris_standard/satisfiable/satisfiable_standard.v): We parameterize the definition of satisfiable by a mode m, a flag which is either Alloc or Running. The idea is that in the Alloc mode, we can allocate global resources (akin to sat_global in Option 1). We then eventually transition to Running (using sat_end_alloc in theories/iris_standard/satisfiable/satisfiable_standard.v). (Once in the Running mode, we cannot return to the Alloc mode.) In the Running mode, we can then pull out disjunctions (classically). As an aside, adequacy proofs that never need to pull out a disjunction can stay in the Alloc mode forever, since all the other properties are the same.

Transfinite Iris

For Transfinite Iris, we prove adequacy of a version of the weakest precondition, which allows an arbitrary number of laters per step. This is enabled in the definition by using an existential quantifier to quantify over the number of laters before the next step. (In standard Iris, this would not be sound, because the quantifier could depend on the step-index. For example, one can prove |- ∃ n, ▷^n False in standard Iris.) The relevant files are contained in the folder theories/iris_transfinite/:

theories/iris_transfinite
 |-prelims/                  # definition of the weakest precondition and an instantiation with HeapLang
 |-base_logic_extension.v    # additional lemmas for "global ghost state" for fancy updates, ghost_maps, ...
 |-program_logic_adequacy.v  # adequacy proof for the weakest precondition with an arbitrary number of laters
 |-heaplang_adequacy.v       # instantiation of the generic proof for HeapLang (including proof of the initial state-interpretation allocation)

Delta over the Iris proof. Despite the difference between the two weakest preconditions, the delta over the standard Iris proof is small. (We don't use later credits in this version, because they are currently not defined in the Transfinite Iris version.) The only interesting difference is in the lemma wp_step (in theories/iris_transfinite/program_logic_adequacy.v). In the transfinite proof, we use SAT_exists to pull out the existential in the definition. That's basically it! All the other lemmas are virtually the same (except for no later credits), since the modalities that are used inside the definition of the weakest precondition are not leaked to the top-level lemma statements (e.g., compare wp_step in the standard and transfinite adequacy proofs).

Global Ghost State. In principle, global ghost state allocation in Transfinite Iris can be handled using own_alloc directly, but we keep the structure close to standard Iris in this demo. More specifically, the standard allocation lemma own_alloc is of the form:

own_alloc:
  ✓ a  →  ⊢ |==> ∃ γ: gname, own γ a

Since satisfiability allows us to eliminate updates and, in the Transfinite Iris model, also to pull out existential quantifiers over countable types like gname, we can use this lemma directly. In contrast, for standard Iris, we cannot use this lemma to allocate global ghost state, because the existentially quantified γ cannot be pulled out.

Iris Without Step-Indexing

For Iris without step-indexing, we use most definitions from Standard Iris, but fix the step-index to be 1 in the definition of satisfiability (hence the name iris_one in the code). "Without step-indexing" means we do not get to use the later modality in our definition of the weakest precondition (otherwise, adequacy breaks). Nevertheless, we can still define a weakest precondition coninductively (see theories/iris_one/prelims/weakestpre.v). The relevant files are contained in the folder theories/iris_one/:

theories/iris_transfinite
 |-prelims/                  # definition of the weakest precondition and an instantiation with HeapLang
 |-base_logic_extension.v    # additional lemmas for "global ghost state" for fancy updates, ghost_maps, ...
 |-program_logic_adequacy.v  # adequacy proof for the coinductively defined weakest precondition without laters
 |-heaplang_adequacy.v       # instantiation of the generic proof for HeapLang (including proof of the initial state-interpretation allocation)

Fixing a Step-Indexing

For the definition of satisfiability, we can essentially fix any concrete natural number i as the step-index. Here, we fix i := 1 in the definition. For any concrete choice of i, we get almost all satisfiability rules. In particular, we get the existential elimination rule sat (∃ x, P x) → ∃ x, sat (P x).

The only rules where the choice matters is interactions with laters. With i:=1, we can prove that sat (◇ P) → sat P where ◇ P := P ∨ ▷ False is Iris's "except-zero" modality. The modality is used inside the definition of fancy updates. Thus, to eliminate fancy updates, we pick i := 1 for this version.