Once again, we know in the abstract invariants that these must be
async endpoint caps or null caps, but this is only knowable in
haskell by asserting it.

Need to be careful about operations that are ambiguous in Haskell
but well-defined in the resulting Isabelle import.

We can't prove that the caller cap must be a reply cap or that
the frames mapped in an arbitrary address space are backed by caps
without appealing to the abstract invariants, which means yet more
assertions in haskell and work in the abstract/haskell refinement.

It's true that the interrupt node must contain async endpoint
caps, but we never proved the relevant invariant, and it doesn't
change much.

Fix: In exynos timer driver, declaring comparator_value variable at top of initTimer to comply with C90.

When initializing the exynos mct, set the initial value of the 64-bit comparator to the sum of the the 64-bit counter and TIMER_TICKS.

bitfield: Allow for controlling how many bits of a word are actually used, and whether the rest of the bits are signed extended or not

This change purely changes the ordering of C symbols, as well as
adding some extra checking

This option is not necessary at compile-time as it is subsumed by the
compiler's #defines, but it is useful for code generators such as CAmkES to
know, at generation-time, the native word size of the platform they are
generating code for. Existing mechanisms either hard code a 32-bit platform or
use a set of fragile heuristics to work out the word size. Note that this
option is set automatically and not visible from menuconfig.

IA32 is 32bit version of the x86 architecture. Whilst only IA32
is supported, much of the code is generic x86. Using a generic
x86 architecture will aid in future 64bit support

Use explicit struct packing instead of using compiler asserts
to check that packing happened as expected

The ACPI standard says these fields are 32bits, not the size
of a machine word or pointer

Using an unsigned long instead of forcing to 32bits allows this code
to be reused in a 64-bit context

This is a paranoia commit as most compilers will not
pad members of a struct if they are all the same size,
but this commit ensures it.

The multiboot specification states that these fields are 32bits in sized,
not the size of machine pointer or integer.