mod: Ext 3 — human-readable proof explanation (mod/explain), 164/164

mod/explain renders a decision's proof tree into legible text: action + rule,
evidence line, and each derivation goal with [proved]/[unproved] and the
unification bindings that satisfied it (e.g. {B=ann, N=3, S=dave}). Pure SX over
the Phase-2 proof data — the audit trail's 'why' made readable. +10 tests.

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

lib/mod/conformance.conf

@@ -13,6 +13,7 @@ PRELOADS=(
   lib/mod/schema.sx
   lib/mod/policy.sx
   lib/mod/engine.sx
+  lib/mod/explain.sx
   lib/mod/lifecycle.sx
   lib/mod/audit.sx
   lib/mod/api.sx

lib/mod/explain.sx

@@ -0,0 +1,55 @@
+;; lib/mod/explain.sx — human-readable proof explanation.
+;;
+;; Turns a decision (from mod/decide-report, or any audit entry) into a readable
+;; multi-line "why": the action, the rule that fired, the evidence in play, and
+;; the derivation goal-by-goal with [proved]/[unproved] marks and the unification
+;; bindings that satisfied each goal. Pure SX over the Phase-2 proof tree.
+
+(define
+  mod/explain-binds
+  (fn
+    (binds)
+    (mod/join-with
+      ", "
+      (map (fn (k) (str k "=" (dict-get binds k))) (keys binds)))))
+
+(define
+  mod/explain-goal
+  (fn
+    (g)
+    (let
+      ((mark (if (get g :solved) "  [proved] " "  [unproved] "))
+        (binds (get g :bindings)))
+      (if
+        (empty? (keys binds))
+        (str mark (get g :goal))
+        (str mark (get g :goal) "  {" (mod/explain-binds binds) "}")))))
+
+(define
+  mod/explain-evidence
+  (fn
+    (evidence)
+    (if
+      (empty? evidence)
+      "Evidence: (none)"
+      (str "Evidence: " (mod/join-with ", " evidence)))))
+
+(define
+  mod/explain
+  (fn
+    (decision)
+    (let
+      ((id (get decision :report-id))
+        (action (get decision :action))
+        (rule (get decision :rule))
+        (proof (get decision :proof)))
+      (let
+        ((goals (get proof :goals)) (evidence (get proof :evidence)))
+        (mod/join-with
+          "\n"
+          (append
+            (list
+              (str "Report " id ": " action " (rule: " rule ")")
+              (mod/explain-evidence evidence)
+              "Because:")
+            (map mod/explain-goal goals)))))))

lib/mod/scoreboard.json

@@ -1,14 +1,14 @@
 {
   "lang": "mod",
-  "total_passed": 154,
+  "total_passed": 164,
   "total_failed": 0,
-  "total": 154,
+  "total": 164,
   "suites": [
     {"name":"decide","passed":31,"failed":0,"total":31},
     {"name":"audit","passed":29,"failed":0,"total":29},
     {"name":"escalation","passed":46,"failed":0,"total":46},
     {"name":"fed","passed":26,"failed":0,"total":26},
-    {"name":"extensions","passed":22,"failed":0,"total":22}
+    {"name":"extensions","passed":32,"failed":0,"total":32}
   ],
-  "generated": "2026-06-06T18:02:25+00:00"
+  "generated": "2026-06-06T18:05:54+00:00"
 }

lib/mod/scoreboard.md

@@ -1,6 +1,6 @@
 # mod scoreboard
 
-**154 / 154 passing** (0 failure(s)).
+**164 / 164 passing** (0 failure(s)).
 
 | Suite | Passed | Total | Status |
 |-------|--------|-------|--------|
@@ -8,4 +8,4 @@
 | audit | 29 | 29 | ok |
 | escalation | 46 | 46 | ok |
 | fed | 26 | 26 | ok |
-| extensions | 22 | 22 | ok |
+| extensions | 32 | 32 | ok |

lib/mod/tests/extensions.sx

@@ -5,6 +5,7 @@
 ;; Ext 2: weighted/aggregate evidence scoring (:score-at-least) + report signals.
 ;;        Many low-confidence signals accumulate past a threshold via Prolog
 ;;        aggregate_all(sum(W), ...).
+;; Ext 3: human-readable proof explanation (mod/explain) over the proof tree.
 ;; Demonstrated with custom rule sets so the default policy (and its conformance
 ;; tests) stays untouched.
 
@@ -247,4 +248,66 @@
   (mod/cond->goal (list :score-at-least 5) "Id")
   "aggregate_all(sum(W), signal(Id, _, W), T), T >= 5")
 
+;; ── Ext 3: human-readable proof explanation ──
+
+(define mod-ext-spam-explain (mod/explain mod-ext-dec))
+
+(mod-ext-test!
+  "explain mentions the report id"
+  (mod/str-contains? mod-ext-spam-explain "Report p1")
+  true)
+(mod-ext-test!
+  "explain mentions the action"
+  (mod/str-contains? mod-ext-spam-explain "hide")
+  true)
+(mod-ext-test!
+  "explain mentions the rule"
+  (mod/str-contains? mod-ext-spam-explain "spam-unverified-hide")
+  true)
+(mod-ext-test!
+  "explain marks proved goals"
+  (mod/str-contains? mod-ext-spam-explain "[proved]")
+  true)
+(mod-ext-test!
+  "explain renders the evidence line"
+  (mod/str-contains? mod-ext-spam-explain "Evidence: spam")
+  true)
+
+;; count-rule explanation shows the unification bindings
+(define mod-ext-rep-r (mod/mk-report "rc" "ann" "dave" "off-topic"))
+(define
+  mod-ext-rep-d
+  (mod/decide-report
+    mod-ext-rep-r
+    (list mod-ext-rep-r mod-ext-rep-r mod-ext-rep-r)
+    mod/default-rules))
+(define mod-ext-rep-explain (mod/explain mod-ext-rep-d))
+(mod-ext-test!
+  "explain shows binding N=3"
+  (mod/str-contains? mod-ext-rep-explain "N=3")
+  true)
+(mod-ext-test!
+  "explain shows subject binding"
+  (mod/str-contains? mod-ext-rep-explain "dave")
+  true)
+
+;; explain-goal direct: unproved goal gets [unproved]
+(mod-ext-test!
+  "explain-goal marks unproved"
+  (mod/str-contains? (mod/explain-goal {:solved false :goal "attr(x, foo)" :bindings {}}) "[unproved]")
+  true)
+;; explain-binds renders key=value pairs
+(mod-ext-test!
+  "explain-binds renders pair"
+  (mod/explain-binds {:N "3"})
+  "N=3")
+;; no-evidence decision says (none)
+(define
+  mod-ext-keep-d
+  (mod/decide-report mod-ext-clean (list mod-ext-clean) mod-ext-rules))
+(mod-ext-test!
+  "explain (none) for empty evidence"
+  (mod/str-contains? (mod/explain mod-ext-keep-d) "Evidence: (none)")
+  true)
+
 (define mod-extensions-tests-run! (fn () {:failures mod-ext-failures :total mod-ext-count :passed mod-ext-pass :failed mod-ext-fail}))

plans/mod-on-sx.md

@@ -16,7 +16,7 @@ federation extension.
 
 ## Status (rolling)
 
-`bash lib/mod/conformance.sh` → **154/154** (roadmap done + extensions in progress)
+`bash lib/mod/conformance.sh` → **164/164** (roadmap done + extensions in progress)
 
 ## Ground rules
 
@@ -142,11 +142,20 @@ lib/mod/fed.sx
   `(:score-at-least N)` → `aggregate_all(sum(W), signal(Id, _, W), T), T >= N`.
   Many weak signals accumulate past a threshold — genuine Prolog arithmetic
   aggregation. Default policy untouched.
-- [ ] Ext 3 — human-readable proof explanation (render a decision's `:goals`)
+- [x] **Ext 3 — proof explanation** (`lib/mod/explain.sx`, +10). `mod/explain`
+  renders a decision into a readable "why": action + rule, evidence line, and the
+  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}`.
 - [ ] Ext 4 — report linking / dedup (relations between reports about one subject)
 
 ## Progress log
 
+- **Ext 3 — proof explanation, 164/164** (+10). `mod/explain` turns the Phase-2
+  proof tree into human-readable text — the audit trail's "why" made legible. Pure
+  SX over existing decision data; no engine change. Renders unification bindings
+  inline (`{B=ann, N=3, S=dave}`) so a moderator sees exactly which facts proved
+  the decision.
 - **Ext 2 — weighted/aggregate scoring, 154/154** (+8). `:signals` + the
   `(:score-at-least N)` condition push aggregation into Prolog
   (`aggregate_all(sum(W), …)`), so low-confidence signals can accumulate to a