Commit 61f69839 authored by Dan Frumin's avatar Dan Frumin

Update a relational rule for store

parent ae47b227
......@@ -459,7 +459,7 @@ Lemma tac_rel_store_l `{logrelG Σ} nam nam_cl Δ1 Δ2 E1 E2 p i1 N P l e' v' K'
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 τ))
(l ↦ᵢ v' - bin_log_related E2 E1 Δ' Γ (fill K' (Lit Unit)) t τ))
(Δ1 bin_log_related E1 E1 Δ' Γ e t τ).
Proof.
intros ??????????.
......@@ -1059,7 +1059,7 @@ Section test.
rel_store_l under choiceN as "Hs" "Hcl".
iDestruct "Hs" as (f) "[>Hy >Hy']". iExists _. iFrame "Hy".
iModIntro. iIntros "Hy".
iModIntro. iNext. iIntros "Hy".
rel_store_r. simpl.
iMod ("Hcl" with "[Hy Hy']").
......
......@@ -316,7 +316,7 @@ Section properties.
rewrite /env_subst fill_subst /=. rewrite of_val_subst_p.
done.
Qed.
Lemma bin_log_related_wp_atomic_l Δ Γ (E1 E2 : coPset) K e1 e2 τ
(Hatomic : atomic e1)
(Hclosed1 : Closed e1) :
......@@ -340,7 +340,7 @@ Section properties.
rewrite /env_subst fill_subst /=. rewrite of_val_subst_p.
by iMod "Hlog".
Qed.
Lemma bin_log_related_step_atomic_l {A} (Φ : A val iProp Σ) Δ Γ E1 E2 K e1 e2 τ
(Hatomic : atomic e1)
(Hclosed1 : Closed e1) :
......@@ -436,7 +436,7 @@ Section properties.
Lemma bin_log_related_store_l Δ Γ E1 E2 K l e v' t τ :
(to_val e = Some v')
(|={E1,E2}=> v, (l ↦ᵢ v)
(l ↦ᵢ v' - {E2,E1;Δ;Γ} fill K (Lit Unit) log t : τ))
(l ↦ᵢ v' - {E2,E1;Δ;Γ} fill K (Lit Unit) log t : τ))
- {E1,E1;Δ;Γ} fill K (Store (Loc l) e) log t : τ.
Proof.
iIntros (?) "Hlog".
......
......@@ -31,3 +31,4 @@ F_mu_ref_conc/examples/bit.v
#F_mu_ref_conc/examples/stack/CG_stack.v
#F_mu_ref_conc/examples/stack/FG_stack.v
#F_mu_ref_conc/examples/stack/refinement.v
F_mu_ref_conc/examples/typetest.v
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