Commit 4cd7e0d5 authored by Ike Mulder's avatar Ike Mulder
Browse files

Fixed broken proofs caused by needing less iStepsS.

parent 47fc6fee
Pipeline #62067 passed with stage
in 11 minutes and 28 seconds
......@@ -125,10 +125,6 @@ Section spec.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS. (* need to manually open invs, otherwise the AU will and can no longer be be opened.
I think this could be fixed by instead using |={⊤,E}=> masks instead of |={⊤ ∖ E, ∅}=> masks.. *)
iMod (inv_acc with "H7") as "[HN HNcl]"; first done.
......
......@@ -212,12 +212,9 @@ Module atomic_lock_stateless.
iApply wp_value. by iApply "Hx".
Qed.
Next Obligation.
intros; cbn. do 13 iStepS. iApply (atomic.atomic_update_mono with "H3").
intros; cbn. do 10 iStepS. iApply (atomic.atomic_update_mono with "H3").
iIntros "!> !>"; iSplit; first eauto.
iExists (id).
simpl. iSplit; first eauto.
iIntros "Hx !> _".
iApply wp_value. by iApply "Hx".
iExists (id). iSplit; iStepsS.
Qed.
End atomic_lock_stateless.
......
Supports Markdown
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