Library zoo.program_logic.bwp
From iris.base_logic Require Export
lib.fancy_updates.
From zoo Require Import
prelude.
From zoo.iris Require Import
diaframe.
From zoo.language Require Import
tactics
notations.
From zoo.program_logic Require Export
state_interp.
From zoo Require Import
options.
Parameter later_coefficient : nat.
Axiom later_coefficient_lb :
2 ≤ later_coefficient.
#[global] Hint Resolve
later_coefficient_lb
: core.
Parameter later_constant : nat.
Axiom later_constant_lb :
2 ≤ later_constant.
#[global] Hint Resolve
later_constant_lb
: core.
Definition later_function ns :=
later_coefficient × ns + later_constant.
Lemma later_function_lb ns :
later_constant ≤ later_function ns.
Lemma later_function_mono ns1 ns2 :
ns1 ≤ ns2 →
later_function ns1 ≤ later_function ns2.
Lemma later_function_0 :
later_function 0 = later_constant.
#[global] Hint Resolve
later_function_lb
later_function_mono
: core.
Fixpoint later_sum ns n : nat :=
match n with
| 0 ⇒
0
| S n ⇒
later_function ns + later_sum (S ns) n
end.
Lemma later_sum_lb ns n :
n × later_constant ≤ later_sum ns n.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition bwp_pre (bwp : expr -d> thread_id -d> coPset -d> (val -d> iPropO Σ) -d> iPropO Σ)
: expr -d> thread_id -d> coPset -d> (val -d> iPropO Σ) -d> iPropO Σ
:= (
λ e tid E Φ,
∀ ns nt σ κs,
state_interp ns nt σ κs ={E}=∗
match to_val e with
| Some v ⇒
state_interp ns nt σ κs ∗
Φ v
| None ⇒
|={E,∅}=>
⌜reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜prim_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) ={∅}=∗
▷ |={∅,E}=>
state_interp (S ns) (nt + length es) σ' κs' ∗
bwp e' tid E Φ ∗
[∗ list] i ↦ e ∈ es,
bwp e (nt + i) ⊤ fork_post
end
)%I.
#[global] Arguments bwp_pre bwp e%_E tid E Φ%_I : rename.
#[local] Instance bwp_pre_contractive :
Contractive bwp_pre.
#[local] Definition bwp_def
: expr → thread_id → coPset → (val → iProp Σ) → iProp Σ
:=
fixpoint bwp_pre.
#[global] Arguments bwp_def e%_E tid E Φ%_I : rename.
End zoo_G.
#[local] Definition bwp_aux : seal (@bwp_def).
Definition bwp :=
bwp_aux.(unseal).
#[global] Arguments bwp {_ _} e%_E tid E Φ%_I : rename.
#[local] Lemma bwp_unseal `{zoo_G : !ZooG Σ} :
bwp = bwp_def.
Notation "" := (
@top coPset _
)(in custom wp_mask
).
Notation "@ E" :=
E
( in custom wp_mask at level 200,
E constr,
format "'/ ' @ E "
).
Notation "'BWP' e ∶ tid E {{ Φ } }" := (
bwp e%E tid E Φ%I
)(at level 0,
e at level 200,
tid at level 200,
E custom wp_mask at level 200,
Φ at level 200,
format "'[hv' BWP '/ ' '[' e ']' '/ ' ∶ tid E '/' {{ '[' Φ ']' '/' } } ']'"
) : bi_scope.
Notation "'BWP' e ∶ tid E {{ v , Q } }" := (
bwp e%E tid E (λ v, Q%I)
)(at level 0,
e at level 200,
tid at level 200,
E custom wp_mask at level 200,
v at level 200 as pattern,
Q at level 200,
format "'[hv' BWP '/ ' '[' e ']' '/ ' ∶ tid E '/' {{ '[' v , '/' Q ']' '/' } } ']'"
) : bi_scope.
Implicit Types ns nt : nat.
Implicit Types l : location.
Implicit Types pid : prophet_id.
Implicit Types e : expr.
Implicit Types es : list expr.
Implicit Types v : val.
Implicit Types tid : thread_id.
Implicit Types σ : state.
Implicit Types κ κs : list observation.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Implicit Types P R : iProp Σ.
Implicit Types Φ : val → iProp Σ.
Lemma bwp_unfold e tid E Φ :
BWP e ∶ tid @ E {{ Φ }} ⊣⊢
bwp_pre bwp e tid E Φ.
#[global] Instance bwp_ne e tid E n :
Proper (pointwise_relation _ (≡{n}≡) ==> (≡{n}≡)) (bwp e tid E).
#[global] Instance bwp_proper e tid E :
Proper (pointwise_relation _ (≡) ==> (≡)) (bwp e tid E).
#[global] Instance bwp_contractive e tid E n :
TCEq (to_val e) None →
Proper (pointwise_relation _ (dist_later n) ==> (≡{n}≡)) (bwp e tid E).
Lemma bwp_state_interp e tid E Φ :
( ∀ ns nt σ κs,
state_interp ns nt σ κs ={E}=∗
state_interp ns nt σ κs ∗
BWP e ∶ tid @ E {{ Φ }}
) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_value_fupd' v tid E Φ :
(|={E}=> Φ v) ⊢
BWP of_val v ∶ tid @ E {{ Φ }}.
Lemma bwp_value_fupd e v tid E Φ :
AsVal e v →
(|={E}=> Φ v) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_value' v tid E Φ :
Φ v ⊢
BWP of_val v ∶ tid @ E {{ Φ }}.
Lemma bwp_value e v tid E Φ :
AsVal e v →
Φ v ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_value_mono v tid E Φ1 Φ2 :
BWP of_val v ∶ tid @ E {{ Φ1 }} -∗
(Φ1 v ={E}=∗ Φ2 v) -∗
BWP of_val v ∶ tid @ E {{ Φ2 }}.
Lemma bwp_strong_mono e tid E1 Φ1 E2 Φ2 :
E1 ⊆ E2 →
BWP e ∶ tid @ E1 {{ Φ1 }} -∗
(∀ v, Φ1 v ={E2}=∗ Φ2 v) -∗
BWP e ∶ tid @ E2 {{ Φ2 }}.
Lemma bwp_mono e tid E Φ1 Φ2 :
(∀ v, Φ1 v ⊢ Φ2 v) →
BWP e ∶ tid @ E {{ Φ1 }} ⊢
BWP e ∶ tid @ E {{ Φ2 }}.
#[global] Instance bwp_mono' e tid E :
Proper (pointwise_relation _ (⊢) ==> (⊢)) (bwp e tid E).
#[global] Instance bwp_flip_mono' e tid E :
Proper (pointwise_relation _ (flip (⊢)) ==> (flip (⊢))) (bwp e tid E).
Lemma fupd_bwp e tid E Φ :
(|={E}=> BWP e ∶ tid @ E {{ Φ }}) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_fupd e tid E Φ :
BWP e ∶ tid @ E {{ v, |={E}=> Φ v }} ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_frame_l e tid E Φ R :
R ∗ BWP e ∶ tid @ E {{ Φ }} ⊢
BWP e ∶ tid @ E {{ v, R ∗ Φ v }}.
Lemma bwp_frame_r e tid E Φ R :
BWP e ∶ tid @ E {{ Φ }} ∗ R ⊢
BWP e ∶ tid @ E {{ v, Φ v ∗ R }}.
Lemma bwp_wand {e tid E} Φ1 Φ2 :
BWP e ∶ tid @ E {{ Φ1 }} -∗
(∀ v, Φ1 v -∗ Φ2 v) -∗
BWP e ∶ tid @ E {{ Φ2 }}.
Lemma bwp_frame_wand e tid E Φ R :
R -∗
BWP e ∶ tid @ E {{ v, R -∗ Φ v }} -∗
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_atomic e `{!Atomic e} tid E1 E2 Φ :
(|={E1,E2}=> BWP e ∶ tid @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢
BWP e ∶ tid @ E1 {{ Φ }}.
Lemma bwp_bind K `{!Context K} e tid E Φ :
BWP e ∶ tid @ E {{ v, BWP K (of_val v) ∶ tid @ E {{ Φ }} }} ⊢
BWP K e ∶ tid @ E {{ Φ }}.
Lemma bwp_bind_inv K `{!Context K} e tid E Φ :
BWP K e ∶ tid @ E {{ Φ }} ⊢
BWP e ∶ tid @ E {{ v, BWP K (of_val v) ∶ tid @ E {{ Φ }} }}.
#[global] Instance frame_bwp p e tid E R Φ1 Φ2 :
(∀ v, Frame p R (Φ1 v) (Φ2 v)) →
Frame
p
R
(BWP e ∶ tid @ E {{ Φ1 }})
(BWP e ∶ tid @ E {{ Φ2 }})
| 2.
#[global] Instance is_except_0_bwp e tid E Φ :
IsExcept0 (BWP e ∶ tid @ E {{ Φ }}).
#[global] Instance elim_modal_bupd_bwp p e tid E P Φ :
ElimModal
True
p
false
(|==> P)
P
(BWP e ∶ tid @ E {{ Φ }})
(BWP e ∶ tid @ E {{ Φ }}).
#[global] Instance elim_modal_fupd_bwp p e tid E P Φ :
ElimModal
True
p
false
(|={E}=> P)
P
(BWP e ∶ tid @ E {{ Φ }})
(BWP e ∶ tid @ E {{ Φ }}).
#[global] Instance elim_modal_fupd_bwp_wrong_mask p e tid E1 E2 P Φ :
ElimModal
(pm_error "Goal and eliminated modality must have the same mask. Use [iApply fupd_bwp; iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
p
false
(|={E2}=> P)
False
(BWP e ∶ tid @ E1 {{ Φ }})
False
| 100.
#[global] Instance elim_modal_fupd_bwp_atomic p e tid E1 E2 P Φ :
ElimModal
(Atomic e)
p
false
(|={E1,E2}=> P)
P
(BWP e ∶ tid @ E1 {{ Φ }})
(BWP e ∶ tid @ E2 {{ v, |={E2,E1}=> Φ v }})%I
| 100.
#[global] Instance elim_modal_fupd_bwp_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
(BWP e ∶ tid @ E1 {{ Φ }})
False
| 200.
#[global] Instance add_modal_fupd_bwp e tid E P Φ :
AddModal
(|={E}=> P)
P
(BWP e ∶ tid @ E {{ Φ }}).
#[global] Instance elim_acc_bwp_atomic {X} e tid E1 E2 α β γ Φ :
ElimAcc (X := X)
(Atomic e)
(fupd E1 E2)
(fupd E2 E1)
α
β
γ
(BWP e ∶ tid @ E1 {{ Φ }})
(λ x, BWP e ∶ tid @ E2 {{ v, |={E2}=> β x ∗ (γ x -∗? Φ v) }})%I
| 100.
#[global] Instance elim_acc_bwp_nonatomic {X} e tid E α β γ Φ :
ElimAcc (X := X)
True
(fupd E E)
(fupd E E)
α
β
γ
(BWP e ∶ tid @ E {{ Φ }})
(λ x, BWP e ∶ tid @ E {{ v, |={E}=> β x ∗ (γ x -∗? Φ v) }})%I.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Implicit Types Φ : val → iProp Σ.
Lemma bwp_lift_step e tid E Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs -∗
|={E, ∅}=>
⌜reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜prim_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) ={∅}=∗
▷ |={∅, E}=>
state_interp ns (nt + length es) σ' κs' ∗
( ⧖ (S ns) -∗
BWP e' ∶ tid @ E {{ Φ }} ∗
[∗ list] i ↦ e ∈ es,
BWP e ∶ nt + i {{ fork_post }}
)
) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_lift_step_nofork e tid E Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs -∗
|={E, ∅}=>
⌜reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜prim_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) ={∅}=∗
▷ |={∅, E}=>
⌜es = []⌝ ∗
state_interp ns nt σ' κs' ∗
( ⧖ (S ns) -∗
BWP e' ∶ tid @ E {{ Φ }}
)
) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_lift_atomic_step e tid E1 E2 Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs ={E1}=∗
⌜reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜prim_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) -∗
|={E1}[E2]▷=>
state_interp ns (nt + length es) σ' κs' ∗
( ⧖ (S ns) -∗
from_option Φ False (to_val e') ∗
[∗ list] i ↦ e ∈ es,
BWP e ∶ nt + i {{ fork_post }}
)
) ⊢
BWP e ∶ tid @ E1 {{ Φ }}.
Lemma bwp_lift_atomic_step_nofork e tid E1 E2 Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs ={E1}=∗
⌜reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜prim_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) -∗
|={E1}[E2]▷=>
⌜es = []⌝ ∗
state_interp ns nt σ' κs' ∗
( ⧖ (S ns) -∗
from_option Φ False (to_val e')
)
) ⊢
BWP e ∶ tid @ E1 {{ Φ }}.
Lemma bwp_lift_pure_step_nofork e tid ns E1 E2 Φ :
( ∀ σ,
reducible tid e σ
) →
( ∀ σ κ e' σ' es,
prim_step tid e σ κ e' σ' es →
κ = [] ∧
σ' = σ ∧
es = []
) →
⧖ ns -∗
( |={E1}[E2]▷=>
∀ σ e' κ es,
⌜prim_step tid e σ κ e' σ es⌝ -∗
⧖ (S ns) -∗
£ (later_function ns) -∗
BWP e' ∶ tid @ E1 {{ Φ }}
) -∗
BWP e ∶ tid @ E1 {{ Φ }}.
Lemma bwp_lift_pure_det_step_nofork e1 e2 tid ns E1 E2 Φ :
( ∀ σ1,
reducible tid e1 σ1
) →
( ∀ σ1 κ e2' σ2 es,
prim_step tid e1 σ1 κ e2' σ2 es →
κ = [] ∧
σ2 = σ1 ∧
e2' = e2 ∧
es = []
) →
⧖ ns -∗
( |={E1}[E2]▷=>
⧖ (S ns) -∗
£ (later_function ns) -∗
BWP e2 ∶ tid @ E1 {{ Φ }}
) -∗
BWP e1 ∶ tid @ E1 {{ Φ }}.
Lemma bwp_pure_step ϕ n e1 e2 ns tid E Φ :
PureExec ϕ n e1 e2 →
ϕ →
⧖ ns -∗
▷^n (
⧖ (ns + n) -∗
£ (later_sum ns n) -∗
BWP e2 ∶ tid @ E {{ Φ }}
) -∗
BWP e1 ∶ tid @ E {{ Φ }}.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Implicit Types Φ : val → iProp Σ.
#[local] Hint Resolve
base_reducible_reducible
base_reducible_prim_step
: core.
Lemma bwp_lift_base_step e tid E Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs -∗
|={E, ∅}=>
⌜base_reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜base_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) ={∅}=∗
▷ |={∅, E}=>
state_interp ns (nt + length es) σ' κs' ∗
( ⧖ (S ns) -∗
BWP e' ∶ tid @ E {{ Φ }} ∗
[∗ list] i ↦ e ∈ es,
BWP e ∶ nt + i {{ fork_post }}
)
) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_lift_base_step_nofork e tid E Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs -∗
|={E, ∅}=>
⌜base_reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜base_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) ={∅}=∗
▷ |={∅, E}=>
⌜es = []⌝ ∗
state_interp ns nt σ' κs' ∗
( ⧖ ns -∗
BWP e' ∶ tid @ E {{ Φ }}
)
) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_lift_atomic_base_step e tid E1 E2 Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs -∗
|={E1}=>
⌜base_reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜base_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) -∗
|={E1}[E2]▷=>
state_interp ns (nt + length es) σ' κs' ∗
( ⧖ (S ns) -∗
from_option Φ False (to_val e') ∗
[∗ list] i ↦ e ∈ es,
BWP e ∶ nt + i {{ fork_post }}
)
) ⊢
BWP e ∶ tid @ E1 {{ Φ }}.
Lemma bwp_lift_atomic_base_step_nofork e tid E1 E2 Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs -∗
|={E1}=>
⌜base_reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜base_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) -∗
|={E1}[E2]▷=>
⌜es = []⌝ ∗
state_interp ns nt σ' κs' ∗
( ⧖ (S ns) -∗
from_option Φ False (to_val e')
)
) ⊢
BWP e ∶ tid @ E1 {{ Φ }}.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Lemma bwp_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 -∗
▷ BWP e ∶ tid @ E {{ Φ }} -∗
BWP Match #l x_fb e_fb brs ∶ tid @ E {{ Φ }}.
Lemma bwp_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 -∗
▷ BWP K e ∶ tid @ E {{ Φ }} -∗
BWP K (Match #l x_fb e_fb brs) ∶ tid @ E {{ Φ }}.
Lemma bwp_resolve e pid v prophs tid E Φ :
Atomic e →
to_val e = None →
prophet_model' pid prophs -∗
BWP e ∶ tid @ E {{ res,
∀ prophs',
⌜prophs = (res, v) :: prophs'⌝ -∗
prophet_model' pid prophs' -∗
Φ res
}} -∗
BWP Resolve e #pid v ∶ tid @ E {{ Φ }}.
End zoo_G.
lib.fancy_updates.
From zoo Require Import
prelude.
From zoo.iris Require Import
diaframe.
From zoo.language Require Import
tactics
notations.
From zoo.program_logic Require Export
state_interp.
From zoo Require Import
options.
Parameter later_coefficient : nat.
Axiom later_coefficient_lb :
2 ≤ later_coefficient.
#[global] Hint Resolve
later_coefficient_lb
: core.
Parameter later_constant : nat.
Axiom later_constant_lb :
2 ≤ later_constant.
#[global] Hint Resolve
later_constant_lb
: core.
Definition later_function ns :=
later_coefficient × ns + later_constant.
Lemma later_function_lb ns :
later_constant ≤ later_function ns.
Lemma later_function_mono ns1 ns2 :
ns1 ≤ ns2 →
later_function ns1 ≤ later_function ns2.
Lemma later_function_0 :
later_function 0 = later_constant.
#[global] Hint Resolve
later_function_lb
later_function_mono
: core.
Fixpoint later_sum ns n : nat :=
match n with
| 0 ⇒
0
| S n ⇒
later_function ns + later_sum (S ns) n
end.
Lemma later_sum_lb ns n :
n × later_constant ≤ later_sum ns n.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition bwp_pre (bwp : expr -d> thread_id -d> coPset -d> (val -d> iPropO Σ) -d> iPropO Σ)
: expr -d> thread_id -d> coPset -d> (val -d> iPropO Σ) -d> iPropO Σ
:= (
λ e tid E Φ,
∀ ns nt σ κs,
state_interp ns nt σ κs ={E}=∗
match to_val e with
| Some v ⇒
state_interp ns nt σ κs ∗
Φ v
| None ⇒
|={E,∅}=>
⌜reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜prim_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) ={∅}=∗
▷ |={∅,E}=>
state_interp (S ns) (nt + length es) σ' κs' ∗
bwp e' tid E Φ ∗
[∗ list] i ↦ e ∈ es,
bwp e (nt + i) ⊤ fork_post
end
)%I.
#[global] Arguments bwp_pre bwp e%_E tid E Φ%_I : rename.
#[local] Instance bwp_pre_contractive :
Contractive bwp_pre.
#[local] Definition bwp_def
: expr → thread_id → coPset → (val → iProp Σ) → iProp Σ
:=
fixpoint bwp_pre.
#[global] Arguments bwp_def e%_E tid E Φ%_I : rename.
End zoo_G.
#[local] Definition bwp_aux : seal (@bwp_def).
Definition bwp :=
bwp_aux.(unseal).
#[global] Arguments bwp {_ _} e%_E tid E Φ%_I : rename.
#[local] Lemma bwp_unseal `{zoo_G : !ZooG Σ} :
bwp = bwp_def.
Notation "" := (
@top coPset _
)(in custom wp_mask
).
Notation "@ E" :=
E
( in custom wp_mask at level 200,
E constr,
format "'/ ' @ E "
).
Notation "'BWP' e ∶ tid E {{ Φ } }" := (
bwp e%E tid E Φ%I
)(at level 0,
e at level 200,
tid at level 200,
E custom wp_mask at level 200,
Φ at level 200,
format "'[hv' BWP '/ ' '[' e ']' '/ ' ∶ tid E '/' {{ '[' Φ ']' '/' } } ']'"
) : bi_scope.
Notation "'BWP' e ∶ tid E {{ v , Q } }" := (
bwp e%E tid E (λ v, Q%I)
)(at level 0,
e at level 200,
tid at level 200,
E custom wp_mask at level 200,
v at level 200 as pattern,
Q at level 200,
format "'[hv' BWP '/ ' '[' e ']' '/ ' ∶ tid E '/' {{ '[' v , '/' Q ']' '/' } } ']'"
) : bi_scope.
Implicit Types ns nt : nat.
Implicit Types l : location.
Implicit Types pid : prophet_id.
Implicit Types e : expr.
Implicit Types es : list expr.
Implicit Types v : val.
Implicit Types tid : thread_id.
Implicit Types σ : state.
Implicit Types κ κs : list observation.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Implicit Types P R : iProp Σ.
Implicit Types Φ : val → iProp Σ.
Lemma bwp_unfold e tid E Φ :
BWP e ∶ tid @ E {{ Φ }} ⊣⊢
bwp_pre bwp e tid E Φ.
#[global] Instance bwp_ne e tid E n :
Proper (pointwise_relation _ (≡{n}≡) ==> (≡{n}≡)) (bwp e tid E).
#[global] Instance bwp_proper e tid E :
Proper (pointwise_relation _ (≡) ==> (≡)) (bwp e tid E).
#[global] Instance bwp_contractive e tid E n :
TCEq (to_val e) None →
Proper (pointwise_relation _ (dist_later n) ==> (≡{n}≡)) (bwp e tid E).
Lemma bwp_state_interp e tid E Φ :
( ∀ ns nt σ κs,
state_interp ns nt σ κs ={E}=∗
state_interp ns nt σ κs ∗
BWP e ∶ tid @ E {{ Φ }}
) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_value_fupd' v tid E Φ :
(|={E}=> Φ v) ⊢
BWP of_val v ∶ tid @ E {{ Φ }}.
Lemma bwp_value_fupd e v tid E Φ :
AsVal e v →
(|={E}=> Φ v) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_value' v tid E Φ :
Φ v ⊢
BWP of_val v ∶ tid @ E {{ Φ }}.
Lemma bwp_value e v tid E Φ :
AsVal e v →
Φ v ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_value_mono v tid E Φ1 Φ2 :
BWP of_val v ∶ tid @ E {{ Φ1 }} -∗
(Φ1 v ={E}=∗ Φ2 v) -∗
BWP of_val v ∶ tid @ E {{ Φ2 }}.
Lemma bwp_strong_mono e tid E1 Φ1 E2 Φ2 :
E1 ⊆ E2 →
BWP e ∶ tid @ E1 {{ Φ1 }} -∗
(∀ v, Φ1 v ={E2}=∗ Φ2 v) -∗
BWP e ∶ tid @ E2 {{ Φ2 }}.
Lemma bwp_mono e tid E Φ1 Φ2 :
(∀ v, Φ1 v ⊢ Φ2 v) →
BWP e ∶ tid @ E {{ Φ1 }} ⊢
BWP e ∶ tid @ E {{ Φ2 }}.
#[global] Instance bwp_mono' e tid E :
Proper (pointwise_relation _ (⊢) ==> (⊢)) (bwp e tid E).
#[global] Instance bwp_flip_mono' e tid E :
Proper (pointwise_relation _ (flip (⊢)) ==> (flip (⊢))) (bwp e tid E).
Lemma fupd_bwp e tid E Φ :
(|={E}=> BWP e ∶ tid @ E {{ Φ }}) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_fupd e tid E Φ :
BWP e ∶ tid @ E {{ v, |={E}=> Φ v }} ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_frame_l e tid E Φ R :
R ∗ BWP e ∶ tid @ E {{ Φ }} ⊢
BWP e ∶ tid @ E {{ v, R ∗ Φ v }}.
Lemma bwp_frame_r e tid E Φ R :
BWP e ∶ tid @ E {{ Φ }} ∗ R ⊢
BWP e ∶ tid @ E {{ v, Φ v ∗ R }}.
Lemma bwp_wand {e tid E} Φ1 Φ2 :
BWP e ∶ tid @ E {{ Φ1 }} -∗
(∀ v, Φ1 v -∗ Φ2 v) -∗
BWP e ∶ tid @ E {{ Φ2 }}.
Lemma bwp_frame_wand e tid E Φ R :
R -∗
BWP e ∶ tid @ E {{ v, R -∗ Φ v }} -∗
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_atomic e `{!Atomic e} tid E1 E2 Φ :
(|={E1,E2}=> BWP e ∶ tid @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢
BWP e ∶ tid @ E1 {{ Φ }}.
Lemma bwp_bind K `{!Context K} e tid E Φ :
BWP e ∶ tid @ E {{ v, BWP K (of_val v) ∶ tid @ E {{ Φ }} }} ⊢
BWP K e ∶ tid @ E {{ Φ }}.
Lemma bwp_bind_inv K `{!Context K} e tid E Φ :
BWP K e ∶ tid @ E {{ Φ }} ⊢
BWP e ∶ tid @ E {{ v, BWP K (of_val v) ∶ tid @ E {{ Φ }} }}.
#[global] Instance frame_bwp p e tid E R Φ1 Φ2 :
(∀ v, Frame p R (Φ1 v) (Φ2 v)) →
Frame
p
R
(BWP e ∶ tid @ E {{ Φ1 }})
(BWP e ∶ tid @ E {{ Φ2 }})
| 2.
#[global] Instance is_except_0_bwp e tid E Φ :
IsExcept0 (BWP e ∶ tid @ E {{ Φ }}).
#[global] Instance elim_modal_bupd_bwp p e tid E P Φ :
ElimModal
True
p
false
(|==> P)
P
(BWP e ∶ tid @ E {{ Φ }})
(BWP e ∶ tid @ E {{ Φ }}).
#[global] Instance elim_modal_fupd_bwp p e tid E P Φ :
ElimModal
True
p
false
(|={E}=> P)
P
(BWP e ∶ tid @ E {{ Φ }})
(BWP e ∶ tid @ E {{ Φ }}).
#[global] Instance elim_modal_fupd_bwp_wrong_mask p e tid E1 E2 P Φ :
ElimModal
(pm_error "Goal and eliminated modality must have the same mask. Use [iApply fupd_bwp; iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
p
false
(|={E2}=> P)
False
(BWP e ∶ tid @ E1 {{ Φ }})
False
| 100.
#[global] Instance elim_modal_fupd_bwp_atomic p e tid E1 E2 P Φ :
ElimModal
(Atomic e)
p
false
(|={E1,E2}=> P)
P
(BWP e ∶ tid @ E1 {{ Φ }})
(BWP e ∶ tid @ E2 {{ v, |={E2,E1}=> Φ v }})%I
| 100.
#[global] Instance elim_modal_fupd_bwp_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
(BWP e ∶ tid @ E1 {{ Φ }})
False
| 200.
#[global] Instance add_modal_fupd_bwp e tid E P Φ :
AddModal
(|={E}=> P)
P
(BWP e ∶ tid @ E {{ Φ }}).
#[global] Instance elim_acc_bwp_atomic {X} e tid E1 E2 α β γ Φ :
ElimAcc (X := X)
(Atomic e)
(fupd E1 E2)
(fupd E2 E1)
α
β
γ
(BWP e ∶ tid @ E1 {{ Φ }})
(λ x, BWP e ∶ tid @ E2 {{ v, |={E2}=> β x ∗ (γ x -∗? Φ v) }})%I
| 100.
#[global] Instance elim_acc_bwp_nonatomic {X} e tid E α β γ Φ :
ElimAcc (X := X)
True
(fupd E E)
(fupd E E)
α
β
γ
(BWP e ∶ tid @ E {{ Φ }})
(λ x, BWP e ∶ tid @ E {{ v, |={E}=> β x ∗ (γ x -∗? Φ v) }})%I.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Implicit Types Φ : val → iProp Σ.
Lemma bwp_lift_step e tid E Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs -∗
|={E, ∅}=>
⌜reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜prim_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) ={∅}=∗
▷ |={∅, E}=>
state_interp ns (nt + length es) σ' κs' ∗
( ⧖ (S ns) -∗
BWP e' ∶ tid @ E {{ Φ }} ∗
[∗ list] i ↦ e ∈ es,
BWP e ∶ nt + i {{ fork_post }}
)
) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_lift_step_nofork e tid E Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs -∗
|={E, ∅}=>
⌜reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜prim_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) ={∅}=∗
▷ |={∅, E}=>
⌜es = []⌝ ∗
state_interp ns nt σ' κs' ∗
( ⧖ (S ns) -∗
BWP e' ∶ tid @ E {{ Φ }}
)
) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_lift_atomic_step e tid E1 E2 Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs ={E1}=∗
⌜reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜prim_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) -∗
|={E1}[E2]▷=>
state_interp ns (nt + length es) σ' κs' ∗
( ⧖ (S ns) -∗
from_option Φ False (to_val e') ∗
[∗ list] i ↦ e ∈ es,
BWP e ∶ nt + i {{ fork_post }}
)
) ⊢
BWP e ∶ tid @ E1 {{ Φ }}.
Lemma bwp_lift_atomic_step_nofork e tid E1 E2 Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs ={E1}=∗
⌜reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜prim_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) -∗
|={E1}[E2]▷=>
⌜es = []⌝ ∗
state_interp ns nt σ' κs' ∗
( ⧖ (S ns) -∗
from_option Φ False (to_val e')
)
) ⊢
BWP e ∶ tid @ E1 {{ Φ }}.
Lemma bwp_lift_pure_step_nofork e tid ns E1 E2 Φ :
( ∀ σ,
reducible tid e σ
) →
( ∀ σ κ e' σ' es,
prim_step tid e σ κ e' σ' es →
κ = [] ∧
σ' = σ ∧
es = []
) →
⧖ ns -∗
( |={E1}[E2]▷=>
∀ σ e' κ es,
⌜prim_step tid e σ κ e' σ es⌝ -∗
⧖ (S ns) -∗
£ (later_function ns) -∗
BWP e' ∶ tid @ E1 {{ Φ }}
) -∗
BWP e ∶ tid @ E1 {{ Φ }}.
Lemma bwp_lift_pure_det_step_nofork e1 e2 tid ns E1 E2 Φ :
( ∀ σ1,
reducible tid e1 σ1
) →
( ∀ σ1 κ e2' σ2 es,
prim_step tid e1 σ1 κ e2' σ2 es →
κ = [] ∧
σ2 = σ1 ∧
e2' = e2 ∧
es = []
) →
⧖ ns -∗
( |={E1}[E2]▷=>
⧖ (S ns) -∗
£ (later_function ns) -∗
BWP e2 ∶ tid @ E1 {{ Φ }}
) -∗
BWP e1 ∶ tid @ E1 {{ Φ }}.
Lemma bwp_pure_step ϕ n e1 e2 ns tid E Φ :
PureExec ϕ n e1 e2 →
ϕ →
⧖ ns -∗
▷^n (
⧖ (ns + n) -∗
£ (later_sum ns n) -∗
BWP e2 ∶ tid @ E {{ Φ }}
) -∗
BWP e1 ∶ tid @ E {{ Φ }}.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Implicit Types Φ : val → iProp Σ.
#[local] Hint Resolve
base_reducible_reducible
base_reducible_prim_step
: core.
Lemma bwp_lift_base_step e tid E Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs -∗
|={E, ∅}=>
⌜base_reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜base_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) ={∅}=∗
▷ |={∅, E}=>
state_interp ns (nt + length es) σ' κs' ∗
( ⧖ (S ns) -∗
BWP e' ∶ tid @ E {{ Φ }} ∗
[∗ list] i ↦ e ∈ es,
BWP e ∶ nt + i {{ fork_post }}
)
) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_lift_base_step_nofork e tid E Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs -∗
|={E, ∅}=>
⌜base_reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜base_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) ={∅}=∗
▷ |={∅, E}=>
⌜es = []⌝ ∗
state_interp ns nt σ' κs' ∗
( ⧖ ns -∗
BWP e' ∶ tid @ E {{ Φ }}
)
) ⊢
BWP e ∶ tid @ E {{ Φ }}.
Lemma bwp_lift_atomic_base_step e tid E1 E2 Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs -∗
|={E1}=>
⌜base_reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜base_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) -∗
|={E1}[E2]▷=>
state_interp ns (nt + length es) σ' κs' ∗
( ⧖ (S ns) -∗
from_option Φ False (to_val e') ∗
[∗ list] i ↦ e ∈ es,
BWP e ∶ nt + i {{ fork_post }}
)
) ⊢
BWP e ∶ tid @ E1 {{ Φ }}.
Lemma bwp_lift_atomic_base_step_nofork e tid E1 E2 Φ :
to_val e = None →
( ∀ ns nt σ κs,
state_interp ns nt σ κs -∗
|={E1}=>
⌜base_reducible tid e σ⌝ ∗
∀ κ κs' e' σ' es,
⌜κs = κ ++ κs'⌝ -∗
⌜base_step tid e σ κ e' σ' es⌝ -∗
£ (later_function ns) -∗
|={E1}[E2]▷=>
⌜es = []⌝ ∗
state_interp ns nt σ' κs' ∗
( ⧖ (S ns) -∗
from_option Φ False (to_val e')
)
) ⊢
BWP e ∶ tid @ E1 {{ Φ }}.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Lemma bwp_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 -∗
▷ BWP e ∶ tid @ E {{ Φ }} -∗
BWP Match #l x_fb e_fb brs ∶ tid @ E {{ Φ }}.
Lemma bwp_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 -∗
▷ BWP K e ∶ tid @ E {{ Φ }} -∗
BWP K (Match #l x_fb e_fb brs) ∶ tid @ E {{ Φ }}.
Lemma bwp_resolve e pid v prophs tid E Φ :
Atomic e →
to_val e = None →
prophet_model' pid prophs -∗
BWP e ∶ tid @ E {{ res,
∀ prophs',
⌜prophs = (res, v) :: prophs'⌝ -∗
prophet_model' pid prophs' -∗
Φ res
}} -∗
BWP Resolve e #pid v ∶ tid @ E {{ Φ }}.
End zoo_G.