A lot of failures in Starling proofs are due to missing exclusivity constraints. Effectively this corresponds to failing to witness a form of mutual exclusion or sequentialism in the program under proof.
There are multiple ways we could use exclusivity constraints to repair a failing proof:
Detect a state machine in one or more of the proof outlines, and suggest adding pairwise exclusivity constraints for each state. The hard part is figuring out what a 'state machine' looks like: is it just a sequence of single views from entry point to exit point, modulo conditionals, that shares a common parameter?
Suggest adding an exclusivity constraints when e.g. one of the failing proof terms has G included in Q, but not in P. This is usually a good model for a command gaining a resource. There might be a way we can restrict this pattern–I still need to look at common failures.
@septract's idea of saturating the exclusivity space then removing exclusivity constraints. What I'm not sure about ATM is how to do this systematically, and I'm also unsure as to whether we can always use full saturation as a canary to check whether the proof failure is due to exclusivity constraints. My gut feeling is that we can, if there are no instances of {emp} in the proof. Even then we can synthesise a new view that captures sequentialism for those cases.
A lot of failures in Starling proofs are due to missing exclusivity constraints. Effectively this corresponds to failing to witness a form of mutual exclusion or sequentialism in the program under proof.
There are multiple ways we could use exclusivity constraints to repair a failing proof: