From 38dbbf59ca981151a847009687c4c51424af2437 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 16 Feb 2019 14:24:32 +0100
Subject: [PATCH] document parts of HeapLang and, in particular, what we are
 doing with the thunk-related notations

---
 HeapLang.md                  | 129 +++++++++++++++++++++++++++++++++++
 ProofMode.md                 |   5 ++
 README.md                    |   2 +
 theories/heap_lang/lib/par.v |   3 +-
 4 files changed, 138 insertions(+), 1 deletion(-)
 create mode 100644 HeapLang.md

diff --git a/HeapLang.md b/HeapLang.md
new file mode 100644
index 000000000..c1c23449e
--- /dev/null
+++ b/HeapLang.md
@@ -0,0 +1,129 @@
+# 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
+integers, booleans, unit, heap locations as well as (binary) sums and products.
+
+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.
+
+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.
+
+However, this also makes values very syntactically uniform, which we exploit in
+the definition of substitution which just skips over `Val` terms, because values
+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.
+
+Noteworthy is the fact that functions (`rec:`, `λ:`) in the value scope (`%V`)
+are *locked*.  This is to prevent them from being unfolded and reduced too
+eagerly.
+
+## Tactics
+
+HeapLang coms with a bunch of tactics that facilitate stepping through HeaLang
+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.
+- `wp_pures`: Perform as many pure reduction steps as possible.
+- `wp_rec`, `wp_lam`: Perform a beta reduction.  Unlike `wp_pure`, this will
+  also reduce locked lambdas.
+- `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
+  location `l` (in the Coq context) and the assertion that we own it `H` (in the
+  spatial context).  You can leave away the `as "H"` to introduce it as an
+  anonymous assertion, i.e., that is equivalent to `as "?"`.
+- `wp_load`: Reduce a load operation.  This automatically finds the necessary
+  ownership in the spatial context, and fails if it cannot be found.
+- `wp_store`: Reduce a store operation.  This automatically finds the necessary
+  ownership in the spatial context, and fails if it cannot be found.
+- `wp_cas_suc`, `wp_cas_fail`: Reduce a succeeding/failing CAS.  This
+  automatically finds the necessary ownership.  It also automatically tries to
+  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
+  it succeeds or fails.  This automatically finds the necessary ownership.  The
+  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`.
+- `wp_faa`: Reduce a FAA.  This automatically finds the necessary ownership.
+
+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
+`e1 ||| e2` notation in the value scope that uses value lambdas.  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.
+
+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
diff --git a/ProofMode.md b/ProofMode.md
index a6446801c..b165c01a5 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -335,3 +335,8 @@ Proof mode terms can be written down using the following shorthand syntaxes, too
         (H $! t1 ... tn)
         H
 
+HeapLang tactics
+================
+
+If you came here looking for the `wp_` tactics, those are described in the
+[HeapLang documentation](HeapLang.md).
diff --git a/README.md b/README.md
index aa81a7c3e..b99d813d2 100644
--- a/README.md
+++ b/README.md
@@ -114,6 +114,8 @@ that should be compatible with this version:
 * Information on how to set up your editor for unicode input and output is
   collected in [Editor.md](Editor.md).
 * The Iris Proof Mode (IPM) / MoSeL is documented at [ProofMode.md](ProofMode.md).
+* HeapLang (the Iris example language) and its tactics are documented at
+  [HeapLang.md](HeapLang.md).
 * Naming conventions are documented at [Naming.md](Naming.md).
 * The generated coqdoc is [available online](https://plv.mpi-sws.org/coqdoc/iris/).
 * Discussion about the Iris Coq development happens on the mailing list
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 34c6ad2e7..558853f4f 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -12,6 +12,7 @@ Definition par : val :=
     let: "v1" := join "handle" in
     ("v1", "v2").
 Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
+Notation "e1 ||| e2" := (par (λ: <>, e1)%V (λ: <>, e2)%V) : val_scope.
 
 Section proof.
 Local Set Default Proof Using "Type*".
@@ -37,7 +38,7 @@ Qed.
 Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) (Φ : val → iProp Σ) :
   WP e1 {{ Ψ1 }} -∗ WP e2 {{ Ψ2 }} -∗
   (∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
-  WP par (LamV BAnon e1) (LamV BAnon e2) {{ Φ }}.
+  WP (e1 ||| e2)%V {{ Φ }}.
 Proof.
   iIntros "H1 H2 H".
   wp_apply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); [by wp_lam..|auto].
-- 
GitLab