From c1449e94c9c1f8aceafe9a704efb84e1b73f90d4 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Thu, 24 Jan 2019 22:05:02 +0100
Subject: [PATCH 1/4] make wp_par usable
---
theories/heap_lang/lib/increment.v | 2 +-
theories/heap_lang/lib/par.v | 4 +++-
2 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index 79f600e20..5b4c6129f 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -155,7 +155,7 @@ Section increment_client.
(* The continuation: From after the atomic triple to the postcondition of the WP *)
done.
}
- wp_apply par_spec; wp_pures.
+ wp_apply wp_par.
- iAssumption.
- iAssumption.
- iIntros (??) "_ !>". done.
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 5fd18ec3f..0d55d3a4b 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -12,6 +12,8 @@ Definition par : val :=
let: "v1" := join "handle" in
("v1", "v2").
Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
+(* Not a value itself, but with *unlocked* value lambdas. *)
+Local Notation "e1 ||| e2" := (par (LamV BAnon e1%E) (LamV BAnon e2%E)) : val_scope.
Section proof.
Local Set Default Proof Using "Type*".
@@ -37,7 +39,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 e1 ||| 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
From 49b0451545856d67b32c3a8ee5fb940157988f2a Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Thu, 24 Jan 2019 22:11:09 +0100
Subject: [PATCH 2/4] avoid non-value notation in val_scope
---
theories/heap_lang/lib/coin_flip.v | 2 +-
theories/heap_lang/lib/par.v | 4 +---
2 files changed, 2 insertions(+), 4 deletions(-)
diff --git a/theories/heap_lang/lib/coin_flip.v b/theories/heap_lang/lib/coin_flip.v
index 57b085436..7e3569b1e 100644
--- a/theories/heap_lang/lib/coin_flip.v
+++ b/theories/heap_lang/lib/coin_flip.v
@@ -1,7 +1,7 @@
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation par.
+From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(** Nondeterminism and Speculation:
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 0d55d3a4b..34c6ad2e7 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -12,8 +12,6 @@ Definition par : val :=
let: "v1" := join "handle" in
("v1", "v2").
Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
-(* Not a value itself, but with *unlocked* value lambdas. *)
-Local Notation "e1 ||| e2" := (par (LamV BAnon e1%E) (LamV BAnon e2%E)) : val_scope.
Section proof.
Local Set Default Proof Using "Type*".
@@ -39,7 +37,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 (e1 ||| e2)%V {{ Φ }}.
+ WP par (LamV BAnon e1) (LamV BAnon e2) {{ Φ }}.
Proof.
iIntros "H1 H2 H".
wp_apply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); [by wp_lam..|auto].
--
GitLab
From 38dbbf59ca981151a847009687c4c51424af2437 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Sat, 16 Feb 2019 14:24:32 +0100
Subject: [PATCH 3/4] 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
From e5c727d82bac64552ad43e7744d1d7bcb5996a81 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Mon, 18 Feb 2019 09:20:50 +0100
Subject: [PATCH 4/4] apply feedback
---
HeapLang.md | 29 +++++++++++++++--------------
1 file changed, 15 insertions(+), 14 deletions(-)
diff --git a/HeapLang.md b/HeapLang.md
index c1c23449e..0ac3a23b9 100644
--- a/HeapLang.md
+++ b/HeapLang.md
@@ -9,10 +9,11 @@ language for simple examples.
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.
+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.
+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.
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
@@ -20,8 +21,8 @@ begin with the `Val` expression former. This means that, for example, `Pair
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
+However, this also makes values 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,
@@ -47,7 +48,7 @@ eagerly.
## Tactics
-HeapLang coms with a bunch of tactics that facilitate stepping through HeaLang
+HeapLang comes with a bunch of tactics that facilitate stepping through HeapLang
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 }}`.
@@ -72,22 +73,22 @@ Tactics to take one or more pure program steps:
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
+ location `l` (in the Coq context) and the points-to assertion `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_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.
- `wp_cas_suc`, `wp_cas_fail`: Reduce a succeeding/failing CAS. This
- automatically finds the necessary ownership. It also automatically tries to
+ automatically finds the points-to assertion. 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
+ it succeeds or fails. This automatically finds the points-to assertion. 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.
+- `wp_faa`: Reduce a FAA. This automatically finds the points-to assertion.
Further tactics:
--
GitLab