Commit 66a75091 authored by Amin Timany's avatar Amin Timany

Revert "Fix for solve_ndisj no longer being able to fail due to Iris 65296d1a."

This reverts commit efe1b574.
parent 928a1c39
......@@ -321,8 +321,8 @@ Section fundamental.
iTimeless "Hw2".
iPvs (step_load _ _ j K l' 1 w' with "[Hv Hw2]") as "[Hv Hw2]";
[unfold logN, specN; solve_ndisj|by iFrame|].
iApply (wp_load _ _ 1); [|iFrame "Hh"]; trivial.
unfold logN, heapN; solve_ndisj.
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.
......@@ -371,21 +371,21 @@ Section fundamental.
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 (unfold logN, specN; solve_ndisj).
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 (unfold logN, heapN; solve_ndisj).
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 (unfold logN, specN; solve_ndisj).
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 (unfold logN, heapN; solve_ndisj).
first unfold logN, heapN; solve_ndisj.
iIntros "{$Hh $Hv1} > Hv1". iPvsIntro. iSplitL "Hv1 Hv2".
+ iNext; iExists (_, _); by iFrame.
+ iExists (v false); eauto.
......
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