atomic.v 705 Bytes
Newer Older
1
2
3
4
5
6
7
8
9
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics classes.
From iris.bi.lib Require Import atomic.
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
    ( Φ, atomic_update α β Eo Em (λ x y, Φ (f x y)) -
14
          WP e {{ Φ }})%I.
15
16
(* Note: To add a private postcondition, use
   atomic_shift α β Eo Em (λ x y, POST x y -∗ Φ (f x y)) *)