Remove valid_ioports' from X64 Refine #830
Conversation
Needed in performX64PortInvocation for InvokeIOPortControl in order to get a hold of all_io_ports_issued' in arch_performInvocation_invs'. Signed-off-by: Rafal Kolanski <[email protected]>
With the exception of performX64PortInvocation_corres and arch_performInvocation_invs', the knowledge about IO port cap validity is unnecessary in Refine. For those two lemmas, we added an assertion and a cross lemma to re-derive the information from valid_ioports over the state relation. This leads to a simlified formulation of post_cap_delete_pre' such that it satisfies the minimum requirements for the arch-generic formulation of cap finalisation proofs. Signed-off-by: Rafal Kolanski <[email protected]>
Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
added
proof engineering
| apply (rename_tac p' cte') | ||
| apply (drule (1) pspace_relation_cte_wp_atI'[OF state_relation_pspace_relation ctes_of_cte_wpD]) | ||
| apply clarsimp | ||
| apply (clarsimp dest!: Retype_AI.F[THEN iffD2] del: subsetI) |
There was a problem hiding this comment.
Wow, Retype_AI.F is an impressively useful name
There was a problem hiding this comment.
Oh yes, I had a moment there as well going "no one gave a better name to this rather useful lemma? F?!"
| (* extra constraints on IO ports are not needed since there is no valid_ioports to preserve in | ||
| Refine *) |
There was a problem hiding this comment.
Hmm, this comment sort of feels like it's only useful now while we still have the context that there used to be extra constraints. Do you think it will still make sense in the future when we've forgotten that valid_ioports' ever existed and had to be reasoned about in Refine?
There was a problem hiding this comment.
This comment exists for only one reason: someone doing a git log in future and seeing that the definition has changed to drop very sane looking IO port cap constraints, replacing them with the exact same thing as IRQ handlers, and going "WTF happened". The comment will then indicate that the reason this is possible is due to valid_ioports' being gone. Does that actually help?
There was a problem hiding this comment.
I think that this is almost a style decision, but for that case shouldn't the person doing the git log get that information from the commit message?
My preference is that comments should make sense with the current state of the repository, and I sort of feel like someone looking at this definition in the future won't be expecting extra constraints to be needed, and will then be confused by the comment unless they do do that git log.
It's hard to get into that future mindspace though, so I definitely might be wrong and won't argue further if you want to keep the comment in.
There was a problem hiding this comment.
I'll keep it then, if only to help jog my memory if/when this comes up in the future... because getting this formulation right took me nearly a day and it wasn't at all obvious why IO port cap constraints were no longer needed, but this thing was. I think I ended up trying every combination at some point.
🦆🦆🦆 This started with examining the IO port situation and arch-split, in particular complications due to the FC proofs on all architectures mentioning IO ports even when the architectures did not have them.
For AInvs, it was possible to fold valid_ioports into valid_arch_state and do the same for valid_ioports' and valid_arch_state' on X64 Refine... which I initially did in #829 but it turned out that for Refine this was ugly and didn't make a lot of sense.
At some point when talking with @corlewis about this, he suggested that it might be possible to do some crossing-over and reduce the IO port invariant burden in X64 Refine. After a lot of pain, I managed to figure out a way to bash the specs and proofs into submission, getting rid of valid_ioports' entirely. That's this PR.
With apologies to @corlewis , this PR now has to get merged before #829 is, because the X64 Refine work on that PR is going to get largely clobbered by these changes (all the AInvs + AC/IF + cleanup of other arches still applies though).
@mbrcknl you might find this one amusing, a sea of red demonstrating the advancement in our proof techniques over time :)