Commit 66e89b20 by Dan Frumin

### Stack with helping example

parent 74269607
 ... @@ -33,6 +33,8 @@ theories/examples/stack/stack_rules.v ... @@ -33,6 +33,8 @@ theories/examples/stack/stack_rules.v theories/examples/stack/CG_stack.v theories/examples/stack/CG_stack.v theories/examples/stack/FG_stack.v theories/examples/stack/FG_stack.v theories/examples/stack/refinement.v theories/examples/stack/refinement.v theories/examples/stack/mailbox.v theories/examples/stack/helping.v theories/tests/typetest.v theories/tests/typetest.v theories/tests/tactics.v theories/tests/tactics.v theories/tests/tactics2.v theories/tests/tactics2.v
 (* 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 (InjR (Pair h t))). Notation Nile := (Fold (InjL #())). 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.
 From iris.proofmode Require Import tactics. From iris.algebra Require Import excl. From iris_logrel Require Export logrel. Notation MAYBE τ := (TSum TUnit τ) (only parsing). Notation NONE := (InjL #()) (only parsing). Notation SOME x := (InjR x) (only parsing). Notation NONEV := (InjLV #()) (only parsing). Notation SOMEV x := (InjRV x) (only parsing). Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" := (Match e0 BAnon e1 x%bind e2) (e0, e1, x, e2 at level 200, only parsing) : expr_scope. Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" := (Match e0 BAnon e1 x%bind e2) (e0, e1, x, e2 at level 200, only parsing) : expr_scope. Definition mk_offer : val := λ: "v", ("v", ref #0). Definition revoke_offer : val := λ: "v", if: CAS (Snd "v") #0 #2 then SOME (Fst "v") else NONE. Definition take_offer : val := λ: "v", if: CAS (Snd "v") #0 #1 then SOME (Fst "v") else NONE. Definition put_mail : val := λ: "r" "v", let: "off" := mk_offer "v" in "r" <- SOME "off";; revoke_offer "off". Definition get_mail : val := λ: "r", match: !"r" with NONE => NONE | SOME "x" => take_offer "x" end. Definition new_mb : val := λ: <>, ref NONE. Definition mailbox : val := PackV (new_mb, put_mail, get_mail). Section typing. Variable τ : type. Definition offerτ := TProd τ (Tref TNat). Definition mbτ := Tref (MAYBE offerτ). Lemma new_mb_typed Γ : Γ ⊢ₜ new_mb : TArrow TUnit mbτ. Proof. solve_typed. Qed. Hint Resolve new_mb_typed : typeable. Lemma get_mail_typed Γ : Γ ⊢ₜ get_mail : TArrow mbτ (MAYBE τ). Proof. unlock get_mail. unlock take_offer. solve_typed. Qed. Hint Resolve get_mail_typed : typeable. Lemma put_mail_typed Γ : Γ ⊢ₜ put_mail : TArrow mbτ (TArrow τ (MAYBE τ)). Proof. unlock put_mail. unlock revoke_offer mk_offer. solve_typed. Qed. Hint Resolve put_mail_typed : typeable. Lemma mailbox_typed Γ : Γ ⊢ₜ mailbox : TExists (TProd (TProd (TArrow TUnit (TVar 0)) (TArrow (TVar 0) (TArrow τ.[ren (+1)] (MAYBE τ.[ren (+1)])))) (TArrow (TVar 0) (MAYBE τ.[ren (+1)]))). Proof. unlock mailbox; simpl. econstructor. econstructor; [ econstructor | ]; asimpl; eauto with typeable. Qed. End typing. Definition channelR := exclR unitR. Class channelG Σ := { channel_inG :> inG Σ channelR }. Definition channelΣ : gFunctors := #[GFunctor channelR]. Instance subG_channelΣ {Σ} : subG channelΣ Σ → channelG Σ. Proof. solve_inG. Qed. Section side_channel. Context `{!heapG Σ, !channelG Σ}. Implicit Types l : loc. Definition stages γ (P : val → iProp Σ) l v := ((l ↦ᵢ #0 ∗ P v) ∨ (l ↦ᵢ #1) ∨ (l ↦ᵢ #2 ∗ own γ (Excl ())))%I. Definition is_offer γ (P : val → iProp Σ) (v : val) : iProp Σ := (∃ v' l, ⌜v = (v', # l)%V⌝ ∗ ∃ ι, inv ι (stages γ P l v'))%I. (* A partial specification for revoke that will be useful later *) Lemma revoke_works γ P v : is_offer γ P v ∗ own γ (Excl ()) -∗ WP revoke_offer v {{ v', (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ P v'') ∨ ⌜v' = InjLV #()⌝ }}. Proof. iIntros "[#Hinv Hγ]". rewrite /is_offer. iDestruct "Hinv" as (v' l) "[% Hinv]"; simplify_eq. iDestruct "Hinv" as (N) "#Hinv". unlock revoke_offer. wp_let. wp_proj. wp_bind (CAS _ _ _). iInv N as "Hstages" "Hclose". iDestruct "Hstages" as "[H | [H | H]]". - iDestruct "H" as "[Hl HP]". wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]"). iRight; iRight; iFrame. iModIntro. wp_if. wp_proj. wp_value. iLeft. iExists v'; iSplit; auto. - wp_cas_fail. iMod ("Hclose" with "[H]"). iRight; iLeft; auto. iModIntro. wp_if. wp_value. iRight; auto. - iDestruct "H" as "[Hl H]". wp_cas_fail. by iDestruct (own_valid_2 with "H Hγ") as %?. Qed. (* A partial specification for take that will be useful later *) Lemma take_works γ N P v l : inv N (stages γ P l v) -∗ WP take_offer (v, LitV l)%V {{ v', (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ P v'') ∨ ⌜v' = InjLV #()⌝ }}. Proof. iIntros "#Hinv". unlock take_offer. wp_rec. wp_proj. wp_bind (CAS _ _ _). iInv N as "Hstages" "Hclose". iDestruct "Hstages" as "[H | [H | H]]". - iDestruct "H" as "[H HP]". wp_cas_suc. iMod ("Hclose" with "[H]"). iRight; iLeft; done. iModIntro. wp_if. wp_proj. wp_value. iLeft. auto. - wp_cas_fail. iMod ("Hclose" with "[H]"). iRight; iLeft; done. iModIntro. wp_if. wp_value; auto. - iDestruct "H" as "[Hl Hγ]". wp_cas_fail. iMod ("Hclose" with "[Hl Hγ]"). iRight; iRight; iFrame. iModIntro. wp_if. wp_value; auto. Qed. Lemma mk_offer_works P (v : val) : P v -∗ WP mk_offer v {{ v', ∃ γ, own γ (Excl ()) ∗ is_offer γ P v' }}. Proof. iIntros "HP". unlock mk_offer. wp_rec. wp_alloc l as "Hl". iApply wp_fupd. wp_value. pose proof (nroot .@ "N'") as N'. iMod (own_alloc (Excl ())) as (γ) "Hγ". done. iMod (inv_alloc N' _ (stages γ P l v) with "[HP Hl]") as "#Hinv'". { iNext. rewrite /stages. iLeft. iFrame. } iModIntro. iExists γ; iFrame. unfold is_offer. iExists _, _; iSplitR; eauto. Qed. End side_channel. Section mailbox. Context `{!heapG Σ, !channelG Σ}. Implicit Types l : loc. Definition mailbox_inv (P : val → iProp Σ) (v : val) : iProp Σ := (∃ l : loc, ⌜v = # l⌝ ∗ (l ↦ᵢ NONEV ∨ (∃ v' γ, l ↦ᵢ SOMEV v' ∗ is_offer γ P v')))%I. Theorem new_mb_works (P : val → iProp Σ) (Φ : val → iProp Σ) : (∀ v N, inv N (mailbox_inv P v) -∗ Φ v) -∗ WP new_mb #() {{ Φ }}. Proof. iIntros "HΦ". unlock new_mb. wp_rec. iApply wp_fupd. wp_alloc r as "Hr". pose proof (nroot .@ "N") as N. iMod (inv_alloc N _ (mailbox_inv P (# r)) with "[Hr]") as "#Hinv". { iExists r; iSplit; try iLeft; auto. } iModIntro. by iApply "HΦ". Qed. Theorem put_mail_works (P : val → iProp Σ) (Φ : val → iProp Σ) N (mb v : val) : inv N (mailbox_inv P mb) -∗ P v -∗ (∀ v', ((∃ v'', ⌜v' = SOMEV v''⌝ ∗ P v'') ∨ ⌜v' = NONEV⌝) -∗ Φ v') -∗ WP put_mail mb v {{ Φ }}. Proof. iIntros "#Hinv HP HΦ". unlock put_mail. wp_rec. wp_let. wp_bind (mk_offer v). iApply (wp_wand with "[HP]"). { iApply (mk_offer_works with "HP"). } iIntros (off). iDestruct 1 as (γ) "[Hγ #Hoffer]". wp_let. wp_bind (mb <- _)%E. iInv N as "Hmailbox" "Hclose". iDestruct "Hmailbox" as (l) "[>% Hl]". simplify_eq/=. iDestruct "Hl" as "[>Hl | Hl]"; [ | iDestruct "Hl" as (off' γ') "[Hl Hoff']"]; (* off' - already existing offer *) wp_store; [iMod ("Hclose" with "[Hl]") | iMod ("Hclose" with "[Hl Hoff']")]; try (iExists _; iNext; iSplit; eauto); iModIntro; wp_let; iApply (wp_wand with "[Hγ Hoffer] HΦ"); iApply (revoke_works with "[\$]"). Qed. Theorem get_mail_works (P : val → iProp Σ) (Φ : val → iProp Σ) N (mb : val) : inv N (mailbox_inv P mb) -∗ (∀ v', ((∃ v'', ⌜v' = SOMEV v''⌝ ∗ P v'') ∨ ⌜v' = NONEV⌝) -∗ Φ v') -∗ WP get_mail mb {{ Φ }}. Proof. iIntros "#Hinv HΦ". unlock get_mail. wp_rec. wp_bind (! _)%E. iInv N as "Hmailbox" "Hclose". iDestruct "Hmailbox" as (l') "[>% H]"; simplify_eq/=. iDestruct "H" as "[H | H]". + wp_load. iMod ("Hclose" with "[H]"). iExists l'; iSplit; auto. iModIntro. wp_case_inl. wp_seq. wp_value. iApply "HΦ"; auto. + iDestruct "H" as (v' γ) "[Hl' #Hoffer]". wp_load. iMod ("Hclose" with "[Hl' Hoffer]"). { iExists l'; iSplit; auto. iRight; iExists v', γ; by iSplit. } iModIntro. simpl. wp_case_inr. (* TODO: [simpl] is require here *) wp_let. iDestruct "Hoffer" as (v'' l'') "[% Hoffer]"; simplify_eq. iDestruct "Hoffer" as (ι) "Hinv'". iApply (wp_wand with "[] HΦ"). iApply take_works; auto. Qed. End mailbox.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!