atomic.v 725 Bytes
Newer Older
1
2
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics classes.
3
From iris.bi.lib Require Export atomic.
4
5
6
7
8
9
Set Default Proof Using "Type".

Definition atomic_wp `{irisG Λ Σ} {A B : Type}
  (e: expr Λ) (* expression *)
  (α: A  iProp Σ) (* atomic pre-condition *)
  (β: A  B  iProp Σ) (* atomic post-condition *)
10
  (Eo Em : coPset) (* outside/module masks *)
11
12
  (f: A  B  val Λ) (* Turn the return data into the return value *)
  : iProp Σ :=
13
14
    ( Q Φ, Q - atomic_update α β Eo Em (λ x y, Q - Φ (f x y)) -
             WP e {{ Φ }})%I.
15
(* Note: To add a private postcondition, use
16
   atomic_update α β Eo Em (λ x y, POST x y -∗ Φ (f x y)) *)