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>
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>
- in VSpace_R
- the same method added to each arch; would be good to unify via
arch split in the future
- also includes some style cleanup
Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
Importing Init_R into ADT_H was causing EmptyFail_H to fail. Since
no other theories actually depend on Init_R we can instead include
it in the Refine session directly.
Signed-off-by: Mitchell Buckley <mitchell.alan.buckley@gmail.com>
Describe an extremely simple abstract kernel state, and haskell state
that obey the state relation. These states are `zeroed` in the sense
that they have empty heaps, and default values of 0, False, None, []
and similar in all fields.
These states do not satisfy invs or invs', and this is not as strong
a result as showing that kernel initial states satisfy the state
relation, but it is a good sanity check on the relation itself.
Signed-off-by: Mitchell Buckley <mitchell.buckley@data61.csiro.au>
This verifies a C kernel patch (seL4/seL4#409) which consolidates
translation between virtual and physical addresses, and makes it
consistent across architectures. In particular, we always use
`addrFromKPPtr`, even on architectures that don't use a distinct region
to map the kernel ELF. This will facilitate future improvements which
move the ELF mapping into a distinct virtual address region.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Ideally all corres lemmas of the form
`corres rrel P P' my_abstract_function myHaskellFunction`
should be named `myHaskellFunction_corres`.
This commit renames over 200 lemmas to match this style.
Signed-off-by: Mitchell Buckley <mitchell.alan.buckley@gmail.com>
Co-authored-by: Victor Phan <Victor.Phan@data61.csiro.au>
Currently this just modifies the rule but not any of the proofs that use
it. The old version is kept for now but should be removed once all of
the proofs are updated.
Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>
This brings the naming convention closer to the other architectures,
closer to the Haskell, and closer to the constant renames that happened
in C. It is, however, quite an invasive change.
kernelBase_addr -> pptrBase
kernelBase -> pptrBase
physMappingOffset -> ptrBaseOffset
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
Remove resolve_address_bits'.simps from the simp set at the definition
site, instead of in the middle of the proofs.
Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>
In Isabelle2020, when isabelle jedit is started without a session
context, e.g. `isabelle jedit -l ASpec`, theory imports with path
references cause the isabelle process to hang.
Since sessions now declare directories, Isabelle can find those files
without path reference and we therefore remove all such path references
from import statements. With this, `jedit` and `build` should work with
and without explicit session context as before.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
Isabelle2020 requires each session to declare it own set of directories that
may not overlap with other session's directories. This commit reorganises
files to comply with that requirement.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
Create ArchMove_R.thy for transporting arch specific lemmas (and generic
lemmas that are used somewhat specifically by one architecture) to theory
files before Refine.
Create Move_R.thy as an arch generic Refine theory file for transporting
generic lemmas to theory files before Refine.
Also delete some lemmas that have existed earlier already or are not
needed.
Rename Move.thy in CRefine to Move_C.thy for consistency.
Several constants are are added to the top level crunch_ignore statement in
Bits_R.thy, then removed from individual crunch statements across Refine and
CRefine.
diminished takes two caps and asserts that one is equal to the other
except that one may have fewer rights. We remove this definition and all
references to it, replacing diminished with equality.
Prior to this commit the kernel would always trigger a full reschedule
on setPriority. This change allows the kernel to attempt a direct
switch, avoiding invoking the scheduler.
Gerwin Klein
Rafal Kolanski
Florian Haftmann
Miki Tanaka
Ryan Barry
Mitchell Buckley
Mitchell Buckley
Matthew Brecknell
Corey Lewis
Rafal Kolanski
Gerwin Klein
Victor Phan
MiladKetabi
Amirreza Zarrabi