Commit aaafdfea by Robbert Krebbers

State soundness and type_soundness separately.

parent a850d3b3
 ... ... @@ -3,10 +3,14 @@ From iris.proofmode Require Import tactics. From iris_logrel.F_mu Require Import rules. From iris.algebra Require Export upred_big_op. Section typed_interp. Definition log_typed {Σ} (Γ : list type) (e : expr) (τ : type) := ∀ Δ vs, @env_PersistentP Σ Δ → ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs]. Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next level). Section fundamental. Context {Σ : iFunctor}. Notation D := (valC -n> iProp lang Σ). Implicit Types Δ : listC D. Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) := iApply (@wp_bind _ _ _ [ctx]); ... ... @@ -16,74 +20,72 @@ Section typed_interp. Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial. Theorem fundamental Δ Γ vs e τ (HΔ : env_PersistentP Δ) : Γ ⊢ₜ e : τ → ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs]. Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → log_typed (Σ:=Σ) Γ e τ. Proof. intros Htyped. revert Δ vs HΔ. induction Htyped; iIntros {Δ vs HΔ} "#HΓ"; cbn. induction 1; iIntros {Δ vs HΔ} "#HΓ"; cbn. - (* var *) iDestruct (interp_env_Some_l with "HΓ") as {v} "[% ?]"; first done. rewrite /env_subst. simplify_option_eq. by value_case. - (* unit *) value_case. - (* pair *) smart_wp_bind (PairLCtx e2.[env_subst vs]) v "# Hv" IHHtyped1. smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2. smart_wp_bind (PairLCtx e2.[env_subst vs]) v "# Hv" IHtyped1. smart_wp_bind (PairRCtx v) v' "# Hv'" IHtyped2. value_case; eauto 10. - (* fst *) smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn. smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn. iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst. iApply wp_fst; eauto using to_of_val. - (* snd *) smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn. smart_wp_bind (SndCtx) v "# Hv" IHtyped; cbn. iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst. iApply wp_snd; eauto using to_of_val. - (* injl *) smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; cbn. smart_wp_bind (InjLCtx) v "# Hv" IHtyped; cbn. value_case; eauto. - (* injr *) smart_wp_bind (InjRCtx) v "# Hv" IHHtyped; cbn. smart_wp_bind (InjRCtx) v "# Hv" IHtyped; cbn. value_case; eauto. - (* case *) smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn. smart_wp_bind (CaseCtx _ _) v "#Hv" IHtyped1; cbn. iDestruct (interp_env_length with "HΓ") as %?. iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as {w} "[% Hw]"; simplify_eq/=. + iApply wp_case_inl; auto 1 using to_of_val; asimpl. iNext. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto. iApply (IHtyped2 Δ (w :: vs)). iApply interp_env_cons; auto. + iApply wp_case_inr; auto 1 using to_of_val; asimpl. iNext. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto. iApply (IHtyped3 Δ (w :: vs)). iApply interp_env_cons; auto. - (* lam *) value_case; iAlways; iIntros {w} "#Hw". iDestruct (interp_env_length with "HΓ") as %?. iApply wp_lam; auto 1 using to_of_val. iNext. asimpl. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped Δ (w :: vs)). iApply interp_env_cons; auto. iApply (IHtyped Δ (w :: vs)). iApply interp_env_cons; auto. - (* app *) smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1. smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2. smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1. smart_wp_bind (AppRCtx v) w "#Hw" IHtyped2. iApply wp_mono; [|iApply "Hv"]; auto. - (* TLam *) value_case. iAlways; iIntros { τi } "%". iApply wp_TLam; iNext. iApply IHHtyped. by iApply interp_env_ren. iApply IHtyped. by iApply interp_env_ren. - (* TApp *) smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn. smart_wp_bind TAppCtx v "#Hv" IHtyped; cbn. iApply wp_wand_r; iSplitL; [iApply ("Hv" \$! (⟦ τ' ⟧ Δ)); iPureIntro; apply _|]. iIntros {w} "?". by rewrite interp_subst. - (* Fold *) iApply (@wp_bind _ _ _ [FoldCtx]); iApply wp_wand_l; iSplitL; [|iApply (IHHtyped Δ vs); auto]. iApply wp_wand_l; iSplitL; [|iApply (IHtyped Δ vs); auto]. iIntros {v} "#Hv". value_case. rewrite /= -interp_subst fixpoint_unfold /=. iAlways; eauto. - (* Unfold *) iApply (@wp_bind _ _ _ [UnfoldCtx]); iApply wp_wand_l; iSplitL; [|iApply IHHtyped; trivial]. iApply wp_wand_l; iSplitL; [|iApply IHtyped; trivial]. iIntros {v} "#Hv". rewrite /= fixpoint_unfold. change (fixpoint _) with (⟦ TRec τ ⟧ Δ); simpl. iDestruct "Hv" as {w} "#[% Hw]"; subst. iApply wp_Fold; cbn; auto using to_of_val. by rewrite -interp_subst. Qed. End typed_interp. End fundamental.
 ... ... @@ -2,22 +2,22 @@ From iris_logrel.F_mu Require Export fundamental. From iris.proofmode Require Import tactics. From iris.program_logic Require Import adequacy. Section soundness. Let Σ := #[]. Theorem soundness Σ e τ e' thp σ σ' : log_typed (Σ:=Σ) [] e τ → rtc step ([e], σ) (e' :: thp, σ') → is_Some (to_val e') ∨ reducible e' σ'. Proof. intros Hlog ?. eapply (wp_adequacy_reducible ⊤ (λ _, True%I)); eauto using ucmra_unit_valid; last by constructor. iIntros "_". rewrite -(empty_env_subst e). iApply wp_wand_l; iSplitR; [|iApply Hlog]; eauto. by iApply interp_env_nil. Qed. Lemma wp_soundness e τ : [] ⊢ₜ e : τ → True ⊢ WP e {{ @interp (globalF Σ) τ [] }}. Proof. iIntros {H} "". rewrite -(empty_env_subst e). iApply (@fundamental _ _ _ []); eauto. by iApply interp_env_nil. Qed. Theorem soundness e τ e' thp : [] ⊢ₜ e : τ → rtc step ([e], ()) (e' :: thp, ()) → is_Some (to_val e') ∨ reducible e' (). Proof. intros ??. eapply wp_adequacy_reducible; eauto using ucmra_unit_valid. - iIntros "H". by iApply wp_soundness. - constructor. Qed. End soundness. Lemma type_soundness e τ e' thp σ σ' : [] ⊢ₜ e : τ → rtc step ([e], σ) (e' :: thp, σ') → is_Some (to_val e') ∨ reducible e' σ'. Proof. set (Σ := #[]). intros Htyped. eapply (@soundness (globalF Σ)), fundamental, Htyped. Qed.
 ... ... @@ -3,10 +3,14 @@ From iris.proofmode Require Import tactics pviewshifts invariants. From iris_logrel.F_mu_ref Require Import rules. From iris.algebra Require Export upred_big_op. Section typed_interp. Definition log_typed `{heapG Σ} (Γ : list type) (e : expr) (τ : type) := ∀ Δ vs, env_PersistentP Δ → heap_ctx ∧ ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs]. Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next level). Section fundamental. Context `{heapG Σ}. Notation D := (valC -n> iPropG lang Σ). Implicit Types Δ : listC D. Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) := iApply (@wp_bind _ _ _ [ctx]); ... ... @@ -15,78 +19,75 @@ Section typed_interp. Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|]. Theorem fundamental Δ Γ vs e τ (HΔ : env_PersistentP Δ) : Γ ⊢ₜ e : τ → heap_ctx ∧ ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs]. Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → Γ ⊨ e : τ. Proof. intros Htyped; revert Δ vs HΔ. induction Htyped; iIntros {Δ vs HΔ} "#[Hheap HΓ] /=". induction 1; iIntros {Δ vs HΔ} "#[Hheap HΓ] /=". - (* var *) iDestruct (interp_env_Some_l with "HΓ") as {v} "[% ?]"; first done. rewrite /env_subst. simplify_option_eq. by value_case. - (* unit *) by value_case. - (* pair *) smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHHtyped1. smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2. smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHtyped1. smart_wp_bind (PairRCtx v) v' "# Hv'" IHtyped2. value_case; eauto 10. - (* fst *) smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn. smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn. iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst. iApply wp_fst; eauto using to_of_val. - (* snd *) smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn. smart_wp_bind (SndCtx) v "# Hv" IHtyped; cbn. iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst. iApply wp_snd; eauto using to_of_val. - (* injl *) smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; cbn. smart_wp_bind (InjLCtx) v "# Hv" IHtyped; cbn. value_case; eauto. - (* injr *) smart_wp_bind (InjRCtx) v "# Hv" IHHtyped; cbn. smart_wp_bind (InjRCtx) v "# Hv" IHtyped; cbn. value_case; eauto. - (* case *) smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn. smart_wp_bind (CaseCtx _ _) v "#Hv" IHtyped1; cbn. iDestruct (interp_env_length with "HΓ") as %?. iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as {w} "[% Hw]"; simplify_eq/=. + iApply wp_case_inl; auto 1 using to_of_val; asimpl. iNext. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped2 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto. iApply (IHtyped2 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto. + iApply wp_case_inr; auto 1 using to_of_val; asimpl. iNext. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped3 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto. iApply (IHtyped3 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto. - (* lam *) value_case; iAlways; iIntros {w} "#Hw". iDestruct (interp_env_length with "HΓ") as %?. iApply wp_lam; auto 1 using to_of_val. iNext. asimpl. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped Δ (w :: vs)). iFrame "Hheap". iApply interp_env_cons; auto. iApply (IHtyped Δ (w :: vs)). iFrame "Hheap". iApply interp_env_cons; auto. - (* app *) smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1. smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2. smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1. smart_wp_bind (AppRCtx v) w "#Hw" IHtyped2. iApply wp_mono; [|iApply "Hv"]; auto. - (* TLam *) value_case. iAlways; iIntros { τi } "%". iApply wp_TLam; iNext. iApply IHHtyped. iFrame "Hheap". by iApply interp_env_ren. iApply IHtyped. iFrame "Hheap". by iApply interp_env_ren. - (* TApp *) smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn. smart_wp_bind TAppCtx v "#Hv" IHtyped; cbn. iApply wp_wand_r; iSplitL; [iApply ("Hv" \$! (interp τ' Δ)); iPureIntro; apply _|]. iIntros {w} "?". by rewrite interp_subst. - (* Fold *) iApply (@wp_bind _ _ _ [FoldCtx]); iApply wp_wand_l; iSplitL; [|iApply (IHHtyped Δ vs); auto]. iApply wp_wand_l; iSplitL; [|iApply (IHtyped Δ vs); auto]. iIntros {v} "#Hv". value_case. rewrite /= -interp_subst fixpoint_unfold /=. iAlways; eauto. - (* Unfold *) iApply (@wp_bind _ _ _ [UnfoldCtx]); iApply wp_wand_l; iSplitL; [|iApply IHHtyped; auto]. iApply wp_wand_l; iSplitL; [|iApply IHtyped; auto]. iIntros {v} "#Hv". rewrite /= fixpoint_unfold. change (fixpoint _) with (interp (TRec τ) Δ); simpl. iDestruct "Hv" as {w} "#[% Hw]"; subst. iApply wp_Fold; cbn; auto using to_of_val. iNext; iPvsIntro. by rewrite -interp_subst. - (* Alloc *) smart_wp_bind AllocCtx v "#Hv" IHHtyped; cbn. iClear "HΓ". smart_wp_bind AllocCtx v "#Hv" IHtyped; cbn. iClear "HΓ". iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|]. iPvsIntro. iApply wp_alloc; auto 1 using to_of_val. ... ... @@ -94,7 +95,7 @@ Section typed_interp. iPvs (inv_alloc _ with "[Hl]") as "HN"; [| | iPvsIntro; iExists _; iSplit; trivial]; eauto. - (* Load *) smart_wp_bind LoadCtx v "#Hv" IHHtyped; cbn. iClear "HΓ". smart_wp_bind LoadCtx v "#Hv" IHtyped; cbn. iClear "HΓ". iDestruct "Hv" as {l} "[% #Hv]"; subst. iApply wp_atomic; cbn; eauto using to_of_val. iPvsIntro. ... ... @@ -102,8 +103,8 @@ Section typed_interp. iApply (wp_load _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj. iIntros "{\$Hw1} > Hw1". iPvsIntro. iSplitL; eauto. - (* Store *) smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn. smart_wp_bind (StoreRCtx _) w "#Hw" IHHtyped2; cbn. iClear "HΓ". smart_wp_bind (StoreLCtx _) v "#Hv" IHtyped1; cbn. smart_wp_bind (StoreRCtx _) w "#Hw" IHtyped2; cbn. iClear "HΓ". iDestruct "Hv" as {l} "[% #Hv]"; subst. iApply wp_atomic; cbn; [trivial| rewrite ?to_of_val; auto |]. iPvsIntro. ... ... @@ -113,4 +114,4 @@ Section typed_interp. iIntros "{\$Hheap \$Hz1} > Hz1". iPvsIntro. iSplitL; eauto 10. Qed. End typed_interp. End fundamental.
 From iris_logrel.F_mu_ref Require Export fundamental. From iris.proofmode Require Import tactics pviewshifts. From iris.program_logic Require Import ownership adequacy. From iris.program_logic Require Import ownership adequacy auth. Section soundness. Let Σ := #[ auth.authGF heapUR ]. Theorem soundness `{authG lang Σ heapUR} e τ e' thp σ σ' : (∀ `{heapG Σ}, [] ⊨ e : τ) → rtc step ([e], σ) (e' :: thp, σ') → is_Some (to_val e') ∨ reducible e' σ'. Proof. intros Hlog ?. eapply (wp_adequacy_reducible ⊤ (λ _, True%I)); eauto using ucmra_unit_valid; last by constructor. iIntros "[Hemp _]". iPvs (heap_alloc with "Hemp") as {h} "[Hheap Hemp]"; first solve_ndisj. rewrite -(empty_env_subst e). iApply wp_wand_l; iSplitR; [|iApply Hlog]; eauto. repeat iSplit; eauto. by iApply interp_env_nil. Qed. Lemma wp_soundness e τ σ : [] ⊢ₜ e : τ → ownP σ ⊢ WP e {{ v, ∃ H : heapG Σ, interp τ [] v}}. Proof. iIntros {H1} "Hemp". iPvs (heap_alloc with "Hemp") as {H} "[Hheap Hemp]"; first solve_ndisj. iApply wp_wand_l. iSplitR. { iIntros {v} "HΦ". iExists H. iExact "HΦ". } rewrite -(empty_env_subst e). iApply fundamental; repeat iSplit; eauto. by iApply interp_env_nil. Qed. Theorem soundness e τ e' thp σ σ' : [] ⊢ₜ e : τ → rtc step ([e], σ) (e' :: thp, σ') → is_Some (to_val e') ∨ reducible e' σ'. Proof. intros ??. eapply wp_adequacy_reducible; eauto using ucmra_unit_valid. - iIntros "[??]". by iApply wp_soundness. - constructor. Qed. End soundness. Lemma type_soundness e τ e' thp σ σ' : [] ⊢ₜ e : τ → rtc step ([e], σ) (e' :: thp, σ') → is_Some (to_val e') ∨ reducible e' σ'. Proof. set (Σ := #[ auth.authGF heapUR ]). intros Htyped. eapply (@soundness Σ _)=> ?. eapply fundamental, Htyped. Qed.
 ... ... @@ -3,10 +3,14 @@ From iris_logrel.F_mu_ref_par Require Import rules. From iris.algebra Require Export upred_big_op. From iris.proofmode Require Import tactics pviewshifts invariants. Definition log_typed `{heapIG Σ} (Γ : list type) (e : expr) (τ : type) := ∀ Δ vs, env_PersistentP Δ → heapI_ctx ∧ ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs]. Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next level). Section typed_interp. Context `{heapIG Σ}. Notation D := (valC -n> iPropG lang Σ). Implicit Types Δ : listC D. Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) := iApply (@wp_bind _ _ _ [ctx]); ... ... @@ -15,12 +19,9 @@ Section typed_interp. Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|]. Theorem fundamental Δ Γ vs e τ (HΔ : env_PersistentP Δ) : Γ ⊢ₜ e : τ → heapI_ctx ∧ ⟦ Γ ⟧* Δ vs ⊢ ⟦ τ ⟧ₑ Δ e.[env_subst vs]. Theorem fundamental Γ e τ : Γ ⊢ₜ e : τ → Γ ⊨ e : τ. Proof. intros Htyped; revert Δ vs HΔ. induction Htyped; iIntros {Δ vs HΔ} "#[Hheap HΓ] /=". induction 1; iIntros {Δ vs HΔ} "#[Hheap HΓ] /=". - (* var *) iDestruct (interp_env_Some_l with "HΓ") as {v} "[% ?]"; first done. rewrite /env_subst. simplify_option_eq. by value_case. ... ... @@ -28,74 +29,74 @@ Section typed_interp. - (* nat *) value_case; simpl; eauto. - (* bool *) value_case; simpl; eauto. - (* nat bin op *) smart_wp_bind (BinOpLCtx _ e2.[env_subst vs]) v "#Hv" IHHtyped1. smart_wp_bind (BinOpRCtx _ v) v' "# Hv'" IHHtyped2. smart_wp_bind (BinOpLCtx _ e2.[env_subst vs]) v "#Hv" IHtyped1. smart_wp_bind (BinOpRCtx _ v) v' "# Hv'" IHtyped2. iDestruct "Hv" as {n} "%"; iDestruct "Hv'" as {n'} "%"; simplify_eq/=. iApply wp_nat_binop. iNext; iPvsIntro. iClear "Hheap HΓ". destruct op; simpl; try destruct eq_nat_dec; try destruct le_dec; try destruct lt_dec; eauto 10. - (* pair *) smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHHtyped1. smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2. smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHtyped1. smart_wp_bind (PairRCtx v) v' "# Hv'" IHtyped2. value_case; eauto. - (* fst *) smart_wp_bind (FstCtx) v "# Hv" IHHtyped; cbn. smart_wp_bind (FstCtx) v "# Hv" IHtyped; cbn. iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst. iApply wp_fst; eauto using to_of_val. - (* snd *) smart_wp_bind (SndCtx) v "# Hv" IHHtyped; cbn. smart_wp_bind (SndCtx) v "# Hv" IHtyped; cbn. iDestruct "Hv" as {w1 w2} "#[% [H2 H3]]"; subst. iApply wp_snd; eauto using to_of_val. - (* injl *) smart_wp_bind (InjLCtx) v "# Hv" IHHtyped; cbn. smart_wp_bind (InjLCtx) v "# Hv" IHtyped; cbn. value_case; eauto. - (* injr *) smart_wp_bind (InjRCtx) v "# Hv" IHHtyped; cbn. smart_wp_bind (InjRCtx) v "# Hv" IHtyped; cbn. value_case; eauto. - (* case *) smart_wp_bind (CaseCtx _ _) v "#Hv" IHHtyped1; cbn. smart_wp_bind (CaseCtx _ _) v "#Hv" IHtyped1; cbn. iDestruct (interp_env_length with "HΓ") as %?. iDestruct "Hv" as "[Hv|Hv]"; iDestruct "Hv" as {w} "[% Hw]"; simplify_eq/=. + iApply wp_case_inl; auto 1 using to_of_val; asimpl. iNext. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped2 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto. iApply (IHtyped2 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto. + iApply wp_case_inr; auto 1 using to_of_val; asimpl. iNext. erewrite typed_subst_head_simpl by naive_solver. iApply (IHHtyped3 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto. iApply (IHtyped3 Δ (w :: vs)). iSplit; [|iApply interp_env_cons]; auto. - (* If *) smart_wp_bind (IfCtx _ _) v "#Hv" IHHtyped1; cbn. smart_wp_bind (IfCtx _ _) v "#Hv" IHtyped1; cbn. iDestruct "Hv" as { [] } "%"; subst; simpl; [iApply wp_if_true| iApply wp_if_false]; iNext; [iApply IHHtyped2| iApply IHHtyped3]; auto. [iApply IHtyped2| iApply IHtyped3]; auto. - (* Rec *) value_case; iAlways. simpl. iLöb as "IH"; iIntros {w} "#Hw". iDestruct (interp_env_length with "HΓ") as %?. iApply wp_rec; auto 1 using to_of_val. iNext. asimpl. change (Rec _) with (# (RecV e.[upn 2 (env_subst vs)])). erewrite typed_subst_head_simpl_2 by naive_solver. iApply (IHHtyped Δ (_ :: w :: vs)). iSplit; [done|]. iApply (IHtyped Δ (_ :: w :: vs)). iSplit; [done|]. iApply interp_env_cons; iSplit; [|iApply interp_env_cons]; auto. - (* app *) smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHHtyped1. smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2. smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1. smart_wp_bind (AppRCtx v) w "#Hw" IHtyped2. iApply wp_mono; [|iApply "Hv"]; auto. - (* TLam *) value_case. iAlways; iIntros { τi } "%". iApply wp_tlam; iNext. iApply IHHtyped. iFrame "Hheap". by iApply interp_env_ren. iApply IHtyped. iFrame "Hheap". by iApply interp_env_ren. - (* TApp *) smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn. smart_wp_bind TAppCtx v "#Hv" IHtyped; cbn. iApply wp_wand_r; iSplitL; [iApply ("Hv" \$! (⟦ τ' ⟧ Δ)); iPureIntro; apply _|]; cbn. iIntros {w} "?". by iApply interp_subst. - (* Fold *) iApply (@wp_bind _ _ _ [FoldCtx]); iApply wp_wand_l; iSplitL; [|iApply (IHHtyped Δ vs); auto]. iApply wp_wand_l; iSplitL; [|iApply (IHtyped Δ vs); auto]. iIntros {v} "#Hv". value_case. rewrite /= -interp_subst fixpoint_unfold /=. iAlways; eauto. - (* Unfold *) iApply (@wp_bind _ _ _ [UnfoldCtx]); iApply wp_wand_l; iSplitL; [|iApply IHHtyped; auto]. iApply wp_wand_l; iSplitL; [|iApply IHtyped; auto]. iIntros {v} "#Hv". rewrite /= fixpoint_unfold. change (fixpoint _) with (⟦ TRec τ ⟧ Δ); simpl. iDestruct "Hv" as {w} "#[% Hw]"; subst. ... ... @@ -103,9 +104,9 @@ Section typed_interp. iNext; iPvsIntro. by iApply interp_subst. - (* Fork *) iApply wp_fork. iNext; iSplitL; trivial. iApply wp_wand_l. iSplitL; [|iApply IHHtyped; auto]; auto. iApply wp_wand_l. iSplitL; [|iApply IHtyped; auto]; auto. - (* Alloc *) smart_wp_bind AllocCtx v "#Hv" IHHtyped; cbn. iClear "HΓ". smart_wp_bind AllocCtx v "#Hv" IHtyped; cbn. iClear "HΓ". iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|]. iPvsIntro. iApply wp_alloc; auto 1 using to_of_val. ... ... @@ -114,7 +115,7 @@ Section typed_interp. iPvs (inv_alloc _ with "[Hl]") as "HN"; [| | iPvsIntro; iExists _; iSplit; trivial]; eauto. - (* Load *) smart_wp_bind LoadCtx v "#Hv" IHHtyped; cbn. iClear "HΓ". smart_wp_bind LoadCtx v "#Hv" IHtyped; cbn. iClear "HΓ". iDestruct "Hv" as {l} "[% #Hv]"; subst. iApply wp_atomic; cbn; eauto using to_of_val. iPvsIntro. ... ... @@ -122,8 +123,8 @@ Section typed_interp. iApply (wp_load _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj. iIntros "{\$Hw1} > Hw1". iPvsIntro; iSplitL; eauto. - (* Store *) smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn. smart_wp_bind (StoreRCtx _) w "#Hw" IHHtyped2; cbn. iClear "HΓ". smart_wp_bind (StoreLCtx _) v "#Hv" IHtyped1; cbn. smart_wp_bind (StoreRCtx _) w "#Hw" IHtyped2; cbn. iClear "HΓ". iDestruct "Hv" as {l} "[% #Hv]"; subst. iApply wp_atomic; cbn; [trivial| rewrite ?to_of_val; auto |]. iPvsIntro. ... ... @@ -132,9 +133,9 @@ Section typed_interp. iApply wp_store; auto using to_of_val. solve_ndisj. iIntros "{\$Hheap \$Hz1} > Hz1". iPvsIntro. iSplitL; eauto 10. - (* CAS *) smart_wp_bind (CasLCtx _ _) v1 "#Hv1" IHHtyped1; cbn. smart_wp_bind (CasMCtx _ _) v2 "#Hv2" IHHtyped2; cbn. smart_wp_bind (CasRCtx _ _) v3 "#Hv3" IHHtyped3; cbn. iClear "HΓ". smart_wp_bind (CasLCtx _ _) v1 "#Hv1" IHtyped1; cbn. smart_wp_bind (CasMCtx _ _) v2 "#Hv2" IHtyped2; cbn. smart_wp_bind (CasRCtx _ _) v3 "#Hv3" IHtyped3; cbn. iClear "HΓ". iDestruct "Hv1" as {l} "[% Hinv]"; subst. iApply wp_atomic; cbn; eauto 10 using to_of_val. iPvsIntro. ... ...
 From iris_logrel.F_mu_ref_par Require Export fundamental_unary. From iris.proofmode Require Import tactics pviewshifts. From iris.program_logic Require Import ownership adequacy. From iris.program_logic Require Import ownership adequacy auth. Section soundness. Let Σ := #[ auth.authGF heapUR ]. Theorem soundness `{authG lang Σ heapUR} e τ e' thp σ σ' : (∀ `{heapIG Σ}, [] ⊨ e : τ) → rtc step ([e], σ) (e' :: thp, σ') → is_Some (to_val e') ∨ reducible e' σ'. Proof. intros Hlog ?. eapply (wp_adequacy_reducible ⊤ (λ _, True%I)); eauto using ucmra_unit_valid; last by constructor. iIntros "[Hemp _]". iPvs (heap_alloc with "Hemp") as {h} "[Hheap Hemp]"; first solve_ndisj. rewrite -(empty_env_subst e). iApply wp_wand_l; iSplitR; [|iApply Hlog]; eauto. repeat iSplit; eauto. by iApply interp_env_nil. Qed. Lemma wp_soundness e τ σ : [] ⊢ₜ e : τ → ownP σ ⊢ WP e {{ v, ∃ H : heapIG Σ, interp τ [] v}}. Proof. iIntros {H1} "Hemp". iPvs (heap_alloc with "Hemp") as {H} "[Hheap Hemp]"; first solve_ndisj. iApply wp_wand_l. iSplitR. { iIntros {v} "HΦ". iExists H. iExact "HΦ". } rewrite -(empty_env_subst e). iApply fundamental; repeat iSplit; eauto. by iApply interp_env_nil. Qed. Theorem soundness e τ e' thp σ σ' : [] ⊢ₜ e : τ → rtc step ([e], σ) (e' :: thp, σ') → is_Some (to_val e') ∨ reducible e' σ'. Proof. intros ??. eapply wp_adequacy_reducible; eauto using ucmra_unit_valid. - iIntros "[??]". by iApply wp_soundness. - constructor. Qed. End soundness. Lemma type_soundness e τ e' thp σ σ' : [] ⊢ₜ e : τ → rtc step ([e], σ) (e' :: thp, σ') → is_Some (to_val e') ∨ reducible e' σ'. Proof. set (Σ := #[ auth.authGF heapUR ]). intros Htyped. eapply (@soundness Σ _)=> ?. eapply fundamental, Htyped. Qed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!