* getHSR confirmed unusued
* setHCR confirmed used on C side for hyp
* addressTranslateS1 was merged into C
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
* explain how canonical_bit concept applies to AArch64
* use powers of 2 for kernelELFBase
* pptrBase unlikely to migrate to 0 in near future
* pptrUserTop_def' is not used on AARCH64, and should not be used as we
try to avoid expanding config_ARM_PA_SIZE_BITS_40 whenever possible
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Draw connection between conjugate wp in the literature and our
exs_valid definition.
Add exs_valid_alt lemma, which is one of the main rules that is
different between wp and conjugate wp (or vs and).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The `export-kernel-builds.py` script expects to be able to run the
build from an arbitrary temporary directory.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add mechanism for adding overlay.dts files to the l4v build for all
architectures apart from X64 (which does not use dts files).
For example, place a file `overlays/ARM/overlay.dts` into the tree and
the build will pick it up as custom overlay file with the correct proof
session dependencies.
If no file is provided, an empty default overlay file is used.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
In order to parametrise the kernel's physical address in verification,
physBase becomes a function in C.
This updates the functional correctness proofs so that they work again.
Proper abstraction of physBase in the proof is forthcoming.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Extract the numeric value PHYS_BASE_RAW from the generated header
gen_headers/plat/machine/devices_gen.h and provide it as the constant
physBase in Kernel_Config.thy.
In C this will later match up with the value returned by physBase().
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Allow more settings to be overridden when using the standalone C parser
to generate kernel.sigs in the l4v kernel make files.
This makes it easier to use a pre-built standalone C parser, say, from a
Docker image.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
The decompilation process (part of binary verification) is more tightly
coupled to the graph-refine repository than l4v, so it makes more sense
to perform decompilation in graph-refine. (It was temporarily performed
here in l4v because the graph-refine branches needed some stabilisation
work.)
This also modifies proof workflows:
- All proof workflows now upload kernel build artifacts. These can be
used as inputs to binary verification.
- Proof workflows other than the one for pull requests (proof.yml)
automatically trigger a decompilation workflow. We can still manually
initiate a decompilation workflow using the uploaded artifacts, but
doint so automatically would consume too many parallel runners.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
This can be used by l4v proof runs in GitHub CI to save kernel build outputs
for later use by binary verification.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
seL4/seL4#975 slightly changed how the config headers are generated.
They now need a (short) `ninja` build step and they produce less spaces
in the header file.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
We have so far not been mentioning L4V_ARCH in the instructions and
haven't pointed out which sessions need generated input.
Add this information to the instructions.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Need to check out the ci-actions repo first (where the nl-unescape.sh
script is located).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Enable use of "eval" and "value" for formulas that quantify over word
values. The code generator will exhaustively run all possible values.
For small word sizes, this works in very reasonable time. E.g. try
lemma "∀(x::8 word) y. x + y = (x AND y) + (x OR y)"
by eval
or
value "∀(x::4 word) y z. y mod z = 0 ⟶
(x * y) div z = x * (y div z)"
Note that as usual for "eval" and "value" terms have to be close, i.e.
you need to use object logic quantifiers.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
A lemma set for the strengthen method to pull `invs` out of
implications. Together with simp and conj_cong, this can help avoid
proving `invs` multiple times (which tends to blow up the proof state).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- pull base-level empty_fail lemmas from AInvs into Monads.Empty_Fail
- apply consistent naming
- apply consistent [intro!, wp]
- make all non-conditional lemmas [simp]
- re-add context building to empty_fail rules, because the select_*
rules may need context to solve their side condition
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- merge EmptyFailLib into Monads.Empty_Fail
- group Empty_Fail lemmas so it is clear where to add new ones
- add [empty_fail] so not every lemma has to declare multiple attributes
- add instructions
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- apply modern style
- contract some proofs
- this commit includes some lemmas factored out from NonDetMonadVCG in
a previous commit
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- style and some proof contraction
- `in_monad` set remains unchanged for now (could now add additional
lemmas, but they might break things)
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- factor out valid_NF definition and lemmas into NonDetMonad_Total
- apply modern style and (very) occasional proof contraction in both
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- factor out valid_exs definition and properties into NonDetMonad_Sat
- apply modern style to both of these and More_NonDetMonadVCG
- factor out one lemma into Monad_Lib
- better grouping of lemmas in NonDetMonadVCG
- occasional proof contraction
Should contain no real semantic differences, but might have subtle
wp set changes due to reordering (to be fixed up in a later commit).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This should allow wpfix to automatically fix up projl/projr proofs.
This was previously not possible without drawing in Lib, but will now
be picked up by Lib since theLeft/theRight are now abbreviations.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Gerwin Klein
Rafal Kolanski
Matthew Brecknell
Peter Chubb
Corey Lewis
Michael McInerney
michaelmcinerney