iris

https://plv.mpi-sws.org/coqdoc/iris/index.html https://plv.mpi-sws.org/semantics-course/

Iris

—

NONEV and SOMEV

Notation NONEV := (InjLV #())
Notation SOMEV x := (InjRV x)

InjLV itself is a constructor of val type:

Inductive expr : Set :=
    Val : val → expr
  | Var : string → expr
  | Rec : binder → binder → expr → expr
  | App : expr → expr → expr
  | UnOp : un_op → expr → expr
  | BinOp : bin_op → expr → expr → expr
  | If : expr → expr → expr → expr
  | Pair : expr → expr → expr
  | Fst : expr → expr
  | Snd : expr → expr
  | InjL : expr → expr
  | InjR : expr → expr
  | Case : expr → expr → expr → expr
  | AllocN : expr → expr → expr
  | Free : expr → expr
  | Load : expr → expr
  | Store : expr → expr → expr
  | CmpXchg : expr → expr → expr → expr
  | Xchg : expr → expr → expr
  | FAA : expr → expr → expr
  | Fork : expr → expr
  | NewProph : expr
  | Resolve : expr → expr → expr → expr
  with val : Set :=
    LitV : base_lit → val
  | RecV : binder → binder → expr → val
  | PairV : val → val → val
  | InjLV : val → val
  | InjRV : val → val.

Concurrency

Iris Proof Mode (IPM)

https://gitlab.mpi-sws.org/iris/iris/blob/master/docs/proof_mode.md

Arrays:

Rules

P1 ⊢ Q1      P2 ⊢ Q2
----------------------
  P1 ∗ P2 ⊢ Q1 ∗ Q2

–

  {P} e {w. Q}
---------------- Frame rule
{P*R} e {w. Q*R}


------------------ Val
{True} v {w. w==v}


---------------------- Alloc
{True} ref(v) {l. l↦v}


------------------------ Load
{l↦v} !l {w. w==v * l↦v}


--------------- Store
{l↦v} l←w {l↦w}

Relevance of frame rule:

HeapLang

HeapLang: an ML-like language that comes with iris.

Types

Functions

Non-recursive:

(* add5 := λx. x+5 *)
λ: "x", "x" + #5 

(* compose := λx. x+5 *)
λ: "f" "g", (λ: "x", "g" ("f" "x"))

Recursive (from here):

Example recursion : expr :=
  let: "fac" :=
    rec: "f" "n" := if: "n" = #0 then #1 else "n" * "f" ("n" - #1)
  in
  ("fac" #4, "fac" #5).

References

let "v" := ref (#0) in
"v"

Evaluate an expr

let expressions

Not native, but available by means of notations that desugars to lambda abstractions.

Example:

let: "a" := #4 in
let: "b" := #2 in
"a" + "b".

Tactics

WP

WP e {{ v, Φ v }} is the weakest precondition such that

Example from here:

Section Proof.         
  Context `{heapGS Σ}.

Section list.                                     
  Context `{heapGS Σ}.                            

  Example arith : expr := #1 + #2 + #3 + #4 + #5. 

  Lemma arith_spec : ⊢ WP arith {{ v, ⌜v = #15⌝ }}. 
  Proof.                                            
    unfold arith.                                   
    by wp_pures.                                    
  Qed.                                              
End Proof.

{{{ P }}} e {{{ RET v, Q }}}

desugars to

∀ Φ, P -∗ (Q -∗ Φ v) -∗ WP e {{ v, Φ v }}

This is logically equivalent to

P -∗ WP e {{ x, x = v ∗ Q }}

WP tactics

https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/heap_lang.md#tactics

These tactics work when goal is like WP e @ E {{ Q }} ??

  1. wplam

    "Hx" : x ↦ v1
"Hy" : y ↦ v2
"Post" : ▷ (x ↦ v2 ∗ y ↦ v1 -∗ Φ #())
--------------------------------------∗
WP (λ: "x" "y", let: "tmp" := ! "x" in "x" <- "y";; "y" <- "tmp")%V #x #y
{{ v, Φ v }}

    becomes

    "Hx" : x ↦ v1
"Hy" : y ↦ v2
"Post" : x ↦ v2 ∗ y ↦ v1 -∗ Φ #()
--------------------------------------∗
WP let: "y" := #y in let: "tmp" := ! #x in #x <- "y";; "y" <- "tmp"
{{ v, Φ v }}

  2. wpstore

    --------------------------------------□
"Hp" : p ↦ (#x, v)
"Hl" : is_list l v
"Post" : (∃ p0 : loc, ⌜InjRV #p = InjRV #p0⌝ ∗
            ∃ v' : val, p0 ↦ (#(n + x), v') ∗ is_list (map (Z.add n) l) v') -∗
         Φ #()
--------------------------------------∗
WP #p <- (#x + #n, v);; inc_list #n v {{ v, Φ v }}

    becomes

    --------------------------------------□
"Hp" : p ↦ (#(x + n), v)
"Hl" : is_list l v
"Post" : (∃ p0 : loc, ⌜InjRV #p = InjRV #p0⌝ ∗
            ∃ v' : val, p0 ↦ (#(n + x), v') ∗ is_list (map (Z.add n) l) v') -∗
         Φ #()
--------------------------------------∗
WP inc_list #n v {{ v, Φ v }}

Interpreter (experimental)

Misc

Doubts

Seperation Logic

Dbt