Library zoo.program_logic.bwp
Require Export iris.base_logic.lib.fancy_updates.
Require Import zoo.prelude.
Require Import zoo.iris.diaframe.
Require Import zoo.language.tactics.
Require Import zoo.language.notations.
Require Export zoo.program_logic.state_interp.
Require Import zoo.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
| ˖n ⇒
later۰function ns + later۰sum ˖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 ˖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 Type ns nt : nat.
Implicit Type l : location.
Implicit Type pid : prophet_id.
Implicit Type e : expr.
Implicit Type es : list expr.
Implicit Type v : val.
Implicit Type tid : thread_id.
Implicit Type σ : state.
Implicit Type κ κs : list observation.
Section zoo۰G.
Context `{zoo۰G : !ZooG Σ}.
Implicit Type P R : iProp Σ.
Implicit Type Φ : 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 Type Φ : 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' ∗
( ⧖ (˖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' ∗
( ⧖ (˖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' ∗
( ⧖ (˖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' ∗
( ⧖ (˖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⌝ -∗
⧖ (˖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]▷=>
⧖ (˖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 Type Φ : 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' ∗
( ⧖ (˖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' ∗
( ⧖ (˖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' ∗
( ⧖ (˖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.
Require Import zoo.prelude.
Require Import zoo.iris.diaframe.
Require Import zoo.language.tactics.
Require Import zoo.language.notations.
Require Export zoo.program_logic.state_interp.
Require Import zoo.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
| ˖n ⇒
later۰function ns + later۰sum ˖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 ˖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 Type ns nt : nat.
Implicit Type l : location.
Implicit Type pid : prophet_id.
Implicit Type e : expr.
Implicit Type es : list expr.
Implicit Type v : val.
Implicit Type tid : thread_id.
Implicit Type σ : state.
Implicit Type κ κs : list observation.
Section zoo۰G.
Context `{zoo۰G : !ZooG Σ}.
Implicit Type P R : iProp Σ.
Implicit Type Φ : 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 Type Φ : 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' ∗
( ⧖ (˖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' ∗
( ⧖ (˖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' ∗
( ⧖ (˖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' ∗
( ⧖ (˖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⌝ -∗
⧖ (˖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]▷=>
⧖ (˖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 Type Φ : 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' ∗
( ⧖ (˖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' ∗
( ⧖ (˖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' ∗
( ⧖ (˖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.