Better support for using logically atomic triple
Currently, we have to manually wire together all the pieces, which is daunting ... example from atomic_incr.v
(* open the invariant *)
iInv N as (x') ">Hl'" "Hclose".
(* mask magic *)
iVs (pvs_intro_mask' (⊤ ∖ nclose N) heapN) as "Hvs"; first set_solver.
iVsIntro. iExists x'. iFrame "Hl'". iSplit.
+ (* provide a way to rollback *)
iIntros "Hl'".
iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.
+ (* provide a way to commit *)
iIntros (v) "[Heq Hl']".
iVs "Hvs". iVs ("Hclose" with "[Hl']"); eauto.