Commit 243b7000 authored by Robbert Krebbers's avatar Robbert Krebbers

Start introducing notations for typing judgments.

parent 63eda220
......@@ -15,14 +15,16 @@ Section typed_interp.
Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
Lemma typed_interp (Δ : varC -n> valC -n> iProp lang Σ) Γ vs e τ
(Htyped : typed Γ e τ) (HΔ : x v, PersistentP (Δ x v)) :
(HΔ : x v, PersistentP (Δ x v)) :
Γ ⊢ₜ e : τ
length Γ = length vs
[] zip_with (λ τ, interp τ Δ) Γ vs WP e.[env_subst vs] {{ interp τ Δ }}.
Proof.
revert Δ HΔ vs. induction Htyped; iIntros {Δ HΔ vs Hlen} "#HΓ"; cbn.
intros Htyped. revert Δ HΔ vs.
induction Htyped; iIntros {Δ HΔ vs Hlen} "#HΓ"; cbn.
- (* var *)
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
rewrite /env_subst Hv; value_case.
iApply (big_and_elem_of with "HΓ").
apply elem_of_list_lookup_2 with x.
......
......@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
Section Soundness.
Definition Σ := #[].
Let Σ := #[].
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof. change (env_subst []) with (@ids expr _). by asimpl. Qed.
......@@ -12,14 +12,14 @@ Section Soundness.
λne x y, True%I.
Lemma wp_soundness e τ :
typed [] e τ True WP e {{ @interp (globalF Σ) τ free_type_context }}.
[] ⊢ₜ e : τ True WP e {{ @interp (globalF Σ) τ free_type_context }}.
Proof.
iIntros {H} "". rewrite -(empty_env_subst e).
by iApply (@typed_interp _ _ _ []).
Qed.
Theorem Soundness e τ :
typed [] e τ
[] ⊢ₜ e : τ
e' thp, rtc step ([e], tt) (e' :: thp, tt)
¬ reducible e' tt is_Some (to_val e').
Proof.
......
From iris_logrel.F_mu Require Export lang.
Inductive type :=
| TUnit : type
| TProd : type type type
| TSum : type type type
| TArrow : type type type
| TRec (τ : {bind 1 of type})
| TVar (x : var)
| TForall (τ : {bind 1 of type}).
| TUnit : type
| TProd : type type type
| TSum : type type type
| TArrow : type type type
| TRec (τ : {bind 1 of type})
| TVar (x : var)
| TForall (τ : {bind 1 of type}).
Instance Ids_type : Ids type. derive. Defined.
Instance Rename_type : Rename type. derive. Defined.
Instance Subst_type : Subst type. derive. Defined.
Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
Inductive typed (Γ : list type) : expr type Prop :=
| Var_typed x τ : Γ !! x = Some τ typed Γ (Var x) τ
| Unit_typed : typed Γ Unit TUnit
| Pair_typed e1 e2 τ1 τ2 :
typed Γ e1 τ1 typed Γ e2 τ2 typed Γ (Pair e1 e2) (TProd τ1 τ2)
| Fst_typed e τ1 τ2 : typed Γ e (TProd τ1 τ2) typed Γ (Fst e) τ1
| Snd_typed e τ1 τ2 : typed Γ e (TProd τ1 τ2) typed Γ (Snd e) τ2
| InjL_typed e τ1 τ2 : typed Γ e τ1 typed Γ (InjL e) (TSum τ1 τ2)
| InjR_typed e τ1 τ2 : typed Γ e τ2 typed Γ (InjR e) (TSum τ1 τ2)
| Case_typed e0 e1 e2 τ1 τ2 ρ :
typed Γ e0 (TSum τ1 τ2)
typed (τ1 :: Γ) e1 ρ typed (τ2 :: Γ) e2 ρ
typed Γ (Case e0 e1 e2) ρ
| Lam_typed e τ1 τ2 :
typed (τ1 :: Γ) e τ2 typed Γ (Lam e) (TArrow τ1 τ2)
| App_typed e1 e2 τ1 τ2 :
typed Γ e1 (TArrow τ1 τ2) typed Γ e2 τ1 typed Γ (App e1 e2) τ2
| TLam_typed e τ :
typed (map (λ t, t.[ren (+1)]) Γ) e τ
typed Γ (TLam e) (TForall τ)
| TApp_typed e τ τ':
typed Γ e (TForall τ) typed Γ (TApp e) (τ.[τ'/])
| TFold e τ :
typed (map (λ t, t.[ren (+1)]) Γ) e τ
typed Γ (Fold e) (TRec τ)
| TUnfold e τ : typed Γ e (TRec τ) typed Γ (Unfold e) (τ.[(TRec τ)/])
.
| Var_typed x τ : Γ !! x = Some τ Γ ⊢ₜ Var x : τ
| Unit_typed : Γ ⊢ₜ Unit : TUnit
| Pair_typed e1 e2 τ1 τ2 :
Γ ⊢ₜ e1 : τ1 Γ ⊢ₜ e2 : τ2 Γ ⊢ₜ Pair e1 e2 : TProd τ1 τ2
| Fst_typed e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 Γ ⊢ₜ Fst e : τ1
| Snd_typed e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 Γ ⊢ₜ Snd e : τ2
| InjL_typed e τ1 τ2 : Γ ⊢ₜ e : τ1 Γ ⊢ₜ InjL e : TSum τ1 τ2
| InjR_typed e τ1 τ2 : Γ ⊢ₜ e : τ2 Γ ⊢ₜ InjR e : TSum τ1 τ2
| Case_typed e0 e1 e2 τ1 τ2 ρ :
Γ ⊢ₜ e0 : TSum τ1 τ2 τ1 :: Γ ⊢ₜ e1 : ρ τ2 :: Γ ⊢ₜ e2 : ρ
Γ ⊢ₜ Case e0 e1 e2 : ρ
| Lam_typed e τ1 τ2 : τ1 :: Γ ⊢ₜ e : τ2 Γ ⊢ₜ Lam e : TArrow τ1 τ2
| App_typed e1 e2 τ1 τ2 : Γ ⊢ₜ e1 : TArrow τ1 τ2 Γ ⊢ₜ e2 : τ1 Γ ⊢ₜ App e1 e2 : τ2
| TLam_typed e τ : map (λ t, t.[ren (+1)]) Γ ⊢ₜ e : τ Γ ⊢ₜ TLam e : TForall τ
| TApp_typed e τ τ' : Γ ⊢ₜ e : TForall τ Γ ⊢ₜ TApp e : τ.[τ'/]
| TFold e τ : map (λ t, t.[ren (+1)]) Γ ⊢ₜ e : τ Γ ⊢ₜ Fold e : TRec τ
| TUnfold e τ : Γ ⊢ₜ e : TRec τ Γ ⊢ₜ Unfold e : τ.[TRec τ/]
where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
Local Hint Extern 1 =>
match goal with [H : context [length (map _ _)] |- _] => rewrite map_length in H end
: typed_subst_invariant.
match goal with
| H : context [length (map _ _)] |- _ => rewrite map_length in H
end : typed_subst_invariant.
Lemma typed_subst_invariant Γ e τ s1 s2 :
typed Γ e τ ( x, x < length Γ s1 x = s2 x) e.[s1] = e.[s2].
Γ ⊢ₜ e : τ ( x, x < length Γ s1 x = s2 x) e.[s1] = e.[s2].
Proof.
intros Htyped; revert s1 s2.
assert ( {A} `{Ids A} `{Rename A}
......@@ -60,21 +55,21 @@ Definition env_subst (vs : list val) (x : var) : expr :=
from_option id (Var x) (of_val <$> vs !! x).
Lemma typed_subst_head_simpl Δ τ e w ws :
typed Δ e τ -> length Δ = S (length ws)
Δ ⊢ₜ e : τ length Δ = S (length ws)
e.[# w .: env_subst ws] = e.[env_subst (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' Hv]; first omega; simpl.
by rewrite Hv.
by rewrite Hv.
Qed.
Local Opaque eq_nat_dec.
Lemma iter_up_subst_type (m : nat) (τ : type) (x : var) :
(iter m up (τ .: ids) x) =
iter m up (τ .: ids) x =
if lt_dec x m then ids x else
if eq_nat_dec x m then τ.[ren (+m)] else ids (x - 1).
if eq_nat_dec x m then τ.[ren (+m)] else ids (x - 1).
Proof.
revert x τ.
induction m; intros x τ; cbn.
......@@ -86,4 +81,4 @@ Proof.
rewrite IHm.
repeat destruct lt_dec; repeat destruct eq_nat_dec;
asimpl; auto with omega.
Qed.
\ No newline at end of file
Qed.
......@@ -16,22 +16,22 @@ Section typed_interp.
Lemma typed_interp N (Δ : varC -n> valC -n> iPropG lang Σ) Γ vs e τ
(HNLdisj : l : loc, N L .@ l)
(Htyped : typed Γ e τ)
(HΔ : x v, PersistentP (Δ x v)) :
Γ ⊢ₜ e : τ
length Γ = length vs
heap_ctx N [] zip_with (λ τ, interp L τ Δ) Γ vs
WP e.[env_subst vs] {{ interp L τ Δ }}.
Proof.
revert Δ HΔ vs.
induction Htyped; intros Δ HΔ vs Hlen; iIntros "#[Hheap HΓ]"; cbn.
intros Htyped; revert Δ HΔ vs.
induction Htyped; iIntros {Δ HΔ vs Hlen} "#[Hheap HΓ] /=".
- (* var *)
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
rewrite /env_subst Hv; value_case.
iApply (big_and_elem_of with "HΓ").
apply elem_of_list_lookup_2 with x.
rewrite lookup_zip_with; simplify_option_eq; trivial.
- (* unit *) value_case; trivial.
by rewrite lookup_zip_with; simplify_option_eq.
- (* unit *) by value_case.
- (* pair *)
smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHHtyped1.
smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2.
......@@ -117,7 +117,7 @@ Section typed_interp.
iInv (L .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial.
specialize (HNLdisj l); set_solver_ndisj.
iFrame "Hw1". iIntros "> Hw1". iPvsIntro. iSplitL; eauto.
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Γ".
......@@ -128,8 +128,7 @@ Section typed_interp.
eapply bool_decide_spec; eauto using to_of_val.
iApply (wp_store N); auto using to_of_val.
specialize (HNLdisj l); set_solver_ndisj.
iFrame "Hheap Hz1".
iIntros "> Hz1". iPvsIntro.
iSplitL; [|iPvsIntro; trivial]. eauto.
iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro.
iSplitL; eauto 10.
Qed.
End typed_interp.
From iris_logrel.F_mu_ref Require Export fundamental.
From iris.proofmode Require Import tactics pviewshifts.
From iris.program_logic Require Import adequacy.
From iris.program_logic Require Import ownership adequacy.
Section Soundness.
Definition Σ := #[ auth.authGF heapUR ].
......@@ -12,8 +12,8 @@ Section Soundness.
λne x y, True%I.
Lemma wp_soundness e τ :
typed [] e τ
ownership.ownP WP e {{ v, H : heapG Σ,
[] ⊢ₜ e : τ
ownP WP e {{ v, H : heapG Σ,
interp (nroot .@ "Fμ,ref" .@ 1) τ free_type_context v}}.
Proof.
iIntros {H1} "Hemp".
......@@ -30,7 +30,7 @@ Section Soundness.
Local Arguments of_heap : simpl never.
Theorem Soundness e τ :
typed [] e τ
[] ⊢ₜ e : τ
e' thp h, rtc step ([e], (of_heap )) (e' :: thp, h)
¬ reducible e' h is_Some (to_val e').
Proof.
......
From iris_logrel.F_mu_ref Require Export lang.
Inductive type :=
| TUnit : type
| TProd : type type type
| TSum : type type type
| TArrow : type type type
| TRec (τ : {bind 1 of type})
| TVar (x : var)
| TForall (τ : {bind 1 of type})
| Tref (τ : type)
.
| TUnit : type
| TProd : type type type
| TSum : type type type
| TArrow : type type type
| TRec (τ : {bind 1 of type})
| TVar (x : var)
| TForall (τ : {bind 1 of type})
| Tref (τ : type).
Instance Ids_type : Ids type. derive. Defined.
Instance Rename_type : Rename type. derive. Defined.
Instance Subst_type : Subst type. derive. Defined.
Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
Inductive typed (Γ : list type) : expr type Prop :=
| Var_typed x τ : Γ !! x = Some τ typed Γ (Var x) τ
| Unit_typed : typed Γ Unit TUnit
| Pair_typed e1 e2 τ1 τ2 :
typed Γ e1 τ1 typed Γ e2 τ2 typed Γ (Pair e1 e2) (TProd τ1 τ2)
| Fst_typed e τ1 τ2 : typed Γ e (TProd τ1 τ2) typed Γ (Fst e) τ1
| Snd_typed e τ1 τ2 : typed Γ e (TProd τ1 τ2) typed Γ (Snd e) τ2
| InjL_typed e τ1 τ2 : typed Γ e τ1 typed Γ (InjL e) (TSum τ1 τ2)
| InjR_typed e τ1 τ2 : typed Γ e τ2 typed Γ (InjR e) (TSum τ1 τ2)
| Case_typed e0 e1 e2 τ1 τ2 ρ :
typed Γ e0 (TSum τ1 τ2)
typed (τ1 :: Γ) e1 ρ typed (τ2 :: Γ) e2 ρ
typed Γ (Case e0 e1 e2) ρ
| Lam_typed e τ1 τ2 :
typed (τ1 :: Γ) e τ2 typed Γ (Lam e) (TArrow τ1 τ2)
| App_typed e1 e2 τ1 τ2 :
typed Γ e1 (TArrow τ1 τ2) typed Γ e2 τ1 typed Γ (App e1 e2) τ2
| TLam_typed e τ :
typed (map (λ t, t.[ren (+1)]) Γ) e τ
typed Γ (TLam e) (TForall τ)
| TApp_typed e τ τ':
typed Γ e (TForall τ) typed Γ (TApp e) (τ.[τ'/])
| TFold e τ :
typed (map (λ t, t.[ren (+1)]) Γ) e τ
typed Γ (Fold e) (TRec τ)
| TUnfold e τ : typed Γ e (TRec τ) typed Γ (Unfold e) (τ.[(TRec τ)/])
| TAlloc e τ : typed Γ e τ typed Γ (Alloc e) (Tref τ)
| TLoad e τ : typed Γ e (Tref τ) typed Γ (Load e) τ
| TStore e e' τ :
typed Γ e (Tref τ) typed Γ e' τ typed Γ (Store e e') TUnit
.
| Var_typed x τ : Γ !! x = Some τ Γ ⊢ₜ Var x : τ
| Unit_typed : Γ ⊢ₜ Unit : TUnit
| Pair_typed e1 e2 τ1 τ2 :
Γ ⊢ₜ e1 : τ1 Γ ⊢ₜ e2 : τ2 Γ ⊢ₜ Pair e1 e2 : TProd τ1 τ2
| Fst_typed e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 Γ ⊢ₜ Fst e : τ1
| Snd_typed e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 Γ ⊢ₜ Snd e : τ2
| InjL_typed e τ1 τ2 : Γ ⊢ₜ e : τ1 Γ ⊢ₜ InjL e : TSum τ1 τ2
| InjR_typed e τ1 τ2 : Γ ⊢ₜ e : τ2 Γ ⊢ₜ InjR e : TSum τ1 τ2
| Case_typed e0 e1 e2 τ1 τ2 ρ :
Γ ⊢ₜ e0 : TSum τ1 τ2 τ1 :: Γ ⊢ₜ e1 : ρ τ2 :: Γ ⊢ₜ e2 : ρ
Γ ⊢ₜ Case e0 e1 e2 : ρ
| Lam_typed e τ1 τ2 : τ1 :: Γ ⊢ₜ e : τ2 Γ ⊢ₜ Lam e : TArrow τ1 τ2
| App_typed e1 e2 τ1 τ2 :
Γ ⊢ₜ e1 : TArrow τ1 τ2 Γ ⊢ₜ e2 : τ1 Γ ⊢ₜ App e1 e2 : τ2
| TLam_typed e τ :
map (λ t : type, t.[ren (+1)]) Γ ⊢ₜ e : τ Γ ⊢ₜ TLam e : TForall τ
| TApp_typed e τ τ' : Γ ⊢ₜ e : TForall τ Γ ⊢ₜ TApp e : τ.[τ'/]
| TFold e τ : map (λ t, t.[ren (+1)]) Γ ⊢ₜ e : τ Γ ⊢ₜ Fold e : TRec τ
| TUnfold e τ : Γ ⊢ₜ e : TRec τ Γ ⊢ₜ Unfold e : τ.[TRec τ/]
| TAlloc e τ : Γ ⊢ₜ e : τ Γ ⊢ₜ Alloc e : Tref τ
| TLoad e τ : Γ ⊢ₜ e : Tref τ Γ ⊢ₜ Load e : τ
| TStore e e' τ : Γ ⊢ₜ e : Tref τ Γ ⊢ₜ e' : τ Γ ⊢ₜ Store e e' : TUnit
where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
Local Hint Extern 1 =>
match goal with [H : context [length (map _ _)] |- _] => rewrite map_length in H end
: typed_subst_invariant.
match goal with
| H : context [length (map _ _)] |- _ => rewrite map_length in H
end : typed_subst_invariant.
Lemma typed_subst_invariant Γ e τ s1 s2 :
typed Γ e τ ( x, x < length Γ s1 x = s2 x) e.[s1] = e.[s2].
Γ ⊢ₜ e : τ ( x, x < length Γ s1 x = s2 x) e.[s1] = e.[s2].
Proof.
intros Htyped; revert s1 s2.
assert ( {A} `{Ids A} `{Rename A}
......@@ -66,7 +61,7 @@ Definition env_subst (vs : list val) (x : var) : expr :=
from_option id (Var x) (of_val <$> vs !! x).
Lemma typed_subst_head_simpl Δ τ e w ws :
typed Δ e τ length Δ = S (length ws)
Δ ⊢ₜ e : τ length Δ = S (length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
intros H1 H2.
......@@ -78,8 +73,8 @@ Qed.
Local Opaque eq_nat_dec.
Lemma iter_up_subst_type (m : nat) (τ : type) (x : var) :
(iter m up (τ .: ids) x) =
if lt_dec x m then ids x else
iter m up (τ .: ids) x =
if lt_dec x m then ids x else
if eq_nat_dec x m then τ.[ren (+m)] else ids (x - 1).
Proof.
revert x τ.
......
From iris_logrel.F_mu_ref_par Require Export fundamental_binary.
Inductive context_item : Type :=
| 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)
(* Nat bin op *)
| CTX_BinOpL (op : binop) (e2 : expr)
| CTX_BinOpR (op : binop) (e1 : expr)
(* If *)
| CTX_IfL (e1 : expr) (e2 : expr)
| CTX_IfM (e0 : expr) (e2 : expr)
| CTX_IfR (e0 : expr) (e1 : expr)
(* Recursive Types *)
| CTX_Fold
| CTX_Unfold
(* Polymorphic Types *)
| CTX_TLam
| CTX_TApp
(* Concurrency *)
| CTX_Fork
(* Reference Types *)
| CTX_Alloc
| CTX_Load
| CTX_StoreL (e2 : expr)
| CTX_StoreR (e1 : expr)
(* Compare and swap used for fine-grained concurrency *)
| CTX_CAS_L (e1 : expr) (e2 : expr)
| CTX_CAS_M (e0 : expr) (e2 : expr)
| CTX_CAS_R (e0 : expr) (e1 : expr).
Inductive context_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)
(* Nat bin op *)
| CTX_BinOpL (op : binop) (e2 : expr)
| CTX_BinOpR (op : binop) (e1 : expr)
(* If *)
| CTX_IfL (e1 : expr) (e2 : expr)
| CTX_IfM (e0 : expr) (e2 : expr)
| CTX_IfR (e0 : expr) (e1 : expr)
(* Recursive Types *)
| CTX_Fold
| CTX_Unfold
(* Polymorphic Types *)
| CTX_TLam
| CTX_TApp
(* Concurrency *)
| CTX_Fork
(* Reference Types *)
| CTX_Alloc
| CTX_Load
| CTX_StoreL (e2 : expr)
| CTX_StoreR (e1 : expr)
(* Compare and swap used for fine-grained concurrency *)
| CTX_CAS_L (e1 : expr) (e2 : expr)
| CTX_CAS_M (e0 : expr) (e2 : expr)
| CTX_CAS_R (e0 : expr) (e1 : expr).
Fixpoint fill_ctx_item (ctx : context_item) (e : expr) : expr :=
match ctx with
......@@ -81,7 +81,7 @@ Local Open Scope bin_logrel_scope.
(** typed context *)
Inductive typed_context_item :
context_item (list type) type (list type) type Prop :=
context_item list type type list type type Prop :=
| TP_CTX_Lam : Γ τ τ',
typed_context_item CTX_Lam (TArrow τ τ' :: τ :: Γ) τ' Γ (TArrow τ τ')
| TP_CTX_AppL (e2 : expr) : Γ τ τ',
......@@ -165,7 +165,7 @@ Lemma typed_context_item_typed k Γ τ Γ' τ' e :
Proof. intros H1 H2; induction H2; simpl; eauto using typed. Qed.
Inductive typed_context :
context (list type) type (list type) type Prop :=
context list type type list type type Prop :=
| TPCTX_nil : Γ τ, typed_context nil Γ τ Γ τ
| TPCTX_cons : Γ1 τ1 Γ2 τ2 Γ3 τ3 k K,
typed_context_item k Γ2 τ2 Γ3 τ3
......
......@@ -82,8 +82,7 @@ Section typed_interp.
iIntros {vs Hlen ρ j K} "(#Hheap & #Hspec & #HΓ & Htr)"; cbn.
smart_wp_bind (SndCtx) v v' "[Hv #Hiv]"
(IHHtyped _ _ _ j (K ++ [SndCtx])); cbn.
iDestruct "Hiv" as {w1 w2} "#[% [Hiv2 Hiv3]]".
inversion H; subst.
iDestruct "Hiv" as {w1 w2} "#[% [Hiv2 Hiv3]]"; simplify_eq.
iPvs (step_snd _ _ _ j K (# (w2.1)) (w2.1) (# (w2.2)) (w2.2)
_ _ _ with "* [-]") as "Hw".
iFrame "Hspec Hv"; trivial.
......@@ -458,10 +457,10 @@ Section typed_interp.
Unshelve. all: eauto using to_of_val. all: SolveDisj 3 l.
Qed.
Lemma typed_binary_interp Δ Γ e τ {HΔ : x vw, PersistentP (Δ x vw)}
(Htyped : typed Γ e τ) : Δ Γ e log e τ.
Lemma typed_binary_interp Δ Γ e τ {HΔ : x vw, PersistentP (Δ x vw)} :
Γ ⊢ₜ e : τ Δ Γ e log e τ.
Proof.
revert Δ HΔ; induction Htyped; intros Δ HΔ.
intros Htyped; revert Δ HΔ; induction Htyped; intros Δ HΔ.
- iIntros {vs Hlen ρ j K} "(#Hheap & #Hspec & #HΓ & Htr) /=".
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
......
......@@ -4,7 +4,7 @@ From iris.algebra Require Export upred_big_op.
From iris.proofmode Require Import tactics pviewshifts invariants.
Section typed_interp.
Context {Σ : gFunctors} `{i : heapIG Σ} `{L : namespace}.
Context {Σ : gFunctors} `{i : heapIG Σ} {L : namespace}.
Implicit Types P Q R : iPropG lang Σ.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
......@@ -15,14 +15,14 @@ Section typed_interp.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
Lemma typed_interp N (Δ : varC -n> valC -n> iPropG lang Σ) Γ vs e τ
(HNLdisj : l : loc, N L .@ l)
(Htyped : typed Γ e τ) (HΔ : x v, PersistentP (Δ x v)) :
(HNLdisj : l : loc, N L .@ l) (HΔ : x v, PersistentP (Δ x v)) :
Γ ⊢ₜ e : τ
length Γ = length vs
heapI_ctx N [] zip_with (λ τ, interp L τ Δ) Γ vs
WP e.[env_subst vs] {{ interp L τ Δ }}.
heapI_ctx N [] zip_with (λ τ, interp L τ Δ) Γ vs
WP e.[env_subst vs] {{ interp L τ Δ }}.
Proof.
revert Δ HΔ vs.
induction Htyped; iIntros {Δ HΔ vs Hlen} "#[Hheap HΓ]"; cbn.
intros Htyped; revert Δ HΔ vs.
induction Htyped; iIntros {Δ HΔ vs Hlen} "#[Hheap HΓ] /=".
- (* var *)
destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
{ by rewrite -Hlen; apply lookup_lt_Some with τ. }
......@@ -147,8 +147,7 @@ Section typed_interp.
eapply bool_decide_spec; eauto using to_of_val.
iApply (wp_store N); auto using to_of_val.
specialize (HNLdisj l); set_solver_ndisj.
iFrame "Hheap Hz1".
iIntros "> Hz1". iPvsIntro. iSplitL; [|iPvsIntro; trivial]; eauto.
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.
......@@ -166,6 +165,6 @@ Section typed_interp.
clear Hneq. specialize (HNLdisj l); set_solver_ndisj.
(* Weird that Hneq above makes set_solver_ndisj diverge or
take exceptionally long!?!? *)
iIntros "{$Hheap $Hw1} > Hw1". iPvsIntro. iSplitL; [|iPvsIntro]; eauto.
iIntros "{$Hheap $Hw1} > Hw1". iPvsIntro. iSplitL; eauto.
Qed.
End typed_interp.
......@@ -2,12 +2,10 @@ From iris_logrel.F_mu_ref_par Require Export context_refinement.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Import ownership auth.
From iris.proofmode Require Import tactics pviewshifts invariants.
From iris.program_logic Require Import adequacy.
From iris.program_logic Require Import ownership adequacy.
Section Soundness.
Context {Σ : gFunctors}
{Hhp : auth.authG lang Σ heapUR}
{Hcfg : auth.authG lang Σ cfgUR}.
Context `{Hhp : authG lang Σ heapUR, Hcfg : authG lang Σ cfgUR}.
Definition free_type_context : varC -n> bivalC -n> iPropG lang Σ := λne x y,
True%I.
......@@ -18,8 +16,8 @@ Section Soundness.
Lemma wp_basic_soundness e e' τ :
( H H' N Δ HΔ, @bin_log_related Σ H H' N Δ [] e e' τ HΔ)
@ownership.ownP lang (globalF Σ)
WP e {{_, ( thp' h v, rtc step ([e'], ) ((# v) :: thp', h)) }}.
@ownP lang (globalF Σ)
WP e {{ _, ( thp' h v, rtc step ([e'], ) (# v :: thp', h)) }}.
Proof.
iIntros {H1} "Hemp".
iPvs (heap_alloc (nroot .@ "Fμ,ref,par" .@ 2) _ _ _ _ with "Hemp")
......
From iris_logrel.F_mu_ref_par Require Export fundamental_unary.
From iris.proofmode Require Import tactics pviewshifts.
From iris.program_logic Require Import adequacy.
From iris.program_logic Require Import ownership adequacy.
Section Soundness.
Definition Σ := #[ auth.authGF heapUR ].
Let Σ := #[ auth.authGF heapUR ].