Commit ee38171a authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

used bool_decide where possible

parent dc62b1b1
Pipeline #17625 failed with stage
......@@ -235,7 +235,7 @@ Section rdcss_minor.
Definition pau P Q γs m1 n1 n2 :=
( P - AU << (m n : Z), rdcss_content γs m n >> @ ∖↑N,
<< rdcss_content γs m (if (decide ((m = m1) (n = n1))) then n2 else n),
COMM Q (if decide (n = n1) then #true else #false) >>)%I.
COMM Q #(bool_decide (n = n1)) >>)%I.
Definition rdcss_inv γ_m γ_n lm lln :=
( (m : Z) (ln : loc) (q : Qp) (s : abstract_state),
......@@ -443,7 +443,7 @@ Section rdcss_minor.
iModIntro. iSplitL "Q Hl_ghost' Hp Hvs Hs Hlln'".
{ iNext. iExists _. iFrame "Hp". iLeft. iFrame.
iRight. iSplitL "Hl_ghost'"; first by iExists _.
destruct (decide _); last done;
case_bool_decide; last done;
destruct (val_to_some_loc vs) eqn:Hvts; iFrame. }
(* close outer inv *)
iModIntro. iSplitR "Hl_ghost'2 HQ Hn●".
......@@ -481,7 +481,7 @@ Section rdcss_minor.
is_rdcss γs v -
<<< (m n: Z), rdcss_content γs m n >>>
rdcss_minor v #m1 #n1 #n2 @∖↑N
<<< rdcss_content γs m (if decide (m = m1 n = n1) then n2 else n), RET if decide (n = n1) then #true else #false >>>.
<<< rdcss_content γs m (if decide (m = m1 n = n1) then n2 else n), RET #(bool_decide (n = n1)) >>>.
Proof.
iIntros "#InvC". iDestruct "InvC" as (γ_m γ_n lm lln) "[Heq InvC]".
iDestruct "Heq" as %[-> ->]. iIntros (Φ) "AU". iLöb as "IH".
......@@ -536,8 +536,9 @@ Section rdcss_minor.
iModIntro. iSplitR "Hln' HΦ".
{ iModIntro. iExists _, _, (q/2)%Qp, (Quiescent n''). iFrame. }
wp_let. wp_load. wp_match.
wp_op. case_bool_decide; simplify_eq; wp_if.
destruct (decide _); done.
case_bool_decide; simplify_eq.
wp_op.
case_bool_decide; simplify_eq. wp_if. iFrame.
- (* l' ↦ injR *)
iModIntro.
(* extract state invariant *)
......
......@@ -31,7 +31,7 @@ Record atomic_rdcss_minor {Σ} `{!heapG Σ} := AtomicRdcss {
is_rdcss N γs v -
<<< (m n: Z), rdcss_content γs m n >>>
rdcss_minor v #m1 #n1 #n2 @∖↑N
<<< rdcss_content γs m (if decide (m = m1 n = n1) then n2 else n), RET if decide (n = n1) then #true else #false >>>;
<<< rdcss_content γs m (if decide (m = m1 n = n1) then n2 else n), RET #(bool_decide (n = n1)) >>>;
set_value_spec N γs v (new_m: Z) :
is_rdcss N γs v -
<<< (m n : Z), rdcss_content γs m n >>>
......
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