diff --git a/theories/logrel/rules.v b/theories/logrel/rules.v index 0dd952596a2b985695ad6ced28d3fb0d669b4c17..71e76a101fbc9a4d65f8354dd76347c279e0c603 100644 --- a/theories/logrel/rules.v +++ b/theories/logrel/rules.v @@ -271,22 +271,21 @@ Section properties. done. Qed. - Lemma bin_log_related_load_r Δ Γ E1 E2 K l q v' t τ + Lemma bin_log_related_load_r Δ Γ E1 E2 K l q v t τ (Hmasked : nclose specN ⊆ E1) : - l ↦ₛ{q} v' -∗ - (l ↦ₛ{q} v' -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (of_val v') : τ) - -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Load (# l)) : τ. + l ↦ₛ{q} v -∗ + (l ↦ₛ{q} v -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (of_val v) : τ) + -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ (fill K !#l) : τ. Proof. iIntros "Hl Hlog". - pose (Φ := (fun w => ⌜w = v'⌝ ∗ l ↦ₛ{q} v')%I). + pose (Φ := (fun w => ⌜w = v⌝ ∗ l ↦ₛ{q} v)%I). iApply (bin_log_related_step_r Φ with "[Hl]"); eauto. { cbv[Φ]. - iIntros (ρ j K') "#Hs Hj /=". iExists v'. + iIntros (ρ j K') "#Hs Hj /=". iExists v. tp_load j. iFrame. eauto. } - iIntros (v) "[% Hl]"; subst. - iApply "Hlog". - done. + iIntros (?) "[% Hl]"; subst. + by iApply "Hlog". Qed. Lemma bin_log_related_store_r Δ Γ E1 E2 K l e e' v v' τ @@ -603,14 +602,14 @@ Section properties. iApply (wp_load with "Hl"); auto. Qed. - Lemma bin_log_related_load_l' Δ Γ E1 K l q v' t τ : - ▷ l ↦ᵢ{q} v' -∗ - ▷ (l ↦ᵢ{q} v' -∗ ({E1;Δ;Γ} ⊨ fill K (of_val v') ≤log≤ t : τ)) + Lemma bin_log_related_load_l' Δ Γ E1 K l q v t τ : + ▷ l ↦ᵢ{q} v -∗ + ▷ (l ↦ᵢ{q} v -∗ ({E1;Δ;Γ} ⊨ fill K (of_val v) ≤log≤ t : τ)) -∗ {E1;Δ;Γ} ⊨ fill K !#l ≤log≤ t : τ. Proof. iIntros "Hl Hlog". iApply (bin_log_related_load_l); auto. - iExists v'. + iExists v. iModIntro. by iFrame. Qed.