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

remove valid_arch_mdb_ctes #849

Merged
merged 3 commits into from
Feb 19, 2025
Merged

remove valid_arch_mdb_ctes #849

merged 3 commits into from
Feb 19, 2025

Conversation

lsf37
Copy link
Member

@lsf37 lsf37 commented Jan 31, 2025

Cross over the contents of valid_arch_mdb_ctes from the abstract side after proving the missing bits as invariants.

Introduces the assertion archMDBAssertions in Haskell, which is defined generically as arch_mdb_assert (ctes_of s). arch_mdb_assert in turn is architecture dependent and True anywhere that is not X64.

This took quite a bit longer than I had anticipated, and doesn't actually remove that many lines of proof, but it hopefully removes many annoying lines that we would have had to write in the future for arch split to continue. So overall still worth it, I think.

This is on top of PR #847 -- when we start RISCV64 that should probably go on top of this work to avoid duplication.

@lsf37 lsf37 requested a review from Xaphiosis January 31, 2025 02:19
@lsf37 lsf37 added the arch-split splitting proofs into generic and architecture dependent label Jan 31, 2025
@lsf37
Copy link
Member Author

lsf37 commented Jan 31, 2025

This is on top of PR #847 -- when we start RISCV64 that should probably go on top of this work to avoid duplication.

Actually, it is better to do it the other way around. I haven't applied the changes to RISCV64 here, because that one doesn't work yet, but they are probably much easier to apply after RISCV64 is split than trying to get the split to work on things that are broken because of the changes here. So RISCV64 split without this PR first, then I can adjust this PR, and then everything should be fine.

@Xaphiosis Xaphiosis force-pushed the arch-split_arm branch 2 times, most recently from 50c3892 to 6de46b6 Compare February 16, 2025 21:37
Base automatically changed from arch-split_arm to arch-split February 16, 2025 21:39
@Xaphiosis Xaphiosis force-pushed the arch-split branch 3 times, most recently from 9b1f4c2 to 3a9be00 Compare February 16, 2025 22:09
Xaphiosis
Xaphiosis reviewed Feb 16, 2025
View reviewed changes
proof/refine/X64/CSpace_R.thy
@@ -4876,6 +4786,15 @@ lemma maskedAsFull_revokable_safe_parent:

context begin interpretation Arch . (*FIXME: arch-split*)

(* FIXME arch-split: generic statement, arch specific proof *)
Copy link
Member

Choose a reason for hiding this comment

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

ok to leave here, but I should ask whether there's a better place...

Copy link
Member Author

Choose a reason for hiding this comment

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

I was going to leave that question for you :-). There probably is eventually, but for now I think leaving it in this theory is good.

Copy link
Member Author

Choose a reason for hiding this comment

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

(Will leave this in for later when we get there in the arch split process)

Xaphiosis
Xaphiosis reviewed Feb 16, 2025
View reviewed changes
proof/invariant-abstract/X64/ArchInvariants_AI.thy
@@ -1051,6 +1051,17 @@ definition
where
"valid_x64_irq_state irqState \<equiv> \<forall>irq > maxIRQ. irqState irq = IRQFree"

definition ioport_control_unique_2 :: "(cslot_ptr \<Rightarrow> cap option) \<Rightarrow> bool" where
Copy link
Member

Choose a reason for hiding this comment

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

might be good to have a comment here about what this means and its intent/use for crossing to Refine

Copy link
Member

Choose a reason for hiding this comment

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

Also, for my own curiosity since I wasn't a part of this: how did you come up with this as the necessary invariant?

Copy link
Member Author

Choose a reason for hiding this comment

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

it's the same invariant as what used to be in Refine minus the bits that are already proved elsewhere in AInvs

Copy link
Member Author

Choose a reason for hiding this comment

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

(comment added)

@Xaphiosis
Copy link
Member

Looks good. Thank you for doing this!
The upstream conflicts are my fault due to the arch-split merge situation. Apologies.

These parts from non-x64 InvariantUpdates_H should be able to go after your changes:

(* FIXME arch-split: valid_arch_mdb_ctes only exists to contain ioport_control on x64, and it is not
   yet clear what the best way to arch-split it is, or whether it can be crossed from AInvs.
   Therefore, for now, export the truth that it doesn't do anything on this arch beyond this point *)
arch_requalify_facts valid_arch_mdb_ctes_def
lemmas [simp] = valid_arch_mdb_ctes_def

and from Invariants_H, the requalify of valid_arch_mdb_ctes as well as dropping it from the definition of valid_mdb_ctes if that already hasn't happened.

Also, upstream got RISCV64 as well now.

Base automatically changed from arch-split to master February 17, 2025 01:16
@lsf37
Copy link
Member Author

lsf37 commented Feb 17, 2025

The conflicts disappear after rebase, so no problem at all. I'll have a look at fixing up the review feedback and RISCV.

@lsf37 lsf37 self-assigned this Feb 18, 2025
lsf37 added 3 commits February 19, 2025 08:20
@lsf37
x64 ainvs: prove uniqueness of IOPortControlCaps
dc8c3a6 
This invariant is currently proved on the Haskell level only. This
commit is in preparation of removing the invariant from the Haskell
level, crossing it over via assertions.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
haskell+design: archMDBAssertions in cteInsert
643c68d 
Introduce the name and assertion "archMDBAssertions" in cteInsert so
that specific architectures can make additional MDB assumptions (e.g.
IOControlPortCap uniqueness in X64).

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
refine+crefine: remove valid_arch_mdb_ctes
2685c3e 
- replace the ioport_control invariant with archMDBAssertions
- remove lemmas needed only for the invariant
- add corresponding crossing lemmas for caps_of_state based on existing
  older cte_wp_at lemmas

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Xaphiosis
Xaphiosis approved these changes Feb 19, 2025
View reviewed changes
Copy link
Member

@Xaphiosis Xaphiosis left a comment

Choose a reason for hiding this comment

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

Looks good!

@lsf37 lsf37 merged commit 023eee3 into master Feb 19, 2025
14 checks passed
@lsf37 lsf37 deleted the ioports branch February 19, 2025 00:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Xaphiosis Xaphiosis Xaphiosis approved these changes

Assignees

@lsf37 lsf37

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
@lsf37 @Xaphiosis