module_refinement.v 5 KB
 Dan Frumin committed Sep 12, 2017 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 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 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 ``````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. Context `{logrelG Σ, stackG Σ}. Notation D := (prodC valC valC -n> iProp Σ). Implicit Types Δ : listC D. Import lang. Program Definition sint `{logrelG Σ, stackG Σ} τi : prodC valC valC -n> iProp Σ := λne vv, (∃ (l stk stk' : loc), ⌜(vv.2) = (# stk', # l)%V⌝ ∗ ⌜(vv.1) = #stk⌝ ∗ inv stackN (sinv τi stk stk' l))%I. Next Obligation. solve_proper. Qed. Instance sint_persistent τi vv : PersistentP (sint τi vv). 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. Lemma module_refinmenet Δ Γ : {⊤,⊤;Δ;Γ} ⊨ 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". rel_alloc_r as stl' "Hstk'". rel_alloc_r as l "Hl". rel_vals. admit. - iApply bin_log_related_arrow_val; eauto. iAlways. iIntros (? ?) "#Hvv /=". iDestruct "Hvv" as (l stk stk') "(% & % & #Hinv)". 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. by iApply FG_CG_pop_refinement'. - iApply bin_log_related_arrow_val; eauto. { unlock FG_push. done. } iAlways. iIntros (? ?) "#Hvv /=". iDestruct "Hvv" as (l stk stk') "(% & % & #Hinv)". 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)]). iApply (FG_CG_push_refinement with "Hinv Hτi"). Admitted. End Mod_refinement.``````