Remove hoare_vcg_precond_imp from wp_comb #747
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
corlewis
added
cleanup
proof engineering
corlewis
force-pushed
the
hoare_vcg_precond_imp_comb
branch
from
134829f to
82b291c
Compare
corlewis
commented
Apr 9, 2024
lsf37
reviewed
Apr 9, 2024
lsf37
reviewed
Apr 9, 2024
lsf37
reviewed
Apr 9, 2024
lsf37
reviewed
Apr 9, 2024
lsf37
approved these changes
Apr 9, 2024
There's actually even more uses of |
Xaphiosis
reviewed
Apr 9, 2024
| lemma switch_to_thread_ct_not_queued[wp]: | ||
| "\<lbrace>valid_queues\<rbrace> switch_to_thread t \<lbrace>\<lambda>rv s. not_queued (cur_thread s) s\<rbrace>" | ||
| unfolding switch_to_thread_def | ||
| by wpsimp |
There was a problem hiding this comment.
Yeah, this was one of the early cases before I found classic_wp_pre and when I was trying to properly fix broken proofs. The previous proof did a lot of very convoluted work to get to the tcb_sched_action tcb_sched_dequeue step with the appropriate precondition in place. Pulling it out to a separate lemma made things a lot simpler.
This being a `wp_comb` rule is a leftover from before `wp_pre` was implemented and it is being removed because in some cases it can cause unintended schematics to appear in the assumptions. This commit also updates all of the proofs that accidentally depended on it being a `wp_comb` rule. In many cases this involved `including classic_wp_pre`, which locally returns the wp attributes to a state similar to what it was when the proofs were first written. Other cases required small rewrites, often involving using `wpsimp` instead of `wp`, and removing some uses of `wp (once)`. Signed-off-by: Corey Lewis <[email protected]>
corlewis
force-pushed
the
hoare_vcg_precond_imp_comb
branch
from
5dbb844 to
23e7d7f
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This being a
wp_combrule is a leftover from beforewp_prewas implemented and it is being removed because in some cases it can cause unintended schematics to appear in the assumptions. See #729 for more discussion of this being a problem.This commit also updates all of the proofs that accidentally depended on it being a wp_comb rule. In many cases this involved
including classic_wp_pre, which locally returns the wp attributes to a state similar to what it was when the proofs were first written. Other cases required small rewrites, often involving usingwpsimpinstead ofwp, and removing some uses ofwp (once).