More monad improvements #765
Conversation
corlewis
added
cleanup
proof engineering
corlewis
force-pushed
the
monad_improvements2
branch
from
b68c9eb
to
ac32aed
Compare
|
There are two new commits in this PR, which removes one lemma from Nondet_VCG, along with removing some FIXMEs that I had recently added and which I no longer think are worth doing. I do still think that the lemmas the FIXMEs refer to are a bit unnecessary, but they're already used in enough proofs that they might as well be left in, and probably should even have their equivalents added to I removed |
| | simp add: projectKO_opt_tcb projectKO_opt_cte | ||
| makeObject_cte makeObject_tcb archObjSize_def | ||
| tcb_cte_cases_def objBitsKO_def APIType_capBits_def | ||
| objBits_def createObjects_def bit_simps | ||
| | intro conjI impI | ||
| | fastforce simp: curDomain_def)+ | ||
| | clarsimp simp: curDomain_def)+ |
There was a problem hiding this comment.
Is this a consequence of removing hoare_gets, or was fastforce more powerful than was needed in general? I've noticed a few instances of that in this commit.
There was a problem hiding this comment.
It's a consequence of removing hoare_gets. Roughly, this proof previously used wp until it hit curDomain, which the fastforce would unfold and then solve using hoare_gets as an intro rule. Now, the clarsimp is just being used to do the unfold and then it goes back to wp to solve the goal. I don't remember exactly why, but for some reason I thought that the unfold couldn't happen ahead of time.
There was a problem hiding this comment.
Looking at it again here, the clarsimp and simp could probably be combined though.
| apply (clarsimp simp: validE_E_def) | ||
| by (wp | assumption)+ | ||
|
|
||
| lemmas bind_wp_fwd = bind_wp[rotated] | ||
| lemmas bindE_wp_fwd = bindE_wp[rotated] | ||
|
|
||
| lemma bind_wpE_R: | ||
| "\<lbrakk>\<And>x. \<lbrace>Q' x\<rbrace> g x \<lbrace>Q\<rbrace>,-; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>,-" | ||
| "\<lbrakk>\<And>rv. \<lbrace>Q' rv\<rbrace> g rv \<lbrace>Q\<rbrace>,-; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= (\<lambda>rv. g rv) \<lbrace>Q\<rbrace>,-" |
There was a problem hiding this comment.
good, I'm glad you remember the significance of the etas
| done | ||
| "\<lbrakk> P \<or> P'; P \<Longrightarrow> \<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>; P' \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> | ||
| \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> S s) \<and> (P' \<longrightarrow> T s)\<rbrace> f \<lbrace>Q\<rbrace>" | ||
| by (fastforce intro: hoare_weaken_pre) |
There was a problem hiding this comment.
I want to say a huge thanks for your recent crusade to reduce the jankiness of our proofs.
Feedback:
commits:
- is it worth having three commits for updating the proofs after the monad consistency commit? I'd squash at least the automated ones together, and maybe even the manual one.
- keeping the remove FIXMES ones separate is a good idea
commit messages:
- apart from hoare_gets -> apart from removing hoare_gets
questions:
- what the
-0777argument toperldo?
I'm happy to squash the automated ones together, I think I mostly did it this way due to starting off with the easy lemma renames and then gradually working out what was needed to change the variables. I wouldn't mind keeping the manual one separate though, I expect it to help when merging into
Agreed, the only one I'm not sure about is the FIXME that was added in the first commit of this PR.
👍
I have to admit that this is a command I dug up from the last time I used |
Agreed, let's squash the automated ones and keep the manual fix-up so we can transfer it. The gitlint check fails because the regular expressions in the commit message are too long. I think I'd be fine overriding the check for this instance. @Xaphiosis do you agree? |
|
Thanks, one more step towards sanity! :-) |
corlewis
force-pushed
the
monad_improvements2
branch
2 times, most recently
from
ce27e67
to
fe38d0f
Compare
This makes the lemma names in the monad rule sets even more consistent, and changes the variables used in the lemmas to avoid R and G being used in pre or post-conditions. These variable names are instead reserved for the rely and guarantee conditions in the trace monads RG rule set. Signed-off-by: Corey Lewis <[email protected]>
The following commands are updates for changed lemma names: sed -i 's/hoare_valid_validE/valid_validE/g' **/*.thy sed -i 's/hoare_vcg_E_conj/hoare_vcg_conj_liftE_E/g' **/*.thy sed -i "s/hoare_vcg_conj_liftE_R/hoare_vcg_conj_liftE_R'/g" **/*.thy sed -i 's/hoare_vcg_R_conj/hoare_vcg_conj_liftE_R/g' **/*.thy sed -i 's/hoare_vcg_E_elim/hoare_vcg_conj_elimE/g' **/*.thy sed -i 's/hoare_vcg_const_imp_lift_R/hoare_vcg_const_imp_liftE_R/g' **/*.thy sed -i 's/hoare_vcg_const_Ball_lift_R/hoare_vcg_const_Ball_liftE_R/g' **/*.thy sed -i 's/hoare_vcg_conj_lift_R/hoare_vcg_conj_liftE_R/g' **/*.thy sed -i 's/hoare_vcg_const_imp_lift_E/hoare_vcg_const_imp_liftE_E/g' **/*.thy sed -i 's/hoare_weak_lift_imp_R/hoare_weak_lift_impE_R/g' **/*.thy sed -i 's/hoare_post_imp_dc2_actual/hoare_post_impE_R_dc_actual/g' **/*.thy sed -i 's/hoare_post_imp_dc2E_actual/hoare_post_impE_E_dc_actual/g' **/*.thy sed -i 's/hoare_post_imp_dc2E/hoare_post_impE_E_dc/g' **/*.thy perl -0777 -pi -e 's/hoare_pre\(1\)/hoare_weaken_pre/g' **/*.thy perl -0777 -pi -e 's/hoare_drop_imps\(2\)/hoare_drop_impE_R/g' **/*.thy sed -i 's/hoare_vcg_imp_lift_R/hoare_vcg_imp_liftE_R/g' **/*.thy The following commmands update changed variable names: perl -0777 -pi -e "s/hoare_post_imp\h*(\s*)\[(\s*)where\h*Q\h*=\h*/hoare_post_imp\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_post_imp/rule_tac Q'=\"\1\"\2in hoare_post_imp/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_strengthen_post/rule_tac Q'=\"\1\"\2in hoare_strengthen_post/g" **/*.thy perl -0777 -pi -e "s/hoare_strengthen_post\h*(\s*)\[(\s*)where\h*Q\h*=\h*/hoare_strengthen_post\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/hoare_strengthen_post\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_strengthen_post\1\[\2where Q=/g" **/*.thy perl -0777 -pi -e "s/hoare_drop_impE_R\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_drop_impE_R\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/hoare_drop_imp\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_drop_imp\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/hoare_drop_imps\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_drop_imps\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*G\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_grab_asm/rule_tac P'=\"\1\"\2in hoare_grab_asm/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*R\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_vcg_if_split/rule_tac P''=\"\1\"\2in hoare_vcg_if_split/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*R\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_post_add/rule_tac Q'=\"\1\"\2in hoare_post_add/g" **/*.thy perl -0777 -pi -e "s/hoare_strengthen_postE\h*(\s*)\[where\h*E\h*=\h*/hoare_strengthen_postE\1\[\2where E'=/g" **/*.thy perl -0777 -pi -e "s/hoare_disjI2\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_disjI2\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_weaken_pre/rule_tac P'=\"\1\"\2in hoare_weaken_pre/g" **/*.thy perl -0777 -pi -e "s/hoare_weaken_pre\h*(\s*)\[(\s*)where\h*Q\h*=\h*/hoare_weaken_pre\1\[\2where P'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_pre_imp/rule_tac P'=\"\1\"\2in hoare_pre_imp/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)and(\s*)E\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_strengthen_postE/rule_tac Q'=\"\1\"\2and\3E'=\"\4\"\5in hoare_strengthen_postE/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*E\h*=\h*\"([^\"]+)\"(\s*)and(\s*)Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_strengthen_postE/rule_tac E'=\"\1\"\2and\3Q'=\"\4\"\5in hoare_strengthen_postE/g" **/*.thy perl -0777 -pi -e "s/hoare_vcg_conj_liftE_R\h*(\s*)\[(\s*)where\h*S\h*=\h*/hoare_vcg_conj_liftE_R\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/hoare_post_add\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_post_add\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)for(.*)(\s*)in\h*hoare_strengthen_post/rule_tac Q'=\"\1\"\2for\3\4in hoare_strengthen_post/g" **/*.thy perl -0777 -pi -e "s/unless_wp\h*(\s*)\[(\s*)where\h*Q\h*=\h*/unless_wp\1\[\2where P'=/g" **/*.thy perl -0777 -pi -e "s/hoare_chain\h*(\s*)\[(\s*)where\h*P\h*=\h*/hoare_chain\1\[\2where P'=/g" **/*.thy Signed-off-by: Corey Lewis <[email protected]>
This fixes the proofs not handled by the automated changes in the previous commits. Signed-off-by: Corey Lewis <[email protected]>
These FIXMEs were recently added and apart from removing hoare_gets I no longer think that they are worth doing, as the lemmas they refer to are used in more proofs than I first thought. Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
corlewis
force-pushed
the
monad_improvements2
branch
from
fe38d0f
to
f69d902
Compare
This makes further improvements to the consistency of the monad rule sets, following on from #759. In particular, it includes additional lemma renamings missed in that PR, and changes the variables used in the lemmas to avoid
RandGbeing used in pre or post-conditions. These variable names are instead reserved for the rely and guarantee conditions in the trace monad's RG rule set.