Types

• val
  • Scope: %V
• expr
  • Scope: %E
• loc

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

• 'Handles' for dynamically allocated values.
• A ref use does this:
  1. A location in heap is found for the value
  2. Value is stored in this location
  3. This location is returned
• Dereference value at a location l: !l
• Update value at location l with another value v: l <- v

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

Evaluate an expr

• Use eval with a fuel parameter
• Eg: eval 10 expvar where 10 is the fuel
• inl _ if result could be obtained. Otherwise inr _

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

• iModIntro: related to ghost variables
• iFrame
  • https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/proof_mode.md?ref_type=heads#separation-logic-specific-tactics
  • 'pairs up hypotheses with pieces of separation sequence'
• iStartProof
• iNext: advance to next step in the step-index relation
• iLöb
• iApply, iIntro, iIntros, iDestruct, iExists, iInduction
• iPureIntro

WP

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

• all executions of the expression e would produce a value v such that Φ v is true
• φ is a proposition
• The {{ v, Φ v }} is the post condition

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 }} ??

• wp_lam: removes λ:
  • Does application. ie, beta-reduction
• wp_rec: similar to wp_lam, but for recursive function
• wp_let: zeta-reduction (ie, substitutes let var with its definition)
• wp_load: substitute !x with v if there is a x ↦ v in assumption
• wp_store: move a p <- v to context as p ↦ v
• wp_seq: reduce a sequential composition
• wp_alloc
• wp_pair
• wp_fork
• wp_apply
• wp_smartapply
• wp_bind
• wp_pures
• wp_cmpxchgsuc, wp_cmpxchgfail
• wp_faa
• wp_proj
• wp_inj
• wp_match, wp_case
• wp_unop, wp_binop, wp_op: reduce unary, binary or other arithmetic operation
• wppure: kind of like 'auto' for wp tactics
• wp_pures: do wp_pure as many times as possible

1. wp_lam

   "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. wp_store

   --------------------------------------□
   "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)

• A heaplang interpreter is available as part of the iris_unstable package.
  • This package contains iris stuff that is not considered ready for release.
• This interpreter is only development version and is not part of standard release.
• Use via exec function with a fuel parameter:
  • Eg: Compute (exec 10 exprn)