evidence: re-seal the Apple route ledger; give promotion_rules a consumer

docs/audit/backend/apple/todo.md

@@ -6327,3 +6327,148 @@ covered not-registered, wrong-region and unavailable-here alike, and once a
 shape axis existed it was actively wrong for the commonest case: the lane IS
 available, on a host that has it, for a shape it cannot serve. It now names
 which of the four gates rejected the candidate (Decision #21).
+
+## Cross-backend sync `ROUTE-LEDGER-RULES-UNCONSUMED-2026-09-01`
+
+**Owning item:** Apple strict route ledger re-seal · **synchronization key:**
+`ROUTE-LEDGER-RULES-UNCONSUMED-2026-09-01`
+
+**The red lane that started this.**
+`test_strict_retune_ledger_admits_on_its_exact_live_apple_host` had been
+failing on this Mac and was reported as "pre-existing" more than once. It was
+right to fail: the ledger was rejected on **four independent axes** —
+`os_version` (26.5.2 → 26.6.2), `compiler_fingerprint`, `runtime_fingerprint`
+(this session edited `apple_gpu_runtime.mm`), and `stale_evidence` (expired
+2026-08-20, twelve days before). The gate was doing its job; the evidence was
+genuinely dead.
+
+**Re-measured, not re-stamped**, per the standing rule for this artifact:
+`benchmark_legacy_retune.py --profile extended` (2 runs × 24 rows), then sealed
+through the existing `seal_strict_route_ledger`. Zero rejections against the
+live context; 16 decisions and 8 ineligible, **identical key sets to the
+July ledger** — nothing lost, nothing invented.
+
+*Near-miss worth recording:* the first re-run used `--profile core`, which
+admitted cleanly with **8** decisions instead of 16. `rejected == ()` would
+have read as success while silently halving the Apple route evidence — the
+same shape as the corpus recorder that once produced a corpus with *less*
+evidence than it started with. Diffing the decision key sets against the
+committed ledger is what caught it, not the admission result.
+
+**One real route change, and its cause is not the obvious one.**
+`retune_mla_decode` end-to-end flips `explicit` → `absorbed` at both shapes.
+`absorbed` was never slower: in July it was **54–57% faster with 100% paired
+wins in both runs**, and was held back solely because its cross-run speedup
+spread (5.97%) missed the ledger's own 5% stability cap by ~1 point. The re-run
+measures 37–39% faster, again 100% paired wins, spread **2.3%** — so it
+promotes. The flip is "the measurement became consistent enough to conclude",
+not "the kernel got faster".
+
+**Diagnostic, deliberately not a route claim** (`promotion_rules` sets
+`absolute_time_drift_is_diagnostic_only: true`): absolute times moved the wrong
+way. `absorbed` went 518µs → 836µs at the 128-token shape and 482µs → 557µs at
+64, while `explicit` held (1.15× / 0.96×). The larger shape's regression is
+outside this harness's own run drift; the smaller one is not. Cause is
+confounded — OS 26.5.2 → 26.6.2, runtime `.mm` edits, and a new compiler
+fingerprint all landed between the two measurements — and is **not attributed
+here**. It is worth a dedicated look.
+
+**The structural finding: `promotion_rules` was a declaration with no
+consumer.** `aggregate_stable_route_reports` computes the thresholds, applies
+them, and writes them into the ledger; `seal_strict_route_ledger` copies them
+forward for audit; **twelve committed ledgers carry the block and nothing ever
+read it back**. `load_strict_route_ledger` checks provenance exhaustively —
+schema, scope, exact context, freshness, source-report digests, native
+provenance, correctness, timing domain, device, duplicates — and the promotion
+criteria not at all, so `status: "promote_candidate"` was self-certifying. A
+row naming a route that lost every paired trial would have been admitted and
+served. Decision #29, in the evidence layer rather than the IR.
+
+`promotion_rule_violations()` now re-derives each promotion from the evidence
+the ledger retained, and the **loader rejects a decision its own ledger's rules
+refuse** — a production gate, not an audit script. Applied to all 12 committed
+strict ledgers: **59 promotions checked, 0 violations**, so this confirms the
+aggregator rather than accusing it. Mutation-verified against seven forged
+rows (lost every trial / speedup under minimum / spread over maximum / no
+numerical proof / no resource evidence / evidence deleted / rules block
+removed) — each is caught, and a missing rules block fails **closed**
+(`promotion_rules_incomplete`), because without a threshold there is nothing to
+hold the promotion to and the honest verdict is "unverifiable", not "fine".
+
+**Outcome for this backend: `parity validated` — measured on the Mac (M1 Max,
+macOS 26.6.2), which is the only host that can produce this evidence.**
+
+## APPLE-DISPATCH-WEDGE-1: a timed-out MPSGraph dispatch has no circuit breaker *(open, investigated 2026-09-01, M1 Max)*
+
+**Trigger.** An Apple `-k apple` sweep sat for **70 minutes** at 0.0% CPU
+(1:42 CPU time), stack-sampled entirely inside
+
+```
+mpsg_run_binary
+ -> commit_mpsgraph_and_wait_with_timeout(ctx, mps_cb, metal_cb, 30000, "mpsgraph_binary", &timing)
+   -> -[IOSurfaceSharedEvent waitUntilSignaledValue:timeoutMS:]  (in IOSurface) + 72
+     -> iokit_user_client_trap  (in IOKit) + 8
+```
+
+**Correction, recorded because the first reading was wrong.** I initially wrote
+that the function's namesake guarantee "doesn't hold" — that
+`waitUntilSignaledValue:timeoutMS:` was ignoring its timeout. **That is false,
+and it was checked rather than assumed.** A standalone probe
+(`scratchpad/event_timeout_probe.mm`, built against the on-machine SDK per
+Decision #27) measures the API honouring its deadline precisely:
+
+| case | timeout | returned | elapsed |
+|---|---|---|---|
+| never signalled | 250 ms | `NO` | 251.0 ms |
+| never signalled | 1000 ms | `NO` | 1001.0 ms |
+| never signalled | 3000 ms | `NO` | 3000.2 ms |
+| CPU signal at 100 ms | 5000 ms | `YES` | 104.2 ms |
+| GPU-encoded signal | 5000 ms | `YES` | 0.1 ms |
+| **committed buffer, unreachable value** | 1000 ms | `NO` | **1001.0 ms** |
+
+The last row is the exact shape of the failure — work committed, awaited value
+never arriving — and it times out correctly.
+
+**And the probe provably exercises the same code path**, which is the step that
+makes the above admissible rather than merely suggestive: sampling the probe
+mid-wait yields the identical frame *at the identical address* as the hung
+process — `-[IOSurfaceSharedEvent waitUntilSignaledValue:timeoutMS:] + 72
+[0x1988de184]` -> `iokit_user_client_trap + 8 [0x190604ae0]`. (`[dev
+newSharedEvent]` returns `_MTLSharedEvent`, whose wait is implemented by
+`IOSurfaceSharedEvent`; the two class names are one path, not two.)
+
+**What is NOT established.** Whether the 70 minutes was *one* uninterruptible
+wait — a driver wedge defeating the kernel-side deadline — or **~140 sequential
+30-second timeouts** (70 min / 30 s = 140, a suspiciously round fit). A `sample`
+aggregates by stack, so it cannot separate one 70-minute wait from 140
+consecutive ones; and the process was killed before forward progress could be
+checked. No GPU fault appeared in `log show --last 4h` and no hang report was
+written, so a driver wedge has **no positive evidence** either. Both remain
+open. It has not reproduced: the same sweep re-ran clean in **4:03**.
+
+**What IS established, and is a defect under either hypothesis: there is no
+circuit breaker.** Seven call sites, six at 30 000 ms and one at 60 000 ms. On
+timeout the caller correctly falls back to the host recovery path — but nothing
+records that the *device* is unusable, so every subsequent dispatch pays the
+full timeout again. Worse, `commit_mpsgraph_and_wait_with_timeout` calls
+`ts_clear_dispatch_telemetry()` **on entry**, so the previous timeout's evidence
+is erased before the next attempt. `g_last_gpu_error_kind` is a `thread_local`
+*last-error* for reporting, not accumulating state, and nothing consults it to
+short-circuit. So a device that wedges early in a suite turns a 4-minute run
+into an unbounded one, and by design leaves no accumulated trace of why.
+
+30 s is a defensible production timeout and a poor test one; the missing piece
+is not a smaller number but a state that says *stop asking*.
+
+**Proposed fix (not yet made, and it carries a sequencing constraint).** A
+process-wide sticky counter: after N consecutive dispatch timeouts, stop
+attempting GPU dispatch, go straight to the host path, and emit one stable
+diagnostic naming the op and the count (Decision #21 — never a silent no-op).
+The telemetry clear must move so it cannot erase the signal it is counting.
+
+**Sequencing.** `AppleRouteContext.runtime_fingerprint` is
+`sha256(apple_gpu_runtime.mm)` (`apple_route_selector.py::_runtime_source_fingerprint`),
+so **any edit to that file invalidates the strict route ledger** and puts
+`test_strict_retune_ledger_admits_on_its_exact_live_apple_host` back to red.
+The fix therefore has to land together with a benchmark re-run and re-seal
+(`ROUTE-LEDGER-RULES-UNCONSUMED-2026-09-01`), not before or after it.

docs/audit/backend/nvidia/todo.md

@@ -5714,3 +5714,29 @@ covered not-registered, wrong-region and unavailable-here alike, and once a
 shape axis existed it was actively wrong for the commonest case: the lane IS
 available, on a host that has it, for a shape it cannot serve. It now names
 which of the four gates rejected the candidate (Decision #21).
+
+## Cross-backend sync `ROUTE-LEDGER-RULES-UNCONSUMED-2026-09-01`
+
+**Owning item:** Apple strict route ledger re-seal · **synchronization key:**
+`ROUTE-LEDGER-RULES-UNCONSUMED-2026-09-01`
+
+Apple's `promotion_rules` block turned out to be a declaration no code read:
+sealed into twelve ledgers for audit, and `status: "promote_candidate"` was
+self-certifying at load. Fixed there (see the Apple plan). All four backends
+are assessed because the *pattern* is what travels, not the Apple code.
+
+**Outcome for this backend: `follow-up required` — the same gap exists here,
+in a milder form.** `nvidia_sm120_legacy_retune.json` and
+`nvidia_sm120_low_precision_native_routes.json` declare `noise_policy`
+(0.03 / 0.04) and `selector_promotions`, and the ratchets assert those values
+**equal a constant** without ever comparing a promoted row's margin against the
+policy the file declares. So a promotion inside the noise band would pass every
+existing check.
+
+Credit where due: `test_nvidia_low_precision_native_routes.py` is otherwise
+well built for this class — it cross-checks the summary count against the rows,
+explicitly guards the vacuous-pass case (`len(promoted) == selector_promotions
+> 0`), and requires timing-domain consensus plus resource fingerprints on every
+promoted row. The missing piece is exactly one: **the margin is never held to
+`noise_policy`.** That is a smaller job than Apple's was, and it needs a
+decision about what "margin" means for these rows before it is written.

docs/audit/backend/rocm/todo.md

@@ -6162,3 +6162,28 @@ covered not-registered, wrong-region and unavailable-here alike, and once a
 shape axis existed it was actively wrong for the commonest case: the lane IS
 available, on a host that has it, for a shape it cannot serve. It now names
 which of the four gates rejected the candidate (Decision #21).
+
+## Cross-backend sync `ROUTE-LEDGER-RULES-UNCONSUMED-2026-09-01`
+
+**Owning item:** Apple strict route ledger re-seal · **synchronization key:**
+`ROUTE-LEDGER-RULES-UNCONSUMED-2026-09-01`
+
+Apple's `promotion_rules` block turned out to be a declaration no code read;
+fixed there (see the Apple plan). Assessed here because the pattern travels.
+
+**Outcome for this backend: `follow-up required`, and this one is furthest
+from checkable.** `rocm_gfx1151_compiler_retune_2026_07_15.json` declares its
+gate as **prose**:
+
+> `"promotion_gate": "correct oracle plus shape-specific repeated-median gate"`
+
+That is unconsumable by construction — no threshold, no field name, nothing a
+loader could re-derive. NVIDIA's `noise_policy` is at least a number that
+nothing reads; this is a sentence. Closing it means first deciding the numeric
+form of "shape-specific repeated-median gate", which is a modelling question,
+not a plumbing one — so it is scoped separately rather than bundled here.
+
+Related and already owed: the `AUTOTUNE-SEPARATION` work gave the ROCm corpus
+real `separation` verdicts and `record_is_admissible` now refuses unsupported
+rankings at every consumer. That is the same discipline in the autotune corpus;
+this entry is its counterpart in the route-ledger corpus.

docs/audit/backend/x86/todo.md

@@ -3693,3 +3693,20 @@ covered not-registered, wrong-region and unavailable-here alike, and once a
 shape axis existed it was actively wrong for the commonest case: the lane IS
 available, on a host that has it, for a shape it cannot serve. It now names
 which of the four gates rejected the candidate (Decision #21).
+
+## Cross-backend sync `ROUTE-LEDGER-RULES-UNCONSUMED-2026-09-01`
+
+**Owning item:** Apple strict route ledger re-seal · **synchronization key:**
+`ROUTE-LEDGER-RULES-UNCONSUMED-2026-09-01`
+
+Apple's `promotion_rules` block turned out to be a declaration no code read;
+fixed there (see the Apple plan). Assessed here because the pattern travels.
+
+**Outcome for this backend: `not applicable` — x86 has no route ledger.** The
+committed x86 baselines (`x86_avx512_e2e_*_comparison.json`, the
+`core_compiler_*_avx512.json` family) are direct measurement comparisons, not
+promotion ledgers: there is no incumbent-vs-candidate selector, so there is no
+promotion to certify and no rules block to leave unread. If an x86 route
+selector is ever added, the Apple loader's shape is the one to copy —
+**re-derive the promotion from the retained evidence at load time**, rather
+than trusting a status string and carrying the thresholds as documentation.

python/tessera/compiler/apple_route_selector.py

@@ -185,6 +185,89 @@ def _parse_utc(value: Any) -> datetime | None:
     return parsed if parsed.tzinfo is not None else parsed.replace(tzinfo=timezone.utc)
 
 
+def promotion_rule_violations(
+    row: Mapping[str, Any], rules: Mapping[str, Any],
+) -> list[str]:
+    """Which of the ledger's own ``promotion_rules`` a promoted row breaks.
+
+    **The rules were a declaration with no consumer.**
+    ``aggregate_stable_route_reports`` computes the thresholds, applies them,
+    and writes them into every sealed ledger; ``seal_strict_route_ledger``
+    copies them forward for audit; and until now nothing read them back. Twelve
+    committed strict ledgers carry this block, and a ``promote_candidate`` row
+    was admitted on the strength of its ``status`` string alone -- so a row
+    naming a route that lost every paired trial would have been served, as long
+    as its provenance fields were right. That is Decision #29 exactly: a
+    contract that reads as closed in review and carries nothing.
+
+    Re-deriving the verdict from the retained evidence is what makes the
+    ledger checkable by someone who did not run the benchmark. It is
+    deliberately a *re-derivation*, not a recomputation from raw times: the
+    aggregate's own numbers are the thing under audit.
+
+    Returns an empty list for a row that is not a promotion.
+    """
+    if row.get("status") != "promote_candidate":
+        return []
+    selected = row.get("selected_route")
+    evidence = row.get("route_evidence")
+    if not isinstance(evidence, Mapping) or not isinstance(selected, str):
+        return ["missing_route_evidence"]
+    chosen = evidence.get(selected)
+    if not isinstance(chosen, Mapping):
+        return [f"missing_evidence_for:{selected}"]
+
+    violations: list[str] = []
+
+    def _threshold(name: str) -> float | None:
+        value = rules.get(name)
+        return float(value) if isinstance(value, (int, float)) else None
+
+    min_speedup = _threshold("minimum_speedup_fraction_each_run")
+    min_win = _threshold("minimum_paired_win_fraction_each_run")
+    max_spread = _threshold("maximum_cross_run_speedup_spread")
+    # A missing threshold is not a pass. Without it there is nothing to hold
+    # the promotion to, and the honest verdict is "unverifiable", not "fine".
+    if min_speedup is None or min_win is None or max_spread is None:
+        violations.append("promotion_rules_incomplete")
+
+    medians = chosen.get("paired_median_speedups")
+    if not isinstance(medians, list) or not medians:
+        violations.append("no_paired_median_speedups")
+    elif min_speedup is not None and any(
+            not isinstance(v, (int, float)) or v < min_speedup for v in medians):
+        violations.append(
+            f"speedup_below_minimum:{min(v for v in medians if isinstance(v, (int, float)))!r}"
+            if any(isinstance(v, (int, float)) for v in medians)
+            else "speedup_below_minimum")
+
+    fractions = chosen.get("paired_win_fractions")
+    if not isinstance(fractions, list) or not fractions:
+        violations.append("no_paired_win_fractions")
+    elif min_win is not None and any(
+            not isinstance(v, (int, float)) or v < min_win for v in fractions):
+        violations.append("paired_win_fraction_below_minimum")
+
+    spread = chosen.get("cross_run_speedup_spread")
+    if not isinstance(spread, (int, float)):
+        violations.append("no_cross_run_speedup_spread")
+    elif max_spread is not None and spread > max_spread:
+        violations.append(f"speedup_spread_above_maximum:{spread!r}")
+
+    # The `requires_*` booleans name evidence that must be PRESENT, not a
+    # threshold to clear. Each maps to the field the aggregator set.
+    for rule, field in (
+        ("requires_native_dispatch", "placement_and_numerical_proof"),
+        ("requires_numerical_validation", "placement_and_numerical_proof"),
+        ("requires_repeated_measurement", "repeated_measurement"),
+        ("requires_interleaved_paired_trials", "paired_measurement"),
+        ("requires_resource_evidence", "resource_evidence_retained"),
+    ):
+        if rules.get(rule) is True and chosen.get(field) is not True:
+            violations.append(f"{rule}:unmet")
+    return violations
+
+
 def load_strict_route_ledger(
     path: str | Path,
     *,
@@ -230,6 +313,13 @@ def load_strict_route_ledger(
     decisions = payload.get("decisions")
     if not isinstance(decisions, list):
         return StrictRouteLedger({}, {}, ("missing_decisions",))
+    # The ledger carries the thresholds it was sealed under; hold it to them.
+    # Without this, `status: "promote_candidate"` was self-certifying -- the
+    # loader checked provenance thoroughly and the promotion criteria not at
+    # all, so a row naming a route that lost every trial would be served.
+    promotion_rules = payload.get("promotion_rules")
+    if not isinstance(promotion_rules, Mapping):
+        promotion_rules = {}
     routes: dict[tuple[str, str, str, str, str], str] = {}
     citations: dict[tuple[str, str, str, str, str], str] = {}
     for index, row in enumerate(decisions):
@@ -275,6 +365,10 @@ def load_strict_route_ledger(
         if key in routes:
             rejected.append(f"{prefix}:duplicate_key")
             continue
+        violations = promotion_rule_violations(row, promotion_rules)
+        if violations:
+            rejected.append(f"{prefix}:promotion_rule:{violations[0]}")
+            continue
         routes[key] = selected
         citations[key] = f"{Path(path)}#decision[{index}]"
     return StrictRouteLedger(routes, citations, tuple(rejected))
@@ -849,6 +943,7 @@ def seal_strict_route_ledger(
     "package_route_selected",
     "production_route_for",
     "production_route_decision",
+    "promotion_rule_violations",
     "live_apple_device_tag",
     "select_route",
     "seal_strict_route_ledger",