# 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/