From 102c806451aa1cdae976cfb76e617e15d1007b2b Mon Sep 17 00:00:00 2001 From: giles Date: Sat, 6 Jun 2026 18:06:29 +0000 Subject: [PATCH] =?UTF-8?q?mod:=20Ext=203=20=E2=80=94=20human-readable=20p?= =?UTF-8?q?roof=20explanation=20(mod/explain),=20164/164?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- lib/mod/conformance.conf | 1 + lib/mod/explain.sx | 55 ++++++++++++++++++++++++++++++++ lib/mod/scoreboard.json | 8 ++--- lib/mod/scoreboard.md | 4 +-- lib/mod/tests/extensions.sx | 63 +++++++++++++++++++++++++++++++++++++ plans/mod-on-sx.md | 13 ++++++-- 6 files changed, 136 insertions(+), 8 deletions(-) create mode 100644 lib/mod/explain.sx diff --git a/lib/mod/conformance.conf b/lib/mod/conformance.conf index c99cb992..53926a76 100644 --- a/lib/mod/conformance.conf +++ b/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 diff --git a/lib/mod/explain.sx b/lib/mod/explain.sx new file mode 100644 index 00000000..6a210393 --- /dev/null +++ b/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))))))) diff --git a/lib/mod/scoreboard.json b/lib/mod/scoreboard.json index d8930e4f..5c1d8a77 100644 --- a/lib/mod/scoreboard.json +++ b/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" } diff --git a/lib/mod/scoreboard.md b/lib/mod/scoreboard.md index 353b11ca..02db4f60 100644 --- a/lib/mod/scoreboard.md +++ b/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 | diff --git a/lib/mod/tests/extensions.sx b/lib/mod/tests/extensions.sx index 46090632..cafd11ba 100644 --- a/lib/mod/tests/extensions.sx +++ b/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})) diff --git a/plans/mod-on-sx.md b/plans/mod-on-sx.md index f7c9c690..fbe820ef 100644 --- a/plans/mod-on-sx.md +++ b/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