diff --git a/Makefile.coq.local b/Makefile.coq.local index fb4d5d7737493631106a8f6f7210ed66fd8d0742..317d90a4fbee005b25622ebacbea3dcd9cb86ea0 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -17,6 +17,9 @@ concurrent_stacks: $(filter theories/concurrent_stacks/%,$(VOFILES)) logrel: $(filter theories/logrel/%,$(VOFILES)) .PHONY: logrel +logrel_heaplang: $(filter theories/logrel_heaplang/%,$(VOFILES)) +.PHONY: logrel_heaplang + hocap: $(filter theories/hocap/%,$(VOFILES)) .PHONY: hocap diff --git a/_CoqProject b/_CoqProject index 3b448da5050848e695d03043f8e4ee30479dec8b..1cd4ba57ea2ab0988de8d2d0e7b2fb33473236b3 100644 --- a/_CoqProject +++ b/_CoqProject @@ -72,6 +72,10 @@ theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v theories/logrel/F_mu_ref_conc/examples/stack/refinement.v theories/logrel/F_mu_ref_conc/examples/fact.v +theories/logrel_heaplang/ltyping.v +theories/logrel_heaplang/ltyping_safety.v +theories/logrel_heaplang/lib/symbol_adt.v + theories/hocap/abstract_bag.v theories/hocap/cg_bag.v theories/hocap/fg_bag.v diff --git a/opam b/opam index 9ea3f4ce425ed058d63f76546e0b67ad67557e95..5a717a6b3b5a7c135b8b5524fd2a40a0fa7f4219 100644 --- a/opam +++ b/opam @@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] install: [make "install"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"] depends: [ - "coq-iris" { (= "dev.2018-11-08.2.9eee9408") | (= "dev") } + "coq-iris" { (= "dev.2018-12-12.0.b1270b7d") | (= "dev") } "coq-autosubst" { = "dev.coq86" } ] diff --git a/theories/logrel_heaplang/lib/symbol_adt.v b/theories/logrel_heaplang/lib/symbol_adt.v new file mode 100644 index 0000000000000000000000000000000000000000..65b234f7b59bbb3c619cd57331acf368ddc64640 --- /dev/null +++ b/theories/logrel_heaplang/lib/symbol_adt.v @@ -0,0 +1,95 @@ +From iris_examples.logrel_heaplang Require Export ltyping. +From iris.heap_lang.lib Require Import assert. +From iris.algebra Require Import auth. +From iris.base_logic.lib Require Import invariants. +From iris.heap_lang Require Import notation proofmode. + +(* Semantic typing of a symbol ADT (taken from Dreyer's POPL'18 talk) *) +Definition symbol_adt_inc : val := λ: "x" <>, FAA "x" #1. +Definition symbol_adt_check : val := λ: "x" "y", assert: "y" < !"x". +Definition symbol_adt : val := λ: <>, + let: "x" := Alloc #0 in (symbol_adt_inc "x", symbol_adt_check "x"). +Definition symbol_adt_ty `{heapG Σ} : lty := + (() → ∃ A, (() → A) * (A → ()))%lty. + +(* The required ghost theory *) +Class symbolG Σ := { symbol_inG :> inG Σ (authR mnatUR) }. +Definition symbolΣ : gFunctors := #[GFunctor (authR mnatUR)]. + +Instance subG_symbolΣ {Σ} : subG symbolΣ Σ → symbolG Σ. +Proof. solve_inG. Qed. + +Section symbol_ghosts. + Context `{!symbolG Σ}. + + Definition counter (γ : gname) (n : nat) : iProp Σ := own γ (● (n : mnat)). + Definition symbol (γ : gname) (n : nat) : iProp Σ := own γ (◯ (S n : mnat)). + + Global Instance counter_timeless γ n : Timeless (counter γ n). + Proof. apply _. Qed. + Global Instance symbol_timeless γ n : Timeless (symbol γ n). + Proof. apply _. Qed. + + Lemma counter_exclusive γ n1 n2 : counter γ n1 -∗ counter γ n2 -∗ False. + Proof. apply bi.wand_intro_r. by rewrite -own_op own_valid auth_validI. Qed. + Global Instance symbol_persistent γ n : Persistent (symbol γ n). + Proof. apply _. Qed. + + Lemma counter_alloc n : (|==> ∃ γ, counter γ n)%I. + Proof. + iMod (own_alloc (● (n:mnat) ⋅ ◯ (n:mnat))) as (γ) "[Hγ Hγf]"; first done. + iExists γ. by iFrame. + Qed. + + Lemma counter_inc γ n : counter γ n ==∗ counter γ (S n) ∗ symbol γ n. + Proof. + rewrite -own_op. + apply own_update, auth_update_alloc, mnat_local_update. omega. + Qed. + + Lemma symbol_obs γ s n : counter γ n -∗ symbol γ s -∗ ⌜(s < n)%nat⌝. + Proof. + iIntros "Hc Hs". + iDestruct (own_valid_2 with "Hc Hs") as %[?%mnat_included _]%auth_valid_discrete_2. + iPureIntro. omega. + Qed. +End symbol_ghosts. + +Typeclasses Opaque counter symbol. + +Section ltyped_symbol_adt. + Context `{heapG Σ, symbolG Σ}. + + Definition symbol_adtN := nroot .@ "symbol_adt". + + Definition symbol_inv (γ : gname) (l : loc) : iProp Σ := + (∃ n : nat, l ↦ #n ∗ counter γ n)%I. + + Definition symbol_ctx (γ : gname) (l : loc) : iProp Σ := + inv symbol_adtN (symbol_inv γ l). + + Definition lty_symbol (γ : gname) : lty := Lty (λ w, + ∃ n : nat, ⌜w = #n⌝ ∧ symbol γ n)%I. + + Lemma ltyped_symbol_adt Γ : Γ ⊨ symbol_adt : symbol_adt_ty. + Proof. + iIntros (vs) "!# _ /=". iApply wp_value. + iIntros "!#" (v ->). wp_lam. wp_alloc l as "Hl"; wp_pures. + iMod (counter_alloc 0) as (γ) "Hc". + iMod (inv_alloc symbol_adtN _ (symbol_inv γ l) with "[Hl Hc]") as "#?". + { iExists 0%nat. by iFrame. } + do 2 (wp_lam; wp_pures). + iExists (lty_symbol γ), _, _; repeat iSplit=> //. + - repeat rewrite /lty_car /=. iIntros "!#" (? ->). wp_pures. + iInv symbol_adtN as (n) ">[Hl Hc]". wp_faa. + iMod (counter_inc with "Hc") as "[Hc #Hs]". + iModIntro; iSplitL; last eauto. + iExists (S n). rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. + - repeat rewrite /lty_car /=. iIntros "!#" (v). + iDestruct 1 as (n ->) "#Hs". wp_pures. iApply wp_assert. + wp_bind (!_)%E. iInv symbol_adtN as (n') ">[Hl Hc]". wp_load. + iDestruct (symbol_obs with "Hc Hs") as %?. iModIntro. iSplitL. + { iExists n'. iFrame. } + wp_op. rewrite bool_decide_true; last lia. eauto. + Qed. +End ltyped_symbol_adt. diff --git a/theories/logrel_heaplang/ltyping.v b/theories/logrel_heaplang/ltyping.v new file mode 100644 index 0000000000000000000000000000000000000000..39af3989733829c6078972f76ac384f15db96fde --- /dev/null +++ b/theories/logrel_heaplang/ltyping.v @@ -0,0 +1,402 @@ +From iris.heap_lang Require Export lifting metatheory. +From iris.base_logic.lib Require Import invariants. +From iris.heap_lang Require Import notation proofmode. + +(* The domain of semantic types: persistent Iris predicates over values *) +Record lty `{heapG Σ} := Lty { + lty_car :> val → iProp Σ; + lty_persistent v : Persistent (lty_car v) +}. +Arguments Lty {_ _} _%I {_}. +Arguments lty_car {_ _} _ _ : simpl never. +Bind Scope lty_scope with lty. +Delimit Scope lty_scope with lty. +Existing Instance lty_persistent. + +(* The COFE structure on semantic types *) +Section lty_ofe. + Context `{heapG Σ}. + + Instance lty_equiv : Equiv lty := λ A B, ∀ w, A w ≡ B w. + Instance lty_dist : Dist lty := λ n A B, ∀ w, A w ≡{n}≡ B w. + Lemma lty_ofe_mixin : OfeMixin lty. + Proof. by apply (iso_ofe_mixin (lty_car : _ → val -c> _)). Qed. + Canonical Structure ltyC := OfeT lty lty_ofe_mixin. + Global Instance lty_cofe : Cofe ltyC. + Proof. + apply (iso_cofe_subtype' (λ A : val -c> iProp Σ, ∀ w, Persistent (A w)) + (@Lty _ _) lty_car)=> //. + - apply _. + - apply limit_preserving_forall=> w. + by apply bi.limit_preserving_Persistent=> n ??. + Qed. + + Global Instance lty_inhabited : Inhabited lty := populate (Lty inhabitant). + + Global Instance lty_car_ne n : Proper (dist n ==> (=) ==> dist n) lty_car. + Proof. by intros A A' ? w ? <-. Qed. + Global Instance lty_car_proper : Proper ((≡) ==> (=) ==> (≡)) lty_car. + Proof. by intros A A' ? w ? <-. Qed. +End lty_ofe. + +(* Typing for operators *) +Class LTyUnboxed `{heapG Σ} (A : lty) := + lty_unboxed v : A v -∗ ⌜ val_is_unboxed v ⌝. + +Class LTyUnOp `{heapG Σ} (op : un_op) (A B : lty) := + lty_un_op v : A v -∗ ∃ w, ⌜ un_op_eval op v = Some w ⌝ ∧ B w. + +Class LTyBinOp `{heapG Σ} (op : bin_op) (A1 A2 B : lty) := + lty_bin_op v1 v2 : A1 v1 -∗ A2 v2 -∗ ∃ w, ⌜ bin_op_eval op v1 v2 = Some w ⌝ ∧ B w. + +(* The type formers *) +Section types. + Context `{heapG Σ}. + + Definition lty_unit : lty := Lty (λ w, ⌜ w = #() ⌝%I). + Definition lty_bool : lty := Lty (λ w, ∃ b : bool, ⌜ w = #b ⌝)%I. + Definition lty_int : lty := Lty (λ w, ∃ n : Z, ⌜ w = #n ⌝)%I. + + Definition lty_arr (A1 A2 : lty) : lty := Lty (λ w, + □ ∀ v, A1 v -∗ WP App w v {{ A2 }})%I. + + Definition lty_prod (A1 A2 : lty) : lty := Lty (λ w, + ∃ w1 w2, ⌜w = PairV w1 w2⌝ ∧ A1 w1 ∧ A2 w2)%I. + + Definition lty_sum (A1 A2 : lty) : lty := Lty (λ w, + (∃ w1, ⌜w = InjLV w1⌝ ∧ A1 w1) ∨ (∃ w2, ⌜w = InjRV w2⌝ ∧ A2 w2))%I. + + Definition lty_forall (C : lty → lty) : lty := Lty (λ w, + □ ∀ A : lty, WP w #() {{ w, C A w }})%I. + Definition lty_exist (C : lty → lty) : lty := Lty (λ w, + ∃ A : lty, C A w)%I. + + Definition lty_rec1 (C : ltyC -n> ltyC) (rec : lty) : lty := Lty (λ w, + ▷ C rec w)%I. + Instance lty_rec1_contractive C : Contractive (lty_rec1 C). + Proof. solve_contractive. Qed. + Definition lty_rec (C : ltyC -n> ltyC) : lty := fixpoint (lty_rec1 C). + + Definition tyN := nroot .@ "ty". + Definition lty_ref (A : lty) : lty := Lty (λ w, + ∃ l : loc, ⌜w = #l⌝ ∧ inv (tyN .@ l) (∃ v, l ↦ v ∗ A v))%I. +End types. + +(* Nice notations *) +Notation "()" := lty_unit : lty_scope. +Infix "→" := lty_arr : lty_scope. +Infix "*" := lty_prod : lty_scope. +Infix "+" := lty_sum : lty_scope. +Notation "∀ A1 .. An , C" := + (lty_forall (λ A1, .. (lty_forall (λ An, C%lty)) ..)) : lty_scope. +Notation "∃ A1 .. An , C" := + (lty_exist (λ A1, .. (lty_exist (λ An, C%lty)) ..)) : lty_scope. +Notation "'ref' A" := (lty_ref A) : lty_scope. + +(* The semantic typing judgment *) +Definition env_ltyped `{heapG Σ} (Γ : gmap string lty) + (vs : gmap string val) : iProp Σ := + (⌜ ∀ x, is_Some (Γ !! x) ↔ is_Some (vs !! x) ⌝ ∧ + [∗ map] i ↦ Av ∈ map_zip Γ vs, lty_car Av.1 Av.2)%I. +Definition ltyped `{heapG Σ} + (Γ : gmap string lty) (e : expr) (A : lty) : iProp Σ := + (□ ∀ vs, env_ltyped Γ vs -∗ WP subst_map vs e {{ A }})%I. +Notation "Γ ⊨ e : A" := (ltyped Γ e A) + (at level 100, e at next level, A at level 200). + +(* To unfold a recursive type, we need to take a step. We thus define the +unfold operator to be the identity function. *) +Definition rec_unfold : val := λ: "x", "x". + +Section types_properties. + Context `{heapG Σ}. + Implicit Types A B : lty. + Implicit Types C : lty → lty. + + (* Boring stuff: all type formers are non-expansive *) + Global Instance lty_prod_ne : NonExpansive2 lty_prod. + Proof. solve_proper. Qed. + Global Instance lty_sum_ne : NonExpansive2 lty_sum. + Proof. solve_proper. Qed. + Global Instance lty_arr_ne : NonExpansive2 lty_arr. + Proof. solve_proper. Qed. + Global Instance lty_forall_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) lty_forall. + Proof. solve_proper. Qed. + Global Instance lty_exist_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) lty_exist. + Proof. solve_proper. Qed. + Global Instance lty_rec_ne n : Proper (dist n ==> dist n) lty_rec. + Proof. intros C C' HC. apply fixpoint_ne. solve_proper. Qed. + Global Instance lty_ref_ne : NonExpansive2 lty_ref. + Proof. solve_proper. Qed. + + Lemma lty_rec_unfold (C : ltyC -n> ltyC) : lty_rec C ≡ lty_rec1 C (lty_rec C). + Proof. apply fixpoint_unfold. Qed. + + (* Environments *) + Lemma env_ltyped_lookup Γ vs x A : + Γ !! x = Some A → + env_ltyped Γ vs -∗ ∃ v, ⌜ vs !! x = Some v ⌝ ∧ A v. + Proof. + iIntros (HΓx) "[Hlookup HΓ]". iDestruct "Hlookup" as %Hlookup. + destruct (proj1 (Hlookup x)) as [v Hx]; eauto. + iExists v. iSplit; first done. iApply (big_sepM_lookup _ _ x (A,v) with "HΓ"). + by rewrite map_lookup_zip_with HΓx /= Hx. + Qed. + Lemma env_ltyped_insert Γ vs x A v : + A v -∗ env_ltyped Γ vs -∗ + env_ltyped (binder_insert x A Γ) (binder_insert x v vs). + Proof. + destruct x as [|x]=> /=; first by auto. + iIntros "#HA [Hlookup #HΓ]". iDestruct "Hlookup" as %Hlookup. iSplit. + - iPureIntro=> y. rewrite !lookup_insert_is_Some'. naive_solver. + - rewrite -map_insert_zip_with. by iApply big_sepM_insert_2. + Qed. + + (* Unboxed types *) + Global Instance lty_unit_unboxed : LTyUnboxed (). + Proof. by iIntros (v ->). Qed. + Global Instance lty_bool_unboxed : LTyUnboxed lty_bool. + Proof. iIntros (v). by iDestruct 1 as (b) "->". Qed. + Global Instance lty_int_unboxed : LTyUnboxed lty_int. + Proof. iIntros (v). by iDestruct 1 as (i) "->". Qed. + Global Instance lty_ref_unboxed A : LTyUnboxed (ref A). + Proof. iIntros (v). by iDestruct 1 as (i ->) "?". Qed. + + (* Operator typing *) + Global Instance lty_bin_op_eq A : LTyBinOp EqOp A A lty_bool. + Proof. iIntros (v1 v2) "_ _". rewrite /bin_op_eval /lty_car /=. eauto. Qed. + Global Instance lty_bin_op_arith op : + TCElemOf op [PlusOp; MinusOp; MultOp; QuotOp; RemOp; + AndOp; OrOp; XorOp; ShiftLOp; ShiftROp] → + LTyBinOp op lty_int lty_int lty_int. + Proof. + iIntros (? v1 v2); iDestruct 1 as (i1) "->"; iDestruct 1 as (i2) "->". + repeat match goal with H : TCElemOf _ _ |- _ => inversion_clear H end; + rewrite /lty_car /=; eauto. + Qed. + Global Instance lty_bin_op_compare op : + TCElemOf op [LeOp; LtOp] → + LTyBinOp op lty_int lty_int lty_bool. + Proof. + iIntros (? v1 v2); iDestruct 1 as (i1) "->"; iDestruct 1 as (i2) "->". + repeat match goal with H : TCElemOf _ _ |- _ => inversion_clear H end; + rewrite /lty_car /=; eauto. + Qed. + Global Instance lty_bin_op_bool op : + TCElemOf op [AndOp; OrOp; XorOp] → + LTyBinOp op lty_bool lty_bool lty_bool. + Proof. + iIntros (? v1 v2); iDestruct 1 as (i1) "->"; iDestruct 1 as (i2) "->". + repeat match goal with H : TCElemOf _ _ |- _ => inversion_clear H end; + rewrite /lty_car /=; eauto. + Qed. + + (* The semantic typing rules *) + Lemma ltyped_var Γ (x : string) A : Γ !! x = Some A → Γ ⊨ x : A. + Proof. + iIntros (HΓx vs) "!# #HΓ /=". + iDestruct (env_ltyped_lookup with "HΓ") as (v ->) "HA"; first done. + by iApply wp_value. + Qed. + + Lemma ltyped_unit Γ : Γ ⊨ #() : (). + Proof. iIntros (vs) "!# _ /=". by iApply wp_value. Qed. + Lemma ltyped_bool Γ (b : bool) : Γ ⊨ #b : lty_bool. + Proof. iIntros (vs) "!# _ /=". iApply wp_value. rewrite /lty_car /=. eauto. Qed. + Lemma ltyped_nat Γ (n : Z) : Γ ⊨ #n : lty_int. + Proof. iIntros (vs) "!# _ /=". iApply wp_value. rewrite /lty_car /=. eauto. Qed. + + Lemma ltyped_rec Γ f x e A1 A2 : + (binder_insert f (A1 → A2)%lty (binder_insert x A1 Γ) ⊨ e : A2) -∗ + Γ ⊨ (rec: f x := e) : A1 → A2. + Proof. + iIntros "#H" (vs) "!# #HΓ /=". wp_pures. iLöb as "IH". + iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _). + iSpecialize ("H" $! (binder_insert f r (binder_insert x v vs)) with "[#]"). + { iApply (env_ltyped_insert with "IH"). by iApply env_ltyped_insert. } + destruct x as [|x], f as [|f]; rewrite /= -?subst_map_insert //. + destruct (decide (x = f)) as [->|]. + - by rewrite subst_subst delete_idemp insert_insert -subst_map_insert. + - rewrite subst_subst_ne // -subst_map_insert. + by rewrite -delete_insert_ne // -subst_map_insert. + Qed. + + Lemma ltyped_app Γ e1 e2 A1 A2 : + (Γ ⊨ e1 : A1 → A2) -∗ (Γ ⊨ e2 : A1) -∗ Γ ⊨ e1 e2 : A2. + Proof. + iIntros "#H1 #H2" (vs) "!# #HΓ /=". + iSpecialize ("H1" with "HΓ"). iSpecialize ("H2" with "HΓ"). + wp_apply (wp_wand with "H2"); iIntros (w) "HA1". + wp_apply (wp_wand with "H1"); iIntros (v) "#HA". by iApply "HA". + Qed. + + Lemma ltyped_fold Γ e (B : ltyC -n> ltyC) : + (Γ ⊨ e : B (lty_rec B)) -∗ Γ ⊨ e : lty_rec B. + Proof. + iIntros "#H" (vs) "!# #HΓ /=". iSpecialize ("H" with "HΓ"). + wp_apply (wp_wand with "H"); iIntros (w) "#HB". + by iEval (rewrite lty_rec_unfold /lty_car /=). + Qed. + Lemma ltyped_unfold Γ e (B : ltyC -n> ltyC) : + (Γ ⊨ e : lty_rec B) -∗ Γ ⊨ rec_unfold e : B (lty_rec B). + Proof. + iIntros "#H" (vs) "!# #HΓ /=". iSpecialize ("H" with "HΓ"). + wp_apply (wp_wand with "H"); iIntros (w) "HB". + iEval (rewrite lty_rec_unfold /lty_car /=) in "HB". by wp_lam. + Qed. + + Lemma ltyped_tlam Γ e C : (∀ A, Γ ⊨ e : C A) -∗ Γ ⊨ (λ: <>, e) : ∀ A, C A. + Proof. + iIntros "#H" (vs) "!# #HΓ /=". wp_pures. + iIntros "!#" (A) "/=". wp_pures. by iApply ("H" $! A). + Qed. + Lemma ltyped_tapp Γ e C A : (Γ ⊨ e : ∀ A, C A) -∗ Γ ⊨ e #() : C A. + Proof. + iIntros "#H" (vs) "!# #HΓ /=". iSpecialize ("H" with "HΓ"). + wp_apply (wp_wand with "H"); iIntros (w) "#HB". by iApply ("HB" $! A). + Qed. + + Lemma ltyped_pack Γ e C A : (Γ ⊨ e : C A) -∗ Γ ⊨ e : ∃ A, C A. + Proof. + iIntros "#H" (vs) "!# #HΓ /=". iSpecialize ("H" with "HΓ"). + wp_apply (wp_wand with "H"); iIntros (w) "#HB". by iExists A. + Qed. + Lemma ltyped_unpack Γ e1 e2 C B : + (Γ ⊨ e1 : ∃ A, C A) -∗ (∀ A, Γ ⊨ e2 : C A → B) -∗ Γ ⊨ e2 e1 : B. + Proof. + iIntros "#H1 #H2" (vs) "!# #HΓ /=". iSpecialize ("H1" with "HΓ"). + wp_apply (wp_wand with "H1"); iIntros (v); iDestruct 1 as (A) "#HC". + iSpecialize ("H2" $! A with "HΓ"). + wp_apply (wp_wand with "H2"); iIntros (w) "HCB". by iApply "HCB". + Qed. + + Lemma ltyped_pair Γ e1 e2 A1 A2 : + (Γ ⊨ e1 : A1) -∗ (Γ ⊨ e2 : A2) -∗ Γ ⊨ (e1,e2) : A1 * A2. + Proof. + iIntros "#H1 #H2" (vs) "!# #HΓ /=". + iSpecialize ("H1" with "HΓ"). iSpecialize ("H2" with "HΓ"). + wp_apply (wp_wand with "H2"); iIntros (w2) "#HA2". + wp_apply (wp_wand with "H1"); iIntros (w1) "#HA1". + wp_pures. iExists w1, w2. auto. + Qed. + Lemma ltyped_fst Γ e A1 A2 : (Γ ⊨ e : A1 * A2) -∗ Γ ⊨ Fst e : A1. + Proof. + iIntros "#H" (vs) "!# #HΓ /=". iSpecialize ("H" with "HΓ"). + wp_apply (wp_wand with "H"); iIntros (w). + iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures. + Qed. + Lemma ltyped_snd Γ e A1 A2 : (Γ ⊨ e : A1 * A2) -∗ Γ ⊨ Snd e : A2. + Proof. + iIntros "#H" (vs) "!# #HΓ /=". iSpecialize ("H" with "HΓ"). + wp_apply (wp_wand with "H"); iIntros (w). + iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures. + Qed. + + Lemma ltyped_injl Γ e A1 A2 : (Γ ⊨ e : A1) -∗ Γ ⊨ InjL e : A1 + A2. + Proof. + iIntros "#H" (vs) "!# HΓ /=". iSpecialize ("H" with "HΓ"). + wp_apply (wp_wand with "H"); iIntros (w) "#HA". + wp_pures. iLeft. iExists w. auto. + Qed. + Lemma ltyped_injr Γ e A1 A2 : (Γ ⊨ e : A2) -∗ Γ ⊨ InjR e : A1 + A2. + Proof. + iIntros "#H" (vs) "!# HΓ /=". iSpecialize ("H" with "HΓ"). + wp_apply (wp_wand with "H"); iIntros (w) "#HA". + wp_pures. iRight. iExists w. auto. + Qed. + Lemma ltyped_case Γ e e1 e2 A1 A2 B : + (Γ ⊨ e : A1 + A2) -∗ (Γ ⊨ e1 : A1 → B) -∗ (Γ ⊨ e2 : A2 → B) -∗ + Γ ⊨ Case e e1 e2 : B. + Proof. + iIntros "#H #H1 #H2" (vs) "!# #HΓ /=". iSpecialize ("H" with "HΓ"). + iSpecialize ("H1" with "HΓ"). iSpecialize ("H2" with "HΓ"). + wp_apply (wp_wand with "H"); iIntros (w) "#[HA|HA]". + - iDestruct "HA" as (w1 ->) "HA". wp_pures. + wp_apply (wp_wand with "H1"); iIntros (v) "#HAB". by iApply "HAB". + - iDestruct "HA" as (w2 ->) "HA". wp_pures. + wp_apply (wp_wand with "H2"); iIntros (v) "#HAB". by iApply "HAB". + Qed. + + Lemma ltyped_un_op Γ e op A B : + LTyUnOp op A B → (Γ ⊨ e : A) -∗ Γ ⊨ UnOp op e : B. + Proof. + intros ?. iIntros "#H" (vs) "!# #HΓ /=". iSpecialize ("H" with "HΓ"). + wp_apply (wp_wand with "H"); iIntros (v) "#HA". + iDestruct (lty_un_op with "HA") as (w ?) "#HB". by wp_unop. + Qed. + Lemma ltyped_bin_op Γ e1 e2 op A1 A2 B : + LTyBinOp op A1 A2 B → (Γ ⊨ e1 : A1) -∗ (Γ ⊨ e2 : A2) -∗ Γ ⊨ BinOp op e1 e2 : B. + Proof. + intros. iIntros "#H1 #H2" (vs) "!# #HΓ /=". + iSpecialize ("H1" with "HΓ"). iSpecialize ("H2" with "HΓ"). + wp_apply (wp_wand with "H2"); iIntros (v2) "#HA2". + wp_apply (wp_wand with "H1"); iIntros (v1) "#HA1". + iDestruct (lty_bin_op with "HA1 HA2") as (w ?) "#HB". by wp_binop. + Qed. + + Lemma ltyped_if Γ e e1 e2 B : + (Γ ⊨ e : lty_bool) -∗ (Γ ⊨ e1 : B) -∗ (Γ ⊨ e2 : B) -∗ + Γ ⊨ (if: e then e1 else e2) : B. + Proof. + iIntros "#H #H1 #H2" (vs) "!# #HΓ /=". iSpecialize ("H" with "HΓ"). + iSpecialize ("H1" with "HΓ"). iSpecialize ("H2" with "HΓ"). + wp_apply (wp_wand with "H"); iIntros (w). iDestruct 1 as ([]) "->"; by wp_if. + Qed. + + Lemma ltyped_fork Γ e : (Γ ⊨ e : ()) -∗ Γ ⊨ Fork e : (). + Proof. + iIntros "#H" (vs) "!# #HΓ /=". iSpecialize ("H" with "HΓ"). + wp_apply wp_fork; last done. by iApply (wp_wand with "H"). + Qed. + + Lemma ltyped_alloc Γ e A : (Γ ⊨ e : A) -∗ Γ ⊨ ref e : ref A. + Proof. + iIntros "#H" (vs) "!# #HΓ /=". iSpecialize ("H" with "HΓ"). + wp_bind (subst_map _ e). iApply (wp_wand with "H"); iIntros (w) "HA". + iApply wp_fupd. wp_alloc l as "Hl". + iMod (inv_alloc (tyN .@ l) _ (∃ v, l ↦ v ∗ A v)%I with "[Hl HA]") as "#?". + { iExists w. iFrame. } + iModIntro. iExists l; auto. + Qed. + Lemma ltyped_load Γ e A : (Γ ⊨ e : ref A) -∗ Γ ⊨ ! e : A. + Proof. + iIntros "#H" (vs) "!# #HΓ /=". iSpecialize ("H" with "HΓ"). + wp_bind (subst_map _ e). iApply (wp_wand with "H"); iIntros (w). + iDestruct 1 as (l ->) "#?". + iInv (tyN.@l) as (v) "[>Hl HA]". wp_load. eauto 10. + Qed. + Lemma ltyped_store Γ e1 e2 A : + (Γ ⊨ e1 : ref A) -∗ (Γ ⊨ e2 : A) -∗ Γ ⊨ (e1 <- e2) : (). + Proof. + iIntros "#H1 #H2" (vs) "!# #HΓ /=". + iSpecialize ("H1" with "HΓ"). iSpecialize ("H2" with "HΓ"). + wp_apply (wp_wand with "H2"); iIntros (w2) "#HA". + wp_apply (wp_wand with "H1"); iIntros (w1); iDestruct 1 as (l ->) "#?". + iInv (tyN.@l) as (v) "[>Hl _]". wp_store. eauto 10. + Qed. + Lemma ltyped_faa Γ e1 e2 : + (Γ ⊨ e1 : ref lty_int) -∗ (Γ ⊨ e2 : lty_int) -∗ Γ ⊨ FAA e1 e2 : lty_int. + Proof. + iIntros "#H1 #H2" (vs) "!# #HΓ /=". + iSpecialize ("H1" with "HΓ"). iSpecialize ("H2" with "HΓ"). + wp_apply (wp_wand with "H2"); iIntros (w2); iDestruct 1 as (n) "->". + wp_apply (wp_wand with "H1"); iIntros (w1); iDestruct 1 as (l ->) "#?". + iInv (tyN.@l) as (v) "[>Hl Hv]"; iDestruct "Hv" as (n') "> ->". + wp_faa. iModIntro. eauto 10. + Qed. + Lemma ltyped_cas Γ A e1 e2 e3 : + LTyUnboxed A → + (Γ ⊨ e1 : ref A) -∗ (Γ ⊨ e2 : A) -∗ (Γ ⊨ e3 : A) -∗ Γ ⊨ CAS e1 e2 e3 : lty_bool. + Proof. + intros. iIntros "#H1 #H2 #H3" (vs) "!# #HΓ /=". iSpecialize ("H1" with "HΓ"). + iSpecialize ("H2" with "HΓ"). iSpecialize ("H3" with "HΓ"). + wp_apply (wp_wand with "H3"); iIntros (w3) "HA3". + wp_apply (wp_wand with "H2"); iIntros (w2) "HA2". + iDestruct (lty_unboxed with "HA2") as %?. + wp_apply (wp_wand with "H1"); iIntros (w1); iDestruct 1 as (l ->) "#?". + iInv (tyN.@l) as (v) "[>Hl Hv]". + destruct (decide (v = w2)) as [->|]. + - wp_cas_suc. eauto 10. + - wp_cas_fail. eauto 10. + Qed. +End types_properties. diff --git a/theories/logrel_heaplang/ltyping_safety.v b/theories/logrel_heaplang/ltyping_safety.v new file mode 100644 index 0000000000000000000000000000000000000000..9e163e8f6decdc9aa2f57550e580507c5b25dacb --- /dev/null +++ b/theories/logrel_heaplang/ltyping_safety.v @@ -0,0 +1,17 @@ +From iris_examples.logrel_heaplang Require Export ltyping. +From iris.heap_lang Require Import adequacy. +From iris.heap_lang Require Import proofmode. + +Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' : + (∀ `{heapG Σ}, ∃ A, ∅ ⊨ e : A) → + rtc erased_step ([e], σ) (es, σ') → e' ∈ es → + is_Some (to_val e') ∨ reducible e' σ'. +Proof. + intros Hty. apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ?. + destruct (Hty _) as [A He]. iStartProof. iDestruct (He $! ∅) as "#He". + iSpecialize ("He" with "[]"). + { iSplit. + - iPureIntro=> x. rewrite !lookup_empty -!not_eq_None_Some. by naive_solver. + - by rewrite map_zip_with_empty. } + rewrite subst_map_empty. iApply (wp_wand with "He"); auto. +Qed.