ProofGuide.md 11.5 KB
 Ralf Jung committed Mar 13, 2019 1 2 3 4 5 6 7 8 ``````# Iris Proof Guide This work-in-progress document serves to explain how Iris proofs are typically carried out in Coq: what are the common patterns, what are the common pitfalls. This complements the tactic documentation for the [proof mode](ProofMode.md) and [HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in the [style guide](StyleGuide.md). `````` Jacques-Henri Jourdan committed Sep 13, 2019 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 ``````## Order of `Requires` In Coq, declarations in modules imported later may override the previous definition. Therefore, in order to make sure the most relevant declarations and notations always take priority, we recommend importing dependencies from the furthest to the closest. In particular, when importing Iris, Stdpp and Coq stdlib modules, we recommend importing in the following order: - Coq - stdpp - iris.bi - iris.proofmode - iris.algebra - iris.base_logic - iris.program_logic - iris.heap_lang `````` Robbert Krebbers committed Jun 04, 2019 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 ``````## Combinators for functors In Iris, the type of propositions [iProp] is described by the solution to the recursive domain equation: ``` iProp ≅ uPred (F (iProp)) ``` Here, `F` is a user-chosen locally contractive bifunctor from COFEs to unital Camaras (a step-indexed generalization of unital resource algebras). To make it convenient to construct such functors out of smaller pieces, we provide a number of abstractions: - [`cFunctor`](theories/algebra/ofe.v): bifunctors from COFEs to OFEs. - [`rFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to cameras. - [`urFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to unital cameras. Besides, there are the classes `cFunctorContractive`, `rFunctorContractive`, and `urFunctorContractive` which describe the subset of the above functors that are contractive. To compose these functors, we provide a number of combinators, e.g.: - `constCF (A : ofeT) : cFunctor := λ (B,B⁻), A ` - `idCF : cFunctor := λ (B,B⁻), B` - `prodCF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻)` - `ofe_morCF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻)` - `laterCF (F : cFunctor) : cFunctor := λ (B,B⁻), later (F (B,B⁻))` - `agreeRF (F : cFunctor) : rFunctor := λ (B,B⁻), agree (F (B,B⁻))` - `gmapURF K (F : rFunctor) : urFunctor := λ (B,B⁻), gmap K (F (B,B⁻))` Using these combinators, one can easily construct bigger functors in point-free style, e.g: ``` F := gmapURF K (agreeRF (prodCF (constCF natC) (laterCF idCF))) ``` which effectively defines `F := λ (B,B⁻), gmap K (agree (nat * later B))`. Furthermore, for functors written using these combinators like the functor `F` above, Coq can automatically `urFunctorContractive F`. To make it a little bit more convenient to write down such functors, we make the constant functors (`constCF`, `constRF`, and `constURF`) a coercion, and provide the usual notation for products, etc. So the above functor can be written as follows (which is similar to the effective definition of `F` above): ``` F := gmapURF K (agreeRF (natC * ▶ ∙)) ``` `````` Ralf Jung committed Mar 13, 2019 81 82 83 84 85 ``````## Resource algebra management When using ghost state in Iris, you have to make sure that the resource algebras you need are actually available. Every Iris proof is carried out using a universally quantified list `Σ: gFunctors` defining which resource algebras are `````` Ralf Jung committed Jun 04, 2019 86 87 88 89 90 91 92 ``````available. The `Σ` is the *global* list of resources that the entire proof can use. We keep the `Σ` universally quantified to enable composition of proofs. You can think of this as a list of resource algebras, though in reality it is a list of locally contractive functors from COFEs to Cameras. This list is used to define the parameter `F` of Iris mentioned in the previous section. The formal side of this is described in §7.4 of `````` Ralf Jung committed Mar 13, 2019 93 ``````[The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.1.pdf); here we `````` Ralf Jung committed Jun 04, 2019 94 ``````describe the user-side Coq aspects of this approach. `````` Ralf Jung committed Mar 13, 2019 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 `````` The assumptions that an Iris proof makes are collected in a type class called `somethingG`. The most common kind of assumptions is `inG`, which says that a particular resource algebra is available for ghost state. For example, in the [one-shot example](tests/one_shot.v): ``` Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }. ``` The `:>` means that the projection `one_shot_inG` is automatically registered as an instance for type-class resolution. If you need several resource algebras, just add more `inG` fields. If you are using another module as part of yours, add a field like `one_shot_other :> otherG Σ`. Having defined the type class, we need to provide a way to instantiate it. This is an important step, as not every resource algebra can actually be used: if your resource algebra refers to `Σ`, the definition becomes recursive. That is actually legal under some conditions (which is why the global list `Σ` contains functors and not just resource algebras), but for the purpose of this guide we will ignore that case. We have to define a list that contains all the resource algebras we need: ``` Definition one_shotΣ : gFunctors := #[GFunctor one_shotR]. ``` This time, there is no `Σ` in the context, so we cannot accidentally introduce a bad dependency. If you are using another module as part of yours, add their `somethingΣ` to yours, as in `#[GFunctor one_shotR; somethingΣ]`. (The `#[F1; F2; ...]` syntax *appends* the functor lists `F1`, `F2`, ... to each other; together with a coercion from a single functor to a singleton list, this means lists can be nested arbitrarily.) Now we can define the one and only instance that our type class will ever need: ``` Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ. Proof. solve_inG. Qed. ``` The `subG` assumption here says that the list `one_shotΣ` is a sublist of the global list `Σ`. Typically, this should be the only assumption your instance needs, showing that the assumptions of the module (and all the modules it uses internally) can trivially be satisfied by picking the right `Σ`. Now you can add `one_shotG` as an assumption to all your module definitions and proofs. We typically use a section for this: ``` Section proof. Context `{!heapG Σ, !one_shotG Σ}. ``` Notice that besides our own assumptions `one_shotG`, we also assume `heapG`, which are assumptions that every HeapLang proof makes (they are related to defining the `↦` connective as well as the basic Iris infrastructure for invariants and WP). For this purpose, `heapG` contains not only assumptions about `Σ`, it also contains some ghost names to refer to particular ghost state (see "global ghost state instances" below). The backtic (`` ` ``) is used to make anonymous assumptions and to automatically generalize the `Σ`. When adding assumptions with backtic, you should most of the time also add a `!` in front of every assumption. If you do not then Coq will also automatically generalize all indices of type-classes that you are assuming. This can easily lead to making more assumptions than you are aware of, and often it leads to duplicate assumptions which breaks type class resolutions. ### Obtaining a closed proof To obtain a closed Iris proof, i.e., a proof that does not make assumptions like `inG`, you have to assemble a list of functors of all the involved modules, and if your proof relies on some singleton (most do, at least indirectly; also see the next section), you have to call the respective initialization or adequacy lemma. [For example](tests/one_shot.v): ``` Section client. Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}. Lemma client_safe : WP client {{ _, True }}%I. (* ... *) End client. (** Assemble all functors needed by the [client_safe] proof. *) Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ]. (** Apply [heap_adequacy] with this list of all functors. *) Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True). Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed. ``` ### Advanced topic: Ghost state singletons Some Iris modules involve a form of "global state". For example, defining the `↦` for HeapLang involves a piece of ghost state that matches the current physical heap. The `gname` of that ghost state must be picked once when the proof starts, and then globally known everywhere. Hence it is added to `gen_heapG`, the type class for the generalized heap module: ``` Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := { gen_heap_inG :> inG Σ (authR (gen_heapUR L V)); gen_heap_name : gname }. ``` Such modules always need some kind of "initialization" to create an instance of their type class. For example, the initialization for `heapG` is happening as part of [`heap_adequacy`](theories/heap_lang/adequacy.v); this in turn uses the initialization lemma for `gen_heapG` from [`gen_heap_init`](theories/base_logic/lib/gen_heap.v): ``` Lemma gen_heap_init `{gen_heapPreG L V Σ} σ : (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I. ``` These lemmas themselves only make assumptions the way normal modules (those without global state) do, which are typically collected in a `somethingPreG` type class (such as `gen_heapPreG`): ``` Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := { gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }. ``` Just like in the normal case, `somethingPreG` type classes have an `Instance` showing that a `subG` is enough to instantiate them: ``` Instance subG_gen_heapPreG {Σ L V} `{Countable L} : subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ. Proof. solve_inG. Qed. ``` The initialization lemma then shows that the `somethingPreG` type class is enough to create an instance of the main `somethingG` class *below a view shift*. This is written with an existential quantifier in the lemma because the statement after the view shift (`gen_heap_ctx σ` in this case) depends on having an instance of `gen_heapG` in the context. Given that these global ghost state instances are singletons, they must be assumed explicitly everywhere. Bundling `heapG` in a module type class like `one_shotG` would lose track of the fact that there exists just one `heapG` instance that is shared by everyone. ### Advanced topic: Additional module assumptions Some modules need additional assumptions. For example, the STS module is parameterized by an STS and assumes that the STS state space is inhabited: ``` Class stsG Σ (sts : stsT) := { sts_inG :> inG Σ (stsR sts); sts_inhabited :> Inhabited (sts.state sts); }. ``` In this rather exceptional case, the `Instance` for this class has more than just a `subG` assumption: ``` Instance subG_stsΣ Σ sts : subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts. ``` If users of this module follow the pattern described above, their own type class instance will check these additional assumption. But this is one more reason why it is important for every module to have an instance for its `somethingG`: to make sure that it does not accidentally make more assumptions than it intends to. Another subtle detail here is that the `subG` assumption comes first in `subG_stsΣ`, i.e., it appears before the `Inhabited`. This is important because otherwise, `sts_inhabited` and `subG_stsΣ` form an instance cycle that makes type class search diverge. ## Canonical structures and type classes In Iris, we use both canonical structures and type classes, and some careful tweaking is necessary to make the two work together properly. The details of this still need to be written up properly, but here is some background material: * [Type Classes for Mathematics in Type Theory](http://www.eelis.net/research/math-classes/mscs.pdf) * [Canonical Structures for the working Coq user](https://hal.inria.fr/hal-00816703v1/document)``````