The worklow_dispatch trigger adds a button in the GitHub UI that lets
one trigger the workflow manually. Useful for testing the workflows.

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Switch exclusion to Refine.

Signed-off-by: Rafal Kolanski <[email protected]>

Quite a few issues remain, notably validity of ASID maps and
relationship to ASID table is missing from valid_arch_state'

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Only text replacement of RISCV64->AARCH64 for now.

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Co-authored-by: Rafal Kolanski <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

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 <[email protected]>

Co-authored-by: Rafal Kolanski <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Add VCPU/hyp material from ARM_HYP, fix up broken lemmas.

Co-authored-by: Rafal Kolanski <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Add VCPU/hyp lemmas from ARM_HYP, fix and update failing lemmas. Leave
1 sorry on pspace_canonical, which might not be needed for AARCH64.

Co-authored-by: Rafal Kolanski <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>

Co-authored-by: Rafal Kolanski <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>

Co-authored-by: Rafal Kolanski <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

The way we handle vcpuBits on AARCH64 is different to ARM_HYP.
This seems the most logical place to put vcpuBits_def to aid automation.

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Up to and including handleVMFault_corres which needed a major overhaul.

Signed-off-by: Rafal Kolanski <[email protected]>

Co-authored-by: Rafal Kolanski <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>

This required a lot of adaptation from ARM_HYP, rearranging, and fixing.
The VCPU lemmas are mostly now constrained to one area, making it
theoretically possible to make a VCPU theory in the future.

Signed-off-by: Rafal Kolanski <[email protected]>

Somehow we missed this on the first pass. Adjusted existing proofs.

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

needed some changes to Schedule_R and VSpace_R

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

These do not exist on AARCH64

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

`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 <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Page is cachable if not a device.

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

bit 0 set = cachable = NOT Device
bit 2 set = execute never = NOT execute

Signed-off-by: Rafal Kolanski <[email protected]>

Check for mapping was incorrect (attempted to check the ASID cap for
ptIsMapped) and it turns out not necessary.

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

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 <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

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 <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

os.environ expects a string, not an integer

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Signed-off-by: Rafal Kolanski <[email protected]>

Piggybacking off of REFINE_QUICK_AND_DIRTY as they are usually linked.

Signed-off-by: Rafal Kolanski <[email protected]>

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 <[email protected]>

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 <[email protected]>

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 <[email protected]>

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 <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

The Orphanage session is no longer conditional on L4V_ARCH_IS_ARM
(instead it is empty for those architectures that don't support it).

Signed-off-by: Gerwin Klein <[email protected]>

REFINE_QUICK_AND_DIRTY is already set correctly in proofs/Makefile,
so doesn't need to be set here.

Signed-off-by: Gerwin Klein <[email protected]>

Currently both workflows have the name "Proofs" which is confusing
in the GitHub UI.

Signed-off-by: Gerwin Klein <[email protected]>

The action will abort when no clean rebase is possible, and force-push
the rebased branch when the rebase over origin/master was clean.

The push will trigger proof runs on the rebased branches.

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

- document the wpc_helper predicate and setup for wpc
  (but not the proof method internals at this point)

- add facilities for a second guard of predicate type

The current setup works well for judgements with one guard of type
predicate or set (valid, validE, etc), or with two guards where one is
a predicate and the other is a set (ccorres), but not for judgements
that have two predicate guards, i.e. plain corres. This commit adds a
second such guard, which can be ignored for the judgements that don't
need it in the same way that valid/validE currently ignore the set-type
guard.

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Factor out pre_tac such that we can have separate theorem sets and
methods for wp_pre, monadic_rewrite_pre, corres_pre, and potentially
others in the future.

Leave everything in wp_pre that we expect to use wp or wpsimp on, in
particular no_fail.

Signed-off-by: Gerwin Klein <[email protected]>

- rename corres_pre set in CRefine to ccorres_pre
- rename internal corres_pre method in Corres_Method to corres_pre'
- use corres_pre instead of old wp_pre in refine

Signed-off-by: Gerwin Klein <[email protected]>

Replace wp_pre with monadic_rewrite_pre in one manual proof instance.

Signed-off-by: Gerwin Klein <[email protected]>

While in many cases using an eta form with a bind (`f >>= (λrv. g rv)`)
does manage to preserve names, this was not true in general when working
with monadic_rewrite. An obvious case of this was when performing a
rewrite in the middle of a function, all bound variables on the way to
that point would get renamed to `x`.

In order to iterate over a chain of bind/bindE with a
monadic_rewrite_bind_tail-style rule such that bound names are
preserved, the rule's `f >>= (λrv. g rv)` must match up with the
relevant bound term `do x <- f'; g' x; ...` on the RHS/LHS and only on
that side:
* if the rule has an eta term on both sides and the goal a schematic on
  any side, the schematic will match trivially producing the correct
  name in the first subgoal only
* if the goal is not schematic and a tail rule applies, we need to
  choose a side to get the name from (usually the left)
This means if the goal is schematic on the RHS, we need a tail rule with
an eta term on its LHS, and vice-versa.

Since a generic form of this is not possible, this commit introduces
transformation lemmas and updates the tactics to use them for stepping
on the left/right.

For stopping the iteration by applying a rule to the head of a bind, the
situation is reversed: to preserve the name of the bind in the tail, the
head rule must not have any eta terms. The bind[E]_head rules have been
updated to reflect this.

Signed-off-by: Rafal Kolanski <[email protected]>

This demonstrates some sanity checking, a standard iterate-rewrite-refl
deployment, and the three symbolic execution methods, with a lot of
commentary.

Signed-off-by: Rafal Kolanski <[email protected]>

The `tcb` that previously became an `x` now remains a `tcb`.

Signed-off-by: Rafal Kolanski <[email protected]>

GHC 9.2.8 has better support for Linux/aarch64/v8 for use in Docker.

Signed-off-by: Gerwin Klein <[email protected]>

The implicit GITHUB_TOKEN does not trigger further push actions in
the same repo, but in this case we do want the push action to happen
on the `-rebased` branches, so we use an explicit auth token instead.

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

Add safe datatype case distinction for corres -- wpc turns out to be
insufficient even after generalisation of the helper predicate.

- corres_cases_left: case distinction on abstract monad
- corres_cases_right: case distinction on concrete monad
- corres_cases: try first corres_cases_left, then corres_cases_right
- corres_cases_both: simultaneous (quadratic) case distinction on
  both sides, with safe elimination of trivially contradictory cases.

Signed-off-by: Gerwin Klein <[email protected]>

This setup didn't actually work. Replaced by corres_cases.

Signed-off-by: Gerwin Klein <[email protected]>

Demonstrates use of corres_cases and corres_cases_both. Main intended
benefit is less thinking about safety of schematics, fewer mentions
of goal parameter names, and fewer manual guard instantiations.

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Corey Lewis <[email protected]>

The default behaviour is now to not rewrite the return relations and
extraction functions.

Signed-off-by: Corey Lewis <[email protected]>

Signed-off-by: Corey Lewis <[email protected]>

This also renames most of the corres* methods to corresK* methods,
including corressimp -> corresKsimp.

Signed-off-by: Gerwin Klein <[email protected]>