refill_budget_check_ccorres
#821
Conversation
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
michaelmcinerney
added
the
MCS
| 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
There was a problem hiding this comment.
I think in these cases, it's nicest to just have it all on the one line, even though it does go over the 100 character blue line a little bit (by 5 characters or so). If that definitely doesn't sound good, then I can go with your suggestion.
| 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.
| 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.
| 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
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