Some rules for Lib and CLib
#785
Conversation
| @@ -83,6 +83,10 @@ lemma ofail_wp[wp]: | |||
| "ovalid (\<lambda>_. True) ofail Q" | |||
| by (simp add: ovalid_def ofail_def) | |||
|
|
|||
| lemma ask_wp: | |||
There was a problem hiding this comment.
I'm never the best judge on whether a lemma should be in one of these named theorem sets like [wp], especially in Lib rules, where they're sometimes added in particular spots. But I can certainly make this one [wp] if that's best
There was a problem hiding this comment.
This one would is basic enough to make sense as [wp], yes. @corlewis any concerns there?
lib/clib/CCorresLemmas.thy
Outdated
| @@ -586,6 +586,13 @@ lemma ccorres_assert2: | |||
| (\<lambda>s. P \<longrightarrow> G s) {s. P \<longrightarrow> s \<in> G'} hs (assert P >>= f) c" | |||
| by (cases P, simp_all add: ccorres_fail') | |||
|
|
|||
| (* A weaker version of ccorres_assert2 that may be easier to match with schematics, since | |||
| the concrete guard does not mention the asserted property *) | |||
| lemma ccorres_assert2': | |||
There was a problem hiding this comment.
Maybe this could have a more informative name. I could rename regular ccorres_assert to ccorres_assert_drop_property or something like that, ccorres_assert2 to ccorres_assert_add_property or something, and then this new rule could maybe be ccorres_assert_add_abstract_property. I'm not married to these names, these are just suggestions to indicate what's happening
There was a problem hiding this comment.
Hm, this is a bit subtle. The default corres_assert doesn't actually drop the property, it does provide it in the subgoal, and it is a bit strange that we do sometimes seem to need it in the generated precondition -- ideally the sub proof should not produce anything that needs P any more, because P was available already and should have been eliminated.
That said, the way the schematics are instantiated, we often do not want to simp or similar in the sub proof, so I agree that we do want these variants. The problem (as you seem to have discovered if you have an abstract-only variant) is that adding implications to the preconditions can make subsequent proofs harder even though they are logically weaker/easier.
Of course the current variant names are terrible. I would propose the following scheme: ccorres_assert should stay the default name, and we add ccorres_assert_both + ccorres_assert_abs. If we ever need it, we could add ccorres_assert_C (or _concrete or similar).
There was a problem hiding this comment.
This is a bit tricky to figure out. After I wrote the original comment about add and dropping properties I wasn't so sure why it is that it seems like the property that's asserted disappears sometimes. Are you thinking that it's because it's simped away? And that having it in the guard explicitly preserves it until the final goal where the guard implications are resolved?
The reason I wanted this variant was that ccorres_symb_exec_l' won't change the schematic, and so if we use ccorres_symb_exec_l' and then want to use an assert rule about the value that we get, then we can't unify with ccorres_assert2.
There was a problem hiding this comment.
This is indeed strange, I feel like we shouldn't need this rule. We generally rewrite stuff on the C side into Haskell side as we symbolically execute forward, meaning that an assertion on the Haskell side might later provide information to clean up the final C part of the proof, so it should be available to both sides, and if it isn't relevant, it shouldn't get in the way.
It's also possible that the ccorres_symb_exec_l' isn't in the right form. I'm guessing none of the other symb_exec_l rules worked for you?
The property "disappearing" sounds like it's getting simped away, but it persists in the guards.
If you want to keep this rule, I'd suggest changing the name to ccorres_assert2_abs and changing the comment to something like (* This variant only propagates the assertion into the abstract side, to aid with schematic matching on the concrete side. *)
There was a problem hiding this comment.
The reason I wanted this variant was that ccorres_symb_exec_l' won't change the schematic, and so if we use ccorres_symb_exec_l' and then want to use an assert rule about the value that we get, then we can't unify with ccorres_assert2.
Right, that makes sense to me. Together with Raf's proposed comment that should resolve the content at least.
After I wrote the original comment about add and dropping properties I wasn't so sure why it is that it seems like the property that's asserted disappears sometimes. Are you thinking that it's because it's simped away?
It's scope: the default rule makes P available in the assumption of all sub goals that are "inside" the scope of the assert rule applications (all new subgoals). The assert2 rule exports P additionally to the C vcg goal that is on the same level as the assert2 rule application -- the vcg goal already exists when the rule is being applied and the goal is being modified by partially instantiating the schematic. This in turn usually make P available in in the big final goal.
Usually that second part shouldn't be necessary, because you should need the P only for code that comes after the assert, which means in the subgoals of the assert rule. But sometimes that fails, because we do export P-dependent conditions in those vcg goals and sometimes also abstract goals.
| while loop, where in particular, the C while loop is parsed into a Simpl While loop that | ||
| updates the cstate as part of the loop condition. In such a case, the CParser will produce a Simpl | ||
| program in the form that is seen in the conclusion of this rule.\<close> | ||
| This rule is intended to be used to show correspondence between a @{term whileLoop} and a Simpl |
There was a problem hiding this comment.
I could add in another bullet point here talking about the requirement that the whileLoop condition be in the the blah form and that this cannot fail, and therefore, we must have the no_ofail assumption.
I think @lsf37 and I discussed briefly the idea that we might want an alternate whileLoop where the condition is always a reader monad function, and where the new whileLoop fails if the reader monad function fails. But that would be a lot of mucking around, especially given all the rules we already have about whileLoop
There was a problem hiding this comment.
Yes, adding that bullet point would make sense, with a remark that eliminating the no_ofail would require a slightly different form of whileLoop that can deal with failure in the condition.
lib/HaskellLib_H.thy
Outdated
| definition ostate_assert :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, unit) lookup" where | ||
| "ostate_assert P \<equiv> do { s \<leftarrow> ask; oassert (P s)}" |
There was a problem hiding this comment.
This definition should be in the monad library, only ohaskell_state_assert should live on HaskellLib_H
| while loop, where in particular, the C while loop is parsed into a Simpl While loop that | ||
| updates the cstate as part of the loop condition. In such a case, the CParser will produce a Simpl | ||
| program in the form that is seen in the conclusion of this rule.\<close> | ||
| This rule is intended to be used to show correspondence between a @{term whileLoop} and a Simpl |
There was a problem hiding this comment.
Yes, adding that bullet point would make sense, with a remark that eliminating the no_ofail would require a slightly different form of whileLoop that can deal with failure in the condition.
| @@ -132,11 +132,6 @@ local_setup \<open>AutoCorresModifiesProofs.new_modifies_rules "../c/build/$L4V_ | |||
|
|
|||
| text \<open>Extra corres_underlying rules.\<close> | |||
|
|
|||
| lemma corres_add_noop_rhs2: | |||
There was a problem hiding this comment.
you're modifying crefine but I didn't see any crefine tag for any of the commits
There was a problem hiding this comment.
I can make the tag for this commit lib+drefine+crefine:. I did have a look through the commit message guide again, and these points weren't explicitly mentioned, but my thinking here was that it's just moved up to lib, and to me, the tag indicates where significant changes are made, and which is the highest session that has been changed, so that we know what would need to be rebuilt.
There was a problem hiding this comment.
See my comment on the other one. it shouldn't be "add" when you're moving. If it's not significant I'd punt it and say lib+proof: move ... to ...
@lsf37 can also weigh in, the moving to lib case is never quite clear.
There was a problem hiding this comment.
I don't have a strong preference either way
| @@ -1082,11 +1082,6 @@ lemma pde_opt_cap_eq: | |||
| apply (clarsimp simp: valid_idle_def st_tcb_at_def obj_at_def pred_tcb_at_def) | |||
| done | |||
|
|
|||
| lemma corres_add_noop_rhs: | |||
There was a problem hiding this comment.
you're modifying drefine but I didn't see any drefine tag for any of the commits
There was a problem hiding this comment.
ah, I think I see, there's a commit that says add ... to ..., which is confusing. It should at minimum say move ... to ..., but I'd prefer adding the tags as well
| @@ -288,6 +301,16 @@ lemma ccorres_from_vcg_nofail: | |||
| apply (rule hoare_complete, simp add: HoarePartialDef.valid_def) | |||
| done | |||
|
|
|||
| lemma ccorres_to_vcg_with_prop': | |||
There was a problem hiding this comment.
I'd put this below the non-prime version. Usually we put the ' one above if it's used to show the non-prime one, and this one seems less intuitive than its no_fail cousin.
There was a problem hiding this comment.
I was actually able to prove the non-prime one from the prime one, so I've done that, and left the prime version where it is. I'm sure I tried this before, so I'm not sure why it didn't work the first time...
| "\<And>s s' xstate. | ||
| \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<Gamma> \<turnstile> \<langle>c, Normal s'\<rangle> \<Rightarrow> xstate; \<not> snd (a s)\<rbrakk> | ||
| \<Longrightarrow> (\<exists>t'. xstate = Normal t' \<and> (\<exists>(r, t) \<in> fst (a s). (t, t') \<in> srel \<and> rrel r (xf t')))" | ||
| shows "ccorresG srel \<Gamma> rrel xf G G' [] a c" |
There was a problem hiding this comment.
This is strange. I think maybe the name should be tweaked to ccorres_empty_handler_stackI so people don't look for a ccorresI like the ccorresG.
The other thing is, do you have a small comment on when one would use this? I'm staring at it and can't figure it out.
There was a problem hiding this comment.
It is a bit confusing having ccorresG as an abbreviation and then having ccorresI and ccorresE (probably as well as others) being intro/elim style rules. I'm happy to change the name, but to me this name makes more sense because it is an intro rule for (ultimately a) ccorres_underlying statement, but with some extra restrictions, namely there being an empty handler stack.
As for when to use it, I'm no expert in C semantics or CRefine, so the handler stack is still a bit mysterious to me. Gerwin mentioned on Mattermost that if we have a schematic handler stack, then to prove ccorres, we would need to make assumptions about what the handler stack does, probably something like it taking any Abrupt state to a Normal state. So if we didn't want to do something like that and we still wanted to prove a ccorres rule, we would need to show that the c function in this rule always returns a Normal state, in which case, the handler stack may as well be empty, since it won't be used. Unfolding ccorres_underlying_def will leave us with terms involving exec_handlers which aren't as nice to deal with as regular hoarep statements, and the exec_handler statement doesn't mean much with an empty handler stack anyway.
So maybe a comment to help explain how it could be used could say "for proving low-level ccorresG statements where the concrete function always returns a Normal state, and therefore, the handler stack will not be used, and can be considered empty". But I'm not sure that's more helpful than what someone might glean from the name of the lemma
There was a problem hiding this comment.
Yes please to this comment. Even if it's a skill issue, I find your explanation and comment helpful.
michaelmcinerney
force-pushed
the
michaelm-Lib_rules_July_2024
branch
from
b5baf6f
to
20e4736
Compare
|
All comments so far have now been addressed. I've forced pushed due to a rebase, and also to redo the commit message for the commit that moved some lemmas to Lib. I'll redo some more commit messages, due to renaming things, when I squash |
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
This helps to reduce dependence between the schematics used in the assumptions, and allows for easier wp reasoning. Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
This adds ostate_assert and ohaskell_state_assert, which are versions of state_assert/stateAssert for the reader monad. Also adds several rules for basic reasoning about these functions. Signed-off-by: Michael McInerney <[email protected]>
Moved from DRefine and CRefine, respectively Signed-off-by: Michael McInerney <[email protected]>
michaelmcinerney
force-pushed
the
michaelm-Lib_rules_July_2024
branch
from
0cbc1f1
to
96799b8
Compare
Please note that all new rules for the reader monad are currently unused in my work in progress; I have added them here just in case we would like them.
I'd be happy to rename any of these, so suggestions are welcome.
And I hope the commit messages are sufficiently informative, and sufficiently specific about where the changes are being made. I'm still not sure what the best approach for just adding lemmas like this is in some cases.