module_refinement.v 4.85 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 Nov 27, 2017 17 `````` Instance sint_persistent `{logrelG Σ, stackPreG Σ} τi vv : Persistent (sint τi vv). `````` Dan Frumin committed Sep 12, 2017 18 19 `````` Proof. apply _. Qed. `````` Dan Frumin committed Sep 13, 2017 20 `````` Lemma module_refinement `{SPG : stackPreG Σ} Δ Γ : `````` Dan Frumin committed Jan 28, 2018 21 `````` {Δ;Γ} ⊨ FG_stack.stackmod ≤log≤ CG_stack.stackmod : TForall \$ TExists \$ TProd (TProd `````` Dan Frumin committed Sep 12, 2017 22 23 24 25 26 27 `````` (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. `````` Dan Frumin committed Feb 01, 2018 28 `````` iIntros (τi) "!#". `````` Dan Frumin committed Jan 28, 2018 29 `````` iApply (bin_log_related_pack (sint τi)). `````` Dan Frumin committed Sep 12, 2017 30 31 32 33 34 35 36 37 38 `````` 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 39 `````` rel_alloc_r as stk' "Hstk'". `````` Dan Frumin committed Sep 12, 2017 40 41 `````` rel_alloc_r as l "Hl". rel_vals. `````` Dan Frumin committed Nov 27, 2017 42 `````` rewrite -persistent. `````` Dan Frumin committed Sep 13, 2017 43 44 45 46 47 48 `````` 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]". `````` Dan Frumin committed Feb 01, 2018 49 `````` iAssert (preStackLink γ (R τi) (#istk, FoldV (InjLV #()))) with "[Histk]" as "#HLK". `````` Dan Frumin committed Sep 13, 2017 50 51 52 53 54 55 56 57 58 `````` { 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 59 60 `````` - iApply bin_log_related_arrow_val; eauto. iAlways. iIntros (? ?) "#Hvv /=". `````` Dan Frumin committed Sep 13, 2017 61 `````` iDestruct "Hvv" as (γ l stk stk') "(% & % & #Hinv)". `````` Dan Frumin committed Sep 12, 2017 62 63 64 65 66 67 68 69 70 71 72 73 74 `````` 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. `````` Dan Frumin committed Sep 13, 2017 75 `````` iApply bin_log_related_weaken_2. `````` Dan Frumin committed Sep 13, 2017 76 77 78 79 80 `````` 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 81 82 83 `````` - iApply bin_log_related_arrow_val; eauto. { unlock FG_push. done. } iAlways. iIntros (? ?) "#Hvv /=". `````` Dan Frumin committed Sep 13, 2017 84 `````` iDestruct "Hvv" as (γ l stk stk') "(% & % & #Hinv)". `````` Dan Frumin committed Sep 12, 2017 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 `````` 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 101 102 103 104 105 106 `````` 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 107 ``````End Mod_refinement. `````` Dan Frumin committed Sep 13, 2017 108 109 110 111 112 113 114 115 116 117 118 119 `````` 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.``````