Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
George Pirlea
Iris
Commits
42eb5ad3
Commit
42eb5ad3
authored
Feb 18, 2019
by
Ralf Jung
Browse files
Merge branch 'ralf/wp_par' into 'master'
make wp_par usable See merge request
iris/iris!210
parents
8da58b7f
e5c727d8
Changes
6
Show whitespace changes
Inline
Sidebyside
Showing
6 changed files
with
141 additions
and
3 deletions
+141
3
HeapLang.md
HeapLang.md
+130
0
ProofMode.md
ProofMode.md
+5
0
README.md
README.md
+2
0
theories/heap_lang/lib/coin_flip.v
theories/heap_lang/lib/coin_flip.v
+1
1
theories/heap_lang/lib/increment.v
theories/heap_lang/lib/increment.v
+1
1
theories/heap_lang/lib/par.v
theories/heap_lang/lib/par.v
+2
1
No files found.
HeapLang.md
0 → 100644
View file @
42eb5ad3
# 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 lambdacalculus with operations to allocate individual locations,
`load`
,
`store`
,
`CAS`
(compareandswap) and
`FAA`
(fetchandadd). 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.
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
(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 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 shorthands, such as nonrecursive functions (
`λ:`
),
letbindings, 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 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 }}`
.
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 letbinding 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 pointsto 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 pointsto
assertion in the spatial context, and fails if it cannot be found.

`wp_store`
: Reduce a store operation. This automatically finds the pointsto
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 pointsto 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 pointsto 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 pointsto assertion.
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 nonrecursive 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.mpisws.org/iris/iris/merge_requests/210#note_32842
ProofMode.md
View file @
42eb5ad3
...
@@ 335,3 +335,8 @@ Proof mode terms can be written down using the following shorthand syntaxes, too
...
@@ 335,3 +335,8 @@ Proof mode terms can be written down using the following shorthand syntaxes, too
(H $! t1 ... tn)
(H $! t1 ... tn)
H
H
HeapLang tactics
================
If you came here looking for the
`wp_`
tactics, those are described in the
[
HeapLang documentation
](
HeapLang.md
)
.
README.md
View file @
42eb5ad3
...
@@ 114,6 +114,8 @@ that should be compatible with this version:
...
@@ 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
*
Information on how to set up your editor for unicode input and output is
collected in
[
Editor.md
](
Editor.md
)
.
collected in
[
Editor.md
](
Editor.md
)
.
*
The Iris Proof Mode (IPM) / MoSeL is documented at
[
ProofMode.md
](
ProofMode.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
)
.
*
Naming conventions are documented at
[
Naming.md
](
Naming.md
)
.
*
The generated coqdoc is
[
available online
](
https://plv.mpisws.org/coqdoc/iris/
)
.
*
The generated coqdoc is
[
available online
](
https://plv.mpisws.org/coqdoc/iris/
)
.
*
Discussion about the Iris Coq development happens on the mailing list
*
Discussion about the Iris Coq development happens on the mailing list
...
...
theories/heap_lang/lib/coin_flip.v
View file @
42eb5ad3
From
iris
.
base_logic
.
lib
Require
Export
invariants
.
From
iris
.
base_logic
.
lib
Require
Export
invariants
.
From
iris
.
program_logic
Require
Export
atomic
.
From
iris
.
program_logic
Require
Export
atomic
.
From
iris
.
proofmode
Require
Import
tactics
.
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"
.
Set
Default
Proof
Using
"Type"
.
(** Nondeterminism and Speculation:
(** Nondeterminism and Speculation:
...
...
theories/heap_lang/lib/increment.v
View file @
42eb5ad3
...
@@ 155,7 +155,7 @@ Section increment_client.
...
@@ 155,7 +155,7 @@ Section increment_client.
(* The continuation: From after the atomic triple to the postcondition of the WP *)
(* The continuation: From after the atomic triple to the postcondition of the WP *)
done
.
done
.
}
}
wp_apply
par
_spec
;
wp_pures
.
wp_apply
wp_
par
.

iAssumption
.

iAssumption
.

iAssumption
.

iAssumption
.

iIntros
(??)
"_ !>"
.
done
.

iIntros
(??)
"_ !>"
.
done
.
...
...
theories/heap_lang/lib/par.v
View file @
42eb5ad3
...
@@ 12,6 +12,7 @@ Definition par : val :=
...
@@ 12,6 +12,7 @@ Definition par : val :=
let
:
"v1"
:
=
join
"handle"
in
let
:
"v1"
:
=
join
"handle"
in
(
"v1"
,
"v2"
).
(
"v1"
,
"v2"
).
Notation
"e1  e2"
:
=
(
par
(
λ
:
<>,
e1
)%
E
(
λ
:
<>,
e2
)%
E
)
:
expr_scope
.
Notation
"e1  e2"
:
=
(
par
(
λ
:
<>,
e1
)%
E
(
λ
:
<>,
e2
)%
E
)
:
expr_scope
.
Notation
"e1  e2"
:
=
(
par
(
λ
:
<>,
e1
)%
V
(
λ
:
<>,
e2
)%
V
)
:
val_scope
.
Section
proof
.
Section
proof
.
Local
Set
Default
Proof
Using
"Type*"
.
Local
Set
Default
Proof
Using
"Type*"
.
...
@@ 37,7 +38,7 @@ Qed.
...
@@ 37,7 +38,7 @@ Qed.
Lemma
wp_par
(
Ψ
1
Ψ
2
:
val
→
iProp
Σ
)
(
e1
e2
:
expr
)
(
Φ
:
val
→
iProp
Σ
)
:
Lemma
wp_par
(
Ψ
1
Ψ
2
:
val
→
iProp
Σ
)
(
e1
e2
:
expr
)
(
Φ
:
val
→
iProp
Σ
)
:
WP
e1
{{
Ψ
1
}}

∗
WP
e2
{{
Ψ
2
}}

∗
WP
e1
{{
Ψ
1
}}

∗
WP
e2
{{
Ψ
2
}}

∗
(
∀
v1
v2
,
Ψ
1
v1
∗
Ψ
2
v2

∗
▷
Φ
(
v1
,
v2
)%
V
)

∗
(
∀
v1
v2
,
Ψ
1
v1
∗
Ψ
2
v2

∗
▷
Φ
(
v1
,
v2
)%
V
)

∗
WP
e1

e2
{{
Φ
}}.
WP
(
e1

e2
)%
V
{{
Φ
}}.
Proof
.
Proof
.
iIntros
"H1 H2 H"
.
iIntros
"H1 H2 H"
.
wp_apply
(
par_spec
Ψ
1
Ψ
2
with
"[H1] [H2] [H]"
)
;
[
by
wp_lam
..
auto
].
wp_apply
(
par_spec
Ψ
1
Ψ
2
with
"[H1] [H2] [H]"
)
;
[
by
wp_lam
..
auto
].
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment