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, CmpXchg (compare-and-exchange) 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.
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. 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.