module_refinement.v 3.99 KB
 Dan Frumin committed Sep 12, 2017 1 2 3 ``````From iris.proofmode Require Import tactics. From iris_logrel Require Import logrel. From iris_logrel.examples.stack Require Import `````` Dan Frumin committed May 02, 2018 4 `````` CG_stack FG_stack refinement. `````` Dan Frumin committed Sep 12, 2017 5 6 `````` 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 May 02, 2018 12 13 14 `````` Program Definition sint τ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. `````` Dan Frumin committed Sep 13, 2017 15 `````` Solve Obligations with solve_proper. `````` Dan Frumin committed Sep 12, 2017 16 `````` `````` Dan Frumin committed May 02, 2018 17 `````` Instance sint_persistent τi vv : Persistent (sint τi vv). `````` Dan Frumin committed Sep 12, 2017 18 `````` Proof. apply _. Qed. `````` Dan Frumin committed May 02, 2018 19 20 `````` Lemma module_refinement Δ Γ : `````` 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 Jan 31, 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 May 02, 2018 43 44 45 `````` iAssert (sinv τi stk stk' l) with "[-]" as "Hinv". { iExists _,_. iFrame. rewrite stack_link_unfold. iExists _; iSplitL; eauto. } `````` Dan Frumin committed Sep 13, 2017 46 47 48 `````` iMod (inv_alloc (stackN.@(stk,stk')) with "[Hinv]") as "#Hinv". { iNext. iExact "Hinv". } iModIntro. `````` Dan Frumin committed May 02, 2018 49 `````` iExists l, stk, stk'. eauto. `````` Dan Frumin committed Sep 12, 2017 50 51 `````` - iApply bin_log_related_arrow_val; eauto. iAlways. iIntros (? ?) "#Hvv /=". `````` Dan Frumin committed May 02, 2018 52 `````` iDestruct "Hvv" as (l stk stk') "(% & % & #Hinv)". `````` Dan Frumin committed Sep 12, 2017 53 54 55 56 57 58 59 60 61 62 63 64 65 `````` 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 66 `````` iApply bin_log_related_weaken_2. `````` Dan Frumin committed May 02, 2018 67 68 `````` iApply (FG_CG_pop_refinement' (stackN.@(stk,stk')) with "Hinv"). solve_ndisj. `````` Dan Frumin committed Sep 12, 2017 69 70 71 `````` - iApply bin_log_related_arrow_val; eauto. { unlock FG_push. done. } iAlways. iIntros (? ?) "#Hvv /=". `````` Dan Frumin committed May 02, 2018 72 `````` iDestruct "Hvv" as (l stk stk') "(% & % & #Hinv)". `````` Dan Frumin committed Sep 12, 2017 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 `````` 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 May 02, 2018 89 90 `````` iApply (FG_CG_push_refinement (stackN.@(stk,stk')) with "Hinv Hτi"). solve_ndisj. `````` Dan Frumin committed Sep 13, 2017 91 `````` Qed. `````` Dan Frumin committed Sep 12, 2017 92 ``````End Mod_refinement. `````` Dan Frumin committed Sep 13, 2017 93 94 95 96 97 98 99 100 `````` 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. `````` Dan Frumin committed May 02, 2018 101 `````` eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ]. `````` Dan Frumin committed Sep 13, 2017 102 103 `````` apply module_refinement. Qed.``````