Commit d579dc8d authored by Ralf Jung's avatar Ralf Jung

bump Iris for comparison changes

parent 06edc222
Pipeline #17790 passed with stage
in 17 minutes and 34 seconds
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-06-18.2.e039d7c7") | (= "dev") }
"coq-iris" { (= "dev.2019-06-18.8.72595700") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -36,9 +36,19 @@ Section stacks.
iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
Qed.
Definition is_list_pre (P : val iProp Σ) (F : val -d> iProp Σ) :
val -d> iProp Σ := λ v,
(v NONEV (l : loc) (h t : val), v SOMEV #l l {-} (h, t)%V P h F t)%I.
Definition oloc_to_val (ol: option loc) : val :=
match ol with
| None => NONEV
| Some loc => SOMEV (#loc)
end.
Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
Proof. intros [|][|]; simpl; congruence. Qed.
Definition is_list_pre (P : val iProp Σ) (F : option loc -d> iProp Σ) :
option loc -d> iProp Σ := λ v, match v with
| None => True
| Some l => (h : val) (t : option loc), l {-} (h, oloc_to_val t)%V P h F t
end%I.
Local Instance is_list_contr (P : val iProp Σ) : Contractive (is_list_pre P).
Proof.
......@@ -58,28 +68,22 @@ Section stacks.
rewrite is_list_eq. apply (fixpoint_unfold (is_list_pre P)).
Qed.
(* TODO: shouldn't have to explicitly return is_list *)
Lemma is_list_unboxed (P : val iProp Σ) v :
is_list P v - val_is_unboxed v is_list P v.
Proof.
iIntros "Hstack"; iSplit; last done;
iDestruct (is_list_unfold with "Hstack") as "[->|Hstack]";
last iDestruct "Hstack" as (l h t) "(-> & _)"; done.
Qed.
Lemma is_list_disj (P : val iProp Σ) v :
is_list P v - is_list P v (v NONEV (l : loc) h t, v SOMEV #l%V l {-} (h, t)%V).
Lemma is_list_dup (P : val iProp Σ) v :
is_list P v - is_list P v match v with
| None => True
| Some l => h t, l {-} (h, oloc_to_val t)%V
end.
Proof.
iIntros "Hstack".
iDestruct (is_list_unfold with "Hstack") as "[%|Hstack]"; simplify_eq.
- rewrite is_list_unfold; iSplitR; [iLeft|]; eauto.
- iDestruct "Hstack" as (l h t) "(% & Hl & Hlist)".
iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]"; simplify_eq.
rewrite (is_list_unfold _ (InjRV _)); iSplitR "Hl2"; iRight; iExists _, _, _; by iFrame.
iIntros "Hstack". iDestruct (is_list_unfold with "Hstack") as "Hstack".
destruct v as [l|].
- iDestruct "Hstack" as (h t) "(Hl & Hlist)".
iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
rewrite (is_list_unfold _ (Some _)); iSplitR "Hl2"; iExists _, _; by iFrame.
- rewrite is_list_unfold; iSplitR; eauto.
Qed.
Definition stack_inv P v :=
( l v', v = #l l v' is_list P v')%I.
( l ol', v = #l l oloc_to_val ol' is_list P ol')%I.
Definition is_stack (P : val iProp Σ) v :=
inv N (stack_inv P v).
......@@ -92,8 +96,8 @@ Section stacks.
wp_lam.
wp_alloc as "Hl".
iMod (inv_alloc N (stack_inv P #) with "[Hl]") as "Hinv".
{ iNext; iExists , NONEV; iFrame;
by iSplit; last (iApply is_list_unfold; iLeft). }
{ iNext; iExists , None; iFrame;
by iSplit; last (iApply is_list_unfold). }
by iApply "Hpost".
Qed.
......@@ -109,17 +113,17 @@ Section stacks.
{ iNext; iExists _, _; by iFrame. }
iModIntro. wp_let. wp_alloc ' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
iInv N as ('' v'') "(>% & >Hl & Hlist)" "Hclose"; simplify_eq.
destruct (decide (v' = v'')) as [ -> |].
- iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
wp_cas_suc.
destruct (decide (v' = v'')) as [->|Hne].
- wp_cas_suc. { destruct v''; left; done. }
iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
{ iNext; iExists _, (InjRV #'); iFrame; iSplit; first done;
rewrite (is_list_unfold _ (InjRV _)). iRight; iExists _, _, _; iFrame; eauto. }
{ iNext; iExists _, (Some '); iFrame; iSplit; first done;
rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
iModIntro.
wp_if.
by iApply "HΦ".
- iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
wp_cas_fail.
- wp_cas_fail.
{ destruct v', v''; simpl; congruence. }
{ destruct v''; left; done. }
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
iModIntro.
......@@ -134,37 +138,36 @@ Section stacks.
iLöb as "IH".
wp_lam. wp_bind (Load _).
iInv N as ( v') "(>% & Hl & Hlist)" "Hclose"; subst.
iDestruct (is_list_dup with "Hlist") as "[Hlist Hlist2]".
wp_load.
iDestruct (is_list_disj with "Hlist") as "[Hlist Hdisj]".
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
iModIntro.
iDestruct "Hdisj" as "[-> | Heq]".
destruct v' as [l|]; last first.
- wp_match.
iApply "HΦ"; by iLeft.
- iDestruct "Heq" as (l h t) "[-> Hl]".
wp_match. wp_bind (Load _).
- wp_match. wp_bind (Load _).
iInv N as (' v') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
iDestruct "Hl" as (q) "Hl".
iDestruct "Hlist2" as (???) "Hl".
wp_load.
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists _, _; by iFrame. }
iModIntro.
wp_pures. wp_bind (CAS _ _ _).
iInv N as ('' v'') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
destruct (decide (v'' = InjRV #l)) as [-> |].
destruct (decide (v'' = (Some l))) as [-> |].
* rewrite is_list_unfold.
iDestruct "Hlist" as "[>% | H]"; first done.
iDestruct "H" as (''' h' t') "(>% & Hl'' & HP & Hlist)"; simplify_eq.
iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
iDestruct "Hl''" as (q') "Hl''".
simpl.
wp_cas_suc.
iDestruct (mapsto_agree with "Hl'' Hl") as "%"; simplify_eq.
iDestruct (mapsto_agree with "Hl'' Hl") as %[= <- <-%oloc_to_val_inj].
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists '', _; by iFrame. }
iModIntro.
wp_pures.
iApply ("HΦ" with "[HP]"); iRight; iExists h; by iFrame.
* wp_cas_fail.
iApply ("HΦ" with "[HP]"); iRight; iExists _; by iFrame.
* wp_cas_fail. { destruct v''; simpl; congruence. }
iMod ("Hclose" with "[Hl' Hlist]") as "_".
{ iNext; iExists '', _; by iFrame. }
iModIntro.
......
......@@ -246,9 +246,19 @@ Section stack_works.
iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
Qed.
Definition is_list_pre (P : val iProp Σ) (F : val -d> iProp Σ) :
val -d> iProp Σ := λ v,
(v NONEV (l : loc) (h t : val), v SOMEV #l l {-} (h, t)%V P h F t)%I.
Definition oloc_to_val (ol: option loc) : val :=
match ol with
| None => NONEV
| Some loc => SOMEV (#loc)
end.
Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
Proof. intros [|][|]; simpl; congruence. Qed.
Definition is_list_pre (P : val iProp Σ) (F : option loc -d> iProp Σ) :
option loc -d> iProp Σ := λ v, match v with
| None => True
| Some l => (h : val) (t : option loc), l {-} (h, oloc_to_val t)%V P h F t
end%I.
Local Instance is_list_contr (P : val iProp Σ) : Contractive (is_list_pre P).
Proof.
......@@ -268,27 +278,21 @@ Section stack_works.
rewrite is_list_eq. apply (fixpoint_unfold (is_list_pre P)).
Qed.
(* TODO: shouldn't have to explicitly return is_list *)
Lemma is_list_unboxed (P : val iProp Σ) v :
is_list P v - val_is_unboxed v is_list P v.
Proof.
iIntros "Hstack"; iSplit; last done;
iDestruct (is_list_unfold with "Hstack") as "[->|Hstack]";
last iDestruct "Hstack" as (l h t) "(-> & _)"; done.
Qed.
Lemma is_list_disj (P : val iProp Σ) v :
is_list P v - is_list P v (v NONEV (l : loc) h t, v SOMEV #l%V l {-} (h, t)%V).
Lemma is_list_dup (P : val iProp Σ) v :
is_list P v - is_list P v match v with
| None => True
| Some l => h t, l {-} (h, oloc_to_val t)%V
end.
Proof.
iIntros "Hstack".
iDestruct (is_list_unfold with "Hstack") as "[%|Hstack]"; simplify_eq.
- rewrite is_list_unfold; iSplitR; [iLeft|]; eauto.
- iDestruct "Hstack" as (l h t) "(% & Hl & Hlist)".
iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]"; simplify_eq.
rewrite (is_list_unfold _ (InjRV _)); iSplitR "Hl2"; iRight; iExists _, _, _; by iFrame.
iIntros "Hstack". iDestruct (is_list_unfold with "Hstack") as "Hstack".
destruct v as [l|].
- iDestruct "Hstack" as (h t) "(Hl & Hlist)".
iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
rewrite (is_list_unfold _ (Some _)); iSplitR "Hl2"; iExists _, _; by iFrame.
- rewrite is_list_unfold; iSplitR; eauto.
Qed.
Definition stack_inv P l := ( v, l v is_list P v)%I.
Definition stack_inv P l := ( v, l oloc_to_val v is_list P v)%I.
Definition is_stack P v :=
( mailbox l, v = (mailbox, #l)%V is_mailbox Nmailbox P mailbox inv N (stack_inv P l))%I.
......@@ -302,7 +306,7 @@ Section stack_works.
wp_apply mk_mailbox_works; first done.
iIntros (mailbox) "#Hmailbox".
iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hinv".
{ by iNext; iExists _; iFrame; rewrite is_list_unfold; iLeft. }
{ iNext; iExists None; iFrame. rewrite is_list_unfold. done. }
wp_pures; iModIntro; iApply "Hpost"; iExists _, _; auto.
Qed.
......@@ -325,16 +329,16 @@ Section stack_works.
wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
iInv N as (list) "(Hl & Hlist)" "Hclose".
destruct (decide (v'' = list)) as [ -> |].
* iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
wp_cas_suc.
* wp_cas_suc. { destruct list; left; done. }
iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
{ iNext; iExists (SOMEV _); iFrame.
rewrite (is_list_unfold _ (InjRV _)). iRight; iExists _, _, _; iFrame; eauto. }
{ iNext; iExists (Some _); iFrame.
rewrite (is_list_unfold _ (Some _)). iExists _, _; iFrame; eauto. }
iModIntro.
wp_if.
by iApply "HΦ".
* iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
wp_cas_fail.
* wp_cas_fail.
{ destruct list, v''; simpl; congruence. }
{ destruct list; left; done. }
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
iModIntro.
......@@ -355,27 +359,25 @@ Section stack_works.
- wp_match. wp_bind (Load _).
iInv N as (list) "[Hl Hlist]" "Hclose".
wp_load.
iDestruct (is_list_disj with "Hlist") as "[Hlist Hdisj]".
iDestruct (is_list_dup with "Hlist") as "[Hlist Hlist2]".
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
iModIntro.
iDestruct "Hdisj" as "[-> | Heq]".
destruct list as [list|]; last first.
* wp_match.
iApply "HΦ"; by iLeft.
* iDestruct "Heq" as (l' h t) "[-> Hl']".
wp_match. wp_bind (Load _).
* wp_match. wp_bind (Load _).
iInv N as (v') "[>Hl Hlist]" "Hclose".
iDestruct "Hl'" as (q) "Hl'".
iDestruct "Hlist2" as (???) "Hl'".
wp_load.
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
iModIntro.
wp_let. wp_proj. wp_bind (CAS _ _ _). wp_pures.
iInv N as (v'') "[Hl Hlist]" "Hclose".
destruct (decide (v'' = InjRV #l')) as [-> |].
destruct (decide (v'' = Some list)) as [-> |].
+ rewrite is_list_unfold.
iDestruct "Hlist" as "[>% | H]"; first done.
iDestruct "H" as (l'' h' t') "(>% & Hl'' & HP & Hlist)"; simplify_eq.
iDestruct "Hlist" as (h' t') "(Hl'' & HP & Hlist)".
iDestruct "Hl''" as (q') "Hl''".
wp_cas_suc.
iDestruct (mapsto_agree with "Hl'' Hl'") as "%"; simplify_eq.
......@@ -383,8 +385,8 @@ Section stack_works.
{ iNext; iExists _; by iFrame. }
iModIntro.
wp_pures.
iApply ("HΦ" with "[HP]"); iRight; iExists h; by iFrame.
+ wp_cas_fail.
iApply ("HΦ" with "[HP]"); iRight; iExists _; by iFrame.
+ wp_cas_fail. { destruct v''; simpl; congruence. }
iMod ("Hclose" with "[Hl Hlist]") as "_".
{ iNext; iExists _; by iFrame. }
iModIntro.
......
......@@ -44,47 +44,51 @@ Section stack_works.
iApply (mapsto_agree with "H1 H2").
Qed.
Definition oloc_to_val (ol: option loc) : val :=
match ol with
| None => NONEV
| Some loc => SOMEV (#loc)
end.
Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
Proof. intros [|][|]; simpl; congruence. Qed.
Fixpoint is_list xs v : iProp Σ :=
(match xs with
| [] => v = NONEV
| x :: xs => l (t : val), v = SOMEV #l%V l {-} (x, t)%V is_list xs t
(match xs, v with
| [], None => True
| x :: xs, Some l => t, l {-} (x, oloc_to_val t)%V is_list xs t
| _, _ => False
end)%I.
Lemma is_list_disj xs v :
is_list xs v - is_list xs v (v = NONEV l (h t : val), v = SOMEV #l l {-} (h, t)%V).
Lemma is_list_dup xs v :
is_list xs v - is_list xs v match v with
| None => True
| Some l => h t, l {-} (h, oloc_to_val t)%V
end.
Proof.
destruct xs; auto.
iIntros "H"; iDestruct "H" as (l t) "(-> & Hl & Hstack)".
destruct xs, v; simpl; auto; first by iIntros "[]".
iIntros "H"; iDestruct "H" as (t) "(Hl & Hstack)".
iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
iSplitR "Hl2"; first by (iExists _, _; iFrame). iRight; auto.
Qed.
Lemma is_list_unboxed xs v :
is_list xs v - val_is_unboxed v is_list xs v.
Proof.
iIntros "Hlist"; iDestruct (is_list_disj with "Hlist") as "[$ Heq]".
iDestruct "Heq" as "[-> | H]"; first done; by iDestruct "H" as (? ? ?) "[-> ?]".
iSplitR "Hl2"; first by (iExists _; iFrame). by iExists _, _.
Qed.
Lemma is_list_empty xs :
is_list xs (InjLV #()) - xs = [].
is_list xs None - xs = [].
Proof.
destruct xs; iIntros "Hstack"; auto.
iDestruct "Hstack" as (? ?) "(% & H)"; discriminate.
Qed.
Lemma is_list_cons xs l h t :
l {-} (h, t)%V -
is_list xs (InjRV #l) -
is_list xs (Some l) -
ys, xs = h :: ys.
Proof.
destruct xs; first by iIntros "? %".
iIntros "Hl Hstack"; iDestruct "Hstack" as (l' t') "(% & Hl' & Hrest)"; simplify_eq.
iIntros "Hl Hstack"; iDestruct "Hstack" as (t') "(Hl' & Hrest)".
iDestruct (partial_mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
Qed.
Definition stack_inv P l :=
( v xs, l v is_list xs v P xs)%I.
( v xs, l oloc_to_val v is_list xs v P xs)%I.
Definition is_stack_pred P v :=
( l, v = #l inv N (stack_inv P l))%I.
......@@ -96,7 +100,7 @@ Section stack_works.
rewrite -wp_fupd.
wp_lam. wp_alloc l as "Hl".
iMod (inv_alloc N _ (stack_inv P l) with "[Hl HP]") as "#Hinv".
{ by iNext; iExists _, []; iFrame. }
{ iNext; iExists None, []; iFrame. }
iModIntro; iApply "HΦ"; iExists _; auto.
Qed.
......@@ -116,16 +120,17 @@ Section stack_works.
iModIntro.
wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
iInv N as (list' xs) "(Hl & Hlist & HP)" "Hclose".
iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
destruct (decide (list = list')) as [ -> |].
- wp_cas_suc.
- wp_cas_suc. { destruct list'; left; done. }
iMod ("Hupd" with "HP") as "[HP HΨ]".
iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_".
{ iNext; iExists (SOMEV _), (v :: xs); iFrame; iExists _, _; iFrame; auto. }
{ iNext; iExists (Some _), (v :: xs); iFrame; iExists _; iFrame; auto. }
iModIntro.
wp_if.
by iApply ("HΦ" with "HΨ").
- wp_cas_fail.
{ destruct list, list'; simpl; congruence. }
{ destruct list'; left; done. }
iMod ("Hclose" with "[Hl HP Hlist]").
{ iExists _, _; iFrame. }
iModIntro.
......@@ -146,8 +151,8 @@ Section stack_works.
wp_lam. wp_bind (Load _).
iInv N as (v xs) "(Hl & Hlist & HP)" "Hclose".
wp_load.
iDestruct (is_list_disj with "Hlist") as "[Hlist H]".
iDestruct "H" as "[-> | HSome]".
iDestruct (is_list_dup with "Hlist") as "[Hlist H]".
destruct v as [l'|]; last first.
- iDestruct (is_list_empty with "Hlist") as %->.
iDestruct "Hupd" as "[_ Hupdnil]".
iMod ("Hupdnil" with "HP") as "[HP HΨ]".
......@@ -156,7 +161,7 @@ Section stack_works.
iModIntro.
wp_match.
iApply ("HΦ" with "HΨ").
- iDestruct "HSome" as (l' h t) "[-> Hl']".
- iDestruct "H" as (h t) "Hl'".
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
......@@ -169,13 +174,13 @@ Section stack_works.
iModIntro.
wp_let. wp_proj. wp_bind (CAS _ _ _). wp_pures.
iInv N as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
destruct (decide (v' = (SOMEV #l'))) as [ -> |].
destruct (decide (v' = (Some l'))) as [ -> |].
* wp_cas_suc.
iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
simplify_eq.
iDestruct "Hupd" as "[Hupdcons _]".
iMod ("Hupdcons" with "HP") as "[HP HΨ]".
iDestruct "Hlist" as (l'' t') "(% & Hl'' & Hlist)"; simplify_eq.
iDestruct "Hlist" as (t') "(Hl'' & Hlist)".
iDestruct "Hl''" as (q') "Hl''".
iDestruct (mapsto_agree with "Hl' Hl''") as "%"; simplify_eq.
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
......@@ -183,7 +188,7 @@ Section stack_works.
iModIntro.
wp_pures.
iApply ("HΦ" with "HΨ").
* wp_cas_fail.
* wp_cas_fail. { destruct v'; simpl; congruence. }
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
......
......@@ -267,47 +267,51 @@ Section proofs.
iApply (mapsto_agree with "H1 H2").
Qed.
Definition oloc_to_val (ol: option loc) : val :=
match ol with
| None => NONEV
| Some loc => SOMEV (#loc)
end.
Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
Proof. intros [|][|]; simpl; congruence. Qed.
Fixpoint is_list xs v : iProp Σ :=
(match xs with
| [] => v = NONEV
| x :: xs => l (t : val), v = SOMEV #l%V l {-} (x, t)%V is_list xs t
(match xs, v with
| [], None => True
| x :: xs, Some l => t, l {-} (x, oloc_to_val t)%V is_list xs t
| _, _ => False
end)%I.
Lemma is_list_disj xs v :
is_list xs v - is_list xs v (v = NONEV l (h t : val), v = SOMEV #l l {-} (h, t)%V).
Lemma is_list_dup xs v :
is_list xs v - is_list xs v match v with
| None => True
| Some l => h t, l {-} (h, oloc_to_val t)%V
end.
Proof.
destruct xs; auto.
iIntros "H"; iDestruct "H" as (l t) "(-> & Hl & Hstack)".
destruct xs, v; simpl; auto; first by iIntros "[]".
iIntros "H"; iDestruct "H" as (t) "(Hl & Hstack)".
iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
iSplitR "Hl2"; first by (iExists _, _; iFrame). iRight; auto.
Qed.
Lemma is_list_unboxed xs v :
is_list xs v - val_is_unboxed v is_list xs v.
Proof.
iIntros "Hlist"; iDestruct (is_list_disj with "Hlist") as "[$ Heq]".
iDestruct "Heq" as "[-> | H]"; first done; by iDestruct "H" as (? ? ?) "[-> ?]".
iSplitR "Hl2"; first by (iExists _; iFrame). by iExists _, _.
Qed.
Lemma is_list_empty xs :
is_list xs (InjLV #()) - xs = [].
is_list xs None - xs = [].
Proof.
destruct xs; iIntros "Hstack"; auto.
iDestruct "Hstack" as (? ?) "(% & H)"; discriminate.
Qed.
Lemma is_list_cons xs l h t :
l {-} (h, t)%V -
is_list xs (InjRV #l) -
is_list xs (Some l) -
ys, xs = h :: ys.
Proof.
destruct xs; first by iIntros "? %".
iIntros "Hl Hstack"; iDestruct "Hstack" as (l' t') "(% & Hl' & Hrest)"; simplify_eq.
iIntros "Hl Hstack"; iDestruct "Hstack" as (t') "(Hl' & Hrest)".
iDestruct (partial_mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
Qed.
Definition stack_inv P l :=
( v xs, l v is_list xs v P xs)%I.
( v xs, l oloc_to_val v is_list xs v P xs)%I.
Definition is_stack_pred P v :=
( mailbox l, v = (mailbox, #l)%V is_mailbox P mailbox inv Nstack (stack_inv P l))%I.
......@@ -321,7 +325,7 @@ Section proofs.
wp_alloc l as "Hl".
wp_apply mk_mailbox_works ; first done. iIntros (v) "#Hmailbox".
iMod (inv_alloc Nstack _ (stack_inv P l) with "[Hl HP]") as "#Hinv".
{ by iNext; iExists _, []; iFrame. }
{ by iNext; iExists None, []; iFrame. }
wp_pures. iModIntro; iApply "HΦ"; iExists _; auto.
Qed.
......@@ -348,18 +352,19 @@ Section proofs.
iModIntro.
wp_let. wp_alloc l' as "Hl'". wp_pures. wp_bind (CAS _ _ _).
iInv Nstack as (list' xs) "(Hl & Hlist & HP)" "Hclose".
iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
destruct (decide (list = list')) as [ -> |].
* wp_cas_suc.
* wp_cas_suc. { destruct list'; left; done. }
iMod (fupd_intro_mask' ( Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
iMod ("Hupd" with "HP") as "[HP HΨ]".
iMod "Hupd'" as "_".
iMod ("Hclose" with "[Hl Hl' HP Hlist]") as "_".
{ iNext; iExists (SOMEV _), (v' :: xs); iFrame; iExists _, _; iFrame; auto. }
{ iNext; iExists (Some _), (v' :: xs); iFrame; iExists _; iFrame; auto. }
iModIntro.
wp_if.
by iApply ("HΦ" with "HΨ").
* wp_cas_fail.
{ destruct list, list'; simpl; congruence. }
{ destruct list'; left; done. }
iMod ("Hclose" with "[Hl HP Hlist]").
{ iExists _, _; iFrame. }
iModIntro.
......@@ -399,8 +404,8 @@ Section proofs.
- wp_match. wp_bind (Load _).
iInv Nstack as (v xs) "(Hl & Hlist & HP)" "Hclose".
wp_load.
iDestruct (is_list_disj with "Hlist") as "[Hlist H]".
iDestruct "H" as "[-> | HSome]".
iDestruct (is_list_dup with "Hlist") as "[Hlist H]".
destruct v as [l'|]; last first.
* iDestruct (is_list_empty with "Hlist") as %->.
iMod (fupd_intro_mask' ( Nstack) inner_mask) as "Hupd'"; first solve_ndisj.
iMod ("Hupd" with "HP") as "[HP HΨ]".
......@@ -410,7 +415,7 @@ Section proofs.
iModIntro.
wp_match.
iApply ("HΦ" with "HΨ").
* iDestruct "HSome" as (l' h t) "[-> Hl']".
* iDestruct "H" as (h t) "Hl'".
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
......@@ -423,7 +428,7 @@ Section proofs.
iModIntro.
wp_pures. wp_bind (CAS _ _ _).
iInv Nstack as (v' xs'') "(Hl & Hlist & HP)" "Hclose".
destruct (decide (v' = (SOMEV #l'))) as [ -> |].
destruct (decide (v' = (Some l'))) as [ -> |].
+ wp_cas_suc.
iDestruct (is_list_cons with "[Hl'] Hlist") as (ys) "%"; first by iExists _.
simplify_eq.
......@@ -431,7 +436,7 @@ Section proofs.
iDestruct "Hupd" as "[Hupdcons _]".
iMod ("Hupdcons" with "HP") as "[HP HΨ]".
iMod "Hupd'" as "_".
iDestruct "Hlist" as (l'' t') "(% & Hl'' & Hlist)"; simplify_eq.
iDestruct "Hlist" as (t') "(Hl'' & Hlist)".
iDestruct "Hl''" as (q') "Hl''".
iDestruct (mapsto_agree with "Hl' Hl''") as "%"; simplify_eq.
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
......@@ -439,7 +444,7 @@ Section proofs.
iModIntro.
wp_pures.
iApply ("HΦ" with "HΨ").
+ wp_cas_fail.
+ wp_cas_fail. { destruct v'; simpl; congruence. }
iMod ("Hclose" with "[Hlist Hl HP]") as "_".
{ iNext; iExists _, _; iFrame. }
iModIntro.
......
......@@ -49,49 +49,51 @@ Section proof.
Lemma rown_duplicate l v : rown l v - rown l v rown l v.
Proof. iDestruct 1 as (q) "[Hl Hl']". iSplitL "Hl"; iExists _; eauto. Qed.
Fixpoint is_list (hd : val) (xs : list val) : iProp Σ :=
match xs with
| [] => hd = NONEV%I
| x::xs => ( (l : loc) (tl : val),
hd = SOMEV #l rown l (x, tl) is_list tl xs)%I
Definition oloc_to_val (ol: option loc) : val :=
match ol with
| None => NONEV