Convert license tags to SPDX identifiers

This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.

x86: declare halt() as DONT_TRANSLATE for verification

Fix licenses (the rest)

s/D61/DATA61/ in license headers for consistency

trivial: print kernel entry reason on halt

It is generally useful to know what operation was occuring
when the kernel halted, as this is usually called from assert.

Remove many DONT_TRANSLATE markers.

The vast majority of the DONT_TRANSLATE markers in the kernel are used
to hide __asm__ statements and builtin functions
(e.g. __builtin_unreachable ()) from the C-to-Isabelle parser.

The parser now supports underscore identifiers and many __asm__ statements,
and the builtin functions are prototyped, meaning the vast majority of the
DONT_TRANSLATE markers can be dropped. The remaining markers cover functions
that must be treated specially.

x86: replace idle/halt[.S] with idle.c