From f8ce13c3c6095a3e2bf882d841bfdb81192766f3 Mon Sep 17 00:00:00 2001
From: Zhen Zhang
Date: Tue, 25 Oct 2016 11:08:11 +0800
Subject: [PATCH] Rewrite iteration

flat.v  123 ++++++++++++++++++++++++++
peritem.v  52 ++++
2 files changed, 68 insertions(+), 107 deletions()
diff git a/flat.v b/flat.v
index 3753263..3906ebe 100644
 a/flat.v
+++ b/flat.v
@@ 183,116 +183,111 @@ Section proof.
⊢ WP iter #hd doOp {{ Φ }}.
Proof.
iIntros (HN) "(#Hf & #? & Ho2 & HR & Hlist' & HΦ)".
 iApply pvs_wp.
 iDestruct (dup_is_list' with "[Hlist']") as "==>[Hl1 Hl2]"; first by iFrame.
 iDestruct (dup_is_list' with "[Hl2]") as "==>[Hl2 Hl3]"; first by iFrame.
 iVsIntro.
 iDestruct (iter_spec _ (p_inv R γm γr) (fun v => v = #() ★ own γr (Excl ()) ★ R)%I γs s
 (is_list' γs hd xs ★ own γr (Excl ()) ★ R)%I (srv_tokm_inv γm) xs hd
 doOp doOp
 with "[Hl1 HΦ]") as "Hiter"=>//.
+ iApply (iter_spec N (p_inv R γm γr) Φ
+ (* (fun v => v = #() ★ own γr (Excl ()) ★ R)%I *)
+ γs s (own γr (Excl ()) ★ R)%I (srv_tokm_inv γm) xs hd doOp doOp
+ with "[]")=>//.
 rewrite /f_spec.
 iIntros (Φ' p _ Hin) "(#Hh & #? & (Hls & Ho2 & HR) & HΦ')".
 wp_let. wp_bind (! _)%E. iInv N as "[Hs >Hm]" "Hclose".
 iDestruct "Hs" as (xs' hd') "[>Hhd [>Hxs HRs]]".
 iDestruct (dup_is_list' with "[Hls]") as "==>[Hls1 Hls2]"; first by iFrame.
+ iIntros (Φ' x _) "(#Hh & #? & Hev & [Hor HR] & HΦ')".
+ iDestruct "Hev" as (xhd) "#Hev".
+ wp_rec. wp_bind (! _)%E. iInv N as "[Hs >Hm]" "Hclose".
+ iDestruct "Hs" as (gxs ghd) "[>Hghd [>Hgxs HRs]]". (* global xs, hd *)
iDestruct "HRs" as (m) "[>Hom HRs]".
(* acccess *)
 iDestruct (access with "[Hom HRs Hls1]") as (hd'') "(Hrest & HRx & % & Hom)"=>//; first iFrame.
 iDestruct "HRx" as (v') "[>% [Hpinv' >Hhd'']]". inversion H0. subst.
+ iDestruct (ev_map_witness _ _ _ m with "[Hev Hom]") as %H'; first by iFrame.
+ iDestruct (big_sepM_delete_later (perR _) m with "HRs") as "[Hp HRm]"=>//.
+ iDestruct "Hp" as (v') "[>% [Hpinv' >Hahd]]". inversion H. subst.
iDestruct "Hpinv'" as (ts p'') "[>% [>#Hevm [Hp  [Hp  [Hp  Hp]]]]]"; subst.
+ iDestruct "Hp" as (y) "(>Hp & Hs)".
 wp_load. iVs ("Hclose" with "[HΦ' Ho2 HR Hls2]").
 { iNext. iFrame. iExists xs', hd'.
 iFrame "Hhd Hxs". iExists m.
 iFrame "Hom". iDestruct (big_sepM_delete _ m with "[Hrest Hhd'' Hevm Hp Hs]") as "?"=>//.
+ wp_load. iVs ("Hclose" with "[Hor HR Hev HΦ']").
+ { iNext. iFrame. iExists gxs, ghd.
+ iFrame "Hghd Hgxs". iExists m.
+ iFrame "Hom". iDestruct (big_sepM_delete _ m with "[]") as "?"=>//.
iFrame. iExists #p''. iSplitR; first done. iExists ts, p''.
iSplitR; first done. iFrame "#". iLeft. iExists y. iFrame. }
 iVsIntro. wp_match. iApply "HΦ'". by iFrame.
+ iVsIntro. wp_match. iVsIntro. iApply ("HΦ'" with "[Hor HR]"). iFrame.
+ iDestruct "Hp" as (f' x') "(Hp & Hs)".
wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq].
 iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf & HoQ& Ho1 & Ho4)".
+ iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf' & HoQ & Ho1 & Ho4)".
iAssert (=r=> own γx (((1/2/2)%Qp, DecAgree x') ⋅
((1/2/2)%Qp, DecAgree x')))%I with "[Hx]" as "==>[Hx1 Hx2]".
{ iDestruct (own_update with "Hx") as "?"; last by iAssumption.
rewrite {1}(Qp_div_2 (1/2)%Qp).
by apply pair_l_frac_op'. }
 iVs ("Hclose" with "[Hf Hls2 Ho1 Hx2 HR HoQ Hpx HΦ']").
 { iNext. iFrame. iExists xs', hd'.
 iFrame "Hhd Hxs". iExists m.
+ iVs ("Hclose" with "[Hf' Ho1 Hx2 HR HoQ HΦ' Hpx]").
+ { iNext. iFrame. iExists gxs, ghd.
+ iFrame "Hghd Hgxs". iExists m.
iFrame "Hom". iDestruct (big_sepM_delete _ m with "[]") as "?"=>//.
simpl. iFrame. iExists #p''. iSplitR; auto. rewrite /allocated.
iExists (γx, γ1, γ3, γ4, γq), p''. iSplitR; auto.
iFrame "#". iRight. iRight. iLeft. iExists f', x'. iFrame. }
iVsIntro. wp_match.
wp_proj. wp_proj.
 wp_bind (f' _). iApply wp_wand_r. iSplitL "Hpx Hf HR".
 { iApply "Hf". iFrame. }
+ wp_bind (f' _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
+ { iApply "Hf'". iFrame. }
iIntros (v) "[HR HQ]".
wp_value. iVsIntro. iInv N as "[Hs >Hm]" "Hclose".
iDestruct "Hs" as (xs'' hd''') "[>Hhd [>Hxs HRs]]".
iDestruct "HRs" as (m') "[>Hom HRs]".
 iDestruct (dup_is_list' with "[Hls2]") as "==>[Hls2 Hls3]"; first by iFrame.
 iDestruct (access with "[Hom HRs Hls2]") as (hd'''') "(Hrest & HRx & % & Hom)"=>//; first iFrame.
 iDestruct "HRx" as (v'') "[>% [Hpinv' >Hhd'']]". inversion H2. subst.
+ iDestruct (ev_map_witness _ _ _ m' with "[Hevm Hom]") as %?; first by iFrame.
+ iDestruct (big_sepM_delete_later (perR _) m' with "HRs") as "[Hp HRm]"=>//.
+ iDestruct "Hp" as (v'') "[>% [Hpinv' >Hhd'']]". inversion H1. subst.
iDestruct "Hpinv'" as ([[[[γx' γ1'] γ3'] γ4'] γq'] p'''') "[>% [>#Hevm2 Hps]]".
 inversion H3. subst.
 destruct (decide (γ1 = γ1' ∧ γx = γx' ∧ γ3 = γ3' ∧ γ4 = γ4' ∧ γq = γq')) as [[? [? [? [? ?]]]]Hneq]; subst.
+ inversion H2. subst.
+ destruct (decide (γ1 = γ1' ∧ γx = γx' ∧ γ3 = γ3' ∧ γ4 = γ4' ∧ γq = γq'))
+ as [[? [? [? [? ?]]]]Hneq]; subst.
{
iDestruct "Hps" as "[Hp  [Hp  [Hp  Hp]]]".
* iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
iApply excl_falso. iFrame.
* iDestruct "Hp" as (? ?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
iApply excl_falso. iFrame.
 * iDestruct "Hp" as (? x5) ">(Hp & Hx & Ho2 & Ho4)".
 iDestruct "Hm" as (m2) "[Hom2 HRm]".
 destruct (m2 !! p'''') eqn:Heqn.
 {
 iDestruct (big_sepM_delete _ m2 with "HRm") as "[HRk HRm]"=>//.
 iDestruct "HRk" as (?) "HRk".
 iDestruct (heap_mapsto_op_1 with "[HRk Hp]") as "[% Hp]"; first by iFrame.
 rewrite Qp_div_2. wp_store.
 (* now close the invariant *)
 iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
 subst. rewrite Qp_div_2. iVs ("Hclose" with "[HΦ' Ho2 HR Hls3]").
 { iNext. iDestruct "Hp" as "[Hp1 Hp2]".
 iAssert (srv_tokm_inv γm) with "[Hp1 HRm Hom2]" as "HRm".
 { iExists m2. iFrame. iApply (big_sepM_delete _ m2)=>//.
 iFrame. eauto. }
 iFrame. iExists xs''. iFrame. iExists hd'''. iFrame.
 iExists m'. iFrame.
 iDestruct (big_sepM_delete _ m' with "[]") as "?"=>//.
 { simpl. iFrame. iExists #p''''.
 iSplitR; first auto. iExists (γx', γ1', γ3', γ4', γq'), p''''.
 iSplitR; first auto. iFrame "Hevm". iRight. iRight.
 iRight. iExists x5, v. iFrame.
 iExists Q. iFrame.
 }
+ * iDestruct "Hp" as (? x5) ">(Hp & Hx & Hor & Ho4)".
+ iDestruct "Hm" as (m2) "[Hom2 HRp]".
+ iDestruct (ev_map_witness _ _ _ m2 with "[Hevm Hom2]") as %?; first by iFrame.
+ iDestruct (big_sepM_delete _ m2 with "HRp") as "[HRk HRp]"=>//.
+ iDestruct "HRk" as (?) "HRk".
+ iDestruct (heap_mapsto_op_1 with "[HRk Hp]") as "[% Hp]"; first by iFrame.
+ rewrite Qp_div_2. wp_store.
+ (* now close the invariant *)
+ iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
+ subst. rewrite Qp_div_2. iVs ("Hclose" with "[HR Hor HΦ']").
+ { iNext. iDestruct "Hp" as "[Hp1 Hp2]".
+ iAssert (srv_tokm_inv γm) with "[Hp1 HRp Hom2]" as "HRp".
+ { iExists m2. iFrame. iApply (big_sepM_delete _ m2)=>//.
+ iFrame. eauto. }
+ iFrame. iExists xs''. iFrame. iExists hd'''. iFrame.
+ iExists m'. iFrame.
+ iDestruct (big_sepM_delete _ m' with "[]") as "?"=>//.
+ { simpl. iFrame. iExists #p''''.
+ iSplitR; first auto. iExists (γx', γ1', γ3', γ4', γq'), p''''.
+ iSplitR; first auto. iFrame "Hevm". iRight. iRight.
+ iRight. iExists x5, v. iFrame.
+ iExists Q. iFrame.
}
 iApply "HΦ'". by iFrame.
}
 { iExFalso. iApply (map_agree_none' _ _ _ m2)=>//. by iFrame. }
+ iApply "HΦ'". iFrame.
* iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
iApply excl_falso. iFrame.
}
{ iDestruct (evmap_frag_agree_split with "[]") as "%"; first iFrame "Hevm Hevm2".
 inversion H4. subst. by contradiction Hneq. }
+ inversion H3. subst. by contradiction Hneq. }
+ destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (? x) "(_ & _ & >Ho2' & _)".
iApply excl_falso. iFrame.
+ destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (x' y) "[Hp Hs]".
iDestruct "Hs" as (Q) "(>Hx & HoQ & HQxy & >Ho1 & >Ho4)".
 wp_load. iVs ("Hclose" with "[HΦ' HR Ho2 Hls2]").
 { iNext. iFrame. iExists xs', hd'.
 iFrame "Hhd Hxs". iExists m.
+ wp_load. iVs ("Hclose" with "[HΦ' HR Hor]").
+ { iNext. iFrame. iExists gxs, ghd.
+ iFrame "Hghd Hgxs". iExists m.
iFrame "Hom". iDestruct (big_sepM_delete _ m with "[]") as "?"=>//.
iFrame. iExists #p''. iSplitR; first auto. iExists (γx, γ1, γ3, γ4, γq), p''.
iSplitR; auto. iFrame "#". iRight. iRight. iRight. iExists x', y. iFrame.
iExists Q. iFrame. }
 iVsIntro. wp_match. iApply "HΦ'". by iFrame.
+ iVsIntro. wp_match.
+ iApply "HΦ'". iFrame.
 apply to_of_val.
  rewrite /srv_stack_inv. iFrame "#". iFrame. iIntros "(? & ? & ?)". by iFrame.
  iApply wp_wand_r. iSplitL "Hiter"; first done.
 iIntros (?) "[% [Ho2 HR]]". subst. iApply ("HΦ" with "Ho2 HR").
+  iFrame "#". iFrame. iIntros "[Hor HR]".
+ iApply ("HΦ" with "Hor HR").
Qed.
Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
diff git a/peritem.v b/peritem.v
index c974d2d..4c6e129 100644
 a/peritem.v
+++ b/peritem.v
@@ 73,12 +73,12 @@ Section defs.
iVsIntro. iSplitL "Hhd Hs1 Hev"; iExists hd', (q / 2)%Qp; by iFrame.
Qed.
 Definition f_spec γ (xs: list val) (s hd: loc) (f: val) (Rf RI: iProp Σ) :=
 (* Rf, RI are some frames *)
+ Definition f_spec γ (xs: list val) (s: loc) (f: val) (Rf RI: iProp Σ) :=
+ (* Rf, RI is some frame *)
∀ Φ (x: val),
 heapN ⊥ N → x ∈ xs →
 heap_ctx ★ inv N ((∃ xs, is_stack' γ xs s) ★ RI) ★
 (is_list' γ hd xs ★ Rf) ★ (is_list' γ hd xs ★ Rf ★ Φ #())
+ heapN ⊥ N →
+ heap_ctx ★ inv N ((∃ xs, is_stack' γ xs s) ★ RI) ★ (∃ hd, evs γ hd x) ★
+ Rf ★ (Rf ★ Φ #())
⊢ WP f x {{ Φ }}.
End defs.
@@ 106,7 +106,7 @@ Lemma new_stack_spec' Φ RI:
Lemma iter_spec Φ γ s (Rf RI: iProp Σ):
∀ xs hd (f: expr) (f': val),
 heapN ⊥ N → f_spec N R γ xs s hd f' Rf RI → to_val f = Some f' →
+ heapN ⊥ N → f_spec N R γ xs s f' Rf RI → to_val f = Some f' →
heap_ctx ★ inv N ((∃ xs, is_stack' R γ xs s) ★ RI) ★
is_list' γ hd xs ★ Rf ★ (Rf ★ Φ #())
⊢ WP (iter #hd) f {{ v, Φ v }}.
@@ 116,19 +116,11 @@ Lemma new_stack_spec' Φ RI:
iDestruct "Hxs1" as (q) "Hhd".
wp_rec. wp_value. iVsIntro. wp_let. wp_load. wp_match. by iApply "HΦ".
 simpl. iIntros (hd f f' HN Hf ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
 iDestruct "Hxs1" as (hd2 q) "(Hhd & #Hev & Hhd2)".
+ iDestruct "Hxs1" as (hd2 q) "(Hhd & Hev & Hhd2)".
wp_rec. wp_value. iVsIntro. wp_let. wp_load. wp_match. wp_proj.
 wp_bind (f' _). iApply Hf=>//; first set_solver.
 iFrame "#". simpl.
 iSplitL "Hev Hhd Hhd2 HRf".
 { iFrame. iExists hd2, q. iFrame. }
 iIntros "Hls HRf".
+ wp_bind (f' _). iApply Hf=>//. iFrame "#".
+ iSplitL "Hev"; first eauto. iFrame. iIntros "HRf".
wp_seq. wp_proj. iApply (IHxs' with "[]")=>//.
 + rewrite /f_spec. iIntros (? ? ? ?) "(#? & #? & ? & ?)".
 iApply Hf=>//.
 * set_solver.
 * iFrame "#".
 by iFrame.
+ apply to_of_val.
+ iFrame "#". by iFrame.
Qed.
@@ 191,30 +183,4 @@ Lemma new_stack_spec' Φ RI:
by iApply "HΦ".
Qed.
 (* some helpers *)
 Lemma access (γ: gname) (x: val) (xs: list val) (m: evmapR loc val unitR) :
 ∀ hd: loc,
 x ∈ xs →
 ▷ ([★ map] hd↦v ∈ m, perR R hd v) ★ own γ (● m) ★
 is_list' γ hd xs
 ⊢ ∃ hd', ▷ ([★ map] hd↦v ∈ delete hd' m, perR R hd v) ★
 ▷ perR R hd' ((∅: unitR), DecAgree x) ★ m !! hd' = Some ((∅: unitR), DecAgree x) ★ own γ (● m).
 Proof.
 induction xs as [x' xs' IHxs'].
  iIntros (? Habsurd). inversion Habsurd.
  destruct (decide (x = x')) as [>Hneq].
 + iIntros (hd _) "(HR & Hom & Hxs)".
 simpl. iDestruct "Hxs" as (hd' q) "[Hhd [#Hev Hxs']]".
 rewrite /evs.
 iDestruct (ev_map_witness _ _ _ m with "[Hev Hom]") as %H'; first by iFrame.
 iDestruct (big_sepM_delete_later (perR R) m with "HR") as "[Hp HRm]"=>//.
 iExists hd. by iFrame.
 + iIntros (hd ?).
 assert (x ∈ xs'); first set_solver.
 iIntros "(HRs & Hom & Hxs')".
 simpl. iDestruct "Hxs'" as (hd' q) "[Hhd [Hev Hxs']]".
 iDestruct (IHxs' hd' with "[HRs Hxs' Hom]") as "?"=>//.
 iFrame.
 Qed.

End proofs.

GitLab