mod: Ext 9 — policy dry-run trace diagnostics, 247/247

mod/trace-rules evaluates a report against every rule, returning each rule's
proved/unproved status + goal-by-goal derivation (an unproved rule shows which
goal failed). mod/first-proved = winner (matches engine precedence, cross-checked),
mod/proved-rules the firing set, mod/trace-report a [fires]/[ - ] rendering.
Answers 'why didn't my rule fire?' without instrumenting the engine. +15 tests.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

plans/mod-on-sx.md

@@ -16,7 +16,7 @@ federation extension.
 
 ## Status (rolling)
 
-`bash lib/mod/conformance.sh` → **232/232** (roadmap + 8 extensions complete)
+`bash lib/mod/conformance.sh` → **247/247** (roadmap + 9 extensions complete)
 
 ## Ground rules
 
@@ -147,6 +147,12 @@ lib/mod/fed.sx
   derivation goal-by-goal with `[proved]`/`[unproved]` marks and unification
   bindings. E.g. `Report rc: escalate (rule: repeated-escalate)` … `[proved]
   report(rc, B, S), report_count(S, N), N >= 3  {B=ann, N=3, S=dave}`.
+- [x] **Ext 9 — policy dry-run trace** (`lib/mod/trace.sx`, +15). `mod/trace-rules`
+  evaluates a report against every rule and returns each rule's proved/unproved
+  status + its goal-by-goal derivation, so an unproved rule shows which goal
+  failed. `mod/first-proved` = the winner (engine precedence), `mod/proved-rules`
+  the full firing set, `mod/trace-report` a `[fires]`/`[  -  ]` rendering. Answers
+  "why didn't my rule fire?" without instrumenting the engine.
 - [x] **Ext 8 — quorum over distinct reporters** (`lib/mod/quorum.sx`, +9). Anti-
   brigade: `(:reporters-at-least N)` compiles to `setof(Br, report(_, Br, Sr), Bsr),
   length(Bsr, Nr), Nr >= N` — distinct reporters, not raw report count.
@@ -180,6 +186,11 @@ lib/mod/fed.sx
 
 ## Progress log
 
+- **Ext 9 — policy dry-run trace, 247/247** (+15). Whole-rule-set diagnostics over
+  the proof machinery: every rule's fire/no-fire and the goal that decided it. The
+  winner agrees with `decide-report` by construction (first proved = pl-query-one),
+  cross-checked in a test. Turns the proof tree from a per-decision artifact into a
+  policy-debugging tool.
 - **Ext 8 — quorum over distinct reporters, 232/232** (+9). Distinct-reporter
   consensus via Prolog `setof`/`length`, requiring a second engine variant that
   asserts all reports (the base engine deliberately scopes facts to the decided