Commit 3aa70947 authored by Dan Frumin's avatar Dan Frumin

Simplify the late/early refinement proof

parent 0a068c24
......@@ -48,16 +48,14 @@ Section Refinement.
- {E1,E1;Γ} fill K (rand #())%E log t : τ.
Proof.
iIntros (?) "#Hs Hlog".
unfold rand at 1. unlock. simpl.
iApply (bin_log_related_rec_l Γ E1 K BAnon BAnon _ #()%E); first done.
iNext. simpl.
unfold rand. unlock. simpl.
rel_rec_l.
rel_bind_l (Alloc _).
iApply bin_log_related_alloc_l'; first eauto. iIntros (y) "Hy". simpl.
iApply (bin_log_related_rec_l _ _ K); first eauto. iNext. simpl.
rel_rec_l.
iMod (inv_alloc choiceN _ ( b, y ↦ᵢ (#v b))%I with "[Hy]") as "#Hinv".
{ iNext. eauto. }
rel_bind_l (Fork _).
iApply bin_log_related_fork_l. iModIntro.
rel_fork_l. iModIntro.
iSplitR.
- iNext.
iInv choiceN as (b) "Hy" "Hcl".
......@@ -66,130 +64,67 @@ Section Refinement.
{ iNext. iExists true. by iFrame. }
done.
- simpl.
iApply (bin_log_related_rec_l _ _ K); first eauto. iNext. simpl.
iApply (bin_log_related_load_l _ _ _ K).
iInv choiceN as (b) "Hy" "Hcl". iModIntro.
iExists (#v b). iFrame. iIntros "Hy".
rel_rec_l.
rel_load_l under choiceN as "Hy" "Hcl".
iDestruct "Hy" as (b) "Hy".
iExists (#v b). iFrame.
iModIntro. iIntros "Hy".
iMod ("Hcl" with "[Hy]").
{ iNext. iExists b. iFrame. }
done.
Qed.
Lemma rand_r b Γ E1 E2 K ρ t τ :
specN E1
choiceN E1
spec_ctx ρ -
{E1,E2;Γ} t log fill K (# b) : τ -
{E1,E2;Γ} t log fill K (rand #())%E : τ.
Proof.
iIntros (??) "#Hs Hlog".
unfold rand. unlock.
rel_rec_r.
rel_alloc_r as y "Hy".
rel_rec_r.
rel_fork_r as j "Hj".
rel_rec_r.
destruct b.
- iApply fupd_logrel'. tp_store j. iModIntro.
by rel_load_r.
- by rel_load_r.
Qed.
Lemma lateChoice_l Γ x v ρ t :
spec_ctx ρ - x ↦ᵢ v -
(x ↦ᵢ (#nv 0) - b, Γ (# b) log t : TBool) -
(x ↦ᵢ (#nv 0) - b, Γ # b log t : TBool) -
Γ lateChoice #x log t : TBool.
Proof.
iIntros "#Hs Hx Hlog".
unfold lateChoice. unlock.
iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl. rewrite !Closed_subst_id.
rel_bind_l (#x <- _)%E.
iApply (bin_log_related_store_l' with "Hx"); eauto. iIntros "Hx".
simpl.
iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
unfold rand at 1. unlock.
iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
rel_bind_l (Alloc _).
iApply bin_log_related_alloc_l'; eauto. iIntros (y) "Hy". simpl.
iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
iMod (inv_alloc choiceN _ ( b, y ↦ᵢ (#v b))%I with "[Hy]") as "#Hinv".
{ iNext. eauto. }
rel_bind_l (Fork _).
iApply bin_log_related_fork_l. iModIntro.
iSplitR.
- iNext.
iInv choiceN as (b) "Hy" "Hcl".
iApply (wp_store with "Hy"); eauto. iNext. iIntros "Hy".
iMod ("Hcl" with "[Hy]").
{ iNext. iExists true. by iFrame. }
done.
- simpl.
iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
iApply (bin_log_related_load_l _ _ _ []).
iInv choiceN as (b) "Hy" "Hcl". iModIntro.
iExists (#v b). iFrame. iIntros "Hy".
iMod ("Hcl" with "[Hy]").
{ iNext. iExists b. iFrame. }
simpl. iApply ("Hlog" with "Hx").
rel_rec_l.
rel_store_l. simpl.
rel_rec_l.
rel_bind_l (rand #())%E.
iApply (rand_l with "Hs"); eauto. simpl.
by iApply "Hlog".
Qed.
(* Lemma lateChoice_l Γ E1 E2 K x t τ R : *)
(* (|={E1,E2}=> n, x ↦ᵢ (#nv n) R(n) *)
(* (( n, x ↦ᵢ (#nv n) R(n)) ={E2,E1}= True) *)
(* (x ↦ᵢ (#nv 0) R(0) - *)
(* b, {E2,E1;Γ} fill K (# b) log t : τ)) *)
(* - {E1,E1;Γ} fill K (lateChoice #x)%E log t : τ. *)
(* Proof. *)
(* iIntros "#H". *)
(* unfold lateChoice. unlock. *)
(* iApply (bin_log_related_rec_l _ _ K); eauto. iNext. simpl. rewrite !Closed_subst_id. *)
(* rel_bind_l (#x <- _)%E. *)
(* iApply (bin_log_related_store_l); eauto. *)
(* iMod "H" as (n) "[Hx [HR Hfin]]". *)
(* iModIntro. iExists (#nv n). iFrame. *)
(* iIntros "Hx". *)
(* simpl. *)
(* rewrite ->uPred.and_elim_l. *)
Definition choice_inv' y y' x x' : iProp Σ :=
(( f, y ↦ᵢ (#v f) y' ↦ₛ (#v f))
( n, x ↦ᵢ (#nv n) x' ↦ₛ (#nv n)))%I.
Lemma prerefinement Γ x x' n ρ :
(spec_ctx ρ - x ↦ᵢ (#nv n) - x' ↦ₛ (#nv n) -
Γ lateChoice #x log earlyChoice #x' : TBool)%I.
Proof.
iIntros "#Hspec Hx Hx'".
unfold lateChoice, earlyChoice. unlock.
rel_rec_l.
iApply (lateChoice_l with "Hspec Hx"). iIntros "Hx".
iIntros (b).
unfold earlyChoice. unlock.
rel_rec_r.
rel_store_l. simpl.
rel_rec_l.
unfold rand at 1. unlock.
rel_rec_l.
rel_alloc_l as y "Hy". simpl.
rel_rec_l.
unfold rand. unlock.
rel_rec_r.
rel_alloc_r as y' "Hy'".
rel_bind_r (rand #())%E.
iApply (rand_r b with "Hspec"); eauto. simpl.
rel_rec_r.
iAssert (choice_inv y y') with "[Hy Hy']" as "Hinv".
{ iExists false. by iFrame. }
iMod (inv_alloc choiceN with "[Hinv]") as "#Hinv".
{ iNext. iApply "Hinv". }
rel_fork_r as i "Hi".
rel_store_r. simpl.
rel_rec_r.
rel_fork_l. iModIntro.
iSplitL "Hi".
- iNext.
iInv choiceN as (f) "[Hy Hy']" "Hcl".
iApply (wp_store with "Hy"); eauto. iNext. iIntros "Hy".
tp_store i.
iMod ("Hcl" with "[Hy Hy']").
{ iNext. iExists true. by iFrame. }
done.
- rel_rec_l.
rel_load_l under choiceN as "Hys" "Hcl".
iDestruct "Hys" as (f) "[Hy >Hy']". iModIntro.
iExists (#v f). iFrame. iIntros "Hy". simpl.
rel_load_r.
iMod ("Hcl" with "[Hy Hy']").
{ iNext. iExists f. iFrame. }
rel_rec_r.
rel_store_r. simpl.
rel_seq_r.
rel_vals. eauto.
rel_vals; eauto.
Qed.
Lemma refinement Γ ρ :
......
......@@ -26,6 +26,18 @@ Section properties.
iSpecialize ("H" with "Hs [HΓ] Hj"); eauto.
Qed.
(* TODO: should there be a corresponding =ElimModal= instance? *)
Lemma fupd_logrel' Γ E1 E2 e e' τ :
((|={E1}=> ({E1,E2;Γ} e log e' : τ))
- {E1,E2;Γ} e log e' : τ)%I.
Proof.
rewrite bin_log_related_eq.
iIntros "H".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
iMod "H".
iSpecialize ("H" with "Hs [HΓ] Hj"); eauto.
Qed.
Global Instance elim_modal_logrel E1 E2 Γ e e' P τ :
ElimModal (|={E1,E2}=> P) P
({E1,E2;Γ} e log e' : τ) ({E2,E2;Γ} e log e' : τ) | 0.
......@@ -70,8 +82,7 @@ Section properties.
rewrite fill_subst. iModIntro.
iApply (wp_bind (subst_ctx (fst <$> vvs) K')).
rewrite Closed_subst_p_id.
iApply wp_lift_pure_det_head_step_no_fork; eauto.
iModIntro. iNext.
iApply wp_lift_pure_det_head_step_no_fork'; eauto. iNext.
iSpecialize ("IH" with "Hs [HΓ] Hj"); auto. simpl.
rewrite /env_subst fill_subst.
rewrite Closed_subst_p_id.
......@@ -80,7 +91,7 @@ Section properties.
change lang with (ectx_lang expr).
change fill with (ectx_language.fill).
eapply ectx_lang_ctx. }
iApply (fupd_mask_mono E); auto.
iApply fupd_wp. by iApply (fupd_mask_mono E).
Qed.
Lemma bin_log_pure_masked_l (Γ : stringmap type) (E1 E2 : coPset)
......
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