clib: move ccorres_cond_both' to CCorresLemmas
#856
Conversation
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
michaelmcinerney
requested review from
Xaphiosis,
lsf37,
corlewis and
ryybrr
| and bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d" | ||
| shows "ccorres_underlying sr G r xf arrel axf | ||
| (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) | ||
| (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) |
There was a problem hiding this comment.
I really have no clue what this Collect is doing here
There was a problem hiding this comment.
This is what I mean in the first half of the comment: it allows you to specify a condition on the C state, much like you would write in ccorres_cond something like ccorres_cond[where R="%s. curThread = ksCurThread s"]. Normally we would use this rule with this Q' just equal to \top, but I guess it's just providing maximum flexibility
There was a problem hiding this comment.
Yes, I agree with that part, but it's an odd phrasing. Typically we write Q' in rules and instantiate it with UNIV, not put Collect Q' in rules and instantiate with \<top>. I don't know of many rules I've seen that use the Collect form, and it results in confusion of concepts.
There was a problem hiding this comment.
Yes, I agree. I didn't write this rule, of course, I'm just moving it. Would it be worth changing it so that Q' is a set of C states? It would be quite a pain, considering that this rule is used on all architectures in CRefine, and it's used a lot in MCS.
There was a problem hiding this comment.
In that case, I'd suggest a FIXME, so that you don't waste your time on this, but so that future victims are aware that this is not the style to go with.
| A stronger version of @{thm ccorres_cond_both}, which allows the user to specify a condition on | ||
| the C state when showing equality of the guards of the conditionals, and which will provide the | ||
| relevant alternative on the truth of the guard of the @{term If} statement as an assumption in the | ||
| @{term ccorres_underlying} assumptions.\<close> |
There was a problem hiding this comment.
Bit wordy, this one.
suggestion, something like: "
A stronger version of @{thm ccorres_cond_both}, which allows specifying a C state predicate
when showing equality of the conditionals' guards, and which supplies the relevant @{term If} guard truth to the @{term ccorres_underlying} assumptions.›"
No description provided.