Commit bbf10435 authored by Dan Frumin's avatar Dan Frumin

Add the rel_ tactics for the RHS and apply them in the examples

parent e13439ec
......@@ -71,9 +71,7 @@ Section CG_Counter.
unfold CG_increment. unlock.
rel_rec_r.
rel_rec_r.
rel_bind_r (Load (Loc x)).
iApply (bin_log_related_load_r with "Hx");auto.
iIntros "Hx". simpl.
rel_load_r.
rel_op_r.
rel_store_r.
by iApply "Hlog".
......@@ -264,8 +262,9 @@ Section CG_Counter.
Proof.
iIntros "Hx Hlog".
Transparent counter_read. unfold counter_read. unlock. simpl.
rel_rec_r.
iApply (bin_log_related_load_r with "Hx"); auto.
rel_rec_r.
rel_load_r.
by iApply "Hlog".
Opaque counter_read.
Qed.
......
......@@ -115,19 +115,36 @@ Section Refinement.
simpl. iApply ("Hlog" with "Hx").
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. *)
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.
iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl. rewrite !Closed_subst_id.
iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl. rewrite !Closed_subst_id.
rel_rec_l. rel_rec_r.
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.
rel_rec_l.
unfold rand at 1. unlock.
iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
......@@ -135,12 +152,10 @@ Section Refinement.
iApply bin_log_related_alloc_l'; eauto. iIntros (y) "Hy". simpl.
iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
rel_bind_r (rand #())%E. unfold rand. unlock.
iApply (bin_log_related_rec_r _ _); eauto. simpl.
rel_bind_r (Alloc _).
iApply bin_log_related_alloc_r; eauto. iIntros (y') "Hy'". simpl.
rel_bind_r (App _ #y')%E.
iApply (bin_log_related_rec_r _ _); eauto. simpl.
unfold rand. unlock.
rel_rec_r.
rel_alloc_r as y' "Hy'".
rel_rec_r.
iAssert (choice_inv y y') with "[Hy Hy']" as "Hinv".
{ iExists false. by iFrame. }
......@@ -150,7 +165,7 @@ Section Refinement.
iApply bin_log_related_fork_r; eauto. iIntros (i) "Hi".
rel_bind_l (Fork _).
iApply bin_log_related_fork_l. iModIntro.
iApply bin_log_related_fork_l;simpl. iModIntro.
iSplitL "Hi".
- iNext.
iInv choiceN as (f) "[Hy Hy']" "Hcl".
......@@ -159,24 +174,19 @@ Section Refinement.
iMod ("Hcl" with "[Hy Hy']").
{ iNext. iExists true. by iFrame. }
done.
- simpl.
iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl.
rel_bind_r (App _ #())%E.
iApply bin_log_related_rec_r; eauto. simpl.
rel_bind_r (Load #y')%E.
- 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".
iApply (bin_log_related_load_r with "Hy'"). { solve_ndisj. }
iIntros "Hy'".
rel_load_r.
iMod ("Hcl" with "[Hy Hy']").
{ iNext. iExists f. iFrame. }
simpl.
iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl.
rel_bind_r (Store _ _).
iApply (bin_log_related_store_r with "Hx'"); eauto. iIntros "Hx'". simpl.
iApply (bin_log_related_rec_r _ _ _ []); eauto. simpl.
rel_rec_r.
rel_store_r. simpl.
rel_seq_r.
iApply bin_log_related_val; eauto.
{ iIntros (Δ). iModIntro. simpl. eauto. }
Qed.
......
......@@ -102,9 +102,7 @@ Section proof.
iIntros "Hl Hlog".
unfold acquire.
rel_rec_r.
rel_bind_r (CAS _ _ _).
iApply (bin_log_related_cas_suc_r with "Hl"); auto.
iIntros "Hl". simpl.
rel_cas_suc_r. simpl.
rel_if_r.
by iApply "Hlog".
Qed.
......
......@@ -170,6 +170,100 @@ Tactic Notation "rel_alloc_r" :=
let H := iFresh "H" in
rel_alloc_r as l H.
Lemma tac_rel_load_r `{heapIG Σ, !cfgSG Σ} Δ1 Δ2 E1 E2 i1 l K' Γ e t τ v :
nclose specN E1
t = fill K' (Load (Loc l))
envs_lookup i1 Δ1 = Some (false, l ↦ₛ v)%I
envs_simple_replace i1 false
(Esnoc Enil i1 (l ↦ₛ v)%I) Δ1 = Some Δ2
(Δ2 bin_log_related E1 E2 Γ e (fill K' (of_val v)) τ)
(Δ1 bin_log_related E1 E2 Γ e t τ).
Proof.
intros ?????.
rewrite (envs_simple_replace_sound Δ1 Δ2 i1) //; simpl.
rewrite right_id.
subst t.
rewrite {1}(bin_log_related_load_r Γ K' E1 E2 l); [ | eassumption ].
rewrite H4.
apply uPred.wand_elim_l.
Qed.
Tactic Notation "rel_load_r" :=
iStartProof;
eapply (tac_rel_load_r);
[solve_ndisj || fail "rel_load_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper (* e = fill K' (Store (Loc l) e') *)
|iAssumptionCore || fail "rel_load_l: cannot find ? ↦ₛ ?"
|env_cbv; reflexivity || fail "rel_load_r: this should not happen"
|simpl (* new goal *)].
Lemma tac_rel_cas_fail_r `{heapIG Σ, !cfgSG Σ} Δ1 Δ2 E1 E2 i1 l K' Γ e t e1 e2 v1 v2 τ v :
nclose specN E1
t = fill K' (CAS (Loc l) e1 e2)
to_val e1 = Some v1
to_val e2 = Some v2
envs_lookup i1 Δ1 = Some (false, l ↦ₛ v)%I
v v1
envs_simple_replace i1 false
(Esnoc Enil i1 (l ↦ₛ v)%I) Δ1 = Some Δ2
(Δ2 bin_log_related E1 E2 Γ e (fill K' (# false)) τ)
(Δ1 bin_log_related E1 E2 Γ e t τ).
Proof.
intros ????????.
rewrite (envs_simple_replace_sound Δ1 Δ2 i1) //; simpl.
rewrite right_id.
subst t.
rewrite {1}(bin_log_related_cas_fail_r Γ E1 E2 _ l e1 e2 v1 v2 v); eauto.
rewrite H7.
apply uPred.wand_elim_l.
Qed.
Tactic Notation "rel_cas_fail_r" :=
iStartProof;
eapply (tac_rel_cas_fail_r);
[solve_ndisj || fail "rel_cas_fail_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper || fail "rel_cas_fail_r: cannot find 'CAS ..'"
|try fast_done
|try fast_done
|iAssumptionCore || fail "rel_cas_fail_l: cannot find ? ↦ₛ ?"
|try fast_done (* v v1 *)
|env_cbv; reflexivity || fail "rel_load_r: this should not happen"
|(* new goal *)].
Lemma tac_rel_cas_suc_r `{heapIG Σ, !cfgSG Σ} Δ1 Δ2 E1 E2 i1 l K' Γ e t e1 e2 v1 v2 τ v :
nclose specN E1
t = fill K' (CAS (Loc l) e1 e2)
to_val e1 = Some v1
to_val e2 = Some v2
envs_lookup i1 Δ1 = Some (false, l ↦ₛ v)%I
v = v1
envs_simple_replace i1 false
(Esnoc Enil i1 (l ↦ₛ v2)%I) Δ1 = Some Δ2
(Δ2 bin_log_related E1 E2 Γ e (fill K' (# true)) τ)
(Δ1 bin_log_related E1 E2 Γ e t τ).
Proof.
intros ????????.
rewrite (envs_simple_replace_sound Δ1 Δ2 i1) //; simpl.
rewrite right_id.
subst t.
rewrite {1}(bin_log_related_cas_suc_r Γ E1 E2 _ l e1 e2 v1 v2 v); eauto.
rewrite H7.
apply uPred.wand_elim_l.
Qed.
Tactic Notation "rel_cas_suc_r" :=
iStartProof;
eapply (tac_rel_cas_suc_r);
[solve_ndisj || fail "rel_cas_suc_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper || fail "rel_cas_suc_r: cannot find 'CAS ..'"
|try fast_done
|try fast_done
|iAssumptionCore || fail "rel_cas_suc_l: cannot find ? ↦ₛ ?"
|try fast_done (* v = v1 *)
|env_cbv; reflexivity || fail "rel_load_r: this should not happen"
|(* 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')
......
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