Commit 96aa3f7a authored by Dan Frumin's avatar Dan Frumin

Add some rel_ tactics for the LHS, enough to do the late-early choice refinement

parent bbf10435
......@@ -280,12 +280,12 @@ Section CG_Counter.
Proof.
iIntros "#H".
Transparent FG_increment. unfold FG_increment. unlock. simpl.
iLöb as "IH".
iApply (bin_log_related_rec_l _ E1 K); auto. iNext. simpl.
iLöb as "IH".
rel_rec_l.
Opaque FG_increment.
rel_bind_l (Load (Loc x)).
iPoseProof "H" as "H2". (* lolwhat *)
Opaque bin_log_related.
rel_bind_l (Load (Loc x)).
iPoseProof "H" as "H2". (* lolwhat *)
iApply (bin_log_related_load_l).
iMod "H" as (n) "[Hx [HR Hrev]]". iModIntro.
iExists (#nv n). iFrame. iIntros "Hx".
......@@ -293,10 +293,8 @@ Section CG_Counter.
iApply fupd_logrel.
iMod ("Hrev" with "[HR Hx]").
{ iExists _. iFrame. } iModIntro. simpl.
iApply (bin_log_related_rec_l); auto. simpl.
iNext.
rel_bind_l (BinOp _ _ _).
iApply (bin_log_related_binop_l). iNext. simpl.
rel_rec_l.
rel_op_l. simpl.
rel_bind_l (CAS _ _ _).
iApply (bin_log_related_cas_l); auto.
iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl.
......
......@@ -139,18 +139,16 @@ Section Refinement.
Proof.
iIntros "#Hspec Hx Hx'".
unfold lateChoice, earlyChoice. unlock.
rel_rec_l. rel_rec_r.
rel_rec_l.
rel_rec_r.
rel_bind_l (#x <- _)%E.
iApply (bin_log_related_store_l' with "Hx"); eauto. iIntros "Hx".
simpl.
rel_store_l. simpl.
rel_rec_l.
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.
rel_rec_l.
rel_alloc_l as y "Hy". simpl.
rel_rec_l.
unfold rand. unlock.
rel_rec_r.
......@@ -161,11 +159,11 @@ Section Refinement.
{ iExists false. by iFrame. }
iMod (inv_alloc choiceN with "[Hinv]") as "#Hinv".
{ iNext. iApply "Hinv". }
rel_bind_r (Fork _).
iApply bin_log_related_fork_r; eauto. iIntros (i) "Hi".
rel_fork_r as i "Hi".
rel_rec_r.
rel_bind_l (Fork _).
iApply bin_log_related_fork_l;simpl. iModIntro.
rel_fork_l. iModIntro.
iSplitL "Hi".
- iNext.
iInv choiceN as (f) "[Hy Hy']" "Hcl".
......@@ -175,11 +173,10 @@ Section Refinement.
{ iNext. iExists true. by iFrame. }
done.
- rel_rec_l.
rel_rec_r.
iApply (bin_log_related_load_l _ _ _ []).
iInv choiceN as (f) "[Hy >Hy']" "Hcl". iModIntro.
iExists (#v f). iFrame. iIntros "Hy".
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. }
......@@ -187,8 +184,7 @@ Section Refinement.
rel_rec_r.
rel_store_r. simpl.
rel_seq_r.
iApply bin_log_related_val; eauto.
{ iIntros (Δ). iModIntro. simpl. eauto. }
rel_vals. eauto.
Qed.
Lemma refinement Γ ρ :
......
......@@ -29,7 +29,6 @@ Lemma tac_rel_bind_r `{heapIG Σ, !cfgSG Σ} t' K Δ E1 E2 Γ e t τ :
Proof. intros. eapply tac_rel_bind_gen; eauto. Qed.
Ltac tac_bind_helper :=
rewrite ?fill_app /=;
lazymatch goal with
| |- fill ?K ?e = fill _ ?efoc =>
reshape_expr e ltac:(fun K' e' =>
......@@ -51,6 +50,15 @@ Ltac rel_reshape_cont_r tac :=
reshape_expr e ltac:(fun K' e' => tac K' e')
end.
Ltac rel_reshape_cont_l tac :=
lazymatch goal with
| |- _ bin_log_related _ _ _ (fill ?K ?e) _ _ =>
reshape_expr e ltac:(fun K' e' =>
tac (K' ++ K) e')
| |- _ bin_log_related _ _ _ ?e _ _ =>
reshape_expr e ltac:(fun K' e' => tac K' e')
end.
Tactic Notation "rel_bind_l" open_constr(efoc) :=
iStartProof;
eapply (tac_rel_bind_l efoc);
......@@ -65,6 +73,195 @@ Tactic Notation "rel_bind_r" open_constr(efoc) :=
| (* new goal *)
].
Lemma tac_rel_rec_l `{heapIG Σ, !cfgSG Σ} Δ E1 Γ e K' f x ef e' efbody v eres t τ :
e = fill K' (App ef e')
ef = Rec f x efbody
Closed (x :b: f :b: ) efbody
to_val e' = Some v
eres = subst' f ef (subst' x e' efbody)
(Δ bin_log_related E1 E1 Γ (fill K' eres) t τ)
(Δ bin_log_related E1 E1 Γ e t τ).
Proof.
intros ??????.
subst e ef eres.
rewrite -(bin_log_related_rec_l Γ E1); eassumption.
Qed.
Tactic Notation "rel_rec_l" :=
iStartProof;
rel_reshape_cont_l ltac:(fun K e' =>
match eval hnf in e' with App ?e1 ?e2 =>
eapply (tac_rel_rec_l _ _ _ _ _ _ _ e1 e2);
[tac_bind_helper (* e = fill K' _ *)
|simpl; fast_done
|solve_closed
|fast_done (* to_val e' = Some v *)
|try fast_done (* eres = subst ... *)
|simpl; rewrite ?Closed_subst_id; iNext (* new goal *)]
end)
|| fail "rel_rec_l: cannot find '(λx.e) ..'".
Tactic Notation "rel_seq_l" := rel_rec_l.
Tactic Notation "rel_let_l" := rel_rec_l.
Lemma tac_rel_binop_l `{heapIG Σ, !cfgSG Σ} Δ E1 Γ e K' op a b eres t τ :
e = fill K' (BinOp op (#n a) (#n b))
eres = of_val (binop_eval op a b)
(Δ bin_log_related E1 E1 Γ (fill K' eres) t τ)
(Δ bin_log_related E1 E1 Γ e t τ).
Proof.
intros ???.
subst e eres.
rewrite -(bin_log_related_binop_l Γ E1); eassumption.
Qed.
Tactic Notation "rel_op_l" :=
iStartProof;
eapply (tac_rel_binop_l);
[tac_bind_helper (* e = fill K' ... *)
|simpl; reflexivity (* eres = of_val .. *)
|iNext (* new goal *)].
Lemma tac_rel_fork_l `{heapIG Σ, !cfgSG Σ} Δ1 E1 E2 e' K' Γ e t τ :
e = fill K' (Fork e')
Closed e'
(Δ1 |={E1,E2}=> WP e' {{ _ , True }} bin_log_related E2 E1 Γ (fill K' (Lit Unit)) t τ)
(Δ1 bin_log_related E1 E1 Γ e t τ).
Proof.
intros ???.
subst e.
rewrite -(bin_log_related_fork_l Γ E1 E2); eassumption.
Qed.
Tactic Notation "rel_fork_l" :=
iStartProof;
eapply (tac_rel_fork_l);
[tac_bind_helper || fail "rel_fork_l: cannot find 'fork'"
|solve_closed
|simpl (* new goal *) ].
Lemma tac_rel_alloc_l `{heapIG Σ, !cfgSG Σ} 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') *)
|try fast_done (* 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 *)].
Lemma tac_rel_alloc_l_simp `{heapIG Σ, !cfgSG Σ} Δ1 E1 e' v' K' Γ e t τ :
e = fill K' (Alloc e')
to_val e' = Some v'
(Δ1 l,
(l ↦ᵢ v' - bin_log_related E1 E1 Γ (fill K' (Loc l)) t τ))
(Δ1 bin_log_related E1 E1 Γ e t τ).
Proof.
intros ???.
subst e.
rewrite -(bin_log_related_alloc_l' Γ E1). 2: eassumption.
done.
Qed.
Tactic Notation "rel_alloc_l" "as" ident(l) constr(H) :=
iStartProof;
eapply (tac_rel_alloc_l_simp);
[tac_bind_helper (* e = fill K' .. *)
|try fast_done (* to_val e' = Some v *)
|iIntros (l) H (* new goal *)].
Lemma tac_rel_load_l `{heapIG Σ, !cfgSG Σ} 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 *)].
Lemma tac_rel_store_l `{heapIG Σ, !cfgSG Σ} 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)
......@@ -117,6 +314,118 @@ Tactic Notation "rel_store_l" "under" constr(N) "as" constr(nam) constr(nam_cl)
|env_cbv; reflexivity || fail "rel_store_l: this should not happen"
|(* new goal *)].
Lemma tac_rel_store_l_simp `{heapIG Σ, !cfgSG Σ} Δ1 Δ2 i1 E1 l v e' v' K' Γ e t τ :
e = fill K' (Store (Loc l) e')
to_val e' = Some v'
envs_lookup i1 Δ1 = Some (false, l ↦ᵢ v)%I
envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ᵢ v')) Δ1 = Some Δ2
(Δ2 bin_log_related E1 E1 Γ (fill K' (Lit Unit)) t τ)
(Δ1 bin_log_related E1 E1 Γ e t τ).
Proof.
intros ?????.
subst e.
rewrite envs_simple_replace_sound //; simpl.
rewrite right_id.
rewrite (uPred.later_intro (l ↦ᵢ v)%I).
rewrite (bin_log_related_store_l' Γ E1). 2: eassumption.
rewrite H4.
apply uPred.wand_elim_l.
Qed.
Tactic Notation "rel_store_l" :=
iStartProof;
eapply (tac_rel_store_l_simp);
[tac_bind_helper (* e = fill K' .. *)
|try fast_done (* to_val e' = Some v' *)
|iAssumptionCore || fail "rel_store_l: cannot find '? ↦ᵢ ?'"
|env_cbv; reflexivity || fail "rel_store_l: this should not happen"
| (* new goal *)].
Lemma tac_rel_cas_l `{heapIG Σ, !cfgSG Σ} 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' ... *)
|try fast_done (* to_val e1 = Some .. *)
|try fast_done (* 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 *)].
(********************************)
Lemma tac_rel_fork_r `{heapIG Σ, !cfgSG Σ} Δ1 E1 E2 t' K' Γ e t τ :
nclose specN E1
t = fill K' (Fork t')
Closed t'
(Δ1 i, i t' - bin_log_related E1 E2 Γ e (fill K' (Lit Unit)) τ)
(Δ1 bin_log_related E1 E2 Γ e t τ).
Proof.
intros ????.
subst t.
rewrite -(bin_log_related_fork_r Γ E1 E2); eassumption.
Qed.
Tactic Notation "rel_fork_r" "as" ident(i) constr(H) :=
iStartProof;
eapply (tac_rel_fork_r);
[solve_ndisj || fail "rel_fork_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper || fail "rel_fork_r: cannot find 'alloc'"
|solve_closed
|simpl; iIntros (i) H (* new goal *)].
Lemma tac_rel_store_r `{heapIG Σ, !cfgSG Σ} Δ1 Δ2 E1 E2 i1 l t' v' K' Γ e t τ v :
nclose specN E1
t = fill K' (Store (Loc l) t')
......@@ -265,30 +574,6 @@ Tactic Notation "rel_cas_suc_r" :=
|(* new goal *)].
Lemma tac_rel_rec_l `{heapIG Σ, !cfgSG Σ} Δ E1 Γ e K' f x ef e' efbody v eres t τ :
e = fill K' (App ef e')
ef = Rec f x efbody
Closed (x :b: f :b: ) efbody
to_val e' = Some v
eres = subst' f ef (subst' x e' efbody)
(Δ bin_log_related E1 E1 Γ (fill K' eres) t τ)
(Δ bin_log_related E1 E1 Γ e t τ).
Proof.
intros ??????.
subst e ef eres.
rewrite -(bin_log_related_rec_l Γ E1); eassumption.
Qed.
Tactic Notation "rel_rec_l" :=
iStartProof;
eapply (tac_rel_rec_l);
[tac_bind_helper (* e = fill K' _ *)
|try fast_done
|solve_closed
|try fast_done (* to_val e' = Some v *)
|try fast_done (* eres = subst ... *)
|iNext; simpl; rewrite ?Closed_subst_id (* new goal *)].
Lemma tac_rel_rec_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' f x ef e' efbody v eres t τ :
nclose specN E1
e = fill K' (App (Rec f x efbody) e')
......@@ -552,6 +837,12 @@ Tactic Notation "rel_op_r" :=
(* TODO: tac_rel_pack_r *)
Tactic Notation "rel_vals" :=
iStartProof;
iApply bin_log_related_val; [ try fast_done | try fast_done | ];
let d := fresh "Δ" in
iIntros (d); simpl.
Section test.
Context `{heapIG Σ, cfgSG Σ}.
......
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