Prove cancelIPC_ccorres1
#831
Conversation
Signed-off-by: Nick Spinale <[email protected]>
nspin
force-pushed
the
pr/prove-cancelipc-ccorres-1
branch
from
6ccdeb1
to
67641d4
Compare
| st_tcb_at' (\<lambda>st. (isBlockedOnSend st \<or> isBlockedOnReceive st) | ||
| \<and> blockingObject st = ep) thread | ||
| and ko_at' ep' ep) | ||
| {s. epptr_' s = Ptr ep} |
There was a problem hiding this comment.
Moving this from the preconditions to the assumptions might seem convenient here, but in general this move is against the flow of automation, e.g. if you want to use ctac; the idea is preconditions bubble up the stack and are resolved at the end. Is there any reason you had to change this?
| and st_tcb_at' (\<lambda>st. (\<exists>oref cg. st = Structures_H.BlockedOnReceive oref cg (Some replyPtr)) | ||
| \<or> st = Structures_H.BlockedOnReply (Some replyPtr)) | ||
| tcbPtr | ||
| and obj_at' (\<lambda>reply. replyTCB reply = Some tcbPtr) replyPtr) |
There was a problem hiding this comment.
indentation: the advantage of putting operators on the left is we can align them with the previous line in most cases (see style guide), so and should align with valid_tcbs'.
Also, the ∨ belongs under the ∃, i.e. under st =
| assumes "ts = BlockedOnReceive bo bicg ro" | ||
| shows "ro \<noteq> Some 0" | ||
| using assms | ||
| by (auto simp: valid_tcb_state'_def) |
There was a problem hiding this comment.
For these simple lemmas, declaring all the assumptions via assumes and then immediately using assms doesn't gain a lot in terms of readability. You can compress them vertically a lot, e.g.:
lemma BlockedOnReceive_replyObject_no_0:
"⟦ no_0_obj' s; valid_tcb_state' ts s; ts = BlockedOnReceive bo bicg ro ⟧
⟹ ro ≠ Some 0"
by (auto simp: valid_tcb_state'_def)
As an aside, rules tend to match better in Isabelle when their first assumption is more specific, since you usually want to make it unify with one of your goal assumptions. In this case valid_tcb_state' ts s or ts = BlockedOnReceive bo bicg ro might be more useful to go first.
Feel free to ask us questions if it's not clear why.
|
|
||
| lemma ctcb_relation_BlockedOnSend_blockingObject: | ||
| assumes "ctcb_relation tcb ctcb" | ||
| assumes "BlockedOnSend bo bib bicg bicgr biic = tcbState tcb" |
There was a problem hiding this comment.
did you invent these bo bib bicg bicgr biic style variable names, or did they come from other lemmas/definitions?
| shows "ep_at' bo s" | ||
| using assms | ||
| apply - | ||
| apply (drule (1) tcb_in_valid_state') |
There was a problem hiding this comment.
if you compress these lemmas like I outlined, you won't need the use assms, and therefore won't need to chain in the facts with apply -. There's also a chance that you might be able to fold the drule (1) tcb_in_valid_state' into the fastforce, so that the proof ends up as:
by (fastforce dest!: tcb_in_valid_state' simp: obj_at'_def valid_tcb_state'_def)
| "\<exists>tcb. ko_at' tcb thread s \<and> tcbState tcb = BlockedOnReceive bo bicg (Some ro)" | ||
| by (clarsimp simp: st_tcb_at'_def obj_at'_def) | ||
| from sy and vo and st and ra and ko show ?thesis | ||
| apply - |
There was a problem hiding this comment.
you don't need apply - for tactics like simp/clarsimp/fastforce/auto/etc, it's mostly for direct rule invocations (obvious, I know :/)
you can also shave off the ko by using with instead of from
| \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sym_refs_asrt s\<rbrace>" | ||
| proof - | ||
| have sy: "threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>sym_refs_asrt\<rbrace>" | ||
| by - (unfold sym_refs_asrt_def, wpsimp wp: threadSet_state_refs_of', simp, |
There was a problem hiding this comment.
if you're doing Isar-style proofs, it makes more sense to do:
unfolding sym_refs_asrt_def
by wpsimp
(force simp: tcb_bound_refs'_def)+
|
|
||
| lemma thread_state_to_tsType_eq_BlockedOnSend: | ||
| "(thread_state_to_tsType ts = scast ThreadState_BlockedOnSend) | ||
| = (\<exists>bo bib bicg bicgr biic. ts = BlockedOnSend bo bib bicg bicgr biic)" |
There was a problem hiding this comment.
indentation on =, also, do these rules really benefit you most as a rewrite rather than a destruction/elimination rule?
| "(thread_state_to_tsType ts = scast ThreadState_BlockedOnSend) | ||
| = (\<exists>bo bib bicg bicgr biic. ts = BlockedOnSend bo bib bicg bicgr biic)" | ||
| by (cases ts, simp_all add: ThreadState_defs) | ||
|
|
||
| lemma cancelIPC_ccorres1: |
There was a problem hiding this comment.
I have more comments for the proof of this lemma, but it would be useful to know how much of the proof is copied, as a bunch of them will be style-and-compression related.
| \<and> valid_tcbs' s | ||
| \<and> (ro = None \<longrightarrow> True) | ||
| \<and> (\<forall>x. ro = Some x \<longrightarrow> obj_at' (\<lambda>reply. replyTCB reply = Some thread) x s)" | ||
| in hoare_post_imp) |
There was a problem hiding this comment.
This kind of explicit goal rephrasing is a sign that backwards reasoning is breaking down for some reason. Usually that's not a good sign, but it is at times unavoidable. Any thoughts on what happened?
|
Firstly, welcome, and huge congratulations for being one of the very very few (maybe the second person ever?) to be a third-party contributor to the verification side of seL4. The proofs look ok, comments are mainly for improvements / learning / style. |
Requires seL4/seL4#1358, which fixes an apparent potential bug that I discovered while working on this proof. That PR also sneaks in a few trivial changes that made verification a bit easier.
I weakened the preconditions in the still-unproven
reply_unlink_ccorreslemma. They now correspond to those inreplyUnlinkTcb_corres.Test with seL4/seL4#1358