* commit 'b9410822':
  arm/tk1: add support for Nvidia Tegra K1 board

Apologies, some final adjustments got lost in the previous pull
request round. This version actually works.

* commit '13715658':
  Verification: bf: use new proof features.

Inline text blocks are not permitted without extra spacing in literate
Haskell files. This tweak makes the Haskell kernel build again.

The plan here is to move some of the proof script complexity embedded
in the text of the bitfield_gen utility into generic proof helpers in the
l4v repository that bitfield_gen can use more modularly. This is a simple
first step.

* commit '3554358c':
  Use correct version file in manual.tex

The type of irq_t differs per platform, this commit just forces
a conversion to an int, which should be sufficient for a debug
message

* commit '9ae867cb':
  SELFOUR-435: change kernel timer from GPT11 to 9

GPT1-9 are configured by uboot to run at 13Mhz,
while GPT10-11 are not and run with a much slower clock.

* commit '289bf92b':
  SELFOUR-114: remove bootinfo.h duplication

* commit '602f5369':
  x86: Change some PHYS_CODE to BOOT_CODE

* commit '2027e2e3':
  SELFOUR-251 Add descriptions of the seL4_Page_GetAddress_t

* commit 'd2030938':
  Added API documentation for the ARM cache flushing functions.

The functions pit_init and pit_wait_wraparound were previously marked as
PHYS_CODE, despite being called from BOOT_CODE elsewhere. This bug has
been present for some time but can be masked by the compiler inlining
all the involved functions, which is what typically happens.

SELFOUR-262

Previously the external build system was relied upon for disablingdisabling sse.
This is not desirable as it has the affect of disabling sse for the entire user
level build. Instead, since we only want to disable it for the kernel, we will
disable it here in the kernel Makefile

Diminish rights were to prevent a user from sending a writeable
cap over a read only endpoint. It turns out this 'security' can
be worked around without difficulty (by putting caps in a cnode
and sending the cnode) making the current diminish rights
implementation functionally useless.

Removing diminish rights has the benefit of simplifying all the
IPC paths.

Newline for latex compilation. This one isn't strictly required but will clash with the regression test.