From b1515733f2da24b526c5086348037978fa3fa73f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 16 Nov 2016 19:20:25 +0100 Subject: [PATCH] Add binary logical relations for F_mu_ref --- F_mu_ref/context_refinement.v | 245 ++++++++++++++++++++++++++ F_mu_ref/fundamental_binary.v | 314 ++++++++++++++++++++++++++++++++++ F_mu_ref/lang.v | 4 +- F_mu_ref/logrel_binary.v | 227 ++++++++++++++++++++++++ F_mu_ref/rules_binary.v | 185 ++++++++++++++++++++ F_mu_ref/soundness_binary.v | 50 ++++++ F_mu_ref/typing.v | 106 +++++++++++- F_mu_ref_conc/lang.v | 2 +- README.md | 2 +- _CoqProject | 5 + 10 files changed, 1130 insertions(+), 10 deletions(-) create mode 100644 F_mu_ref/context_refinement.v create mode 100644 F_mu_ref/fundamental_binary.v create mode 100644 F_mu_ref/logrel_binary.v create mode 100644 F_mu_ref/rules_binary.v create mode 100644 F_mu_ref/soundness_binary.v diff --git a/F_mu_ref/context_refinement.v b/F_mu_ref/context_refinement.v new file mode 100644 index 0000000..71029d3 --- /dev/null +++ b/F_mu_ref/context_refinement.v @@ -0,0 +1,245 @@ +From iris_logrel.F_mu_ref Require Export fundamental_binary. + +Inductive ctx_item := + | CTX_Lam + | CTX_AppL (e2 : expr) + | CTX_AppR (e1 : expr) + (* Products *) + | CTX_PairL (e2 : expr) + | CTX_PairR (e1 : expr) + | CTX_Fst + | CTX_Snd + (* Sums *) + | CTX_InjL + | CTX_InjR + | CTX_CaseL (e1 : expr) (e2 : expr) + | CTX_CaseM (e0 : expr) (e2 : expr) + | CTX_CaseR (e0 : expr) (e1 : expr) + (* Recursive Types *) + | CTX_Fold + | CTX_Unfold + (* Polymorphic Types *) + | CTX_TLam + | CTX_TApp + (* Reference Types *) + | CTX_Alloc + | CTX_Load + | CTX_StoreL (e2 : expr) + | CTX_StoreR (e1 : expr). + +Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr := + match ctx with + | CTX_Lam => Lam e + | CTX_AppL e2 => App e e2 + | CTX_AppR e1 => App e1 e + | CTX_PairL e2 => Pair e e2 + | CTX_PairR e1 => Pair e1 e + | CTX_Fst => Fst e + | CTX_Snd => Snd e + | CTX_InjL => InjL e + | CTX_InjR => InjR e + | CTX_CaseL e1 e2 => Case e e1 e2 + | CTX_CaseM e0 e2 => Case e0 e e2 + | CTX_CaseR e0 e1 => Case e0 e1 e + | CTX_Fold => Fold e + | CTX_Unfold => Unfold e + | CTX_TLam => TLam e + | CTX_TApp => TApp e + | CTX_Alloc => Alloc e + | CTX_Load => Load e + | CTX_StoreL e2 => Store e e2 + | CTX_StoreR e1 => Store e1 e + end. + +Definition ctx := list ctx_item. + +Definition fill_ctx (K : ctx) (e : expr) : expr := foldr fill_ctx_item e K. + +(** typed ctx *) +Inductive typed_ctx_item : + ctx_item → list type → type → list type → type → Prop := + | TP_CTX_Lam Γ τ τ' : + typed_ctx_item CTX_Lam (τ :: Γ) τ' Γ (TArrow τ τ') + | TP_CTX_AppL Γ e2 τ τ' : + typed Γ e2 τ → + typed_ctx_item (CTX_AppL e2) Γ (TArrow τ τ') Γ τ' + | TP_CTX_AppR Γ e1 τ τ' : + typed Γ e1 (TArrow τ τ') → + typed_ctx_item (CTX_AppR e1) Γ τ Γ τ' + | TP_CTX_PairL Γ e2 τ τ' : + typed Γ e2 τ' → + typed_ctx_item (CTX_PairL e2) Γ τ Γ (TProd τ τ') + | TP_CTX_PairR Γ e1 τ τ' : + typed Γ e1 τ → + typed_ctx_item (CTX_PairR e1) Γ τ' Γ (TProd τ τ') + | TP_CTX_Fst Γ τ τ' : + typed_ctx_item CTX_Fst Γ (TProd τ τ') Γ τ + | TP_CTX_Snd Γ τ τ' : + typed_ctx_item CTX_Snd Γ (TProd τ τ') Γ τ' + | TP_CTX_InjL Γ τ τ' : + typed_ctx_item CTX_InjL Γ τ Γ (TSum τ τ') + | TP_CTX_InjR Γ τ τ' : + typed_ctx_item CTX_InjR Γ τ' Γ (TSum τ τ') + | TP_CTX_CaseL Γ e1 e2 τ1 τ2 τ' : + typed (τ1 :: Γ) e1 τ' → typed (τ2 :: Γ) e2 τ' → + typed_ctx_item (CTX_CaseL e1 e2) Γ (TSum τ1 τ2) Γ τ' + | TP_CTX_CaseM Γ e0 e2 τ1 τ2 τ' : + typed Γ e0 (TSum τ1 τ2) → typed (τ2 :: Γ) e2 τ' → + typed_ctx_item (CTX_CaseM e0 e2) (τ1 :: Γ) τ' Γ τ' + | TP_CTX_CaseR Γ e0 e1 τ1 τ2 τ' : + typed Γ e0 (TSum τ1 τ2) → typed (τ1 :: Γ) e1 τ' → + typed_ctx_item (CTX_CaseR e0 e1) (τ2 :: Γ) τ' Γ τ' + | TP_CTX_Fold Γ τ : + typed_ctx_item CTX_Fold Γ τ.[(TRec τ)/] Γ (TRec τ) + | TP_CTX_Unfold Γ τ : + typed_ctx_item CTX_Unfold Γ (TRec τ) Γ τ.[(TRec τ)/] + | TP_CTX_TLam Γ τ : + typed_ctx_item CTX_TLam (subst (ren (+1)) <$> Γ) τ Γ (TForall τ) + | TP_CTX_TApp Γ τ τ' : + typed_ctx_item CTX_TApp Γ (TForall τ) Γ τ.[τ'/] + | TPCTX_Alloc Γ τ : + typed_ctx_item CTX_Alloc Γ τ Γ (Tref τ) + | TP_CTX_Load Γ τ : + typed_ctx_item CTX_Load Γ (Tref τ) Γ τ + | TP_CTX_StoreL Γ e2 τ : + typed Γ e2 τ → typed_ctx_item (CTX_StoreL e2) Γ (Tref τ) Γ TUnit + | TP_CTX_StoreR Γ e1 τ : + typed Γ e1 (Tref τ) → + typed_ctx_item (CTX_StoreR e1) Γ τ Γ TUnit. + +Lemma typed_ctx_item_typed k Γ τ Γ' τ' e : + typed Γ e τ → typed_ctx_item k Γ τ Γ' τ' → + typed Γ' (fill_ctx_item k e) τ'. +Proof. induction 2; simpl; eauto using typed. Qed. + +Inductive typed_ctx: ctx → list type → type → list type → type → Prop := + | TPCTX_nil Γ τ : + typed_ctx nil Γ τ Γ τ + | TPCTX_cons Γ1 τ1 Γ2 τ2 Γ3 τ3 k K : + typed_ctx_item k Γ2 τ2 Γ3 τ3 → + typed_ctx K Γ1 τ1 Γ2 τ2 → + typed_ctx (k :: K) Γ1 τ1 Γ3 τ3. + +Lemma typed_ctx_typed K Γ τ Γ' τ' e : + typed Γ e τ → typed_ctx K Γ τ Γ' τ' → typed Γ' (fill_ctx K e) τ'. +Proof. induction 2; simpl; eauto using typed_ctx_item_typed. Qed. + +Lemma typed_ctx_n_closed K Γ τ Γ' τ' e : + (∀ f, e.[upn (length Γ) f] = e) → typed_ctx K Γ τ Γ' τ' → + ∀ f, (fill_ctx K e).[upn (length Γ') f] = (fill_ctx K e). +Proof. + intros H1 H2; induction H2; simpl; auto. + induction H => f; asimpl; simpl in *; + repeat match goal with H : _ |- _ => rewrite fmap_length in H end; + try f_equal; + eauto using typed_n_closed; + try match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end. +Qed. + +Definition ctx_refines (Γ : list type) + (e e' : expr) (τ : type) := ∀ K thp σ v, + typed_ctx K Γ τ [] TUnit → + rtc step ([fill_ctx K e], ∅) (of_val v :: thp, σ) → + ∃ thp' σ' v', rtc step ([fill_ctx K e'], ∅) (of_val v' :: thp', σ'). +Notation "Γ ⊨ e '≤ctx≤' e' : τ" := + (ctx_refines Γ e e' τ) (at level 74, e, e', τ at next level). + +Ltac fold_interp := + match goal with + | |- context [ interp_expr (interp_arrow (interp ?A) (interp ?A')) + ?B (?C, ?D) ] => + change (interp_expr (interp_arrow (interp A) (interp A')) B (C, D)) with + (interp_expr (interp (TArrow A A')) B (C, D)) + | |- context [ interp_expr (interp_prod (interp ?A) (interp ?A')) + ?B (?C, ?D) ] => + change (interp_expr (interp_prod (interp A) (interp A')) B (C, D)) with + (interp_expr (interp (TProd A A')) B (C, D)) + | |- context [ interp_expr (interp_prod (interp ?A) (interp ?A')) + ?B (?C, ?D) ] => + change (interp_expr (interp_prod (interp A) (interp A')) B (C, D)) with + (interp_expr (interp (TProd A A')) B (C, D)) + | |- context [ interp_expr (interp_sum (interp ?A) (interp ?A')) + ?B (?C, ?D) ] => + change (interp_expr (interp_sum (interp A) (interp A')) B (C, D)) with + (interp_expr (interp (TSum A A')) B (C, D)) + | |- context [ interp_expr (interp_rec (interp ?A)) ?B (?C, ?D) ] => + change (interp_expr (interp_rec (interp A)) B (C, D)) with + (interp_expr (interp (TRec A)) B (C, D)) + | |- context [ interp_expr (interp_forall (interp ?A)) + ?B (?C, ?D) ] => + change (interp_expr (interp_forall (interp A)) B (C, D)) with + (interp_expr (interp (TForall A)) B (C, D)) + | |- context [ interp_expr (interp_ref (interp ?A)) + ?B (?C, ?D) ] => + change (interp_expr (interp_ref (interp A)) B (C, D)) with + (interp_expr (interp (Tref A)) B (C, D)) + end. + +Section bin_log_related_under_typed_ctx. + Context `{heapG Σ, cfgSG Σ}. + + Lemma bin_log_related_under_typed_ctx Γ e e' τ Γ' τ' K : + (∀ f, e.[upn (length Γ) f] = e) → + (∀ f, e'.[upn (length Γ) f] = e') → + typed_ctx K Γ τ Γ' τ' → + Γ ⊨ e ≤log≤ e' : τ → Γ' ⊨ fill_ctx K e ≤log≤ fill_ctx K e' : τ'. + Proof. + revert Γ τ Γ' τ' e e'. + induction K as [|k K]=> Γ τ Γ' τ' e e' H1 H2; simpl. + - inversion_clear 1; trivial. + - inversion_clear 1 as [|? ? ? ? ? ? ? ? Hx1 Hx2]. intros H3. + specialize (IHK _ _ _ _ e e' H1 H2 Hx2 H3). + inversion Hx1; subst; simpl; try fold_interp. + + eapply bin_log_related_lam; eauto; + match goal with + H : _ |- _ => eapply (typed_ctx_n_closed _ _ _ _ _ _ _ H) + end. + + eapply bin_log_related_app; eauto using binary_fundamental. + + eapply bin_log_related_app; eauto using binary_fundamental. + + eapply bin_log_related_pair; eauto using binary_fundamental. + + eapply bin_log_related_pair; eauto using binary_fundamental. + + eapply bin_log_related_fst; eauto. + + eapply bin_log_related_snd; eauto. + + eapply bin_log_related_injl; eauto. + + eapply bin_log_related_injr; eauto. + + match goal with + H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst + end. + eapply bin_log_related_case; + eauto using binary_fundamental; + match goal with + H : _ |- _ => eapply (typed_n_closed _ _ _ H) + end. + + match goal with + H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst + end. + eapply bin_log_related_case; + eauto using binary_fundamental; + try match goal with + H : _ |- _ => eapply (typed_n_closed _ _ _ H) + end; + match goal with + H : _ |- _ => eapply (typed_ctx_n_closed _ _ _ _ _ _ _ H) + end. + + match goal with + H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst + end. + eapply bin_log_related_case; + eauto using binary_fundamental; + try match goal with + H : _ |- _ => eapply (typed_n_closed _ _ _ H) + end; + match goal with + H : _ |- _ => eapply (typed_ctx_n_closed _ _ _ _ _ _ _ H) + end. + + eapply bin_log_related_fold; eauto. + + eapply bin_log_related_unfold; eauto. + + eapply bin_log_related_tlam; eauto with typeclass_instances. + + eapply bin_log_related_tapp; eauto. + + eapply bin_log_related_alloc; eauto. + + eapply bin_log_related_load; eauto. + + eapply bin_log_related_store; eauto using binary_fundamental. + + eapply bin_log_related_store; eauto using binary_fundamental. + Unshelve. all: trivial. + Qed. +End bin_log_related_under_typed_ctx. diff --git a/F_mu_ref/fundamental_binary.v b/F_mu_ref/fundamental_binary.v new file mode 100644 index 0000000..5f237c1 --- /dev/null +++ b/F_mu_ref/fundamental_binary.v @@ -0,0 +1,314 @@ +From iris_logrel.F_mu_ref Require Export logrel_binary. +From iris.proofmode Require Import tactics. +From iris_logrel.F_mu_ref Require Import rules_binary. +From iris.base_logic Require Export big_op. + +Section bin_log_def. + Context `{cfgSG Σ}. + Notation D := (prodC valC valC -n> iProp Σ). + + Definition bin_log_related (Γ : list type) (e e' : expr) (τ : type) := ∀ Δ vvs ρ, + env_PersistentP Δ → + heap_ctx ∧ spec_ctx ρ ∧ + ⟦ Γ ⟧* Δ vvs ⊢ ⟦ τ ⟧ₑ Δ (e.[env_subst (vvs.*1)], e'.[env_subst (vvs.*2)]). +End bin_log_def. + +Notation "Γ ⊨ e '≤log≤' e' : τ" := + (bin_log_related Γ e e' τ) (at level 74, e, e', τ at next level). + +Section fundamental. + Context `{cfgSG Σ}. + Notation D := (prodC valC valC -n> iProp Σ). + Implicit Types e : expr. + Implicit Types Δ : listC D. + Hint Resolve to_of_val. + + Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) ident(w) + constr(Hv) uconstr(Hp) := + iApply (wp_bind [ctx]); + iApply wp_wand_l; iSplitR; + [|iApply Hp; rewrite ?fill_app /=; iFrame "#"; trivial]; + let Htmp := iFresh in + iIntros (v) Htmp; iDestruct Htmp as (w) Hv; + rewrite fill_app; simpl. + + Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|]. + + (* Put all quantifiers at the outer level *) + Lemma bin_log_related_alt {Γ e e' τ} : Γ ⊨ e ≤log≤ e' : τ → ∀ Δ vvs ρ K, + env_PersistentP Δ → + heap_ctx ∗ spec_ctx ρ ∗ ⟦ Γ ⟧* Δ vvs ∗ ⤇ fill K (e'.[env_subst (vvs.*2)]) + ⊢ WP e.[env_subst (vvs.*1)] {{ v, ∃ v', + ⤇ fill K (of_val v') ∗ interp τ Δ (v, v') }}. + Proof. + iIntros (Hlog Δ vvs ρ K ?) "(#Hh & #Hs & HΓ & Hj)". + iApply (Hlog with "[HΓ] *"); iFrame; eauto. + Qed. + + Notation "' H" := (bin_log_related_alt H) (at level 8). + + Lemma bin_log_related_var Γ x τ : + Γ !! x = Some τ → Γ ⊨ Var x ≤log≤ Var x : τ. + Proof. + iIntros (? Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + iDestruct (interp_env_Some_l with "HΓ") as ([v v']) "[% ?]"; first done. + rewrite /env_subst !list_lookup_fmap; simplify_option_eq. value_case; eauto. + Qed. + + Lemma bin_log_related_unit Γ : Γ ⊨ Unit ≤log≤ Unit : TUnit. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + value_case. iExists UnitV; eauto. + Qed. + + Lemma bin_log_related_pair Γ e1 e2 e1' e2' τ1 τ2 + (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : τ1) + (IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ2) : + Γ ⊨ Pair e1 e2 ≤log≤ Pair e1' e2' : TProd τ1 τ2. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + smart_wp_bind (PairLCtx e2.[env_subst _]) v v' "[Hv #Hiv]" + ('IHHtyped1 _ _ _ (K ++ [PairLCtx e2'.[env_subst _] ])). + smart_wp_bind (PairRCtx v) w w' "[Hw #Hiw]" + ('IHHtyped2 _ _ _ (K ++ [PairRCtx v'])). + value_case. iExists (PairV v' w'); iFrame "Hw". + iExists (v, v'), (w, w'); simpl; repeat iSplit; trivial. + Qed. + + Lemma bin_log_related_fst Γ e e' τ1 τ2 + (IHHtyped : Γ ⊨ e ≤log≤ e' : TProd τ1 τ2) : + Γ ⊨ Fst e ≤log≤ Fst e' : τ1. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + smart_wp_bind (FstCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ (K ++ [FstCtx])); cbn. + iDestruct "Hiv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq. + iMod (step_fst _ _ K (of_val w1') w1' (of_val w2') w2' with "* [-]") as "Hw"; eauto. + iApply wp_fst; eauto. + Qed. + + Lemma bin_log_related_snd Γ e e' τ1 τ2 + (IHHtyped : Γ ⊨ e ≤log≤ e' : TProd τ1 τ2) : + Γ ⊨ Snd e ≤log≤ Snd e' : τ2. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + smart_wp_bind (SndCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ (K ++ [SndCtx])); cbn. + iDestruct "Hiv" as ([w1 w1'] [w2 w2']) "#[% [Hw1 Hw2]]"; simplify_eq. + iMod (step_snd _ _ K (of_val w1') w1' (of_val w2') w2' with "* [-]") as "Hw"; eauto. + iApply wp_snd; eauto. + Qed. + + Lemma bin_log_related_injl Γ e e' τ1 τ2 + (IHHtyped : Γ ⊨ e ≤log≤ e' : τ1) : + Γ ⊨ InjL e ≤log≤ InjL e' : (TSum τ1 τ2). + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + smart_wp_bind (InjLCtx) v v' "[Hv #Hiv]" + ('IHHtyped _ _ _ (K ++ [InjLCtx])); cbn. + value_case. iExists (InjLV v'); iFrame "Hv". + iLeft; iExists (_,_); eauto 10. + Qed. + + Lemma bin_log_related_injr Γ e e' τ1 τ2 + (IHHtyped : Γ ⊨ e ≤log≤ e' : τ2) : + Γ ⊨ InjR e ≤log≤ InjR e' : TSum τ1 τ2. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + smart_wp_bind (InjRCtx) v v' "[Hv #Hiv]" + ('IHHtyped _ _ _ (K ++ [InjRCtx])); cbn. + value_case. iExists (InjRV v'); iFrame "Hv". + iRight; iExists (_,_); eauto 10. + Qed. + + Lemma bin_log_related_case Γ e0 e1 e2 e0' e1' e2' τ1 τ2 τ3 + (Hclosed2 : ∀ f, e1.[upn (S (length Γ)) f] = e1) + (Hclosed3 : ∀ f, e2.[upn (S (length Γ)) f] = e2) + (Hclosed2' : ∀ f, e1'.[upn (S (length Γ)) f] = e1') + (Hclosed3' : ∀ f, e2'.[upn (S (length Γ)) f] = e2') + (IHHtyped1 : Γ ⊨ e0 ≤log≤ e0' : TSum τ1 τ2) + (IHHtyped2 : τ1 :: Γ ⊨ e1 ≤log≤ e1' : τ3) + (IHHtyped3 : τ2 :: Γ ⊨ e2 ≤log≤ e2' : τ3) : + Γ ⊨ Case e0 e1 e2 ≤log≤ Case e0' e1' e2' : τ3. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + iDestruct (interp_env_length with "HΓ") as %?. + smart_wp_bind (CaseCtx _ _) v v' "[Hv #Hiv]" + ('IHHtyped1 _ _ _ (K ++ [CaseCtx _ _])); cbn. + iDestruct "Hiv" as "[Hiv|Hiv]". + - iDestruct "Hiv" as ([w w']) "[% Hw]"; simplify_eq. + iMod (step_case_inl _ _ K (of_val w') w' with "* [-]") as "Hz"; eauto. + iApply wp_case_inl; auto 1 using to_of_val. iNext. + asimpl. erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto). + iApply ('IHHtyped2 _ ((w,w') :: vvs)); repeat iSplit; eauto. + iApply interp_env_cons; auto. + - iDestruct "Hiv" as ([w w']) "[% Hw]"; simplify_eq. + iMod (step_case_inr _ _ K (of_val w') w' with "* [-]") as "Hz"; eauto. + iApply wp_case_inr; auto 1 using to_of_val. iNext. + asimpl. erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto). + iApply ('IHHtyped3 _ ((w,w') :: vvs)); repeat iSplit; eauto. + iApply interp_env_cons; auto. + Qed. + + Lemma bin_log_related_lam Γ (e e' : expr) τ1 τ2 + (Hclosed : ∀ f, e.[upn (S (length Γ)) f] = e) + (Hclosed' : ∀ f, e'.[upn (S (length Γ)) f] = e') + (IHHtyped : τ1 :: Γ ⊨ e ≤log≤ e' : τ2) : + Γ ⊨ Lam e ≤log≤ Lam e' : TArrow τ1 τ2. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + value_case. iExists (LamV _). iIntros "{$Hj} !#". + iIntros ([v v']) "#Hiv". iIntros (K') "Hj". + iDestruct (interp_env_length with "HΓ") as %?. + iApply wp_lam; auto 1 using to_of_val. iNext. + iMod (step_lam _ _ K' _ (of_val v') v' with "* [-]") as "Hz"; eauto. + asimpl. erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto). + iApply ('IHHtyped _ ((v,v') :: vvs)); repeat iSplit; eauto. + iApply interp_env_cons; iSplit; auto. + Qed. + + Lemma bin_log_related_app Γ e1 e2 e1' e2' τ1 τ2 + (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : TArrow τ1 τ2) + (IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ1) : + Γ ⊨ App e1 e2 ≤log≤ App e1' e2' : τ2. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + smart_wp_bind (AppLCtx (e2.[env_subst (vvs.*1)])) v v' "[Hv #Hiv]" + ('IHHtyped1 _ _ _ (K ++ [(AppLCtx (e2'.[env_subst (vvs.*2)]))])); cbn. + smart_wp_bind (AppRCtx v) w w' "[Hw #Hiw]" + ('IHHtyped2 _ _ _ (K ++ [AppRCtx v'])); cbn. + iApply ("Hiv" $! (w, w') with "Hiw *"); simpl; eauto. + Qed. + + Lemma bin_log_related_tlam Γ e e' τ + (IHHtyped : (subst (ren (+1)) <$> Γ) ⊨ e ≤log≤ e' : τ) : + Γ ⊨ TLam e ≤log≤ TLam e' : TForall τ. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + value_case. iExists (TLamV _). + iIntros "{$Hj} /= !#"; iIntros (τi ? K') "Hv /=". + iApply wp_tlam; iNext. + iMod (step_tlam _ _ K' (e'.[env_subst (vvs.*2)]) with "* [-]") as "Hz"; eauto. + iApply 'IHHtyped; repeat iSplit; eauto. by iApply interp_env_ren. + Qed. + + Lemma bin_log_related_tapp Γ e e' τ τ' + (IHHtyped : Γ ⊨ e ≤log≤ e' : TForall τ) : + Γ ⊨ TApp e ≤log≤ TApp e' : τ.[τ'/]. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + smart_wp_bind (TAppCtx) v v' "[Hj #Hv]" + ('IHHtyped _ _ _ (K ++ [TAppCtx])); cbn. + iApply wp_wand_r; iSplitL. + { iSpecialize ("Hv" $! (interp τ' Δ) with "[#]"); [iPureIntro; apply _|]. + iApply "Hv"; eauto. } + iIntros (w); iDestruct 1 as (w') "[Hw #Hiw]". + iExists _; rewrite -interp_subst; eauto. + Qed. + + Lemma bin_log_related_fold Γ e e' τ + (IHHtyped : Γ ⊨ e ≤log≤ e' : τ.[(TRec τ)/]) : + Γ ⊨ Fold e ≤log≤ Fold e' : TRec τ. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + iApply (wp_bind [FoldCtx]); iApply wp_wand_l; iSplitR; + [|iApply ('IHHtyped _ _ _ (K ++ [FoldCtx])); + rewrite ?fill_app; simpl; repeat iSplitR; trivial]. + iIntros (v); iDestruct 1 as (w) "[Hv #Hiv]"; rewrite fill_app. + value_case. iExists (FoldV w); iFrame "Hv". + rewrite fixpoint_unfold /= -interp_subst. + iAlways; iExists (_, _); eauto. + Qed. + + Lemma bin_log_related_unfold Γ e e' τ + (IHHtyped : Γ ⊨ e ≤log≤ e' : TRec τ) : + Γ ⊨ Unfold e ≤log≤ Unfold e' : τ.[(TRec τ)/]. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + iApply (wp_bind [UnfoldCtx]); iApply wp_wand_l; iSplitR; + [|iApply ('IHHtyped _ _ _ (K ++ [UnfoldCtx])); + rewrite ?fill_app; simpl; repeat iSplitR; trivial]. + iIntros (v). iDestruct 1 as (v') "[Hw #Hiw]"; rewrite fill_app. + rewrite /= fixpoint_unfold /=. + change (fixpoint _) with (interp (TRec τ) Δ). + iDestruct "Hiw" as ([w w']) "#[% Hiz]"; simplify_eq/=. + iMod (step_Fold _ _ K (of_val w') w' with "* [-]") as "Hz"; eauto. + iApply wp_fold; cbn; auto. + iNext; iModIntro; iExists _; iFrame "Hz". by rewrite -interp_subst. + Qed. + + Lemma bin_log_related_alloc Γ e e' τ + (IHHtyped : Γ ⊨ e ≤log≤ e' : τ) : + Γ ⊨ Alloc e ≤log≤ Alloc e' : Tref τ. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + smart_wp_bind (AllocCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ (K ++ [AllocCtx])). + iMod (step_alloc _ _ K (of_val v') v' with "* [-]") as (l') "[Hj Hl]"; eauto. + iApply wp_fupd. iApply (wp_alloc with "[]"); auto. + iIntros "!>"; iIntros (l) "Hl'". + iMod (inv_alloc (logN .@ (l,l')) _ (∃ w : val * val, + l ↦ w.1 ∗ l' ↦ₛ w.2 ∗ interp τ Δ w)%I with "[Hl Hl']") as "HN"; eauto. + { iNext; iExists (v, v'); by iFrame. } + iModIntro; iExists (LocV l'). iFrame "Hj". iExists (l, l'); eauto. + Qed. + + Lemma bin_log_related_load Γ e e' τ + (IHHtyped : Γ ⊨ e ≤log≤ e' : (Tref τ)) : + Γ ⊨ Load e ≤log≤ Load e' : τ. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + smart_wp_bind (LoadCtx) v v' "[Hv #Hiv]" ('IHHtyped _ _ _ (K ++ [LoadCtx])). + iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=. + iInv (logN .@ (l,l')) as ([w w']) "[Hw1 [Hw2 #Hw]]" "Hclose"; simpl. + iMod "Hw2". + iMod (step_load _ _ K l' 1 w' with "[Hv Hw2]") as "[Hv Hw2]"; + [solve_ndisj|by iFrame|]. + iApply (wp_load _ _ 1 with "[Hw1]"); [|iFrame "Hh"|]; trivial; try solve_ndisj. + iNext. iIntros "Hw1". iMod ("Hclose" with "[Hw1 Hw2]"). + { iNext. iExists (w,w'); by iFrame. } + iModIntro. iExists w'; by iFrame. + Qed. + + Lemma bin_log_related_store Γ e1 e2 e1' e2' τ + (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : (Tref τ)) + (IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ) : + Γ ⊨ Store e1 e2 ≤log≤ Store e1' e2' : TUnit. + Proof. + iIntros (Δ vvs ρ ?) "#(Hh & Hs & HΓ)"; iIntros (K) "Hj /=". + smart_wp_bind (StoreLCtx _) v v' "[Hv #Hiv]" + ('IHHtyped1 _ _ _ (K ++ [StoreLCtx _])). + smart_wp_bind (StoreRCtx _) w w' "[Hw #Hiw]" + ('IHHtyped2 _ _ _ (K ++ [StoreRCtx _])). + iDestruct "Hiv" as ([l l']) "[% Hinv]"; simplify_eq/=. + iInv (logN .@ (l,l')) as ([v v']) "[>Hv1 [>Hv2 #Hv]]" "Hclose". + iMod (step_store _ _ K l' v' (of_val w') w' with "[Hw Hv2]") + as "[Hw Hv2]"; [eauto|solve_ndisj|by iFrame|]. + iApply (wp_store with "[Hv1]"); auto using to_of_val. solve_ndisj. + iNext. iIntros "Hv1". iMod ("Hclose" with "[Hv1 Hv2]"). + { iNext; iExists (w, w'); by iFrame. } + iExists UnitV; iFrame; auto. + Qed. + + Theorem binary_fundamental Γ e τ : + Γ ⊢ₜ e : τ → Γ ⊨ e ≤log≤ e : τ. + Proof. + induction 1. + - by apply bin_log_related_var. + - by apply bin_log_related_unit. + - apply bin_log_related_pair; eauto. + - eapply bin_log_related_fst; eauto. + - eapply bin_log_related_snd; eauto. + - eapply bin_log_related_injl; eauto. + - eapply bin_log_related_injr; eauto. + - eapply bin_log_related_case; eauto; + match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end. + - eapply bin_log_related_lam; eauto; + match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end. + - eapply bin_log_related_app; eauto. + - eapply bin_log_related_tlam; eauto with typeclass_instances. + - eapply bin_log_related_tapp; eauto. + - eapply bin_log_related_fold; eauto. + - eapply bin_log_related_unfold; eauto. + - eapply bin_log_related_alloc; eauto. + - eapply bin_log_related_load; eauto. + - eapply bin_log_related_store; eauto. + Qed. +End fundamental. diff --git a/F_mu_ref/lang.v b/F_mu_ref/lang.v index 46ea277..d030306 100644 --- a/F_mu_ref/lang.v +++ b/F_mu_ref/lang.v @@ -124,8 +124,6 @@ Module lang. | StoreRCtx v1 => Store (of_val v1) e end. - Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K. - Definition state : Type := gmap loc val. Inductive head_step : expr → state → expr → state → list expr → Prop := @@ -247,4 +245,4 @@ Ltac solve_atomic := rewrite ?to_of_val; eapply mk_is_Some; fast_done. Hint Extern 0 (language.atomic _) => solve_atomic. -Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances. +Hint Extern 0 (language.atomic _) => solve_atomic : atomic. diff --git a/F_mu_ref/logrel_binary.v b/F_mu_ref/logrel_binary.v new file mode 100644 index 0000000..9be30f2 --- /dev/null +++ b/F_mu_ref/logrel_binary.v @@ -0,0 +1,227 @@ +From iris.proofmode Require Import tactics. +From iris.program_logic Require Export weakestpre. +From iris.base_logic Require Export big_op invariants. +From iris_logrel.F_mu_ref Require Export rules_binary typing. +From iris.algebra Require Import list. +From iris.prelude Require Import tactics. +Import uPred. + +(* HACK: move somewhere else *) +Ltac auto_equiv ::= + (* Deal with "pointwise_relation" *) + repeat lazymatch goal with + | |- pointwise_relation _ _ _ _ => intros ? + end; + (* Normalize away equalities. *) + repeat match goal with + | H : _ ≡{_}≡ _ |- _ => apply (timeless_iff _ _) in H + | _ => progress simplify_eq + end; + (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *) + try (f_equiv; fast_done || auto_equiv). + +Definition logN : namespace := nroot .@ "logN". + +(** interp : is a unary logical relation. *) +Section logrel. + Context `{heapG Σ, cfgSG Σ}. + Notation D := (prodC valC valC -n> iProp Σ). + Implicit Types τi : D. + Implicit Types Δ : listC D. + Implicit Types interp : listC D → D. + + Definition interp_expr (τi : listC D -n> D) (Δ : listC D) + (ee : expr * expr) : iProp Σ := (∀ K, + ⤇ fill K (ee.2) → + WP ee.1 {{ v, ∃ v', ⤇ fill K (of_val v') ∗ τi Δ (v, v') }})%I. + Global Instance interp_expr_ne n : + Proper (dist n ==> dist n ==> (=) ==> dist n) interp_expr. + Proof. solve_proper. Qed. + + Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ, + from_option id (cconst True)%I (Δ !! x). + Solve Obligations with solve_proper_alt. + + Program Definition interp_unit : listC D -n> D := λne Δ ww, + (ww.1 = UnitV ∧ ww.2 = UnitV)%I. + Solve Obligations with solve_proper_alt. + + Program Definition interp_prod + (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww, + (∃ vv1 vv2, ww = (PairV (vv1.1) (vv2.1), PairV (vv1.2) (vv2.2)) ∧ + interp1 Δ vv1 ∧ interp2 Δ vv2)%I. + Solve Obligations with solve_proper. + + Program Definition interp_sum + (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww, + ((∃ vv, ww = (InjLV (vv.1), InjLV (vv.2)) ∧ interp1 Δ vv) ∨ + (∃ vv, ww = (InjRV (vv.1), InjRV (vv.2)) ∧ interp2 Δ vv))%I. + Solve Obligations with solve_proper. + + Program Definition interp_arrow + (interp1 interp2 : listC D -n> D) : listC D -n> D := + λne Δ ww, + (□ ∀ vv, interp1 Δ vv → + interp_expr + interp2 Δ (App (of_val (ww.1)) (of_val (vv.1)), + App (of_val (ww.2)) (of_val (vv.2))))%I. + Solve Obligations with solve_proper. + + Program Definition interp_forall + (interp : listC D -n> D) : listC D -n> D := λne Δ ww, + (□ ∀ τi, + (■ ∀ ww, PersistentP (τi ww)) → + interp_expr + interp (τi :: Δ) (TApp (of_val (ww.1)), TApp (of_val (ww.2))))%I. + Solve Obligations with solve_proper. + + Program Definition interp_rec1 + (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne ww, + (□ ∃ vv, ww = (FoldV (vv.1), FoldV (vv.2)) ∧ ▷ interp (τi :: Δ) vv)%I. + Solve Obligations with solve_proper. + + Global Instance interp_rec1_contractive + (interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ). + Proof. + intros n τi1 τi2 Hτi ww; cbn. + apply always_ne, exist_ne; intros vv; apply and_ne; trivial. + apply later_contractive =>i Hi. by rewrite Hτi. + Qed. + + Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ, + fixpoint (interp_rec1 interp Δ). + Next Obligation. + intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi ww. solve_proper. + Qed. + + Program Definition interp_ref_inv (ll : loc * loc) : D -n> iProp Σ := λne τi, + (∃ vv, ll.1 ↦ vv.1 ∗ ll.2 ↦ₛ vv.2 ∗ τi vv)%I. + Solve Obligations with solve_proper. + + Program Definition interp_ref + (interp : listC D -n> D) : listC D -n> D := λne Δ ww, + (∃ ll, ww = (LocV (ll.1), LocV (ll.2)) ∧ + inv (logN .@ ll) (interp_ref_inv ll (interp Δ)))%I. + Solve Obligations with solve_proper. + + Fixpoint interp (τ : type) : listC D -n> D := + match τ return _ with + | TUnit => interp_unit + | TProd τ1 τ2 => interp_prod (interp τ1) (interp τ2) + | TSum τ1 τ2 => interp_sum (interp τ1) (interp τ2) + | TArrow τ1 τ2 => interp_arrow (interp τ1) (interp τ2) + | TVar x => ctx_lookup x + | TForall τ' => interp_forall (interp τ') + | TRec τ' => interp_rec (interp τ') + | Tref τ' => interp_ref (interp τ') + end. + Notation "⟦ τ ⟧" := (interp τ). + + Definition interp_env (Γ : list type) + (Δ : listC D) (vvs : list (val * val)) : iProp Σ := + (length Γ = length vvs ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vvs)%I. + Notation "⟦ Γ ⟧*" := (interp_env Γ). + + Class env_PersistentP Δ := + ctx_persistentP : Forall (λ τi, ∀ vv, PersistentP (τi vv)) Δ. + Global Instance ctx_persistent_nil : env_PersistentP []. + Proof. by constructor. Qed. + Global Instance ctx_persistent_cons τi Δ : + (∀ vv, PersistentP (τi vv)) → env_PersistentP Δ → env_PersistentP (τi :: Δ). + Proof. by constructor. Qed. + Global Instance ctx_persistent_lookup Δ x vv : + env_PersistentP Δ → PersistentP (ctx_lookup x Δ vv). + Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed. + Global Instance interp_persistent τ Δ vv : + env_PersistentP Δ → PersistentP (⟦ τ ⟧ Δ vv). + Proof. + revert vv Δ; induction τ=> vv Δ HΔ; simpl; try apply _. + rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec1 /=. + by apply always_intro'. + Qed. + Global Instance interp_env_persistent Γ Δ vvs : + env_PersistentP Δ → PersistentP (⟦ Γ ⟧* Δ vvs) := _. + + Lemma interp_weaken Δ1 Π Δ2 τ : + ⟦ τ.[upn (length Δ1) (ren (+ length Π))] ⟧ (Δ1 ++ Π ++ Δ2) + ≡ ⟦ τ ⟧ (Δ1 ++ Δ2). + Proof. + revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto. + - intros ww; simpl; properness; auto. + - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2. + - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2. + - unfold interp_expr. + intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2. + - apply fixpoint_proper=> τi ww /=. + properness; auto. apply (IHτ (_ :: _)). + - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl. + { by rewrite !lookup_app_l. } + rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done. + - unfold interp_expr. + intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)). + - intros ww; simpl; properness; auto. by apply IHτ. + Qed. + + Lemma interp_subst_up Δ1 Δ2 τ τ' : + ⟦ τ ⟧ (Δ1 ++ interp τ' Δ2 :: Δ2) + ≡ ⟦ τ.[upn (length Δ1) (τ' .: ids)] ⟧ (Δ1 ++ Δ2). + Proof. + revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl; auto. + - intros ww; simpl; properness; auto. + - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2. + - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2. + - unfold interp_expr. + intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2. + - apply fixpoint_proper=> τi ww /=. + properness; auto. apply (IHτ (_ :: _)). + - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl. + { by rewrite !lookup_app_l. } + rewrite !lookup_app_r; [|lia ..]. + destruct (x - length Δ1) as [|n] eqn:?; simpl. + { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). } + rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done. + - unfold interp_expr. + intros ww; simpl; properness; auto. apply (IHτ (_ :: _)). + - intros ww; simpl; properness; auto. by apply IHτ. + Qed. + + Lemma interp_subst Δ2 τ τ' : ⟦ τ ⟧ (⟦ τ' ⟧ Δ2 :: Δ2) ≡ ⟦ τ.[τ'/] ⟧ Δ2. + Proof. apply (interp_subst_up []). Qed. + + Lemma interp_env_length Δ Γ vvs : ⟦ Γ ⟧* Δ vvs ⊢ length Γ = length vvs. + Proof. by iIntros "[% ?]". Qed. + + Lemma interp_env_Some_l Δ Γ vvs x τ : + Γ !! x = Some τ → ⟦ Γ ⟧* Δ vvs ⊢ ∃ vv, vvs !! x = Some vv ∧ ⟦ τ ⟧ Δ vv. + Proof. + iIntros (?) "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen. + destruct (lookup_lt_is_Some_2 vvs x) as [v Hv]. + { by rewrite -Hlen; apply lookup_lt_Some with τ. } + iExists v; iSplit. done. iApply (big_sep_elem_of with "HΓ"). + apply elem_of_list_lookup_2 with x. + rewrite lookup_zip_with; by simplify_option_eq. + Qed. + + Lemma interp_env_nil Δ : True ⊢ ⟦ [] ⟧* Δ []. + Proof. iIntros ""; iSplit; auto. Qed. + Lemma interp_env_cons Δ Γ vvs τ vv : + ⟦ τ :: Γ ⟧* Δ (vv :: vvs) ⊣⊢ ⟦ τ ⟧ Δ vv ∗ ⟦ Γ ⟧* Δ vvs. + Proof. + rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ (_ = _)%I) -assoc. + by apply sep_proper; [apply pure_proper; omega|]. + Qed. + + Lemma interp_env_ren Δ (Γ : list type) vvs τi : + ⟦ subst (ren (+1)) <$> Γ ⟧* (τi :: Δ) vvs ⊣⊢ ⟦ Γ ⟧* Δ vvs. + Proof. + apply sep_proper; [apply pure_proper; by rewrite fmap_length|]. + revert Δ vvs τi; induction Γ=> Δ [|v vs] τi; csimpl; auto. + apply sep_proper; auto. apply (interp_weaken [] [τi] Δ). + Qed. + +End logrel. + +Typeclasses Opaque interp_env. +Notation "⟦ τ ⟧" := (interp τ). +Notation "⟦ τ ⟧ₑ" := (interp_expr (interp τ)). +Notation "⟦ Γ ⟧*" := (interp_env Γ). diff --git a/F_mu_ref/rules_binary.v b/F_mu_ref/rules_binary.v new file mode 100644 index 0000000..b43b39a --- /dev/null +++ b/F_mu_ref/rules_binary.v @@ -0,0 +1,185 @@ +From iris.program_logic Require Import lifting. +From iris.algebra Require Import frac dec_agree gmap list. +From iris.base_logic Require Import big_op auth. +From iris_logrel.F_mu_ref Require Export rules. +From iris.proofmode Require Import tactics. +Import uPred. + +Definition specN := nroot .@ "spec". + +(** The CMRA for the heap of the specification. *) +Definition cfgUR := prodUR (optionUR (exclR exprC)) heapUR. + +(** The CMRA for the thread pool. *) +Class cfgSG Σ := + CFGSG { ctg_heapG :> heapG Σ; cfg_inG :> authG Σ cfgUR; cfg_name : gname }. + +Section definitionsS. + Context `{cfgSG Σ}. + + Definition heapS_mapsto (l : loc) (q : Qp) (v: val) : iProp Σ := + own cfg_name (◯ (∅, {[ l := (q, DecAgree v) ]})). + + Definition tpool_mapsto (e: expr) : iProp Σ := + own cfg_name (◯ (Excl' e, ∅)). + + Definition spec_inv (ρ : cfg lang) : iProp Σ := + (∃ e σ, own cfg_name (● (Excl' e , to_heap σ)) ∗ ■ rtc step ρ ([e],σ))%I. + Definition spec_ctx (ρ : cfg lang) : iProp Σ := + inv specN (spec_inv ρ). + + Global Instance heapS_mapsto_timeless l q v : TimelessP (heapS_mapsto l q v). + Proof. apply _. Qed. + Global Instance spec_ctx_persistent ρ : PersistentP (spec_ctx ρ). + Proof. apply _. Qed. +End definitionsS. +Typeclasses Opaque heapS_mapsto tpool_mapsto. + +Notation "l ↦ₛ{ q } v" := (heapS_mapsto l q v) + (at level 20, q at level 50, format "l ↦ₛ{ q } v") : uPred_scope. +Notation "l ↦ₛ v" := (heapS_mapsto l 1 v) (at level 20) : uPred_scope. +Notation "⤇ e" := (tpool_mapsto e) (at level 20) : uPred_scope. + +Section cfg. + Context `{cfgSG Σ}. + Implicit Types P Q : iProp Σ. + Implicit Types Φ : val → iProp Σ. + Implicit Types σ : state. + Implicit Types g : heapUR. + Implicit Types e : expr. + Implicit Types v : val. + + (** Conversion to tpools and back *) + Lemma step_insert_no_fork K e σ e' σ' : + head_step e σ e' σ' [] → step ([fill K e], σ) ([fill K e'], σ'). + Proof. intros Hst. eapply (step_atomic _ _ _ _ _ _ [] [] []); eauto. + by apply: Ectx_step'. + Qed. + + Lemma step_pure E ρ K e e' : + (∀ σ, head_step e σ e' σ []) → + nclose specN ⊆ E → + spec_ctx ρ ∗ ⤇ fill K e ={E}=∗ ⤇ fill K e'. + Proof. + iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto. + iInv specN as ">Hinv" "Hclose". iDestruct "Hinv" as (e2 σ) "[Hown %]". + iDestruct (own_valid_2 _ with "[$Hown $Hj]") + as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2. + subst. + iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + { by eapply auth_update, prod_local_update_1, option_local_update, + (exclusive_local_update _ (Excl (fill K e'))). } + iFrame "Hj". iApply "Hclose". iNext. iExists (fill K e'), σ. + iFrame. iPureIntro. eapply rtc_r, step_insert_no_fork; eauto. + Qed. + + Lemma step_alloc E ρ K e v: + to_val e = Some v → nclose specN ⊆ E → + spec_ctx ρ ∗ ⤇ fill K (Alloc e) ={E}=∗ ∃ l, ⤇ fill K (Loc l) ∗ l ↦ₛ v. + Proof. + iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx /tpool_mapsto. + iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]". + destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom]. + iDestruct (own_valid_2 _ with "[$Hown $Hj]") + as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2. + subst. + iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + { by eapply auth_update, prod_local_update_1, option_local_update, + (exclusive_local_update _ (Excl (fill K (Loc l)))). } + iMod (own_update with "Hown") as "[Hown Hl]". + { eapply auth_update_alloc, prod_local_update_2, + (alloc_singleton_local_update _ l (1%Qp,DecAgree v)); last done. + by apply lookup_to_heap_None. } + iExists l. rewrite /heapS_mapsto. iFrame "Hj Hl". iApply "Hclose". iNext. + iExists (fill K (Loc l)), (<[l:=v]>σ). + rewrite to_heap_insert; last eauto. iFrame. iPureIntro. + eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto. + Qed. + + Lemma step_load E ρ K l q v: + nclose specN ⊆ E → + spec_ctx ρ ∗ ⤇ fill K (Load (Loc l)) ∗ l ↦ₛ{q} v + ={E}=∗ ⤇ fill K (of_val v) ∗ l ↦ₛ{q} v. + Proof. + iIntros (?) "(#Hinv & Hj & Hl)". + rewrite /spec_ctx /tpool_mapsto /heapS_mapsto. + iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]". + iDestruct (own_valid_2 _ with "[$Hown $Hj]") + as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2. + subst. + iDestruct (own_valid_2 _ with "[$Hown $Hl]") + as %[[_ ?%heap_singleton_included]%prod_included _]%auth_valid_discrete_2. + iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + { by eapply auth_update, prod_local_update_1, option_local_update, + (exclusive_local_update _ (Excl (fill K (of_val v)))). } + iFrame "Hj Hl". iApply "Hclose". iNext. + iExists (fill K (of_val v)), σ. + iFrame. iPureIntro. + eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto. + Qed. + + Lemma step_store E ρ K l v' e v: + to_val e = Some v → nclose specN ⊆ E → + spec_ctx ρ ∗ ⤇ fill K (Store (Loc l) e) ∗ l ↦ₛ v' + ={E}=∗ ⤇ fill K Unit ∗ l ↦ₛ v. + Proof. + iIntros (??) "(#Hinv & Hj & Hl)". + rewrite /spec_ctx /tpool_mapsto /heapS_mapsto. + iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]". + iDestruct (own_valid_2 _ with "[$Hown $Hj]") + as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2. + subst. + iDestruct (own_valid_2 _ with "[$Hown $Hl]") + as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_valid_discrete_2. + iMod (own_update_2 with "[$Hown $Hj]") as "[Hown Hj]". + { by eapply auth_update, prod_local_update_1, option_local_update, + (exclusive_local_update _ (Excl (fill K Unit))). } + iMod (own_update_2 with "[$Hown $Hl]") as "[Hown Hl]". + { eapply auth_update, prod_local_update_2, singleton_local_update, + (exclusive_local_update _ (1%Qp, DecAgree v)); last done. + by rewrite /to_heap lookup_fmap Hl. } + iFrame "Hj Hl". iApply "Hclose". iNext. + iExists (fill K Unit), (<[l:=v]>σ). + rewrite to_heap_insert; last eauto. iFrame. iPureIntro. + eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto. + Qed. + + Lemma step_lam E ρ K e1 e2 v : + to_val e2 = Some v → nclose specN ⊆ E → + spec_ctx ρ ∗ ⤇ fill K (App (Lam e1) e2) + ={E}=∗ ⤇ fill K (e1.[e2/]). + Proof. intros ?; apply step_pure => σ; econstructor; eauto. Qed. + + Lemma step_tlam E ρ K e : + nclose specN ⊆ E → + spec_ctx ρ ∗ ⤇ fill K (TApp (TLam e)) ={E}=∗ ⤇ fill K e. + Proof. apply step_pure => σ; econstructor; eauto. Qed. + + Lemma step_Fold E ρ K e v : + to_val e = Some v → nclose specN ⊆ E → + spec_ctx ρ ∗ ⤇ fill K (Unfold (Fold e)) ={E}=∗ ⤇ fill K e. + Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed. + + Lemma step_fst E ρ K e1 v1 e2 v2 : + to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E → + spec_ctx ρ ∗ ⤇ fill K (Fst (Pair e1 e2)) ={E}=∗ ⤇ fill K e1. + Proof. intros H1 H2; apply step_pure => σ; econstructor; eauto. Qed. + + Lemma step_snd E ρ K e1 v1 e2 v2 : + to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E → + spec_ctx ρ ∗ ⤇ fill K (Snd (Pair e1 e2)) ={E}=∗ ⤇ fill K e2. + Proof. intros H1 H2; apply step_pure => σ; econstructor; eauto. Qed. + + Lemma step_case_inl E ρ K e0 v0 e1 e2 : + to_val e0 = Some v0 → nclose specN ⊆ E → + spec_ctx ρ ∗ ⤇ fill K (Case (InjL e0) e1 e2) + ={E}=∗ ⤇ fill K (e1.[e0/]). + Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed. + + Lemma step_case_inr E ρ K e0 v0 e1 e2 : + to_val e0 = Some v0 → nclose specN ⊆ E → + spec_ctx ρ ∗ ⤇ fill K (Case (InjR e0) e1 e2) + ={E}=∗ ⤇ fill K (e2.[e0/]). + Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed. + +End cfg. diff --git a/F_mu_ref/soundness_binary.v b/F_mu_ref/soundness_binary.v new file mode 100644 index 0000000..022b55d --- /dev/null +++ b/F_mu_ref/soundness_binary.v @@ -0,0 +1,50 @@ +From iris_logrel.F_mu_ref Require Export context_refinement. +From iris.algebra Require Import frac dec_agree. +From iris.base_logic Require Import big_op auth. +From iris.proofmode Require Import tactics. +From iris.program_logic Require Import adequacy. + +Lemma basic_soundness Σ `{irisPreG lang Σ, authG Σ heapUR, authG Σ cfgUR} + e e' τ v thp hp : + (∀ `{cfgSG Σ}, [] ⊨ e ≤log≤ e' : τ) → + rtc step ([e], ∅) (of_val v :: thp, hp) → + (∃ thp' hp' v', rtc step ([e'], ∅) (of_val v' :: thp', hp')). +Proof. + intros Hlog Hsteps. + cut (adequate e ∅ (λ _, ∃ thp' h v, rtc step ([e'], ∅) (of_val v :: thp', h))). + { destruct 1; naive_solver. } + eapply (wp_adequacy Σ); iIntros (?) "Hσ". + iMod (auth_alloc to_heap ownP heapN _ ∅ with "[Hσ]") + as (γh) "[#Hh1 Hh2]"; auto; first done. + iMod (own_alloc (● (Excl' e', ∅) + ⋅ ◯ ((Excl' e', ∅) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]". + { apply auth_valid_discrete_2. split=>//. } + set (Hcfg := CFGSG _ (HeapG _ _ _ γh) _ γc). + iMod (inv_alloc specN _ (spec_inv ([e'], ∅)) with "[Hcfg1]") as "#Hcfg". + { iNext. iExists e', ∅. rewrite {2}/to_heap fin_maps.map_fmap_empty. auto. } + rewrite -(empty_env_subst e). + iApply wp_fupd; iApply wp_wand_r; iSplitL; [iApply (bin_log_related_alt + (Hlog _) [] [] ([e'], ∅) [])|]; simpl. + { rewrite /heap_ctx /spec_ctx /auth_ctx /tpool_mapsto /auth_own /=. + rewrite empty_env_subst -interp_env_nil. by iFrame "Hh1 Hcfg Hcfg2". } + iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]". + iInv specN as ">Hinv" "Hclose". iDestruct "Hinv" as (e'' σ) "[Hown Hsteps]". + iDestruct "Hsteps" as %Hsteps'. + rewrite /tpool_mapsto /auth.auth_own /=. + iDestruct (own_valid_2 with "[$Hown $Hj]") as %Hvalid. + move: Hvalid=> /auth_valid_discrete_2 + [/prod_included [Hv2 _] _]. apply Excl_included, leibniz_equiv in Hv2. subst. + iMod ("Hclose" with "[-]") as "_"; [iExists _, σ; auto|]. + iIntros "!> !%"; eauto. +Qed. + +Lemma binary_soundness Σ `{irisPreG lang Σ, authG Σ heapUR, authG Σ cfgUR} + Γ e e' τ : + (∀ f, e.[upn (length Γ) f] = e) → + (∀ f, e'.[upn (length Γ) f] = e') → + (∀ `{cfgSG Σ}, Γ ⊨ e ≤log≤ e' : τ) → + Γ ⊨ e ≤ctx≤ e' : τ. +Proof. + intros He He' Hlog K thp σ v ?. eapply (basic_soundness Σ)=> ?. + eapply (bin_log_related_under_typed_ctx _ _ _ _ []); eauto. +Qed. diff --git a/F_mu_ref/typing.v b/F_mu_ref/typing.v index 87de4c3..4e48bd7 100644 --- a/F_mu_ref/typing.v +++ b/F_mu_ref/typing.v @@ -54,18 +54,114 @@ Proof. induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega. Qed. +Lemma n_closed_invariant n (e : expr) s1 s2 : + (∀ f, e.[upn n f] = e) → (∀ x, x < n → s1 x = s2 x) → e.[s1] = e.[s2]. +Proof. + intros Hnc. specialize (Hnc (ren (+1))). + revert n Hnc s1 s2. + induction e => m Hmc s1 s2 H1; asimpl in *; try f_equal; + try (match goal with H : _ |- _ => eapply H end; eauto; + try inversion Hmc; try match goal with H : _ |- _ => by rewrite H end; + fail). + - apply H1. rewrite iter_up in Hmc. destruct lt_dec; try omega. + asimpl in *. cbv in x. replace (m + (x - m)) with x in Hmc by omega. + inversion Hmc; omega. + - unfold upn in *. + change (e.[up (upn m (ren (+1)))]) with + (e.[iter (S m) up (ren (+1))]) in *. + apply (IHe (S m)). + + inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end. + + intros [|[|x]] H2; [by cbv| |]. + asimpl; rewrite H1; auto with omega. + asimpl; rewrite H1; auto with omega. + - change (e1.[up (upn m (ren (+1)))]) with + (e1.[iter (S m) up (ren (+1))]) in *. + apply (IHe0 (S m)). + + inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end. + + intros [|x] H2; [by cbv |]. + asimpl; rewrite H1; auto with omega. + - change (e2.[up (upn m (ren (+1)))]) with + (e2.[upn (S m) (ren (+1))]) in *. + apply (IHe1 (S m)). + + inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end. + + intros [|x] H2; [by cbv |]. + asimpl; rewrite H1; auto with omega. +Qed. + Definition env_subst (vs : list val) (x : var) : expr := from_option id (Var x) (of_val <$> vs !! x). +Lemma typed_n_closed Γ τ e : Γ ⊢ₜ e : τ → (∀ f, e.[upn (length Γ) f] = e). +Proof. + intros H. induction H => f; asimpl; simpl in *; auto with f_equal. + - apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with omega. + - by f_equal; rewrite map_length in IHtyped. +Qed. + +Lemma n_closed_subst_head_simpl n e w ws : + (∀ f, e.[upn n f] = e) → + S (length ws) = n → + e.[of_val w .: env_subst ws] = e.[env_subst (w :: ws)]. +Proof. + intros H1 H2. + rewrite /env_subst. eapply n_closed_invariant; eauto=> /= -[|x] ? //=. + destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl. + by rewrite Hv. +Qed. + Lemma typed_subst_head_simpl Δ τ e w ws : Δ ⊢ₜ e : τ → length Δ = S (length ws) → - e.[# w .: env_subst ws] = e.[env_subst (w :: ws)]. + e.[of_val w .: env_subst ws] = e.[env_subst (w :: ws)]. +Proof. eauto using n_closed_subst_head_simpl, typed_n_closed. Qed. + +Lemma n_closed_subst_head_simpl_2 n e w w' ws : + (∀ f, e.[upn n f] = e) → (S (S (length ws))) = n → + e.[of_val w .: of_val w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)]. Proof. - intros H1 H2. rewrite /env_subst. - eapply typed_subst_invariant; eauto=> /= -[|x] ? //=. - destruct (lookup_lt_is_Some_2 ws x) as [v' ?]; first omega. - by simplify_option_eq. + intros H1 H2. + rewrite /env_subst. eapply n_closed_invariant; eauto => /= -[|[|x]] H3 //=. + destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl. + by rewrite Hv. Qed. +Lemma typed_subst_head_simpl_2 Δ τ e w w' ws : + Δ ⊢ₜ e : τ → length Δ = 2 + length ws → + e.[of_val w .: of_val w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)]. +Proof. eauto using n_closed_subst_head_simpl_2, typed_n_closed. Qed. + Lemma empty_env_subst e : e.[env_subst []] = e. Proof. change (env_subst []) with (@ids expr _). by asimpl. Qed. + +(** Weakening *) +Lemma context_gen_weakening ξ Γ' Γ e τ : + Γ' ++ Γ ⊢ₜ e : τ → + Γ' ++ ξ ++ Γ ⊢ₜ e.[upn (length Γ') (ren (+ (length ξ)))] : τ. +Proof. + intros H1. + remember (Γ' ++ Γ) as Ξ. revert Γ' Γ ξ HeqΞ. + induction H1 => Γ1 Γ2 ξ HeqΞ; subst; asimpl in *; eauto using typed. + - rewrite iter_up; destruct lt_dec as [Hl | Hl]. + + constructor. rewrite lookup_app_l; trivial. by rewrite lookup_app_l in H. + + asimpl. constructor. rewrite lookup_app_r; auto with omega. + rewrite lookup_app_r; auto with omega. + rewrite lookup_app_r in H; auto with omega. + match goal with + |- _ !! ?A = _ => by replace A with (x - length Γ1) by omega + end. + - econstructor; eauto. by apply (IHtyped2 (_::_)). by apply (IHtyped3 (_::_)). + - constructor. by apply (IHtyped (_ :: _)). + - constructor. + specialize (IHtyped + (subst (ren (+1)) <$> Γ1) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)). + asimpl in *. rewrite ?map_length in IHtyped. + repeat rewrite fmap_app. apply IHtyped. + by repeat rewrite fmap_app. +Qed. + +Lemma context_weakening ξ Γ e τ : + Γ ⊢ₜ e : τ → ξ ++ Γ ⊢ₜ e.[(ren (+ (length ξ)))] : τ. +Proof. eapply (context_gen_weakening _ []). Qed. + +Lemma closed_context_weakening ξ Γ e τ : + (∀ f, e.[f] = e) → Γ ⊢ₜ e : τ → ξ ++ Γ ⊢ₜ e : τ. +Proof. intros H1 H2. erewrite <- H1. by eapply context_weakening. Qed. diff --git a/F_mu_ref_conc/lang.v b/F_mu_ref_conc/lang.v index 9038bdb..dff9ecc 100644 --- a/F_mu_ref_conc/lang.v +++ b/F_mu_ref_conc/lang.v @@ -312,4 +312,4 @@ Ltac solve_atomic := rewrite ?to_of_val; eapply mk_is_Some; fast_done. Hint Extern 0 (language.atomic _) => solve_atomic. -Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances. +Hint Extern 0 (language.atomic _) => solve_atomic : atomic. diff --git a/README.md b/README.md index 316f3f0..21a6e23 100644 --- a/README.md +++ b/README.md @@ -5,4 +5,4 @@ This version is known to compile with: - Coq 8.5pl2 - Ssreflect 1.6 - Autosubst 1.5 - - Iris version https://gitlab.mpi-sws.org/FP/iris-coq/commit/37cf94e2 + - Iris version https://gitlab.mpi-sws.org/FP/iris-coq/commit/2a7755f diff --git a/_CoqProject b/_CoqProject index fa6a0a6..0246a2d 100644 --- a/_CoqProject +++ b/_CoqProject @@ -15,9 +15,14 @@ F_mu/soundness.v F_mu_ref/lang.v F_mu_ref/typing.v F_mu_ref/rules.v +F_mu_ref/rules_binary.v F_mu_ref/logrel.v +F_mu_ref/logrel_binary.v F_mu_ref/fundamental.v +F_mu_ref/fundamental_binary.v F_mu_ref/soundness.v +F_mu_ref/context_refinement.v +F_mu_ref/soundness_binary.v F_mu_ref_conc/lang.v F_mu_ref_conc/rules.v F_mu_ref_conc/typing.v -- GitLab