arch-split Refine up to Invariants_H for ARM+ARM_HYP #847
+3,302
−8,296
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sets up ARM for Invariants_H arch-splitting using AARCH64 as a template. Includes removal of ARM Invariants_H. Signed-off-by: Rafal Kolanski <[email protected]>
Updates the rest of ARM Refine+Orphanage 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 - valid_pde_mappings' moved to valid_arch_state', resulting in valid_arch_state' lifting lemmas to have poor generic applicability (likely future interface lemmas will be based around preserving valid_arch_state') - 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]>
…dates_H Most of the changes were ported from X64 (which were adapted from AARCH64). Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
added
the
arch-split
Sets up ARM_HYP for Invariants_H arch-splitting using AARCH64 as a template. Includes removal of ARM_HYP Invariants_H. Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
changed the title
Updates the rest of ARM_HYP 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 - valid_pde_mappings' moved to valid_arch_state', resulting in valid_arch_state' lifting lemmas to have poor generic applicability (likely future interface lemmas will be based around preserving valid_arch_state') - 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]>
Most of the changes were ported from ARM (which were adapted from AARCH64). Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis
force-pushed
the
arch-split_arm
branch
from
3e1c0fb to
d33a5bf
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
As seen with X64 (#842), you'll have to review this commit-by-commit. Fortunately there didn't need to be any interface changes this time, so we only have three commits. Copying from AARCH64 (nothing interesting there), updating the definitions/lemmas for Refine, and then fixing up anything else. This seems like a good approach, and keeping the copy commit separate is turning out to be a good idea for large changes like these.
Then I did the same thing again for ARM_HYP, adapting changes from ARM. Ran out of time for RISCV64 though.
I'm not entirely clear whether I should be saying "Up to Invariants_H" or "Up to InvariantUpdates_H". Currently going with the latter.
observations from this pass:
OR adding tcb_cte_cases_neqs to simpset (for future)
PDEs on ARM; to do a proper lifting lemma we have to say preservation of all
arch objects instead of PDEs
gen_objBits_simps because I wasn't consistent/observant enough to notice early