(* Stack with helping *) From iris.proofmode Require Import tactics. From iris_logrel Require Export logrel examples.stack.mailbox. Definition LIST τ := TRec (TSum TUnit (TProd τ.[ren (+1)] (TVar 0))). Notation Conse h t := (Fold (SOME (Pair h t))). Notation Nile := (Fold NONE). Definition pop_st : val := λ: "r" "get", rec: "pop" <> := match: "get" #() with NONE => (match: Unfold !"r" with NONE => NONE | SOME "hd" => if: CAS "r" (Fold (SOME "hd")) (Snd "hd") then SOME (Fst "hd") else "pop" #() end) | SOME "x" => SOME "x" end. Definition push_st : val := λ: "r" "put", rec: "push" "n" := match: "put" "n" with NONE => #() | SOME "n" => let: "r'" := !"r" in let: "r''" := Fold (SOME ("n", "r'")) in if: CAS "r" "r'" "r''" then #() else "push" "n" end. Definition mk_stack : val := λ: "_", Unpack mailbox \$ λ: "M", let: "new_mb" := Fst (Fst "M") in let: "put" := Snd (Fst "M") in let: "get" := Snd "M" in let: "mb" := "new_mb" #() in let: "r" := ref (Fold NONE) in (pop_st "r" (λ: <>, "get" "mb"), push_st "r" (λ: "n", "put" "mb" "n")). Section stack_works. Context `{!heapG Σ}. Implicit Types l : loc. Definition is_stack_pre (P : val → iProp Σ) (F : val -c> iProp Σ) : val -c> iProp Σ := λ v, (v ≡ FoldV NONEV ∨ ∃ (h t : val), v ≡ FoldV (SOMEV (h, t))%V ∗ P h ∗ ▷ F t)%I. Local Instance is_stack_contr (P : val → iProp Σ): Contractive (is_stack_pre P). Proof. rewrite /is_stack_pre => n f f' Hf v. repeat (f_contractive || f_equiv). apply Hf. Qed. Definition is_stack_def (P : val -> iProp Σ) := fixpoint (is_stack_pre P). Definition is_stack_aux P : seal (@is_stack_def P). by eexists. Qed. Definition is_stack P := unseal (is_stack_aux P). Definition is_stack_eq P : @is_stack P = @is_stack_def P := seal_eq (is_stack_aux P). Definition stack_inv P v := (∃ l v', ⌜v = # l⌝ ∗ l ↦ᵢ v' ∗ is_stack P v')%I. Lemma is_stack_unfold (P : val → iProp Σ) v : is_stack P v ⊣⊢ is_stack_pre P (is_stack P) v. Proof. rewrite is_stack_eq. apply (fixpoint_unfold (is_stack_pre P)). Qed. Lemma is_stack_disj (P : val → iProp Σ) v : is_stack P v -∗ is_stack P v ∗ (v ≡ FoldV NONEV ∨ ∃ (h t : val), v ≡ FoldV (SOMEV (h, t))%V). Proof. iIntros "Hstack". iDestruct (is_stack_unfold with "Hstack") as "[#Hstack|Hstack]". - iSplit; try iApply is_stack_unfold; iLeft; auto. - iDestruct "Hstack" as (h t) "[#Heq rest]". iSplitL; try iApply is_stack_unfold; iRight; auto. Qed. Theorem stack_works {channelG0 : channelG Σ} P Φ : (∀ (f₁ f₂ : val), (□ WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ P v') ∨ v ≡ NONEV }}) -∗ (∀ (v : val), □ (P v -∗ WP f₂ v {{ v, True }})) -∗ Φ (f₁, f₂)%V)%I -∗ WP mk_stack #() {{ Φ }}. Proof. iIntros "HΦ". unlock mk_stack. wp_rec. wp_pack. wp_let. repeat wp_proj; wp_let. repeat wp_proj; wp_let. repeat wp_proj; wp_let. wp_bind (new_mb _). iApply (new_mb_works P). iIntros (mb Nmb) "#Hinv". wp_let. wp_alloc r as "Hr". wp_let. pose proof (nroot .@ "N") as N. iMod (inv_alloc N _ (stack_inv P #r) with "[Hr]") as "#Hisstack". { iExists r, (FoldV NONEV); iFrame; iSplit; auto. iApply is_stack_unfold; iLeft; done. } unlock pop_st. do 2 wp_rec. unlock push_st. do 2 wp_rec. iApply wp_value. (* TODO: solve_to_val. either doesn't work or too slow *) { simpl. rewrite ?decide_left. simpl. done. } iApply "HΦ". (* The verification of pop *) - iIntros "!#". iLöb as "IH". wp_rec. wp_rec. wp_bind (get_mail _). iApply (get_mail_works P with "Hinv"). iIntros (v) "Hv". iDestruct "Hv" as "[H | H]". + iDestruct "H" as (v') "[% HP]". subst. simpl. wp_case_inr. (* TODO: we require a simpl here *) wp_let. wp_value. iLeft; iExists v'; auto. + iDestruct "H" as "%"; subst. wp_case. wp_seq. wp_bind (! #r)%E. iInv N as "Hstack" "Hclose". iDestruct "Hstack" as (l'' v'') "[>% [Hl' Hstack]]". simplify_eq/=. wp_load. iDestruct (is_stack_disj with "Hstack") as "[Hstack #Heq]". iMod ("Hclose" with "[Hl' Hstack]"). { iExists l'', v''; iFrame; auto. } iModIntro. iDestruct "Heq" as "[H | H]". * iRewrite "H". wp_unfold. wp_case. wp_seq. wp_value. iRight; auto. * iDestruct "H" as (h t) "H"; iRewrite "H". simpl. wp_unfold. simpl. wp_case_inr. (* TODO: same comment *) wp_let. wp_proj. wp_bind (CAS _ _ _). iInv N as "Hstack" "Hclose". iDestruct "Hstack" as (l''' v''') "[>% [Hl'' Hstack]]". simplify_eq/=. destruct (decide (v''' = FoldV (InjRV (h, t))%V)) as [Heq | Heq]; subst. ++ (* If nothing has changed, the cas succeeds *) wp_cas_suc. iDestruct (is_stack_unfold with "Hstack") as "[Hstack | Hstack]". { iDestruct "Hstack" as "%"; discriminate. } iDestruct "Hstack" as (h' t') "[% [HP Hstack]]". simplify_eq/=. iMod ("Hclose" with "[Hl'' Hstack]"). { iExists l''', t'; iFrame; auto. } iModIntro. wp_if. wp_proj. wp_value. iLeft; auto. ++ (* The case in which we fail *) wp_cas_fail. iMod ("Hclose" with "[Hl'' Hstack]"). iExists l''', v'''; iFrame; auto. iModIntro. wp_if. (* Now we use our IH to loop *) iApply "IH". (* The verification of push. This is actually markedly simpler. *) - iIntros (v) "!# HP /=". (* We grab an IH to be used in the case that we loop *) iLöb as "IH" forall (v). wp_rec. wp_rec. wp_bind (put_mail _ _). iApply (put_mail_works P with "Hinv HP"). iIntros (v') "Hv'". iDestruct "Hv'" as "[H | H]". * iDestruct "H" as (v'') "[% HP]"; subst. simpl. wp_case. (* TODO: same comment here *) wp_let. wp_bind (! _)%E. iInv N as "Hstack" "Hclose". iDestruct "Hstack" as (l'' v') "[>% [Hl' Hstack]]". simplify_eq/=. wp_load. iMod ("Hclose" with "[Hl' Hstack]"). { by (iExists l'', v'; iFrame). } iModIntro. do 2 wp_let. wp_bind (CAS _ _ _). iInv N as "Hstack" "Hclose". iDestruct "Hstack" as (l''' v''') "[>% [Hl'' Hstack]]". simplify_eq/=. destruct (decide (v''' = v'%V)) as [Heq|Heq]; subst. + wp_cas_suc. iMod ("Hclose" with "[Hl'' HP Hstack]"). { iExists l''', (FoldV (InjRV (v'', v')%V)). iSplit; iFrame; auto. iApply is_stack_unfold; iRight. iExists v'', v'; iFrame. eauto. } iModIntro. wp_if. by wp_value. + wp_cas_fail. iMod ("Hclose" with "[Hl'' Hstack]"). iExists l''', v'''; iFrame; auto. iModIntro. wp_if. iApply ("IH" with "HP"). * (* This is the case that our sidechannel offer succeeded *) iDestruct "H" as "%"; subst. wp_case. wp_seq. by wp_value. Qed. End stack_works.