Commit 65081e7d authored by Zhen Zhang's avatar Zhen Zhang

add quirky spec

parent ec2684b0
From iris.program_logic Require Export auth weakestpre saved_prop.
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
......@@ -407,12 +406,11 @@ Section proof.
Qed.
Definition flatten (f' f: val) :=
( P Q, ( x:val, {{ R P x }} f x {{ v, R Q x v }})
( x:val, {{ P x }} f' x {{ v, Q x v }}))%I.
( P Q (x: val), ({{ R P x }} f x {{ v, R Q x v }}) ({{ P x }} f' x {{ v, Q x v }}))%I.
Lemma mk_flat_spec (f: val) :
(Φ: val iProp Σ),
heapN N
heapN N
heap_ctx R ( f', flatten f' f - Φ f') WP mk_flat f {{ Φ }}.
Proof.
iIntros (Φ HN) "(#Hh & HR & HΦ)".
......@@ -427,8 +425,8 @@ Section proof.
iApply (new_stack_spec' _ (p_inv γm γr f))=>//.
iFrame "Hh Hm". iIntros (γ s) "#Hss".
wp_let. iVsIntro. iApply "HΦ". rewrite /flatten.
iAlways. iIntros (P Q) "#Hf".
iIntros (x) "!# Hp". wp_let.
iAlways. iIntros (P Q x) "#Hf".
iIntros "!# Hp". wp_let.
wp_bind ((install _) _).
iApply (install_spec _ P Q)=>//.
iFrame "#". iFrame "Hp". iSplitR; first iApply "Hf".
......@@ -439,10 +437,108 @@ Section proof.
iDestruct "Hs" as (Q') "(Hx' & HoQ' & HQ')".
destruct (decide (x = a)) as [->|Hneq].
- iDestruct (saved_prop_agree with "[HoQ HoQ']") as "Heq"; first by iFrame.
iNext. admit. (* iRewrite "Heq" in "HQ'". *)
iNext. iDestruct (uPred.cofe_funC_equivI with "Heq") as "Heq".
iSpecialize ("Heq" $! a0). by iRewrite "Heq" in "HQ'".
- iExFalso. iCombine "Hx" "Hx'" as "Hx".
iDestruct (own_valid with "Hx") as %[_ H1].
rewrite pair_op //= dec_agree_ne in H1=>//.
Admitted.
Qed.
End proof.
Definition syncR := prodR fracR (dec_agreeR val). (* FIXME: can't use a general A instead of val *)
Class syncG Σ := sync_tokG :> inG Σ syncR.
Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
Instance subG_syncΣ {Σ} : subG syncΣ Σ syncG Σ.
Proof. by intros ?%subG_inG. Qed.
Section atomic_sync.
Context `{!heapG Σ, !lockG Σ, !syncG Σ, !evidenceG loc val Σ, !flatG Σ} (N : namespace).
Definition A := val.
Definition gFragR g : syncR := ((1/2)%Qp, DecAgree g).
Definition gFullR g : syncR := ((1/2)%Qp, DecAgree g).
Definition gFrag (γ: gname) g : iProp Σ := own γ (gFragR g).
Definition gFull (γ: gname) g : iProp Σ := own γ (gFullR g).
Global Instance frag_timeless γ g: TimelessP (gFrag γ g).
Proof. apply _. Qed.
Global Instance full_timeless γ g: TimelessP (gFull γ g).
Proof. apply _. Qed.
Definition atomic_triple'
(α: val iProp Σ)
(β: val A A val iProp Σ)
(Ei Eo: coPset)
(f x: val) γ : iProp Σ :=
( P Q, ( g, (P x ={Eo, Ei}=> gFrag γ g α x)
(gFrag γ g α x ={Ei, Eo}=> P x)
( g' r, gFrag γ g' β x g g' r ={Ei, Eo}=> Q x r))
- {{ P x }} f x {{ v, Q x v }})%I.
Definition sync : val :=
λ: "f_cons" "f_seq",
let: "l" := "f_cons" #() in
mk_flat ("f_seq" "l").
Definition seq_spec (f: val) (ϕ: val A iProp Σ) α β (E: coPset) :=
(Φ: val iProp Σ) (l: val),
{{ True }} f l {{ f', ( (x: val) (Φ: val iProp Σ) (g: A),
heapN N
heap_ctx ϕ l g α x
( (v: val) (g': A), ϕ l g' - β x g g' v - |={E}=> Φ v)
WP f' x @ E {{ Φ }} )}}.
Definition cons_spec (f: val) (g: A) ϕ :=
Φ: val iProp Σ, heapN N
heap_ctx ( (l: val) (γ: gname), ϕ l g - gFull γ g - gFrag γ g - Φ l)
WP f #() {{ Φ }}.
Lemma atomic_spec (f_cons f_seq: val) (ϕ: val A iProp Σ) α β Ei:
(g0: A),
heapN N seq_spec f_seq ϕ α β cons_spec f_cons g0 ϕ
heap_ctx
WP sync f_cons f_seq {{ f, γ, gFrag γ g0 x, atomic_triple' α β Ei f x γ }}.
Proof.
iIntros (g0 HN Hseq Hcons) "#Hh". repeat wp_let.
wp_bind (f_cons _). iApply Hcons=>//. iFrame "Hh".
iIntros (l γ) "Hϕ HFull HFrag".
wp_let. wp_bind (f_seq _)%E.
iApply wp_wand_r. iSplitR; first by iApply (Hseq with "[]")=>//.
iIntros (f Hf). iApply (mk_flat_spec _ ( g: A, ϕ l g gFull γ g)%I)=>//.
iFrame "#". iSplitL "HFull Hϕ".
{ iExists g0. by iFrame. }
iIntros (f') "#Hflatten".
iExists γ. iFrame.
iIntros (x). iAlways.
rewrite /atomic_triple'.
iIntros (P Q) "#Hvss".
rewrite /flatten.
iSpecialize ("Hflatten" $! P Q).
iApply ("Hflatten" with "[]").
iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ HgFull]".
(* we should view shift at this point *)
iDestruct ("Hvss" $! g) as "[Hvs1 [Hvs2 Hvs3]]".
iApply pvs_wp.
iVs ("Hvs1" with "HP") as "[HgFrag #Hα]".
iVs ("Hvs2" with "[HgFrag]") as "HP"; first by iFrame.
iVsIntro. iApply Hf=>//.
iFrame "Hh Hϕ". iSplitR; first done. iIntros (ret g') "Hϕ' Hβ".
iVs ("Hvs1" with "HP") as "[HgFrag _]".
iCombine "HgFull" "HgFrag" as "Hg".
rewrite /gFullR /gFragR.
iAssert (|=r=> own γ (((1 / 2)%Qp, DecAgree g') ((1 / 2)%Qp, DecAgree g')))%I with "[Hg]" as "Hupd".
{ iApply (own_update); last by iAssumption. apply pair_l_frac_update. }
iVs "Hupd" as "[HgFull HgFrag]".
iVs ("Hvs3" $! g' ret with "[HgFrag Hβ]"); first by iFrame.
iVsIntro.
iSplitL "HgFull Hϕ'".
- iExists g'. by iFrame.
- done.
Qed.
End atomic_sync.
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