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>
globally (for all arches) removes word simp rules that are too eager
for 64 bit bitfield proofs.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Isabelle2021-1 simplifies `a << Suc 0` too eagerly, so we add simp
rules to compensate for new forms of goals. Removing the too-eager simp
rules would be less stable against theory merge.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Gerwin Klein
Rafal Kolanski
Corey Lewis
Matthew Brecknell