From 975d454b744761e77211ee99564cf3156acc0cb1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 12 Dec 2016 20:46:59 +0100
Subject: [PATCH] Fix some FIXMEs.
---
theories/atomic_incr.v | 10 ++++------
theories/flat.v | 3 +--
theories/misc.v | 3 +--
theories/treiber.v | 32 +++++++++++---------------------
4 files changed, 17 insertions(+), 31 deletions(-)
diff --git a/theories/atomic_incr.v b/theories/atomic_incr.v
index d3bb577..65628b7 100644
--- a/theories/atomic_incr.v
+++ b/theories/atomic_incr.v
@@ -32,14 +32,12 @@ Section incr.
iLöb as "IH".
iIntros "!# HP".
wp_rec.
- (* FIXME: I should not have to apply wp_atomic manually here and below. *)
- wp_bind (! _)%E. iApply (wp_atomic _ ∅); first by eauto.
+ wp_bind (! _)%E.
iMod ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
- iModIntro. wp_load.
+ wp_load.
iMod ("Hvs'" with "Hl") as "HP".
iModIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
- iApply (wp_atomic _ ∅); first by eauto.
- iMod ("Hvs" with "HP") as (x') "[Hl Hvs']". iModIntro.
+ iMod ("Hvs" with "HP") as (x') "[Hl Hvs']".
destruct (decide (x = x')).
- subst.
iDestruct "Hvs'" as "[_ Hvs']".
@@ -68,7 +66,7 @@ Section user.
Lemma incr_2_safe:
∀ (x: Z), (WP incr_2 #x {{ _, True }})%I.
Proof.
- iIntros (x). iProof. (* FIXME: I did iIntros, this should not be needed. *)
+ iIntros (x) "". (* FIXME: I did iIntros, this should not be needed. *)
rewrite /incr_2 /=.
wp_lam.
wp_alloc l as "Hl".
diff --git a/theories/flat.v b/theories/flat.v
index eeca011..39b4370 100644
--- a/theories/flat.v
+++ b/theories/flat.v
@@ -245,8 +245,7 @@ Section proof.
iDestruct (ev_map_witness _ _ _ m2 with "[Hevm Hom2]") as %?; first by iFrame.
iDestruct (big_sepM_delete _ m2 with "HRp") as "[HRk HRp]"=>//.
iDestruct "HRk" as (?) "HRk".
- (* FIXME: Giving the types here should not be necessary. *)
- iDestruct (@mapsto_agree loc val with "[$HRk $Hp]") as %->.
+ iDestruct (@mapsto_agree with "[$HRk $Hp]") as %->.
iCombine "HRk" "Hp" as "Hp". wp_store.
(* now close the invariant *)
iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
diff --git a/theories/misc.v b/theories/misc.v
index deb897d..7d1b326 100644
--- a/theories/misc.v
+++ b/theories/misc.v
@@ -36,8 +36,7 @@ Section heap_extra.
p ↦{q1} a ∗ p ↦{q2} b ⊢ False.
Proof.
iIntros (?) "Hp".
- (* FIXME: If I dont give the types here, it loops. *)
- iDestruct (@mapsto_valid_2 loc val with "Hp") as %H'. done.
+ iDestruct (@mapsto_valid_2 with "Hp") as %H'. done.
Qed.
End heap_extra.
diff --git a/theories/treiber.v b/theories/treiber.v
index 43b99f4..817c085 100644
--- a/theories/treiber.v
+++ b/theories/treiber.v
@@ -63,18 +63,18 @@ Section proof.
+ iIntros (hd) "(Hxs & Hys)".
simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
iExFalso. iDestruct "Hxs" as (?) "Hhd'".
- (* FIXME: If I dont give the types here and below through this file, it loops. *)
- by iDestruct (@mapsto_agree loc val with "[$Hhd $Hhd']") as %?.
+ (* FIXME: If I dont use the @ here and below through this file, it loops. *)
+ by iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %?.
- induction ys as [|y ys' IHys'].
+ iIntros (hd) "(Hxs & Hys)".
simpl.
iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
iDestruct "Hys" as (?) "Hhd'".
- by iDestruct (@mapsto_agree loc val with "[$Hhd $Hhd']") as %?.
+ by iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %?.
+ iIntros (hd) "(Hxs & Hys)".
simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
iDestruct "Hys" as (? ?) "(Hhd' & Hys')".
- iDestruct (@mapsto_agree loc val with "[$Hhd $Hhd']") as %[= Heq].
+ iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %[= Heq].
subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
by subst.
Qed.
@@ -112,19 +112,16 @@ Section proof.
Lemma push_atomic_spec (s: loc) (x: val) :
push_triple s x.
Proof.
- iProof. rewrite /push_triple /atomic_triple.
+ rewrite /push_triple /atomic_triple.
iIntros (P Q) "#Hvs".
iLöb as "IH". iIntros "!# HP". wp_rec.
wp_let. wp_bind (! _)%E.
- (* FIXME: I should not have to apply wp_atomic manually here and below. *)
- iApply (wp_atomic _ ∅); first by eauto.
- iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]". iModIntro.
+ iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
wp_bind (CAS _ _ _)%E.
- iApply (wp_atomic _ ∅); first by eauto.
iMod ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']".
- iModIntro. destruct (decide (hd = hd')) as [->|Hneq].
+ destruct (decide (hd = hd')) as [->|Hneq].
* wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" $! #() with "[-]") as "HQ".
{ iExists l. iSplitR; first done. by iFrame. }
@@ -150,15 +147,12 @@ Section proof.
Lemma pop_atomic_spec (s: loc):
pop_triple s.
Proof.
- iProof.
rewrite /pop_triple /atomic_triple.
iIntros (P Q) "#Hvs".
iLöb as "IH". iIntros "!# HP". wp_rec.
wp_bind (! _)%E.
- (* FIXME: I should not have to apply wp_atomic manually here and below. *)
- iApply (wp_atomic _ ∅); first by eauto.
iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] Hvs']".
- iModIntro. destruct xs as [|y' xs'].
+ destruct xs as [|y' xs'].
- simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']".
iDestruct "Hhd" as (q) "[Hhd Hhd']".
iMod ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
@@ -172,18 +166,16 @@ Section proof.
{ iFrame. iExists hd', (q / 2)%Qp. by iFrame. }
iModIntro. wp_let. wp_load. wp_match. wp_proj.
wp_bind (CAS _ _ _).
- (* FIXME: I should not have to apply wp_atomic manually here and below. *)
- iApply (wp_atomic _ ∅); first by eauto.
iMod ("Hvs" with "HP") as ([xs hd'']) "[[Hs Hhd''] Hvs']".
- iModIntro. destruct (decide (hd = hd'')) as [->|Hneq].
+ destruct (decide (hd = hd'')) as [->|Hneq].
+ wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" $! (SOMEV y') with "[-]") as "HQ".
{ iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
destruct xs as [|x' xs''].
- simpl. iDestruct "Hhd''" as (?) "H".
- iExFalso. by iDestruct (@mapsto_agree loc val with "[$Hhd1 $H]") as %?.
+ iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1 $H]") as %?.
- simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
- iDestruct (@mapsto_agree loc val with "[$Hhd1 $Hhd'']") as %[=].
+ iDestruct (@mapsto_agree with "[$Hhd1 $Hhd'']") as %[=].
subst.
iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
repeat (iSplitR "Hxs1 Hs"; first done).
@@ -193,6 +185,4 @@ Section proof.
iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
iModIntro. wp_if. by iApply "IH".
Qed.
-
End proof.
-
--
GitLab