Commit 3a99baa4 authored by Simon Friis Vindum's avatar Simon Friis Vindum

Refactor proof and cleanup things

parent 33247d9f
......@@ -165,34 +165,25 @@ Section CG_queue.
(App (Fst (Var 0)) Unit)
).
(* Lemma CG_queue_test : WP program {{ v, ⌜v = #nv 3⌝ }}%I. *)
(* Proof. *)
(* rewrite /program. *)
(* iApply (wp_bind (fill [LetInCtx _])). *)
(* iApply wp_pure_step_later; auto. iNext. *)
(* Abort. *)
(* Representation predicate for the course grained queue. *)
Fixpoint isCGQueue_go (xs : list val) : val :=
Fixpoint isCGQueue (xs : list val) : val :=
match xs with
| nil => FoldV noneV
| x :: xs' => FoldV (InjRV (PairV x (isCGQueue_go xs')))
| x :: xs' => FoldV (InjRV (PairV x (isCGQueue xs')))
end.
Definition isCGQueue ( : loc) (xs : list val) : iProp Σ :=
↦ₛ (isCGQueue_go xs).
Definition cgQueueInv ( : loc) (xs : list val) lock : iProp Σ :=
↦ₛ (isCGQueue xs) lock ↦ₛ (#v false).
Lemma steps_CG_dequeue_cons E j K x xs lock :
nclose specN E
spec_ctx j fill K (App (CG_dequeue (Loc ) (Loc lock)) Unit)
isCGQueue (x :: xs)
lock ↦ₛ (#v false)
cgQueueInv (x :: xs) lock
|={E}=> j fill K (InjR (of_val x))
isCGQueue (xs)
lock ↦ₛ (#v false).
cgQueueInv xs lock.
Proof.
iIntros (HNE) "(#spec & Hj & isQueue & lofal)".
rewrite /isCGQueue /CG_dequeue. simpl.
rewrite /cgQueueInv /CG_dequeue. simpl.
iMod (steps_with_lock _ _ _ _ _ ( ↦ₛ FoldV (InjRV (PairV x _)))%I
_ (InjRV x) UnitV
with "[$Hj $isQueue $lofal]") as "Hj"; eauto.
......@@ -218,14 +209,12 @@ Section CG_queue.
Lemma steps_CG_dequeue_nil E j K lock :
nclose specN E
spec_ctx j fill K (App (CG_dequeue (Loc ) (Loc lock)) Unit)
isCGQueue []
lock ↦ₛ (#v false)
cgQueueInv [] lock
|={E}=> j fill K (none)
isCGQueue []
lock ↦ₛ (#v false).
cgQueueInv [] lock.
Proof.
iIntros (HNE) "(#spec & Hj & isQueue & lofal)".
rewrite /isCGQueue /CG_dequeue. simpl.
rewrite /cgQueueInv /CG_dequeue. simpl.
iMod (steps_with_lock _ _ _ _ _ ( ↦ₛ FoldV (noneV))%I
_ (noneV) UnitV
with "[$Hj $isQueue $lofal]") as "Hj"; eauto.
......@@ -251,12 +240,12 @@ Section CG_queue.
(InjR
(Pair (Fst (ids 0))
(App (ids 1) (Unfold (Snd (ids 0)))))))))
(Unfold (of_val (isCGQueue_go xs)))).
(Unfold (of_val (isCGQueue xs)))).
Lemma steps_CG_enqueue_body E j K x xs :
nclose specN E
spec_ctx j fill K (inner x xs)
|={E}=> j fill K (of_val (isCGQueue_go (xs ++ [x]))).
|={E}=> j fill K (of_val (isCGQueue (xs ++ [x]))).
Proof.
iIntros (HNE) "(#spec & Hj)".
iInduction xs as [|x' xs'] "IH" forall (K).
......@@ -281,19 +270,17 @@ Section CG_queue.
Lemma steps_CG_enqueue E j K x xs lock :
nclose specN E
spec_ctx j fill K (App (CG_enqueue (Loc ) (Loc lock)) (of_val x))
isCGQueue (xs)
lock ↦ₛ (#v false)
cgQueueInv (xs) lock
|={E}=> j fill K (Unit)
isCGQueue (xs ++ [x])
lock ↦ₛ (#v false).
cgQueueInv (xs ++ [x]) lock.
Proof.
iIntros (HNE) "(#spec & Hj & isQueue & lofal)".
iMod (steps_with_lock _ _ _ _ _ (isCGQueue _ _)
iMod (steps_with_lock _ _ _ _ _ ( ↦ₛ (isCGQueue xs))%I
_ UnitV x
with "[$Hj $isQueue $lofal]") as "Hj"; eauto.
iIntros (K') "(#Hspec & isQueue & Hj)".
iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl.
rewrite /isCGQueue.
rewrite /cgQueueInv.
iMod (step_load _ _ (UnfoldCtx :: AppRCtx (RecV _) :: StoreRCtx (LocV _) :: K') with "[Hj $isQueue]")
as "[Hj isQueue]"; eauto.
simpl.
......
......@@ -67,8 +67,7 @@ Definition MS_dequeue :=
tail <- n ;;
()
else try ()
Right c' =>
try (snd c')
Right c' => try ()
)
()
*)
......
(* This module contains definitions and lemmas that are used in the refinement
proofs of both variants of the MS-queue. *)
From Coq.Lists Require Import List.
From iris.algebra Require Import csum excl auth list gmap.
From iris.program_logic Require Import adequacy ectxi_language.
......@@ -15,15 +18,55 @@ Ltac iExistsFrame :=
(done || (iLeft; iExistsFrame) || (iRight; iExistsFrame) || fail "Could not solve goal").
Notation "◓ v" := ((1/2)%Qp, to_agree v) (at level 20).
Notation "◔ v" := ((1/4)%Qp, to_agree v) (at level 20).
Section common.
Definition noneV := InjLV UnitV.
Definition someV v := InjRV v.
Definition locO := leibnizO loc.
Definition fracAgreeR : cmraT := prodR fracR (agreeR locO).
Definition nodeStateR : cmraT := authUR mnatUR.
Context `{heapIG Σ, cfgSG Σ, inG Σ fracAgreeR, inG Σ exlTokR, inG Σ nodeUR, inG Σ nodeStateR}.
(* Lemmas and definitions for the state of a node in relation to the sentinel
position. *)
Definition nodeLive := 0 : mnat.
Definition nodeSentinel := 1 : mnat.
Definition nodeDead := 2 : mnat.
Lemma node_update ι (x y : mnat) : x y own ι ( x) == own ι ( y).
Proof.
iIntros. iApply (own_update with "[$]"). by eapply auth_update_auth, mnat_local_update.
Qed.
Lemma update_sentinel_dead ι : own ι ( nodeSentinel) == own ι ( nodeDead).
Proof. iApply node_update. unfold nodeSentinel, nodeDead. lia. Qed.
Lemma update_live_sentinel ι : own ι ( nodeLive) == own ι ( nodeSentinel).
Proof. iApply node_update. unfold nodeLive, nodeSentinel. lia. Qed.
Lemma state_agree ι q p s1 s2 : own ι ({q} s1) - own ι ({p} s2) - s1 = s2.
Proof.
iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %E%auth_auth_frac_op_invL.
Qed.
Lemma state_leq ι q (s1 s2 : mnat) : own ι ({q} s1) - own ι ( s2) - s2 s1.
Proof.
iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %[_ [a%mnat_included _]]%auth_both_frac_valid.
Qed.
(* Lemmas related to nodes. *)
(* Expresses that ℓ points to a non-nil node. *)
Definition pointsToSome : iProp Σ :=
n x next, ↦ᵢ{-} (LocV n) n ↦ᵢ{-} FoldV (someV (PairV x next)).
(* Lemmas regarding fractional agreement. *)
Lemma fracAgree_agree γ (q1 q2 : Qp) v1 v2 :
own γ (q1, to_agree v1) - own γ (q2, to_agree v2) - v1 = v2.
Proof.
......@@ -58,6 +101,8 @@ Section common.
iIntros. iApply (own_update with "[$]"). by apply cmra_update_exclusive.
Qed.
(* Auxillary lemmas. *)
Lemma mapsto_full_to_frac l v : l ↦ᵢ v - l ↦ᵢ{-} v.
Proof. iIntros. by iExists _. Qed.
......@@ -97,4 +142,26 @@ Section common.
iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[]%Qp_not_plus_q_ge_1.
Qed.
End common.
\ No newline at end of file
End common.
Section node_map.
Definition nmapUR (A : Type) : ucmraT := gmapUR loc (agreeR (leibnizO A)).
Definition nnodeUR (A : Type) : ucmraT := authUR (nmapUR A).
Context `{A : Type}.
Context `{heapIG Σ, cfgSG Σ, inG Σ fracAgreeR, inG Σ exlTokR, inG Σ (nodeUR A), inG Σ nodeStateR}.
Lemma mapUR_alloc (m : nmapUR A) (i : loc) v :
m !! i = None m ~~> (<[i := to_agree v]> m) {[ i := to_agree v ]}.
Proof. intros. by apply auth_update_alloc, alloc_singleton_local_update. Qed.
Lemma map_singleton_included (m : gmap loc A) (l : loc) v :
({[l := to_agree v]} : nmapUR A) ((to_agree <$> m) : nmapUR A) m !! l = Some v.
Proof.
move /singleton_included_l=> -[y].
rewrite lookup_fmap fmap_Some_equiv => -[[x [-> ->]]].
by move /Some_included_total /to_agree_included /leibniz_equiv_iff ->.
Qed.
End node_map.
\ No newline at end of file
......@@ -7,25 +7,18 @@ From iris_examples.logrel.F_mu_ref_conc.examples Require Import lock.
From iris_examples.logrel.F_mu_ref_conc.examples.queue Require Import
common CG_queue MS_queue.
From iris.proofmode Require Import tactics.
From iris_string_ident Require Import ltac2_string_ident.
Definition queueN : namespace := nroot .@ "queue".
Definition nodesN : namespace := nroot .@ "nodes".
Definition exlTokR : cmraT := exclR (unitR).
Definition nodeStateR : cmraT := authUR mnatUR.
Definition nodeLive := 0 : mnat.
Definition nodeSentinel := 1 : mnat.
Definition nodeDead := 2 : mnat.
Canonical Structure gnameO := leibnizO gname.
Definition mapUR : ucmraT := gmapUR loc (agreeR (leibnizO (gname * loc))).
Definition nodeUR : ucmraT := authUR (gmapUR loc (agreeR (leibnizO (gname * loc)))).
Definition mapUR : ucmraT := nmapUR (gname * loc).
Definition nodeUR : ucmraT := authUR mapUR.
Section Queue_refinement.
Context `{heapIG Σ, cfgSG Σ, inG Σ fracAgreeR, inG Σ exlTokR, inG Σ nodeUR, inG Σ nodeStateR}.
Context `{heapIG Σ, cfgSG Σ, inG Σ fracAgreeR, inG Σ nodeUR, inG Σ nodeStateR}.
Notation D := (prodO valO valO -n> iPropO Σ).
......@@ -35,30 +28,6 @@ Section Queue_refinement.
- ι for the authorative sum for the state of nodes.
*)
Definition noneV := InjLV UnitV.
Definition someV v := InjRV v.
Lemma node_update ι (x y : mnat) : x y own ι ( x) == own ι ( y).
Proof.
iIntros. iApply (own_update with "[$]"). by eapply auth_update_auth, mnat_local_update.
Qed.
Lemma update_sentinel_dead ι : own ι ( nodeSentinel) == own ι ( nodeDead).
Proof. iApply node_update. unfold nodeSentinel, nodeDead. lia. Qed.
Lemma update_live_sentinel ι : own ι ( nodeLive) == own ι ( nodeSentinel).
Proof. iApply node_update. unfold nodeLive, nodeSentinel. lia. Qed.
Lemma state_agree ι q p s1 s2 : own ι ({q} s1) - own ι ({p} s2) - s1 = s2.
Proof.
iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %E%auth_auth_frac_op_invL.
Qed.
Lemma state_leq ι q (s1 s2 : mnat) : own ι ({q} s1) - own ι ( s2) - s2 s1.
Proof.
iIntros. by iDestruct (own_valid_2 with "[$] [$]") as %[_ [a%mnat_included _]]%auth_both_frac_valid.
Qed.
Definition node_singleton s ι n : mapUR := {[ s := to_agree ((ι, n) : leibnizO (gname * loc))]}.
Definition node_mapsto κ s ι (n : loc) : iProp Σ :=
......@@ -67,7 +36,7 @@ Section Queue_refinement.
(* Represents the information that the location ℓ points to a series of nodes
correscponding to the list `xs`.
*)
Fixpoint isNodeList γ κ ( : loc) (xs : list val) : iProp Σ :=
Fixpoint isMSQueue γ κ ( : loc) (xs : list val) : iProp Σ :=
match xs with
| nil => 2, ↦ᵢ{1/2} (LocV 2) 2 ↦ᵢ{-} FoldV noneV own γ ( )
| x :: xs' =>
......@@ -75,7 +44,7 @@ Section Queue_refinement.
own κ ( {[ 2 := to_agree (ι, next) ]})
own ι ({1/2} nodeLive)
↦ᵢ{-} (LocV 2) 2 ↦ᵢ{-} FoldV (someV (PairV (InjRV x) (LocV next)))
isNodeList γ κ next xs')
isMSQueue γ κ next xs')
end.
Definition nextNode γ κ into : iProp Σ :=
......@@ -101,7 +70,7 @@ Section Queue_refinement.
((* ℓ is dead. It has been the sentinel, but no longer is. *)
(own ι ( nodeDead)
(* We know that the node points to a non-nil node. *)
x' b next, toNext ↦ᵢ{-} LocV next next ↦ᵢ{-} FoldV (someV (PairV x' b)))
pointsToSome toNext)
(* ℓn is currently the sentinel. *)
(own ι ({1/2} nodeSentinel)
q ↦ᵢ{1/2} (LocV n)) (* We own half the pointer into the sentinel. *)
......@@ -109,14 +78,14 @@ Section Queue_refinement.
(own ι ({1/2} nodeLive))).
(* Predicate expressing that ℓq points to a queue with the values xs *)
Definition isMSQueue γ κ (τi : D) (q t : loc) (xs : list val) : iProp Σ :=
Definition msQueueInv γ κ (q t : loc) (xs : list val) : iProp Σ :=
( sentinel last hdPt pt ι ι',
q ↦ᵢ{1/2} (LocV sentinel) (* queue own half the pointer, the sentinels owns the other half. *)
node_mapsto κ sentinel ι hdPt
t ↦ᵢ LocV last
node_mapsto κ last ι' pt
own ι ({1/2} nodeSentinel)
isNodeList γ κ hdPt xs).
isMSQueue γ κ hdPt xs).
(* Ties the map to nodeInv *)
Definition map_map γ κ q (m : gmap loc (gname * loc)) : iProp Σ :=
......@@ -127,10 +96,6 @@ Section Queue_refinement.
own κ ( (to_agree <$> m) : nodeUR)
map_map γ κ q m.
Lemma mapUR_alloc (m : mapUR) (i : loc) v :
m !! i = None m ~~> (<[i := to_agree v]> m) {[ i := to_agree v ]}.
Proof. intros. by apply auth_update_alloc, alloc_singleton_local_update. Qed.
Lemma insert_node_subset γ κ q s ι n m m' :
m' m -
m !! s = None -
......@@ -171,14 +136,6 @@ Section Queue_refinement.
iExistsFrame.
Qed.
Lemma map_singleton_included (m : gmap loc (gname * loc)) (l : loc) v :
({[l := to_agree v]} : mapUR) ((to_agree <$> m) : mapUR) m !! l = Some v.
Proof.
move /singleton_included_l=> -[y].
rewrite lookup_fmap fmap_Some_equiv => -[[x [-> ->]]].
by move /Some_included_total /to_agree_included /leibniz_equiv_iff ->.
Qed.
Lemma auth_node_mapsto_Some γ m s ι n :
own γ ( (to_agree <$> m) : nodeUR) -
node_mapsto γ s ι n -
......@@ -254,9 +211,8 @@ Section Queue_refinement.
Definition queueInv γ κ τi q t s lock: iProp Σ :=
( xs xs,
isMSQueue γ κ τi q t xs
isCGQueue s xs
lock ↦ₛ (#v false)
msQueueInv γ κ q t xs
cgQueueInv s xs lock
[ list] x ; x xs ; xs, τi (x, x))%I.
(* With the token and the nodeList one can perform a CAS on the last node. *)
......@@ -269,7 +225,7 @@ Section Queue_refinement.
nil ↦ᵢ FoldV (InjLV UnitV)
tail ↦ᵢ (LocV nil) (* ℓtail points to the nil node *)
node ↦ᵢ (FoldV (InjRV (PairV (InjRV x) (LocV tail)))) (* node contains x and points to nil *)
isNodeList γ κ hdPt xs
isMSQueue γ κ hdPt xs
↦ᵢ{1/2} (LocV 2)
own γ ( ) (* Proof that ℓ is the pointer pointing to nil. *)
}}}
......@@ -279,20 +235,20 @@ Section Queue_refinement.
own κ ( (to_agree <$> (<[node := (ι, tail)]> m)) : nodeUR)
map_map γ κ q (delete sentinel (<[node := (ι, tail)]>m))
node ↦ᵢ{-} (FoldV (InjRV (PairV (InjRV x) (LocV tail))))
isNodeList γ κ hdPt (xs ++ [x])
isMSQueue γ κ hdPt (xs ++ [x])
node_mapsto κ node ι tail
↦ᵢ{-} (LocV node)
}}}.
Proof.
iIntros (ϕ) "(% & authM & bigSep & #nodesInv & nilPts & tailPts & nodePts & nodeList & ℓPts & tok) Hϕ".
iIntros (ϕ) "(%Neq & authM & bigSep & #nodesInv & nilPts & tailPts & nodePts & nodeList & ℓPts & tok) Hϕ".
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 & _ &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.
iDestruct (mapsto_combine with "ℓhdPt ℓPts") as "[ℓpts %Eq]".
inversion_clear Eq.
rewrite Qp_half_half.
iMod (fracAgree_update with "tok tok'") as "[tok tok']".
iMod (own_alloc ( nodeLive _)) as (ι) "[[authNodeState authNodeState'] _]".
......@@ -325,29 +281,24 @@ Section Queue_refinement.
iExistsFrame.
Qed.
(* This lemma has been commited upstream to Iris and will be available in the future. *)
Lemma auth_update_core_id_frac {A : ucmraT} (a b : A) `{!CoreId b} q :
b a {q} a ~~> {q} a b.
Proof. Admitted.
Lemma cas_tail_node γ κ τi q t s lock node ι tail prev :
{{{ inv queueN (queueInv γ κ τi q t s lock) node_mapsto κ node ι tail }}}
CAS (Loc t) (Loc prev) (Loc node)
{{{ v, RET v; True }}}.
Proof.
iIntros (ϕ) "#[inv mapsto] Hϕ".
iInv queueN as (xs xs) "(isMSQ & Hsq & lofal & Hlink)" "Hclose".
rewrite /isMSQueue.
iInv queueN as (xs xs) "(isMSQ & Hsq & Hlink)" "Hclose".
rewrite /msQueueInv.
iDestruct "isMSQ" as (sentinel last hdPt' t' ι2 ι3)
"(qPts & lastMapsto & tPts & tailMapsto & sentState & nodeList)".
destruct (decide (prev = last)) as [|Hneq]; subst.
- iApply (wp_cas_suc with "tPts"); auto. iNext.
iIntros "tPts".
iMod ("Hclose" with "[qPts lastMapsto tPts tailMapsto lofal Hlink Hsq sentState nodeList]") as "_".
iMod ("Hclose" with "[qPts lastMapsto tPts tailMapsto Hlink Hsq sentState nodeList]") as "_".
{ iNext. iExistsN. iFrame. iExistsN. iFrame "tPts". iFrame. iAssumption. }
by iApply "Hϕ".
- iApply (wp_cas_fail with "tPts"). congruence. iNext. iIntros "tPts".
iMod ("Hclose" with "[qPts lastMapsto tPts tailMapsto lofal Hlink Hsq sentState nodeList]") as "_".
iMod ("Hclose" with "[qPts lastMapsto tPts tailMapsto Hlink Hsq sentState nodeList]") as "_".
{ iNext. iExistsFrame. }
by iApply "Hϕ".
Qed.
......@@ -362,7 +313,7 @@ Section Queue_refinement.
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). }
{ by apply (auth_update_core_id _ _ nodeSentinel). }
iApply (wp_load with "qPts"). iNext. iIntros "qPts".
iMod ("Hclose" with "[-Hϕ nodeState]"). { iNext. iExistsFrame. }
iModIntro. iApply "Hϕ". auto.
......@@ -508,8 +459,8 @@ Section Queue_refinement.
}
2: { iDestruct (state_leq with "live nodeState") as %le. inversion le. }
iDestruct "sent" as ">(authState & qPts)".
iInv queueN as (xs2 xs2) "(isMSQ & >Hsq & >lofal & Hlink)" "closeQueueInv".
rewrite /isMSQueue.
iInv queueN as (xs2 xs2) "(isMSQ & >Hsq & Hlink)" "closeQueueInv".
rewrite /msQueueInv.
iDestruct "isMSQ" as (sentinel2 last2 hdPt2 pt2 ι2 ι2')
"(>qPts2 & >#fragO' & >tPts & >lastMapsto & >nodeState' & nodeList)".
(* We can conclude that the queue still points to the same sentinel that
......@@ -526,16 +477,16 @@ Section Queue_refinement.
iDestruct (mapsto_agree_frac_frac with "nPts ℓ2Pts") as %[=].
}
destruct xs2 as [|x2' xs2'].
2: { iDestruct (big_sepL2_length with "Hlink") as ">%". inversion H6. }
2: { iDestruct (big_sepL2_length with "Hlink") as ">%Eq". inversion Eq. }
simpl.
(* We now step over the specification code. *)
iMod (steps_CG_dequeue_nil with "[$Hspec $Hj $Hsq $lofal]") as "(Hj & Hsq & lofal)".
iMod (steps_CG_dequeue_nil with "[$Hspec $Hj $Hsq]") as "(Hj & Hsq)".
{ solve_ndisj. }
iApply (wp_load with "[$hdPtPts]"). iNext. iIntros "hdPtPts".
(* We now close all the invariants that we opened. *)
iDestruct (reinsert_node with "authM fragO bigSep [sentinelPts authState qPts2 hdPtPts nPts' tok]") as "(authM & bigSep)".
{ iExistsN. iFrame. iSplitL "hdPtPts nPts' tok"; iExistsFrame. }
iMod ("closeQueueInv" with "[qPts tPts lastMapsto lofal Hsq nodeList nodeState']") as "_".
iMod ("closeQueueInv" with "[qPts tPts lastMapsto Hsq nodeList nodeState']") as "_".
{ iNext. iExists [], []. simpl. iExistsFrame. }
iModIntro.
iMod ("closeNodesInv" with "[authM bigSep]") as "_".
......@@ -580,8 +531,8 @@ Section Queue_refinement.
iApply wp_value. simpl.
iApply (wp_load_frac with "hdPtPts"). iNext. iIntros "hdPtPts".
simpl.
iInv queueN as (xs2 xs2) "(isMSQ & Hsq & lofal & Hlink)" "Hclose".
rewrite /isMSQueue.
iInv queueN as (xs2 xs2) "(isMSQ & Hsq & Hlink)" "Hclose".
rewrite /msQueueInv.
iDestruct "isMSQ" as (sentinel2 last2 hdPt2 pt2 ι3 ι'3)
"(>qPts & >#fragO' & tPts & lastMapsto & >sentinelState & nodeList)".
(* We now open the nodes invariant. *)
......@@ -629,7 +580,7 @@ Section Queue_refinement.
iDestruct (mapsto_agree_frac_frac with "otherPts tailPts") as %[= -> ->].
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)".
iMod (steps_CG_dequeue_cons with "[$Hspec $Hj $Hsq]") as "(Hj & Hsq)".
{ solve_ndisj. }
(* We split qPts again such that we can put one half in the sentinel
invariant and one half directly in the queue invariant. *)
......@@ -648,7 +599,7 @@ Section Queue_refinement.
{ iNext. iExistsFrame. }
iModIntro.
(* We are now ready to reestablish the invariant. *)
iMod ("Hclose" with "[qPts tPts lastMapsto lofal Hlink Hsq nodeList nodeState1]") as "_".
iMod ("Hclose" with "[qPts tPts lastMapsto Hlink Hsq nodeList nodeState1]") as "_".
{ iNext. iExistsFrame. }
(* Step over the remainder of the code. *)
iModIntro. simpl.
......@@ -673,7 +624,7 @@ Section Queue_refinement.
iMod ("closeNodesInv" with "[authM bigSep]") as "_".
{ iNext. iExistsFrame. }
iModIntro.
iMod ("Hclose" with "[qPts tPts lastMapsto lofal Hsq nodeList sentinelState' Hlink]") as "_".
iMod ("Hclose" with "[qPts tPts lastMapsto Hsq nodeList sentinelState' Hlink]") as "_".
{ iNext. iExistsFrame. }
iModIntro.
iApply wp_pure_step_later; auto. iNext.
......@@ -765,8 +716,8 @@ Section Queue_refinement.
iApply (wp_bind (fill [IfCtx _ _])).
(* 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".
rewrite /isMSQueue.
iInv queueN as (xs xs) "(isMSQ & Hsq & Hlink)" "Hclose".
rewrite /msQueueInv.
iDestruct "isMSQ" as (sentinel2 last2 hdPt' t2 ι2 ι2')
"(qPts & nextMapsto' & tPts & tailMapsto & sentState' & nodeList)".
(* Lookup node *)
......@@ -796,14 +747,14 @@ Section Queue_refinement.
{ done. }
iNext.
iDestruct 1 as (ι3) "(authM & bigSep & nodePts & nodeList & #frag & ℓPts)".
iMod (steps_CG_enqueue with "[$Hspec $Hj $lofal $Hsq]") as "(Hj & Hsq & lofal)".
iMod (steps_CG_enqueue with "[$Hspec $Hj $Hsq]") as "(Hj & Hsq)".
{ solve_ndisj. }
iDestruct (reinsert_node with "authM nextMapsto bigSep [sentinelPts ℓPts nodePts rest]") as "(authM & bigSep)".
{ iExistsFrame. }
iMod ("closeNodesInv" with "[authM bigSep]").
{ iNext. iExists _. iFrame. }
iModIntro.
iMod ("Hclose" with "[qPts tPts tailMapsto lofal Hlink Hsq nodeList sentState' nextMapsto']") as "_".
iMod ("Hclose" with "[qPts tPts tailMapsto Hlink Hsq nodeList sentState' nextMapsto']") as "_".
{ iNext. iExists (xs ++ [v1]), (xs ++ [v2]).
iFrame.
iSplitL; first iExistsFrame.
......@@ -828,7 +779,7 @@ Section Queue_refinement.
iMod ("closeNodesInv" with "[authM bigSep]").
{ iNext. iExistsFrame. }
iModIntro.
iMod ("Hclose" with "[qPts tPts tailMapsto lofal Hlink Hsq nodeList sentState' nextMapsto']") as "_".
iMod ("Hclose" with "[qPts tPts tailMapsto Hlink Hsq nodeList sentState' nextMapsto']") as "_".
{ iNext. iExists xs, xs. iExistsFrame. }
iModIntro.
simpl.
......@@ -842,7 +793,7 @@ Section Queue_refinement.
iMod ("closeNodesInv" with "[authM bigSep]").
{ iNext. iExists _. iFrame. }
iModIntro.
iMod ("Hclose" with "[qPts tPts tailMapsto lofal Hlink Hsq nodeList sentState' nextMapsto']") as "_".
iMod ("Hclose" with "[qPts tPts tailMapsto Hlink Hsq nodeList sentState' nextMapsto']") as "_".
{ iNext. iExists xs, xs. iExistsFrame. }
iModIntro.