A brief introduction to Iris

Iris 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 value x.

  • #x is overloaded to turn x 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 resources P (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 that P 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:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
a:A.(ofe_car)
⊢ |==> γ : gname, own γ (●E a) ∗ own γ (◯E a)
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
a:A.(ofe_car)
⊢ |==> γ : gname, own γ (●E a) ∗ own γ (◯E a)
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
a:A.(ofe_car)
✓ (●E a ⋅ ◯E a)
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin: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:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
a:A.(ofe_car)
✓ (●E a ⋅ ◯E a)
apply excl_auth_valid.
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin: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:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin: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:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
a:A.(ofe_car)
γ:gname
"H1" : own γ (●E a) "H2" : own γ (◯E a) --------------------------------------∗ own γ (●E a) ∗ own γ (◯E a)
iFrame. Qed.

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:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
γ:gname
a1, a2:A.(ofe_car)
own γ (●E a1) -∗ own γ (◯E a2) -∗ ⌜a1 = a2⌝
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
γ:gname
a1, a2:A.(ofe_car)
own γ (●E a1) -∗ own γ (◯E a2) -∗ ⌜a1 = a2⌝
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
γ:gname
a1, a2:A.(ofe_car)
"Hγ1" : own γ (●E a1) "Hγ2" : own γ (◯E a2) --------------------------------------∗ ⌜a1 = a2⌝
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
γ:gname
a1, a2:A.(ofe_car)
"H" : ✓ (●E a1 ⋅ ◯E a2) --------------------------------------∗ ⌜a1 = a2⌝
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
γ:gname
a1:A.(ofe_car)
--------------------------------------∗ ⌜a1 = a1⌝
done. Qed.

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:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
γ:gname
a1', a1, a2:A.(ofe_car)
own γ (●E a1) -∗ own γ (◯E a2) ==∗ own γ (●E a1') ∗ own γ (◯E a1')
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
γ:gname
a1', a1, a2:A.(ofe_car)
own γ (●E a1) -∗ own γ (◯E a2) ==∗ own γ (●E a1') ∗ own γ (◯E a1')
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
γ:gname
a1', a1, a2:A.(ofe_car)
"Hγ●" : own γ (●E a1) "Hγ◯" : own γ (◯E a2) --------------------------------------∗ |==> own γ (●E a1') ∗ own γ (◯E a1')
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
γ:gname
a1', a1, a2:A.(ofe_car)
●E a1 ⋅ ◯E a2 ~~> ●E a1' ⋅ ◯E a1'
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
γ:gname
a1', a1, a2:A.(ofe_car)
--------------------------------------∗ |==> True
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
γ:gname
a1', a1, a2:A.(ofe_car)
●E a1 ⋅ ◯E a2 ~~> ●E a1' ⋅ ◯E a1'
apply excl_auth_update.
A:ofeT
Hequiv:LeibnizEquiv A
Hdiscrete:OfeDiscrete A
Σ:gFunctors
Hin:inG Σ (authR (optionUR (exclR A)))
γ:gname
a1', a1, a2:A.(ofe_car)
--------------------------------------∗ |==> True
done. Qed.

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 |==>.

Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
{{{ True }}} new_bank #() {{{ (b : val), RET b; is_bank b }}}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
{{{ True }}} new_bank #() {{{ (b : val), RET b; is_bank b }}}
Σ:gFunctors
heapG0: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 }}
Σ:gFunctors
heapG0: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 }}
Σ:gFunctors
heapG0: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 }}
Σ:gFunctors
heapG0: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 for the two halves, respectively:

  
Σ:gFunctors
heapG0: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.

  
Σ:gFunctors
heapG0: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
Σ:gFunctors
heapG0: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 }}
Σ:gFunctors
heapG0: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
iExists _; iFrame.
Σ:gFunctors
heapG0: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
"Hb" : b_ref ↦ #0 "Hγ2" : own γ2 (◯E 0) --------------------------------------∗ account_inv γ2 b_ref
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
"Hb" : b_ref ↦ #0 "Hγ2" : own γ2 (◯E 0) --------------------------------------∗ account_inv γ2 b_ref
iExists _; iFrame.
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_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:

bank_inv = λ γ : gname * gname, ( bal1 bal2 : Z, own γ.1 (●E bal1) ∗ own γ.2 (●E bal2) ∗ ⌜(bal1 + bal2)%Z = 0⌝)%I : gname * gname → iProp Σ

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.

  
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_b:val
γlk2:gname
"Hown1" : own γ1 (●E 0) "Hown2" : own γ2 (●E 0) --------------------------------------∗ ▷ bank_inv (γ1, γ2)
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_b:val
γlk2:gname
"Hown1" : own γ1 (●E 0) "Hown2" : own γ2 (●E 0) --------------------------------------∗ ▷ bank_inv (γ1, γ2)
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_b:val
γlk2:gname
"Hown1" : own γ1 (●E 0) "Hown2" : own γ2 (●E 0) --------------------------------------∗ bank_inv (γ1, γ2)
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_b:val
γlk2:gname
--------------------------------------∗ ⌜(0 + 0)%Z = 0
iPureIntro; auto.
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_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
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_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))
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_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
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_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
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_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
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_b:val
γlk2:gname
"Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) --------------------------------------∗ is_account (lk_a, #a_ref) γ1
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_b:val
γlk2:gname
"Hlk2" : is_lock γlk2 lk_b (account_inv γ2 b_ref) --------------------------------------∗ is_account (lk_b, #b_ref) γ2
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_b:val
γlk2:gname
"Hlk1" : is_lock γlk1 lk_a (account_inv γ1 a_ref) --------------------------------------∗ is_account (lk_a, #a_ref) γ1
iExists _; eauto with iFrame.
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
a_ref, b_ref:loc
γ1:gname
lk_a:val
γlk1, γ2:gname
lk_b:val
γlk2:gname
"Hlk2" : is_lock γlk2 lk_b (account_inv γ2 b_ref) --------------------------------------∗ is_account (lk_b, #b_ref) γ2
iExists _; eauto with iFrame. Qed.

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.

Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
b:val
amt:Z
{{{ is_bank b }}} transfer b #amt {{{ RET #(); True }}}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
b:val
amt:Z
{{{ is_bank b }}} transfer b #amt {{{ RET #(); True }}}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
b:val
amt:Z
Φ:val → iPropI Σ
"Hb" : is_bank b --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #()) --------------------------------------∗ WP transfer b #amt {{ v, Φ v }}
(* Breaking apart the above definitions is really quite painful. I have written better infrastructure for this but it isn't upstream in Iris (yet!) *)
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
acct2:val
γ:(gname * gname)%type
bal_ref1:loc
lk1: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
acct2:val
γ:(gname * gname)%type
bal_ref1:loc
lk1: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, 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 *)
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, 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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, 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.

Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, 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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2, bal1', bal2':Z
H: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 }})
(* we use the agreement and update theorems above for these ghost variables *)
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2, bal2':Z
H: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 }})
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }})
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }})
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }})
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }})
(* 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 *)
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 γ
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 γ
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 γ
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H:bal1 + bal2 = 0
bal1 - amt + (bal2 + amt) = 0
lia.
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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.

  
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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
iExists _; iFrame.
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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
iExists _; iFrame.
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
amt:Z
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 -∗ Φ #() --------------------------------------∗ Φ #()
by iApply "HΦ". Qed.

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.

Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
b:val
{{{ is_bank b }}} check_consistency b {{{ RET #true; True }}}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
b: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 *)
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
b:val
Φ:val → iPropI Σ
"Hb" : is_bank b --------------------------------------□ "HΦ" : ▷ (True -∗ Φ #true) --------------------------------------∗ WP check_consistency b {{ v, Φ v }}
Σ:gFunctors
heapG0: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
acct2:val
γ:(gname * gname)%type
bal_ref1:loc
lk1: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
acct2:val
γ:(gname * gname)%type
bal_ref1:loc
lk1: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, 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 }}
(* the critical section is easy *)
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, 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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, 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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, 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 }}
(* 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. *)
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, 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 *)
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2, bal1', bal2':Z
H: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 }})
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2, bal2':Z
H: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 }})
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }})
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }})
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 γ
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 γ
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 γ
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H:bal1 + bal2 = 0
bal1 + bal2 = 0
lia.
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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
iExists _; iFrame.
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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
iExists _; iFrame.
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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))
(* the calculation always returns true because of the H hypothesis we got from the invariant *)
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
γ:(gname * gname)%type
bal_ref1:loc
lk1:val
γl1:gname
bal_ref2:loc
lk:val
γl2:gname
bal1, bal2:Z
H: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
by iApply "HΦ". Qed.

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.

Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
{{{ True }}} demo_check_consistency #() {{{ RET #true; True }}}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
{{{ True }}} demo_check_consistency #() {{{ RET #true; True }}}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
"HΦ" : ▷ (True -∗ Φ #true) --------------------------------------∗ WP demo_check_consistency #() {{ v, Φ v }}
Σ:gFunctors
heapG0: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 }}
Σ:gFunctors
heapG0: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 }}
(* 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 *)
Σ:gFunctors
heapG0: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.

  
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
b:val
"Hb" : is_bank b --------------------------------------□ WP transfer b #5 {{ _, True }}
Σ:gFunctors
heapG0: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 }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
b:val
"Hb" : is_bank b --------------------------------------□ WP transfer b #5 {{ _, True }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
b:val
"Hb" : is_bank b --------------------------------------□ True -∗ True
auto.
Σ:gFunctors
heapG0: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 }}
(* `check_consistency` always returns true, assuming `is_bank` *)
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
b:val
"Hb" : is_bank b --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ True -∗ Φ #true
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
Φ:val → iPropI Σ
b:val
"Hb" : is_bank b --------------------------------------□ "HΦ" : True -∗ Φ #true --------------------------------------∗ Φ #true
by iApply "HΦ". Qed.

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'.

Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
P, Q:iProp Σ
e, e':expr
(P -∗ WP e {{ _, True }}) -∗ Φ : val → iProp Σ, (Q -∗ WP e' {{ v, Φ v }}) -∗ P ∗ Q -∗ WP Fork e;; e' {{ v, Φ v }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
P, Q:iProp Σ
e, e':expr
(P -∗ WP e {{ _, True }}) -∗ Φ : val → iProp Σ, (Q -∗ WP e' {{ v, Φ v }}) -∗ P ∗ Q -∗ WP Fork e;; e' {{ v, Φ v }}
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
P, 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 *)
  
Σ:gFunctors
heapG0:heapG Σ
lockG0:lockG Σ
inG0:inG Σ (ghostR ZO)
N:=nroot.@"bank":namespace
P, Q:iProp Σ
e, e':expr
Φ:val → iProp Σ
"Hwp2" : Q -∗ WP e' {{ v, Φ v }} "HQ" : Q --------------------------------------∗ WP #();; e' {{ v, Φ v }}
wp_apply ("Hwp2" with "HQ"). Qed. End heap.

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.