- add ghost state corresponding to gsPTTypes in Haskell and ASpec
- add ghost type comments
- style update for old definitions since we need to touch most of these
- define vs/pt_array_len for use in C annotations
- make NormalPT_T/VSRootPT_T names available for use in C annotations
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Setting the environment variable INPUT_NUM_DOMAINS will cause the
build to override the KernelNumDomains setting in the config file with
the provided setting.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
PR seL4/seL4#1105 moves config generation back to configure time.
This means we can revert eaf735c38f.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Correctly check the type of the table the PageTableCap points to in
checkVSpaceRoot (must be a VSRootPT, not NormalPT).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The argument numbers in the error messages for
decodeARMFrameInvocationMap are slightly off.
Same bug exists in C, see also seL4/seL4#1075.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The user_vtop check in decode_fr_inv_map_wf can be relaxed from >= to >
as done in Haskell and C.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Tweak formulation of createNewCaps for page tables to be in the expected
"addr ~elem~ map .." form. The previous definition was not wrong, but
the lemmas in Retype_R expect the set membership form.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Refine needs slightly stricter information about asid maps, in
particular we need to know explicitly that asid 0 never maps to
a VSpace. This is the reverse of valid_vmid_table, but unfortunately
does not fully follow from valid_vmid_table, because there can
be VSpaces mapped without an assigned VMID.
We shift the test for 0 < asid from entry_for_asid to vspace_for_asid
so we can use entry_for_asid in the formulation of the invariant.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
AArch64 C code changes now designate PageDirectoryObj as the VSpace
object type, which comes first in the enum.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This adds sch_act_target/schActTarget accessor names for the
switch_thread/SwitchToThread constructor of the scheduler_action
datatype at the aspec and Haskell level, respectively
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
CI is introducing an `L4V_PLAT` variable to support proof runs across
more platform configurations. This commit incorporates `L4V_PLAT` into
the paths generated by `export-kernel-builds.py`, to ensure that
exported builds can be disambiguated.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
L4V_PLAT selects a platform variation within a L4V_ARCH. This mostly
affects which seL4 cmake config file is loaded when building config
data and the kernel C code. This in turn affects (and will rebuild)
ASpec, ExecSpec, and CSpec.
Examples:
L4V_ARCH=ARM L4V_FEATURES="" L4V_PLAT=""
will load `ARM_verified.cmake`
L4V_ARCH=ARM L4V_FEATURES="" L4V_PLAT=imx8mm
will load `ARM_imx8mm_verified.cmake`, and
L4V_ARCH=ARM L4V_FEATURES=MCS L4V_PLAT=imx8mm
will load `ARM_MCS_imx8mm_verified.cmake`
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Provide L4V_ARCH targets in the Haskell Makefile and constrain
run_tests to use only the current L4V_ARCH, to avoid building all
architectures in all tests.
A manual invocation of just `make` will still build all architectures
for easier checking.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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>
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>
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>
`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>
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>
The condition `pptrBase < kernelELFBase` is not required on AArch64 in
hyp mode and was left over from the initial RISC-V setup.
Since this check does fail for some platforms (where physBase = 0 and
consequently pptrBase = kernelELFBase) we remove it here.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Avoid mixing `isabelle`, `make`, and `run_tests` invocations.
Standardise on `run_tests` and mention `L4V_ARCH` each time to
indicate that you can and should set `L4V_ARCH`.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Move physBase into Arch_Kernel_Config_Lemmas, and move basic lemmas
about kernel constants that do not directly unfold physBase into
ArchInvariants_AI.
Because Arch_Kernel_Config_Lemmas does not have all names available
yet, some of the lemmas are folded and shadowed later in
ArchInvariants_AI.
Also refactor translate_address_kernel_elf_window to have two helper
lemmas that can be used in infoflow.
Co-authored-by: Corey Lewis <corey.lewis@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- adjust the example init state such that it does not constrain the
value of physBase and kernelELFBase too much. We assume 4M physical
memory and 4k of kernel ELF memory. We need 4M for the infoflow
example, because it requires a 2M RISCVLargePage plus additional
kernel objects.
- make the PagePTE for kernelELFBase point to kernelELFPAddrBase so
that the mapping stays consistent when physBase changes.
- introduce shorthand constants for the index in the page table that
is responsible for kernelELFBase, and for the number of bits left
to translate from the top-level page table (= size of the pages in
that table).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Factor out pptrTop from the definition in kernelELFBase and define it
as a constant as on other platforms. Shadows the equivalent definition
in Haskell.
Also remove incorrect comment -- the term was not PADDR_TOP, but
PPTR_TOP in C.
Co-authored-by: Corey Lewis <corey.lewis@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Remove the only unfolding of Kernel_Config.physBase_def in
ArchKernelInit by removing an unused lemma. Move the remaining
unfolding in ArchAInvariants to Kernel_Config_Lemmas.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
While having a single Kernel_Config_Lemmas was fine for constraining the
number of domains, it does not work for constraining architecture-specific
configuration options/values.
Add an (empty for now) Arch_Kernel_Config_Lemmas theory to every architecture
that imports the generic Kernel_Config_Lemmas. Change all imports of
Kernel_Config_Lemmas to import Arch_Kernel_Config_Lemmas instead.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Make the C kernel config extraction visible as a separate test session
in run_tests so that run_tests can do concurrency control for it.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
physBase is now a generated definition on all arches except X64, with
the expectation that this value can change (for static multikernel systems).
All definitions that depend on physBase in C must therefore adapt to
depend on the physBase constant instead of its unfolded value.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
* getHSR confirmed unusued
* setHCR confirmed used on C side for hyp
* addressTranslateS1 was merged into C
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
* explain how canonical_bit concept applies to AArch64
* use powers of 2 for kernelELFBase
* pptrBase unlikely to migrate to 0 in near future
* pptrUserTop_def' is not used on AARCH64, and should not be used as we
try to avoid expanding config_ARM_PA_SIZE_BITS_40 whenever possible
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The `export-kernel-builds.py` script expects to be able to run the
build from an arbitrary temporary directory.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Achim D. Brucker
Gerwin Klein
Rafal Kolanski
Corey Lewis
Michael McInerney
Matthew Brecknell