iMod doesn't handle mismatched mask
Like in
Lemma vs_demo (l: loc) (E1 E2: coPset):
((|={E1, E2}=> True) ★ l ↦ #1)%I
⊢ WP !#l @ ⊤ {{ _, True }}.
Proof.
iIntros "(HPQ & Hl)".
iVs "HPQ". (* error: not a view shift *)
Ideally, since load is atomic, using iVs
here should generate two goals, the first one as a side condition saying that E1 ⊆ ⊤
, and second one doing the view shift and send us to E2
masked weakest pre.
cc @robbertkrebbers @jung. Hope I clarify the problem :p
Edited by Ralf Jung