Adding satisfiable to Iris
Several Iris projects have structured their adequacy proofs using the notion of a "satisfiable
-proposition" (instead of following the current adequacy setup of the weakest precondition). It could be interesting to see whether the notion of satisfiable
can be added to Iris in a meaningful way and whether it can enable more modular adequacy proofs in the future.