exercises.adequacy

From iris.algebra Require Import excl.
From iris.base_logic.lib Require Export token.
From iris.heap_lang Require Import adequacy lang proofmode notation par.
From exercises Require Import spin_lock.

(* ################################ *)

Adequacy

Thus far, we have assumed that the weakest precondition is correct. But what does that even mean? This is what is called adequacy, and its definition depends on the properties we want it to satisfy. In Iris, we have decided to focus on two properties:

The program won't get stuck.
The program satisfies the postcondition.

In this chapter, we go over how to define these properties and show that the weakest precondition satisfies them.

HeapLang is defined using a step relation. This relation defines how an expression can be reduced in a single step.

prim_step e1 σ1 κs e2 σ2 efs

Here, e1 is the expression we want to reduce, and σ1 is the current state of the machine. e2 and σ2 are then the new expression and new state. efs is a list of expressions representing new threads spawned. Finally, κs represents a list of something called observations. We won't use these, so κs will remain empty.

This relation isn't very nice to work with by itself. To fix this, we package the state of the program into what we call a configuration. Notice that this configuration takes a list of expressions. These represent all the threads that are currently running.

Definition cfg : Type := list expr * state.

Now, let us define steps in terms of configurations. To model the non-sequential behaviour of threads, we define steps to be a step in any thread.

Inductive step (ρ1 ρ2 : cfg) : Prop :=
  step_atomic e1 σ1 e2 σ2 efs t1 t2 :
    ρ1 = (t1 ++ e1 :: t2 , σ1 ) →
    ρ2 = (t1 ++ e2 :: t2 ++ efs , σ2 ) →
    prim_step e1 σ1 [] e2 σ2 efs →
    step ρ1 ρ2.

With this, we can define multiple steps as the reflexive transitive closure (rtc) of step.

Now, a program is stuck if any thread cannot take a step and is not a value. Conversely, a thread is not stuck if it is either a value or can take a step.

Definition not_stuck e σ :=
is_Some (to_val e) ∨ ∃ e' σ' efs , prim_step e σ [] e' σ' efs.

With this, we can now express the first adequacy criterion: a program will not get stuck if all possible future configurations are not stuck.

∀ t σ' e', rtc step ([e], σ) (t, σ') → e' ∈ t → not_stuck e' σ'

Likewise, for the second criterion, we say that a program satisfies a postcondition when the main thread terminates to a value, and that value satisfies the postcondition.

∀ t σ' v, rtc step ([e], σ) (of_val v :: t, σ') → φ v σ'

Together, these two properties define adequate. However, adequate takes an extra parameter of type stuckness. This parameter specifies whether adequacy includes the first criterion.

The proof that the weakest precondition implies adequacy is:

    heap_adequacy Σ `{!heapGpreS Σ} s e σ φ : ∀ _ : heapGS Σ,
      inv_heap_inv -∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝}} → adequate s e σ (λ v σ,
      φ v)

To use this statement, we have to actually instantiate Σ. It needs to contain all the kinds of resources we needed to prove the weakest precondition. Let us use prog from the Spin Lock chapter as an example. To prove prog_spec, we used the resource of heaps as well as tokens. The resources needed by the resource of heaps are all contained in heapΣ. Likewise, the resources needed by token (exclR unitO) are contained in tokenΣ.

Definition progΣ : gFunctors := #[
heapΣ; (* The resources required by HeapLang *)
tokenΣ (* The resources we used for spin-lock *)
].

Finally, we can combine the pieces to prove adequacy.

Lemma prog_adequacy σ :
  adequate NotStuck prog σ (λ v _, v = #0 ∨ v = #1).
Proof.
  apply (heap_adequacy progΣ).
  iIntros "%_ _".
  iApply prog_spec.
Qed.

With this, we now have a closed proof that prog does not get stuck, and if it terminates at some value v, then v = #0 ∨ v = #1.