Commit 8d103530 authored by Dan Frumin's avatar Dan Frumin

Strengthen the Load rule

parent 94f9e811
......@@ -167,7 +167,7 @@ Section CG_Counter.
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".
iExists (#nv n). iFrame. iNext. iIntros "Hx".
rewrite ->uPred.and_elim_l.
iApply fupd_logrel.
iMod ("Hrev" with "[HR Hx]").
......@@ -208,7 +208,7 @@ Section CG_Counter.
iApply (bin_log_related_rec_l _ E1 _); auto. iNext. simpl.
iApply (bin_log_related_load_l).
iMod "H" as (n) "[Hx [HR Hfin]]". iModIntro.
iExists _; iFrame "Hx".
iExists _; iFrame "Hx". iNext.
iIntros "Hx".
rewrite ->uPred.and_elim_r. (* TODO: a tactic for this *)
iApply "Hfin". by iFrame.
......
......@@ -67,8 +67,8 @@ Section Refinement.
rel_rec_l.
rel_load_l under choiceN as "Hy" "Hcl".
iDestruct "Hy" as (b) "Hy".
iExists (#v b). iFrame.
iModIntro. iIntros "Hy".
iExists (#v b). iFrame.
iModIntro. iNext. iIntros "Hy".
iMod ("Hcl" with "[Hy]").
{ iNext. iExists b. iFrame. }
done.
......
......@@ -228,7 +228,7 @@ Lemma tac_rel_load_l `{heapIG Σ, !cfgSG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P l
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 τ))
(l ↦ᵢ v - bin_log_related E2 E1 Γ (fill K' (of_val v)) t τ))
(Δ1 bin_log_related E1 E1 Γ e t τ).
Proof.
intros ?????????.
......
......@@ -431,7 +431,7 @@ Section properties.
Lemma bin_log_related_load_l Γ E1 E2 K l t τ :
(|={E1,E2}=> v',
(l ↦ᵢ v')
(l ↦ᵢ v' - ({ E2,E1; Γ } fill K (of_val v') log t : τ)))%I
(l ↦ᵢ v' - ({ E2,E1; Γ } fill K (of_val v') log t : τ)))%I
- {E1,E1;Γ} fill K (Load (Loc l)) log t : τ.
Proof.
iIntros "Hlog".
......
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