module_refinement.v 6.66 KB
 Dan Frumin committed Sep 12, 2017 1 2 3 4 5 6 ``````From iris.proofmode Require Import tactics. From iris_logrel Require Import logrel. From iris_logrel.examples.stack Require Import CG_stack FG_stack stack_rules refinement. Section Mod_refinement. `````` Dan Frumin committed Sep 13, 2017 7 `````` Context `{HLR : logrelG Σ}. `````` Dan Frumin committed Sep 12, 2017 8 9 10 11 `````` Notation D := (prodC valC valC -n> iProp Σ). Implicit Types Δ : listC D. Import lang. `````` Dan Frumin committed Sep 13, 2017 12 13 14 15 `````` Program Definition sint {LG : logrelG Σ} {Z : stackPreG Σ} τi : prodC valC valC -n> iProp Σ := λne vv, (∃ γ (l stk stk' : loc), ⌜(vv.2) = (#stk', #l)%V⌝ ∗ ⌜(vv.1) = #stk⌝ ∗ inv (stackN .@ (stk,stk')) (sinv' γ τi stk stk' l))%I. Solve Obligations with solve_proper. `````` Dan Frumin committed Sep 12, 2017 16 `````` `````` Dan Frumin committed Sep 13, 2017 17 `````` Instance sint_persistent `{logrelG Σ, stackPreG Σ} τi vv : PersistentP (sint τi vv). `````` Dan Frumin committed Sep 12, 2017 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 `````` Proof. apply _. Qed. Lemma interp_subst_up_2 Δ1 Δ2 τ τi : ⟦ τ ⟧ (Δ1 ++ Δ2) ≡ ⟦ τ.[upn (length Δ1) (ren (+1))] ⟧ (Δ1 ++ τi :: Δ2). Proof. revert Δ1 Δ2. induction τ => Δ1 Δ2; simpl; eauto. - intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2. - intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2. - unfold interp_expr. intros vv; simpl; properness; eauto. by apply IHτ1. by apply IHτ2. - apply fixpoint_proper=> τ' ww /=. properness; auto. apply (IHτ (_ :: _)). - intros vv; simpl. rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl; properness. { by rewrite !lookup_app_l. } rewrite !lookup_app_r; [|lia ..]. assert ((length Δ1 + S (x - length Δ1) - length Δ1) = S (x - length Δ1)) as Hwat. { lia. } rewrite Hwat. simpl. done. - unfold interp_expr. intros vv; simpl; properness; auto. apply (IHτ (_ :: _)). - intros vv; simpl; properness; auto. apply (IHτ (_ :: _)). - intros vv; simpl; properness; auto. by apply IHτ. Qed. Lemma interp_subst_2 τ τi Δ : ⟦ τ ⟧ Δ ≡ ⟦ τ.[ren (+1)] ⟧ (τi :: Δ). Proof. by apply (interp_subst_up_2 []). Qed. Lemma bin_log_weaken_2 τi Δ Γ e1 e2 τ : {⊤,⊤;Δ;Γ} ⊨ e1 ≤log≤ e2 : τ -∗ {⊤,⊤;τi::Δ;Autosubst_Classes.subst (ren (+1)) <\$>Γ} ⊨ e1 ≤log≤ e2 : τ.[ren (+1)]. Proof. rewrite bin_log_related_eq /bin_log_related_def. iIntros "Hlog" (vvs ρ) "#Hs #HΓ". iSpecialize ("Hlog" \$! vvs with "Hs [HΓ]"). { by rewrite interp_env_ren. } unfold interp_expr. iIntros (j K) "Hj /=". iMod ("Hlog" with "Hj") as "Hlog". iApply (wp_mono with "Hlog"). iIntros (v). simpl. iDestruct 1 as (v') "[Hj Hτ]". iExists v'. iFrame. by rewrite -interp_subst_2. Qed. `````` Dan Frumin committed Sep 13, 2017 63 `````` Lemma module_refinement `{SPG : stackPreG Σ} Δ Γ : `````` Dan Frumin committed Sep 12, 2017 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 `````` {⊤,⊤;Δ;Γ} ⊨ FG_stack.stackmod ≤log≤ CG_stack.stackmod : TForall \$ TExists \$ TProd (TProd (TArrow TUnit (TVar 0)) (TArrow (TVar 0) (TSum TUnit (TVar 1)))) (TArrow (TVar 0) (TArrow (TVar 1) TUnit)). Proof. unlock FG_stack.stackmod CG_stack.stackmod. iApply bin_log_related_tlam; auto. iIntros (τi Hτi) "!#". iApply (bin_log_related_pack _ (sint τi)). do 3 rel_tlam_l. do 3 rel_tlam_r. repeat iApply bin_log_related_pair. - iApply bin_log_related_arrow; eauto. iAlways. iIntros (? ?) "_". rel_seq_l. rel_seq_r. rel_alloc_l as istk "Histk". simpl. rel_alloc_l as stk "Hstk". `````` Dan Frumin committed Sep 13, 2017 82 `````` rel_alloc_r as stk' "Hstk'". `````` Dan Frumin committed Sep 12, 2017 83 84 `````` rel_alloc_r as l "Hl". rel_vals. `````` Dan Frumin committed Sep 13, 2017 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 `````` rewrite -persistentP. iMod (own_alloc (● (∅ : stackUR))) as (γ) "Hemp"; first done. pose (SG := StackG Σ _ γ). iAssert (prestack_owns γ ∅) with "[Hemp]" as "Hoe". { 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 (LitV Unit)))) with "[Histk]" as "#HLK". { rewrite preStackLink_unfold. iExists _, _. iSplitR; simpl; trivial. iFrame "Histk". iLeft. iSplit; trivial. } iAssert (sinv' γ τi stk stk' l) with "[Hoe Hstk Hstk' HLK Hl]" as "Hinv". { iExists _, _, _. by iFrame. } iMod (inv_alloc (stackN.@(stk,stk')) with "[Hinv]") as "#Hinv". { iNext. iExact "Hinv". } iModIntro. iExists γ, l, stk, stk'. eauto. `````` Dan Frumin committed Sep 12, 2017 102 103 `````` - iApply bin_log_related_arrow_val; eauto. iAlways. iIntros (? ?) "#Hvv /=". `````` Dan Frumin committed Sep 13, 2017 104 `````` iDestruct "Hvv" as (γ l stk stk') "(% & % & #Hinv)". `````` Dan Frumin committed Sep 12, 2017 105 106 107 108 109 110 111 112 113 114 115 116 117 118 `````` simplify_eq/=. rel_let_l. rel_let_r. Transparent FG_pop CG_locked_pop. rel_rec_l. rel_proj_r; rel_rec_r. unlock CG_locked_pop. simpl_subst/=. rel_proj_r. rel_let_r. replace (#();; acquire # l ;; let: "v" := (CG_pop #stk') #() in release # l ;; "v")%E with ((CG_locked_pop \$/ LitV (Loc stk') \$/ LitV (Loc l)) #())%E; last first. { unlock CG_locked_pop. simpl_subst/=. reflexivity. } replace (TSum TUnit (TVar 1)) with (TSum TUnit (TVar 0)).[ren (+1)] by done. iApply bin_log_weaken_2. `````` Dan Frumin committed Sep 13, 2017 119 120 121 122 123 `````` pose (SG := StackG Σ _ γ). change γ with stack_name. iApply (FG_CG_pop_refinement' (stackN.@(stk,stk'))). { solve_ndisj. } by rewrite sinv_unfold. `````` Dan Frumin committed Sep 12, 2017 124 125 126 `````` - iApply bin_log_related_arrow_val; eauto. { unlock FG_push. done. } iAlways. iIntros (? ?) "#Hvv /=". `````` Dan Frumin committed Sep 13, 2017 127 `````` iDestruct "Hvv" as (γ l stk stk') "(% & % & #Hinv)". `````` Dan Frumin committed Sep 12, 2017 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 `````` simplify_eq/=. rel_let_r. Transparent FG_push. rel_rec_l. iApply bin_log_related_arrow_val; eauto. { unlock FG_push. simpl_subst/=. done. } { unlock FG_push. simpl_subst/=. solve_closed. } iAlways. iIntros (v v') "#Hτi /=". rel_let_r. rel_proj_r; rel_rec_r. unlock CG_locked_push. simpl_subst/=. rel_proj_r; rel_let_r. replace (let: "x" := v' in acquire # l ;; (CG_push #stk') "x" ;; release # l)%E with ((CG_locked_push \$/ LitV stk' \$/ LitV l) v')%E; last first. { unlock CG_locked_push. simpl_subst/=. done. } change TUnit with (TUnit.[ren (+1)]). `````` Dan Frumin committed Sep 13, 2017 144 145 146 147 148 149 `````` pose (SG := StackG Σ _ γ). change γ with stack_name. iApply (FG_CG_push_refinement (stackN.@(stk,stk')) with "[Hinv] Hτi"). { solve_ndisj. } by rewrite sinv_unfold. Qed. `````` Dan Frumin committed Sep 12, 2017 150 ``````End Mod_refinement. `````` Dan Frumin committed Sep 13, 2017 151 152 153 154 155 156 157 158 159 160 161 162 `````` Theorem module_ctx_refinement : ∅ ⊨ FG_stack.stackmod ≤ctx≤ CG_stack.stackmod : TForall \$ TExists \$ TProd (TProd (TArrow TUnit (TVar 0)) (TArrow (TVar 0) (TSum TUnit (TVar 1)))) (TArrow (TVar 0) (TArrow (TVar 1) TUnit)). Proof. set (Σ := #[logrelΣ; GFunctor (authR stackUR)]). eapply (logrel_ctxequiv Σ); [solve_closed.. | intros ]. apply module_refinement. Qed.``````