Correct mistake in node invariant and advance enqueue proof

theories/logrel/F_mu_ref_conc/examples/queue/refinement.v

@@ -20,13 +20,12 @@ Section Queue_refinement.
 
   Program Definition nodeInv_pre : (valO -n> iPropO Σ) -n> (valO -n> iPropO Σ) :=
     λne P n,
-    (∃ ℓ, ⌜n = LocV ℓ⌝ ∗
-                   (ℓ ↦ᵢ{1/2} FoldV noneV (* FIXME: Maybe we need more info here? *)
+      (∃ ℓ ℓ2 q, ⌜n = LocV ℓ⌝ ∗
+        ((ℓ ↦ᵢ{1/2} (LocV ℓ2) ∗ ℓ2 ↦ᵢ{q} FoldV (noneV))
                     ∨
-                    (∃ (x : valO) q ℓtail n',
-                        ℓ ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV ℓtail)))
-                          ∗ ℓtail ↦ᵢ{q} n' ∗ inv nodeN (P n')
-                   )))%I.
+         (∃ x next, ℓ ↦ᵢ{q} (LocV ℓ2) ∗ ℓ2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) next))
+                    ∗ inv nodeN (P next)))
+      )%I.
   Solve Obligations with solve_proper.
 
   Global Instance nodeInv_pre_contractive : Contractive (nodeInv_pre).
@@ -36,12 +35,13 @@ Section Queue_refinement.
   Definition nodeInv : valO -n> iPropO Σ := fixpoint (nodeInv_pre).
 
   Lemma nodeInv_unfold n :
-    nodeInv n ≡ (∃ ℓ, ⌜n = LocV ℓ⌝ ∗
-                                (ℓ ↦ᵢ{1/2} FoldV noneV ∨
-                                 (∃ (x : valO) q ℓtail n',
-                                     ℓ ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV ℓtail)))
-                                       ∗ ℓtail ↦ᵢ{q} n' ∗ inv nodeN (nodeInv n')
-                )))%I.
+    nodeInv n ≡ (
+      ∃ ℓ ℓ2 q, ⌜n = LocV ℓ⌝ ∗
+        ((ℓ ↦ᵢ{1/2} (LocV ℓ2) ∗ ℓ2 ↦ᵢ{q} FoldV (noneV))
+         ∨
+         (∃ x next, ℓ ↦ᵢ{q} (LocV ℓ2) ∗ ℓ2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) next))
+                    ∗ inv nodeN (nodeInv next)))
+    )%I.
   Proof. rewrite /nodeInv. apply (fixpoint_unfold nodeInv_pre n). Qed.
 
   Fixpoint isCGQueue_go (xs : list val) : val :=
@@ -58,12 +58,11 @@ Section Queue_refinement.
    *)
   Fixpoint isNodeList q (ℓ : loc) (xs : list val) : iProp Σ :=
     match xs with
-    | nil => ℓ ↦ᵢ{1/2} FoldV noneV
+    | nil => ∃ ℓ2, ℓ ↦ᵢ{1/2} (LocV ℓ2) ∗ ℓ2 ↦ᵢ{q} FoldV noneV
     | x :: xs' =>
-      (∃ ℓtail ℓnext,
-          ℓ ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV ℓtail)))
-            ∗ ℓtail ↦ᵢ{q} (LocV ℓnext)
-            ∗ isNodeList q ℓnext xs')
+      (∃ ℓ2 next,
+          ℓ ↦ᵢ{q} (LocV ℓ2) ∗ ℓ2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV next)))
+            ∗ isNodeList q next xs')
     end.
 
   (* Represents that the location ℓ points to a series of nodes corresponding to
@@ -75,10 +74,8 @@ Section Queue_refinement.
     match xs with
     | nil => True (* Here we should be able to say that ℓ is either another node or the end. *)
     | x :: xs' =>
-      (∃ ℓtail ℓnext,
-          ℓ ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV ℓtail)))
-            ∗ ℓtail ↦ᵢ{q} (LocV ℓnext)
-            ∗ firstXsValues q ℓnext xs')
+      (∃ ℓ2 next, ℓ ↦ᵢ{q} (LocV ℓ2) ∗ ℓ2 ↦ᵢ{q} FoldV (someV (PairV (InjRV x) (LocV next)))
+                  ∗ firstXsValues q next xs')
     end.
 
   Lemma firstXsValues_split q ℓ xs : firstXsValues q ℓ xs -∗ firstXsValues (q/2) ℓ xs ∗ firstXsValues (q/2) ℓ xs : iProp Σ.
@@ -96,21 +93,22 @@ Section Queue_refinement.
     iIntros "isNodeList".
     (* generalize dependent ℓ. *)
     iInduction xs as [|x xs'] "IH" forall (ℓ); simpl.
-    - iFrame.
-    - iDestruct "isNodeList" as (ℓtail ℓnext) "([ℓPts1 ℓPts2] & [ℓtailPts1 ℓtailPts2] & Hnl)".
+    - iDestruct "isNodeList" as (ℓ2) "(ℓPts1 & [ℓtailPts1 ℓtailPts2] & Hnl)".
+      iSplit; auto. iExists _. iFrame.
+    - iDestruct "isNodeList" as (ℓ2 ℓnext) "([ℓPts1 ℓPts2] & [ℓtailPts1 ℓtailPts2] & Hnl)".
       iDestruct ("IH" with "Hnl") as "[Ha Hb]".
       iSplitL "ℓPts1 ℓtailPts1 Ha"; iExists _, _; iFrame.
   Qed.
 
   (* Predicate expression that ℓ points to a queue with the values xs *)
   Definition isMSQueue (τi : D) (ℓ : loc) (xsᵢ : list val) : iProp Σ :=
-    (∃ ℓsentinel v ℓhdPt ℓhd q p,
+    (∃ ℓsentinel v ℓhdPt q p,
         ℓ ↦ᵢ (LocV ℓsentinel)
           ∗ ℓsentinel ↦ᵢ{q} (FoldV (someV (PairV v (LocV ℓhdPt))))
-          ∗ ℓhdPt ↦ᵢ{q} (LocV ℓhd)
-          ∗ isNodeList p ℓhd xsᵢ
+          (* ∗ ℓhdPt ↦ᵢ{q} (LocV ℓhd) *)
+          ∗ isNodeList p ℓhdPt xsᵢ
           (* ∗ firstXsValues p ℓhd xsᵢ *)
-          ∗ inv nodeN (nodeInv (LocV ℓhd))
+          ∗ inv nodeN (nodeInv (LocV ℓhdPt))
     )%I.
 
   Fixpoint xsLink (τi : D) (xsᵢ xsₛ : list val) : iProp Σ :=
@@ -195,26 +193,30 @@ Section Queue_refinement.
     iApply (wp_bind (fill [PairRCtx (InjLV UnitV); InjRCtx; FoldCtx])).
     iApply (wp_bind (fill [AllocCtx])).
     iApply wp_alloc; first done.
-    iNext. iIntros (nil) "[nilPts1 nilPts2] /=".
+    iNext. iIntros (nil) "[nilPts nilPts'] /=".
     iApply wp_alloc; first done.
-    iNext. iIntros (tail) "tailPts /=".
+    iNext. iIntros (tail) "[tailPts tailPts'] /=".
     iApply wp_value.
     iApply wp_alloc; first done. iNext.
     iIntros (sentinel) "sentinelPts /=".
     iApply wp_alloc; first done. iNext.
     iIntros (head) "headPts /=".
     iApply wp_pure_step_later; auto. iNext.
-    iMod (inv_alloc nodeN _ (nodeInv (LocV nil)) with "[nilPts1]") as "#nodeInv".
-    { iNext. rewrite nodeInv_unfold. iExists _. auto. }
+    iMod (inv_alloc nodeN _ (nodeInv (LocV tail)) with "[tailPts nilPts]") as "#nodeInv".
+    { iNext. rewrite nodeInv_unfold. iExists _, _, _. iSplit; auto. iLeft. iFrame. }
     iMod (inv_alloc queueN _ (invariant τi (Loc head) (Loc list) _)
-            with "[headPts lockPts listPts' sentinelPts tailPts nilPts2]")
+            with "[headPts lockPts listPts' sentinelPts tailPts' nilPts']")
       as "#Hinv".
     { iNext. iExists _, _, [], [].
       simpl.
       iFrame.
       iSplit. done.
-      iSplitL "headPts sentinelPts tailPts nilPts2".
-      { iExists _, _, _, _, _, _. iFrame. iAssumption. }
+      iSplitL "headPts sentinelPts tailPts' nilPts'".
+      { rewrite /isMSQueue. iExists _, _, _, _, _. simpl. iFrame.
+        iSplitL "tailPts' nilPts'".
+        { iExists _. iFrame. }
+        iAssumption. 
+      }
       iSplit; done.
     }
     iApply wp_value.
@@ -233,16 +235,17 @@ Section Queue_refinement.
       iApply wp_pure_step_later; auto. iNext. asimpl.
       iApply (wp_bind (fill [LetInCtx _])).
       iInv queueN as (ℓq ℓ' xs xsₛ) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
-      iDestruct "isMSQ" as (ℓsentinel v ℓhdPt ℓhd q p)
-                             "(qPts & [sentinelPts sentinelPts'] & [hdPts hdPts'] & nodeList & nodeinv)".
+      rewrite /isMSQueue.
+      iDestruct "isMSQ" as (ℓsentinel v ℓhdPt q p)
+                             "(qPts & [sentinelPts sentinelPts'] & nodeList & nodeinv)".
       iApply (wp_load with "qPts"). iNext. iIntros "qPts".
       iDestruct (splitIsNodeList with "nodeList") as "[nodeList first]".
-      iMod ("Hclose" with "[qPts lofal Hlink Hsq sentinelPts' hdPts' nodeList nodeinv]") as "_".
+      iMod ("Hclose" with "[qPts lofal Hlink Hsq sentinelPts' nodeList nodeinv]") as "_".
       { iNext. iExists _, _, _, _.
         iFrame.
         iSplit; auto.
-        iSplitL "qPts sentinelPts' hdPts' nodeList nodeinv".
-        { iExists _, _, _, _, _, _. iFrame. }
+        iSplitL "qPts sentinelPts' nodeList nodeinv".
+        { iExists _, _, _, _, _. iFrame. }
         iSplit; auto.
       }
       simpl.
@@ -268,8 +271,6 @@ Section Queue_refinement.
       iApply (wp_bind (fill [LoadCtx])).
       iApply wp_pure_step_later; auto. iNext.
       iApply wp_value. simpl.
-      iApply (wp_load with "[$hdPts]"). iNext. iIntros "hdPts".
-      simpl.
       destruct xs as [|x xs']; simpl.
       (* xs is the empty list *)
       + assert (xsₛ = []) as ->.
@@ -288,9 +289,12 @@ Section Queue_refinement.
         (* iApply wp_value. *)
         admit.
       (* xs is not the empty list *)
-      + destruct xsₛ as [|xₛ xsₛ'].
+      + iDestruct "first" as (ℓhd next) "(hdPts & hdPts' & Hnodes)".
+        iApply (wp_load with "[$hdPts]"). iNext. iIntros "hdPts".
+        simpl.
+        destruct xsₛ as [|xₛ xsₛ'].
         { inversion H3. }
-        iDestruct "first" as (ℓhd' ℓtail') "(hdPts' & tailPts' & Hnodes')".
+        (* iDestruct "first" as (ℓhd' ℓtail') "(hdPts' & tailPts' & Hnodes')". *)
         iApply (wp_load with "[$hdPts']"). iNext. iIntros "hdPts'".
         simpl.
         iApply wp_pure_step_later; auto. iNext.
@@ -306,8 +310,9 @@ Section Queue_refinement.
         simpl.
         rename ℓq into ℓq'.
         iInv queueN as (ℓq ℓ'2 xs2 xsₛ2) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
-        iDestruct "isMSQ" as (ℓsentinel2 v2 ℓhdPt2 ℓhd2 q2 p2)
-                               "(qPts & sentinelPts' & hdPts2 & nodeList & #nodeInv')".
+        rewrite /isMSQueue.
+        iDestruct "isMSQ" as (ℓsentinel2 v2 ℓhdPt2 q2 p2)
+                               "(qPts & sentinelPts' & nodeList & #nodeInv')".
         destruct (decide (ℓsentinel2 = ℓsentinel)) as [|Hneq]; subst.
         * (* The queue still points to the same sentinel that we read earlier--the CAS succeeds *)
           iApply (wp_cas_suc with "qPts"); auto.
@@ -320,52 +325,57 @@ Section Queue_refinement.
           { iDestruct (mapsto_agree with "sentinelPts sentinelPts'") as %[=->]. done. }
           iAssert (⌜ℓhdPt = ℓhdPt2⌝)%I as %<-.
           { iDestruct (mapsto_agree with "sentinelPts sentinelPts'") as %[=->]. done. }
-          iAssert (⌜ℓhd = ℓhd2⌝)%I as %<-.
-          { iDestruct (mapsto_agree with "hdPts hdPts2") as %[=->]. done. }
-
           (* TODO: Maybe we could clear nodeInv at an earlier point? *)
           iClear (nil) "nodeInv".
           rewrite nodeInv_unfold.
-          iInv nodeN as (ℓother) "(>% & two)" "closeNodeInv".
+          iInv nodeN as (ℓother hdPt'2 q3) "(>% & Disj)" "closeNodeInv".
           { admit. } (* FIXME *)
           inversion H5 as [Heq].
           rewrite -Heq.
           clear ℓother H5 Heq.
-          iDestruct "two" as "[hdPts''|Right]".
-          { iDestruct (mapsto_agree with "hdPts' hdPts''") as ">%". inversion H5. }
-          iDestruct "Right" as (x0 q0 ℓtail0 nwhat) "([hdPts3 hdPts3'] & [what3 what3'] & #tailInv)".
-          iMod ("closeNodeInv" with "[hdPts3' what3' tailInv]").
-          { iNext. iExists _. iFrame.
+          iDestruct "Disj" as "[[hdPts'' hdPts''']|Right]".
+          {
+             iDestruct (mapsto_agree with "hdPts hdPts''") as ">%".
+             inversion H5 as [Eq]. rewrite -Eq.
+             iDestruct (mapsto_agree with "hdPts' hdPts'''") as ">%".
+             inversion H6.
+          }
+          iDestruct "Right" as (x0 ℓtail0) "([hdPts3 hdPts3'] & [what3 what3'] & #tailInv)".
+          iMod ("closeNodeInv" with "[hdPts3' what3']").
+          { iNext. iExists _, _, _. 
             iSplit; auto.
-            iRight. iExists _, _, _, _. iFrame. iAssumption.
+            iRight. iExists _, _. iFrame. iAssumption.
           }
           (* xs2 is not necessarily equal to xs, but, since the CAS succeeded,
           it still has xs as a prefix. And since we know that xs is a cons xs2
           must also be a cons with the same element. *)
           destruct xs2 as [|x2' xs2']; simpl.
-          { iDestruct (mapsto_agree with "nodeList hdPts'") as %[=->]. }
+          { iDestruct "nodeList" as (ℓ2) "[ℓhdPts ℓ2Pts]".
+            iDestruct (mapsto_agree with "ℓhdPts hdPts") as %[= ->].
+            iDestruct (mapsto_agree with "hdPts' ℓ2Pts") as %[=].
+          }
           destruct xsₛ2 as [|xₛ2' xsₛ2']; simpl.
           { inversion H4. }
           iDestruct "nodeList" as (ℓtail ℓnext) "(hdPts'' & tailPts & nodeList)".
-          iAssert (⌜x = x2'⌝)%I as %<-.
-          { iDestruct (mapsto_agree with "hdPts' hdPts''") as %[=<-]. done. }
+          iDestruct (mapsto_agree with "hdPts hdPts''") as %[= <-].
+          iDestruct (mapsto_agree with "hdPts' tailPts") as %[= <- <-].
+          (* iAssert (⌜x = x2'⌝)%I as %<-.
+          { iDestruct (mapsto_agree with "hdPts' hdPts''") as %[=<-]. done. } *)
           iDestruct "Hlink" as "[Hτi Hlink]".
           (* We step through the specificaion code. *)
           iMod (steps_CG_dequeue_cons with "[$Hspec $Hj $Hsq $lofal]") as "(Hj & Hsq & lofal)".
           { solve_ndisj. }
-          (* FIXME: I think the brackets can be removed here. *)
           (* We are now ready to reestablish the invariant. *)
-          iMod ("Hclose" with "[qPts lofal Hlink Hsq nodeList hdPts'' hdPts3 what3 tailPts tailInv]") as "_".
+          iMod ("Hclose" with "[qPts lofal Hlink Hsq nodeList hdPts hdPts'' hdPts' tailPts hdPts3 what3]") as "_".
           { iNext.
-            (* We now determine that nwhat is equal to LocV ℓnext. *)
-            iDestruct (mapsto_agree with "hdPts3 hdPts''") as %[= -> ->].
-            iDestruct (mapsto_agree with "what3 tailPts") as %->.
+            iDestruct (mapsto_agree with "hdPts hdPts3") as %[= <-].
+            iDestruct (mapsto_agree with "hdPts' what3") as %[= <- <-].
             rewrite /invariant.
             iExists _, _, xs2', xsₛ2'.
             iFrame.
             iSplit; auto.
             iSplitL "qPts hdPts'' nodeList tailPts".
-            { iExists _, _, _ ,_, _, _. iFrame. iAssumption. }
+            { iExists _ ,_, _, _, _. iFrame. iAssumption. }
             iSplit; auto.
           }
           (* Step over the remainder of the code. *)
@@ -414,16 +424,16 @@ Section Queue_refinement.
       simpl.
       iInv queueN as (ℓq ℓ' xs xsₛ) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
       rewrite /isMSQueue.
-      iDestruct "isMSQ" as (ℓsentinel v ℓhdPt ℓhd q p)
-                             "(qPts & [sentinelPts sentinelPts'] & [hdPts hdPts'] & nodeList & #nodeInv)".
+      iDestruct "isMSQ" as (ℓsentinel v ℓhdPt q p)
+                             "(qPts & [sentinelPts sentinelPts'] & nodeList & #nodeInv)".
       iApply (wp_load with "qPts").
       iNext. iIntros "qPts". 
-      iMod ("Hclose" with "[qPts lofal Hlink Hsq sentinelPts' hdPts' nodeList nodeInv]") as "_".
+      iMod ("Hclose" with "[qPts lofal Hlink Hsq sentinelPts' nodeList nodeInv]") as "_".
       { iNext. iExists _, _, _, _.
         iFrame.
         iSplit; auto.
-        iSplitL "qPts sentinelPts' hdPts' nodeList".
-        { iExists _, _, _, _, _, _. iFrame. }
+        iSplitL "qPts sentinelPts' nodeList".
+        { iExists _, _, _, _, _. iFrame. iAssumption. }
         iSplit; auto.
       }
       iModIntro.
@@ -439,27 +449,58 @@ Section Queue_refinement.
       (* We are now done evaluating the argument. *)
       iApply wp_pure_step_later; auto. iNext. asimpl.
       iApply (wp_bind (fill [LetInCtx _])).
-      iApply (wp_load with "hdPts").
-      iNext. iIntros "hdPts". 
-      simpl. 
-      iApply wp_pure_step_later; auto. iNext. asimpl.
-      iApply (wp_bind (fill [CaseCtx _ _])).
-      iApply (wp_bind (fill [UnfoldCtx])).
       rewrite nodeInv_unfold.
-      iInv nodeN as (ℓhd') "(>% & Disj)" "closeNodeInv".
-      inversion H4 as [eq]. rewrite -eq. clear eq.
+      iInv nodeN as (ℓ ℓ2 q0) "(>% & Disj)" "closeNodeInv".
+      inversion_clear H4.
       (* Are we at the end yet? *)
-      iDestruct "Disj" as "[hdPts'|right]".
+      iDestruct "Disj" as "[(ℓPts & [ℓ2Pts ℓ2Pts'])|RIGHT]".
       + (* We are at the end and can attempt inserting our node. *)
-        iApply (wp_load with "hdPts'").
-        iNext. iIntros "hdPts'". 
+        iApply (wp_load with "ℓPts").
+        iNext. iIntros "ℓPts". simpl.
+        iMod ("closeNodeInv" with "[ℓPts ℓ2Pts']") as "_".
+        { iNext. iExists _, _, _. iSplit; auto. iLeft. iFrame. }
+        iModIntro.
+        iApply wp_pure_step_later; auto. iNext.
+        iApply (wp_bind (fill [CaseCtx _ _])).
+        iApply (wp_bind (fill [UnfoldCtx])).
+        simpl.
+        iApply (wp_load with "ℓ2Pts").
+        iNext. iIntros "ℓ2Pts". simpl.
+        iApply wp_pure_step_later; auto; iNext.
+        iApply wp_value.
+        iApply wp_pure_step_later; auto; iNext. simpl.
+        iApply (wp_bind (fill [IfCtx _ _])).
+        clear.
+        (* We must open the invariant, case on whether ℓ is equal to ℓ2, and
+           somehow extract that ℓ is the last node. *)
+        iInv queueN as (ℓq2 ℓ'2 xs xsₛ) "(>-> & isMSQ & >-> & Hsq & lofal & Hlink & >%)" "Hclose".
+        rewrite /isMSQueue.
+        iDestruct "isMSQ" as (ℓsentinel2 v3 ℓhdPt q2 p2)
+                              "(qPts & sentinelPts2 & nodeList & nodeinv)".
+        iInv nodeN as (ℓtup ℓ2' q0') "(>% & Disj)" "closeNodeInv".
+        { admit. }
+        inversion H2. rewrite -H4. clear H2 H4.
+        destruct (decide (ℓ2' = ℓ2)) as [|Hneq]; subst.
+        * (* We are still at the end. *)
+          iDestruct "Disj" as "[(ℓPts & ℓ2Pts2)|Right]".
+          (* The second case is a contradiction since we know that the node
+             points to the same thing as before and we have investigated that node
+             and found it to be a nil-node. *)
+          2: {
+            iDestruct "Right" as (x next) "(ℓPts' & ℓ2Pts' & nodeInvFunk)".
+            iDestruct (mapsto_agree with "ℓ2Pts ℓ2Pts'") as ">%".
+            inversion H2.
+          }
+          simpl.
+          clear.
+          destruct xs as [|x xs'].
+          -- simpl.
+             iDestruct "nodeList" as (ℓ0) "(ℓhdPt & ℓ0Pts)".
+             (* FIXME: We need to be able to conclude that ℓhdPt is equal to ℓ. *)
         admit.
-      + (* Gotta keep on going. *)
-        iDestruct "right" as (x q' ℓtail' n') "(headPts & tailPts' & nextInv)".
-      (* iMod (inv_alloc nodeN _ (nodeInv (LocV nil)) with "[nilPts1]") as "#nodeInv".
-      { iNext. rewrite nodeInv_unfold. iExists _. auto. } *)
-      iApply (wp_load with "hdPts").
-      iNext. iIntros "hdPts". 
+          -- admit.
+        * admit. (* Another thread changed the end in the meantime. *) 
+      + admit. (* Gotta keep on going. *)
   Abort.
 
 End Queue_refinement.