refill_budget_check_ccorres
#821
Conversation
michaelmcinerney
added
the
MCS
proof/crefine/RISCV64/Schedule_C.thy
Outdated
| apply (rule refill_head_ccorres) | ||
| apply clarsimp | ||
| apply clarsimp | ||
| apply clarsimp |
proof/crefine/RISCV64/Schedule_C.thy
Outdated
| 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.
There was a problem hiding this comment.
I was actually able to remove a few instances of normalise_obj_at' from this proof. I think they were just copied from other proofs that used updateSchedContext ccorres rules. I most often use normalise_obj_at' after using something like obj_at_cslift_tcb or obj_at_cslift_sc, or arguing about there being an object at the tcbSchedContext, or something.
| 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.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
michaelmcinerney
force-pushed
the
michaelm-rbc_ccorres
branch
from
323bee6 to
0e7f485
Compare
michaelmcinerney
force-pushed
the
michaelm-rbc_ccorres
branch
from
e1f8660 to
b54c251
Compare
This also includes a refactoring of the definitions associated with refill_budget_check in the ASpec and the Haskell, in order to ease the ccorres proof. While the semantics are preserved, this necessitated a rather large change in AInvs, mostly due to the rather specialised lemmas regarding valid_refills. Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
michaelmcinerney
force-pushed
the
michaelm-rbc_ccorres
branch
from
b54c251 to
4c8055d
Compare
No description provided.