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>
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.
now that we have valid_vspace_objs to express validiy of
vspace objects, we do not need valid_arch_objs: we have
valid_objs to state the validity of non-vspace arch objects.
Corey Lewis
Rafal Kolanski
Miki Tanaka
Gerwin Klein
Victor Phan
Edward Pierzchalski
Mitchell Buckley
Matthew Brecknell
Thomas Sewell
Miki Tanaka
Joel Beeren
Daniel Matichuk
Alejandro Gomez-Londono
Alejandro Gomez-Londono
Rafal Kolanski