Library zoo.program_logic.wp
From zoo Require Import
prelude.
From zoo.iris Require Import
diaframe.
From zoo.language Require Import
tactics
notations.
From zoo.language Require Export
typeclasses.
From zoo.program_logic Require Export
bwp.
From zoo Require Import
options.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[local] Definition wp_def e tid E Φ :=
match tid with
| None ⇒
∀ tid, BWP e ∶ tid @ E {{ Φ }}
| Some tid ⇒
BWP e ∶ tid @ E {{ Φ }}
end%I.
#[global] Arguments wp_def _ _%_E _ _%_I : assert.
End zoo_G.
#[local] Definition wp_aux : seal (@wp_def).
Definition wp :=
wp_aux.(unseal).
#[global] Arguments wp {_ _} _ _%_E _ _%_I : assert.
#[local] Lemma wp_unseal `{zoo_G : !ZooG Σ} :
wp = wp_def.
#[local] Ltac wp_unseal :=
rewrite wp_unseal /wp_def;
select (option thread_id) (fun tid ⇒ destruct tid).
Notation "" := (
None
)(in custom wp_thread_id
).
Notation "∶ tid" := (
Some tid
)(in custom wp_thread_id at level 200,
tid constr,
format "'/ ' ∶ tid "
).
Notation "∷ tid" :=
tid
( in custom wp_thread_id at level 200,
tid constr,
format "'/ ' ∷ tid "
).
Notation "'WP' e tid E {{ Φ } }" := (
wp e%E tid E Φ%I
)(at level 0,
e at level 200,
tid custom wp_thread_id at level 200,
E custom wp_mask at level 200,
Φ at level 200,
format "'[hv' WP '/ ' '[' e ']' tid E '/' {{ '[' Φ ']' '/' } } ']'"
) : bi_scope.
Notation "'WP' e tid E {{ v , Q } }" := (
wp e%E tid E (λ v, Q%I)
)(at level 0,
e at level 200,
tid custom wp_thread_id at level 200,
E custom wp_mask at level 200,
v at level 200 as pattern,
Q at level 200,
format "'[hv' WP '/ ' '[' e ']' tid E '/' {{ '[' v , '/' Q ']' '/' } } ']'"
) : bi_scope.
Notation "'{{{' P } } } e tid E {{{ x1 .. xn , 'RET' v ; Q } } }" :=
( □ ∀ Φ,
P -∗
▷ (∀ x1, .. (∀ xn, Q -∗ Φ (v : val)) ..) -∗
wp e%E tid E Φ
)%I
( at level 20,
P at level 200,
e at level 200,
tid custom wp_thread_id at level 200,
E custom wp_mask at level 200,
x1 closed binder,
xn closed binder,
Q at level 200,
format "'[hv' {{{ '/ ' '[' P ']' '/' } } } '/ ' '[' e ']' tid E '/' {{{ x1 .. xn , '/ ' RET v ; '/ ' '[' Q ']' '/' } } } ']'"
) : bi_scope.
Notation "'{{{' P } } } e tid E {{{ 'RET' v ; Q } } }" :=
( □ ∀ Φ,
P -∗
▷ (Q -∗ Φ (v : val)) -∗
wp e%E tid E Φ
)%I
( at level 20,
P at level 200,
e at level 200,
tid custom wp_thread_id at level 200,
E custom wp_mask at level 200,
Q at level 200,
format "'[hv' {{{ '/ ' '[' P ']' '/' } } } '/ ' '[' e ']' tid E '/' {{{ '/ ' RET v ; '/ ' '[' Q ']' '/' } } } ']'"
) : bi_scope.
Notation "'{{{' P } } } e tid E {{{ x1 .. xn , 'RET' v ; Q } } }" := (
∀ Φ,
P%I -∗
▷ (∀ x1, .. (∀ xn, Q%I -∗ Φ (v : val)) ..) -∗
wp e%E tid E Φ%I
) : stdpp_scope.
Notation "'{{{' P } } } e tid E {{{ 'RET' v ; Q } } }" := (
∀ Φ,
P%I -∗
▷ (Q%I -∗ Φ (v : val)) -∗
wp e%E tid E Φ%I
) : stdpp_scope.
Implicit Types b : bool.
Implicit Types l : location.
Implicit Types pid : prophet_id.
Implicit Types e : expr.
Implicit Types es : list expr.
Implicit Types v w : val.
Implicit Types σ : state.
Implicit Types κ κs : list observation.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Implicit Types P R : iProp Σ.
Implicit Types Φ : val → iProp Σ.
#[global] Instance wp_ne e tid E n :
Proper (pointwise_relation _ (≡{n}≡) ==> (≡{n}≡)) (wp e tid E).
#[global] Instance wp_proper e tid E :
Proper (pointwise_relation _ (≡) ==> (≡)) (wp e tid E).
#[global] Instance wp_contractive e tid E n :
TCEq (to_val e) None →
Proper (pointwise_relation _ (dist_later n) ==> (≡{n}≡)) (wp e tid E).
Lemma wp_thread_id_mono e tid E Φ :
WP e @ E {{ Φ }} ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_bwp e tid E Φ :
WP e ∶ tid @ E {{ Φ }} ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_wp e tid E Φ :
BWP e ∶ tid @ E {{ Φ }} ⊢
WP e ∶ tid @ E {{ Φ }}.
Lemma bwp_wp_weak e tid E Φ :
(∀ tid, BWP e ∶ tid @ E {{ Φ }}) ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_state_interp e tid E Φ :
( ∀ ns nt σ κs,
state_interp ns nt σ κs ={E}=∗
state_interp ns nt σ κs ∗
WP e ∷ tid @ E {{ Φ }}
) ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_value_fupd' v tid E Φ :
(|={E}=> Φ v) ⊢
WP of_val v ∷ tid @ E {{ Φ }}.
Lemma wp_value_fupd e v tid E Φ :
AsVal e v →
(|={E}=> Φ v) ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_value' v tid E Φ :
Φ v ⊢
WP of_val v ∷ tid @ E {{ Φ }}.
Lemma wp_value e v tid E Φ :
AsVal e v →
Φ v ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_value_mono v tid E Φ1 Φ2 :
WP of_val v ∷ tid @ E {{ Φ1 }} -∗
(Φ1 v ={E}=∗ Φ2 v) -∗
WP of_val v ∷ tid @ E {{ Φ2 }}.
Lemma wp_strong_mono e tid E1 Φ1 E2 Φ2 :
E1 ⊆ E2 →
WP e ∷ tid @ E1 {{ Φ1 }} -∗
(∀ v, Φ1 v ={E2}=∗ Φ2 v) -∗
WP e ∷ tid @ E2 {{ Φ2 }}.
Lemma wp_mono e tid E Φ1 Φ2 :
(∀ v, Φ1 v ⊢ Φ2 v) →
WP e ∷ tid @ E {{ Φ1 }} ⊢
WP e ∷ tid @ E {{ Φ2 }}.
#[global] Instance wp_mono' e tid E :
Proper (pointwise_relation _ (⊢) ==> (⊢)) (wp e tid E).
#[global] Instance wp_flip_mono' e tid E :
Proper (pointwise_relation _ (flip (⊢)) ==> (flip (⊢))) (wp e tid E).
Lemma fupd_wp e tid E Φ :
(|={E}=> WP e ∷ tid @ E {{ Φ }}) ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_fupd e tid E Φ :
WP e ∷ tid @ E {{ v, |={E}=> Φ v }} ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_frame_l e tid E Φ R :
R ∗ WP e ∷ tid @ E {{ Φ }} ⊢
WP e ∷ tid @ E {{ v, R ∗ Φ v }}.
Lemma wp_frame_r e tid E Φ R :
WP e ∷ tid @ E {{ Φ }} ∗ R ⊢
WP e ∷ tid @ E {{ v, Φ v ∗ R }}.
Lemma wp_wand {e tid E} Φ1 Φ2 :
WP e ∷ tid @ E {{ Φ1 }} -∗
(∀ v, Φ1 v -∗ Φ2 v) -∗
WP e ∷ tid @ E {{ Φ2 }}.
Lemma wp_frame_wand e tid E Φ R :
R -∗
WP e ∷ tid @ E {{ v, R -∗ Φ v }} -∗
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_atomic e `{!Atomic e} tid E1 E2 Φ :
(|={E1,E2}=> WP e ∷ tid @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢
WP e ∷ tid @ E1 {{ Φ }}.
Lemma wp_bind K `{!Context K} e tid1 tid2 E Φ :
( if tid2 is Some tid2 then
if tid1 is Some tid1 then
tid1 = tid2
else
False
else
True
) →
WP e ∷ tid2 @ E {{ v, WP K (of_val v) ∷ tid1 @ E {{ Φ }} }} ⊢
WP K e ∷ tid1 @ E {{ Φ }}.
Lemma wp_bind' K `{!Context K} e tid E Φ :
WP e ∷ tid @ E {{ v, WP K (of_val v) ∷ tid @ E {{ Φ }} }} ⊢
WP K e ∷ tid @ E {{ Φ }}.
#[global] Instance frame_wp p e tid E R Φ1 Φ2 :
(∀ v, Frame p R (Φ1 v) (Φ2 v)) →
Frame
p
R
(WP e ∷ tid @ E {{ Φ1 }})
(WP e ∷ tid @ E {{ Φ2 }})
| 2.
#[global] Instance is_except_0_wp e tid E Φ :
IsExcept0 (WP e ∷ tid @ E {{ Φ }}).
#[global] Instance elim_modal_bupd_wp p e tid E P Φ :
ElimModal
True
p
false
(|==> P)
P
(WP e ∷ tid @ E {{ Φ }})
(WP e ∷ tid @ E {{ Φ }}).
#[global] Instance elim_modal_fupd_wp p e tid E P Φ :
ElimModal
True
p
false
(|={E}=> P)
P
(WP e ∷ tid @ E {{ Φ }})
(WP e ∷ tid @ E {{ Φ }}).
#[global] Instance elim_modal_fupd_wp_wrong_mask p e tid E1 E2 P Φ :
ElimModal
(pm_error "Goal and eliminated modality must have the same mask. Use [iApply fupd_wp; iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
p
false
(|={E2}=> P)
False
(WP e ∷ tid @ E1 {{ Φ }})
False
| 100.
#[global] Instance elim_modal_fupd_wp_atomic p e tid E1 E2 P Φ :
ElimModal
(Atomic e)
p
false
(|={E1,E2}=> P)
P
(WP e ∷ tid @ E1 {{ Φ }})
(WP e ∷ tid @ E2 {{ v, |={E2,E1}=> Φ v }})%I
| 100.
#[global] Instance elim_modal_fupd_wp_atomic_wrong_mask p e tid E1 E2 E2' P Φ :
ElimModal
(pm_error "Goal and eliminated modality must have the same mask. Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
p
false
(|={E2,E2'}=> P)
False
(WP e ∷ tid @ E1 {{ Φ }})
False
| 200.
#[global] Instance add_modal_fupd_wp e tid E P Φ :
AddModal
(|={E}=> P)
P
(WP e ∷ tid @ E {{ Φ }}).
#[global] Instance elim_acc_wp_atomic {X} e tid E1 E2 α β γ Φ :
ElimAcc (X := X)
(Atomic e)
(fupd E1 E2)
(fupd E2 E1)
α
β
γ
(WP e ∷ tid @ E1 {{ Φ }})
(λ x, WP e ∷ tid @ E2 {{ v, |={E2}=> β x ∗ (γ x -∗? Φ v) }})%I
| 100.
#[global] Instance elim_acc_wp_nonatomic {X} e tid E α β γ Φ :
ElimAcc (X := X)
True
(fupd E E)
(fupd E E)
α
β
γ
(WP e ∷ tid @ E {{ Φ }})
(λ x, WP e ∷ tid @ E {{ v, |={E}=> β x ∗ (γ x -∗? Φ v) }})%I.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Implicit Types Φ : val → iProp Σ.
Lemma wp_pure_step_strong ϕ n e1 e2 ns tid E Φ :
PureExec ϕ n e1 e2 →
ϕ →
⧖ ns -∗
▷^n (
⧖ (ns + n) -∗
£ (later_sum ns n) -∗
WP e2 ∷ tid @ E {{ Φ }}
) -∗
WP e1 ∷ tid @ E {{ Φ }}.
Lemma wp_pure_step ϕ n e1 e2 tid E Φ :
PureExec ϕ n e1 e2 →
ϕ →
▷^n (
£ (n × later_constant) -∗
WP e2 ∷ tid @ E {{ Φ }}
) ⊢
WP e1 ∷ tid @ E {{ Φ }}.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Lemma wp_equal_nobranch v1 v2 tid E Φ :
▷ (
∀ b,
⌜(if b then (≈) else (≉)) v1 v2⌝ -∗
Φ #b
) ⊢
WP v1 == v2 ∷ tid @ E {{ Φ }}.
Lemma wp_equal v1 v2 tid E Φ :
▷ (
( ⌜v1 ≉ v2⌝ -∗
Φ false%V
) ∧ (
⌜v1 ≈ v2⌝ -∗
Φ true%V
)
) ⊢
WP v1 == v2 ∷ tid @ E {{ Φ }}.
Lemma wp_alloc (tag : Z) n tid E :
(0 ≤ tag)%Z →
(0 ≤ n)%Z →
{{{
True
}}}
Alloc #tag #n ∷ tid @ E
{{{
l
, RET #l;
l ↦ₕ Header ₊tag ₊n ∗
meta_token l ⊤ ∗
l ↦∗ replicate ₊n ()%V
}}}.
Lemma wp_block_mutable {es tag} vs tid E :
0 < length es →
to_vals es = Some vs →
{{{
True
}}}
Block Mutable tag es ∷ tid @ E
{{{
l
, RET #l;
l ↦ₕ Header tag (length es) ∗
meta_token l ⊤ ∗
l ↦∗ vs
}}}.
Lemma wp_block_generative {es tag} vs tid E :
to_vals es = Some vs →
{{{
True
}}}
Block ImmutableGenerativeStrong tag es ∷ tid @ E
{{{
bid
, RET ValBlock (Generative (Some bid)) tag vs;
True
}}}.
Lemma wp_match l hdr x_fb e_fb brs e tid E Φ :
eval_match hdr.(header_tag) hdr.(header_size) (SubjectLoc l) x_fb e_fb brs = Some e →
▷ l ↦ₕ hdr -∗
▷ WP e ∷ tid @ E {{ Φ }} -∗
WP Match #l x_fb e_fb brs ∷ tid @ E {{ Φ }}.
Lemma wp_match_context K `{!Context K} l hdr x_fb e_fb brs e tid E Φ :
eval_match hdr.(header_tag) hdr.(header_size) (SubjectLoc l) x_fb e_fb brs = Some e →
▷ l ↦ₕ hdr -∗
▷ WP K e ∷ tid @ E {{ Φ }} -∗
WP K (Match #l x_fb e_fb brs) ∷ tid @ E {{ Φ }}.
Lemma wp_tag l hdr tid E Φ :
▷ l ↦ₕ hdr -∗
▷ Φ #(encode_tag hdr.(header_tag)) -∗
WP GetTag #l ∷ tid @ E {{ Φ }}.
Lemma wp_size l hdr tid E Φ :
▷ l ↦ₕ hdr -∗
▷ Φ #hdr.(header_size) -∗
WP GetSize #l ∷ tid @ E {{ Φ }}.
Lemma wp_load l fld dq v tid E :
{{{
▷ (l +ₗ fld) ↦{dq} v
}}}
Load #l #fld ∷ tid @ E
{{{
RET v;
(l +ₗ fld) ↦{dq} v
}}}.
Lemma wp_store l fld w v tid E :
{{{
▷ (l +ₗ fld) ↦ w
}}}
Store #l #fld v ∷ tid @ E
{{{
RET ();
(l +ₗ fld) ↦ v
}}}.
Lemma wp_xchg l fld w v tid E :
{{{
▷ (l +ₗ fld) ↦ w
}}}
Xchg (#l, #fld)%V v ∷ tid @ E
{{{
RET w;
(l +ₗ fld) ↦ v
}}}.
Lemma wp_cas_nobranch l fld dq v v1 v2 tid E Φ :
▷ (l +ₗ fld) ↦{dq} v -∗
▷ (
∀ b,
⌜(if b then (≈) else (≉)) v v1⌝ -∗
(l +ₗ fld) ↦{dq} v -∗
⌜if b then dq = DfracOwn 1 else True⌝ ∗
(l +ₗ fld) ↦{dq} v ∗
( (l +ₗ fld) ↦{dq} (if b then v2 else v) -∗
Φ #b
)
) -∗
WP CAS (#l, #fld)%V v1 v2 ∷ tid @ E {{ Φ }}.
Lemma wp_cas_nobranch' l fld v v1 v2 tid E Φ :
▷ (l +ₗ fld) ↦ v -∗
▷ (
∀ b,
⌜(if b then (≈) else (≉)) v v1⌝ -∗
(l +ₗ fld) ↦ (if b then v2 else v) -∗
Φ #b
) -∗
WP CAS (#l, #fld)%V v1 v2 ∷ tid @ E {{ Φ }}.
Lemma wp_cas l fld dq v v1 v2 tid E Φ :
▷ (l +ₗ fld) ↦{dq} v -∗
▷ (
( ⌜v ≉ v1⌝ -∗
(l +ₗ fld) ↦{dq} v -∗
Φ false%V
) ∧ (
⌜v ≈ v1⌝ -∗
(l +ₗ fld) ↦{dq} v -∗
⌜dq = DfracOwn 1⌝ ∗
(l +ₗ fld) ↦{dq} v ∗
( (l +ₗ fld) ↦ v2 -∗
Φ true%V
)
)
) -∗
WP CAS (#l, #fld)%V v1 v2 ∷ tid @ E {{ Φ }}.
Lemma wp_cas' l fld v v1 v2 tid E Φ :
▷ (l +ₗ fld) ↦ v -∗
▷ (
( ⌜v ≉ v1⌝ -∗
(l +ₗ fld) ↦ v -∗
Φ false%V
) ∧ (
⌜v ≈ v1⌝ -∗
(l +ₗ fld) ↦ v2 -∗
Φ true%V
)
) -∗
WP CAS (#l, #fld)%V v1 v2 ∷ tid @ E {{ Φ }}.
Lemma wp_faa l fld (i1 i2 : Z) tid E :
{{{
▷ (l +ₗ fld) ↦ #i1
}}}
FAA (#l, #fld)%V #i2 ∷ tid @ E
{{{
RET #i1;
(l +ₗ fld) ↦ #(i1 + i2)
}}}.
Lemma wp_fork e tid E Φ :
▷ (
∀ tid v,
tid ↦ₗ v -∗
WP e ∶ tid {{ λ _, True }}
) -∗
▷ Φ ()%V -∗
WP Fork e ∷ tid @ E {{ Φ }}.
Lemma wp_get_local tid dq v E :
{{{
▷ tid ↦ₗ{dq} v
}}}
GetLocal ∶ tid @ E
{{{
RET v;
tid ↦ₗ{dq} v
}}}.
Lemma wp_set_local tid w v E :
{{{
▷ tid ↦ₗ w
}}}
SetLocal v ∶ tid @ E
{{{
RET ();
tid ↦ₗ v
}}}.
Lemma wp_proph tid E :
{{{
True
}}}
Proph ∷ tid @ E
{{{
prophs pid
, RET #pid;
prophet_model' pid prophs
}}}.
Lemma wp_resolve e pid v prophs tid E Φ :
Atomic e →
to_val e = None →
prophet_model' pid prophs -∗
WP e ∷ tid @ E {{ res,
∀ prophs',
⌜prophs = (res, v) :: prophs'⌝ -∗
prophet_model' pid prophs' -∗
Φ res
}} -∗
WP Resolve e #pid v ∷ tid @ E {{ Φ }}.
End zoo_G.
prelude.
From zoo.iris Require Import
diaframe.
From zoo.language Require Import
tactics
notations.
From zoo.language Require Export
typeclasses.
From zoo.program_logic Require Export
bwp.
From zoo Require Import
options.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[local] Definition wp_def e tid E Φ :=
match tid with
| None ⇒
∀ tid, BWP e ∶ tid @ E {{ Φ }}
| Some tid ⇒
BWP e ∶ tid @ E {{ Φ }}
end%I.
#[global] Arguments wp_def _ _%_E _ _%_I : assert.
End zoo_G.
#[local] Definition wp_aux : seal (@wp_def).
Definition wp :=
wp_aux.(unseal).
#[global] Arguments wp {_ _} _ _%_E _ _%_I : assert.
#[local] Lemma wp_unseal `{zoo_G : !ZooG Σ} :
wp = wp_def.
#[local] Ltac wp_unseal :=
rewrite wp_unseal /wp_def;
select (option thread_id) (fun tid ⇒ destruct tid).
Notation "" := (
None
)(in custom wp_thread_id
).
Notation "∶ tid" := (
Some tid
)(in custom wp_thread_id at level 200,
tid constr,
format "'/ ' ∶ tid "
).
Notation "∷ tid" :=
tid
( in custom wp_thread_id at level 200,
tid constr,
format "'/ ' ∷ tid "
).
Notation "'WP' e tid E {{ Φ } }" := (
wp e%E tid E Φ%I
)(at level 0,
e at level 200,
tid custom wp_thread_id at level 200,
E custom wp_mask at level 200,
Φ at level 200,
format "'[hv' WP '/ ' '[' e ']' tid E '/' {{ '[' Φ ']' '/' } } ']'"
) : bi_scope.
Notation "'WP' e tid E {{ v , Q } }" := (
wp e%E tid E (λ v, Q%I)
)(at level 0,
e at level 200,
tid custom wp_thread_id at level 200,
E custom wp_mask at level 200,
v at level 200 as pattern,
Q at level 200,
format "'[hv' WP '/ ' '[' e ']' tid E '/' {{ '[' v , '/' Q ']' '/' } } ']'"
) : bi_scope.
Notation "'{{{' P } } } e tid E {{{ x1 .. xn , 'RET' v ; Q } } }" :=
( □ ∀ Φ,
P -∗
▷ (∀ x1, .. (∀ xn, Q -∗ Φ (v : val)) ..) -∗
wp e%E tid E Φ
)%I
( at level 20,
P at level 200,
e at level 200,
tid custom wp_thread_id at level 200,
E custom wp_mask at level 200,
x1 closed binder,
xn closed binder,
Q at level 200,
format "'[hv' {{{ '/ ' '[' P ']' '/' } } } '/ ' '[' e ']' tid E '/' {{{ x1 .. xn , '/ ' RET v ; '/ ' '[' Q ']' '/' } } } ']'"
) : bi_scope.
Notation "'{{{' P } } } e tid E {{{ 'RET' v ; Q } } }" :=
( □ ∀ Φ,
P -∗
▷ (Q -∗ Φ (v : val)) -∗
wp e%E tid E Φ
)%I
( at level 20,
P at level 200,
e at level 200,
tid custom wp_thread_id at level 200,
E custom wp_mask at level 200,
Q at level 200,
format "'[hv' {{{ '/ ' '[' P ']' '/' } } } '/ ' '[' e ']' tid E '/' {{{ '/ ' RET v ; '/ ' '[' Q ']' '/' } } } ']'"
) : bi_scope.
Notation "'{{{' P } } } e tid E {{{ x1 .. xn , 'RET' v ; Q } } }" := (
∀ Φ,
P%I -∗
▷ (∀ x1, .. (∀ xn, Q%I -∗ Φ (v : val)) ..) -∗
wp e%E tid E Φ%I
) : stdpp_scope.
Notation "'{{{' P } } } e tid E {{{ 'RET' v ; Q } } }" := (
∀ Φ,
P%I -∗
▷ (Q%I -∗ Φ (v : val)) -∗
wp e%E tid E Φ%I
) : stdpp_scope.
Implicit Types b : bool.
Implicit Types l : location.
Implicit Types pid : prophet_id.
Implicit Types e : expr.
Implicit Types es : list expr.
Implicit Types v w : val.
Implicit Types σ : state.
Implicit Types κ κs : list observation.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Implicit Types P R : iProp Σ.
Implicit Types Φ : val → iProp Σ.
#[global] Instance wp_ne e tid E n :
Proper (pointwise_relation _ (≡{n}≡) ==> (≡{n}≡)) (wp e tid E).
#[global] Instance wp_proper e tid E :
Proper (pointwise_relation _ (≡) ==> (≡)) (wp e tid E).
#[global] Instance wp_contractive e tid E n :
TCEq (to_val e) None →
Proper (pointwise_relation _ (dist_later n) ==> (≡{n}≡)) (wp e tid E).
Lemma wp_thread_id_mono e tid E Φ :
WP e @ E {{ Φ }} ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_bwp e tid E Φ :
WP e ∶ tid @ E {{ Φ }} ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_wp e tid E Φ :
BWP e ∶ tid @ E {{ Φ }} ⊢
WP e ∶ tid @ E {{ Φ }}.
Lemma bwp_wp_weak e tid E Φ :
(∀ tid, BWP e ∶ tid @ E {{ Φ }}) ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_state_interp e tid E Φ :
( ∀ ns nt σ κs,
state_interp ns nt σ κs ={E}=∗
state_interp ns nt σ κs ∗
WP e ∷ tid @ E {{ Φ }}
) ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_value_fupd' v tid E Φ :
(|={E}=> Φ v) ⊢
WP of_val v ∷ tid @ E {{ Φ }}.
Lemma wp_value_fupd e v tid E Φ :
AsVal e v →
(|={E}=> Φ v) ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_value' v tid E Φ :
Φ v ⊢
WP of_val v ∷ tid @ E {{ Φ }}.
Lemma wp_value e v tid E Φ :
AsVal e v →
Φ v ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_value_mono v tid E Φ1 Φ2 :
WP of_val v ∷ tid @ E {{ Φ1 }} -∗
(Φ1 v ={E}=∗ Φ2 v) -∗
WP of_val v ∷ tid @ E {{ Φ2 }}.
Lemma wp_strong_mono e tid E1 Φ1 E2 Φ2 :
E1 ⊆ E2 →
WP e ∷ tid @ E1 {{ Φ1 }} -∗
(∀ v, Φ1 v ={E2}=∗ Φ2 v) -∗
WP e ∷ tid @ E2 {{ Φ2 }}.
Lemma wp_mono e tid E Φ1 Φ2 :
(∀ v, Φ1 v ⊢ Φ2 v) →
WP e ∷ tid @ E {{ Φ1 }} ⊢
WP e ∷ tid @ E {{ Φ2 }}.
#[global] Instance wp_mono' e tid E :
Proper (pointwise_relation _ (⊢) ==> (⊢)) (wp e tid E).
#[global] Instance wp_flip_mono' e tid E :
Proper (pointwise_relation _ (flip (⊢)) ==> (flip (⊢))) (wp e tid E).
Lemma fupd_wp e tid E Φ :
(|={E}=> WP e ∷ tid @ E {{ Φ }}) ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_fupd e tid E Φ :
WP e ∷ tid @ E {{ v, |={E}=> Φ v }} ⊢
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_frame_l e tid E Φ R :
R ∗ WP e ∷ tid @ E {{ Φ }} ⊢
WP e ∷ tid @ E {{ v, R ∗ Φ v }}.
Lemma wp_frame_r e tid E Φ R :
WP e ∷ tid @ E {{ Φ }} ∗ R ⊢
WP e ∷ tid @ E {{ v, Φ v ∗ R }}.
Lemma wp_wand {e tid E} Φ1 Φ2 :
WP e ∷ tid @ E {{ Φ1 }} -∗
(∀ v, Φ1 v -∗ Φ2 v) -∗
WP e ∷ tid @ E {{ Φ2 }}.
Lemma wp_frame_wand e tid E Φ R :
R -∗
WP e ∷ tid @ E {{ v, R -∗ Φ v }} -∗
WP e ∷ tid @ E {{ Φ }}.
Lemma wp_atomic e `{!Atomic e} tid E1 E2 Φ :
(|={E1,E2}=> WP e ∷ tid @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢
WP e ∷ tid @ E1 {{ Φ }}.
Lemma wp_bind K `{!Context K} e tid1 tid2 E Φ :
( if tid2 is Some tid2 then
if tid1 is Some tid1 then
tid1 = tid2
else
False
else
True
) →
WP e ∷ tid2 @ E {{ v, WP K (of_val v) ∷ tid1 @ E {{ Φ }} }} ⊢
WP K e ∷ tid1 @ E {{ Φ }}.
Lemma wp_bind' K `{!Context K} e tid E Φ :
WP e ∷ tid @ E {{ v, WP K (of_val v) ∷ tid @ E {{ Φ }} }} ⊢
WP K e ∷ tid @ E {{ Φ }}.
#[global] Instance frame_wp p e tid E R Φ1 Φ2 :
(∀ v, Frame p R (Φ1 v) (Φ2 v)) →
Frame
p
R
(WP e ∷ tid @ E {{ Φ1 }})
(WP e ∷ tid @ E {{ Φ2 }})
| 2.
#[global] Instance is_except_0_wp e tid E Φ :
IsExcept0 (WP e ∷ tid @ E {{ Φ }}).
#[global] Instance elim_modal_bupd_wp p e tid E P Φ :
ElimModal
True
p
false
(|==> P)
P
(WP e ∷ tid @ E {{ Φ }})
(WP e ∷ tid @ E {{ Φ }}).
#[global] Instance elim_modal_fupd_wp p e tid E P Φ :
ElimModal
True
p
false
(|={E}=> P)
P
(WP e ∷ tid @ E {{ Φ }})
(WP e ∷ tid @ E {{ Φ }}).
#[global] Instance elim_modal_fupd_wp_wrong_mask p e tid E1 E2 P Φ :
ElimModal
(pm_error "Goal and eliminated modality must have the same mask. Use [iApply fupd_wp; iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
p
false
(|={E2}=> P)
False
(WP e ∷ tid @ E1 {{ Φ }})
False
| 100.
#[global] Instance elim_modal_fupd_wp_atomic p e tid E1 E2 P Φ :
ElimModal
(Atomic e)
p
false
(|={E1,E2}=> P)
P
(WP e ∷ tid @ E1 {{ Φ }})
(WP e ∷ tid @ E2 {{ v, |={E2,E1}=> Φ v }})%I
| 100.
#[global] Instance elim_modal_fupd_wp_atomic_wrong_mask p e tid E1 E2 E2' P Φ :
ElimModal
(pm_error "Goal and eliminated modality must have the same mask. Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
p
false
(|={E2,E2'}=> P)
False
(WP e ∷ tid @ E1 {{ Φ }})
False
| 200.
#[global] Instance add_modal_fupd_wp e tid E P Φ :
AddModal
(|={E}=> P)
P
(WP e ∷ tid @ E {{ Φ }}).
#[global] Instance elim_acc_wp_atomic {X} e tid E1 E2 α β γ Φ :
ElimAcc (X := X)
(Atomic e)
(fupd E1 E2)
(fupd E2 E1)
α
β
γ
(WP e ∷ tid @ E1 {{ Φ }})
(λ x, WP e ∷ tid @ E2 {{ v, |={E2}=> β x ∗ (γ x -∗? Φ v) }})%I
| 100.
#[global] Instance elim_acc_wp_nonatomic {X} e tid E α β γ Φ :
ElimAcc (X := X)
True
(fupd E E)
(fupd E E)
α
β
γ
(WP e ∷ tid @ E {{ Φ }})
(λ x, WP e ∷ tid @ E {{ v, |={E}=> β x ∗ (γ x -∗? Φ v) }})%I.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Implicit Types Φ : val → iProp Σ.
Lemma wp_pure_step_strong ϕ n e1 e2 ns tid E Φ :
PureExec ϕ n e1 e2 →
ϕ →
⧖ ns -∗
▷^n (
⧖ (ns + n) -∗
£ (later_sum ns n) -∗
WP e2 ∷ tid @ E {{ Φ }}
) -∗
WP e1 ∷ tid @ E {{ Φ }}.
Lemma wp_pure_step ϕ n e1 e2 tid E Φ :
PureExec ϕ n e1 e2 →
ϕ →
▷^n (
£ (n × later_constant) -∗
WP e2 ∷ tid @ E {{ Φ }}
) ⊢
WP e1 ∷ tid @ E {{ Φ }}.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Lemma wp_equal_nobranch v1 v2 tid E Φ :
▷ (
∀ b,
⌜(if b then (≈) else (≉)) v1 v2⌝ -∗
Φ #b
) ⊢
WP v1 == v2 ∷ tid @ E {{ Φ }}.
Lemma wp_equal v1 v2 tid E Φ :
▷ (
( ⌜v1 ≉ v2⌝ -∗
Φ false%V
) ∧ (
⌜v1 ≈ v2⌝ -∗
Φ true%V
)
) ⊢
WP v1 == v2 ∷ tid @ E {{ Φ }}.
Lemma wp_alloc (tag : Z) n tid E :
(0 ≤ tag)%Z →
(0 ≤ n)%Z →
{{{
True
}}}
Alloc #tag #n ∷ tid @ E
{{{
l
, RET #l;
l ↦ₕ Header ₊tag ₊n ∗
meta_token l ⊤ ∗
l ↦∗ replicate ₊n ()%V
}}}.
Lemma wp_block_mutable {es tag} vs tid E :
0 < length es →
to_vals es = Some vs →
{{{
True
}}}
Block Mutable tag es ∷ tid @ E
{{{
l
, RET #l;
l ↦ₕ Header tag (length es) ∗
meta_token l ⊤ ∗
l ↦∗ vs
}}}.
Lemma wp_block_generative {es tag} vs tid E :
to_vals es = Some vs →
{{{
True
}}}
Block ImmutableGenerativeStrong tag es ∷ tid @ E
{{{
bid
, RET ValBlock (Generative (Some bid)) tag vs;
True
}}}.
Lemma wp_match l hdr x_fb e_fb brs e tid E Φ :
eval_match hdr.(header_tag) hdr.(header_size) (SubjectLoc l) x_fb e_fb brs = Some e →
▷ l ↦ₕ hdr -∗
▷ WP e ∷ tid @ E {{ Φ }} -∗
WP Match #l x_fb e_fb brs ∷ tid @ E {{ Φ }}.
Lemma wp_match_context K `{!Context K} l hdr x_fb e_fb brs e tid E Φ :
eval_match hdr.(header_tag) hdr.(header_size) (SubjectLoc l) x_fb e_fb brs = Some e →
▷ l ↦ₕ hdr -∗
▷ WP K e ∷ tid @ E {{ Φ }} -∗
WP K (Match #l x_fb e_fb brs) ∷ tid @ E {{ Φ }}.
Lemma wp_tag l hdr tid E Φ :
▷ l ↦ₕ hdr -∗
▷ Φ #(encode_tag hdr.(header_tag)) -∗
WP GetTag #l ∷ tid @ E {{ Φ }}.
Lemma wp_size l hdr tid E Φ :
▷ l ↦ₕ hdr -∗
▷ Φ #hdr.(header_size) -∗
WP GetSize #l ∷ tid @ E {{ Φ }}.
Lemma wp_load l fld dq v tid E :
{{{
▷ (l +ₗ fld) ↦{dq} v
}}}
Load #l #fld ∷ tid @ E
{{{
RET v;
(l +ₗ fld) ↦{dq} v
}}}.
Lemma wp_store l fld w v tid E :
{{{
▷ (l +ₗ fld) ↦ w
}}}
Store #l #fld v ∷ tid @ E
{{{
RET ();
(l +ₗ fld) ↦ v
}}}.
Lemma wp_xchg l fld w v tid E :
{{{
▷ (l +ₗ fld) ↦ w
}}}
Xchg (#l, #fld)%V v ∷ tid @ E
{{{
RET w;
(l +ₗ fld) ↦ v
}}}.
Lemma wp_cas_nobranch l fld dq v v1 v2 tid E Φ :
▷ (l +ₗ fld) ↦{dq} v -∗
▷ (
∀ b,
⌜(if b then (≈) else (≉)) v v1⌝ -∗
(l +ₗ fld) ↦{dq} v -∗
⌜if b then dq = DfracOwn 1 else True⌝ ∗
(l +ₗ fld) ↦{dq} v ∗
( (l +ₗ fld) ↦{dq} (if b then v2 else v) -∗
Φ #b
)
) -∗
WP CAS (#l, #fld)%V v1 v2 ∷ tid @ E {{ Φ }}.
Lemma wp_cas_nobranch' l fld v v1 v2 tid E Φ :
▷ (l +ₗ fld) ↦ v -∗
▷ (
∀ b,
⌜(if b then (≈) else (≉)) v v1⌝ -∗
(l +ₗ fld) ↦ (if b then v2 else v) -∗
Φ #b
) -∗
WP CAS (#l, #fld)%V v1 v2 ∷ tid @ E {{ Φ }}.
Lemma wp_cas l fld dq v v1 v2 tid E Φ :
▷ (l +ₗ fld) ↦{dq} v -∗
▷ (
( ⌜v ≉ v1⌝ -∗
(l +ₗ fld) ↦{dq} v -∗
Φ false%V
) ∧ (
⌜v ≈ v1⌝ -∗
(l +ₗ fld) ↦{dq} v -∗
⌜dq = DfracOwn 1⌝ ∗
(l +ₗ fld) ↦{dq} v ∗
( (l +ₗ fld) ↦ v2 -∗
Φ true%V
)
)
) -∗
WP CAS (#l, #fld)%V v1 v2 ∷ tid @ E {{ Φ }}.
Lemma wp_cas' l fld v v1 v2 tid E Φ :
▷ (l +ₗ fld) ↦ v -∗
▷ (
( ⌜v ≉ v1⌝ -∗
(l +ₗ fld) ↦ v -∗
Φ false%V
) ∧ (
⌜v ≈ v1⌝ -∗
(l +ₗ fld) ↦ v2 -∗
Φ true%V
)
) -∗
WP CAS (#l, #fld)%V v1 v2 ∷ tid @ E {{ Φ }}.
Lemma wp_faa l fld (i1 i2 : Z) tid E :
{{{
▷ (l +ₗ fld) ↦ #i1
}}}
FAA (#l, #fld)%V #i2 ∷ tid @ E
{{{
RET #i1;
(l +ₗ fld) ↦ #(i1 + i2)
}}}.
Lemma wp_fork e tid E Φ :
▷ (
∀ tid v,
tid ↦ₗ v -∗
WP e ∶ tid {{ λ _, True }}
) -∗
▷ Φ ()%V -∗
WP Fork e ∷ tid @ E {{ Φ }}.
Lemma wp_get_local tid dq v E :
{{{
▷ tid ↦ₗ{dq} v
}}}
GetLocal ∶ tid @ E
{{{
RET v;
tid ↦ₗ{dq} v
}}}.
Lemma wp_set_local tid w v E :
{{{
▷ tid ↦ₗ w
}}}
SetLocal v ∶ tid @ E
{{{
RET ();
tid ↦ₗ v
}}}.
Lemma wp_proph tid E :
{{{
True
}}}
Proph ∷ tid @ E
{{{
prophs pid
, RET #pid;
prophet_model' pid prophs
}}}.
Lemma wp_resolve e pid v prophs tid E Φ :
Atomic e →
to_val e = None →
prophet_model' pid prophs -∗
WP e ∷ tid @ E {{ res,
∀ prophs',
⌜prophs = (res, v) :: prophs'⌝ -∗
prophet_model' pid prophs' -∗
Φ res
}} -∗
WP Resolve e #pid v ∷ tid @ E {{ Φ }}.
End zoo_G.