This MR ensures that opening an invariant or eliminating a mask-changing update modality around a non-atomic weakest precondition creates an side-condition Atomic ...
. Before, this would fail with the mysterious error "iMod: cannot eliminate modality (|={E1,E2}=> ...) in (WP ...)".
For example:
Lemma wp_iInv_atomic_acc N E P :
↑ N ⊆ E →
inv N P -∗ WP #() #() @ E {{ _, True }}.
Proof.
iIntros (?) "H". iInv "H" as "H".
Abort.
This now creates a side-condition Atomic (stuckness_to_atomicity NotStuck) (#() #())
.
The new behavior is implemented by threading the side-condition Atomic
through the instances for ElimModal
, ElimInv
, and ElimAcc
. This makes sure that the side-condition is not established during TC search, but afterwards. For example:
Global Instance elim_modal_fupd_wp_atomic p s E1 E2 e P Φ :
- Atomic (stuckness_to_atomicity s) e →
- ElimModal True p false (|={E1,E2}=> P) P
- (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I.
+ ElimModal (Atomic (stuckness_to_atomicity s) e) p false
+ (|={E1,E2}=> P) P
+ (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
A parameter for such a side-condition was already present in the ElimModal
and ElimInv
classes, but this MR also adds it to the ElimAcc
class.