atomic.v 927 Bytes
Newer Older
1 2
(* Logically atomic triple *)

3 4
From iris.base_logic Require Export fancy_updates.
From iris.program_logic Require Export hoare weakestpre.
Zhen Zhang's avatar
Zhen Zhang committed
5 6 7 8
From iris.prelude Require Export coPset.
Import uPred.

Section atomic.
Ralf Jung's avatar
Ralf Jung committed
9
  Context `{irisG Λ Σ} {A: Type}.
Zhen Zhang's avatar
Zhen Zhang committed
10

11
  (* TODO RJ: IMHO it would make more sense to have the outer mask first, after all, that's what the shifts "starts" with. *)
Ralf Jung's avatar
Ralf Jung committed
12 13
  (* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
  Definition atomic_triple
14 15 16
             (α: A  iProp Σ) (* atomic pre-condition *)
             (β: A  val _  iProp Σ) (* atomic post-condition *)
             (Ei Eo: coPset) (* inside/outside masks *)
Ralf Jung's avatar
Ralf Jung committed
17 18
             (e: expr _) : iProp Σ :=
    ( P Q, (P ={Eo, Ei}=>  x:A,
19 20 21 22
                       α x 
                       ((α x ={Ei, Eo}= P) 
                        ( v, β x v ={Ei, Eo}= Q v))
     ) - {{ P }} e @  {{ Q }})%I.
Zhen Zhang's avatar
Zhen Zhang committed
23
End atomic.