-
Notifications
You must be signed in to change notification settings - Fork 105
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Have wp warn when resulting in a goal with a schematic assumption. #729
Comments
In some sense there's two issues here, there's the new free variables that the schematic precondition doesn't depend on, and there's the fact that I think the first is going to be hard to deal with. It's outside of the scope of The second issue is a bit more concerning, our standard Removing that line will hopefully avoid this issue in this specific case, but who knows what other proofs have accidentally depended on it over the years. Even if we do remove it, adding a warning when |
Thanks for tracking down the Yeah, for the former there's no good solution. One can block the |
We should really track down the pairs when we have some time. |
I've started having a look at this and while removing it doesn't affect too many lemmas, it does break more than I expected. So far it's only lemmas that do Possible easier workarounds that I can think of are:
Currently, out of those three options my preference would be the third one. The second would be the least work and keep things the closest to the current behaviour, but the third shouldn't take too much more effort and would result in what I think would be the most sane state, with the least amount of unexpected side-effects from including bundles. |
I agree, the third option would also be my favourite. I think the The line you linked to (https://github.com/seL4/l4v/blob/master/proof/invariant-abstract/Syscall_AI.thy#L1149) also declares |
That strange |
I did try removing that one as well but it broke a proof in a way that was going to require some thought, so I decided to remove |
Another issue that I've just discovered is that So far I've been able to remove the |
Could we make Then the "once" semantics would be preserved and we still get the |
The I also agree with |
I like the idea of In more detail, The optimal result of any changes would be if we could make it so that |
It's a technicality and doesn't really matter, but this would actually need to be |
So |
Hang on, wouldn't that make the new This conversation is getting me a bit worried about |
I was more thinking to make |
In a ccorres or wp proof with a
∃val. x = Some val
or anything like that, an accidental clarsimp will introduce new free variable, and if the schematic only depends onx
, but now the postcondition relies onval
, applyingwp
will result in a schematic assumption in the goal. The very next simp (because we're trying to avoid clarsimp, right? hence also no wpsimp) will the instantiate that schematic toFalse
and we're in trouble.In order to at least get a heads-up about this,
wp
should warn when this happens.wpfix
does not handle these cases,datatype_schem
doesn't help eitherDiscussed a bit with @corlewis so far
The text was updated successfully, but these errors were encountered: