Commit a850d3b3 authored by Robbert Krebbers's avatar Robbert Krebbers

Put the quantification over Δ in the definition bin_log_related.

parent 9a182da8
......@@ -194,16 +194,12 @@ Notation "Γ ⊨ e '≤ctx≤' e' : τ" :=
Section bin_log_related_under_typed_ctx.
Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodC valC valC -n> iPropG lang Σ).
Implicit Types Δ : listC D.
Lemma bin_log_related_under_typed_ctx Γ e e' τ Γ' τ' K :
( f, e.[base.iter (length Γ) up f] = e)
( f, e'.[base.iter (length Γ) up f] = e')
typed_ctx K Γ τ Γ' τ'
( Δ (HΔ : env_PersistentP Δ), Δ Γ e log e' : τ)
Δ (HΔ : env_PersistentP Δ),
Δ Γ' fill_ctx K e log fill_ctx K e' : τ'.
Γ 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.
......
......@@ -253,10 +253,10 @@ Section CG_Counter.
Definition counterN : namespace := nroot .@ "counter".
Lemma FG_CG_counter_refinement Δ {HΔ : env_PersistentP Δ} :
Δ [] FG_counter log CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
Lemma FG_CG_counter_refinement :
[] FG_counter log CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
Proof.
iIntros { [|??] ρ} "#(Hheap & Hspec & HΓ)"; iIntros {j K} "Hj"; last first.
iIntros { Δ [|??] ρ ? } "#(Hheap & Hspec & HΓ)"; iIntros {j K} "Hj"; last first.
{ iDestruct (interp_env_length with "HΓ") as %[=]. }
iClear "HΓ". cbn -[FG_counter CG_counter].
rewrite ?empty_env_subst /CG_counter /FG_counter.
......
......@@ -12,14 +12,14 @@ Section Stack_refinement.
Notation D := (prodC valC valC -n> iPropG lang Σ).
Implicit Types Δ : listC D.
Lemma FG_CG_counter_refinement Δ {HΔ : env_PersistentP Δ} :
Δ [] FG_stack log CG_stack : TForall (TProd (TProd
(TArrow (TVar 0) TUnit)
(TArrow TUnit (TSum TUnit (TVar 0))))
(TArrow (TArrow (TVar 0) TUnit) TUnit)).
Lemma FG_CG_counter_refinement :
[] FG_stack log CG_stack : TForall (TProd (TProd
(TArrow (TVar 0) TUnit)
(TArrow TUnit (TSum TUnit (TVar 0))))
(TArrow (TArrow (TVar 0) TUnit) TUnit)).
Proof.
(* executing the preambles *)
iIntros { [|??] ρ} "#(Hheap & Hspec & HΓ)"; iIntros {j K} "Hj"; last first.
iIntros { Δ [|??] ρ ? } "#(Hheap & Hspec & HΓ)"; iIntros {j K} "Hj"; last first.
{ iDestruct (interp_env_length with "HΓ") as %[=]. }
iClear "HΓ". cbn -[FG_stack CG_stack].
rewrite ?empty_env_subst /CG_stack /FG_stack.
......@@ -378,5 +378,5 @@ Proof.
eapply (@binary_soundness Σ);
eauto using FG_stack_closed, CG_stack_closed.
all: try typeclasses eauto.
intros. apply FG_CG_counter_refinement, _.
intros. apply FG_CG_counter_refinement.
Qed.
This diff is collapsed.
......@@ -12,7 +12,7 @@ Section soundness.
Local Opaque to_heap.
Lemma wp_basic_soundness e e' τ :
( `{heapIG Σ, cfgSG Σ} Δ (HΔ : env_PersistentP Δ), Δ [] e log e' : τ)
( `{heapIG Σ, cfgSG Σ}, [] e log e' : τ)
ownP (Σ:=globalF Σ)
WP e {{ _, thp' h v, rtc step ([e'], ) (# v :: thp', h) }}.
Proof.
......@@ -30,7 +30,8 @@ Section soundness.
iPureIntro. rewrite from_to_cfg; constructor. }
iPvs (inv_alloc specN with "[Hinv]") as "#Hcfg"; trivial.
{ iNext. iExact "Hinv". }
iPoseProof (bin_log_related_alt (H1 h (@CFGSG _ _ γ) [] _) [] _ 0 [] with "[Hcfg2]") as "HBR".
iPoseProof (bin_log_related_alt (H1 h (@CFGSG _ _ γ)) [] [] _ 0 [] with "[Hcfg2]") as "HBR".
{ apply _. }
{ rewrite /spec_ctx /auth_ctx /tpool_mapsto /auth_own empty_env_subst /=.
iFrame "Hheap Hcfg Hcfg2". by rewrite -interp_env_nil. }
rewrite /= empty_env_subst.
......@@ -60,29 +61,21 @@ Section soundness.
Qed.
Lemma basic_soundness e e' τ v thp hp :
( `{heapIG Σ, cfgSG Σ} Δ (HΔ : env_PersistentP Δ), Δ [] e log e' : τ)
( `{heapIG Σ, cfgSG Σ}, [] e log e' : τ)
rtc step ([e], ) (# v :: thp, hp)
( thp' hp' v', rtc step ([e'], ) (# v' :: thp', hp')).
Proof.
intros H1 H2.
match goal with
|- ?A =>
eapply (@wp_adequacy_result lang _ (λ _, A) e v thp hp); eauto
end.
- apply ucmra_unit_valid.
- iIntros "[Hp Hg]".
iApply wp_wand_l; iSplitR; [| iApply wp_basic_soundness]; auto.
by iIntros {w} "H".
intros. eapply wp_adequacy_result; eauto using ucmra_unit_valid.
iIntros "[??]". by iApply wp_basic_soundness.
Qed.
Lemma binary_soundness Γ e e' τ :
( f, e.[base.iter (length Γ) up f] = e)
( f, e'.[base.iter (length Γ) up f] = e')
( `{heapIG Σ, cfgSG Σ} Δ (HΔ : env_PersistentP Δ), Δ Γ e log e' : τ)
( `{heapIG Σ, cfgSG Σ}, Γ e log e' : τ)
Γ e ctx e' : τ.
Proof.
intros H1 K HK htp hp v Hstp Hc Hc'.
eapply basic_soundness; eauto.
intros H1 K HK htp hp v Hstp Hc Hc'; eapply basic_soundness; eauto.
intros H' H'' N Δ HΔ.
eapply (bin_log_related_under_typed_ctx _ _ _ _ []); eauto.
Qed.
......
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