arch-split Refine up to Invariants_H for X64 #842
Conversation
Even though comments indicate it should be moved somewhere, at least we can make it consistent and have them all in ArchInvariants_AI for now. Signed-off-by: Rafal Kolanski <[email protected]>
Now requalified in Invariants_H. Signed-off-by: Rafal Kolanski <[email protected]>
(also add cte_heap) This should be squashed before arch-split goes into master. Signed-off-by: Rafal Kolanski <[email protected]>
This required: - adding valid_arch_mdb_ctes (for ioport_control) (possible cross candidate) - valid_arch_obj' now takes a state - adding pspace_in_kernel_mappings' - adding kernel_mappings to valid_cap' (needed for X64 and RISCV64; since pspace_in_kernel_mappings' is only proved at the Refine level, it can't be crossed over) Signed-off-by: Rafal Kolanski <[email protected]>
Mostly dealing with valid_arch_mdb_ctes (ioport_control wrapper), pspace_in_kernel_mappings, kernel_mappings and valid_arch_cap taking a state. Signed-off-by: Rafal Kolanski <[email protected]>
Signed-off-by: Rafal Kolanski <[email protected]>
Migrate X64 concepts into the files copied from AARCH64, in order to get X64 definitions/invariants that conform to arch-split interface. Signed-off-by: Rafal Kolanski <[email protected]>
Updates the rest of X64 Refine to conform to the generic arch-split invariant interface. When things broke and when possible, we took the proof or chunks of proof from AARCH64. There is a major outstanding issue: - pspace_in_kernel_mappings combined with an absence of kernel_mappings from valid_cap' for the Untyped case results in several sorries Otherwise: - projectKOs is not in the simpset - ioport_control/valid_arch_mdb_ctes hasn't been renamed in all cases, only made work for now - the power-of-two vs mask situation is still a mess, requiring changing proofs to go one way or the other Signed-off-by: Rafal Kolanski <[email protected]>
When possible, the proof/fix was ported from AARCH64 to reduce future diffs. Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
added
the
arch-split
Agreed. Putting them into the simset does lead to some failures, but they should be few. The main annoyance is a lot of warnings, but they could be removed separately.
Even just
It might be worth starting an issue where we collect some of these smaller TODO items so that they don't all become FIXMEs. |
| definition kernel_mappings :: "machine_word set" where | ||
| "kernel_mappings \<equiv> UNIV" | ||
|
|
||
| definition pspace_in_kernel_mappings' :: "kernel_state \<Rightarrow> bool" where | ||
| "pspace_in_kernel_mappings' \<equiv> \<top>" |
There was a problem hiding this comment.
Not for now, but maybe to note in a FIXME or issue: we should really rename these two, because pspace and cap references are of course not in the kernel mappings, but in the area mapped by the kernel mappings (maybe pspace_in_kernel_window', which I think we did add in RISCV64 AInvs).
For splitting, I'd leave them, though, the rename can probably be automated by script at some later point.
There was a problem hiding this comment.
Massive amount of work! And I cannot find anything to complain about either :-). Really nice to see an effective > 2k lines removed even at this stage already.
There are FIXMEs, of course, but I we will get to these points later and I had expected much worse from how far apart X64 and AARCH64 in terms of concepts.
Let me confirm: you agree that handling some of these would be good, but not as part of this PR, and so I should make an issue? Or should I add some of these to this PR? I think I can try do some of these on the next arch, or if you are keen while I'm away, though I'll have a week in Jan before I leave to maybe get another arch or two through, leaving one for mop-up (RISCV64?) and some of these fixes. Then again if they don't get fixed on next arch, they'll get duplicated. Hmm. Thoughts? |
yes
It's ok for them to get duplicated in the arch split and then later cleaned up. The only one we could deploy now already is |
You'll have to review this commit-by-commit. I tried to keep them as separate as possible, and some should probably get squashed into commits that are already on the
arch-splitbranch (from #833).The approach I used was:
Here are some observations I had along the way:
tcb_cte_cases_def tcb_cte_cases_neqscan often replace usingtcb_cte_cases_def cteSizeBits_defand is much faster; maybe I should add the neqs to some kind of bundle so tcb_cte_cases_def includes it automatically? what's a good way of doing that?tcbBlockSizeBits_defis still exported into generic context for now; doesn't seem too dangerous, but someday it might be nice to fix that