Small IPC lemmas #822
Small IPC lemmas #822
Conversation
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
This is achieved by asserting active_sc_at' in the appropriate places within the Haskell. Signed-off-by: Michael McInerney <[email protected]>
Moved, along with some associated lemmas, in order for these results to be available for postpone_ccorres. Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
michaelmcinerney
added
the
MCS
| lemma obj_at_cslift_ntfn: | ||
| fixes P :: "notification \<Rightarrow> bool" | ||
| shows "\<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.
Do you actually need the type annotation/fixes? I would have thought the cnotification_relation would constrain ko, which then should constrain P.
There was a problem hiding this comment.
I can check this. This lemma started off life as a copy paste of the analogous lemma for TCBs and was then modified. That’s where the fixes and type annotations would be from
| apply wpsimp | ||
| apply (vcg exspec=refill_sufficient_modifies) | ||
| apply (rule ccorres_cond_seq) | ||
| apply (rule ccorres_cond_false) |
There was a problem hiding this comment.
when you do the ccorres_cond_seq + _true or _false combo, you're relying on someone having the proof state loaded in front of them. I much prefer having comments saying what is going on, because I have no idea whatsoever what branches this proof is following
| valid_sched_context'_def from_bool_def | ||
| split: option.splits bool.splits) | ||
| apply ceqv | ||
| apply (rule ccorres_cond[where R=\<top>]) |
There was a problem hiding this comment.
I don't like how we've reverted to not having any comments in CRefine. I want to know, what are branches we're looking at...
| sign_extend_canonical_address | ||
| split: ntfn.splits) | ||
| apply fastforce | ||
| apply (simp add: refill_buffer_relation_def image_def dom_def Let_def typ_heap_simps |
There was a problem hiding this comment.
there's a good chance some/all of these simps can be compressed
There was a problem hiding this comment.
I think generally this is good, but I'm noticing a regression to the mean of not adding comments to guide the reader and future repairer, especially in CRefine, which concerns me a bit. I have too much joyous experience with proofs that break, and then I when I have to fix them I don't know what they were trying to do since whoever wrote them depended on the implicit state to inform the reader.
No description provided.