Moves some unnecessary stuff out of the locale and now specifies the label type
as `string` rather than a locale parameter. The purpose of the latter is to
allow us to talk about concrete labels rather than continually falling back on
the user's projection, but it's not clear yet whether this is a big win.
This commit contains a grab bag of lemmas used in CAmkES↔CapDL correspondence
proofs. Some of them are exceedingly brain dead. This is, in most cases,
because they have been extracted from automated proofs in order to avoid
generated proofs repeatedly proving the same trivial facts.
These were phrased as slots containing NULL caps, but the translation of CapDL
specifications into Isabelle actually just restricts the domain of the
underlying capability map. This is much cleaner and we now have exact
equivalence.
This connection actually uses read/write caps on both sides because it is
implemented using Send and Wait. It may be worthwhile modelling seL4RPCCall
(which is implemented using Call and ReplyWait) as well. This would be a
trivial extension.
CAmkES deliberately skips over CSlot 0 when allocating caps to allow typos and
misallocations to be more easily detected. This commit captures this logic in
the generator function.
Previously, the CapDL-generating function assumed a CNode size of 12 bits for
each component instance, though this was known to be inaccurate. In the
implementation of CAmkES, the code generator calculates the minimum required
size of each CNode on the fly. This commit updates the formalised generator to
perform the same calculation. The calculation is currently written in terms of
the `LEAST` binder, which as it turns out is sometimes awkward to reason about.
It may be worthwhile rephrasing this in future.
The CapDL translation tools produce threads with an undefined intent, rather
than no intent. This commit modifies the CAmkES generation to do the same to
ease the correspondence proof.
Presumably this is only the case for when there are no assigned interrupts in
the system. These theories will need some tweaking to support systems with
interrupts.
Thomas Sewell
Matthew Fernandez
Joel Beeren
Japheth Lim
Daniel Matichuk
Gerwin Klein
Daniel Matichuk
Toby Murray