Conversation
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
michaelmcinerney
added
the
MCS
proof/crefine/RISCV64/Finalise_C.thy
Outdated
| lemma option_to_ctcb_ptr_canonical: | ||
| "\<lbrakk>pspace_canonical' s; tcb_at' tcb s\<rbrakk> | ||
| \<Longrightarrow> option_to_ctcb_ptr (Some tcb) | ||
| = tcb_Ptr (sign_extend canonical_bit (ptr_val (tcb_ptr_to_ctcb_ptr tcb)))" |
There was a problem hiding this comment.
I'm surprised we don't have this yet, it looks like something we'd want all over the place.
In AARCH64 we introduced make_canonical for similar things (just the sign_extend part) -- the definition from AARCH64 doesn't fit here, because AARCH64 doesn't sign extend, for RISCV64 it'd probably be exactly make_canonical = sign_extend canonical_bit. I'm not sure it makes sense to introduce that here now into RISCV64, because it would probably introduce a bit of noise for not too much gain, but if you find yourself having to do slots of things about sign_extend canonical_bit then maybe consider it.
In any case, we should move this lemma somewhere high up in the hierarchy, at least TcbAcc_C, so that it is visible to earlier proofs.
There was a problem hiding this comment.
This was just moved up in this file, but I can put it in TcbAcc_C.
There was a problem hiding this comment.
Possibly not even from MCS, but it would still be good to move it up to make sure it's visible.
| lemma cancelIPC_ccorres1: | ||
| assumes cteDeleteOne_ccorres: |
proof/crefine/RISCV64/Finalise_C.thy
Outdated
| lemma obj_at_cslift_ntfn: | ||
| "\<lbrakk>obj_at' P ntfn s; (s, s') \<in> rf_sr\<rbrakk> | ||
| \<Longrightarrow> \<exists>ko ko'. ko_at' ko ntfn s \<and> P ko \<and> cslift s' (Ptr ntfn) = Some ko' | ||
| \<and> cnotification_relation (cslift s') ko ko'" |
There was a problem hiding this comment.
Is this one moved from somewhere? It should be moved high up, to wherever we have basic lemmas about notifications (not sure if PSpace_C is too high, maybe TcbAcc_C. We should resurrect that tool that tells us the highest theory something can go into.).
There was a problem hiding this comment.
style nitpick: the indentation of the /\ looks off by one
There was a problem hiding this comment.
This is new, but I can move it. It's just the notification version of other lemmas like this that we have.
And there's no meta for-all here. Did you mean another lemma?
There was a problem hiding this comment.
Oh that's a conjunction, sorry. It looks OK to me in jedit. In the second line of the conclusion, the /\ is aligned with the ko_at' because it's all part of the unquantified bit.
There was a problem hiding this comment.
Yes, I meant that conjunction. Perfectly possible that it just looks off because of the GitHub symbol rendering.
lsf37
left a comment
lsf37
left a comment
There was a problem hiding this comment.
Looking good, only very minor comments/queries. Nice to see how adding the assertions simplifies a lot of the preconditions!
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
2 participants
Test with seL4/seL4#1474