This means Isabelle will automatically insert `level_type` when it
finds a term of type `vm_level` but expects one of type `pt_type`.
This only works when the context is unambiguous, but it does make quite
a few terms shorter.
This is input-only, `level_type` will still show up in output.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Replaces bool with a dedicated type for page table types. This should
generalise nicely to more different levels and removes the slightly
confusing occurrence of bool.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This replaces 'a word for indices with machine_word. Since we can't use
a specific word length for a generic table index (because different
tables can have different index types), we don't win much by using 'a
word, but we do lose something: we must instantiate 'a when we use the
term, which means we need to decide at that point which type of table
we are talking about. This forces early case distinctions in proofs.
Using machine_word allows us to delay committing to a particular table
type and instead write a generic condition on the width of the index.
We are using machine_word instead of nat or a different specific word
length, because the index into the table is a slice of either an
obj_ref (in ptes_of) or a vref (when we do page table walks), both of
which are compatible with machine_word.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
With separate pte levels the proofs become simpler and shorter, but
some of the statements longer.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Some properties that crunch can be used for have different legacy naming
schemes. This commit makes it possible for different instances of crunch
to be configured for either prefix or suffix naming.
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
It is possible to do this with one line now that crunch does not produce
duplicate attribute warnings.
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Several parts of CRefine did not or should not depend on anything
C-related, but the import hierarchy (and theory content) did not reflect
this. Namely:
* Move_C and ArchMove_C were intended to hold items that could be moved
to Refine yet used `kernel_m` locale and imported the C spec.
* IsolatedThreadAction indicates how to rearrange statements in the
design spec and has nothing to do with the C spec or framework.
* Fastpath_C contained the design spec of the fastpath, the design spec
rewrite proofs, and the C refinement. Having to rebuild nearly all of
CRefine to work on rewrite proofs wasted time.
In the new import hierarchy:
* Move_C imports only Refine; ArchMove_C builds on Move_C
* IsolatedThreadAction imports only ArchMove_C
* The fastpath proofs are split into the spec definition (Fastpath_Defs)
and rewrite proofs (Fastpath_Equiv), which don't depend on anything
C-related, with their C refinement remaining in Fastpath_C.
While it is possible to separate out the fastpath definitions and rewire
proofs into a separate image or even move them to Refine, development
experience indicates keeping them alongside their C refinement remains
more convenient for the proof engineer involved.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
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>
- 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>
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>
- 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>
findVSpaceForASIDAssert is needed for modeling the hardware ASID lookup
on ARM. None of AARCH64, RISCV64, X64 use that mechanism and the
function is unused. There are some proof about it, but those are unused
as well. This commit removes all of these.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Three main thrusts:
- speed up the `updateMDB_the_lot` chain by using more targeted
proof methods
- drastically reduce goal size by removing unused assumptions when
that becomes possible (this is the largest overall speed win)
- use `subgoal` to unblock interactive proof progress
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Both AInvs and the refinement chain need the generated files necessary
for ASpec and ExecSpec. We could depend on ASpec directly, but that
would mess with Isabelle being able to schedule sessions as it wants
them.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add a bundle for global word simp set changes -- unfortunately we
can't actually do this globally, because they are mostly simp rule
removals which will be overwritten by theory merges. So this new
l4v_word_lib bundle will have to be activated/unbundled multiple times.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This invariant states that the current active vcpu is
equal to the vcpu of the current thread
Signed-off-by: Michael McInerney <m.mcinerney@unsw.edu.au>
This includes replacing previous ASpec names for such constants with
the names used in Haskell/ExecSpec to avoid duplication. This also
makes some of the proofs slightly more generic.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The InfoFlow proof itself does not care about the number of domains, and
that assumption was removed in another commit.
The specific example in the information flow refinement requires two
domains (one "high" and one "low") to be of any interest. Since it
cannot be instantiated with only one domain, the example theorems in
Example_Valid_StateH now assume that `1 <= maxDomain`.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
For CRefine, this process is much more complex than for Refine and up,
as the C code both has its own definitions `maxDom` and `numDomains`,
but they are not defined in terms of each other, only numbers.
Similarly, array size types and their corresponding ArrayGuard bounds
checks refer to specific numbers, making a fullproof abstraction impossible.
A reasonably constrained interface to numDomains/maxDomain/maxDom in
Wellformed_C provides a sufficient abstraction to allow the proofs to be
independent of the number of domains (constrained to <= 256). Using the
value_type command allows more abstraction techniques, such as linking
the size of the scheduler queues back to numDomains*numPriorities,
without stating what the numbers are. Finally, for getting past the
ArrayGuard bounds checks, we do leak some information in the form of
`explicit` lemmas. These are the least safe, but short of augmenting the
C parser to re-wrap array sizes into equivalent constants/types, they
constitute a limited risk. Nonetheless, `explicit` lemmas should be used
as sparingly as possible.
Refinement to C proceeds by pretending we don't know the number of
domains, and whenever a control flow decision is made based on
`numDomains > 1`, we follow both branches, as we did for Refine. We also
attempt to avoid clever rewrites such as `(x < 1) = (x = 0)` which mess
up bounds checks into a domain-size array when `numDomains = 1`.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Proofs now don't care about numDomains, except for a small interface in
Invariants_H. The interface is currently by convention only, and has no
enforcement capabilities.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The proofs work without knowing the number of domains, including with
only a single domain.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Make proofs work with any number of domains that fits in the domain type
(at this time an 8-bit word).
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The aim of the PR was readability, but it actually also brings the
C more in line with the spec.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The PR seL4/seL4#473 removes Arch_finaliseInterrupt; this commit
updates the C proofs accordingly.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Gerwin Klein
Corey Lewis
Rafal Kolanski
Corey Lewis
Michael McInerney
Ryan Barry
Gerwin Klein
Gerwin Klein
Florian Haftmann