Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

arch-split Refine up to Invariants_H for X64 #842

Merged
merged 9 commits into from
Jan 6, 2025
Merged

arch-split Refine up to Invariants_H for X64 #842

merged 9 commits into from
Jan 6, 2025
+1,758 −4,255

Conversation

Xaphiosis
Copy link
Member

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-split branch (from #833).

The approach I used was:

  1. I put the kernel_data_refs junk first, along with the fixup of the locale graph (I missed two edges)
  2. All the tweaks to Invariants_H that are needed to make it work with X64 (see commit message)
  3. Update AARCH64 Refine to deal with (2).
  4. Use result of (3) to copy ArchInvsDefs/Lemmas_H from AARCH64 to X64, and delete X64's Invariants_H
  5. Put the X64 definitions and invariants into ArchInvsDefs/Lemmas_H manually, to generate at least a comprehensible diff
  6. Fix up X64 Refine, and then CRefine

Here are some observations I had along the way:

  • projectKOs are not in simp on X64 or earlier arches, but we all agree they should be
  • tcb_cte_cases_def tcb_cte_cases_neqs can often replace using tcb_cte_cases_def cteSizeBits_def and 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_def is still exported into generic context for now; doesn't seem too dangerous, but someday it might be nice to fix that

@Xaphiosis
ainvs+refine: standardise kernel_data_refs location
f6a7d30 
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]>
@Xaphiosis
refine: remove kernel_data_refs from InvariantsPre_H
73a0494 
Now requalified in Invariants_H.

Signed-off-by: Rafal Kolanski <[email protected]>
@Xaphiosis
refine: fix InvariantsPre_H locale hierarchy
86702e9 
(also add cte_heap)

This should be squashed before arch-split goes into master.

Signed-off-by: Rafal Kolanski <[email protected]>
@Xaphiosis
refine: Invariants_H: update generic interface for X64
85b8001 
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]>
@Xaphiosis
aarch64 refine: update for X64-related interface changes
935fc31 
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]>
@Xaphiosis Xaphiosis added the arch-split splitting proofs into generic and architecture dependent label Dec 18, 2024
@Xaphiosis Xaphiosis requested review from lsf37 and corlewis December 18, 2024 04:12
@Xaphiosis Xaphiosis changed the base branch from master to arch-split December 18, 2024 04:13
@lsf37
Copy link
Member

lsf37 commented Dec 19, 2024

  • projectKOs are not in simp on X64 or earlier arches, but we all agree they should be

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.

  • tcb_cte_cases_def tcb_cte_cases_neqs can often replace using tcb_cte_cases_def cteSizeBits_def and 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?

Even just lemmas tcb_cte_cases = tcb_cte_cases_def tcb_cte_cases_neqs would probably be quite nice already.

  • tcbBlockSizeBits_def is still exported into generic context for now; doesn't seem too dangerous, but someday it might be nice to fix that

It might be worth starting an issue where we collect some of these smaller TODO items so that they don't all become FIXMEs.

lsf37
lsf37 reviewed Dec 19, 2024
View reviewed changes
proof/refine/AARCH64/ArchInvsDefs_H.thy
Comment on lines +44 to +48
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>"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

lsf37
lsf37 approved these changes Dec 19, 2024
View reviewed changes
Copy link
Member

@lsf37 lsf37 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@Xaphiosis
Copy link
Member Author

  • projectKOs are not in simp on X64 or earlier arches, but we all agree they should be

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.

  • tcb_cte_cases_def tcb_cte_cases_neqs can often replace using tcb_cte_cases_def cteSizeBits_def and 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?

Even just lemmas tcb_cte_cases = tcb_cte_cases_def tcb_cte_cases_neqs would probably be quite nice already.

  • tcbBlockSizeBits_def is still exported into generic context for now; doesn't seem too dangerous, but someday it might be nice to fix that

It might be worth starting an issue where we collect some of these smaller TODO items so that they don't all become FIXMEs.

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?

@lsf37
Copy link
Member

lsf37 commented Dec 19, 2024

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?

yes

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?

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 lemmas tcb_cte_cases = tcb_cte_cases_def tcb_cte_cases_neqs, because that might make life easier during the splitting already.

@Xaphiosis
x64 refine: copy ArchInvsDefs/Lemmas_H from AARCH64
0e10ac6 
Sets up X64 for Invariants_H arch-splitting using AARCH64 as a template.
Includes removal of X64 Invariants_H.

Signed-off-by: Rafal Kolanski <[email protected]>
@Xaphiosis
x64 refine: update ArchInvsDefs/Lemmas for X64
38174e1 
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]>
@Xaphiosis
x64 refine: arch-split up to InvariantUpdates_H
fe7cf9c 
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.

Otherwise:
- projectKOs is not in the simpset
- ioport_control/valid_arch_mdb_ctes hasn't been renamed in all cases, only
  made to work for now
- the power-of-two vs mask situation is still a mess, requiring changing
  proofs to go one way or the other
- unfolding tcb_cte_cases_def would benefit from tcb_cte_cases_neqs
  being in the simpset so that people avoid unfolding cteSizeBits when
  not necessary, but that can be done via a separate pass later

Signed-off-by: Rafal Kolanski <[email protected]>
@Xaphiosis
x64 crefine: minimal fixups for arch-split up to InvariantUpdates_H
a60f6c2 
When possible, the proof/fix was ported from AARCH64 to reduce future
diffs.

Signed-off-by: Rafal Kolanski <[email protected]>
@Xaphiosis
Copy link
Member Author

Xaphiosis commented Jan 6, 2025 •
edited
Loading

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 lemmas tcb_cte_cases = tcb_cte_cases_def tcb_cte_cases_neqs, because that might make life easier during the splitting already.

This has the disadvantage of being difficult to grep for later vs the constant. For the next PR, how about I add a tcb_cte_cases_def' with a FIXME to add to simpset? Then grepping for the def' version will show places that can trivially be replaced by the def version once we add the neqs to the simpset.

@Xaphiosis Xaphiosis merged commit 493e71a into arch-split Jan 6, 2025
10 of 14 checks passed
@Xaphiosis Xaphiosis deleted the arch-split_x64 branch January 6, 2025 10:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lsf37 lsf37 lsf37 approved these changes

@corlewis corlewis Awaiting requested review from corlewis

Assignees
No one assigned
Labels
arch-split splitting proofs into generic and architecture dependent
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@Xaphiosis @lsf37