# GPFSL (iRC11) COQ DEVELOPMENT
This is a separation logic for [ORC11] based on [iGPS] and [FSL]. It has been recently renamed as **iRC11**.
## Prerequisites
This version is known to compile with:
- Coq 8.11.2 / 8.12.0
- A development version of [ORC11] and [Iris]. See the [opam](opam) file for the exact
version.
The easiest way to install the correct versions of the dependencies is through
opam (2.0.0 or newer). You will need the Coq and Iris opam repositories:
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
## Updating
After doing `git pull`, the development may fail to compile because of outdated
dependencies. To fix that, please run `opam update` followed by
`make build-dep`.
## Building Instructions
Run `make -jN` to build the full development, where `N` is the number of your
CPU cores.
## STRUCTURE
iRC11 formalizes the actual language of RBrlx, as well as the logic for general
verification of programs written that language.
* [lang/lang.v](theories/lang/lang.v) defines the language as a
combination of ORC11 and a *CPS-style expression* language following that of
lambda-Rust.
* The expression language is defined with `base.head_step`.
* The complete language combines `base.head_step`, `lbl_machine_step`,
`drf_pre`, and `drf_post` into `head_step`.
* [base_logic](theories/base_logic) is the instantiation of the
language in Iris. The view-predicate assertion type `vProp` (Section 3.1, 4.2
of the RBrlx paper) is defined in [vprop.v](theories/base_logic/vprop.v).
The points-to assertions `l ↦ v` (Section 3.1) are defined in
[na.v](theories/base_logic/na.v).
* [adequacy.v](theories/base_logic/adequacy.v) proves that
expressions verified in the base logic are actually safe and functionally
correct. Since iRC11 is built on the base logic, this in turn implies that
expressions verified in iRC11 are also safe and functionally correct.
* [gps](theories/gps) provides the model of iRC11 single-location
cancellable invariants (Section 3.2, 4.4). Note that iRC11 single-location
invariants presented in the paper are only a very simplified version of what
we actually need in Coq.
* The ATOM definition (iRC11-CInv-Model, Section 4.4) is called `GPS_INV` in
Coq, see `GPS_INV_def` in
[middleware.v](theories/gps/middleware.v).
The actual instantiation with raw cancellable invariants can be found in
[surface.v](theories/gps/surface.v), for example
`GPS_vSP_Reader`.
* [surface.v](theories/gps/surface.v) contains a *single-writer*
instance of iRC11 single-location cancellable invariants. The following
table lists the rules that are ***similar*** but not exactly the same as the
rules presented in Section 3 of the RBrlx paper, because in Coq they are
more powerful and hence more complicated.
| Proof Rule (Fig. 3) | File | *Similar* lemma |
|-----------------------|--------------------|--------------------------|
| iRC11-CInv-New | surface.v | GPS_vSP_Init |
| iRC11-CInv-FAA-Rlx | surface.v | GPS_vSP_SWWrite_rel |
| iRC11-CInv-FAA-Rlx | surface.v | GPS_vSP_Read |
| iRC11-CInv-Cancel | surface.v | GPS_vSP_dealloc |
The rule iRC11-CInv-Tok is exactly the rule Raw-CInv-Tok (see below),
because single-location cancellable invariants are built from raw
cancellable invariants.
More details on the single-writer invariants can be found in Section 5 of
the technical appendix of the RBrlx paper.
* [logic](theories/logic) provides the models of various other
features of the logic.
* [view_invariants.v](theories/logic/view_invariants.v) provides
the model of raw cancellable invariants (Section 4.2, 4.3). So in Coq, raw
cancellable invariants are call *view invariants*.
In Coq, raw cancellable invariants have more complex rules than what were
presented in the paper. Below is only the mapping of rules in the paper to
Coq.
| Definition (Sect. 4.3)| File | Definition |
|-----------------------|--------------------|--------------------------|
| Raw-CInv-Model-Tok | view_invariants.v | view_tok_def |
| Raw-CInv-Model | view_invariants.v | view_inv_def |
| Proof Rule (Fig. 7) | File | Lemma |
|-----------------------|--------------------|--------------------------|
| Raw-CInv-New | view_invariants.v | view_inv_alloc |
| Raw-CInv-Tok | view_invariants.v | view_tok_asfractional |
| Raw-CInv-Acc | view_invariants.v | view_inv_acc_consume |
| Raw-CInv-Cancel | view_invariants.v | view_inv_dealloc |
Note that the access rule Raw-CInv-Acc is given Coq with Iris style, where
viewshifts are used instead of Hoare triples.
* [relacq.v](theories/logic/relacq.v) provides the model of
fence modalities (Section 5.2).
| Definition (Sect. 5.2)| File | Definition |
|-----------------------|--------------------|--------------------------|
| RelMod-Model | relacq.v | rel_mod_def |
| AcqMod-Model | relacq.v | acq_mod_def |
* The Ghost-Mod rule is realized by `rel_embed_elim` and `acq_embed_elim`
(in [relacq.v](theories/logic/relacq.v)),
because ghost elements are embedded in iRC11 directly from Iris.
If `ownGhost(γ,a)` is the ghost ownership assertion in Iris (dashed box in
Fig. 3 of the paper), then `⎡ownGhost(γ,a)⎤` is the ghost ownership
assertion in iRC11.
The *embedding* modality `⎡·⎤` is defined with `monPred_embed_def` in Iris's
[monPred.v](https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/bi/monpred.v).
* [lifting.v](theories/logic/lifting.v) provides the rules of
various features around Hoare triples.
In Iris's Coq, we use weakest preconditions `wp` instead of Hoare triples.
Again, not all rules are exact matches with what were presented in the
paper. For example, allocation and deallocation of locations
additionally involve the *freeable* resource ⎡†l…n⎤.
| Proof Rule (Fig. 3) | File | Lemma |
|-----------------------|--------------------|--------------------------|
| Dealloc | lifting.v | wp_free |
| NA-Read | lifting.v | wp_read_non_atomic |
| NA-Write | lifting.v | wp_write_non_atomic |
| Rel-Fence | lifting.v | wp_rel_fence |
| Acq-Fence | lifting.v | wp_acq_fence |
* An example verification of the Message-Passing example, which has stronger
resource reclamation than both examples given in Figure 4 of the RBrlx paper,
is given in [examples/mp_reclaim.v](theories/examples/mp_reclaim.v)
[ORC11]: https://gitlab.mpi-sws.org/iris/orc11
[Iris]: https://gitlab.mpi-sws.org/iris/iris
[iGPS]: http://plv.mpi-sws.org/igps/
[FSL]: http://plv.mpi-sws.org/fsl/