# Iris

## Why this blog post?

- We want to introduce Iris as an example of concurrency using program
  logic-based reasoning as opposed to state machines seen in earlier lectures.
- Our research is based on Iris, so it's state-of-the-art and we believe it's
  useful.
- I wrote a blog post because there was no paper on Iris I could expect a
  systems person to understand.

## Goals for this lecture

- Understand what a lock invariant means formally.
- Understand how to add ghost variables to an Iris proof.
- Be able to read IPM goals.

## Bank example and specification

Recall: purely functional bank from first day

`sum_balances(transfer(b, amt)) = sum_balances(b)`

Could extend this property to sequential bank:

```
{{{ bank(l, b) }}}
  bank_transfer(l, amt)
{{{ bank(l, transfer(b, amt)) }}}

{{{ bank(l, b) }}}
  check_bals(l)
{{{ RET #(sum_balances(b) = 0); bank(l, bals) }}}
```

We're able to show the imperative bank implementation `bank_transfer` simulates
the Gallina specification (using a record for the balances) in `transfer`.

With concurrency, this kind of spec no longer makes sense.
- Can't share between threads
- Implementation locks per-account
- If we had >2 accounts, then would have true concurrency between accounts

Approach we've seen so far: prove transfers are atomic.

In Armada, spec would have logical balances, behave like sequential bank above,
with transfer atomic. Could introduce an invariant that sum of balances is 0.
Would need to use movers for lock pattern.

Let's see how that the proof works in Iris.

## Lock invariants

Intuitive idea: locks "protect" certain resources, especially shared state
(memory locations/pointers).

Some examples, this time for the entire bank state:

Go:

```go
type Bank struct {
  // m protects bal1 and bal2
  // ensures bal1+bal2 = 0
  m    *sync.Mutex
  bal1 *int64
  bal2 *int64
}
```

Rust:

```rust
struct Balances {
  bal1: i64,
  bal2: i64,
}

// bal1 + bal2 = 0
type Bank = Mutex<Balances>

fn transfer(b: &Bank, n: i64) {
    let mut bals = b.lock();
    bals.bal1 -= n;
    bals.bal2 -= n;
    // bals implicitly unlocked (out of scope)
}
```

Rust mutex has a couple interesting features:
- Code (not comment) embodies that balances are "inside" mutex
- Cannot access balances without locking
- Release lock when we stop using the balances ("return" balances to mutex)

However, Rust can't enforce what we intended to use the mutex for, only what
data is mediated by the mutex.

Iris:

```
Definition is_bank b: iProp Σ :=
    is_lock(b.m,
        (* lock invariant spells out what lock _means_ *)
        ∃ amt1 amt2. b.bal1 ↦ amt1 ∗ b.bal2 ↦ amt2 ∗ ⌜amt1+amt2=0⌝)
```

```
{is_bank(b)}
  b.m.lock()
{b.bal1 ↦ amt1 ∗ b.bal2 ↦ amt2 ∗ ⌜amt1+amt2=0⌝}
  b.bal1 -= n
  b.bal2 += n
{bal1 ↦ (amt1-n) ∗ b.bal2 ↦ (amt2+n)}
  (* need to give mapsto facts AND prove (amt1-n) + (amt2+n) = 0 *)
  b.m.unlock()
{emp}
```

## Adding ghost state for finer-grained concurrency

diagrams for introducing logical bal1 and bal2

fractional split:
`ghost_var(γ, 1/2, bal1) ∗ ghost_var(γ, 1/2, bal1) ≡ ghost_var(γ, 1, bal1)`

agreement: `ghost_var(γ, 1/2, bal1) ∗ ghost_var(γ, 1/2, bal2) ⊢ bal1=bal2`

fractional permissions generally useful in concurrency: read-only permissions
but also ability to "gather all the permissions" and change the value

new invariant:

```
account_inv γ bal_ref :=
  ∃ bal. bal_ref ↦ bal ∗ ghost_var(γ, 1/2, bal)

bank_inv γ1 γ2 :=
  ∃ bal1 bal2. ghost_var(γ1, 1/2, bal1) ∗ ghost_var(γ2, 1/2, bal2) ∗ ⌜bal1 + bal2 = 0⌝
```

## Reading IPM contexts

Brief review of what these look like

Walk through proof of `demo_check_consistency`, and maybe `check_consistency`.

## What else can we do with Iris?

### More sophisticated ghost state

Invariants are user-defined ghost state!

Locks and lock invariants are implemented using some simple ghost state!

Monotonic counter:

- `mnat_own_auth(γ, n)` "the counter value is exactly n"
- `mnat_own_lb(γ, m)` "the counter value is at least m"

Key property: `mnat_own_lb(γ, m)` is persistent and can't be broken by other
threads

### Refinement proofs

We can do what we said in the Armada example and prove that transfer is
logically atomic (the spec that says this is a little complicated, so I didn't
do that). On top of that spec we could prove `check_consistency` using an
invariant.

### Semantic type safety

Want to show type safety: if we have an expression of type `T`, at runtime it'll
actually be a value of type `T`.

Relate Rust types to owning some predicate over the value, eg `&mut i64` is like
`λ v, ∃ (i: Z), v ↦ i`.

Lets us do things like prove unsafe code interacts well with rest of language.

For example, prove that `Vec<u64>` and all its methods behave like their types.
(More interesting than above because `Vec` needs `unsafe` in its implementation).