Commit 15005661 authored by Amin Timany's avatar Amin Timany

Fix the problem with solve_ndisj not working

parent 72eef741
......@@ -96,14 +96,15 @@ Section fundamental.
smart_wp_bind LoadCtx v "#Hv" IHtyped; cbn. iClear "HΓ".
iDestruct "Hv" as {l} "[% #Hv]"; subst.
iInv (logN .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj.
iApply (wp_load _ _ 1); [|iFrame "Hheap"]; trivial.
unfold logN, heapN; solve_ndisj.
iIntros "{$Hw1} > Hw1". iPvsIntro. iSplitL; eauto.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHtyped1; cbn.
smart_wp_bind (StoreRCtx _) w "#Hw" IHtyped2; cbn. iClear "HΓ".
iDestruct "Hv" as {l} "[% #Hv]"; subst.
iInv (logN .@ l) as {z} "[Hz1 #Hz2]"; [cbn; eauto 10 using to_of_val|].
iApply wp_store; auto using to_of_val. solve_ndisj.
iApply wp_store; auto using to_of_val. unfold logN, heapN; solve_ndisj.
iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro; iSplitL; eauto 10.
Qed.
End fundamental.
......@@ -306,7 +306,7 @@ Section CG_Counter.
iApply (@wp_bind _ _ _ [AppRCtx (RecV _)]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iInv> counterN as {n} "[Hl [Hcnt Hcnt']]".
iApply wp_load; [|iFrame "Hheap"]. solve_ndisj.
iApply wp_load; [|iFrame "Hheap"]. unfold heapN, counterN; solve_ndisj.
iIntros "> {$Hcnt} Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iApply wp_rec; trivial. asimpl. iNext.
......@@ -325,7 +325,8 @@ Section CG_Counter.
iPvs (steps_CG_locked_increment
_ _ _ _ _ _ _ _ with "[Hj Hl Hcnt']") as "[Hj [Hcnt' Hl]]".
{ iFrame "Hspec Hcnt' Hl Hj"; trivial. }
iApply wp_cas_suc; simpl; trivial; [|iFrame "Hheap"]. solve_ndisj.
iApply wp_cas_suc; simpl; trivial; [|iFrame "Hheap"].
unfold heapN, counterN; solve_ndisj.
iIntros "{$Hcnt} > Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iApply wp_if_true. iNext. iApply wp_value; trivial.
......@@ -333,7 +334,8 @@ Section CG_Counter.
+ (* CAS fails *)
(* In this case, we perform a recursive call *)
iApply (wp_cas_fail _ _ _ (v n')); simpl; trivial;
[inversion 1; subst; auto | | iFrame "Hheap"]. solve_ndisj.
[inversion 1; subst; auto | | iFrame "Hheap"].
unfold heapN, counterN; solve_ndisj.
iIntros "{$Hcnt} > Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iApply wp_if_false. iNext. by iApply "Hlat".
......@@ -346,13 +348,13 @@ Section CG_Counter.
iApply wp_rec; trivial. simpl.
iNext. iInv> counterN as {n} "[Hl [Hcnt Hcnt']]".
iPvs (steps_counter_read with "[Hj Hcnt']") as "[Hj Hcnt']".
{ solve_ndisj. }
{ unfold specN, counterN; solve_ndisj. }
{ by iFrame "Hspec Hcnt' Hj". }
iApply wp_load; [|iFrame "Hheap"]. solve_ndisj.
iApply wp_load; [|iFrame "Hheap"]. unfold heapN, counterN; solve_ndisj.
iIntros "{$Hcnt} > Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iExists (v _); eauto.
Unshelve. solve_ndisj.
Unshelve. unfold specN, counterN; solve_ndisj.
Qed.
End CG_Counter.
......
......@@ -364,7 +364,7 @@ Section Stack_refinement.
end.
all: trivial.
all: try match goal with |- _ _ => congruence end.
all: solve_ndisj.
all: unfold heapN, specN, stackN, specN; solve_ndisj.
Qed.
End Stack_refinement.
......
......@@ -319,8 +319,9 @@ Section fundamental.
iInv (logN .@ (l,l')) as { [w w'] } "[Hw1 [Hw2 #Hw]]"; simpl.
iTimeless "Hw2".
iPvs (step_load _ _ j K l' 1 w' with "[Hv Hw2]") as "[Hv Hw2]";
[solve_ndisj|by iFrame|].
iApply (wp_load _ _ 1); [|iFrame "Hh"]; trivial; try solve_ndisj.
[unfold logN, specN; solve_ndisj|by iFrame|].
iApply (wp_load _ _ 1); [|iFrame "Hh"]; trivial;
try unfold logN, heapN; solve_ndisj.
iIntros "{$Hw1} > Hw1". iPvsIntro. iSplitL "Hw1 Hw2".
- iNext; iExists (w,w'); by iFrame.
- iExists w'; by iFrame.
......@@ -341,8 +342,8 @@ Section fundamental.
{ eapply bool_decide_spec; eauto using to_of_val. }
iTimeless "Hv2".
iPvs (step_store _ _ j K l' v' (# w') w' with "[Hw Hv2]")
as "[Hw Hv2]"; [eauto|solve_ndisj|by iFrame|].
iApply wp_store; auto using to_of_val. solve_ndisj.
as "[Hw Hv2]"; [eauto|unfold logN, specN; solve_ndisj|by iFrame|].
iApply wp_store; auto using to_of_val. unfold logN, heapN; solve_ndisj.
iIntros "{$Hh $Hv1} > Hv1". iPvsIntro. iSplitL "Hv1 Hv2".
- iNext; iExists (w, w'); by iFrame.
- iExists UnitV; iFrame; auto.
......@@ -368,18 +369,22 @@ Section fundamental.
iTimeless "Hv2".
destruct (decide (v = w)) as [|Hneq]; subst.
- iPvs (step_cas_suc _ _ j K l' (# w') w' v' (# u') u'
with "[Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
with "[Hu Hv2]") as "[Hw Hv2]"; simpl; eauto;
first unfold logN, specN; solve_ndisj.
{ iIntros "{$Hs $Hu $Hv2} >".
rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. }
iApply wp_cas_suc; eauto using to_of_val; first solve_ndisj.
iApply wp_cas_suc; eauto using to_of_val;
first unfold logN, heapN; solve_ndisj.
iIntros "{$Hh $Hv1} > Hv1". iPvsIntro. iSplitL "Hv1 Hv2".
+ iNext; iExists (_, _); by iFrame.
+ iExists (v true); iFrame; eauto.
- iPvs (step_cas_fail _ _ j K l' 1 v' (# w') w' (# u') u'
with "[Hu Hv2]") as "[Hw Hv2]"; simpl; eauto; first solve_ndisj.
with "[Hu Hv2]") as "[Hw Hv2]"; simpl; eauto;
first unfold logN, specN; solve_ndisj.
{ iIntros "{$Hs $Hu $Hv2} >".
rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. }
iApply wp_cas_fail; eauto using to_of_val; first solve_ndisj.
iApply wp_cas_fail; eauto using to_of_val;
first unfold logN, heapN; solve_ndisj.
iIntros "{$Hh $Hv1} > Hv1". iPvsIntro. iSplitL "Hv1 Hv2".
+ iNext; iExists (_, _); by iFrame.
+ iExists (v false); eauto.
......
......@@ -115,14 +115,16 @@ Section typed_interp.
smart_wp_bind LoadCtx v "#Hv" IHtyped; cbn. iClear "HΓ".
iDestruct "Hv" as {l} "[% #Hv]"; subst; simpl.
iInv (logN .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj.
iApply (wp_load _ _ 1); [|iFrame "Hheap"]; trivial.
unfold logN, heapN; solve_ndisj.
iIntros "{$Hw1} > Hw1". iPvsIntro; iSplitL; eauto.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHtyped1; cbn.
smart_wp_bind (StoreRCtx _) w "#Hw" IHtyped2; cbn. iClear "HΓ".
iDestruct "Hv" as {l} "[% #Hv]"; subst.
iInv (logN .@ l) as {z} "[Hz1 #Hz2]"; [cbn; eauto 10 using to_of_val|].
iApply wp_store; auto using to_of_val. solve_ndisj.
iApply wp_store; auto using to_of_val.
unfold logN, heapN; solve_ndisj.
iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro. iSplitL; eauto 10.
- (* CAS *)
smart_wp_bind (CasLCtx _ _) v1 "#Hv1" IHtyped1; cbn.
......@@ -131,9 +133,11 @@ Section typed_interp.
iDestruct "Hv1" as {l} "[% Hinv]"; subst.
iInv (logN .@ l) as {w} "[Hw1 #Hw2]"; [cbn; eauto 10 using to_of_val|].
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.
unfold logN, heapN; solve_ndisj.
iIntros "{$Hheap $Hw1} > Hw1"; iPvsIntro; iSplitL; eauto.
+ iApply wp_cas_fail; eauto using to_of_val. solve_ndisj.
+ iApply wp_cas_fail; eauto using to_of_val.
unfold logN, heapN; solve_ndisj.
iIntros "{$Hheap $Hw1} > Hw1"; iPvsIntro; iSplitL; eauto.
Qed.
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