Commit Graph

5239 Commits

Author SHA1 Message Date
Rafal Kolanski 7cdd203136
aarch64 refine: first run through Orphanage
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:49 +10:00
Rafal Kolanski 496f70f7a6
run_tests: fix QUICK_AND_DIRTY handling
os.environ expects a string, not an integer

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:49 +10:00
Rafal Kolanski 7b73a18757
run_tests: enable Refine (quick_and_dirty) for AARCH64
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:49 +10:00
Rafal Kolanski 2f3e333500
aarch64 refine: first pass through EmptyFail_H (sorry-free)
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:48 +10:00
Rafal Kolanski 81d382ec71
aarch64 refine: first pass through Refine (sorry-free)
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:48 +10:00
Rafal Kolanski 7154cc9d31
aarch64 refine: remove final mention of vs_valid_duplicates'
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:48 +10:00
Rafal Kolanski c4dee689b0
aarch64: update Init_R+PageTableDuplicates for PT ghost state
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:48 +10:00
Gerwin Klein 9298456475
refine: update other architectures for ghost state change
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:48 +10:00
Gerwin Klein aa2eb9ad6d
design: fix ExecSpec for other architectures
Include the new ArchPSpace_H file, which on the other (non-AArch64)
architectures will only contain an empty placeholder function.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:48 +10:00
Gerwin Klein d24d2f8397
aarch64 refine: first pass through ADT_H
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:47 +10:00
Gerwin Klein 064d102047
aarch64 ainvs+refine: proof updates for PT type ghost state
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:47 +10:00
Gerwin Klein e0ae44a577
aarch64 haskell+design: record PT types in ghost state
For making the state relation functional in refine/ADH_H we need to
know to which type of page table each PTE belongs. Record this
information in ghost state, similar to what we do for CNode size and
user page size.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:47 +10:00
Gerwin Klein a4f944d094
aarch64 refine: copy PageTableDuplicates from RISCV64
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:47 +10:00
Rafal Kolanski c58c007f94
aarch64 refine: copy KernelInit_R from RISCV64
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:47 +10:00
Rafal Kolanski 72dfb53e91
aarch64 refine: copy IncKernelLemmas+InitLemmas from RISCV64
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:46 +10:00
Rafal Kolanski ee346ba108
aarch64 refine: first pass though Init_R
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:46 +10:00
Gerwin Klein 59d303b020
aarch64 refine: first pass through Syscall_R
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:46 +10:00
Rafal Kolanski 226c2f6a95
aarch64 refine: first pass through Arch_R
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:46 +10:00
Rafal Kolanski 7ed847638d
aarch64 haskell: update decodeARMASIDPoolInvocation
Check for mapping was incorrect (attempted to check the ASID cap for
ptIsMapped) and it turns out not necessary.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:45 +10:00
Rafal Kolanski 7cea1dc893
aarch64 aspec: attribs_from_word used wrong bits
bit 0 set = cachable = NOT Device
bit 2 set = execute never = NOT execute

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:45 +10:00
Gerwin Klein 8de14306d4
aarch64 refine: first pass through Tcb_R
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:45 +10:00
Rafal Kolanski 20fad5b9fc
aarch64 refine: update vmattributes_map for devices
Page is cachable if not a device.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:45 +10:00
Gerwin Klein a88bf412a5
aarch64 refine: remove 1 sorry
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:45 +10:00
Gerwin Klein f3bbd47537
aarch64 haskell: prefer fail over error
`error` is mapped to `undefined` which does not work well with `crunch`.
`fail` is mapped to monadic `fail` in Isabelle, works fine with crunch
and we have to prove that it's not called in `corres`.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:45 +10:00
Gerwin Klein 4834c2589a
aarch64 refine: first pass through CNodeInv_R
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:44 +10:00
Gerwin Klein 835d82c253
aarch64 refine: first pass through Interrupt_R
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:44 +10:00
Gerwin Klein 865facfde9
aarch64 refine: first pass through Ipc_R
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:44 +10:00
Rafal Kolanski 4dfb6f8ad3
aarch64 refine: first pass through Finalise_R
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:44 +10:00
Gerwin Klein be22c7bfcc
aarch64 refine: set up Untyped_R from RISCV64, add hyp/vcpu
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:44 +10:00
Gerwin Klein 0a7eaece00
aarch64 refine: copy over Invocations_R from RISCV64
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:44 +10:00
Gerwin Klein f4c12a6d85
aarch64 refine: remove kernel_mappings in Retype/Detype
These do not exist on AARCH64

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:43 +10:00
Gerwin Klein 5601abc530
aarch64 refine: fill in VSpaceObject cases in Retype_R
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:43 +10:00
Rafal Kolanski a4536a17ce
aarch64 refine: first pass through Detype_R
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:43 +10:00
Rafal Kolanski e508693534
aarch64 refine: first pass through Retype_R
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:43 +10:00
Rafal Kolanski 3a77d097c4
aarch64 refine: first pass through IpcCancel_R
needed some changes to Schedule_R and VSpace_R

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:43 +10:00
Rafal Kolanski 044a97ed1a
aarch64 refine: first run through Schedule_R
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:42 +10:00
Rafal Kolanski 904056868d
aarch64 refine: add state_hyp_refs_of' to valid_state'
Somehow we missed this on the first pass. Adjusted existing proofs.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:42 +10:00
Rafal Kolanski a79e06f419
aarch64 refine: first run through VSpace_R
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>
2023-05-26 18:04:42 +10:00
Gerwin Klein 0f11a7a52a
aarch64 refine: progress in ArchAcc
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:42 +10:00
Rafal Kolanski 97ebd07298
aarch64 refine: start on VSpace_R
Up to and including handleVMFault_corres which needed a major overhaul.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:42 +10:00
Rafal Kolanski 059afc8743
aarch64 refine: add InterruptAcc_R
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:41 +10:00
Rafal Kolanski cb03631312
aarch64 refine: add TcbAcc_R and ArchMove_R
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:41 +10:00
Rafal Kolanski 2b543da5f3
aarch64 refine: add CSpace_R
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:41 +10:00
Rafal Kolanski 18d76ef54b
aarch64 refine: add vcpuBits_def to objBits_defs
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>
2023-05-26 18:04:41 +10:00
Rafal Kolanski a93a62641d
aarch64 refine: copy RAB_FN from RISCV64
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:41 +10:00
Rafal Kolanski e0114eef06
aarch64 refine: add CSpace_I and CSpace1_R
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:41 +10:00
Gerwin Klein 3b5a983362
aarch64 refine: first pass through ArchAcc_R
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:40 +10:00
Gerwin Klein b42665460d
aarch64 refine: use ptTranslationBits for indices
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:18 +10:00
Gerwin Klein 38a65fd453
aarch64 refine: adjust KHeap_R from RISCV64
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>
2023-05-25 19:34:17 +10:00
Gerwin Klein b882216086
aarch64 refine: copy Machine_R from RISCV64
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:17 +10:00