The C code has an unnecessary name indirection via isValidNativeRoot
here, which I replicated to make more obvious what maps to what.
Eventually this should disappear.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This is a bit speculative since the C is not there yet, but I think
it's a good candidate, esp turning the VMPageSize parameters into Int,
because that will save the C from converting it back and forth.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Uses lookupFrame which still needs to be filled in. We already have
a form of that in the formalisation, and can maybe reuse some of that.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This adds first AArch64-specific flushing. More to come when we add
the explicit flush API.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This refactors getASIDPoolEntry to extract code that is shared between
lookup and update, and should make conversion to reader monad later
easier.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
We are on an Arm board, where <= maxIRQ implies != irqInvalid, so use
original ARM version.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This adjusts ptBitsLeft and ptIndex to properly take into account
the potentially different-sized top-level table. This is all that is
needed for the rest of the lookup code to be correct.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This is a sketch of what I think the API will look like after C code
changes. In particular, this adds a VSpaceRoot API object type
that stands for a top-level page table. The name may change, but a
different API object type for the different page size will probably
stay.
Different top-level table size only applies in some configurations. The
spec attempts to model both cases by making ptBits and
ptTranslationBits dependent on whether it is a top-level table or not.
The rest follows from that.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Validated constants defined in Structures/AARCH64.lhs
PT caps now include a flag whether they are for a top-level table or
not. This could later be generalised to a level, but that's likely not
necessary for AArch64.
Amazingly, only the creation of new PT caps was affected by this
change. That creation will need user-level input which size of table to
create (to be added later).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Previously renamed invocation labels, as well as decodeARMMMUInvocation
and performARMMMUInvocation.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Largely adapted from ARM_HYP, modified and checked against C code.
Remaining known issues marked with FIXMEs.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The repo token allows the action to work on a private repo, and
the S3 cache bucket name allows it to charge a different org.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Model AARCH64-specific global kernel data, which means:
- adjust vspace region mapping names
- remove global page tables, including accesses (copyGlobalMappings)
- add pointer to empty user page table
This commit does not yet include VCPU and SMMU.
As on 32-bit ARM_HYP, global page tables exist on AARCH64, but are not
accessed by any code after boot, so are not visible in verified code
apart from defining the (constant) kernel window and kernel mappings
during execution. User code without a valid VSpace root is assigned a
pointer to an empty table.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Set the naming convention for global state components to armKS..
This overlaps with ARM and ARM_HYP, but so do the concepts as well
as the C convention.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit adds hardware ASID handling from ARM/ARM_HYP, and tweaks it
to use local ASID pool entries for hardware ASIDs instead of a global
ASID map.
Naming here is unfortunate in multiple dimensions:
- C calls the entries asid_map (from the global function in Haskell)
- what is actually mapped is a seL4 ASID to a HW ASID + VSpace root,
but only via multiple functions, the type is not a map
- the HW ASIDS are not actual ASIDs, but instead VMIDs in AArch64 EL-2
To be cleaned up when nomenclature is clearer in C.
Validation against C is minimal at the moment; only the types are
validated to correspond with C, and which functions are present, but
not their full behaviour/structure yet.
Signed-off-by: Gerwin Klein <gerwin.klein@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>
Adds FPU state to UserContext, uses 64 general-purpose registers as seen
on TX2.
Abstracts FPU operations to fpuThreadDelete required for thread
deletion, thereby not including intricacies of lazy FPU switching.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This adds the AARCH64 L4V_ARCH and adds a long initial test exclusion
list that will be reduced as verification proceeds.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit will only come into full effect when it is merged into
master, which is also the time AARCH64 tests should run regularly
in the main repository.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This is a separate workflow instead of being added to `proof.yml` so
that it can be switched on/off separately.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Use RISCV64 version of Haskell spec as a basis for upcoming work on
spec for AARCH64 architecture.
Only minimal RISCV64 to AARCH64 substitution done to yield a compiling
target, with a big FIXME stuck on top to remind people this got no human
oversight.
Signed-off-by: Rafal Kolanski <rafal.kolanski@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>
This adds a small script that parses two run_tests logs for session
times and compares them.
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>
The previous version of the `binary` workflow assumed that its input
artifacts would be available for download before a `binary` workflow run
is started. However, the `binary` workflow typically wants to download
those artifacts from the same workflow run that triggered the `binary`
run via `repository_dispatch`.
It appears that GitHub Actions does not make artifacts available for
download from a workflow until *after* the relevant job has finished.
Hence, there's a race between the `binary` workflow and the workflow
that triggered it. We resolve this by making the `binary` workflow retry
its artifact download for up to 10 minutes.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
The previous version was erroneously downloading artifacts from the repo
in which the `binary` workflow was triggered, when it should have been
downloading from the repo identified by the payload of the trigger.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
ci-actions/aws-proofs no longer excludes the AutoCorresSEL4 session by
default, so we no longer need to provide a fake argument to the session
parameter to not exclude it.
This is significant, because we now want the default to be non-verbose
since we're running multiple sessions in parallel.
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>
Gerwin Klein
Rafal Kolanski
Corey Lewis
Matthew Brecknell