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

MCS: merge master into rt #680

Merged
merged 207 commits into from
Oct 13, 2023
Merged

MCS: merge master into rt #680

merged 207 commits into from
Oct 13, 2023

Conversation

corlewis
Copy link
Member

This includes the update to Isabelle2023. As usual with merges, the last commit is probably the only one that it makes sense to review.

lsf37 and others added 30 commits May 3, 2023 14:23
@lsf37
github: add manual triggers for testing
2545aa0 
The worklow_dispatch trigger adds a button in the GitHub UI that lets
one trigger the workflow manually. Useful for testing the workflows.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@Xaphiosis
docs: style: right- vs left-wrapping of operators
59bf9d9 
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@Xaphiosis @lsf37
run_tests: enable BaseRefine for AARCH64
0794e0a 
Switch exclusion to Refine.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@Xaphiosis @lsf37
aarch64 refine: first attempt at Invariants_H
1483554 
Quite a few issues remain, notably validity of ASID maps and
relationship to ASID table is missing from valid_arch_state'

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@Xaphiosis @lsf37
aarch64 refine: copy InvariantUpdates_H from RISCV64
01575f2 
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@Xaphiosis @lsf37
aarch64 refine: add StateRelation
1404b9c 
Only text replacement of RISCV64->AARCH64 for now.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@lsf37
aarch64 ainvs: fix typo
96851e8 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
aarch64 refine: copy LevityCatch from RISCV64
44fc3ec 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
aarch64 refine: iteration on Invariants_H
0b0b3b3 
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.system>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
aarch64 aspec: sync vmid bit width with Haskell+C
394f74b 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
aarch64 haskell: use ppn concept for PageTablePTEs
9f25a4e 
Don't store the bottom 12 bits of the base address for page table PTEs,
because we know they are zero. This gives us implicit alignment to
pageBits in the page table walker.

The C code stores only 36 significant bits, whereas this commit still
uses a full 64-bit machine word for the ppn in Haskell. To be adjusted
in a future change.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37 @Xaphiosis
aarch64 refine: complete StateRelation
55a01f1 
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
aarch64 refine: copy Corres.thy from RISCV64
61bce83 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37 @Xaphiosis
aarch64 refine: adjust Bits_R from RISCV64
bf3929b 
Add VCPU/hyp material from ARM_HYP, fix up broken lemmas.

Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
aarch64 refine: copy EmptyFail from RISCV64
7cdb85f 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
aarch64 refine: copy SubMonad_R from RISCV64
555bff6 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
aarch64 refine: copy Machine_R from RISCV64
b882216 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37 @Xaphiosis
aarch64 refine: adjust KHeap_R from RISCV64
38a65fd 
Add VCPU/hyp lemmas from ARM_HYP, fix and update failing lemmas. Leave
1 sorry on pspace_canonical, which might not be needed for AARCH64.

Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37 @Xaphiosis
aarch64 refine: use ptTranslationBits for indices
b426654 
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37 @Xaphiosis
aarch64 refine: first pass through ArchAcc_R
3b5a983 
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@Xaphiosis @lsf37
aarch64 refine: add CSpace_I and CSpace1_R
e0114ee 
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@Xaphiosis @lsf37
aarch64 refine: copy RAB_FN from RISCV64
a93a626 
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@Xaphiosis @lsf37
aarch64 refine: add vcpuBits_def to objBits_defs
18d76ef 
The way we handle vcpuBits on AARCH64 is different to ARM_HYP.
This seems the most logical place to put vcpuBits_def to aid automation.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@Xaphiosis @lsf37
aarch64 refine: add CSpace_R
2b543da 
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@Xaphiosis @lsf37
aarch64 refine: add TcbAcc_R and ArchMove_R
cb03631 
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@Xaphiosis @lsf37
aarch64 refine: add InterruptAcc_R
059afc8 
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@Xaphiosis @lsf37
aarch64 refine: start on VSpace_R
97ebd07 
Up to and including handleVMFault_corres which needed a major overhaul.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@lsf37 @Xaphiosis
aarch64 refine: progress in ArchAcc
0f11a7a 
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@Xaphiosis @lsf37
aarch64 refine: first run through VSpace_R
a79e06f 
This required a lot of adaptation from ARM_HYP, rearranging, and fixing.
The VCPU lemmas are mostly now constrained to one area, making it
theoretically possible to make a VCPU theory in the future.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@Xaphiosis @lsf37
aarch64 refine: add state_hyp_refs_of' to valid_state'
9040568 
Somehow we missed this on the first pass. Adjusted existing proofs.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
corlewis and others added 21 commits October 5, 2023 22:00
@corlewis
lib/monads: improve style of nondet and trace
3333395 
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
@corlewis
lib/monads/nondet: remove uses of _tac methods
34038fc 
In particular, try to remove as many as possible _tac methods that refer
to system-generated variable names. Any remaining uses are explicitly
protected by a rename_tac.

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
@michaelmcinerney
lib/monads: add no_fail_ex_lift and no_fail_grab_asm
6680297 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: improve corres_underlying rules for whileLoop
e7cca6a 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@lsf37
lib: sync Word_Lib with AFP
6721c7a 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
lib/Eisbach_Tools: morphism type changed in Isabelle2023
3f66cb0 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
lib: Isabelle2023 update
eeae2af 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@Xaphiosis @lsf37
misc: goto-error jEdit macro: update for 2023
286278d 
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
@lsf37
aspec: mapsto syntax update for Isabelle2023
450234e 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
c-parser: sync Simpl from AFP for Isabelle2023
83fc513 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
c-parser: update to Isabelle2023 maps-to syntax
be44fad 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
c-parser: adapt standalone parser to Isabelle2023
26807f7 
The code draws in table.ML from the Isabelle source, which changed
in the 2023 release. This commit adds further library functions from
Isabelle library.ML and extracts the parts of unsynchronized.ML that
work with mlton.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
clib: update to Isabelle2023 mapsto syntax
f88d2d4 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
proof: update to Isabelle2023 mapsto syntax
3141584 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
sep-capDL: update to Isabelle2023 mapsto syntax
f7768ee 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
capdDL-api: update to Isabelle2023 mapsto syntax
4c0b3df 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
autocorres: update to Isabelle2023
0f99a75 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
camkes: update to Isabelle2023 mapsto syntax
0d984f3 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37
word lib: fix broken style introduced from AFP
ad24d95 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@corlewis
Merge branch 'master' into rt
3036f22 
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
@corlewis
rt proof: update for merge
3308a0b 
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
@corlewis corlewis added the MCS related to `rt` branch and mixed-criticality systems label Oct 12, 2023
@corlewis corlewis self-assigned this Oct 12, 2023
lsf37
lsf37 approved these changes Oct 12, 2023
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.

Good work. There's a whole lot more mapsto and corresKsimp going on in rt than I thought.

Since the test is still set to Isabelle2022 we should probably do a PR on mcs.xml in the manifest repo first and the re-run the tests here to double-check before we merge.

michaelmcinerney
michaelmcinerney approved these changes Oct 12, 2023
View reviewed changes
Copy link
Contributor

@michaelmcinerney michaelmcinerney 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!

Yeah that is a lot of corresKsimp, almost all mine, I think. It would be interesting to go through and see how quickly they could be replaces with the new corres method.

corlewis
corlewis commented Oct 12, 2023
View reviewed changes
proof/invariant-abstract/CSpace_AI.thy
apply (rule alternative_valid; (solves wpsimp)?)
apply (rule alternative_wp[where P=P and P'=P for P, simplified]; (solves wpsimp)?)
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 forgot to point this out when I made this PR. alternative_valid was removed on master due to not being used, but did have a couple of uses in rt as part of some forward reasoning proofs.

Are we ok with what I've done here, which is basically inlining it in the two places it was used? The obvious to me other options would be to either add alternative_valid back to Nondet_VCG, or to rework these proofs to be backwards.

Copy link
Contributor

Choose a reason for hiding this comment

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

I'd be OK with what you've done here, but wouldn't mind if these proofs were reworked to be backwards. I'm pretty sure they'd be my proofs originally, so I'd be happy to do that. I think these were for preemption_point, which is not the nicest function to deal with, so it might not be so straightforward.

Copy link
Member

Choose a reason for hiding this comment

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

I'd be fine with either. Definitely no problems with it being reworked as backwards proof. Could also be in a separate PR.

@corlewis corlewis merged commit 3308a0b into seL4:rt Oct 13, 2023
9 of 10 checks passed
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

@michaelmcinerney michaelmcinerney michaelmcinerney approved these changes

@Xaphiosis Xaphiosis Awaiting requested review from Xaphiosis

Assignees

@corlewis corlewis

Labels
MCS related to `rt` branch and mixed-criticality systems
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@corlewis @lsf37 @michaelmcinerney @Xaphiosis @mbrcknl