SPTM: function-level TLBI evidence (369 vs 264 insns, added completion wait)

docs/SPTM-MIE-27.2.md

@@ -48,8 +48,21 @@ hardening — none of it is named in the 162-CVE advisory:
 
 The TLBI string has five code xrefs in 27.2, at functions starting near
 `0xfffffff0270c7aac`, `0xfffffff0270c85f8`, `0xfffffff0270c987c`,
-`0xfffffff0270cacf4` and `0xfffffff027109940`. These are new/edited DART
+`0xfffffff0270cacf4` and `0xfffffff027109940`.
-invalidation paths, not present in the 27.0.1 image.
+
+Function-level alignment makes the change concrete. The first TLBI function
+(`0xfffffff0270c7aac`, **369 instructions**) matches a **264-instruction**
+function at `0xfffffff0270b7a90` in 27.0.1 (prefix similarity 0.90). The 27.2
+version inserts a block that:
+
+1. reads `DAIF` and masks interrupts (`msr DAIFSet, #0x7`, `dsb sy`);
+2. reads `CNTVCTSS_EL0` and `CNTFRQ_EL0` and computes a deadline;
+3. loads a timeout constant (`0x3d40` = 15680 units) and the TLBI verification
+   register address;
+4. polls/validates the GMMU TLBI completion, and only then continues.
+
+The 27.0.1 function issues the invalidation and proceeds without that wait. This
+is not a relocated instruction; it is an added completion check.
 
 The DART violation names are not referenced by a direct `adr`/`adrp+add` — they
 are indexed through a violation table, so their exact raiser is a table lookup.
@@ -107,6 +120,14 @@ These are grounded in the 27.2 changes and the unchanged MIE checks. None is a
 working exploit; each needs a reachable primitive that the firmware diff does
 not supply.
 
+0. **GMMU TLBI completion race (strongest static lead).** 27.0.1 lacks the
+   completion wait that 27.2 adds to the DART invalidation path. A DMA-capable
+   device whose translation is invalidated can keep using a stale GMMU entry if
+   the invalidation has not completed; the stale entry is a DMA read/write to a
+   page that SPTM has already unmapped or repurposed. This is an IOMMU bypass,
+   not a page-table permission bypass, but it defeats the same isolation goal.
+   Reachability requires a userclient that owns DART mappings and can keep DMA
+   in flight across an unmap — the next thing to test on hardware.
 1. **DART unganged-GAPF race.** 27.2 adds a violation for a race between
    unganging a DART and a page-table remap. On 27.0.1 the race can leave a stale
    DART translation if a mapping is unganged while a PTE is remapped. A stale