HeapLang.md 6.91 KB
 1 2 3 4 5 6 7 8 9 10 11 ``````# HeapLang overview HeapLang is the example language that gets shipped with Iris. It is not the only language you can reason about with Iris, but meant as a reasonable demo language for simple examples. ## Language HeapLang is a lambda-calculus with operations to allocate individual locations, `load`, `store`, `CAS` (compare-and-swap) and `FAA` (fetch-and-add). Moreover, it has a `fork` construct to spawn new threads. In terms of values, we have `````` Ralf Jung committed Feb 18, 2019 12 ``````integers, booleans, unit, heap locations, as well as (binary) sums and products. `````` 13 `````` `````` Ralf Jung committed Feb 18, 2019 14 15 16 ``````Recursive functions are the only binders, so the sum elimination (`Case`) expects both branches to be of function type and passes them the data component of the sum. `````` 17 18 19 20 21 22 23 `````` For technical reasons, the only terms that are considered values are those that begin with the `Val` expression former. This means that, for example, `Pair (Val a) (Val b)` is *not* a value -- it reduces to `Val (PairV a b)`, which is. This leads to some administrative redexes, and to a distinction between "value pairs", "value sums", "value closures" and their "expression" counterparts. `````` Ralf Jung committed Feb 18, 2019 24 25 ``````However, this also makes values syntactically uniform, which we exploit in the definition of substitution which just skips over `Val` terms, because values `````` 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 ``````should be closed and hence not affected by substitution. As a consequence, we can entirely avoid even talking about "closed terms", that notion just does not have to come up anywhere. We also exploit this when writing specifications, because we can just write lemmas involving terms of the form `Val ?v` and Coq can determine `?v` by unification (because all values start with the `Val` constructor). ## Notation Notation for writing HeapLang terms is defined in [`notation.v`](theories/heap_lang/notation.v). There are two scopes, `%E` for expressions and `%V` for values. For example, `(a, b)%E` is an expression pair and `(a, b)%V` a value pair. The `e` of a `WP e {{ Q }}` is implicitly in `%E` scope. We define a whole lot of short-hands, such as non-recursive functions (`λ:`), let-bindings, sequential composition, and a more conventional `match:` that has binders in both branches. `````` Ralf Jung committed Feb 26, 2019 45 46 47 48 49 ``````The widely used `#` is a short-hand to turn a basic literal (an integer, a location, a boolean literal or a unit value) into a value. Since values coerce to expressions, `#` is widely used whenever a Coq value needs to be placed into a HeapLang term. `````` 50 51 ``````## Tactics `````` Ralf Jung committed Feb 18, 2019 52 ``````HeapLang comes with a bunch of tactics that facilitate stepping through HeapLang `````` 53 54 55 56 57 58 59 60 ``````programs as part of proving a weakest precondition. All of these tactics assume that the current goal is of the shape `WP e @ E {{ Q }}`. Tactics to take one or more pure program steps: - `wp_pure`: Perform one pure reduction step. Pure steps are defined by the `PureExec` typeclass and include beta reduction, projections, constructors, as well as unary and binary arithmetic operators. `````` Robbert Krebbers committed Mar 14, 2019 61 62 ``````- `wp_pures`: Perform as many pure reduction steps as possible. This tactic will **not** reduce lambdas/recs that are hidden behind a definition. `````` 63 ``````- `wp_rec`, `wp_lam`: Perform a beta reduction. Unlike `wp_pure`, this will `````` Robbert Krebbers committed Mar 14, 2019 64 `````` also reduce lambdas that are hidden behind a definition. `````` 65 66 67 68 69 70 71 72 73 74 75 76 77 ``````- `wp_let`, `wp_seq`: Reduce a let-binding or a sequential composition. - `wp_proj`: Reduce a projection. - `wp_if_true`, `wp_if_false`, `wp_if`: Reduce a conditional expression. The discriminant must already be `true` or `false`. - `wp_unop`, `wp_binop`, `wp_op`: Reduce a unary, binary or either kind of arithmetic operator. - `wp_case`, `wp_match`: Reduce `Case`/`match:` constructs. - `wp_inj`, `wp_pair`, `wp_closure`: Reduce constructors that turn expression sums/pairs/closures into their value counterpart. Tactics for the heap: - `wp_alloc l as "H"`: Reduce an allocation instruction and call the new `````` Ralf Jung committed Feb 18, 2019 78 `````` location `l` (in the Coq context) and the points-to assertion `H` (in the `````` 79 80 `````` spatial context). You can leave away the `as "H"` to introduce it as an anonymous assertion, i.e., that is equivalent to `as "?"`. `````` Ralf Jung committed Feb 18, 2019 81 82 83 84 ``````- `wp_load`: Reduce a load operation. This automatically finds the points-to assertion in the spatial context, and fails if it cannot be found. - `wp_store`: Reduce a store operation. This automatically finds the points-to assertion in the spatial context, and fails if it cannot be found. `````` 85 ``````- `wp_cas_suc`, `wp_cas_fail`: Reduce a succeeding/failing CAS. This `````` Ralf Jung committed Feb 18, 2019 86 `````` automatically finds the points-to assertion. It also automatically tries to `````` 87 88 89 `````` solve the (in)equality to show that the CAS succeeds/fails, and opens a new goal if it cannot prove this goal. - `wp_cas as H1 | H2`: Reduce a CAS, performing a case distinction over whether `````` Ralf Jung committed Feb 18, 2019 90 `````` it succeeds or fails. This automatically finds the points-to assertion. The `````` 91 92 `````` proof of equality in the first new subgoal will be called `H1`, and the proof of the inequality in the second new subgoal will be called `H2`. `````` Ralf Jung committed Feb 18, 2019 93 ``````- `wp_faa`: Reduce a FAA. This automatically finds the points-to assertion. `````` 94 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 `````` Further tactics: - `wp_bind pat`: Apply the bind rule to "focus" the term matching `pat`. For example, `wp_bind (!_)%E` focuses a load operation. This is useful in particular when accessing invariants, which is only possible when the `WP` in the goal is for a single, atomic operation -- `wp_bind` can be used to bring the goal into the right shape. - `wp_apply pm_trm`: Apply a lemma whose conclusion is a `WP`, automatically applying `wp_bind` as needed. See the [ProofMode docs](ProofMode.md) for an explanation of `pm_trm`. There is no tactic for `Fork`, just do `wp_apply wp_fork`. ## Notation and lemmas for derived notions involving a thunk Sometimes, it is useful to define a derived notion in HeapLang that involves thunks. For example, the parallel composition `e1 ||| e2` is defineable in HeapLang, but that requires thunking `e1` and `e2` before passing them to `par`. (This is defined in [`par.v`](theories/heap_lang/lib/par.v).) However, this is somewhat subtle because of the distinction between expression lambdas and value lambdas. The normal `e1 ||| e2` notation uses expression lambdas, because clearly we want `e1` and `e2` to behave normal under substitution (which they would not in a value lambda). However, the *specification* for parallel composition should use value lambdas, because prior to applying it the term will be reduced as much as possible to achieve a normal form. To facilitate this, we define a copy of the `````` Robbert Krebbers committed Mar 14, 2019 122 ```````e1 ||| e2` notation in the value scope that uses value lambdas. `````` Ralf Jung committed Feb 18, 2019 123 124 125 126 ``````This is not actually a value, but we still but it in the value scope to differentiate from the other notation that uses expression lambdas. (In the future, we might decide to add a separate scope for this.) Then, we write the canonical specification using the notation in the value scope. `````` 127 128 129 130 131 132 `````` This works very well for non-recursive notions. For `while` loops, the situation is unfortunately more complex and proving the desired specification will likely be more involved than expected, see this [discussion]. [discussion]: https://gitlab.mpi-sws.org/iris/iris/merge_requests/210#note_32842``````