GitLab

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.