atomic.v 927 Bytes
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
2
(* Logically atomic triple *)

Ralf Jung's avatar
Ralf Jung committed
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

Ralf Jung's avatar
Ralf Jung committed
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
Zhen Zhang's avatar
Zhen Zhang committed
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
                       α x 
                       ((α x ={Ei, Eo}= P) 
21
22
                        ( v, β x v ={Ei, Eo}= Q v))
     ) - {{ P }} e @  {{ Q }})%I.
Zhen Zhang's avatar
Zhen Zhang committed
23
End atomic.