# Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
This repository contains the Iron logic, as described in the POPL'19 paper
"[Iron: Managing Obligations in Higher-Order Concurrent Separation Logic](https://iris-project.org/pdfs/2019-popl-iron-final.pdf)" by
Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal.
## Building Iron
Iron has been built and tested with the following dependencies
- Coq 8.9.0
- A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq)
- A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
## Directory Structure
- In [theories/algebra/ufrac_auth.v](theories/algebra/ufrac_auth.v), the
fractional authoritative camera described in Section 6 with improper
fractions is defined.
- The semantics of the connectives of fractional predicates logic are given in
[theories/bi/fracpred.v](theories/bi/fracpred.v).
This file does not contain a description of the lifted program
logic but instead contains the definitions of ∧, ∗, ∀, and other
the other connectives. It also contains all the rules of the
specific to this logic that are used later.
- The machinery for connecting the generalized proofmode/MoSeL from to
fractional predicates is contained in [theories/proofmode](theories/proofmode).
- In [theories/iron_logic](theories/iron_logic) much of the core Iron logic
discussed in Section 3 is defined.
* _Uniformity_ with respect to fractions is defined in
[theories/iron_logic/iron.v](theories/iron_logic/iron.v) as `Uniform` and
several closure properties of it are proved.
* _Trackable invariants_ as discussed in Section 3.2 are formalized
in [theories/iron_logic/fcinv.v](theories/iron_logic/fcinv.v).
* The definition of weakest preconditions from Section 6 is in
[theories/iron_logic/weakestpre.v](theories/iron_logic/weakestpre.v).
- The formalization specific to the λref,conc is in
[theories/heap_lang](theories/heap_lang).
* The definition of the heap in terms of ghost state from Section 6 is in
[theories/heap_lang/heap.v](theories/heap_lang/heap.v) as `heapG`. So too
are the definitions of ↦ and 𝖊 (in the formalization called `perm`).
* The theorems mentioned in Section 6 about updates to the heap ghost
state are proven in [theories/heap_lang/heap.v](theories/heap_lang/heap.v).
* The state interpretation from Section 6 is defined in
[theories/heap_lang/heap.v](theories/heap_lang/heap.v) as `heap_ctx`.
* Theorems 3.1 and 6.1 are proven in
[theories/heap_lang/adequacy.v](theories/heap_lang/adequacy.v).
* The operational semantics from Figure 5 are defined in
[theories/heap_lang/lang.v](theories/heap_lang/lang.v).
* The rules from Figures 4 and 7 are proven in
[theories/heap_lang/lifting.v](theories/heap_lang/lifting.v).
- All of the examples of the paper are formalized and may be found in
[theories/heap_lang/lib/](theories/heap_lang/lib/). All of the examples are
formalized purely within the lifted logic. There is no fraction accounting in
the proofs and no significant bookkeeping beyond what is found in
vanilla Iris.
As mentioned in the paper, a small portion of `par` cannot be formalized in
the lifted logic but in the formalization this is factored out into `spawn`
in [theories/heap_lang/lib/spawn.v](theories/heap_lang/lib/spawn.v)
* The example from 4.1 is in [theories/heap_lang/lib/resource_transfer_par.v](theories/heap_lang/lib/resource_transfer_par.v).
* The example from 4.2 is in [theories/heap_lang/lib/resource_transfer_fork.v](theories/heap_lang/lib/resource_transfer_fork.v).
* The example from 4.3 is in [theories/heap_lang/lib/message_passing.v](theories/heap_lang/lib/message_passing.v).
* The example from 4.4 is in [theories/heap_lang/lib/message_passing_example.v](theories/heap_lang/lib/message_passing_example.v).
* The example from 4.5 is in [theories/heap_lang/lib/par.v](theories/heap_lang/lib/resource_transfer_par.v).
Note that `spawn.v`, `resource_transfer_par.v`, and `resource_transfer_fork.v`
use the same state transition system (from Figure 3). This is formalized in
[theories/heap_lang/lib/transfer_resource_sts.v](theories/heap_lang/lib/transfer_resource_sts.v).
## Differences Between the Formalization and The Paper
There are a number of small differences between the paper presentation
of Iron and the formalization in Coq. We briefly discuss them here.
### Weakest Preconditions and Texan Triples
In the paper we have worked with Hoare triples in
specifying theorems and rules. In the Iris formalization we have used
weakest preconditions. Weakest preconditions are used for the
definition of Hoare triples (see Section 5) but in the formalization
we also work with them throughout the proofs and in some
specifications. They are often easier more convenient to work with in
Coq because they allow us to use the Iris proofmode context and native
Coq context for manipulating preconditions.
More than this, in the paper we define Hoare triples as follows:
{P} e {v. Q(v)} ≜ □ (P -∗ wp e {v. Q(v)})
In the Coq formalization this proves to be often unwieldy. Generally
when we has a Hoare triple `{P} e {v.Q(v)}` we use it by applying it to a
goal of the form `wp e {v. Q'(v')}`. With this definition, we must
first apply a lemma about the monotonicity of Hoare triples to obtain
`{P} e {Q'(v)}` from `∀ v. Q(v) -∗ Q'(v)` and then we may apply
this. In Coq we *bake in this cut* with so called Texan Triples,
defined as follows:
{P} e {v. Q(v)} ≜
□ ∀ Φ : Val → iProp. P -∗ ▷ (∀ v. Q(v) -∗ Φ(v)) -∗ wp e {v. Φ(v)}
With this formulation we can apply `{P} e {v. Q(v)}` to any goal of the
form `wp e {v. Q'(v)}`, saving a step. Additionally, the fact that we
only need to prove the implication for post-conditions under a ▷ is
a strictly more general requirement.
### Invariant Rules
In the paper all of the invariant rules are stated in terms of Hoare
triples. In Coq this is a needless entangling and a more flexible
collection of invariant rules is used instead.
Specifically, rather than proving rules such as
`LTINV-OPEN` which specify how to open an invariant with a Hoare
triple, we have rules specifying invariants in terms of the fancy
update modality.
This modality was briefly discussed in the paper. It is defined in
`iris-coq/theories/base_logic/lib/fancy_update.v` (as `fupd_def`) and
its adaption to for the the lifted logic is defined in
`theories/iron_logic/iron.v` (as `iron_fupd_def`). Briefly, it's
a frame-preserving update which also allows for the use of invariants.
Since weakest preconditions (and by extension Hoare triples) are
defined with fancy updates the invariant rules written in terms of fancy
updates lift easily to the ones described in the paper.
The paper rules are less flexible though because they only
apply when the goal is a weakest precondition or Hoare triple rather
than any goal with fancy updates.
Instead of the Hoare rule for invariant allocation, for instance, in
the formalization we have `fcinv_alloc_named` from
`theories/iron_logic/fcinv.v` which states that the following
holds:
▷ (∀ γ. Ψ γ) -∗
|={E}=> ∃ γ. fcinv_own γ 1 ∗ fcinv_cancel_own γ 1 ∗ fcinv N γ (Ψ γ)
This can be used to derive `LINV-ALLOC` when used in conjunction with
`HOARE-CONS`. The latter rule is called `ht_vs` in
`iris-coq/theories/program_logic/hoare.v`.
There is a correspondence between the invariant rules presented in the
paper with Hoare triples and those in the formalization.
- `TINV-ALLOC` and `LTINV-ALLOC` follow from `fcinv_alloc_named`.
- `TINV-OPEN` and `LTINV-OPEN` follow from `fcinv_open`.
- `TINV-DEALLOC` and `LTINV-DEALLOC` follow from `fcinv_cancel`.
All of these theorems are proven in `theories/iron_logic/fcinv.v`.
The rules governing normal Iris invariants, such as those for `INV-OPEN`,
are also defined using the fancy update modality. They may be found in
`iris-coq/theories/base_logic/lib/invariants.v`.
## A Correspondence of Theorems, Definitions, and Examples in the Paper to the Formalization
While the correspondence between the contents of the paper and the formalization
is discussed above, we also provide an explicit table for convenience.
| Paper definition or theorem | Coq definition or theorem | File |
|-------|--------|---------|
| The language definition in Sec. 3 | `expr` | `iron/theories/heap_lang/lang.v` |
| `𝖊` and `↪` | `perm` and `↦` | `iron/theories/heap_lang/heap.v` |
| Trackable invariants | `fcinv` | `iron/theories/iron_logic/fcinv.v` |
| `OPerm(-, -)` | `fcinv_own` | `iron/theories/iron_logic/fcinv.v` |
| `DPerm(-, -)` | `fcinv_cancel_own` | `iron/theories/iron_logic/fcinv.v` |
| `HOARE-FRAME` | `hoare_frame_r` | `iris-coq/theories/program_logic/hoare.v` |
| `HOARE-VAL` | `ht_val` | `iris-coq/theories/program_logic/hoare.v` |
| `HOARE-λ` | `pure_rec` | `iron/theories/heap_lang/lifting.v` |
| `HOARE-BIND` | `ht_bind` | `iris-coq/theories/program_logic/hoare.v` |
| `EMP-SPLIT` | `perm_split` | `iron/theories/heap_lang/heap.v` |
| `PT-SPLIT` | `mapsto_uniform` | `iron/theories/heap_lang/heap.v` |
| `PT-DISJ` | `mapsto_valid_2` | `iron/theories/heap_lang/heap.v` |
| `HOARE-ALLOC` | `wp_alloc` | `iron/theories/heap_lang/lifting.v` |
| `HOARE-FREE` | `wp_free` | `iron/theories/heap_lang/lifting.v` |
| `HOARE-LOAD` | `wp_load` | `iron/theories/heap_lang/lifting.v` |
| `HOARE-STORE` | `wp_store` | `iron/theories/heap_lang/lifting.v` |
| `HOARE-FORK-EMP`/`HOARE-FORK-TRUE` | `wp_fork` | `iron/theories/heap_lang/lifting.v` |
| `INV-DUP` | `inv_persistent` | `iron/theories/heap_lang/lifting.v` |
| `INV-ALLOC` | `inv_alloc` | `iris-coq/theories/base_logic/lib/invariants.v` |
| `INV-OPEN` | `inv_open` | `iris-coq/theories/base_logic/lib/invariants.v` |
| `TINV-SPLIT` | `fcinv_own_fractional` | `iron/theories/iron_logic/fcinv.v` |
| `TINV-DUP` | `fcinv_persistent` | `iron/theories/iron_logic/fcinv.v` |
| `TINV-ALLOC` | `fcinv_alloc_named` | `iron/theories/iron_logic/fcinv.v` |
| `TINV-OPEN` | `fcinv_open` | `iron/theories/iron_logic/fcinv.v` |
| `TINV-DEALLOC` | `fcinv_cancel` | `iron/theories/iron_logic/fcinv.v` |
| Uniform with respect to fractions | `Uniform` | `iron/theories/iron_logic/iron.v` |
| `HOARE-CONS` | `ht_vs` | `iris-coq/theories/program_logic/hoare.v` |
| The rules from Figure 5 | `head_step` | `iron/theories/heap_lang/lang.v` |
| Theorem 3.1 | `heap_basic_adequacy` | `iron/theories/heap_lang/adequacy.v` |
| Theorem 3.2 | `heap_all_adequacy` | `iron/theories/heap_lang/adequacy.v` |
| `HOARE-PAR` | `par_spec` | `iron/theories/heap_lang/lib/par.v` |
| The example from 4.1 | `transfer_works1` | `iron/theories/heap_lang/lib/resource_transfer_par.v` |
| The rules from Figure 6 | Several theorems | `iron/theories/heap_lang/lib/resource_transfer_sts.v` |
| The example from 4.2 | `transfer_works1` | `iron/theories/heap_lang/lib/resource_transfer_fork.v` |
| The example from 4.3 | Several theorems | `iron/theories/heap_lang/lib/message_passing.v` |
| The queue specifications from 4.3 | Several theorems in Section `queue_bag_spec` | `iron/theories/heap_lang/lib/queue.v` |
| The example from 4.4 | `program_spec` | `iron/theories/heap_lang/lib/message_passing_example.v` |
| The example from 4.5 | Several theorems | `iron/theories/heap_lang/lib/{spawn,par}.v` |
| Definitions of lifted connectives | Several definitions | `iron/theories/bi/fracpred.v` |
| Definition of lifted `↦` | `↦` | `iron/theories/heap_lang/heap.v` |
| `LHOARE-FRAME` | `iron_wp_frame_r` | `iris-coq/theories/program_logic/hoare.v` |
| `LHOARE-VAL` | `iron_wp_val` | `iris-coq/theories/program_logic/hoare.v` |
| `LHOARE-λ` | `pure_rec` | `iron/theories/heap_lang/lifting.v` |
| `LHOARE-BIND` | `iron_wp_bind` | `iris-coq/theories/program_logic/hoare.v` |
| `LPT-DISJ` | `mapsto_valid_2` | `iron/theories/heap_lang/heap.v` |
| `LHOARE-ALLOC` | `iron_wp_alloc` | `iron/theories/heap_lang/lifting.v` |
| `LHOARE-FREE` | `iron_wp_free` | `iron/theories/heap_lang/lifting.v` |
| `LHOARE-LOAD` | `iron_wp_load` | `iron/theories/heap_lang/lifting.v` |
| `LHOARE-STORE` | `iron_wp_store` | `iron/theories/heap_lang/lifting.v` |
| `LHOARE-FORK` | `iron_wp_fork` | `iron/theories/heap_lang/lifting.v` |
| `LTINV-SPLIT` | `fcinv_own_fractional` | `iron/theories/iron_logic/fcinv.v` |
| `LTINV-DUP` | `fcinv_persistent` | `iron/theories/iron_logic/fcinv.v` |
| `LTINV-ALLOC` | `fcinv_alloc_named` | `iron/theories/iron_logic/fcinv.v` |
| `LTINV-OPEN` | `fcinv_open` | `iron/theories/iron_logic/fcinv.v` |
| `LTINV-DEALLOC` | `fcinv_cancel` | `iron/theories/iron_logic/fcinv.v` |
| Definition of Hoare triples | `iron_wp` | `iron/theories/iron_logic/weakestpre.v` |
| Theorem 5.1 | `heap_basic_adequacy` | `iron/theories/heap_lang/adequacy.v` |
| Theorem 5.2 | `heap_all_adequacy` | `iron/theories/heap_lang/adequacy.v` |
| Definition of WP in Section 6 | `wp_def` | `iris-coq/theories/program_logic/weakestpre.v` |
| Definition of state interpretation from Section 6 | `heap_ctx` | `iron/theories/heap_lang/heap.v` |
| Theorem 6.1 | `wp_strong_all_adequacy` | `iris-coq/theories/program_logic/adequacy.v` |
| The lock specifications | Several theorems | `iron/theories/heap_lang/lib/spin_lock_track.v` |
| Adequacy for the lock | `lock_always_freed` | `iron/theories/heap_lang/lib/spin_lock_track.v` |