Skip to content

different approach to monPred framing

Ralf Jung requested to merge ci/ralf/monpred-frame into gen_proofmode

I have verified that GPFSL still compiles unchanged, and iGPS needs a tiny patch. I couldn't test lambda-rust:ci/weak_mem because that doesn't compile against latest Iris currently.

Fixes #197 (closed). Also mostly fixes the FIXME left in the text about backtracking by reducing the overlap between instances. There is still some possible overlap though: When framing e.g. (P * R) i and the goal is (_ * _) j, it'll both try to use frame_monPred_at_here and frame_monPred_at_sep. However, I believe that matches that "normal" framing does?

Merge request reports