From 73b0c36ce262697594577c02b97744e7d03302ce Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Mon, 30 May 2016 21:25:56 +0200 Subject: [PATCH] Prove context refinement for stacks --- F_mu_ref_par/examples/counter.v | 5 ++++- F_mu_ref_par/examples/stack/refinement.v | 27 +++++++++++++++++++++--- F_mu_ref_par/soundness_binary.v | 22 ++++++++++--------- 3 files changed, 40 insertions(+), 14 deletions(-) diff --git a/F_mu_ref_par/examples/counter.v b/F_mu_ref_par/examples/counter.v index 59b50f6..db4cbca 100644 --- a/F_mu_ref_par/examples/counter.v +++ b/F_mu_ref_par/examples/counter.v @@ -392,11 +392,14 @@ Section CG_Counter. End CG_Counter. +Definition Σ := #[auth.authGF heapR; auth.authGF cfgR]. + Theorem counter_context_refinement : context_refines [] FG_counter CG_counter (TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)). Proof. - eapply Binary_Soundness; + eapply (@Binary_Soundness Σ); auto using FG_counter_closed, CG_counter_closed, FG_CG_counter_refinement. + all: typeclasses eauto. Qed. \ No newline at end of file diff --git a/F_mu_ref_par/examples/stack/refinement.v b/F_mu_ref_par/examples/stack/refinement.v index dea7c73..df33359 100644 --- a/F_mu_ref_par/examples/stack/refinement.v +++ b/F_mu_ref_par/examples/stack/refinement.v @@ -2,13 +2,13 @@ From iris.proofmode Require Import invariants ghost_ownership tactics. From iris.program_logic Require Import auth namespaces. From iris_logrel.F_mu_ref_par Require Import lang examples.lock examples.stack.CG_stack examples.stack.FG_stack examples.stack.stack_rules - typing logrel_binary fundamental_binary rules_binary rules. + typing logrel_binary fundamental_binary rules_binary rules +context_refinement soundness_binary. Import uPred. Section Stack_refinement. Context {Σ : gFunctors} {iS : cfgSG Σ} {iI : heapIG Σ} {iSTK : authG lang Σ stackR}. - Ltac prove_disj N n n' := let Hneq := fresh "Hneq" in let Hdsj := fresh "Hdsj" in @@ -518,4 +518,25 @@ Section Stack_refinement. end. Qed. -End Stack_refinement. \ No newline at end of file +End Stack_refinement. + +Definition Σ := #[authGF heapR; authGF cfgR; authGF stackR]. + +Theorem stack_context_refinement : + context_refines + [] FG_stack CG_stack + (TForall + (TProd + (TProd + (TArrow (TVar 0) TUnit) + (TArrow TUnit (TSum TUnit (TVar 0))) + ) + (TArrow (TArrow (TVar 0) TUnit) TUnit) + ) + ). +Proof. + eapply (@Binary_Soundness Σ); + eauto using FG_stack_closed, CG_stack_closed. + all: try typeclasses eauto. + intros. apply FG_CG_counter_refinement. +Qed. \ No newline at end of file diff --git a/F_mu_ref_par/soundness_binary.v b/F_mu_ref_par/soundness_binary.v index 7de706d..903a458 100644 --- a/F_mu_ref_par/soundness_binary.v +++ b/F_mu_ref_par/soundness_binary.v @@ -10,9 +10,11 @@ Require Import iris.program_logic.adequacy. Import uPred. Section Soundness. - Definition binlogΣ := #[auth.authGF heapR; auth.authGF cfgR]. + Context {Σ : gFunctors} + {Hhp : auth.authG lang Σ heapR} + {Hcfg : auth.authG lang Σ cfgR}. - Definition free_type_context : varC -n> bivalC -n> iPropG lang binlogΣ := + Definition free_type_context : varC -n> bivalC -n> iPropG lang Σ := {| cofe_mor_car := λ x, {| cofe_mor_car := λ y, (True)%I |} |}. Local Notation Δφ := free_type_context. @@ -23,8 +25,8 @@ Section Soundness. Proof. intros x v; apply const_persistent. Qed. Lemma wp_basic_soundness e e' τ : - (∀ Σ H H' N Δ HΔ , @bin_log_related Σ H H' N Δ [] e e' τ HΔ) → - (@ownership.ownP lang (globalF binlogΣ) ∅) + (∀ H H' N Δ HΔ , @bin_log_related Σ H H' N Δ [] e e' τ HΔ) → + (@ownership.ownP lang (globalF Σ) ∅) ⊢ WP e {{_, ■ (∃ thp' h v, rtc step ([e'], ∅) ((# v) :: thp', h))}}. Proof. @@ -43,13 +45,13 @@ Section Soundness. } iDestruct "Hcfg" as {γ} "Hcfg". rewrite own_op. iDestruct "Hcfg" as "[Hcfg1 Hcfg2]". - iAssert (@auth.auth_inv _ binlogΣ _ _ _ γ (Spec_inv (to_cfg ([e'], ∅)))) + iAssert (@auth.auth_inv _ Σ _ _ _ γ (Spec_inv (to_cfg ([e'], ∅)))) as "Hinv" with "[Hcfg1]". { iExists _; iFrame "Hcfg1". apply const_intro; constructor. } iPvs (inv_alloc (nroot .@ "Fμ,ref,par" .@ 3) with "[Hinv]") as "#Hcfg"; trivial. { iNext. iExact "Hinv". } - iPoseProof (H1 binlogΣ H (@CFGSG _ _ γ) _ Δφ _ [] _ _ 0 [] + iPoseProof (H1 H (@CFGSG _ _ γ) _ Δφ _ [] _ _ 0 [] with "[Hcfg2]") as "HBR". { unfold Spec_ctx, auth.auth_ctx, tpool_mapsto, auth.auth_own. simpl. rewrite empty_env_subst. by iFrame "Hheap Hcfg Hcfg2". } @@ -61,7 +63,7 @@ Section Soundness. iDestruct "Hp" as %Hp. unfold tpool_mapsto, auth.auth_own; simpl. iCombine "Hj" "Hown" as "Hown". - iDestruct (@own_valid _ binlogΣ (authR cfgR) _ γ _ with "Hown !") + iDestruct (@own_valid _ Σ (authR cfgR) _ γ _ with "Hown !") as "#Hvalid". iDestruct (auth_validI _ with "Hvalid") as "[Ha' #Hb]"; simpl; iClear "Hvalid". @@ -84,7 +86,7 @@ Section Soundness. Qed. Lemma basic_soundness e e' τ : - (∀ Σ H H' N Δ HΔ , @bin_log_related Σ H H' N Δ [] e e' τ HΔ) → + (∀ H H' N Δ HΔ , @bin_log_related Σ H H' N Δ [] e e' τ HΔ) → ∀ v thp hp, rtc step ([e], ∅) ((# v) :: thp, hp) → (∃ thp' hp' v', rtc step ([e'], ∅) ((# v') :: thp', hp')). @@ -103,12 +105,12 @@ Section Soundness. Lemma Binary_Soundness Γ e e' τ : (∀ f, e.[iter (List.length Γ) up f] = e) → (∀ f, e'.[iter (List.length Γ) up f] = e') → - (∀ Σ H H' N Δ HΔ , @bin_log_related Σ H H' N Δ Γ e e' τ HΔ) → + (∀ H H' N Δ HΔ , @bin_log_related Σ H H' N Δ Γ e e' τ HΔ) → context_refines Γ e e' τ. Proof. intros H1 K HK htp hp v Hstp Hc Hc'. eapply basic_soundness; eauto. - intros Σ H H' N Δ HΔ. + intros H H' N Δ HΔ. eapply (bin_log_related_under_typed_context _ _ _ _ []); eauto. Qed. -- GitLab