Commit dc297188 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove some weird uses of wp_atomic.

parent aaafdfea
...@@ -88,17 +88,13 @@ Section fundamental. ...@@ -88,17 +88,13 @@ Section fundamental.
iNext; iPvsIntro. by rewrite -interp_subst. iNext; iPvsIntro. by rewrite -interp_subst.
- (* Alloc *) - (* Alloc *)
smart_wp_bind AllocCtx v "#Hv" IHtyped; cbn. iClear "HΓ". smart_wp_bind AllocCtx v "#Hv" IHtyped; cbn. iClear "HΓ".
iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|].
iPvsIntro.
iApply wp_alloc; auto 1 using to_of_val. iApply wp_alloc; auto 1 using to_of_val.
iFrame "Hheap". iNext. iIntros {l} "Hl". iPvsIntro. iIntros "{$Hheap} >"; iIntros {l} "Hl".
iPvs (inv_alloc _ with "[Hl]") as "HN"; iPvs (inv_alloc _ with "[Hl]") as "HN";
[| | iPvsIntro; iExists _; iSplit; trivial]; eauto. [| | iPvsIntro; iExists _; iSplit; trivial]; eauto.
- (* Load *) - (* Load *)
smart_wp_bind LoadCtx v "#Hv" IHtyped; cbn. iClear "HΓ". smart_wp_bind LoadCtx v "#Hv" IHtyped; cbn. iClear "HΓ".
iDestruct "Hv" as {l} "[% #Hv]"; subst. iDestruct "Hv" as {l} "[% #Hv]"; subst.
iApply wp_atomic; cbn; eauto using to_of_val.
iPvsIntro.
iInv (logN .@ l) as {w} "[Hw1 #Hw2]". iInv (logN .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj. iApply (wp_load _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj.
iIntros "{$Hw1} > Hw1". iPvsIntro. iSplitL; eauto. iIntros "{$Hw1} > Hw1". iPvsIntro. iSplitL; eauto.
...@@ -106,12 +102,8 @@ Section fundamental. ...@@ -106,12 +102,8 @@ Section fundamental.
smart_wp_bind (StoreLCtx _) v "#Hv" IHtyped1; cbn. smart_wp_bind (StoreLCtx _) v "#Hv" IHtyped1; cbn.
smart_wp_bind (StoreRCtx _) w "#Hw" IHtyped2; cbn. iClear "HΓ". smart_wp_bind (StoreRCtx _) w "#Hw" IHtyped2; cbn. iClear "HΓ".
iDestruct "Hv" as {l} "[% #Hv]"; subst. iDestruct "Hv" as {l} "[% #Hv]"; subst.
iApply wp_atomic; cbn; [trivial| rewrite ?to_of_val; auto |]. iInv (logN .@ l) as {z} "[Hz1 #Hz2]"; [cbn; eauto 10 using to_of_val|].
iPvsIntro.
iInv (logN .@ l) as {z} "[Hz1 #Hz2]".
eapply bool_decide_spec; eauto using to_of_val.
iApply wp_store; auto using to_of_val. solve_ndisj. iApply wp_store; auto using to_of_val. solve_ndisj.
iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro. iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro; iSplitL; eauto 10.
iSplitL; eauto 10.
Qed. Qed.
End fundamental. End fundamental.
...@@ -107,18 +107,13 @@ Section typed_interp. ...@@ -107,18 +107,13 @@ Section typed_interp.
iApply wp_wand_l. iSplitL; [|iApply IHtyped; auto]; auto. iApply wp_wand_l. iSplitL; [|iApply IHtyped; auto]; auto.
- (* Alloc *) - (* Alloc *)
smart_wp_bind AllocCtx v "#Hv" IHtyped; cbn. iClear "HΓ". smart_wp_bind AllocCtx v "#Hv" IHtyped; cbn. iClear "HΓ".
iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|].
iPvsIntro.
iApply wp_alloc; auto 1 using to_of_val. iApply wp_alloc; auto 1 using to_of_val.
iFrame "Hheap". iNext. iIntros "{$Hheap} >"; iIntros {l} "Hl".
iIntros {l} "Hl". iPvsIntro.
iPvs (inv_alloc _ with "[Hl]") as "HN"; iPvs (inv_alloc _ with "[Hl]") as "HN";
[| | iPvsIntro; iExists _; iSplit; trivial]; eauto. [| | iPvsIntro; iExists _; iSplit; trivial]; eauto.
- (* Load *) - (* Load *)
smart_wp_bind LoadCtx v "#Hv" IHtyped; cbn. iClear "HΓ". smart_wp_bind LoadCtx v "#Hv" IHtyped; cbn. iClear "HΓ".
iDestruct "Hv" as {l} "[% #Hv]"; subst. iDestruct "Hv" as {l} "[% #Hv]"; subst; simpl.
iApply wp_atomic; cbn; eauto using to_of_val.
iPvsIntro.
iInv (logN .@ l) as {w} "[Hw1 #Hw2]". iInv (logN .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj. iApply (wp_load _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj.
iIntros "{$Hw1} > Hw1". iPvsIntro; iSplitL; eauto. iIntros "{$Hw1} > Hw1". iPvsIntro; iSplitL; eauto.
...@@ -126,10 +121,7 @@ Section typed_interp. ...@@ -126,10 +121,7 @@ Section typed_interp.
smart_wp_bind (StoreLCtx _) v "#Hv" IHtyped1; cbn. smart_wp_bind (StoreLCtx _) v "#Hv" IHtyped1; cbn.
smart_wp_bind (StoreRCtx _) w "#Hw" IHtyped2; cbn. iClear "HΓ". smart_wp_bind (StoreRCtx _) w "#Hw" IHtyped2; cbn. iClear "HΓ".
iDestruct "Hv" as {l} "[% #Hv]"; subst. iDestruct "Hv" as {l} "[% #Hv]"; subst.
iApply wp_atomic; cbn; [trivial| rewrite ?to_of_val; auto |]. iInv (logN .@ l) as {z} "[Hz1 #Hz2]"; [cbn; eauto 10 using to_of_val|].
iPvsIntro.
iInv (logN .@ l) as {z} "[Hz1 #Hz2]".
eapply bool_decide_spec; eauto using to_of_val.
iApply wp_store; auto using to_of_val. solve_ndisj. iApply wp_store; auto using to_of_val. solve_ndisj.
iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro. iSplitL; eauto 10. iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro. iSplitL; eauto 10.
- (* CAS *) - (* CAS *)
...@@ -137,14 +129,11 @@ Section typed_interp. ...@@ -137,14 +129,11 @@ Section typed_interp.
smart_wp_bind (CasMCtx _ _) v2 "#Hv2" IHtyped2; cbn. smart_wp_bind (CasMCtx _ _) v2 "#Hv2" IHtyped2; cbn.
smart_wp_bind (CasRCtx _ _) v3 "#Hv3" IHtyped3; cbn. iClear "HΓ". smart_wp_bind (CasRCtx _ _) v3 "#Hv3" IHtyped3; cbn. iClear "HΓ".
iDestruct "Hv1" as {l} "[% Hinv]"; subst. iDestruct "Hv1" as {l} "[% Hinv]"; subst.
iApply wp_atomic; cbn; eauto 10 using to_of_val.
iPvsIntro.
iInv (logN .@ l) as {w} "[Hw1 #Hw2]"; [cbn; eauto 10 using to_of_val|]. iInv (logN .@ l) as {w} "[Hw1 #Hw2]"; [cbn; eauto 10 using to_of_val|].
destruct (decide (v2 = w)) as [|Hneq]; subst. destruct (decide (v2 = w)) as [|Hneq]; subst.
+ iApply wp_cas_suc; eauto using to_of_val. solve_ndisj. + iApply wp_cas_suc; eauto using to_of_val. solve_ndisj.
iIntros "{$Hheap $Hw1} > Hw1"; iPvsIntro. iIntros "{$Hheap $Hw1} > Hw1"; iPvsIntro; iSplitL; eauto.
iSplitL; [|iPvsIntro]; eauto.
+ iApply wp_cas_fail; eauto using to_of_val. solve_ndisj. + iApply wp_cas_fail; eauto using to_of_val. solve_ndisj.
iIntros "{$Hheap $Hw1} > Hw1". iPvsIntro. iSplitL; eauto. iIntros "{$Hheap $Hw1} > Hw1"; iPvsIntro; iSplitL; eauto.
Qed. Qed.
End typed_interp. End typed_interp.
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