Commit ba2fcff2 authored by Robbert Krebbers's avatar Robbert Krebbers

Same the same for the binary logrel on F_mu_ref_par.

parent f69f3e5b
This diff is collapsed.
......@@ -35,8 +35,9 @@ Definition FG_counter : expr :=
App (Lam (FG_counter_body (Var 1))) (Alloc ( 0)).
Section CG_Counter.
Context {Σ : gFunctors} {iS : cfgSG Σ} {iI : heapIG Σ}.
Implicit Types Δ : varC -n> bivalC -n> iPropG lang Σ.
Context `{iS : cfgSG Σ, heapIG Σ}.
Notation D := (prodC valC valC -n> iPropG lang Σ).
Implicit Types Δ : listC D.
(* Coarse-grained increment *)
Lemma CG_increment_type x Γ :
......@@ -50,7 +51,7 @@ Section CG_Counter.
Lemma CG_increment_closed (x : expr) :
( f, x.[f] = x) f, (CG_increment x).[f] = CG_increment x.
Proof. intros H f. unfold CG_increment. asimpl. rewrite ?H; trivial. Qed.
Proof. intros Hx f. unfold CG_increment. asimpl. rewrite ?Hx; trivial. Qed.
Lemma CG_increment_subst (x : expr) f :
(CG_increment x).[f] = CG_increment x.[f].
......@@ -221,7 +222,7 @@ Section CG_Counter.
Lemma FG_increment_closed (x : expr) :
( f, x.[f] = x) f, (FG_increment x).[f] = FG_increment x.
Proof. intros H f. asimpl. unfold FG_increment. rewrite ?H; trivial. Qed.
Proof. intros Hx f. asimpl. unfold FG_increment. rewrite ?Hx; trivial. Qed.
Lemma FG_counter_body_type x Γ :
typed Γ x (Tref TNat)
......@@ -251,14 +252,14 @@ Section CG_Counter.
Lemma FG_counter_closed f : FG_counter.[f] = FG_counter.
Proof. asimpl; rewrite counter_read_subst; by asimpl. Qed.
Lemma FG_CG_counter_refinement N Δ {HΔ : x v, PersistentP (Δ x v)} :
Lemma FG_CG_counter_refinement N Δ {HΔ : ctx_PersistentP Δ} :
@bin_log_related _ _ _ N Δ [] FG_counter CG_counter
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)) HΔ.
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
Proof.
(* executing the preambles *)
intros [|v vs] Hlen; simplify_eq.
intros [|v vs] ρ j K [=].
cbn -[FG_counter CG_counter].
iIntros {ρ j K} "(#Hheap & #Hspec & _ & Hj)".
iIntros "(#Hheap & #Hspec & _ & Hj)".
rewrite ?empty_env_subst /CG_counter /FG_counter.
iPvs (steps_newlock _ _ _ j (K ++ [AppRCtx (LamV _)]) _ with "[Hj]")
as {l} "[Hj Hl]"; eauto.
......@@ -358,11 +359,11 @@ End CG_Counter.
Definition Σ := #[auth.authGF heapUR; auth.authGF cfgUR].
Theorem counter_context_refinement :
context_refines [] FG_counter CG_counter
Theorem counter_ctx_refinement :
ctx_refines [] FG_counter CG_counter
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)).
Proof.
eapply (@Binary_Soundness Σ);
eapply (@binary_soundness Σ);
auto using FG_counter_closed, CG_counter_closed, FG_CG_counter_refinement.
all: typeclasses eauto.
Qed.
......@@ -6,11 +6,11 @@ From iris_logrel.F_mu_ref_par.examples.stack Require Import
From iris.proofmode Require Import invariants ghost_ownership tactics.
Section Stack_refinement.
Context {Σ : gFunctors} {iS : cfgSG Σ} {iI : heapIG Σ}
{iSTK : authG lang Σ stackUR}.
Implicit Types Δ : varC -n> bivalC -n> iPropG lang Σ.
Context `{cfgSG Σ, heapIG Σ, authG lang Σ stackUR}.
Notation D := (prodC valC valC -n> iPropG lang Σ).
Implicit Types Δ : listC D.
Lemma FG_CG_counter_refinement N Δ {HΔ : x vw, PersistentP (Δ x vw)} :
Lemma FG_CG_counter_refinement N Δ {HΔ : ctx_PersistentP Δ} :
@bin_log_related _ _ _ N Δ [] FG_stack CG_stack
(TForall
(TProd
......@@ -19,10 +19,10 @@ Section Stack_refinement.
(TArrow TUnit (TSum TUnit (TVar 0)))
)
(TArrow (TArrow (TVar 0) TUnit) TUnit)
)) HΔ.
)).
Proof.
(* executing the preambles *)
iIntros { [|??] [=] ρ j K } "[#Hheap [#Hspec [_ Hj]]]".
iIntros { [|??] ρ j K [=] } "[#Hheap [#Hspec [_ Hj]]]".
cbn -[FG_stack CG_stack].
rewrite ?empty_env_subst /CG_stack /FG_stack.
iApply wp_value; eauto.
......@@ -64,7 +64,7 @@ Section Stack_refinement.
{ constructor; eauto. eapply ucmra_unit_valid. }
set (istkG := StackG _ _ γ).
change γ with (@stack_name _ istkG).
change iSTK with (@stack_inG _ istkG).
change H1 with (@stack_inG _ istkG).
clearbody istkG. clear γ.
iAssert (@stack_owns _ istkG _ ) with "[Hemp]" as "Hoe".
{ unfold stack_owns; rewrite big_sepM_empty; iFrame "Hemp"; trivial. }
......@@ -374,8 +374,8 @@ End Stack_refinement.
Definition Σ := #[authGF heapUR; authGF cfgUR; authGF stackUR].
Theorem stack_context_refinement :
context_refines [] FG_stack CG_stack
Theorem stack_ctx_refinement :
ctx_refines [] FG_stack CG_stack
(TForall
(TProd
(TProd
......@@ -386,8 +386,8 @@ Theorem stack_context_refinement :
)
).
Proof.
eapply (@Binary_Soundness Σ);
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.
......@@ -20,19 +20,17 @@ Class stackG Σ :=
StackG { stack_inG :> authG lang Σ stackUR; stack_name : gname }.
Section Rules.
Context {Σ : gFunctors} {istk : stackG Σ}.
Context `{stackG Σ}.
Notation D := (prodC valC valC -n> iPropG lang Σ).
Definition stack_mapsto (l : loc) (v: val) : iPropG lang Σ :=
auth_own stack_name ({[ l := DecAgree v ]}).
auth_own stack_name {[ l := DecAgree v ]}.
Notation "l ↦ˢᵗᵏ v" := (stack_mapsto l v) (at level 20) : uPred_scope.
Lemma stack_mapsto_dup l v : True%I l ↦ˢᵗᵏ v - (l ↦ˢᵗᵏ v l ↦ˢᵗᵏ v).
Lemma stack_mapsto_dup l v : l ↦ˢᵗᵏ v l ↦ˢᵗᵏ v l ↦ˢᵗᵏ v.
Proof.
iIntros "H".
unfold stack_mapsto, auth_own.
rewrite -own_op -auth_frag_op.
rewrite -stackR_self_op; trivial.
by rewrite /stack_mapsto /auth_own -own_op -auth_frag_op -stackR_self_op.
Qed.
Lemma stack_mapstos_agree l v w:
......@@ -47,53 +45,37 @@ Section Rules.
cbv -[decide] in Hvalid; destruct decide; trivial.
Qed.
Program Definition StackLink_pre (Q : bivalC -n> iPropG lang Σ)
{HQ : vw, PersistentP (Q vw)} :
(bivalC -n> iPropG lang Σ) -n> bivalC -n> iPropG lang Σ := λne P v,
Program Definition StackLink_pre (Q : D) : D -n> D := λ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. solve_proper. Qed.
Solve Obligations with solve_proper.
Global Instance StackLink_pre_contractive Q {HQ} :
Contractive (@StackLink_pre Q HQ).
Global Instance StackLink_pre_contractive Q : Contractive (StackLink_pre Q).
Proof.
intros n P1 P2 HP v; simpl. repeat (apply exist_ne => ?).
repeat apply sep_ne; trivial. rewrite or_ne; trivial.
repeat (apply exist_ne => ?).
repeat apply sep_ne; trivial.
apply later_contractive => i H. by apply HP.
apply later_contractive => i ?. by apply HP.
Qed.
Definition StackLink Q {HQ} := fixpoint (@StackLink_pre Q HQ).
Definition StackLink Q := fixpoint (StackLink_pre Q).
Lemma StackLink_unfold Q {HQ} v :
@StackLink Q HQ 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)
@StackLink Q HQ (z1, z2)
)
)
)%I.
Proof.
unfold StackLink at 1.
rewrite fixpoint_unfold; trivial.
Qed.
Lemma StackLink_unfold Q v :
StackLink Q 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) @StackLink Q (z1, z2))))%I.
Proof. by rewrite {1}/StackLink fixpoint_unfold. Qed.
Global Opaque StackLink. (* So that we can only use the unfold above. *)
Lemma StackLink_dup Q {HQ} v :
@StackLink Q HQ v @StackLink Q HQ v @StackLink Q HQ v.
Lemma StackLink_dup (Q : D) v `{ vw, PersistentP (Q vw)} :
StackLink Q v StackLink Q v StackLink Q v.
Proof.
iIntros "H". iLöb {v} as "Hlat". rewrite StackLink_unfold.
iDestruct "H" as {l w} "[% [Hl Hr]]"; subst.
......@@ -113,8 +95,8 @@ Section Rules.
Lemma stackR_valid (h : stackUR) (i : loc) :
h h !! i = None v, h !! i = Some (DecAgree v).
Proof.
intros H; specialize (H i).
match type of H with
intros Hh; specialize (Hh i).
by match type of Hh with
?A => match goal with
| |- ?B = _ ( _, ?C = _) =>
change B with A; change C with A;
......@@ -182,10 +164,10 @@ Section Rules.
end
end.
- set (H5 := dec_agree_valid_op_eq _ _ H4); clearbody H5. subst.
inversion H1; subst.
inversion H3; subst.
destruct x as [x|]; cbv -[decide]; try destruct decide;
constructor; intuition trivial.
- inversion H1; subst. constructor; trivial.
- inversion H3; subst. constructor; trivial.
Qed.
Context {iI : heapIG Σ}.
......
This diff is collapsed.
This diff is collapsed.
......@@ -57,13 +57,13 @@ Section logrel.
intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper.
Qed.
Program Definition interp_ref_pred (l : loc) : D -n> iPropG lang Σ := λne τi,
Program Definition interp_ref_inv (l : loc) : D -n> iPropG lang Σ := λne τi,
( v, l ↦ᵢ v τi v)%I.
Solve Obligations with solve_proper.
Program Definition interp_ref
(interp : listC D -n> D) : listC D -n> D := λne Δ w,
( l, w = LocV l inv (L .@ l) (interp_ref_pred l (interp Δ)))%I.
( l, w = LocV l inv (L .@ l) (interp_ref_inv l (interp Δ)))%I.
Solve Obligations with solve_proper.
Fixpoint interp (τ : type) : listC D -n> D :=
......
......@@ -4,52 +4,47 @@ From iris.program_logic Require Import ownership auth.
From iris.proofmode Require Import tactics pviewshifts invariants.
From iris.program_logic Require Import ownership adequacy.
Section Soundness.
Context `{Hhp : authG lang Σ heapUR, Hcfg : authG lang Σ cfgUR}.
Definition free_type_context : varC -n> bivalC -n> iPropG lang Σ := λne x y,
True%I.
Local Notation Δφ := free_type_context.
Section soundness.
Context `{authG lang Σ heapUR, authG lang Σ cfgUR}.
Notation D := (prodC valC valC -n> iPropG lang Σ).
Implicit Types Δ : listC D.
Local Opaque to_heap.
Lemma wp_basic_soundness e e' τ :
( H H' N Δ HΔ, @bin_log_related Σ H H' N Δ [] e e' τ HΔ)
@ownP lang (globalF Σ)
WP e {{ _, ( thp' h v, rtc step ([e'], ) (# v :: thp', h)) }}.
( H H' N Δ (HΔ : ctx_PersistentP Δ),
@bin_log_related Σ H H' N Δ [] e e' τ)
ownP (Σ:=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")
as {H} "[#Hheap _]".
iPvs (heap_alloc (nroot .@ 2) with "Hemp")
as {h} "[#Hheap _]"; first solve_ndisj.
iPvs (own_alloc ( (to_cfg ([e'], ) : cfgUR)
(({[ 0 := Excl' e' ]} : tpoolUR, ) : cfgUR))) as {γ} "[Hcfg1 Hcfg2]".
{ constructor; eauto.
- intros n; simpl. exists . unfold to_cfg; simpl. rewrite to_empty_heap.
by rewrite left_id right_id.
- repeat constructor; simpl; by auto.
}
- repeat constructor; simpl; by auto. }
iAssert (@auth.auth_inv _ Σ _ _ γ (Spec_inv ([e'], )))
with "[Hcfg1]" as "Hinv".
{ iExists _; iFrame "Hcfg1".
iPureIntro. rewrite from_to_cfg; constructor.
}
iPvs (inv_alloc (nroot .@ "Fμ,ref,par" .@ 3) with "[Hinv]") as "#Hcfg";
trivial.
iPureIntro. rewrite from_to_cfg; constructor. }
iPvs (inv_alloc (nroot .@ 3) with "[Hinv]") as "#Hcfg"; trivial.
{ iNext. iExact "Hinv". }
iPoseProof (H1 H (@CFGSG _ _ γ) _ Δφ _ [] _ _ 0 [] with "[Hcfg2]") as "HBR".
{ unfold Spec_ctx, auth.auth_ctx, tpool_mapsto, auth.auth_own.
simpl. rewrite empty_env_subst. by iFrame "Hheap Hcfg Hcfg2". }
simpl. rewrite empty_env_subst.
iPoseProof (H1 h (@CFGSG _ _ γ) _ [] _ [] _ 0 [] with "[Hcfg2]") as "HBR".
{ done. }
{ rewrite /Spec_ctx /auth_ctx /tpool_mapsto /auth_own empty_env_subst /=.
by iFrame "Hheap Hcfg Hcfg2". }
rewrite /= empty_env_subst.
iApply wp_pvs.
iApply wp_wand_l; iSplitR; [|iApply "HBR"].
iIntros {v}; iDestruct 1 as {v'} "[Hj #Hinterp]".
iInv> (nroot .@ "Fμ,ref,par" .@ 3) as {ρ} "[Hown #Hp]".
iInv> (nroot .@ 3) as {ρ} "[Hown #Hp]".
iDestruct "Hp" as %Hp.
unfold tpool_mapsto, auth.auth_own; simpl.
iCombine "Hj" "Hown" as "Hown".
iDestruct (@own_valid _ Σ (authR cfgUR) _ γ _ with "#Hown")
as "#Hvalid".
iDestruct (@own_valid _ Σ (authR cfgUR) _ γ with "#Hown") as "#Hvalid".
iDestruct (auth_validI _ with "Hvalid") as "[Ha' #Hb]";
simpl; iClear "Hvalid".
iDestruct "Hb" as %Hb.
......@@ -66,35 +61,33 @@ Section Soundness.
destruct r as [q r|]; simpl in *; eauto.
inversion Hx1 as [|? ? Hx]; subst.
destruct q as [?|]. by move: Hx=> [/exclusive_r ??]. done.
Unshelve. all: trivial.
Qed.
Lemma basic_soundness e e' τ :
( H H' N Δ HΔ , @bin_log_related Σ H H' N Δ [] e e' τ HΔ)
v thp hp,
rtc step ([e], ) ((# v) :: thp, hp)
( thp' hp' v', rtc step ([e'], ) ((# v') :: thp', hp')).
Lemma basic_soundness e e' τ v thp hp :
( H H' N Δ (HΔ : ctx_PersistentP Δ), @bin_log_related Σ H H' N Δ [] e e' τ)
rtc step ([e], ) (# v :: thp, hp)
( thp' hp' v', rtc step ([e'], ) (# v' :: thp', hp')).
Proof.
intros H1 v thp hp H2.
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; [| by iApply wp_basic_soundness].
iApply wp_wand_l; iSplitR; [| iApply wp_basic_soundness]; auto.
by iIntros {w} "H".
Qed.
Lemma Binary_Soundness Γ e e' τ :
Lemma binary_soundness Γ e e' τ :
( f, e.[base.iter (length Γ) up f] = e)
( f, e'.[base.iter (length Γ) up f] = e')
( H H' N Δ HΔ, @bin_log_related Σ H H' N Δ Γ e e' τ HΔ)
context_refines Γ e e' τ.
( H H' N Δ (HΔ : ctx_PersistentP Δ), @bin_log_related Σ H H' N Δ Γ e e' τ)
ctx_refines Γ e e' τ.
Proof.
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_context _ _ _ _ []); eauto.
intros H' H'' N Δ HΔ.
eapply (bin_log_related_under_typed_ctx _ _ _ _ []); eauto.
Qed.
End Soundness.
End soundness.
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