Commit 09ef8477 authored by Robbert Krebbers's avatar Robbert Krebbers

Use λne notation and many clean ups.

parent 655c9011
......@@ -17,13 +17,11 @@ 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))
: List.length Γ = List.length vs
[] zip_with (λ τ, interp τ Δ) Γ vs WP e.[env_subst vs] {{ interp τ Δ }}.
(Htyped : typed Γ e τ) (HΔ : x v, PersistentP (Δ x v)) :
List.length Γ = List.length vs
[] zip_with (λ τ, interp τ Δ) Γ vs WP e.[env_subst vs] {{ interp τ Δ }}.
Proof.
revert Δ HΔ vs.
induction Htyped; intros Δ HΔ vs Hlen; iIntros "#HΓ"; cbn.
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 τ. }
......@@ -72,14 +70,13 @@ Section typed_interp.
iApply wp_mono; [|iApply "Hv"]; auto.
- (* TLam *)
value_case.
iIntros { [τi τiPr] } "!". iApply wp_TLam; iNext; simpl in *.
iIntros { τi } "! %". iApply wp_TLam; iNext; simpl in *.
iApply (IHHtyped (extend_context_interp_fun1 τi Δ)); [rewrite map_length|]; trivial.
by iDestruct (zip_with_context_interp_subst with "HΓ") as "?".
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
unshelve iSpecialize ("Hv" $! ((interp τ' Δ) _)); try apply _; cbn.
iApply always_elim. iApply always_mono; [|trivial].
apply wp_mono => w. by rewrite interp_subst.
iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (interp τ' Δ)); iPureIntro; apply _|].
iIntros{w} "?". by rewrite interp_subst.
- (* Fold *)
rewrite map_length in IHHtyped.
iApply (@wp_bind _ _ _ [FoldCtx]).
......
This diff is collapsed.
......@@ -18,17 +18,10 @@ Section Soundness.
Qed.
Definition free_type_context : varC -n> valC -n> iProp lang (globalF Σ) :=
{|
cofe_mor_car :=
λ x,
{|
cofe_mor_car :=
λ y, True%I
|}
|}.
λne x y, True%I.
Lemma wp_soundness e τ
: typed [] e τ True WP e {{ @interp (globalF Σ) τ free_type_context}}.
Lemma wp_soundness e τ :
typed [] e τ True WP e {{ @interp (globalF Σ) τ free_type_context }}.
Proof.
iIntros {H} "". rewrite -(empty_env_subst e).
by iApply (@typed_interp _ _ _ []).
......
......@@ -23,12 +23,12 @@ 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))
: List.length Γ = List.length vs
heap_ctx N [] zip_with (λ τ, interp L τ Δ) Γ vs
WP e.[env_subst vs] {{ interp L τ Δ }}.
(HNLdisj : l : loc, N L .@ l)
(Htyped : typed Γ e τ)
(HΔ : x v, PersistentP (Δ x v)) :
List.length Γ = List.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.
......@@ -79,15 +79,14 @@ Section typed_interp.
smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
iApply wp_mono; [|iApply "Hv"]; auto.
- (* TLam *)
value_case. iIntros { [τi τiPr] } "!".
value_case. iIntros {τi} "! %".
iApply wp_TLam; iNext. simpl.
iApply (IHHtyped (extend_context_interp_fun1 τi Δ)); [rewrite map_length|]; trivial.
rewrite -zip_with_context_interp_subst. auto.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
unshelve iSpecialize ("Hv" $! ((interp L τ' Δ) _)); try apply _; cbn.
iApply wp_mono; [|done].
intros w; rewrite interp_subst; trivial.
iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (interp L τ' Δ)); iPureIntro; apply _|]; cbn.
iIntros {w} "?"; rewrite interp_subst; trivial.
- (* Fold *)
rewrite map_length in IHHtyped.
iApply (@wp_bind _ _ _ [FoldCtx]).
......
This diff is collapsed.
......@@ -18,18 +18,11 @@ Section Soundness.
Qed.
Definition free_type_context: varC -n> valC -n> iPropG lang Σ :=
{|
cofe_mor_car :=
λ x,
{|
cofe_mor_car :=
λ y, True%I
|}
|}.
λne x y, True%I.
Lemma wp_soundness e τ
: typed [] e τ
ownership.ownP WP e {{v, H, @interp Σ H (nroot .@ "Fμ,ref" .@ 1)
Lemma wp_soundness e τ :
typed [] e τ
ownership.ownP WP e {{ v, H, @interp Σ H (nroot .@ "Fμ,ref" .@ 1)
τ free_type_context v}}.
Proof.
iIntros {H1} "Hemp".
......
......@@ -26,7 +26,7 @@ Section CG_Counter.
Proof. intros H f. unfold CG_increment. asimpl. rewrite ?H; trivial. Qed.
Lemma CG_increment_subst (x : expr) f :
(CG_increment x).[f] = CG_increment x.[f].
(CG_increment x).[f] = CG_increment x.[f].
Proof. unfold CG_increment; asimpl; trivial. Qed.
Lemma steps_CG_increment N E ρ j K x n:
......
......@@ -18,9 +18,8 @@ Section Stack_refinement.
set (Hdsj := ndot_ne_disjoint N n n' Hneq); set_solver_ndisj.
Lemma FG_CG_counter_refinement N Δ
{HΔ : x vw, PersistentP (Δ x vw)}
:
(@bin_log_related _ _ _ N Δ [] FG_stack CG_stack
{HΔ : x vw, PersistentP (Δ x vw)}:
(@bin_log_related _ _ _ N Δ [] FG_stack CG_stack
(TForall
(TProd
(TProd
......@@ -38,8 +37,7 @@ Section Stack_refinement.
unfold CG_stack, FG_stack.
iApply wp_value; eauto.
iExists (TLamV _); iFrame "Hj".
iIntros {τi}. destruct τi as [τi Hτ]; simpl.
iAlways. clear j K. iIntros {j K} "Hj".
clear j K. iAlways. iIntros {τi j K} "% Hj /=".
iPvs (step_Tlam _ _ _ j K with "[Hj]") as "Hj"; eauto.
iApply wp_TLam; iNext.
iPvs (steps_newlock _ _ _ j (K ++ [AppRCtx (LamV _)]) _ with "[Hj]")
......@@ -334,7 +332,7 @@ Section Stack_refinement.
rewrite ?fill_app. simpl.
rewrite -FG_iter_folding.
iRevert {istk3 w} "Hj HLK'". iLöb as "Hlat".
iIntros {istk3 w} "Hj". iIntros "HLK". (* A bug in iIntros? *)
iIntros {istk3 w} "Hj HLK".
rewrite -> FG_iter_folding at 1.
iApply wp_lam; simpl; trivial.
rewrite -FG_iter_folding. asimpl. rewrite FG_iter_subst.
......@@ -422,105 +420,13 @@ Section Stack_refinement.
all: try match goal with
|- _ _ => let H := fresh "H" in intros H; inversion H; auto
end.
(* This seems to be a bug in all: mechanism!? *)
match goal with
all: match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
abstract (prove_disj N A B)
end.
match goal with
|- @subseteq
_ _ (nclose (N .@ ?A))
(@difference _ _ (nclose (N .@ ?B))) =>
_ _ (nclose (?N .@ ?A))
(@difference _ _ (nclose (?N .@ ?B))) =>
abstract (prove_disj N A B)
end.
Qed.
End Stack_refinement.
Definition Σ := #[authGF heapUR; authGF cfgUR; authGF stackUR].
......
......@@ -52,35 +52,17 @@ Section Rules.
Qed.
Program Definition StackLink_pre (Q : bivalC -n> iPropG lang Σ)
{HQ : vw, PersistentP (Q vw)} :
(bivalC -n> iPropG lang Σ) -n> bivalC -n> iPropG lang Σ :=
{|
cofe_mor_car :=
λ P,
{|
cofe_mor_car :=
λ v, ( l w, v.1 = LocV l l ↦ˢᵗᵏ w
((w = InjLV UnitV
v.2 = FoldV (InjLV UnitV))
( y1 z1 y2 z2,
(w = InjRV (PairV y1 (FoldV z1)))
(v.2 = FoldV (InjRV (PairV y2 z2)))
Q (y1, y2) P(z1, z2)
)
)
)%I
|}
|}.
{HQ : vw, PersistentP (Q vw)} :
(bivalC -n> iPropG lang Σ) -n> bivalC -n> iPropG lang Σ := λne P v,
( l w, v.1 = LocV l l ↦ˢᵗᵏ w
((w = InjLV UnitV v.2 = FoldV (InjLV UnitV))
( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1))
v.2 = FoldV (InjRV (PairV y2 z2)) Q (y1, y2) P(z1, z2))))%I.
Next Obligation.
intros Q HQ P n [v1 v2] [w1 w2] [Hv1 Hv2]; simpl in *;
by rewrite Hv1 Hv2.
Qed.
Next Obligation.
intros Q HQ n P1 P2 HP v; simpl in *.
repeat (apply exist_ne => ?). repeat apply sep_ne; trivial.
rewrite or_ne; trivial. repeat (apply exist_ne => ?).
by rewrite HP.
Qed.
Next Obligation. solve_proper. Qed.
Global Instance StackLink_pre_contractive Q {HQ} :
Contractive (@StackLink_pre Q HQ).
......
This diff is collapsed.
......@@ -23,12 +23,11 @@ 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))
: List.length Γ = List.length vs
heapI_ctx N [] zip_with (λ τ, interp L τ Δ) Γ vs
WP e.[env_subst vs] {{ interp L τ Δ }}.
(HNLdisj : l : loc, N L .@ l)
(Htyped : typed Γ e τ) (HΔ : x v, PersistentP (Δ x v)) :
List.length Γ = List.length vs
heapI_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.
......@@ -94,14 +93,14 @@ Section typed_interp.
smart_wp_bind (AppRCtx v) w "#Hw" IHHtyped2.
iApply wp_mono; [|iApply "Hv"]; auto.
- (* TLam *)
value_case. iIntros { [τi τiPr] } "! /=". iApply wp_TLam; iNext.
value_case. iIntros {τi} "! /= %". iApply wp_TLam; iNext.
iApply (IHHtyped (extend_context_interp_fun1 τi Δ)); [rewrite map_length|]; trivial.
iSplit; trivial.
rewrite zip_with_context_interp_subst; trivial.
- (* TApp *)
smart_wp_bind TAppCtx v "#Hv" IHHtyped; cbn.
unshelve iSpecialize ("Hv" $! ((interp L τ' Δ) _)); try apply _; cbn.
iApply wp_mono; [|done] => w. by rewrite -interp_subst; simpl.
iApply wp_wand_r; iSplitL; [iApply ("Hv" $! (interp L τ' Δ)); iPureIntro; apply _|]; cbn.
iIntros {w} "?". by rewrite -interp_subst; simpl.
- (* Fold *)
specialize (IHHtyped Δ HΔ vs Hlen).
iApply (@wp_bind _ _ _ [FoldCtx]).
......
This diff is collapsed.
This diff is collapsed.
......@@ -14,18 +14,17 @@ Section Soundness.
{Hhp : auth.authG lang Σ heapUR}
{Hcfg : auth.authG lang Σ cfgUR}.
Definition free_type_context : varC -n> bivalC -n> iPropG lang Σ :=
{| cofe_mor_car := λ x, {| cofe_mor_car := λ y, (True)%I |} |}.
Definition free_type_context : varC -n> bivalC -n> iPropG lang Σ := λne x y,
True%I.
Local Notation Δφ := free_type_context.
Local Opaque to_heap.
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))}}.
( H H' N Δ HΔ, @bin_log_related Σ H H' N Δ [] e e' τ HΔ)
@ownership.ownP lang (globalF Σ)
WP e {{_, ( thp' h v, rtc step ([e'], ) ((# v) :: thp', h)) }}.
Proof.
iIntros {H1} "Hemp".
iPvs (heap_alloc (nroot .@ "Fμ,ref,par" .@ 2) _ _ _ _ with "Hemp")
......
......@@ -11,21 +11,13 @@ Import uPred.
Section Soundness.
Definition Σ := #[ auth.authGF heapUR ].
Definition free_type_context: varC -n> valC -n> iPropG lang Σ :=
{|
cofe_mor_car :=
λ x,
{|
cofe_mor_car :=
λ y, (True)%I
|}
|}.
Definition free_type_context: varC -n> valC -n> iPropG lang Σ := λne x y,
True%I.
Lemma wp_soundness e τ
: typed [] e τ
ownership.ownP
WP e {{v, H, @interp Σ H (nroot .@ "Fμ,ref,par" .@ 1)
τ free_type_context v }}.
Lemma wp_soundness e τ :
typed [] e τ
ownership.ownP WP e {{v, H, @interp Σ H (nroot .@ "Fμ,ref,par" .@ 1)
τ free_type_context v }}.
Proof.
iIntros {H1} "Hemp".
iPvs (heap_alloc (nroot .@ "Fμ,ref,par" .@ 2) _ _ _ _ with "Hemp")
......@@ -42,17 +34,13 @@ Section Soundness.
Theorem Soundness e τ :
typed [] e τ
e' thp h, rtc step ([e], (of_heap )) (e' :: thp, h)
¬ reducible e' h is_Some (to_val e').
¬reducible e' h is_Some (to_val e').
Proof.
intros H1 e' thp h Hstp Hnr.
eapply wp_soundness in H1; eauto.
edestruct (@wp_adequacy_reducible lang (globalF Σ)
(λ v,
( H, @interp
Σ H (nroot .@ "Fμ,ref,par" .@ 1)
τ free_type_context v)%I)
e e' (e' :: thp) h)
as [Ha|Ha]; eauto; try tauto.
edestruct (@wp_adequacy_reducible lang (globalF Σ) (λ v, ( H,
@interp Σ H (nroot .@ "Fμ,ref,par" .@ 1) τ free_type_context v)%I)
e e' (e' :: thp) h) as [Ha|Ha]; eauto; try tauto.
- apply ucmra_unit_valid.
- iIntros "[Hp Hg]". by iApply H1.
- by rewrite of_empty_heap in Hstp.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment