:: commit 0ec37e7e5be5ac06943240ea25c01e565ce88597

diff --git a/PROTOCOL.md b/PROTOCOL.md
index edf1bcb7..8a0b96fa 100644
--- a/PROTOCOL.md
+++ b/PROTOCOL.md
@@ -122,6 +122,19 @@ The MTRRs are left as the firmware set them up.
 The PAT's (Page Attribute Table) layout is unspecified and the OS should
 not be making assumptions about it.
 
+### aarch64
+
+All HHDM memory regions are mapped using the Normal Write-Back RW-Allocate
+non-transient caching mode, except for the framebuffer regions, which are
+mapped in using an unspecified caching mode, correct for use with the
+framebuffer on the platform.
+
+The `MAIR_EL1` register will at least contain entries for the above-mentioned
+caching modes, in an unspecified order.
+
+In order to access MMIO regions, the kernel must ensure the correct caching mode
+is used on it's own.
+
 ## Entry machine state
 
 ### x86_64
@@ -173,27 +186,25 @@ All other general purpose registers are set to 0.
 unless the an Entry Point feature is requested (see below), in which case,
 the value of `PC` is going to be taken from there.
 
-The contents of the `VBAR_EL1` register are undefined, and the kernel must load it's own.
-
-The `MAIR_EL1` register will contain at least these entries, in an unspecified order:
- - Normal, Write-back RW-Allocate non-transient (`0b11111111`),
- - Unspecified, correct for use with the framebuffer.
+The contents of the `VBAR_EL1` register are undefined, and the kernel must load
+it's own.
 
-The kernel and the lower-half identity mapping will be mapped with Normal write-back memory,
-while the framebuffer is mapped with the correct caching mode. The kernel must ensure that
-MMIO it wants to access is mapped with the correct caching mode.
+The `MAIR_EL1` register contents are described above, in the caching section.
 
 All interrupts are masked (`PSTATE.{D, A, I, F}` are set to 1).
 
-The kernel is entered in little-endian AArch64 EL1t (EL1 with `PSTATE.SP` set to 0, `PSTATE.E` set to 0, and `PSTATE.nRW` set to 0).
+The kernel is entered in little-endian AArch64 EL1t (EL1 with `PSTATE.SP` set to
+0, `PSTATE.E` set to 0, and `PSTATE.nRW` set to 0).
 
 Other fields of `PSTATE` are undefined.
 
-At entry: the MMU (`SCTLR_EL1.M`) is enabled, the I-Cache and D-Cache (`SCTLR_EL1.{I, C}`) are enabled,
-data alignment checking (`SCTLR_EL1.A`) is disabled. SP alignment checking (`SCTLR_EL1.{SA, SA0}`) is enabled.
-Other fields of `SCTLR_EL1` are reset to 0 or to their reserved value.
+At entry: the MMU (`SCTLR_EL1.M`) is enabled, the I-Cache and D-Cache
+(`SCTLR_EL1.{I, C}`) are enabled, data alignment checking (`SCTLR_EL1.A`) is
+disabled. SP alignment checking (`SCTLR_EL1.{SA, SA0}`) is enabled. Other fields
+of `SCTLR_EL1` are reset to 0 or to their reserved value.
 
-Higher ELs do not interfere with accesses to vector or floating point instructions or registers.
+Higher ELs do not interfere with accesses to vector or floating point
+instructions or registers.
 
 Higher ELs do not interfere with accesses to the generic timer and counter.
 
@@ -205,7 +216,8 @@ If booted by EFI/UEFI, boot services are exited.
 at least 64KiB (65536 bytes) in size, or the size specified in the Stack
 Size Request (see below).
 
-All other general purpose registers (including `X29` and `X30`) are set to 0. Vector registers are in an undefined state.
+All other general purpose registers (including `X29` and `X30`) are set to 0.
+Vector registers are in an undefined state.
 
 ### riscv64