Prove decodeSchedControl_configureFlags_ccorres and decodeInvocation_ccorres
#902
Conversation
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
The definition of decode_sched_control_configure_flags is updated to align with the C. Additionally, TIME_ARG_SIZE/timeArgSize is made arch dependent, and its value is corrected for RISCV64. Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
michaelmcinerney
added
the
MCS
| @@ -25,6 +25,7 @@ arch_requalify_facts (A) | |||
| reply_bits_def | |||
| parse_time_arg_def | |||
| words_from_time_def | |||
| TIME_ARG_SIZE_def | |||
There was a problem hiding this comment.
Is this a good idea, given we want to do arch-split of MCS in the future? I guess it's consistent with the other ones, but when doing arch-split I'd rather keep the definition in Arch and then break it with RISCV64.TIME_ARG_SIZE_def in the places it's needed (and with a (* FIXME arch-split *) at the places where it's egregious.
I guess given how the rest are already leaking, now might not be the time, but the direction this goes in will cause friction later in a way that's annoying to detect. You'd have to notice that arch stuff is being leaked through the Arch interface after being unable to reconcile proofs on two arches, then go back to this point, investigate what this is, remove the requalify and do more rounds.
There was a problem hiding this comment.
Agreed, if we can we should not export the _def. Ideally we'd only really need it in generic theories in CRefine, and only some conditions exported in the rest. Not sure if that ideal case is easily achievable, but Raf's suggestion of using the fully qualified name with a FIXME should at least help us to find them later.
|
|
||
| lemma refillAbsoluteMax_size_helper: | ||
| "\<lbrakk>valid_cap' cap s; isSchedContextCap cap\<rbrakk> | ||
| \<Longrightarrow> MIN_REFILLS \<le> refillAbsoluteMax cap \<and> refillAbsoluteMax cap < 2 ^ LENGTH(64)" |
| \<and> (\<forall>v \<in> set extraCaps. s \<turnstile>' fst v) | ||
| \<and> (\<forall>v \<in> set extraCaps. \<forall>y \<in> zobj_refs' (fst v). ex_nonz_cap_to' y s) | ||
| \<and> sysargs_rel args buffer s) | ||
| \<and> isSchedControlCap cp) |
There was a problem hiding this comment.
indent looks off (on github at least)
| (Call decodeSchedControl_ConfigureFlags_'proc)" | ||
| apply (intro ccorres_gen_asm[simplified pred_conj_def]) | ||
| supply Collect_const[simp del] if_cong[cong] option.case_cong[cong] | ||
| sched_context_C_size[simp del] refill_C_size[simp del] |
There was a problem hiding this comment.
how come you need to hide the two _sizes?
| apply (clarsimp simp: maxPeriodUs_def word_less_nat_alt) | ||
| apply (force intro: mult_le_mono3[where a="5 * unat MAX_PERIOD_US"]) | ||
| apply (clarsimp simp: excaps_map_def neq_Nil_conv cte_wp_at_ctes_of dest!: interpret_excaps_eq) | ||
| done |
There was a problem hiding this comment.
usual comment: this proof is very hard to review without any guiding comments and not seeing the intermittent proof state myself
|
|
||
| lemma ct_in_state'_rewrite: | ||
| "ct_in_state' st s = st_tcb_at' st (ksCurThread s) s" | ||
| by (clarsimp simp: ct_in_state'_def cur_tcb'_def) |
There was a problem hiding this comment.
do we want to move such things to SR_lemmas? @lsf37
There was a problem hiding this comment.
In fact, isn't this just ct_in_state'_def?
In Invariants_H:
"ct_in_state' test \<equiv> \<lambda>s. st_tcb_at' test (ksCurThread s) s"
ct_in_state'_cur_tcb' should go into Invariants_H I think.
| apply (simp+)[3] | ||
| apply vcg | ||
| apply (rule ccorres_Cond_rhs) | ||
| apply (simp add: if_to_top_of_bind) |
There was a problem hiding this comment.
seeing a lot of if_to_top_of_bind ... are there multiple ifs in here, or is something dodgy with automation?
There was a problem hiding this comment.
It's a pattern in some of the decode proofs. I don't remember exactly where anymore (maybe here), but I remember doing the same for a few of these, mostly adjusting existing ones, to avoid blowup of if cases.
There was a problem hiding this comment.
Good progress. Minor comments on content.
Have an issue with the commit "rt spec+crefine: prove decodeSchedControl_ConfigureFlags_ccorres": it's doing too much. Doing a multi-arch restructure like that and making something arch-specific should be in its own commit. This will be particularly important when dealing with arch-split in future.
The decode_sched_control_configure_flags update can indeed go in with the proof commit.
| definition TIME_ARG_SIZE :: nat where | ||
| "TIME_ARG_SIZE \<equiv> 2" (* sizeof(ticks_t) / sizeof(word_t) *) |
There was a problem hiding this comment.
That comment is exciting, because it would actually make that definition generic. If you define it as what the comment says, only the C version of this will need to be arch specific. Not sure it does that much since words_from_time still will need to be arch specific, but you could add a comment with FIXME arch-split that this could be a generic definition so we remember when we get there.
Test with seL4/seL4#1472