Commit 553737c5 authored by Simon Friis Vindum's avatar Simon Friis Vindum

Refactor refinement proof

parent e230c27b
......@@ -288,14 +288,14 @@ Section Queue_refinement.
iInduction xs as [|x' xs'] "IH" forall (hdPt).
- iDestruct (mapsto_full_to_frac_2 with "nilPts") as "(nilPts & nilPts')".
iDestruct "tailPts" as "[tailPts tailPts']".
iDestruct "nodeList" as (0) ">(ℓhdPt & ℓ0Pts &tok')".
iDestruct "nodeList" as (0) ">(ℓhdPt & _ &tok')".
(* We need to be able to conclude that ℓhdPt is equal to ℓ. *)
iDestruct (fracAgree_agree with "tok tok'") as %<-.
iDestruct (mapsto_combine with "ℓhdPt ℓPts") as "[ℓpts %]".
inversion_clear H6.
rewrite Qp_half_half.
iMod (fracAgree_update with "tok tok'") as "[tok tok']".
iMod (own_alloc ( nodeLive _)) as (ι) "[[authNodeState authNodeState'] fragNodeState]".
iMod (own_alloc ( nodeLive _)) as (ι) "[[authNodeState authNodeState'] _]".
{ by apply auth_both_valid. }
destruct (m !! node) as [v|] eqn:Eq.
{ iDestruct (big_sepM_lookup with "bigSep") as "conj".
......@@ -304,25 +304,23 @@ Section Queue_refinement.
iDestruct "sentInv" as (v') "(>nodePts' & _)".
iDestruct (mapsto_exclusive_frac with "nodePts nodePts'") as %[]. }
iDestruct (mapsto_full_to_frac_3 with "nodePts") as "(nodePts & nodePts' & nodePts'')".
(* iDestruct "nodePts" as "[nodePts [nodePts' nodePts'']]". *)
iMod (insert_node_subset _ _ _ _ _ _ m (delete sentinel m) with "[%] [% //] authM bigSep [authNodeState' nodePts'' tok tailPts' nilPts']")
as "(authM & bigSep & #frag)".
{ apply delete_subseteq. }
{ iExists _. iFrame "nodePts''".
iSplitL "tailPts' nilPts' tok"; iExistsFrame. }
iApply (wp_cas_suc with "ℓpts").
iNext. iIntros "ℓpts".
iDestruct (mapsto_full_to_frac_3 with "ℓpts") as "(ℓpts & ℓpts' & ℓpts'')".
iApply (wp_cas_suc with "ℓpts"). iNext. iIntros "ℓpts".
iDestruct (mapsto_full_to_frac_2 with "ℓpts") as "(ℓpts & ℓpts')".
iApply "Hϕ". iExists _.
rewrite delete_insert_ne; last done.
iFrame "frag nodePts". iFrame.
simpl.
iExistsN. iFrame "frag nodePts'". iFrame.
iFrame. iExists _. iFrame "tailPts". iFrame.
- iDestruct "nodeList" as (0 next ι) "(FOO & BAR & BAZ & HIHI & nodeListTail)".
- iDestruct "nodeList" as (? ? ?) "(? & ? & ? & ? & nodeListTail)".
iApply ("IH" with "authM bigSep nilPts tailPts nodePts nodeListTail ℓPts tok").
iNext.
iDestruct 1 as (ι') "(authM & bigSep & nilPts & tailPts & nodePts & ℓPts)".
iDestruct 1 as (?) "(authM & bigSep & nilPts & tailPts & nodePts & ℓPts)".
iApply "Hϕ".
iExistsFrame.
Qed.
......@@ -354,13 +352,38 @@ Section Queue_refinement.
by iApply "Hϕ".
Qed.
Lemma load_sentinel γ κ τi q t list lock :
{{{ inv queueN (queueInv γ κ τi q t list lock) }}}
Load (Loc q)
{{{ sentinel ι hdPt, RET (LocV sentinel);
node_mapsto κ sentinel ι hdPt own ι ( nodeSentinel) }}}.
Proof.
iIntros (ϕ) "inv Hϕ".
iInv queueN as (xs xs) "(isMSQ & Hrest)" "Hclose".
iDestruct "isMSQ" as (? ? ? ? ? ?) "(>qPts & >#frag & ? & ? & >nodeState & ?)".
iMod (own_update with "nodeState") as "[authNodeState nodeState]".
{ by apply (auth_update_core_id_frac _ nodeSentinel). }
iApply (wp_load with "qPts"). iNext. iIntros "qPts".
iMod ("Hclose" with "[-Hϕ nodeState]"). { iNext. iExistsFrame. }
iModIntro. iApply "Hϕ". auto.
Qed.
Lemma load_tail γ κ τi q t list lock :
{{{ inv queueN (queueInv γ κ τi q t list lock) }}}
Load (Loc t)
{{{ ι last pt, RET (LocV last); node_mapsto κ last ι pt }}}.
Proof.
iIntros (ϕ) "inv Hϕ".
iInv queueN as (xs xs) "(isMSQ & Hrest)" "Hclose".
iDestruct "isMSQ" as (? ? ? ? ? ?) "(? & ? & >tPts & >#lastMapsto & ?)".
iApply (wp_load with "tPts"). iNext. iIntros "tPts".
iMod ("Hclose" with "[-Hϕ]"). { iNext. iExistsFrame. }
iModIntro. iApply "Hϕ". auto.
Qed.
Lemma MS_CG_counter_refinement :
[] MS_queue log CG_queue :
(TForall (TProd
(TArrow TUnit (TMaybe (TVar 0)))
(TArrow (TVar 0) TUnit)
)
).
(TForall (TProd (TArrow TUnit (TMaybe (TVar 0))) (TArrow (TVar 0) TUnit))).
Proof.
iIntros (Δ vs ?) "#[Hspec HΓ]".
iDestruct (interp_env_empty with "HΓ") as "->". iClear "HΓ".
......@@ -442,17 +465,7 @@ Section Queue_refinement.
iLöb as "Hlat".
iApply wp_pure_step_later; auto. iNext. iAsimpl.
iApply (wp_bind (fill [LetInCtx _])).
iInv queueN as (xs xs) "(isMSQ & Hsq & lofal & Hlink)" "Hclose".
rewrite /isMSQueue.
iDestruct "isMSQ" as (sentinel last hdPt pt ι ι')
"(>qPts & >#fragO & >tPts & lastMapsto & >nodeState & nodeList)".
iMod (own_update with "nodeState") as "[authNodeState nodeState]".
{ by apply (auth_update_core_id_frac _ nodeSentinel). }
iApply (wp_load with "qPts"). iNext. iIntros "qPts".
iMod ("Hclose" with "[qPts tPts lastMapsto lofal Hlink Hsq authNodeState nodeList]") as "_".
{ iNext. iExistsFrame. }
simpl.
iModIntro.
iApply (load_sentinel with "[$]"). iNext. iIntros (sentinel ι hdPt) "(#fragO & nodeState)".
iApply wp_pure_step_later; auto. iNext. iAsimpl.
iApply (wp_bind (fill [LetInCtx _])).
iApply (wp_bind (fill [UnfoldCtx; CaseCtx _ _])).
......@@ -683,13 +696,7 @@ Section Queue_refinement.
iNext. iIntros (node) "nodePts /=".
iApply wp_pure_step_later; auto. iNext.
iApply (wp_bind (fill [LetInCtx _])). simpl.
iInv queueN as (xs xs) "(isMSQ & Hsq & lofal & Hlink)" "Hclose".
iDestruct "isMSQ" as (sentinel last hdPt pt ι ι')
"(>qPts & >fragO & >tPts & >#lastMapsto & >sentState & nodeList)".
iApply (wp_load with "tPts"). iNext. iIntros "tPts".
iMod ("Hclose" with "[qPts tPts fragO lofal Hlink Hsq sentState nodeList]") as "_".
{ iNext. iExistsFrame. }
iModIntro.
iApply (load_tail with "[$]"). iNext. iIntros (ι last pt) "#lastMapsto".
iApply wp_pure_step_later; auto. iNext.
(* Evaluate the argument to the recursive function. *)
iApply (wp_bind (fill [AppRCtx (RecV _)])).
......@@ -698,19 +705,10 @@ Section Queue_refinement.
iApply (wp_bind (fill [UnfoldCtx])).
iApply (wp_bind (fill [LoadCtx])).
iApply wp_value. simpl.
(* iInv queueN as (xs xsₛ) "(isMSQ & Hsq & lofal & Hlink)" "Hclose".
iDestruct "isMSQ" as (ℓsentinel ℓlast ℓhdPt ℓpt ι ι')
"(>qPts & >#fragO & >tPts & lastMapsto & >sentState & nodeList)".
iApply (wp_load with "qPts").
iNext. iIntros "qPts".
iMod ("Hclose" with "[qPts tPts lastMapsto lofal Hlink Hsq sentState nodeList]") as "_".
{ iNext. iExistsFrame. }
iModIntro. *)
(* Lookup node *)
iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
iDestruct (node_lookup with "authM bigSep [$]") as "(sentInv & authM & bigSep)".
iDestruct "sentInv" as (x) "(>sentinelPts & nextNode & rest)".
(* iDestruct (mapsto_frac_duplicable with "sentinelPts") as "sentinelPts". *)
iApply (wp_load_frac with "sentinelPts").
iNext. iIntros "sentinelPts".
simpl.
......@@ -732,12 +730,12 @@ Section Queue_refinement.
This is not going to be the case when we want to use the IH. Therefore
we have to generalize the goal such that we "split" occurences of
ℓlast. *)
iAssert (node_mapsto κ last ι' pt) as "nextMapsto". iAssumption.
iAssert (node_mapsto κ last ι pt) as "nextMapsto". iAssumption.
generalize last at 2 3 4 5 6 8 9 10 11. iIntros (next).
generalize pt at 1. iIntros (pt').
generalize ι' at 1. iIntros (ι'').
generalize ι at 1. iIntros (ι').
(* We are now done evaluating the argument. *)
iLöb as "Hlat" forall (ι' next pt) "nextMapsto".
iLöb as "Hlat" forall (ι next pt) "nextMapsto".
iApply wp_pure_step_later; auto. iNext. iAsimpl.
iApply (wp_bind (fill [LetInCtx _])).
(* Lookup node *)
......@@ -765,7 +763,6 @@ Section Queue_refinement.
iApply wp_value.
iApply wp_pure_step_later; auto; iNext. simpl.
iApply (wp_bind (fill [IfCtx _ _])).
clear xs xs.
(* We must open the invariant, case on whether ℓ is equal to ℓ2, and
extract that ℓ is the last node. *)
iInv queueN as (xs xs) "(isMSQ & Hsq & lofal & Hlink)" "Hclose".
......@@ -853,7 +850,6 @@ Section Queue_refinement.
iApply ("Hlat" $! _ _ _ with "Hj nilPts tailPts nodePts nextMapsto").
+ (* We are not at the end yet, keep on going. *)
iDestruct "right" as (ι3 next) "(>ℓPts & #nodeInvNext)".
(* iDestruct "right" as (x next) "(>[ℓPts ℓPts'] & [ℓ2Pts ℓ2Pts'] & #nodeInvNext)". *)
iApply (wp_load_frac with "ℓPts").
iNext. iIntros "ℓPts". simpl.
iDestruct (reinsert_node with "authM nextMapsto bigSep [sentinelPts' ℓPts rest nodeInvNext]") as "(authM & bigSep)".
......
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