- opt_pred takes a predicate P and an option value x and
returns P y if x = Some y and False if x = None
- infix notation (|<), which lets us write in the style of
P |< projections
Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
- ogets and asks are equivalent
- make ogets a full abrreviation of asks
- provide the original definition of ogets as ogets_def
Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
Put all lemmas for vm_level from the bit1/bit0 classes into one place
so we can later assign these automatically.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Making vs_index_len a sybmolic value instead of a plain number means we
have to unfold config_ARM_PA_SIZE_BITS_40 less often (instead, we need
to consider both cases, which forces us to stay generic).
This also makes sure the type vs_index_len is always distinct from
pt_index_len (even if the sizes are the same), which was only
guaranteed in one of the two configurations before.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The previous proof inadvertently relied on the fact that
config_ARM_PA_SIZE_BITS_40 is not configured and solved the lemma
trivially instead of really proving that case.
This is only relevant for the config_ARM_PA_SIZE_BITS_40 configuration,
which is not the current verification target, but it is nicer to stay
generic in config_ARM_PA_SIZE_BITS_40 as far as we can.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This means that the invariants are strong enough to support all of the
basic properties of page table walks and vspace address arithmetic.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
In some AArch64 configurations, some slots in the top-level table are
not accessible, because the IPA space size is smaller than the number
of bits the page tables can translate. invalid_mapping_slots indicates
which slots have to remain set to InvalidPTE in those tables.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The bit width of intermediate physical addresses (IPA) is occasionally
useful in the invariants later.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- update lemma statements to include pspace_distinct where needed,
and adjust for multiple PT sizes.
- update most proofs accordingly, leave the rest sorried.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- introduce max_page_level to express that PagePTEs can only occur
on levels 0-2 (regardless of PA/IPA space size)
- PageTablePTEs must always point to normal tables (can't point back
to the top)
- PageTables at max_pt_level must be VSRootPTs
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Make the function usable not only in the code+specs, but also in the
invariants by adding a case for asid_pool_level (= max_pt_level + 1).
At this level, we also need to translate the bits of the top-level
table.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This is a bit more complex than before. The general approach is to do
lemmas per level first, then combine them in the map union of pte_of.
For ptes_of_Some, with pspace_distinct, we get the expected two cases.
Without pspace_distinct we need in the second case a condition that the
first case doesn't apply (they are only mutually exclusive when
pspace_distinct holds).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This makes sure we're accessing the right kind of object for the level
we are interested in. Relying on alignment is Ok when the invariants
are in scope, but this check is more immediate and avoids us needing
pspace_aligned and pspace_distinct in all lemmas.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- void type is not used in AArch64
- remove duplication of level_of_vmsize
- state equivalence lemma
- unified formulation of valid_vspace_obj turned out to be usable so far
- confirmed that no further vmid properties are needed (in addition to
inverse)
- removed alternative version of arch_valid_obj (but remains in history)
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Since user addresses are intermediate physical addresses in hyp mode,
the concept of canonical_user is different to other architectures.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
At this stage ArchInvariants_AI should process cleanly, but is still
missing some interface lemmas for Invariants_AI.
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This is a first draft of what we think needs to change in the
invariants to model AArch64. VCPU-related definitions are still
missing, and further tweaks are likely.
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Copied from RISCV64 with minimal search/replace, added FIXMEs.
Should be enough for formulating architecture-specific invariants.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Give more time for downloading and compiling dependencies for runs
where these are not cached.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This makes sure we're catching all dependencies that are declared for
`design-spec` in the top-level Makefile. In particular, we want
`c-config` to run at least once before either `ASpec` or `ExecSpec` run
it, to make sure these two are not racing on config generation in
`-j 2`.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
We import some documentation with notes/issues on the refinement from
Haskell to C.
The file is a Markdown-ified version of previous documentation hosted at
UNSW.
Signed-off-by: Corey Lewis <corey.lewis@unsw.edu.au>
We had put a lot of VCPU content into ArchVSpace and ArchVSpaceAcc even
though VCPUs aren't really very related to VSpace. These functions now
live in a separate files VCPUAcc in analogy to VSpaceAcc and TcbAcc.
Some of these functions could also move into VCPU_A instead.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
As Corey points out, the rest of the fields are in perfect order with
Haskell, and keeping all of them fully in sync will save us shuffling
and looking up things later in the proofs.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- tune comment
- make vs_index_len the generic interface for vs_index_len_def
- provide relationship to ptTranslationBits
The two latter points will help to keep invariant proofs generic over
the size of the top-level table.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Config files should be re-generated when generator content changes,
because that generally changes the content of the output.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
On AArch64 pptrUserTop is not page aligned, which also suits us fine for
reusing the value later in AInvs.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Definitions in Platform.thy may depend on kernel config options, so
we need Kernel_Config_Lemmas there already, and need to replace the
dependency in Machine_Types to avoid a dependency circle.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>