A brief introduction to Iris
Posted by tutorial. Suggest edits or corrections.
on Fri 26 June 2020 inIris is a powerful framework for doing concurrency reasoning. In the PDOS group we've been using it to verify concurrent storage systems, including reasoning about code implemented in Go. Iris stands out among concurrency frameworks in my mind for two reasons: it is extremely modular, allowing us to adapt it to a setting quite different from its original purposes; and it is extremely well-engineered, allowing us to work with it as a library rather than re-implement it. Iris stands out, especially among Coq frameworks, for how usable it is.
Iris is also, unfortunately, a beast to learn. It can be hard to tell where to start, hard to figure out what Iris even is, and hard to appreciate why Iris is such a good framework. In this post we'll work through a sort of "hello, world" example of concurrency verification, proving it correct in Iris. My goal is to convince you that the underlying ideas are approachable and get you excited about Iris; if I succeed then you'll walk away appreciating Iris a bit more and maybe be curious enough to dive deeper into other material.
I'm explicitly not aiming to teach you how to do these proofs on your own - I give some resources at the bottom of the post if you want to go further and really learn how to use Iris.
This post will assume some knowledge of Hoare logic and Coq (if you want to follow the proofs). The intention is that even if some of the separation logic details don't make sense the intuition still comes through. Iris is built on top of separation logic, though, so to really understand it you do need some understanding of at least sequential separation logic.
A simple proof about a bank
In this post we'll implement a sort of bank that stores user balances and allows transfers between accounts. We want to show that in some sense transfers preserve the sum of balances.
First, let's make a few drastic simplifications to focus on the essential difficulty: we'll only have two accounts, and only transfer from one to the other. The balances will be represented as mathematical integers Z and their sum will be 0. We won't try executing this code, only proving it correct.
What's left is that we will still have a lock per account, acquiring both locks to do a transfer. This still leaves a difficulty that the balances don't necessarily sum to zero at every instant in time (for example, they might not while a transfer is in progress); however, if we acquire both account locks, we should observe a sum of 0. Thus we'll write a function that acquires both locks and checks that the sum is zero. If we had more accounts, this check would have to acquire all of the locks.
We won't prove anything else about the bank functionality or implement anything else (like reading balances).
First, we'll import some stuff from Iris.
(* we'll use this library to set up ghost state later *) From iris.algebra Require Import lib.excl_auth. From iris.heap_lang Require Import proofmode notation. From iris.heap_lang.lib Require Import lock spin_lock.
Implementing the bank
In this post, we'll implement the bank in HeapLang, a simple default language for Iris. HeapLang is a core functional language with mutable references that we can write directly from Coq, with a set of notations to make the syntax readable.
We'll write HeapLang functions as Coq definitions of type
val
, which is a HeapLang value.Variables are represented as strings (and thus need to be quoted everywhere).
ref x
allocates a new reference with an initial valuex
.#x
is overloaded to turnx
into a value; we'll use it for integers (Z
in Coq) and for the unit literal#()
.!l
dereferences a pointer l ("l" stands for "location").Many constructs have a colon to disambiguate them from the analogous Coq syntax, such as
let:
andλ:
λ: <>, ...
uses <> for an anonymous binder, much like_
in Coq and other languages.This language has no static type system.
First we'll write a function to create a new bank. new_bank
constructs a bank
with two accounts that both have zero balance, which initially satisfies the
desired invariant.
Definition new_bank: val :=
λ: <>,
let: "a_bal" := ref #0 in
let: "b_bal" := ref #0 in
let: "lk_a" := newlock #() in
let: "lk_b" := newlock #() in
(* the bank is represented as a pair of accounts, each of
which is a pair of a lock and a pointer to its balance *)
(("lk_a", "a_bal"), ("lk_b", "b_bal")).
transfer
moves money from the first to the second account (there's no check
that there's enough money, and we totally allow negative balances). We want to
prove this function is safe, but we won't prove that it actually modifies the
bank state correctly because that would require more setup. Note that we need to
be consistent about lock acquisition order to avoid the possibility of a
deadlock; proofs in Iris do not show that code terminates and hence deadlocks
are possible even for verified code.
Definition transfer: val :=
λ: "bank" "amt",
let: "a" := Fst "bank" in
let: "b" := Snd "bank" in
acquire (Fst "a");;
acquire (Fst "b");;
Snd "a" <- !(Snd "a") - "amt";;
Snd "b" <- !(Snd "b") + "amt";;
release (Fst "b");;
release (Fst "a");;
#().
check_consistency
is the core function of interest: we'll eventually prove
that even in the presence of transfer
's, this function always returns true.
Definition check_consistency: val :=
λ: "bank",
let: "a" := Fst "bank" in
let: "b" := Snd "bank" in
acquire (Fst "a");;
acquire (Fst "b");;
let: "a_bal" := !(Snd "a") in
let: "b_bal" := !(Snd "b") in
let: "ok" := "a_bal" + "b_bal" = #0 in
release (Fst "b");;
release (Fst "a");;
"ok".
To tie everything together we'll specifically prove that the following function
always returns true, which doesn't take any arguments and does all the setup
internally. The semantics of Fork e
are to spawn a new thread running e
, so
the call to check_consistency
will race with transfer
. Nonetheless we'll
still be able to prove the whole function always returns true.
Definition demo_check_consistency: val :=
λ: <>,
let: "bank" := new_bank #() in
Fork (transfer "bank" #5);;
check_consistency "bank".
Proving the bank correct
Before we can prove it correct, I should briefly talk about what the
specification is. To keep things simple, we're going to prove a Hoare triple
that says demo_check_consistency
always returns true. However, it's possible
to prove theorems using Iris whose statement doesn't mention anything in the
Iris logic.
Note
Iris isn't just for proving Hoare triples - it can be used to prove properties of languages with logical relations and refinement theorems. The key is that we can apply the Iris adequacy theorem to derive a theorem that "eliminates" the Iris logic.
For example, if we can prove a Hoare triple whose precondition is true and
whose conclusion is some pure fact φ(v)
about the return value v
,
then if the function runs to a value v
then φ(v)
will indeed hold.
The full adequacy theorem is more powerful than this, giving a way to talk
about the intermediate behaviors of the program as well (something we would
need in order to derive a refinement theorem).
Iris is based on separation logic, specifically a variant called concurrent
separation logic. If you haven't seen separation logic, here's a one-paragraph
summary: separation logic is a way of describing resources. A predicate P
in
separation logic represents a collection of resources, which we'll also describe
as ownership of those resources. When reasoning about programs, a typical
resource that comes up is l ↦ v
, which says pointer l
points to value
v
in memory and represents ownership of that location. A crucial idea of
separation logic is the separating conjunction P ∗ Q
(pronounced "P and
separately Q", or just "P and Q" when you've worked in separation logic long
enough), which represents disjoint ownership of (resources satisfying the
predicate) P
and Q
. The CACM article Separation logic is an excellent and accessible overview.
The syntax it uses for separation logic here includes:
P ∗ Q
(note that's a Unicode symbol) is separating conjunction.P -∗ Q
is separating implication (think of it as P implies Q and just remember that(P -∗ Q) ∗ P ⊢ Q
), sometimes called "magic wand".⌜φ⌝
embeds a "pure" (Coq) propositionφ: Prop
into separation logic∃ (x:T), ...
is overloaded to also work within separation logic. This is so natural you can easily forget that separation logic and Coq exists aren't the same thing.|==> P
is an "update modality" (the|==>
part) around some proposition P, which you might pronounce "an update to P." It's the most complicated thing we'll need and is an innovation of Iris over the original concurrent separation logic. To prove concurrent programs correct, it's necessary in general to introduce "ghost state", state that exists logically in the proof alongside the program execution but doesn't show up in the operational semantics or the running code. This is a resource in Iris that represents the ability to update the ghost state in a way that produces resourcesP
(for example, we'll use a theorem of this form which allows creating new ghost variables). If you like you can mostly ignore this and just imagine that we can always update ghost state, so thatP
and|==> P
are the same thing.
Ghost state
To do this proof we need some simple ghost state. Iris has very general support for user-extensible ghost state. I'll go over the properties of the type of ghost variables we're constructing here, just not how it is constructed from the lower-level primitives.
Ghost state in Iris might be different from what you're used to, if you've seen them in other implementations. Many frameworks (for example, Dafny) have a similar mechanism that involves annotating the source program with ghost variables and ghost code which updates the ghost state. Then, those frameworks need to prove an erasure theorem that shows removing ghost variables doesn't affect the program, since these operations aren't going to be used at runtime. By contrast in Iris the ghost state only shows up in the proof, so there's no need to do any erasure. Instead, Iris has general rules for how ghost state can be created and manipulated that are proven sound once and for all. The one downside is that ghost state and ghost updates are no longer adjacent to the program, but instead show up only as steps in the proof (which we'll see below). However, the flip side is more flexibility, since the updates can depend on state that's only in the proof and not the code.
The ghost state I'll create will have two resources, written own γ (●E a)
and
own γ (◯E a)
, where a:A
is an element of an arbitrary type. The first
one represents "authoritative ownership" and the second one is "fragmentary
ownership," and because this is exclusive ownership (represented by the E),
these two are symmetric. I'll typically pronounce own γ (●E a)
as just "auth
a" and own γ (◯E a)
as "fragment a", leaving everything else implicit (since
this particular ghost state is so common). Generally the auth goes in an
invariant and we hand out the fragment in lock invariants and such. There's also
a ghost name, which uses the metavariable γ
, to name this particular
variable.
We can do three things with this type of ghost state: allocate a pair of them
(at any step in the proof, since this is ghost state), derive that the auth and
fragment agree on the same value, and update the variable if we have both. You
can think about this ghost state as being a variable of type A
which we have
two views of, the auth and the fragment. Both of these views agree because
there's only one underlying value, and together they represent exclusive access
to the variable and hence we can update it if we have both.
We can allocate a new ghost variable, under an update modality because this requires modifying the global ghost state. The proof for this lemma will likely be a bit inscrutable; I'll focus mostly on explaining the program proofs of Hoare triples below, and just try to convey what these lemma statements mean.
A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))a:A.(ofe_car)⊢ |==> ∃ γ : gname, own γ (●E a) ∗ own γ (◯E a)A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))a:A.(ofe_car)⊢ |==> ∃ γ : gname, own γ (●E a) ∗ own γ (◯E a)A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))a:A.(ofe_car)✓ (●E a ⋅ ◯E a)A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))a:A.(ofe_car)γ:gname"H1" : own γ (●E a) "H2" : own γ (◯E a) --------------------------------------∗ |==> ∃ γ0 : gname, own γ0 (●E a) ∗ own γ0 (◯E a)apply excl_auth_valid.A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))a:A.(ofe_car)✓ (●E a ⋅ ◯E a)A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))a:A.(ofe_car)γ:gname"H1" : own γ (●E a) "H2" : own γ (◯E a) --------------------------------------∗ |==> ∃ γ0 : gname, own γ0 (●E a) ∗ own γ0 (◯E a)A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))a:A.(ofe_car)γ:gname"H1" : own γ (●E a) "H2" : own γ (◯E a) --------------------------------------∗ ∃ γ0 : gname, own γ0 (●E a) ∗ own γ0 (◯E a)iFrame. Qed.A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))a:A.(ofe_car)γ:gname"H1" : own γ (●E a) "H2" : own γ (◯E a) --------------------------------------∗ own γ (●E a) ∗ own γ (◯E a)
Now I'll prove that the two parts always agree, written using separating
implication (also pronounced "magic wand" but that obscures its meaning). You
can read -∗
exactly like ->
and you'll basically have the right
intuition.
A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))γ:gnamea1, a2:A.(ofe_car)own γ (●E a1) -∗ own γ (◯E a2) -∗ ⌜a1 = a2⌝A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))γ:gnamea1, a2:A.(ofe_car)own γ (●E a1) -∗ own γ (◯E a2) -∗ ⌜a1 = a2⌝A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))γ:gnamea1, a2:A.(ofe_car)"Hγ1" : own γ (●E a1) "Hγ2" : own γ (◯E a2) --------------------------------------∗ ⌜a1 = a2⌝A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))γ:gnamea1, a2:A.(ofe_car)"H" : ✓ (●E a1 ⋅ ◯E a2) --------------------------------------∗ ⌜a1 = a2⌝done. Qed.A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))γ:gnamea1:A.(ofe_car)--------------------------------------∗ ⌜a1 = a1⌝
Finally I'll prove a theorem that lets us change ghost state. It requires the
right to change ghost state, hence producing a conclusion under |==>
. Unlike
the previous theorem this consumes the old ownership and gives new resources,
having modified the ghost variable. Reading the whole thing, it says we can use an auth and a fragment for a particular variable γ
and update them to an auth and a fragment for some new value a1'
.
A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))γ:gnamea1', a1, a2:A.(ofe_car)own γ (●E a1) -∗ own γ (◯E a2) ==∗ own γ (●E a1') ∗ own γ (◯E a1')A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))γ:gnamea1', a1, a2:A.(ofe_car)own γ (●E a1) -∗ own γ (◯E a2) ==∗ own γ (●E a1') ∗ own γ (◯E a1')A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))γ:gnamea1', a1, a2:A.(ofe_car)"Hγ●" : own γ (●E a1) "Hγ◯" : own γ (◯E a2) --------------------------------------∗ |==> own γ (●E a1') ∗ own γ (◯E a1')A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))γ:gnamea1', a1, a2:A.(ofe_car)●E a1 ⋅ ◯E a2 ~~> ●E a1' ⋅ ◯E a1'A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))γ:gnamea1', a1, a2:A.(ofe_car)--------------------------------------∗ |==> Trueapply excl_auth_update.A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))γ:gnamea1', a1, a2:A.(ofe_car)●E a1 ⋅ ◯E a2 ~~> ●E a1' ⋅ ◯E a1'done. Qed.A:ofeTHequiv:LeibnizEquiv AHdiscrete:OfeDiscrete AΣ:gFunctorsHin:inG Σ (authR (optionUR (exclR A)))γ:gnamea1', a1, a2:A.(ofe_car)--------------------------------------∗ |==> True
It's also true that two auth or fragments for the same ghost name are contradictory, but we don't need that in this particular proof so I won't prove it.
Note
How do you type these funny symbols?
Even if you aren't ready (yet!) to prove things in Iris, you might be wondering how you're supposed to type all of these funny Unicode symbols. You also might think the Iris developers are crazy for such a rich syntax.
I use Emacs, so I type them with a special math input mode. For example, I
can write own \gname (\aaE a1) -\sep own \gname (\afE a1)
to get own γ
(●E a1) -∗ own γ (◯E a1)
. If you're using CoqIDE or VSCode you can set up
fairly similar support; see the Iris editor setup documentation for details.
Unicode syntax sometimes puts people off, but I think it's actually quite helpful. It means Iris code is both more compact and looks closer to mathematical practice (for example, the papers), which makes it much easier to read once you're used to it. Having lots of symbols not used anywhere else also makes it vastly easier to get this code to parse correctly without long sequences of ASCII symbols.
Section heap. (* mostly standard boilerplate *) Context `{!heapG Σ}. Context `{!lockG Σ}. Context `{!inG Σ (ghostR ZO)}. Let N := nroot.@"bank".
We can now talk about iProp Σ
, the type of Iris propositions. This includes
the own
fact we saw above for ghost resources, l ↦ v
for the usual points-to
in HeapLang, and all the separation logic connectives. You can ignore the Σ
,
which is there for technical reasons.
The overall idea of the proof is to use two Z-valued ghost variables to represent the logical balance of each account. These logical balances will always add up to zero. We'll relate the logical balance to the physical balance of an account by requiring them to match up only when the lock is free. This means that upon acquiring both locks, the balances will satisfy the global invariant, and during the transfer operation we're free to let the logical and physical balances get out-of-sync until the operation is done.
Now we just need to implement that in a machine-checked way using Iris!
Setting up the invariants
The first thing we need is a lock invariant for each account's lock. The idea of
lock invariants is that first the proof associates a lock invariant P
to the lock.
When a thread acquires a lock, it get (resources satisfying) P
, and when it releases
it has to give back (resources satisfying) P
. Crucially during the
critical section the thread has access to P
and can violate this proposition
freely. Once a lock invariant is allocated, the resources protected by the lock
are "owned" by the lock and governed through the lock, which is what makes this
specification sound.
account_inv
will be the lock invariant associated with each account. It
exposes a ghost name γ
used to tie the account balance to a ghost variable,
and also takes the location bal_ref
where this account balance is stored.
Definition account_inv γ bal_ref : iProp Σ :=
∃ (bal: Z), bal_ref ↦ #bal ∗ own γ (◯E bal).
An account is a pair of a lock and an account protected by the lock, where
is_lock
associates the lock to the lock invariant written above.
Definition is_account (acct: val) γ : iProp Σ :=
∃ (bal_ref: loc) lk,
⌜acct = (lk, #bal_ref)%V⌝ ∗
(* you can ignore this ghost name for the lock *)
∃ (γl: gname), is_lock γl lk (account_inv γ bal_ref).
bank_inv
is an invariant (the usual one that holds at all intermediate points,
not a lock invariant) that holds the fragments for the account balances and,
importantly, states that the logical balances sum to 0. Any thread can open the
invariant to "read" the logical balances, but modifications must respect the
constraint here.
We need to give names for the logical account balance variables, so this definition also takes two ghost names.
Definition bank_inv (γ: gname * gname) : iProp Σ :=
(* the values in the accounts are arbitrary... *)
∃ (bal1 bal2: Z),
own γ.1 (●E bal1) ∗
own γ.2 (●E bal2) ∗
(* ... except that they add up to 0 *)
⌜(bal1 + bal2)%Z = 0⌝.
Finally is_bank
ties together the per-account and global invariant:
Definition is_bank (b: val): iProp Σ :=
∃ (acct1 acct2: val) (γ: gname*gname),
⌜b = (acct1, acct2)%V⌝ ∗
is_account acct1 γ.1 ∗
is_account acct2 γ.2 ∗
inv N (bank_inv γ).
Importantly is_bank b
is persistent, which means we can share it among
threads. We'll see this used in wp_demo_check_consistency
.
Instance is_bank_Persistent b : Persistent (is_bank b). Proof. apply _. Qed.
This proof was trivial because the components of is_bank
are persistent,
which typeclass resolution can figure out. These include the pure facts (it
should be intuitive that these are persistent, since they don't talk about
resources at all), the invariant (because inv N P
is just knowledge of an
invariant, which can and should be shared) and is_lock γl lk P
(similarly,
this is knowledge that there is a lock at lk and is
shareable)
A specification for new_bank
new_bank
is actually interesting because its proof has to create all the ghost
state, lock invariants, and invariant, and argue these things initially hold.
I won't completely explain how these proofs work but I'll highlight a few
things. The code is fairly simple and can basically be symbolically executed.
The most parts will be related to ghost state. In particular look out for the
iMod
tactic, which "executes" a ghost state change under a |==>
.
Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespace{{{ True }}} new_bank #() {{{ (b : val), RET b; is_bank b }}}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespace{{{ True }}} new_bank #() {{{ (b : val), RET b; is_bank b }}}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σ"HΦ" : ▷ (∀ b : val, is_bank b -∗ Φ b) --------------------------------------∗ WP new_bank #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σ"HΦ" : ∀ b : val, is_bank b -∗ Φ b --------------------------------------∗ WP let: "a_bal" := ref #0 in let: "b_bal" := ref #0 in let: "lk_a" := newlock #() in let: "lk_b" := newlock #() in ("lk_a", "a_bal", ("lk_b", "b_bal")) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref:loc"HΦ" : ∀ b : val, is_bank b -∗ Φ b "Ha" : a_ref ↦ #0 --------------------------------------∗ WP let: "a_bal" := #a_ref in let: "b_bal" := ref #0 in let: "lk_a" := newlock #() in let: "lk_b" := newlock #() in ("lk_a", "a_bal", ("lk_b", "b_bal")) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:loc"HΦ" : ∀ b : val, is_bank b -∗ Φ b "Ha" : a_ref ↦ #0 "Hb" : b_ref ↦ #0 --------------------------------------∗ WP let: "b_bal" := #b_ref in let: "lk_a" := newlock #() in let: "lk_b" := newlock #() in ("lk_a", #a_ref, ("lk_b", "b_bal")) {{ v, Φ v }}
Note
Before moving on it's worth explaining what's going on in this proof goal.
First, there's the Coq context you're used to, which is rendered with bold
variable names and separated with a solid horizontal line due to the blog infrastructure
(thanks Clément!). Then in the Coq goal is another context, which is being
rendered by the Iris Proof Mode (IPM), using fancy Coq notations. This is a
spatial context, which has three hypotheses, for example on of them is "Ha"
: a_ref ↦ #0
.
The IPM comes with tactics like iDestruct
, iIntros
, and
iApply
which work like the analogous Coq tactics but manipulate these
spatial hypotheses. The context/goal display and tactics let you do proofs
within separation logic as if it were the native logic of Coq instead of
(just) dependent types and higher-order logic. Learning these tactics is a
lot like learning how to do Coq proofs all over again (that is, there is a
learning curve but you do get used to it). Separation logic does introduce
some fundamental complexity into these tactics not seen in Coq: the basic
difference is that whenever you need to prove P ∗ Q
, you have to decide
how to split the hypotheses to prove P
vs Q
, whereas you don't need
to make any analogous decision in Coq (the technical term for this is that
separation logic is a substructural logic, while Coq's higher-order logic
is structural).
The first interesting step of the proof is that we execute the ghost variable
change in ghost_var_alloc
and at the same time destruct it with as (γ1)
"(Hown1&Hγ1)"
, using γ1
for the ghost name and Hown1
and Hγ
for
the two halves, respectively:
Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gname"HΦ" : ∀ b : val, is_bank b -∗ Φ b "Ha" : a_ref ↦ #0 "Hb" : b_ref ↦ #0 "Hown1" : own γ1 (●E 0) "Hγ1" : own γ1 (◯E 0) --------------------------------------∗ WP let: "b_bal" := #b_ref in let: "lk_a" := newlock #() in let: "lk_b" := newlock #() in ("lk_a", #a_ref, ("lk_b", "b_bal")) {{ v, Φ v }}
Now we can initialize the lock invariant for the first account, which will own
the auth "Hγ1"
created above.
Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gname"Ha" : a_ref ↦ #0 "Hγ1" : own γ1 (◯E 0) --------------------------------------∗ account_inv γ1 a_refΣ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gname"HΦ" : ∀ b : val, is_bank b -∗ Φ b "Hb" : b_ref ↦ #0 "Hown1" : own γ1 (●E 0) --------------------------------------∗ ∀ (lk : val) (γ : gname), is_lock γ lk (account_inv γ1 a_ref) -∗ WP let: "lk_a" := lk in let: "lk_b" := newlock #() in ("lk_a", #a_ref, ("lk_b", #b_ref)) {{ v, Φ v }}iExists _; iFrame.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gname"Ha" : a_ref ↦ #0 "Hγ1" : own γ1 (◯E 0) --------------------------------------∗ account_inv γ1 a_refΣ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gname"HΦ" : ∀ b : val, is_bank b -∗ Φ b "Hb" : b_ref ↦ #0 "Hown1" : own γ1 (●E 0) --------------------------------------∗ ∀ (lk : val) (γ : gname), is_lock γ lk (account_inv γ1 a_ref) -∗ WP let: "lk_a" := lk in let: "lk_b" := newlock #() in ("lk_a", #a_ref, ("lk_b", #b_ref)) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1:gname"HΦ" : ∀ b : val, is_bank b -∗ Φ b "Hb" : b_ref ↦ #0 "Hown1" : own γ1 (●E 0) "Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) --------------------------------------∗ WP let: "lk_a" := lk_a in let: "lk_b" := newlock #() in ("lk_a", #a_ref, ("lk_b", #b_ref)) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gname"HΦ" : ∀ b : val, is_bank b -∗ Φ b "Hb" : b_ref ↦ #0 "Hown1" : own γ1 (●E 0) "Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) "Hown2" : own γ2 (●E 0) "Hγ2" : own γ2 (◯E 0) --------------------------------------∗ WP let: "lk_a" := lk_a in let: "lk_b" := newlock #() in ("lk_a", #a_ref, ("lk_b", #b_ref)) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gname"Hb" : b_ref ↦ #0 "Hγ2" : own γ2 (◯E 0) --------------------------------------∗ account_inv γ2 b_refΣ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gname"HΦ" : ∀ b : val, is_bank b -∗ Φ b "Hown1" : own γ1 (●E 0) "Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) "Hown2" : own γ2 (●E 0) --------------------------------------∗ ∀ (lk : val) (γ : gname), is_lock γ lk (account_inv γ2 b_ref) -∗ WP let: "lk_b" := lk in (lk_a, #a_ref, ("lk_b", #b_ref)) {{ v, Φ v }}iExists _; iFrame.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gname"Hb" : b_ref ↦ #0 "Hγ2" : own γ2 (◯E 0) --------------------------------------∗ account_inv γ2 b_refΣ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gname"HΦ" : ∀ b : val, is_bank b -∗ Φ b "Hown1" : own γ1 (●E 0) "Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) "Hown2" : own γ2 (●E 0) --------------------------------------∗ ∀ (lk : val) (γ : gname), is_lock γ lk (account_inv γ2 b_ref) -∗ WP let: "lk_b" := lk in (lk_a, #a_ref, ("lk_b", #b_ref)) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"HΦ" : ∀ b : val, is_bank b -∗ Φ b "Hown1" : own γ1 (●E 0) "Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) "Hown2" : own γ2 (●E 0) "Hlk2" : is_lock γlk2 lk_b (account_inv γ2 b_ref) --------------------------------------∗ WP let: "lk_b" := lk_b in (lk_a, #a_ref, ("lk_b", #b_ref)) {{ v, Φ v }}
At this point we'll allocate the bank_inv
invariant. For reference here's what it says:
The invariant says the logical balances add up to 0, which we'll prove initially
holds here. Notice in the current proof state (shown above), we still have the
auths (own γ (●E 0)
), but the fragments have been used up by calls to
newlock_spec
, which is a typical feature of separation logic. Those
resources are now permanently owned by the account lock invariants.
Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"Hown1" : own γ1 (●E 0) "Hown2" : own γ2 (●E 0) --------------------------------------∗ ▷ bank_inv (γ1, γ2)Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"HΦ" : ∀ b : val, is_bank b -∗ Φ b "Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) "Hlk2" : is_lock γlk2 lk_b (account_inv γ2 b_ref) "Hinv" : inv N (bank_inv (γ1, γ2)) --------------------------------------∗ WP let: "lk_b" := lk_b in (lk_a, #a_ref, ("lk_b", #b_ref)) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"Hown1" : own γ1 (●E 0) "Hown2" : own γ2 (●E 0) --------------------------------------∗ ▷ bank_inv (γ1, γ2)Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"Hown1" : own γ1 (●E 0) "Hown2" : own γ2 (●E 0) --------------------------------------∗ bank_inv (γ1, γ2)iPureIntro; auto.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname--------------------------------------∗ ⌜(0 + 0)%Z = 0⌝Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"HΦ" : ∀ b : val, is_bank b -∗ Φ b "Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) "Hlk2" : is_lock γlk2 lk_b (account_inv γ2 b_ref) "Hinv" : inv N (bank_inv (γ1, γ2)) --------------------------------------∗ WP let: "lk_b" := lk_b in (lk_a, #a_ref, ("lk_b", #b_ref)) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"HΦ" : ∀ b : val, is_bank b -∗ Φ b "Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) "Hlk2" : is_lock γlk2 lk_b (account_inv γ2 b_ref) "Hinv" : inv N (bank_inv (γ1, γ2)) --------------------------------------∗ Φ (lk_a, #a_ref, (lk_b, #b_ref))%VΣ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) "Hlk2" : is_lock γlk2 lk_b (account_inv γ2 b_ref) "Hinv" : inv N (bank_inv (γ1, γ2)) --------------------------------------∗ is_bank (lk_a, #a_ref, (lk_b, #b_ref))Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) "Hlk2" : is_lock γlk2 lk_b (account_inv γ2 b_ref) --------------------------------------∗ ⌜(lk_a, #a_ref, (lk_b, #b_ref))%V = (?Goal, ?Goal0)%V⌝ ∗ is_account ?Goal (γ1, γ2).1 ∗ is_account ?Goal0 (γ1, γ2).2Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) "Hlk2" : is_lock γlk2 lk_b (account_inv γ2 b_ref) --------------------------------------∗ is_account (lk_a, #a_ref) (γ1, γ2).1 ∗ is_account (lk_b, #b_ref) (γ1, γ2).2Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) "Hlk2" : is_lock γlk2 lk_b (account_inv γ2 b_ref) --------------------------------------∗ is_account (lk_a, #a_ref) γ1 ∗ is_account (lk_b, #b_ref) γ2Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) --------------------------------------∗ is_account (lk_a, #a_ref) γ1Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"Hlk2" : is_lock γlk2 lk_b (account_inv γ2 b_ref) --------------------------------------∗ is_account (lk_b, #b_ref) γ2iExists _; eauto with iFrame.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) --------------------------------------∗ is_account (lk_a, #a_ref) γ1iExists _; eauto with iFrame. Qed.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σa_ref, b_ref:locγ1:gnamelk_a:valγlk1, γ2:gnamelk_b:valγlk2:gname"Hlk2" : is_lock γlk2 lk_b (account_inv γ2 b_ref) --------------------------------------∗ is_account (lk_b, #b_ref) γ2
A specification for transfer
As mentioned above, we don't prove anything except for safety for
transfer
. This still has to prove that we follow the lock invariants and
global invariant - after is_bank
is created we can no longer add to a single
account in isolation, for example.
You might expect because this is separation logic that we should return is_bank
b
here. It turns out we don't need to since the fact is persistent, so the
caller will never lose this fact.
Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceb:valamt:Z{{{ is_bank b }}} transfer b #amt {{{ RET #(); True }}}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceb:valamt:Z{{{ is_bank b }}} transfer b #amt {{{ RET #(); True }}}(* Breaking apart the above definitions is really quite painful. I have written better infrastructure for this but it isn't upstream in Iris (yet!) *)Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceb:valamt:ZΦ:val → iPropI Σ"Hb" : is_bank b --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #()) --------------------------------------∗ WP transfer b #amt {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σacct1, acct2:valγ:(gname * gname)%type"Hacct1" : is_account acct1 γ.1 "Hacct2" : is_account acct2 γ.2 "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #()) --------------------------------------∗ WP transfer (acct1, acct2)%V #amt {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σacct2:valγ:(gname * gname)%typebal_ref1:loclk1:val"Hlk" : ∃ γl : gname, is_lock γl lk1 (account_inv γ.1 bal_ref1) "Hacct2" : is_account acct2 γ.2 "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #()) --------------------------------------∗ WP transfer (lk1, #bal_ref1, acct2)%V #amt {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σacct2:valγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hacct2" : is_account acct2 γ.2 "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #()) --------------------------------------∗ WP transfer (lk1, #bal_ref1, acct2)%V #amt {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:val"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk" : ∃ γl : gname, is_lock γl lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #()) --------------------------------------∗ WP transfer (lk1, #bal_ref1, (lk, #bal_ref2))%V #amt {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #()) --------------------------------------∗ WP transfer (lk1, #bal_ref1, (lk, #bal_ref2))%V #amt {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() --------------------------------------∗ WP let: "amt" := #amt in let: "a" := Fst (lk1, #bal_ref1, (lk, #bal_ref2))%V in let: "b" := Snd (lk1, #bal_ref1, (lk, #bal_ref2))%V in acquire (Fst "a");; acquire (Fst "b");; Snd "a" <- ! (Snd "a") - "amt";; Snd "b" <- ! (Snd "b") + "amt";; release (Fst "b");; release (Fst "a");; #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() --------------------------------------∗ WP acquire lk1;; acquire (Fst (lk, #bal_ref2)%V);; Snd (lk1, #bal_ref1)%V <- ! (Snd (lk1, #bal_ref1)%V) - #amt;; Snd (lk, #bal_ref2)%V <- ! (Snd (lk, #bal_ref2)%V) + #amt;; release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() --------------------------------------∗ locked γl1 ∗ account_inv γ.1 bal_ref1 -∗ WP #();; acquire (Fst (lk, #bal_ref2)%V);; Snd (lk1, #bal_ref1)%V <- ! (Snd (lk1, #bal_ref1)%V) - #amt;; Snd (lk, #bal_ref2)%V <- ! (Snd (lk, #bal_ref2)%V) + #amt;; release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Haccount1" : account_inv γ.1 bal_ref1 --------------------------------------∗ WP #();; acquire (Fst (lk, #bal_ref2)%V);; Snd (lk1, #bal_ref1)%V <- ! (Snd (lk1, #bal_ref1)%V) - #amt;; Snd (lk, #bal_ref2)%V <- ! (Snd (lk, #bal_ref2)%V) + #amt;; release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Haccount1" : account_inv γ.1 bal_ref1 --------------------------------------∗ locked γl2 ∗ account_inv γ.2 bal_ref2 -∗ WP #();; Snd (lk1, #bal_ref1)%V <- ! (Snd (lk1, #bal_ref1)%V) - #amt;; Snd (lk, #bal_ref2)%V <- ! (Snd (lk, #bal_ref2)%V) + #amt;; release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Haccount1" : account_inv γ.1 bal_ref1 "Hlocked2" : locked γl2 "Haccount2" : account_inv γ.2 bal_ref2 --------------------------------------∗ WP #();; Snd (lk1, #bal_ref1)%V <- ! (Snd (lk1, #bal_ref1)%V) - #amt;; Snd (lk, #bal_ref2)%V <- ! (Snd (lk, #bal_ref2)%V) + #amt;; release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1:Z"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Haccount2" : account_inv γ.2 bal_ref2 --------------------------------------∗ WP #();; Snd (lk1, #bal_ref1)%V <- ! (Snd (lk1, #bal_ref1)%V) - #amt;; Snd (lk, #bal_ref2)%V <- ! (Snd (lk, #bal_ref2)%V) + #amt;; release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:Z"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ WP #();; Snd (lk1, #bal_ref1)%V <- ! (Snd (lk1, #bal_ref1)%V) - #amt;; Snd (lk, #bal_ref2)%V <- ! (Snd (lk, #bal_ref2)%V) + #amt;; release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}
If you look at the proof goal now, there are a bunch of things going on.
The Iris Proof Mode (IPM) embeds a separation logic context within the Coq
goal. This means we have the Coq context and the IPM context. Furthermore, it
actually uses two contexts: a persistent context (which comes first and is
separated by ---------□
) of facts that are duplicable and thus don't go away
when we need to split, and then a spatial context (separated by ---------∗
) of
ordinary spatial premises.
(* this steps through the critical section *)Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:Z"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ WP Snd (lk, #bal_ref2)%V <- ! #bal_ref2 + #amt;; release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:Z"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #(bal2 + amt) "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}
Now the physical state is updated but not the logical balances in ghost
state. In order to restore the lock invariant, we have to do that, and this
requires using the invariant with iInv
.
iInv
opens the invariant for us and also takes a pattern to destruct the
resulting bank_inv
right away. You can see that it gives us resources in the
context but also adds bank_inv γ
to the goal, since this invariant needs to
hold at all points. The |={⊤ ∖ ↑N}=>
in the goal is another modality (called
a "fancy update"), which you should read as |==>
but with a label of ⊤ ∖
↑N
. This label is the set of invariants we're allowed to open, and currently
it's everything (⊤
or "top") except for the namespace N
, which is the
name chosen for the bank invariant.
Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:Z"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #(bal2 + amt) "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ |={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}(* we use the agreement and update theorems above for these ghost variables *)Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2, bal1', bal2':ZH:bal1' + bal2' = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #(bal2 + amt) "Hown2" : own γ.2 (◯E bal2) "Hγ1" : own γ.1 (●E bal1') "Hγ2" : own γ.2 (●E bal2') --------------------------------------∗ |={⊤ ∖ ↑N}=> ▷ bank_inv γ ∗ (|={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }})Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2, bal2':ZH:bal1 + bal2' = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #(bal2 + amt) "Hown2" : own γ.2 (◯E bal2) "Hγ1" : own γ.1 (●E bal1) "Hγ2" : own γ.2 (●E bal2') --------------------------------------∗ |={⊤ ∖ ↑N}=> ▷ bank_inv γ ∗ (|={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }})Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #(bal2 + amt) "Hown2" : own γ.2 (◯E bal2) "Hγ1" : own γ.1 (●E bal1) "Hγ2" : own γ.2 (●E bal2) --------------------------------------∗ |={⊤ ∖ ↑N}=> ▷ bank_inv γ ∗ (|={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }})Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #(bal2 + amt) "Hown2" : own γ.2 (◯E bal2) "Hγ2" : own γ.2 (●E bal2) "Hγ1" : own γ.1 (●E (bal1 - amt)) "Hown1" : own γ.1 (◯E (bal1 - amt)) --------------------------------------∗ |={⊤ ∖ ↑N}=> ▷ bank_inv γ ∗ (|={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }})Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #(bal2 + amt) "Hγ1" : own γ.1 (●E (bal1 - amt)) "Hown1" : own γ.1 (◯E (bal1 - amt)) "Hγ2" : own γ.2 (●E (bal2 + amt)) "Hown2" : own γ.2 (◯E (bal2 + amt)) --------------------------------------∗ |={⊤ ∖ ↑N}=> ▷ bank_inv γ ∗ (|={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }})(* we can't just modify ghost state however we want - to continue, `iInv` added `bank_inv` to our goal to prove, requiring us to restore the invariant *)Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #(bal2 + amt) "Hγ1" : own γ.1 (●E (bal1 - amt)) "Hown1" : own γ.1 (◯E (bal1 - amt)) "Hγ2" : own γ.2 (●E (bal2 + amt)) "Hown2" : own γ.2 (◯E (bal2 + amt)) --------------------------------------∗ ▷ bank_inv γ ∗ (|={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }})Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hγ1" : own γ.1 (●E (bal1 - amt)) "Hγ2" : own γ.2 (●E (bal2 + amt)) --------------------------------------∗ ▷ bank_inv γΣ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #(bal2 + amt) "Hown1" : own γ.1 (◯E (bal1 - amt)) "Hown2" : own γ.2 (◯E (bal2 + amt)) --------------------------------------∗ |={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hγ1" : own γ.1 (●E (bal1 - amt)) "Hγ2" : own γ.2 (●E (bal2 + amt)) --------------------------------------∗ ▷ bank_inv γΣ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hγ1" : own γ.1 (●E (bal1 - amt)) "Hγ2" : own γ.2 (●E (bal2 + amt)) --------------------------------------∗ bank_inv γΣ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ ⌜(bal1 - amt + (bal2 + amt))%Z = 0⌝lia.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0bal1 - amt + (bal2 + amt) = 0Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #(bal2 + amt) "Hown1" : own γ.1 (◯E (bal1 - amt)) "Hown2" : own γ.2 (◯E (bal2 + amt)) --------------------------------------∗ |={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #(bal2 + amt) "Hown1" : own γ.1 (◯E (bal1 - amt)) "Hown2" : own γ.2 (◯E (bal2 + amt)) --------------------------------------∗ WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}
We've done all the hard work of maintaining the invariant and updating the ghost variables to their new values.
Now we'll be able to release both locks (in any order, actually) by re-proving their lock invariants, with the new values of the ghost variables.
Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hbal2" : bal_ref2 ↦ #(bal2 + amt) "Hown2" : own γ.2 (◯E (bal2 + amt)) --------------------------------------∗ account_inv γ.2 bal_ref2Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hown1" : own γ.1 (◯E (bal1 - amt)) --------------------------------------∗ True -∗ WP #();; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}iExists _; iFrame.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hbal2" : bal_ref2 ↦ #(bal2 + amt) "Hown2" : own γ.2 (◯E (bal2 + amt)) --------------------------------------∗ account_inv γ.2 bal_ref2Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hown1" : own γ.1 (◯E (bal1 - amt)) --------------------------------------∗ True -∗ WP #();; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hown1" : own γ.1 (◯E (bal1 - amt)) --------------------------------------∗ WP #();; release (Fst (lk1, #bal_ref1)%V);; #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hown1" : own γ.1 (◯E (bal1 - amt)) --------------------------------------∗ account_inv γ.1 bal_ref1Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() --------------------------------------∗ True -∗ WP #();; #() {{ v, Φ v }}iExists _; iFrame.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hbal1" : bal_ref1 ↦ #(bal1 - amt) "Hown1" : own γ.1 (◯E (bal1 - amt)) --------------------------------------∗ account_inv γ.1 bal_ref1Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() --------------------------------------∗ True -∗ WP #();; #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() --------------------------------------∗ WP #();; #() {{ v, Φ v }}by iApply "HΦ". Qed.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceamt:ZΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #() --------------------------------------∗ Φ #()
A specification for check_consistency
We'll now prove that check_consistency
always returns true, using the
protocol established by is_bank
. This proof is fairly similar to the one
above, and simpler because it doesn't modify any state.
Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceb:val{{{ is_bank b }}} check_consistency b {{{ RET #true; True }}}(* most of this proof is the same: open everything up and acquire the locks, then destruct the lock invariants *)Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceb:val{{{ is_bank b }}} check_consistency b {{{ RET #true; True }}}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceb:valΦ:val → iPropI Σ"Hb" : is_bank b --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #true) --------------------------------------∗ WP check_consistency b {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σacct1, acct2:valγ:(gname * gname)%type"Hacct1" : is_account acct1 γ.1 "Hacct2" : is_account acct2 γ.2 "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #true) --------------------------------------∗ WP check_consistency (acct1, acct2)%V {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σacct2:valγ:(gname * gname)%typebal_ref1:loclk1:val"Hlk" : ∃ γl : gname, is_lock γl lk1 (account_inv γ.1 bal_ref1) "Hacct2" : is_account acct2 γ.2 "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #true) --------------------------------------∗ WP check_consistency (lk1, #bal_ref1, acct2)%V {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σacct2:valγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hacct2" : is_account acct2 γ.2 "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #true) --------------------------------------∗ WP check_consistency (lk1, #bal_ref1, acct2)%V {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:val"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk" : ∃ γl : gname, is_lock γl lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #true) --------------------------------------∗ WP check_consistency (lk1, #bal_ref1, (lk, #bal_ref2))%V {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #true) --------------------------------------∗ WP check_consistency (lk1, #bal_ref1, (lk, #bal_ref2))%V {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ WP let: "a" := Fst (lk1, #bal_ref1, (lk, #bal_ref2))%V in let: "b" := Snd (lk1, #bal_ref1, (lk, #bal_ref2))%V in acquire (Fst "a");; acquire (Fst "b");; let: "a_bal" := ! (Snd "a") in let: "b_bal" := ! (Snd "b") in let: "ok" := "a_bal" + "b_bal" = #0 in release (Fst "b");; release (Fst "a");; "ok" {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ WP acquire lk1;; acquire (Fst (lk, #bal_ref2)%V);; let: "a_bal" := ! (Snd (lk1, #bal_ref1)%V) in let: "b_bal" := ! (Snd (lk, #bal_ref2)%V) in let: "ok" := "a_bal" + "b_bal" = #0 in release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; "ok" {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ locked γl1 ∗ account_inv γ.1 bal_ref1 -∗ WP #();; acquire (Fst (lk, #bal_ref2)%V);; let: "a_bal" := ! (Snd (lk1, #bal_ref1)%V) in let: "b_bal" := ! (Snd (lk, #bal_ref2)%V) in let: "ok" := "a_bal" + "b_bal" = #0 in release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; "ok" {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Haccount1" : account_inv γ.1 bal_ref1 --------------------------------------∗ WP #();; acquire (Fst (lk, #bal_ref2)%V);; let: "a_bal" := ! (Snd (lk1, #bal_ref1)%V) in let: "b_bal" := ! (Snd (lk, #bal_ref2)%V) in let: "ok" := "a_bal" + "b_bal" = #0 in release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; "ok" {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Haccount1" : account_inv γ.1 bal_ref1 --------------------------------------∗ locked γl2 ∗ account_inv γ.2 bal_ref2 -∗ WP #();; let: "a_bal" := ! (Snd (lk1, #bal_ref1)%V) in let: "b_bal" := ! (Snd (lk, #bal_ref2)%V) in let: "ok" := "a_bal" + "b_bal" = #0 in release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; "ok" {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gname"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Haccount1" : account_inv γ.1 bal_ref1 "Hlocked2" : locked γl2 "Haccount2" : account_inv γ.2 bal_ref2 --------------------------------------∗ WP #();; let: "a_bal" := ! (Snd (lk1, #bal_ref1)%V) in let: "b_bal" := ! (Snd (lk, #bal_ref2)%V) in let: "ok" := "a_bal" + "b_bal" = #0 in release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; "ok" {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1:Z"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Haccount2" : account_inv γ.2 bal_ref2 --------------------------------------∗ WP #();; let: "a_bal" := ! (Snd (lk1, #bal_ref1)%V) in let: "b_bal" := ! (Snd (lk, #bal_ref2)%V) in let: "ok" := "a_bal" + "b_bal" = #0 in release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; "ok" {{ v, Φ v }}(* the critical section is easy *)Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:Z"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ WP #();; let: "a_bal" := ! (Snd (lk1, #bal_ref1)%V) in let: "b_bal" := ! (Snd (lk, #bal_ref2)%V) in let: "ok" := "a_bal" + "b_bal" = #0 in release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; "ok" {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:Z"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ WP let: "a_bal" := #bal1 in let: "b_bal" := ! (Snd (lk, #bal_ref2)%V) in let: "ok" := "a_bal" + "b_bal" = #0 in release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; "ok" {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:Z"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ WP let: "b_bal" := #bal2 in let: "ok" := #bal1 + "b_bal" = #0 in release (Fst (lk, #bal_ref2)%V);; release (Fst (lk1, #bal_ref1)%V);; "ok" {{ v, Φ v }}(* Now we need to prove something about our return value using information derived from the invariant. As before we'll open the invariant, but this time we don't need to modify anything, just extract a pure fact. *)Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:Z"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }}(* the [%] here is the pure fact, actually *)Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:Z"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ |={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2, bal1', bal2':ZH:bal1' + bal2' = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) "Hγ1" : own γ.1 (●E bal1') "Hγ2" : own γ.2 (●E bal2') --------------------------------------∗ |={⊤ ∖ ↑N}=> ▷ bank_inv γ ∗ (|={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }})Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2, bal2':ZH:bal1 + bal2' = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) "Hγ1" : own γ.1 (●E bal1) "Hγ2" : own γ.2 (●E bal2') --------------------------------------∗ |={⊤ ∖ ↑N}=> ▷ bank_inv γ ∗ (|={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }})Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) "Hγ1" : own γ.1 (●E bal1) "Hγ2" : own γ.2 (●E bal2) --------------------------------------∗ |={⊤ ∖ ↑N}=> ▷ bank_inv γ ∗ (|={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }})Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) "Hγ1" : own γ.1 (●E bal1) "Hγ2" : own γ.2 (●E bal2) --------------------------------------∗ ▷ bank_inv γ ∗ (|={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }})Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hγ1" : own γ.1 (●E bal1) "Hγ2" : own γ.2 (●E bal2) --------------------------------------∗ ▷ bank_inv γΣ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ |={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hγ1" : own γ.1 (●E bal1) "Hγ2" : own γ.2 (●E bal2) --------------------------------------∗ ▷ bank_inv γΣ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hγ1" : own γ.1 (●E bal1) "Hγ2" : own γ.2 (●E bal2) --------------------------------------∗ bank_inv γΣ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ ⌜(bal1 + bal2)%Z = 0⌝lia.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0bal1 + bal2 = 0Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ |={⊤}=> WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) "Hlocked2" : locked γl2 "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ WP release lk;; release (Fst (lk1, #bal_ref1)%V);; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ account_inv γ.2 bal_ref2Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) --------------------------------------∗ True -∗ WP #();; release (Fst (lk1, #bal_ref1)%V);; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }}iExists _; iFrame.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hbal2" : bal_ref2 ↦ #bal2 "Hown2" : own γ.2 (◯E bal2) --------------------------------------∗ account_inv γ.2 bal_ref2Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) --------------------------------------∗ True -∗ WP #();; release (Fst (lk1, #bal_ref1)%V);; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true "Hlocked1" : locked γl1 "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) --------------------------------------∗ WP #();; release (Fst (lk1, #bal_ref1)%V);; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) --------------------------------------∗ account_inv γ.1 bal_ref1Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ True -∗ WP #();; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }}iExists _; iFrame.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "Hbal1" : bal_ref1 ↦ #bal1 "Hown1" : own γ.1 (◯E bal1) --------------------------------------∗ account_inv γ.1 bal_ref1Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ True -∗ WP #();; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ WP #();; #(bool_decide (#(bal1 + bal2) = #0)) {{ v, Φ v }}(* the calculation always returns true because of the H hypothesis we got from the invariant *)Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ Φ #(bool_decide (#(bal1 + bal2) = #0))by iApply "HΦ". Qed.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σγ:(gname * gname)%typebal_ref1:loclk1:valγl1:gnamebal_ref2:loclk:valγl2:gnamebal1, bal2:ZH:bal1 + bal2 = 0"Hlk1" : is_lock γl1 lk1 (account_inv γ.1 bal_ref1) "Hlk2" : is_lock γl2 lk (account_inv γ.2 bal_ref2) "Hinv" : inv N (bank_inv γ) --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ Φ #true
The final theorem
The final theorem we'll prove is demo_check_consistency
, which ties everything
together into a Hoare triple that has no precondition. The intuition is that
this theorem says that if demo_check_consistency
terminates, it returns true,
which implies the consistency check works at least with one concurrent transfer.
We could prove a theorem along these lines more directly, but I won't do that
here.
Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespace{{{ True }}} demo_check_consistency #() {{{ RET #true; True }}}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespace{{{ True }}} demo_check_consistency #() {{{ RET #true; True }}}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σ"HΦ" : ▷ (True -∗ Φ #true) --------------------------------------∗ WP demo_check_consistency #() {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σ"HΦ" : True -∗ Φ #true --------------------------------------∗ WP let: "bank" := new_bank #() in Fork (transfer "bank" #5);; check_consistency "bank" {{ v, Φ v }}(* we use `#Hb` to put the newly created `is_bank` in the "persistent context" in the Iris Proof Mode - these are persistent facts and thus are available even when we need to split to prove a separating conjunction *)Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σ"HΦ" : True -∗ Φ #true --------------------------------------∗ ∀ b : val, is_bank b -∗ WP let: "bank" := b in Fork (transfer "bank" #5);; check_consistency "bank" {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σb:val"Hb" : is_bank b --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ WP let: "bank" := b in Fork (transfer "bank" #5);; check_consistency "bank" {{ v, Φ v }}
The proof is easy now - the fork rule requires us to split the context and
prove any Hoare triple for the forked thread. transfer
only needs Hb
, but
that's persistent and will thus be available. We've coincidentally already
proven a triple for it with a postcondition of True
.
Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σb:val"Hb" : is_bank b --------------------------------------□ WP transfer b #5 {{ _, True }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σb:val"Hb" : is_bank b --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ WP #();; check_consistency b {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σb:val"Hb" : is_bank b --------------------------------------□ WP transfer b #5 {{ _, True }}auto.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σb:val"Hb" : is_bank b --------------------------------------□ True -∗ True(* `check_consistency` always returns true, assuming `is_bank` *)Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σb:val"Hb" : is_bank b --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ WP #();; check_consistency b {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σb:val"Hb" : is_bank b --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ True -∗ Φ #trueby iApply "HΦ". Qed.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceΦ:val → iPropI Σb:val"Hb" : is_bank b --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ Φ #true
The above proof and specification for wp_fork
might not be clear; here's a
derived specification for Fork
that might be easier to interpret. This
specification makes explicit that the caller splits their context into two
parts, one to use for proving e
and the other for the remainder of the
program e'
.
Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceP, Q:iProp Σe, e':expr(P -∗ WP e {{ _, True }}) -∗ ∀ Φ : val → iProp Σ, (Q -∗ WP e' {{ v, Φ v }}) -∗ P ∗ Q -∗ WP Fork e;; e' {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceP, Q:iProp Σe, e':expr(P -∗ WP e {{ _, True }}) -∗ ∀ Φ : val → iProp Σ, (Q -∗ WP e' {{ v, Φ v }}) -∗ P ∗ Q -∗ WP Fork e;; e' {{ v, Φ v }}Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceP, Q:iProp Σe, e':exprΦ:val → iProp Σ"Hwp1" : P -∗ WP e {{ _, True }} "Hwp2" : Q -∗ WP e' {{ v, Φ v }} "HP" : P "HQ" : Q --------------------------------------∗ WP Fork e;; e' {{ v, Φ v }}
The goal here shows that we assumed some resources P
and Q
, and what
we'll do is distribute them to prove that e
is safe and that we can continue
with running e'
.
(* the details of the rest of this proof aren't important *)wp_apply ("Hwp2" with "HQ"). Qed. End heap.Σ:gFunctorsheapG0:heapG ΣlockG0:lockG ΣinG0:inG Σ (ghostR ZO)N:=nroot.@"bank":namespaceP, Q:iProp Σe, e':exprΦ:val → iProp Σ"Hwp2" : Q -∗ WP e' {{ v, Φ v }} "HQ" : Q --------------------------------------∗ WP #();; e' {{ v, Φ v }}
Conclusions
Now you've seen the whole process of writing some code and reasoning about in Iris! Many parts of this proof will surely seem mysterious, but I hope you still saw the basic parts of the argument show up in the formal, machine-checked reasoning.
Taking a step back, I want to emphasize again that this is just a taste of what Iris can do. You don't have to use HeapLang, you can write your own, like our GooseLang language (heavily based on HeapLang) which we use to model Go. You don't have to prove Hoare triples, you can prove refinement. You don't even have to use the Iris base logic to take advantage of the interactive proof mode. It still takes quite a bit of expertise to do these things, but we're talking about concurrent verification here. Iris has significantly lowered the barrier to entry, and it makes it possible to do all these proofs in a machine-checked way.
What to try next
If you're now excited about Iris, here are a few things you can try next:
The POPL 2018 tutorial is fairly accessible and well-documented, and will help you actually write program proofs using Iris. There's also a POPL 2020 tutorial, which is about a semantic type soundness proof using Iris, another big use case for Iris (other than program proofs).
The journal paper Iris from the ground up explains the theory and logical foundations behind Iris. It does an excellent job of teaching Iris, well, from the ground up, especially compared to the papers because Iris was developed over the course of several conference papers, none of which quite explain the technical details for the current version. However, it spends almost no time motivating Iris, leaving that to the many papers published using Iris.
If you still want more to convince you Iris is great, you can look at the variety of papers published using it, which you can see on the Iris website. I think some papers that highlight the diversity of applications include the following:
The original RustBelt POPL 2018 paper defines semantic type safety for Rust. Iris is essential to correctly model Rust's higher-order features, like first-class functions.
The original Iris Proof Mode POPL 2017 paper shows off the proof mode and how it is used for both program proofs and logical relations. (Unfortunately some terminology has to be translated to relate this paper to the current implementation, which is based on a generalized proof mode described in the MoSeL ICFP 2018 paper.)
The gDOT ICFP 2020 paper proves soundness of the Scala type system using an interesting subset of the Iris framework (notably it uses step indexing, the proof mode, and a program logic, but no separation logic).
In a shameless plug, our own Perennial SOSP 2019 paper uses Iris to do crash-safety reasoning for Go code.
You don't actually have to read all of these papers, even just looking at the abstracts gives a sense for what Iris can be used for.
Learning Iris is hard - if you're seriously considering it, do reach out and find someone who can help you while you're getting started! The Iris community is not large but it is welcoming.