diff --git a/include/arch/arm/arch/machine/gic_v3.h b/include/arch/arm/arch/machine/gic_v3.h
index 6e5802fd1..b1f5a1d82 100644
--- a/include/arch/arm/arch/machine/gic_v3.h
+++ b/include/arch/arm/arch/machine/gic_v3.h
@@ -23,6 +23,11 @@
 
 #include "gic_common.h"
 
+/**
+ * Per §4.8 of ARM GICv3/v4 Spec (IHI0069 Hb):
+ *  - higher numbers are lower priorities
+ *  - the GIC must support at least priority bits [7:4], i.e 0x00-0xF0 in steps of 16.
+ **/
 #define GIC_PRI_LOWEST     0xf0
 #define GIC_PRI_IRQ        0xa0
 #define GIC_PRI_HIGHEST    0x80 /* Higher priorities belong to Secure-World */
@@ -33,8 +38,21 @@
 #define GIC_SGI_NUM_TARGETS 16
 
 /* Register bits */
+
+/**
+ * The GICD_CTLR distributor control register (per IHI0069 Hb) has various
+ * layouts depending on the security state configuration. seL4 assumes that
+ * we are in:
+ *
+ *   - "access is Non-secure, in a system that supports two Security states", or
+ *   - "When in a system that supports only a single Security state".
+ *
+ * and not "When access is Secure, in a system that supports two Security states".
+ * In both these cases GICD_CTLR_ARE_NS is bit 4. RWP, Enable_G1NS and EnableG0
+ * bits do not move around depending on the layout.
+ */
 #define GICD_CTLR_RWP                BIT(31)
-#define GICD_CTLR_ARE_NS             BIT(5)
+#define GICD_CTLR_ARE_NS             BIT(4)
 #define GICD_CTLR_ENABLE_G1NS        BIT(1)
 #define GICD_CTLR_ENABLE_G0          BIT(0)