refill_budget_check_ccorres
#821
Conversation
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
| @@ -172,6 +172,10 @@ lemma word32_and_max_simp: | |||
| using word_and_full_mask_simp [of x] | |||
| by (simp add: numeral_eq_Suc mask_Suc_exp) | |||
|
|
|||
| lemma max_minus_one_word32: | |||
There was a problem hiding this comment.
We should name both of them just max_minus_one_word, so that we can use the same name in 32 and 64 contexts (maybe with another postfix for indicating that it is for fixed lengths, not sure).
The theory name can be used to specify a specific version if that is needed.
michaelmcinerney
added
the
MCS
| @@ -11810,34 +11800,34 @@ lemma set_refills_bounded_release_time: | |||
| apply (wpsimp wp: valid_sched_wp) | |||
| by (clarsimp simp: vs_all_heap_simps bounded_release_time_def pred_map_simps obj_at_def | |||
| heap_upd_def split: if_split) | |||
|
|
|||
| thm refill_budget_check_def | |||
There was a problem hiding this comment.
Remove this thm
|
|
||
| lemma merge_nonoverlapping_head_refill_no_fail[wp]: | ||
| "no_fail (\<lambda>s. sc_refills_sc_at (\<lambda>refills. 1 < length refills) sc_ptr s) | ||
| (merge_nonoverlapping_head_refill sc_ptr)" |
There was a problem hiding this comment.
indent looks off here, should align with ( on prev line. same for update_refill_hd_no_fail
| (update_refill_hd sc_ptr f)" | ||
| unfolding update_refill_hd_def refill_pop_head_def | ||
| apply wpsimp | ||
| by (clarsimp simp: obj_at_def sc_at_pred_n_def) |
There was a problem hiding this comment.
you can combine two-steps into a single by
| done | ||
|
|
||
| lemmas no_fail_get_refill_tail[wp] = | ||
| no_ofail_gets_the[OF no_ofail_read_refill_tail, simplified get_refill_tail_def[symmetric]] |
There was a problem hiding this comment.
, folded get_refill_tail_def] might work here
| "no_ofail (\<lambda>s. sc_refills_sc_at (\<lambda>refills. refills \<noteq> []) scp s) (read_refill_tail scp)" | ||
| unfolding read_refill_tail_def | ||
| apply wpsimp | ||
| apply (clarsimp simp: sc_at_pred_n_def obj_at_def) |
| by wpsimp | ||
|
|
||
| lemmas get_refill_tail_wp[wp] = | ||
| ovalid_gets_the[OF read_refill_tail_wp, simplified get_refill_tail_def[symmetric]] |
There was a problem hiding this comment.
also a chance folded will work here
| apply simp | ||
| apply simp | ||
| apply wpsimp | ||
| apply wpsimp |
There was a problem hiding this comment.
can shorten this by using simp+ and wpsimp+, or even wpsimp+ to cover all 4 steps
| apply (clarsimp simp: get_refill_tail_def getRefillTail_def read_refill_tail_def | ||
| readRefillTail_def getSchedContext_def[symmetric] | ||
| read_sched_context_get_sched_context | ||
| readSchedContext_def getObject_def[symmetric]) |
There was a problem hiding this comment.
dunno if this is from older proofs, but checking that you know you can do clarsimp simp: ... simp flip: ... to not need the [symmetric]
| apply (rule refill_head_ccorres) | ||
| apply clarsimp | ||
| apply clarsimp | ||
| apply clarsimp |
| apply (rule ccorres_split_nothrow) | ||
| apply (clarsimp simp: setRefillTl_def updateRefillTl_def) | ||
| apply (rule updateSchedContext_ccorres_lemma3 | ||
| [where P="\<lambda>sc. scRefillTail sc < length (scRefills sc)" and P'="?abs"]) |
There was a problem hiding this comment.
[ should be two spaces deeper than u, am seeing one on the github diff (saw this above as well in same file)
There was a problem hiding this comment.
Is there any particular reason that we would want two spaces here, rather than one? I thought that as long as it's strictly to the right of the name of the rule, it would be fine.
There was a problem hiding this comment.
as discussed offline: indent is nearly always by 2 spaces, except for subgoal-indentation where it's two spaces plus number of subgoals - 1
Also, there are other issues (the modification belongs to the lemma not to rule);
it might be better to have ..._lemma3[ to indicate the lemma is being modified, then wrap how it's modified onto the next line, with the where 2 in from updateSched.... Might be a tight fit still
| in rf_sr_refill_update2; fastforce?) | ||
| apply (fastforce simp: sched_context.expand) | ||
| apply (clarsimp simp: typ_heap_simps) | ||
| apply (fastforce simp: typ_heap_simps' sc_ptr_to_crefill_ptr_def crefill_relation_def) |
There was a problem hiding this comment.
unusual having typ_heap_simps in two commands like this; is this proof copied?
There was a problem hiding this comment.
The clarsimp uses typ_heap_simps and then the fastforce uses typ_heap_simps'. I'm quite sure that neither can be removed, and I think I have also tried without success before to condense it into one command. It would be cool to see whether this could be improved, or to properly understand what's going on, but I don't think I could figure it out before
There was a problem hiding this comment.
And yes the proof was copied, and it appears like this in a few places, now
There was a problem hiding this comment.
We can leave it then. If it were new, would be worth more investigation.
| apply (clarsimp simp: typ_heap_simps' sc_ptr_to_crefill_ptr_def | ||
| csched_context_relation_def) | ||
| apply (clarsimp simp: typ_heap_simps csched_context_relation_def) | ||
| apply normalise_obj_at' |
There was a problem hiding this comment.
unexpected to see normalise_obj_at' so distant from the subgoal-solving statement, anything interesting going on herer?
There was a problem hiding this comment.
Maybe some of these normalise_obj_at' can be removed or moved elsewhere. Maybe I don't understand what you mean by it being distant from the subgoal-solving statement. Were you expecting it to be further up or further down?
There was a problem hiding this comment.
Well, normally I see it used, and then the subgoal is discharged immediately, or on the next step. This one goes on for a bit until it's actually discharged, making me wonder if something is going the long way around.
| simp: refill_pop_head_def vs_all_heap_simps obj_at_def refill_single_def refill_size_def | ||
| update_sched_context_set_refills_rewrite update_refill_hd_rewrite | ||
| schedule_used_defs) | ||
| method charge_entire_head_refill_simple |
There was a problem hiding this comment.
are these methods used in multiple places? they seem highly specific, so if they are only used in one place, local_method might be better
There was a problem hiding this comment.
Yes these _simple methods were quite handy, actually. I at first wanted to remove them, but there were quite a few places where they're used. Handy, but annoying, because I did have to go through quite a few iterations before I found something that would work everywhere it was being used. There might be a bit more that I could do to optimise these, but considering how long it takes to process this file, it's very painful to do
There was a problem hiding this comment.
I guess take a quick look, or maybe examine it when you're next there.
Not sure if it's clear what I meant by local method, I specifically meant a tool Ed hacked up, supply_local_method, whose uses you can see in Local_Method_Tests.thy in lib, and proof/crefine/ARM_HYP/Arch_C.thy ... did that one ever make an appearance in MCS?
| sc_valid_refills_def vs_all_heap_simps obj_at_def refill_budget_check_defs | ||
| update_sched_context_set_refills_rewrite schedule_used_defs) | ||
| method handle_overrun_simple | ||
| = (clarsimp simp: handle_overrun_def)?, |
There was a problem hiding this comment.
this looks nearly identical to the previous method, am I missing why we need two methods?
There was a problem hiding this comment.
They are slightly different. It's possible that they could be combined into one method that could be used instead of the two, but it could be rather annoying to try this.
| apply (case_tac list; simp) | ||
| done | ||
| method merge_nonoverlapping_head_refill_simple | ||
| = clarsimp simp: merge_nonoverlapping_head_refill_def refill_pop_head_def merge_refill_def |
There was a problem hiding this comment.
again consider local_method, I think this is only used once
| in hoare_strengthen_post[rotated]) | ||
| apply (fastforce simp: valid_refills_def vs_all_heap_simps) | ||
| apply (intro hoare_vcg_conj_lift_pre_fix; (solves head_insufficient_loop_simple)?) | ||
| apply (wpsimp wp: head_insufficient_loop_refills_sum) |
There was a problem hiding this comment.
this looks like you can combine the rest of the proof into a (wpsimp wp: ... | clarsimp simp: ...)+, I don't think there's much of interest here for the proof length
| vs_all_heap_simps refill_sufficient_def refill_capacity_def | ||
| MIN_BUDGET_nonzero sc_valid_refills_def vs_all_heap_simps | ||
| split: option.splits kernel_object.splits if_splits)+) | ||
| = clarsimp simp: handle_overrun_def, |
There was a problem hiding this comment.
again, not sure about these / local_method / folding into other methods;
the methods namespace is global, i.e. print_methods will print all these methods along with the others
| apply (rule bind_wp[OF _ get_refills_sp]) | ||
| apply (clarsimp simp: handle_overrun_def) | ||
| apply (wpsimp wp: valid_whileLoop | ||
| [where I="\<lambda>_ s. sc_refills_sc_at (\<lambda>refills. refills \<noteq> []) sc_ptr s"]) |
There was a problem hiding this comment.
Nice work. That was a much bigger change than I expected. I have minor/cleanup comments mostly.
On the "prove" commit, you're changing the spec, would be nice to have some more info, because the commit diff is huge, but the message makes it sound like something rather simple.
Test with seL4/seL4#1323