Several sorries in IpcCancel_C
#789
Conversation
michaelmcinerney
added
the
MCS
Refine does seem to shrink most of the time I have to touch it. I often do add asserts and might need to strengthen an abstract guard as a result, but I am often able to remove lines by making proofs that were forwards backwards instead, or removing Hoare triples about properties that we no longer need, like |
michaelmcinerney
force-pushed
the
michaelm-isSchedulable_ccorres
branch
from
08ea860
to
eecc6ee
Compare
proof/refine/RISCV64/IpcCancel_R.thy
Outdated
| @@ -3079,7 +3037,7 @@ lemma ct_not_in_ntfnQueue: | |||
|
|
|||
| lemma sch_act_wf_weak[elim!]: | |||
| "sch_act_wf sa s \<Longrightarrow> weak_sch_act_wf sa s" | |||
| by (case_tac sa, (simp add: weak_sch_act_wf_def)+) | |||
| by (case_tac sa, (fastforce simp: weak_sch_act_wf_def st_tcb_at'_def obj_at'_def)+) | |||
There was a problem hiding this comment.
While you're changing this line, I think this would be slightly better style
| by (case_tac sa, (fastforce simp: weak_sch_act_wf_def st_tcb_at'_def obj_at'_def)+) | |
| by (cases sa; fastforce simp: weak_sch_act_wf_def st_tcb_at'_def obj_at'_def) |
| supply Collect_const[simp del] | ||
| if_split[split del] |
There was a problem hiding this comment.
Incredibly minor, but do we have a style preference between these?
| supply Collect_const[simp del] | |
| if_split[split del] | |
| supply Collect_const[simp del] if_split[split del] |
There was a problem hiding this comment.
Reviewing further, we also sometimes see this alternative
| supply Collect_const[simp del] | |
| if_split[split del] | |
| supply Collect_const[simp del] | |
| supply if_split[split del] |
There was a problem hiding this comment.
My thoughts here were that we might like to emphasise that we're doing different sorts of things. Sometimes I add a bunch of things to the simp set and then if if_split[split del] is right alongside, it's hard to see. So I thought maybe we'd like one line per attribute, or whatever the correct terminology is. But I'm happy to go along with whatever
There was a problem hiding this comment.
Hmm, now that you point out the different attributes I think I like your approach
| (invs' | ||
| and cte_wp_at' (\<lambda>ct. w = -1 \<or> cteCap ct = NullCap | ||
| \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot) |
There was a problem hiding this comment.
This indentation doesn't seem quite right yet, at first glance I was still confused before realising that the final ∨ is inside the cte_wp_at'. This looks like a bit of a painful one to do properly without some awkward linebreaks, but at the very least I think the final line should be indented two more.
There was a problem hiding this comment.
Ah I misread this bit. I can open it up and redo it
proof/refine/RISCV64/IpcCancel_R.thy
Outdated
| by (case_tac sa, (fastforce simp: weak_sch_act_wf_def st_tcb_at'_def obj_at'_def)+) | ||
| by (clarsimp simp: weak_sch_act_wf_def) |
There was a problem hiding this comment.
Haha, that's a lot nicer than what I suggested!
There was a problem hiding this comment.
I significantly weakened weak_sch_act_wf as part of this PR, so it really didn't need much. I should have looked more closely when I first came across this.
About the weakening: we've got valid_sched_action in AInvs that has lots of information that we can cross if we need. I really just wanted there to be a TCB at the switch to target to make CRefine easier in a few spots. We often definitely do want a TCB somewhere so we can argue about NULL properly, together with no_0_obj'
This proves ccorres rules for isSchedulable, rescheduleRequired, possibleSwitchTo, and setThreadState, including variants for when sch_act_simple holds. This also changes the Haskell definition of isSchedulable to more closely align with the C, to ease the proof of isSchedulable_ccorres. Signed-off-by: Michael McInerney <[email protected]>
michaelmcinerney
force-pushed
the
michaelm-isSchedulable_ccorres
branch
from
e044074
to
63f0cde
Compare
Please see the commit message