Commit 627ec511 by Dan Frumin

Remove the persistence requirements from the forall interpretation

parent 9357c013
 ... ... @@ -196,8 +196,8 @@ Section cell_refinement. Definition lockR (R : D) (r1 r2 r3 r : loc) : iProp Σ := (∃ (a b c : val), r ↦ₛ a ∗ r2 ↦ᵢ b ∗ r3 ↦ᵢ c ∗ ( (r1 ↦ᵢ #true ∗ R (c, a)) ∨ (r1 ↦ᵢ #false ∗ R (b, a))))%I. ( (r1 ↦ᵢ #true ∗ □ R (c, a)) ∨ (r1 ↦ᵢ #false ∗ □ R (b, a))))%I. Definition cellInt (R : D) (r1 r2 r3 l r : loc) : iProp Σ := (∃ γ N, is_lock N γ #l (lockR R r1 r2 r3 r))%I. ... ... @@ -216,7 +216,7 @@ Section cell_refinement. iIntros (Δ). unlock cell2 cell1 cellτ. iApply bin_log_related_tlam; auto. iIntros (R HR) "!#". iIntros (R) "!#". iApply (bin_log_related_pack (cellR R)). repeat iApply bin_log_related_pair. - (* New cell *) ... ... @@ -250,7 +250,7 @@ Section cell_refinement. iDestruct "Hr1" as "[[Hr1 #Ha] | [Hr1 #Ha]]"; rel_load_l; rel_if_l; repeat rel_proj_l; rel_load_l; rel_let_l. + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto. { iExists _,_,_; iFrame. iLeft; by iFrame. } { iExists a,b,c; iFrame. iLeft; by iFrame. } rel_let_l. rel_vals; eauto. + rel_apply_l (bin_log_related_release_l with "Hlk Htok [-]"); auto. { iExists _,_,_; iFrame. iRight; by iFrame. } ... ...
 ... ... @@ -25,7 +25,7 @@ Section Mod_refinement. Proof. unlock FG_stack.stackmod CG_stack.stackmod. iApply bin_log_related_tlam; auto. iIntros (τi Hτi) "!#". iIntros (τi) "!#". iApply (bin_log_related_pack (sint τi)). do 3 rel_tlam_l. do 3 rel_tlam_r. ... ... @@ -46,7 +46,7 @@ Section Mod_refinement. { rewrite /prestack_owns big_sepM_empty fmap_empty. iFrame "Hemp". } iMod (stack_owns_alloc with "[\$Hoe \$Histk]") as "[Hoe #Histk]". iAssert (preStackLink γ τi (#istk, FoldV (InjLV #()))) with "[Histk]" as "#HLK". iAssert (preStackLink γ (R τi) (#istk, FoldV (InjLV #()))) with "[Histk]" as "#HLK". { rewrite preStackLink_unfold. iExists _, _. iSplitR; simpl; trivial. iFrame "Histk". iLeft. iSplit; trivial. } ... ...
 ... ... @@ -11,11 +11,14 @@ Section Stack_refinement. Implicit Types Δ : listC D. Import lang. Program Definition R (τi : prodC valC valC -> iProp Σ) := λne ww, (□ τi ww)%I. Next Obligation. solve_proper. Qed. Definition sinv' {SPG : authG Σ stackUR} γ τi stk stk' l' : iProp Σ := (∃ (istk : loc) v h, (prestack_owns γ h) ∗ stk' ↦ₛ v ∗ stk ↦ᵢ (FoldV #istk) ∗ preStackLink γ τi (#istk, v) ∗ preStackLink γ (R τi) (#istk, v) ∗ l' ↦ₛ #false)%I. Context `{stackG Σ}. ... ... @@ -23,7 +26,7 @@ Section Stack_refinement. (∃ (istk : loc) v h, (stack_owns h) ∗ stk' ↦ₛ v ∗ stk ↦ᵢ (FoldV #istk) ∗ StackLink τi (#istk, v) ∗ StackLink (R τi) (#istk, v) ∗ l ↦ₛ #false)%I. Lemma sinv_unfold τi stk stk' l : sinv τi stk stk' l = sinv' stack_name τi stk stk' l. ... ... @@ -33,9 +36,9 @@ Section Stack_refinement. iMod (Hcl with asn) as "_"; [iNext; rewrite /sinv; iExists _,_,_; by iFrame |]; try iModIntro. Lemma FG_CG_push_refinement N st st' (τi : D) (v v' : val) l {τP : ∀ ww, Persistent (τi ww)} Γ : Lemma FG_CG_push_refinement N st st' (τi : D) (v v' : val) l Γ : N ## logrelN → inv N (sinv τi st st' l) -∗ τi (v,v') -∗ inv N (sinv τi st st' l) -∗ (R τi) (v,v') -∗ Γ ⊨ (FG_push \$/ (LitV (Loc st))) v ≤log≤ (CG_locked_push \$/ (LitV (Loc st')) \$/ (LitV (Loc l))) v' : TUnit. Proof. iIntros (?) "#Hinv #Hvv'". iIntros (Δ). ... ... @@ -80,7 +83,7 @@ Section Stack_refinement. by iApply "IH". Qed. Lemma FG_CG_pop_refinement' N st st' (τi : D) l {τP : ∀ ww, Persistent (τi ww)} Δ Γ : Lemma FG_CG_pop_refinement' N st st' (τi : D) l Δ Γ : N ## logrelN → inv N (sinv τi st st' l) -∗ {τi::Δ;Γ} ⊨ (FG_pop \$/ LitV (Loc st)) #() ≤log≤ (CG_locked_pop \$/ LitV (Loc st') \$/ LitV (Loc l)) #() : TSum TUnit (TVar 0). ... ... @@ -179,7 +182,7 @@ replace ((rec: "pop" "st" <> := iApply "IH". Qed. Lemma FG_CG_pop_refinement st st' (τi : D) l {τP : ∀ ww, Persistent (τi ww)} Δ Γ : Lemma FG_CG_pop_refinement st st' (τi : D) l Δ Γ : inv stackN (sinv τi st st' l) -∗ {τi::Δ;Γ} ⊨ FG_pop \$/ LitV (Loc st) ≤log≤ CG_locked_pop \$/ LitV (Loc st') \$/ LitV (Loc l) : TArrow TUnit (TSum TUnit (TVar 0)). Proof. ... ... @@ -194,7 +197,7 @@ replace ((rec: "pop" "st" <> := { solve_ndisj. } Qed. Lemma FG_CG_iter_refinement st st' (τi : D) l Δ {τP : ∀ ww, Persistent (τi ww)} Γ: Lemma FG_CG_iter_refinement st st' (τi : D) l Δ Γ: inv stackN (sinv τi st st' l) -∗ {τi::Δ;Γ} ⊨ FG_read_iter \$/ LitV (Loc st) ≤log≤ CG_snap_iter \$/ LitV (Loc st') \$/ LitV (Loc l) : TArrow (TArrow (TVar 0) TUnit) TUnit. Proof. ... ... @@ -319,7 +322,7 @@ Section Full_refinement. Proof. unfold FG_stack. unfold CG_stack. iApply bin_log_related_tlam; auto. iIntros (τi) "% !#". iIntros (τi) "!#". rel_alloc_r as l "Hl". rel_rec_r. rel_alloc_r as st' "Hst'". ... ... @@ -332,7 +335,6 @@ Section Full_refinement. rel_alloc_l as st "Hst". simpl. rel_rec_l. iMod (own_alloc (● (∅ : stackUR))) as (γ) "Hemp"; first done. set (istkG := StackG _ _ γ). change γ with (@stack_name _ istkG). ... ... @@ -342,7 +344,7 @@ Section Full_refinement. { rewrite /stack_owns /prestack_owns big_sepM_empty fmap_empty. iFrame "Hemp". } iMod (stack_owns_alloc with "[\$Hoe \$Histk]") as "[Hoe #Histk]". iAssert (StackLink τi (#istk, FoldV (InjLV Unit))) with "[Histk]" as "#HLK". iAssert (StackLink (R τi) (#istk, FoldV (InjLV Unit))) with "[Histk]" as "#HLK". { rewrite StackLink_unfold. iExists _, _. iSplitR; simpl; trivial. iFrame "Histk". iLeft. iSplit; trivial. } ... ...
 ... ... @@ -130,7 +130,7 @@ Section bin_log_related_under_typed_ctx. with (dom (gset string) (subst (ren (+1)) <\$> Γ')); last first. { unfold_leibniz. by rewrite !dom_fmap. } eapply typed_ctx_closed; eauto. iIntros (τi) "%". iAlways. iIntros (τi). iAlways. iApply (IHK with "[Hrel]"); auto. + iApply (bin_log_related_tapp' with "[]"); try fundamental. iApply (IHK with "[Hrel]"); auto. ... ...
 ... ... @@ -330,11 +330,12 @@ Section fundamental. Lemma bin_log_related_tlam Δ Γ e e' τ : Closed (dom _ Γ) e → Closed (dom _ Γ) e' → (∀ (τi : D), ⌜∀ ww, Persistent (τi ww)⌝ → □ ({(τi::Δ);⤉Γ} ⊨ e ≤log≤ e' : τ)) -∗ (∀ (τi : D), □ ({(τi::Δ);⤉Γ} ⊨ e ≤log≤ e' : τ)) -∗ {Δ;Γ} ⊨ TLam e ≤log≤ TLam e' : TForall τ. Proof. rewrite bin_log_related_eq. iIntros (??) "#IH". iIntros (? ?) "#IH". iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=". iDestruct (interp_env_dom with "HΓ") as %Hdom. assert (Closed ∅ (env_subst (fst <\$> vvs) e)). ... ... @@ -344,11 +345,12 @@ Section fundamental. iModIntro. iApply wp_value. iExists (TLamV (env_subst (snd <\$> vvs) e')). cbn. iFrame "Hj". iAlways. iIntros (τi ? j' K') "Hv /=". iIntros (τi). iIntros (j' K') "Hv /=". (* iIntros (τi ? j' K') "Hv /=". *) iModIntro. wp_tlam. iApply fupd_wp. tp_tlam j'; eauto. iSpecialize ("IH" \$! τi with "[] Hs [HΓ]"); auto. iSpecialize ("IH" \$! τi with "Hs [HΓ]"); auto. { by rewrite interp_env_ren. } iApply ("IH" with "Hv"). Qed. ... ... @@ -359,7 +361,7 @@ Section fundamental. Proof. iIntros "IH". rel_bind_ap e e' "IH" v v' "IH". iSpecialize ("IH" \$! (interp ⊤ τ' Δ) with "[#]"); [iPureIntro; apply _|]. iSpecialize ("IH" \$! (interp ⊤ τ' Δ)). iApply (related_ret ⊤). iApply (interp_expr_subst Δ τ τ' (TApp v, TApp v') with "IH"). Qed. ... ... @@ -379,10 +381,7 @@ Section fundamental. iMod "IH" as "IH /=". iModIntro. iApply (wp_wand with "IH"). iIntros (v). iDestruct 1 as (v') "[Hj #IH]". iSpecialize ("IH" \$! τi with "[]"); auto. unfold interp_expr. iMod ("IH" with "Hj") as "IH /=". done. iMod ("IH" \$! τi with "Hj"); auto. Qed. Lemma bin_log_related_fold Δ Γ e e' τ : ... ...
 ... ... @@ -77,7 +77,8 @@ Section semtypes. Program Definition interp_forall (E : coPset) (interp : listC D -n> D) : listC D -n> D := λne Δ ww, (□ ∀ τi, ⌜∀ ww, Persistent (τi ww)⌝ → (* □ (∀ ww, (τi ww -∗ □ (τi ww))) → *) (* ⌜∀ ww, Persistent (τi ww)⌝ → *) interp_expr E interp (τi :: Δ) (TApp (of_val (ww.1)), TApp (of_val (ww.2))))%I. Solve Obligations with solve_proper. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment