Commit 975d454b authored by Robbert Krebbers's avatar Robbert Krebbers

Fix some FIXMEs.

parent fc4ae5bc
Pipeline #3321 failed with stage
in 1 minute and 22 seconds
...@@ -32,14 +32,12 @@ Section incr. ...@@ -32,14 +32,12 @@ Section incr.
iLöb as "IH". iLöb as "IH".
iIntros "!# HP". iIntros "!# HP".
wp_rec. wp_rec.
(* FIXME: I should not have to apply wp_atomic manually here and below. *) wp_bind (! _)%E.
wp_bind (! _)%E. iApply (wp_atomic _ ); first by eauto.
iMod ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]". iMod ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
iModIntro. wp_load. wp_load.
iMod ("Hvs'" with "Hl") as "HP". iMod ("Hvs'" with "Hl") as "HP".
iModIntro. wp_let. wp_bind (CAS _ _ _). wp_op. iModIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
iApply (wp_atomic _ ); first by eauto. iMod ("Hvs" with "HP") as (x') "[Hl Hvs']".
iMod ("Hvs" with "HP") as (x') "[Hl Hvs']". iModIntro.
destruct (decide (x = x')). destruct (decide (x = x')).
- subst. - subst.
iDestruct "Hvs'" as "[_ Hvs']". iDestruct "Hvs'" as "[_ Hvs']".
...@@ -68,7 +66,7 @@ Section user. ...@@ -68,7 +66,7 @@ Section user.
Lemma incr_2_safe: Lemma incr_2_safe:
(x: Z), (WP incr_2 #x {{ _, True }})%I. (x: Z), (WP incr_2 #x {{ _, True }})%I.
Proof. 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 /=. rewrite /incr_2 /=.
wp_lam. wp_lam.
wp_alloc l as "Hl". wp_alloc l as "Hl".
......
...@@ -245,8 +245,7 @@ Section proof. ...@@ -245,8 +245,7 @@ Section proof.
iDestruct (ev_map_witness _ _ _ m2 with "[Hevm Hom2]") as %?; first by iFrame. iDestruct (ev_map_witness _ _ _ m2 with "[Hevm Hom2]") as %?; first by iFrame.
iDestruct (big_sepM_delete _ m2 with "HRp") as "[HRk HRp]"=>//. iDestruct (big_sepM_delete _ m2 with "HRp") as "[HRk HRp]"=>//.
iDestruct "HRk" as (?) "HRk". iDestruct "HRk" as (?) "HRk".
(* FIXME: Giving the types here should not be necessary. *) iDestruct (@mapsto_agree with "[$HRk $Hp]") as %->.
iDestruct (@mapsto_agree loc val with "[$HRk $Hp]") as %->.
iCombine "HRk" "Hp" as "Hp". wp_store. iCombine "HRk" "Hp" as "Hp". wp_store.
(* now close the invariant *) (* now close the invariant *)
iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame. iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
......
...@@ -36,8 +36,7 @@ Section heap_extra. ...@@ -36,8 +36,7 @@ Section heap_extra.
p {q1} a p {q2} b False. p {q1} a p {q2} b False.
Proof. Proof.
iIntros (?) "Hp". iIntros (?) "Hp".
(* FIXME: If I dont give the types here, it loops. *) iDestruct (@mapsto_valid_2 with "Hp") as %H'. done.
iDestruct (@mapsto_valid_2 loc val with "Hp") as %H'. done.
Qed. Qed.
End heap_extra. End heap_extra.
......
...@@ -63,18 +63,18 @@ Section proof. ...@@ -63,18 +63,18 @@ Section proof.
+ iIntros (hd) "(Hxs & Hys)". + iIntros (hd) "(Hxs & Hys)".
simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')". simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
iExFalso. iDestruct "Hxs" as (?) "Hhd'". iExFalso. iDestruct "Hxs" as (?) "Hhd'".
(* FIXME: If I dont give the types here and below through this file, it loops. *) (* FIXME: If I dont use the @ here and below through this file, it loops. *)
by iDestruct (@mapsto_agree loc val with "[$Hhd $Hhd']") as %?. by iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %?.
- induction ys as [|y ys' IHys']. - induction ys as [|y ys' IHys'].
+ iIntros (hd) "(Hxs & Hys)". + iIntros (hd) "(Hxs & Hys)".
simpl. simpl.
iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)". iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
iDestruct "Hys" 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)". + iIntros (hd) "(Hxs & Hys)".
simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')". simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
iDestruct "Hys" as (? ?) "(Hhd' & Hys')". 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. subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
by subst. by subst.
Qed. Qed.
...@@ -112,19 +112,16 @@ Section proof. ...@@ -112,19 +112,16 @@ Section proof.
Lemma push_atomic_spec (s: loc) (x: val) : Lemma push_atomic_spec (s: loc) (x: val) :
push_triple s x. push_triple s x.
Proof. Proof.
iProof. rewrite /push_triple /atomic_triple. rewrite /push_triple /atomic_triple.
iIntros (P Q) "#Hvs". iIntros (P Q) "#Hvs".
iLöb as "IH". iIntros "!# HP". wp_rec. iLöb as "IH". iIntros "!# HP". wp_rec.
wp_let. wp_bind (! _)%E. wp_let. wp_bind (! _)%E.
(* FIXME: I should not have to apply wp_atomic manually here and below. *) iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
iApply (wp_atomic _ ); first by eauto.
iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]". iModIntro.
wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame. wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
iModIntro. wp_let. wp_alloc l as "Hl". wp_let. iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
wp_bind (CAS _ _ _)%E. wp_bind (CAS _ _ _)%E.
iApply (wp_atomic _ ); first by eauto.
iMod ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']". 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']". * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" $! #() with "[-]") as "HQ". iMod ("Hvs'" $! #() with "[-]") as "HQ".
{ iExists l. iSplitR; first done. by iFrame. } { iExists l. iSplitR; first done. by iFrame. }
...@@ -150,15 +147,12 @@ Section proof. ...@@ -150,15 +147,12 @@ Section proof.
Lemma pop_atomic_spec (s: loc): Lemma pop_atomic_spec (s: loc):
pop_triple s. pop_triple s.
Proof. Proof.
iProof.
rewrite /pop_triple /atomic_triple. rewrite /pop_triple /atomic_triple.
iIntros (P Q) "#Hvs". iIntros (P Q) "#Hvs".
iLöb as "IH". iIntros "!# HP". wp_rec. iLöb as "IH". iIntros "!# HP". wp_rec.
wp_bind (! _)%E. 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']". 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']". - simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']".
iDestruct "Hhd" as (q) "[Hhd Hhd']". iDestruct "Hhd" as (q) "[Hhd Hhd']".
iMod ("Hvs'" $! NONEV with "[-Hhd]") as "HQ". iMod ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
...@@ -172,18 +166,16 @@ Section proof. ...@@ -172,18 +166,16 @@ Section proof.
{ iFrame. iExists hd', (q / 2)%Qp. by iFrame. } { iFrame. iExists hd', (q / 2)%Qp. by iFrame. }
iModIntro. wp_let. wp_load. wp_match. wp_proj. iModIntro. wp_let. wp_load. wp_match. wp_proj.
wp_bind (CAS _ _ _). 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']". 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']". + wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" $! (SOMEV y') with "[-]") as "HQ". iMod ("Hvs'" $! (SOMEV y') with "[-]") as "HQ".
{ iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'. { iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
destruct xs as [|x' xs'']. destruct xs as [|x' xs''].
- simpl. iDestruct "Hhd''" as (?) "H". - 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'')". - simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
iDestruct (@mapsto_agree loc val with "[$Hhd1 $Hhd'']") as %[=]. iDestruct (@mapsto_agree with "[$Hhd1 $Hhd'']") as %[=].
subst. subst.
iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst. iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
repeat (iSplitR "Hxs1 Hs"; first done). repeat (iSplitR "Hxs1 Hs"; first done).
...@@ -193,6 +185,4 @@ Section proof. ...@@ -193,6 +185,4 @@ Section proof.
iMod ("Hvs'" with "[-]") as "HP"; first by iFrame. iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
iModIntro. wp_if. by iApply "IH". iModIntro. wp_if. by iApply "IH".
Qed. Qed.
End proof. End proof.
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