Commit 2850f888 authored by Ralf Jung's avatar Ralf Jung

Add first definition of (logically) atomic shifts and triples

parent 26fdda7a
......@@ -37,6 +37,7 @@ theories/bi/fixpoint.v
theories/bi/monpred.v
theories/bi/embedding.v
theories/bi/lib/fractional.v
theories/bi/lib/atomic.v
theories/base_logic/upred.v
theories/base_logic/derived.v
theories/base_logic/base_logic.v
......@@ -72,6 +73,7 @@ theories/program_logic/ectx_lifting.v
theories/program_logic/ownp.v
theories/program_logic/total_lifting.v
theories/program_logic/total_ectx_lifting.v
theories/program_logic/atomic.v
theories/heap_lang/lang.v
theories/heap_lang/tactics.v
theories/heap_lang/lifting.v
......
From iris.bi Require Export bi updates.
From stdpp Require Import coPset.
From iris.proofmode Require Import classes class_instances.
Set Default Proof Using "Type".
Definition atomic_shift {PROP: sbi} `{!FUpd PROP} {A B : Type}
(α: A PROP) (* atomic pre-condition *)
(β: A B PROP) (* atomic post-condition *)
(Ei Eo: coPset) (* inside/outside masks *)
(Q: A B PROP) (* post-condition *)
: PROP :=
( (F P:PROP), F P ( P ={Eo, Ei}= x, α x
((α x ={Ei, Eo}= P) ( y, β x y ={Ei, Eo}= F - Q x y)))
)%I.
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 *)
(Ei Eo: coPset) (* inside/outside masks *)
(f: A B val Λ) (* Turn the return data into the return value *)
: iProp Σ :=
( Φ, atomic_shift α β Ei Eo (λ x y, Φ (f x y)) -
WP e {{ Φ }})%I.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment