Commit 8b94528d authored by Dan Frumin's avatar Dan Frumin
Browse files

rel_apply_l/r tactics

parent d7cada37
......@@ -50,15 +50,15 @@ Section CG_Counter.
Proof.
iIntros (?) "Hx Hl Hlog".
unfold CG_increment. unlock. simpl_subst/=.
rel_rec_r.
rel_bind_r (acquire #l).
iApply (bin_log_related_acquire_r with "Hl"); eauto. iIntros "Hl". simpl.
rel_rec_r.
rel_apply_r (bin_log_related_acquire_r with "Hl"); eauto.
iIntros "Hl".
rel_rec_r.
rel_load_r.
rel_op_r.
rel_store_r. simpl.
rel_rec_r.
iApply (bin_log_related_release_r with "Hl"); eauto.
rel_apply_r (bin_log_related_release_r with "Hl"); eauto.
by iApply "Hlog".
Qed.
......@@ -150,8 +150,7 @@ Section CG_Counter.
iLöb as "IH".
rel_rec_l.
iPoseProof "H" as "H2". (* lolwhat *)
rel_bind_l (Load #x).
iApply (bin_log_related_load_l).
rel_load_l_atomic.
iMod "H" as (n) "[Hx [HR Hrev]]". iModIntro.
iExists (#nv n). iFrame. iNext. iIntros "Hx".
iDestruct "Hrev" as "[Hrev _]".
......@@ -160,8 +159,7 @@ Section CG_Counter.
{ iExists _. iFrame. } iModIntro. simpl.
rel_rec_l.
rel_op_l.
rel_bind_l (CAS _ _ _).
iApply (bin_log_related_cas_l); auto.
rel_cas_l_atomic.
iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl.
destruct (decide (n = n')); subst.
- iExists (#nv n'). iFrame.
......@@ -169,12 +167,12 @@ Section CG_Counter.
iIntros "_ !> Hx". simpl.
iDestruct "HQ" as "[_ HQ]".
iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. }
iApply bin_log_related_if_true_masked_l; auto.
rel_if_true_l. done.
- iExists (#nv n'). iFrame.
iSplitL; eauto; last first.
{ iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
iIntros "_ !> Hx". simpl.
iApply bin_log_related_if_false_masked_l; auto.
rel_if_false_l.
iDestruct "HQ" as "[HQ _]".
iMod ("HQ" with "[Hx HR]").
{ iExists _; iFrame. }
......@@ -192,7 +190,7 @@ Section CG_Counter.
iIntros "#H".
unfold counter_read. unlock. simpl.
rel_rec_l.
iApply bin_log_related_load_l.
rel_load_l_atomic.
iMod "H" as (n) "[Hx [HR Hfin]]". iModIntro.
iExists _; iFrame "Hx". iNext.
iIntros "Hx".
......@@ -267,8 +265,7 @@ Section CG_Counter.
iApply bin_log_related_arrow; try by (unlock; eauto).
iAlways. iIntros ([? ?]) "/= [% %]"; simplify_eq/=.
unlock. rel_rec_l. rel_rec_r.
rel_bind_r (newlock ())%E.
iApply (bin_log_related_newlock_r); auto; simpl.
rel_apply_r bin_log_related_newlock_r; auto.
iIntros (l) "Hl".
rel_rec_r.
rel_alloc_r as cnt' "Hcnt'".
......
......@@ -50,8 +50,7 @@ Section Refinement.
iIntros (?) "#Hs Hlog".
unfold rand. unlock. simpl.
rel_rec_l.
rel_bind_l (Alloc _).
iApply bin_log_related_alloc_l'; first eauto. iNext. iIntros (y) "Hy". simpl.
rel_alloc_l as y "Hy". simpl.
rel_rec_l.
iMod (inv_alloc choiceN _ ( b, y ↦ᵢ (#v b))%I with "[Hy]") as "#Hinv".
{ iNext. eauto. }
......@@ -65,10 +64,10 @@ Section Refinement.
done.
- simpl.
rel_rec_l.
rel_load_l under choiceN as "Hy" "Hcl".
iDestruct "Hy" as (b) "Hy".
iExists (#v b). iFrame.
iModIntro. iNext. iIntros "Hy".
rel_load_l_atomic.
iInv choiceN as (b) "Hy" "Hcl".
iExists (#v b). iFrame.
iModIntro. iNext. iIntros "Hy".
iMod ("Hcl" with "[Hy]").
{ iNext. iExists b. iFrame. }
done.
......@@ -104,8 +103,7 @@ Section Refinement.
rel_rec_l.
rel_store_l. simpl.
rel_rec_l.
rel_bind_l (rand ())%E.
iApply (rand_l with "Hs"); eauto. simpl.
rel_apply_l (rand_l with "Hs"); eauto.
by iApply "Hlog".
Qed.
......@@ -119,12 +117,11 @@ Section Refinement.
unfold earlyChoice. unlock.
rel_rec_r.
rel_bind_r (rand ())%E.
iApply (rand_r b with "Hspec"); eauto. simpl.
rel_apply_r (rand_r b with "Hspec"); eauto.
rel_rec_r.
rel_store_r. simpl.
rel_rec_r.
rel_vals; simpl; eauto.
rel_vals; eauto.
Qed.
Lemma prerefinement2 Δ Γ x x' n ρ :
......@@ -134,20 +131,19 @@ Section Refinement.
iIntros "#Hspec Hx Hx'".
unfold earlyChoice. unlock.
rel_rec_l.
rel_bind_l (rand ())%E.
iApply (rand_l with "Hspec"); eauto. simpl. iIntros (b).
rel_apply_l (rand_l with "Hspec"); eauto.
iIntros (b).
rel_rec_l.
unfold lateChoice. unlock.
rel_rec_r.
rel_store_r. simpl.
rel_rec_r.
rel_bind_r (rand ())%E.
iApply (rand_r b with "Hspec"); eauto. simpl.
rel_apply_r (rand_r b with "Hspec"); eauto.
rel_store_l. simpl.
rel_rec_l.
rel_vals; simpl; eauto.
rel_vals; eauto.
Qed.
End Refinement.
......@@ -671,8 +671,8 @@ Section masked.
Qed.
End masked.
Theorem binary_fundamental Γ e τ :
Γ ⊢ₜ e : τ (Γ e log e : τ)%I.
Theorem binary_fundamental Δ Γ e τ :
Γ ⊢ₜ e : τ ({,;Δ;Γ} e log e : τ)%I.
Proof. by eapply binary_fundamental_masked. Qed.
End fundamental.
......@@ -7,6 +7,7 @@ From iris_logrel.F_mu_ref_conc.proofmode Require Export tactics classes.
Set Default Proof Using "Type".
Import lang.
(** General tactics *)
Lemma tac_rel_bind_l `{logrelG Σ} e' K Δ E1 E2 Γ e t Δ' τ :
e = fill K e'
(Δ bin_log_related E1 E2 Δ' Γ (fill K e') t τ)
......@@ -57,18 +58,42 @@ Tactic Notation "rel_bind_l" open_constr(efoc) :=
| (* new goal *)
].
Ltac rel_bind_ctx_l K :=
eapply (tac_rel_bind_l _ K);
[reflexivity || tac_bind_helper
|].
Tactic Notation "rel_bind_r" open_constr(efoc) :=
iStartProof;
eapply (tac_rel_bind_r efoc);
[ tac_bind_helper
[tac_bind_helper
| (* new goal *)
].
Ltac rel_bind_ctx_r K :=
eapply (tac_rel_bind_r _ K);
[reflexivity || tac_bind_helper
|].
Tactic Notation "rel_vals" :=
iStartProof;
iApply bin_log_related_val; [ try solve_to_val | try solve_to_val | ].
iApply bin_log_related_val; [ try solve_to_val | try solve_to_val | simpl ].
Tactic Notation "rel_apply_l" open_constr(lem) :=
iStartProof;
rel_reshape_cont_l ltac:(fun K e =>
rel_bind_ctx_l K; iApply lem; tac_rel_done; try iNext; simpl_subst/=)
|| fail "rel_apply_l: Cannot apply " lem.
Tactic Notation "rel_apply_r" open_constr(lem) :=
iStartProof;
rel_reshape_cont_r ltac:(fun K e =>
rel_bind_ctx_r K; iApply lem; tac_rel_done; try iNext; simpl_subst/=)
|| fail "rel_apply_r: Cannot apply " lem.
(** Pure reductions *)
Lemma tac_rel_pure_l `{logrelG Σ} K e1 Δ' E1 E2 Δ Γ e e2 ϕ t τ (b : bool) :
e = fill K e1
PureExec ϕ e1 e2
......@@ -193,56 +218,7 @@ Tactic Notation "rel_fork_l" :=
|solve_closed
|simpl (* new goal *) ].
Lemma tac_rel_alloc_l `{logrelG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P e' v' K' Γ e t Δ' τ :
nclose N E1
envs_lookup i1 Δ1 = Some (p, inv N P)
E2 = E1 N
e = fill K' (Alloc e')
to_val e' = Some v'
envs_lookup nam Δ1 = None
envs_lookup nam_cl Δ1 = None
nam_cl nam
Δ2 = envs_snoc (envs_snoc Δ1 false nam ( P)%I) false nam_cl ( P ={E1 N,E1}= True)%I
(Δ2 |={E2}=> l,
(l ↦ᵢ v' - bin_log_related E2 E1 Δ' Γ (fill K' (Loc l)) t τ))
(Δ1 bin_log_related E1 E1 Δ' Γ e t τ).
Proof.
intros ??????????.
rewrite -(idemp uPred_and Δ1).
rewrite {1}envs_lookup_sound'. 2: eassumption.
rewrite uPred.sep_elim_l uPred.always_and_sep_l.
rewrite inv_open. 2: eassumption.
subst e.
rewrite -(bin_log_related_alloc_l Δ' Γ E1 E2). 2: eassumption.
rewrite fupd_frame_r.
rewrite -(fupd_trans E1 E2 E2).
subst E2.
apply fupd_mono.
rewrite -H9.
subst Δ2.
rewrite (envs_snoc_sound Δ1 false nam (P)) /=. 2: eassumption.
rewrite comm.
rewrite assoc.
rewrite uPred.wand_elim_l.
rewrite (envs_snoc_sound (envs_snoc Δ1 false nam ( P)) false nam_cl ( P ={E1 N,E1}= True)) //;
last first.
{ rewrite (envs_lookup_snoc_ne Δ1); eassumption. }
apply uPred.wand_elim_l.
Qed.
Tactic Notation "rel_alloc_l" "under" constr(N) "as" constr(nam) constr(nam_cl) :=
iStartProof;
eapply (tac_rel_alloc_l nam nam_cl);
[solve_ndisj || fail "rel_alloc_l: cannot prove 'nclose " N " ⊆ ?'"
|iAssumptionCore || fail "rel_alloc_l: cannot find inv " N " ?"
|try fast_done (* E2 = E1 \ N *)
|tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
|solve_to_val (* to_val e' = Some v *)
|try fast_done (* nam fresh *)
|try fast_done (* nam_cl fresh *)
|eauto (* nam =/= nam_cl *)
|env_cbv; reflexivity || fail "rel_alloc_l: this should not happen"
|(* new goal *)].
Tactic Notation "rel_alloc_l_atomic" := rel_apply_l bin_log_related_alloc_l.
Lemma tac_rel_alloc_l_simp `{logrelG Σ} Δ1 Δ2 E1 e' v' K' Γ e t Δ' τ :
e = fill K' (Alloc e')
......@@ -261,61 +237,13 @@ Qed.
Tactic Notation "rel_alloc_l" "as" ident(l) constr(H) :=
iStartProof;
eapply (tac_rel_alloc_l_simp);
[tac_bind_helper (* e = fill K' .. *)
|apply _ (* IntoLaterNEnvs _ _ _ *)
|solve_to_val (* to_val e' = Some v *)
|iIntros (l) H (* new goal *)].
eapply tac_rel_alloc_l_simp;
[tac_bind_helper (* e = fill K' .. *)
|apply _ (* IntoLaterNEnvs _ _ _ *)
|solve_to_val (* to_val e' = Some v *)
|iIntros (l) H (* new goal *)].
Lemma tac_rel_load_l `{logrelG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P l K' Γ e t Δ' τ :
nclose N E1
envs_lookup i1 Δ1 = Some (p, inv N P)
E2 = E1 N
e = fill K' (Load (Loc l))
envs_lookup nam Δ1 = None
envs_lookup nam_cl Δ1 = None
nam_cl nam
Δ2 = envs_snoc (envs_snoc Δ1 false nam ( P)%I) false nam_cl ( P ={E1 N,E1}= True)%I
(Δ2 |={E2}=> v, (l ↦ᵢ v)
(l ↦ᵢ v - bin_log_related E2 E1 Δ' Γ (fill K' (of_val v)) t τ))
(Δ1 bin_log_related E1 E1 Δ' Γ e t τ).
Proof.
intros ?????????.
rewrite -(idemp uPred_and Δ1).
rewrite {1}envs_lookup_sound'. 2: eassumption.
rewrite uPred.sep_elim_l uPred.always_and_sep_l.
rewrite inv_open. 2: eassumption.
subst e.
rewrite -(bin_log_related_load_l Δ' Γ E1 E2).
rewrite fupd_frame_r.
rewrite -(fupd_trans E1 E2 E2).
subst E2.
apply fupd_mono.
rewrite -H8.
subst Δ2.
rewrite (envs_snoc_sound Δ1 false nam (P)) /=. 2: eassumption.
rewrite comm.
rewrite assoc.
rewrite uPred.wand_elim_l.
rewrite (envs_snoc_sound (envs_snoc Δ1 false nam ( P)) false nam_cl ( P ={E1 N,E1}= True)) //;
last first.
{ rewrite (envs_lookup_snoc_ne Δ1); eassumption. }
rewrite uPred.wand_elim_l.
done.
Qed.
Tactic Notation "rel_load_l" "under" constr(N) "as" constr(nam) constr(nam_cl) :=
iStartProof;
eapply (tac_rel_load_l nam nam_cl);
[solve_ndisj || fail "rel_load_l: cannot prove 'nclose " N " ⊆ ?'"
|iAssumptionCore || fail "rel_load_l: cannot find inv " N " ?"
|try fast_done (* E2 = E1 \ N *)
|tac_bind_helper (* e = fill K' .. *)
|try fast_done (* nam fresh *)
|try fast_done (* nam_cl fresh *)
|eauto (* nam =/= nam_cl *)
|env_cbv; reflexivity || fail "rel_load_l: this should not happen"
|(* new goal *)].
Tactic Notation "rel_load_l_atomic" := rel_apply_l bin_log_related_load_l.
Lemma tac_rel_load_l_simp `{logrelG Σ} Δ1 Δ2 E1 i1 l v K' Γ e t Δ' τ :
e = fill K' (Load (Loc l))
......@@ -341,58 +269,7 @@ Tactic Notation "rel_load_l" :=
|iAssumptionCore || fail 3 "rel_load_l: cannot find ? ↦ᵢ ?"
| (* new goal *)].
Lemma tac_rel_store_l `{logrelG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P l e' v' K' Γ e t Δ' τ :
nclose N E1
envs_lookup i1 Δ1 = Some (p, inv N P)
E2 = E1 N
e = fill K' (Store (Loc l) e')
to_val e' = Some v'
envs_lookup nam Δ1 = None
envs_lookup nam_cl Δ1 = None
nam_cl nam
Δ2 = envs_snoc (envs_snoc Δ1 false nam ( P)%I) false nam_cl ( P ={E1 N,E1}= True)%I
(Δ2 |={E2}=> v, (l ↦ᵢ v)
(l ↦ᵢ v' - bin_log_related E2 E1 Δ' Γ (fill K' (Lit Unit)) t τ))
(Δ1 bin_log_related E1 E1 Δ' Γ e t τ).
Proof.
intros ??????????.
rewrite -(idemp uPred_and Δ1).
rewrite {1}envs_lookup_sound'. 2: eassumption.
rewrite uPred.sep_elim_l uPred.always_and_sep_l.
rewrite inv_open. 2: eassumption.
subst e.
rewrite -(bin_log_related_store_l Δ' Γ E1 E2). 2: eassumption.
rewrite fupd_frame_r.
rewrite -(fupd_trans E1 E2 E2).
subst E2.
apply fupd_mono.
rewrite -H9.
subst Δ2.
rewrite (envs_snoc_sound Δ1 false nam (P)) /=. 2: eassumption.
rewrite comm.
rewrite assoc.
rewrite uPred.wand_elim_l.
rewrite (envs_snoc_sound (envs_snoc Δ1 false nam ( P)) false nam_cl ( P ={E1 N,E1}= True)) //;
last first.
{ rewrite (envs_lookup_snoc_ne Δ1); eassumption. }
rewrite uPred.wand_elim_l.
done.
Qed.
Tactic Notation "rel_store_l" "under" constr(N) "as" constr(nam) constr(nam_cl) :=
iStartProof;
eapply (tac_rel_store_l nam nam_cl);
[solve_ndisj || fail "rel_store_l: cannot prove 'nclose " N " ⊆ ?'"
|iAssumptionCore || fail "rel_store_l: cannot find inv " N " ?"
|try fast_done (* E2 = E1 \ N *)
|tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
|solve_to_val (* to_val e' = Some v *)
|try fast_done (* nam fresh *)
|try fast_done (* nam_cl fresh *)
|eauto (* nam =/= nam_cl *)
|env_cbv; reflexivity || fail "rel_store_l: this should not happen"
|(* new goal *)].
Tactic Notation "rel_store_l_atomic" := rel_apply_l bin_log_related_store_l.
Lemma tac_rel_store_l_simp `{logrelG Σ} Δ1 Δ2 i1 E1 l v e' v' K' Γ e t Δ' τ :
e = fill K' (Store (Loc l) e')
......@@ -421,67 +298,7 @@ Tactic Notation "rel_store_l" :=
|env_cbv; reflexivity || fail "rel_store_l: this should not happen"
| (* new goal *)].
Lemma tac_rel_cas_l `{logrelG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P l e1 e2 v1 v2 K' Γ e t Δ' τ :
nclose N E1
envs_lookup i1 Δ1 = Some (p, inv N P)
E2 = E1 N
e = fill K' (CAS (Loc l) e1 e2)
to_val e1 = Some v1
to_val e2 = Some v2
envs_lookup nam Δ1 = None
envs_lookup nam_cl Δ1 = None
nam_cl nam
Δ2 = envs_snoc (envs_snoc Δ1 false nam ( P)%I) false nam_cl ( P ={E1 N,E1}= True)%I
(Δ2 |={E2}=> v, (l ↦ᵢ v)
((v v1 (l ↦ᵢ v - {E2,E1;Δ';Γ} fill K' (# false) log t : τ))
(v = v1 (l ↦ᵢ v2 - {E2,E1;Δ';Γ} fill K' (# true) log t : τ))))
(Δ1 bin_log_related E1 E1 Δ' Γ e t τ).
Proof.
intros ???????????.
rewrite -(idemp uPred_and Δ1).
rewrite {1}envs_lookup_sound'. 2: eassumption.
rewrite uPred.sep_elim_l uPred.always_and_sep_l.
rewrite inv_open. 2: eassumption.
subst e.
rewrite -(bin_log_related_cas_l Δ' Γ E1 E2); try eassumption.
rewrite fupd_frame_r.
rewrite -(fupd_trans E1 E2 E2).
subst E2.
apply fupd_mono.
subst Δ2.
rewrite (envs_snoc_sound Δ1 false nam (P)) /=. 2: eassumption.
rewrite comm.
rewrite assoc.
rewrite uPred.wand_elim_l.
rewrite (envs_snoc_sound (envs_snoc Δ1 false nam ( P)) false nam_cl ( P ={E1 N,E1}= True)) //;
last first.
{ rewrite (envs_lookup_snoc_ne Δ1); eassumption. }
rewrite H10.
rewrite uPred.wand_elim_l.
apply fupd_mono.
iDestruct 1 as (v) "[Hl Hv]". iExists v. iFrame "Hl".
iDestruct "Hv" as "[[% Hv] | [% Hv]]"; subst.
- iSplitL; last first; iIntros "%". by exfalso.
done.
- iSplitR; iIntros "%". by exfalso.
done.
Qed.
Tactic Notation "rel_cas_l" "under" constr(N) "as" constr(nam) constr(nam_cl) :=
iStartProof;
eapply (tac_rel_cas_l nam nam_cl);
[solve_ndisj || fail "rel_store_l: cannot prove 'nclose " N " ⊆ ?'"
|iAssumptionCore || fail "rel_store_l: cannot find inv " N " ?"
|try fast_done (* E2 = E1 \ N *)
|tac_bind_helper (* e = fill K' ... *)
|solve_to_val (* to_val e1 = Some .. *)
|solve_to_val (* to_val e2 = Some .. *)
|try fast_done (* nam fresh *)
|try fast_done (* nam_cl fresh *)
|eauto (* nam =/= nam_cl *)
|env_cbv; reflexivity || fail "rel_store_l: this should not happen"
|(* new goal *)].
Tactic Notation "rel_cas_l_atomic" := rel_apply_l bin_log_related_cas_l.
(********************************)
......@@ -663,9 +480,9 @@ Section test.
Definition storeFalse : val := λ: "y", "y" <- # false.
Lemma test_store Γ y y':
Lemma test_store Γ Δ y y':
inv choiceN (choice_inv y y')
- Γ (storeFalse (Fst (#y, 3))) log (storeFalse #y') : TUnit.
- {,;Δ;Γ} (storeFalse (Fst (#y, 3))) log (storeFalse #y') : TUnit.
Proof.
iIntros "#Hinv".
unfold storeFalse. unlock.
......@@ -673,15 +490,17 @@ Section test.
rel_rec_l.
rel_rec_r.
rel_store_l under choiceN as "Hs" "Hcl".
iDestruct "Hs" as (f) "[>Hy >Hy']". iExists _. iFrame "Hy".
iModIntro. iNext. iIntros "Hy".
rel_store_r. simpl.
rel_apply_l bin_log_related_store_l.
iInv choiceN as (f) ">[Hy Hy']" "Hcl".
iExists _. iFrame "Hy".
iModIntro. iNext. iIntros "Hy".
rel_store_r. simpl.
iMod ("Hcl" with "[Hy Hy']").
{ iNext. iExists _. iFrame. }
iApply bin_log_related_val; eauto.
rel_vals; eauto.
Qed.
End test.
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