From iris.program_logic Require Export weakestpre. From iris.heap_lang Require Export lang. From iris.heap_lang Require Import proofmode notation. From iris.algebra Require Import frac auth gmap csum. From iris_atomic Require Import atomic misc. Definition new_stack: val := λ: <>, ref (ref NONE). Definition push: val := rec: "push" "s" "x" := let: "hd" := !"s" in let: "s'" := ref SOME ("x", "hd") in if: CAS "s" "hd" "s'" then #() else "push" "s" "x". Definition pop: val := rec: "pop" "s" := let: "hd" := !"s" in match: !"hd" with SOME "cell" => if: CAS "s" "hd" (Snd "cell") then SOME (Fst "cell") else "pop" "s" | NONE => NONE end. Definition iter: val := rec: "iter" "hd" "f" := match: !"hd" with NONE => #() | SOME "cell" => "f" (Fst "cell") ;; "iter" (Snd "cell") "f" end. Section proof. Context `{!heapG Σ} (N: namespace). Fixpoint is_list (hd: loc) (xs: list val) : iProp Σ := match xs with | [] => (∃ q, hd ↦{ q } NONEV)%I | x :: xs => (∃ (hd': loc) q, hd ↦{ q } SOMEV (x, #hd') ∗ is_list hd' xs)%I end. Lemma dup_is_list : ∀ xs hd, is_list hd xs ⊢ is_list hd xs ∗ is_list hd xs. Proof. induction xs as [|y xs' IHxs']. - iIntros (hd) "Hs". simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto. - iIntros (hd) "Hs". simpl. iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & Hs')". iDestruct (IHxs' with "[Hs']") as "[Hs1 Hs2]"; first by iFrame. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame. Qed. Lemma uniq_is_list: ∀ xs ys hd, is_list hd xs ∗ is_list hd ys ⊢ ⌜xs = ys⌝. Proof. induction xs as [|x xs' IHxs']. - induction ys as [|y ys' IHys']. + auto. + iIntros (hd) "(Hxs & Hys)". simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')". iExFalso. iDestruct "Hxs" as (?) "Hhd'". (* FIXME: If I dont use the @ here and below through this file, it loops. *) by iDestruct (@mapsto_agree with "[\$Hhd] [\$Hhd']") as %?. - induction ys as [|y ys' IHys']. + iIntros (hd) "(Hxs & Hys)". simpl. iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)". iDestruct "Hys" as (?) "Hhd'". by iDestruct (@mapsto_agree with "[\$Hhd] [\$Hhd']") as %?. + iIntros (hd) "(Hxs & Hys)". simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')". iDestruct "Hys" as (? ?) "(Hhd' & Hys')". iDestruct (@mapsto_agree with "[\$Hhd] [\$Hhd']") as %[= Heq]. subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame. by subst. Qed. Definition is_stack (s: loc) xs: iProp Σ := (∃ hd: loc, s ↦ #hd ∗ is_list hd xs)%I. Global Instance is_list_timeless xs hd: Timeless (is_list hd xs). Proof. generalize hd. induction xs; apply _. Qed. Global Instance is_stack_timeless xs hd: Timeless (is_stack hd xs). Proof. generalize hd. induction xs; apply _. Qed. Lemma new_stack_spec: ∀ (Φ: val → iProp Σ), (∀ s, is_stack s [] -∗ Φ #s) ⊢ WP new_stack #() {{ Φ }}. Proof. iIntros (Φ) "HΦ". wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl". wp_alloc l' as "Hl'". iApply "HΦ". rewrite /is_stack. iExists l. iFrame. by iExists 1%Qp. Qed. Definition push_triple (s: loc) (x: val) := atomic_triple (fun xs_hd: list val * loc => let '(xs, hd) := xs_hd in s ↦ #hd ∗ is_list hd xs)%I (fun xs_hd ret => let '(xs, hd) := xs_hd in ∃ hd': loc, ⌜ret = #()⌝ ∗ s ↦ #hd' ∗ hd' ↦ SOMEV (x, #hd) ∗ is_list hd xs)%I ∅ ⊤ (push #s x). Lemma push_atomic_spec (s: loc) (x: val) : push_triple s x. Proof. rewrite /push_triple /atomic_triple. iIntros (P Q) "#Hvs". iLöb as "IH". iIntros "!# HP". wp_rec. wp_let. wp_bind (! _)%E. iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]". wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame. iModIntro. wp_let. wp_alloc l as "Hl". wp_let. wp_bind (CAS _ _ _)%E. iMod ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']". destruct (decide (hd = hd')) as [->|Hneq]. * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']". iMod ("Hvs'" \$! #() with "[-]") as "HQ". { iExists l. iSplitR; first done. by iFrame. } iModIntro. wp_if. eauto. * wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]". iMod ("Hvs'" with "[-]") as "HP"; first by iFrame. iModIntro. wp_if. by iApply "IH". Qed. Definition pop_triple (s: loc) := atomic_triple (fun xs_hd: list val * loc => let '(xs, hd) := xs_hd in s ↦ #hd ∗ is_list hd xs)%I (fun xs_hd ret => let '(xs, hd) := xs_hd in (⌜ret = NONEV⌝ ∗ ⌜xs = []⌝ ∗ s ↦ #hd ∗ is_list hd []) ∨ (∃ x q (hd': loc) xs', hd ↦{q} SOMEV (x, #hd') ∗ ⌜ret = SOMEV x⌝ ∗ ⌜xs = x :: xs'⌝ ∗ s ↦ #hd' ∗ is_list hd' xs'))%I ∅ ⊤ (pop #s). Lemma pop_atomic_spec (s: loc): pop_triple s. Proof. rewrite /pop_triple /atomic_triple. iIntros (P Q) "#Hvs". iLöb as "IH". iIntros "!# HP". wp_rec. wp_bind (! _)%E. iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] Hvs']". destruct xs as [|y' xs']. - simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']". iDestruct "Hhd" as (q) "[Hhd Hhd']". iMod ("Hvs'" \$! NONEV with "[-Hhd]") as "HQ". { iLeft. iSplit=>//. iSplit=>//. iFrame. eauto. } iModIntro. wp_let. wp_load. wp_match. eauto. - simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')". iDestruct (dup_is_list with "[Hxs']") as "[Hxs1 Hxs2]"; first by iFrame. wp_load. iDestruct "Hvs'" as "[Hvs' _]". iMod ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "HP". { iFrame. iExists hd', (q / 2)%Qp. by iFrame. } iModIntro. wp_let. wp_load. wp_match. wp_proj. wp_bind (CAS _ _ _). iMod ("Hvs" with "HP") as ([xs hd'']) "[[Hs Hhd''] Hvs']". destruct (decide (hd = hd'')) as [->|Hneq]. + wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']". iMod ("Hvs'" \$! (SOMEV y') with "[-]") as "HQ". { iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'. destruct xs as [|x' xs'']. - simpl. iDestruct "Hhd''" as (?) "H". iExFalso. by iDestruct (@mapsto_agree with "[\$Hhd1] [\$H]") as %?. - simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')". iDestruct (@mapsto_agree with "[\$Hhd1] [\$Hhd'']") as %[=]. subst. iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst. repeat (iSplitR "Hxs1 Hs"; first done). iFrame. } iModIntro. wp_if. wp_proj. eauto. + wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]". iMod ("Hvs'" with "[-]") as "HP"; first by iFrame. iModIntro. wp_if. by iApply "IH". Qed. End proof.