From 6e825e1283a53a5e00051f3423369f7dd22d7cdd Mon Sep 17 00:00:00 2001 From: giles Date: Sat, 6 Jun 2026 17:37:02 +0000 Subject: [PATCH] =?UTF-8?q?mod:=20Phase=202=20=E2=80=94=20evidence=20accum?= =?UTF-8?q?ulation=20+=20proof=20trees=20+=20audit=20log,=2060/60?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reports carry an :evidence list, asserted as evidence/3 facts; reviewer-remove rule (highest precedence) lets human review override classification. Proof tree built constructively by re-querying each rule body goal against the same DB with the report id bound, so derivations carry real unification bindings. Append-only audit log records decision + proof + evidence snapshot per decide, monotonic seq, never mutates prior entries. +29 audit tests. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/mod/api.sx | 36 +++++++- lib/mod/audit.sx | 54 +++++++++++ lib/mod/conformance.conf | 2 + lib/mod/engine.sx | 27 +++++- lib/mod/policy.sx | 29 ++++-- lib/mod/schema.sx | 51 +++++++++-- lib/mod/scoreboard.json | 9 +- lib/mod/scoreboard.md | 3 +- lib/mod/tests/audit.sx | 187 +++++++++++++++++++++++++++++++++++++++ plans/mod-on-sx.md | 33 +++++-- 10 files changed, 400 insertions(+), 31 deletions(-) create mode 100644 lib/mod/audit.sx create mode 100644 lib/mod/tests/audit.sx diff --git a/lib/mod/api.sx b/lib/mod/api.sx index 929c39ea..88204426 100644 --- a/lib/mod/api.sx +++ b/lib/mod/api.sx @@ -1,8 +1,9 @@ ;; lib/mod/api.sx — report registry + public entry points. ;; ;; mod/report files a report (assigning a sequential id) into the in-memory -;; registry; mod/decide resolves an id and runs the policy engine against the -;; current registry and rule set. +;; registry; mod/add-evidence accumulates evidence onto a filed report; +;; mod/decide resolves an id, runs the policy engine against the current registry +;; and rule set, and commits the decision to the append-only audit log. (define mod/*reports* (list)) (define mod/*counter* 0) @@ -12,7 +13,10 @@ mod/reset! (fn () - (begin (set! mod/*reports* (list)) (set! mod/*counter* 0)))) + (begin + (set! mod/*reports* (list)) + (set! mod/*counter* 0) + (mod/audit-reset!)))) (define mod/report @@ -35,10 +39,34 @@ nil mod/*reports*))) +(define + mod/add-evidence + (fn + (id kind val) + (let + ((r (mod/get-report id))) + (if + (nil? r) + nil + (let + ((updated (mod/attach-evidence r (mod/mk-evidence kind val)))) + (begin + (set! + mod/*reports* + (map + (fn (x) (if (= (mod/report-id x) id) updated x)) + mod/*reports*)) + updated)))))) + (define mod/decide (fn (id) (let ((r (mod/get-report id))) - (if (nil? r) nil (mod/decide-report r mod/*reports* mod/*rules*))))) + (if + (nil? r) + nil + (let + ((d (mod/decide-report r mod/*reports* mod/*rules*))) + (begin (mod/log-decision! d (mod/report-evidence r)) d)))))) diff --git a/lib/mod/audit.sx b/lib/mod/audit.sx new file mode 100644 index 00000000..2cebc70e --- /dev/null +++ b/lib/mod/audit.sx @@ -0,0 +1,54 @@ +;; lib/mod/audit.sx — append-only decision log. +;; +;; Every decision the api commits is recorded as an immutable audit entry holding +;; the decision (action + matching rule), the proof tree (the derivation that +;; justified it), and a snapshot of the evidence in force at decision time. The +;; log is append-only: entries are never mutated or removed, only appended, each +;; with a monotonic sequence number. Retrieval is by report id (full history) or +;; by sequence. + +(define mod/*audit-log* (list)) +(define mod/*audit-seq* 0) + +(define + mod/audit-reset! + (fn + () + (begin (set! mod/*audit-log* (list)) (set! mod/*audit-seq* 0)))) + +(define mod/mk-audit-entry (fn (seq decision evidence-snapshot) {:action (get decision :action) :evidence evidence-snapshot :proof (get decision :proof) :rule (get decision :rule) :report-id (get decision :report-id) :seq seq})) + +(define + mod/log-decision! + (fn + (decision evidence-snapshot) + (begin + (set! mod/*audit-seq* (+ mod/*audit-seq* 1)) + (let + ((entry (mod/mk-audit-entry mod/*audit-seq* decision evidence-snapshot))) + (begin (append! mod/*audit-log* entry) entry))))) + +;; entries for one report, in chronological (sequence) order +(define + mod/audit + (fn + (id) + (reduce + (fn + (acc e) + (if (= (get e :report-id) id) (append acc (list e)) acc)) + (list) + mod/*audit-log*))) + +(define mod/audit-all (fn () mod/*audit-log*)) +(define mod/audit-count (fn () (len mod/*audit-log*))) + +;; most recent decision logged for a report (nil if none) +(define + mod/audit-latest + (fn + (id) + (reduce + (fn (acc e) (if (= (get e :report-id) id) e acc)) + nil + mod/*audit-log*))) diff --git a/lib/mod/conformance.conf b/lib/mod/conformance.conf index b2c0b751..7752fb8e 100644 --- a/lib/mod/conformance.conf +++ b/lib/mod/conformance.conf @@ -13,9 +13,11 @@ PRELOADS=( lib/mod/schema.sx lib/mod/policy.sx lib/mod/engine.sx + lib/mod/audit.sx lib/mod/api.sx ) SUITES=( "decide:lib/mod/tests/decide.sx:(mod-decide-tests-run!)" + "audit:lib/mod/tests/audit.sx:(mod-audit-tests-run!)" ) diff --git a/lib/mod/engine.sx b/lib/mod/engine.sx index 20e7de5b..866c0232 100644 --- a/lib/mod/engine.sx +++ b/lib/mod/engine.sx @@ -3,8 +3,12 @@ ;; build-program assembles the report's facts plus the compiled policy clauses; ;; decide-report runs the Prolog query and returns a decision. A decision is a ;; proof, not a bare keyword: it carries the matching rule, the conditions it -;; required, the evidence that satisfied them, and the report count — everything -;; Phase 2's audit trail needs to persist a "why". +;; required, the evidence that satisfied them, and a derivation — the proof tree. +;; +;; The proof tree is built constructively: for the matching rule, each body goal +;; is re-queried against the same DB with the report id bound, recording the goal +;; text, whether it was solved, and the bindings that satisfied it. That is a +;; genuine derivation drawn from the Prolog database, ready for the audit trail. (define mod/find-rule @@ -23,6 +27,21 @@ (r count rules) (str (mod/report-facts r count) "\n" (mod/rules->program rules)))) +(define + mod/proof-goals + (fn + (db id conds) + (if + (empty? conds) + (list {:solved true :goal "true" :bindings {}}) + (map + (fn + (c) + (let + ((g (mod/cond->goal c id))) + (let ((sols (pl-query-all db g))) {:solved (if (empty? sols) false true) :goal g :bindings (if (empty? sols) {} (first sols))}))) + conds)))) + (define mod/decide-report (fn @@ -39,7 +58,7 @@ ((sol (pl-query-one db (str "policy_action(" id ", Action, Rule)")))) (if (nil? sol) - {:action "keep" :proof {:evidence kinds :conditions (list) :rule "none" :count count} :report-id id :rule "none"} + {:action "keep" :proof {:goals (list) :evidence kinds :conditions (list) :rule "none" :count count} :report-id id :rule "none"} (let ((rname (dict-get sol "Rule"))) - (let ((rule (mod/find-rule rules rname))) {:action (mod/rule-action rule) :proof {:evidence kinds :conditions (mod/rule-when rule) :rule rname :count count} :report-id id :rule rname}))))))))) + (let ((rule (mod/find-rule rules rname))) {:action (mod/rule-action rule) :proof {:goals (mod/proof-goals db id (mod/rule-when rule)) :evidence kinds :conditions (mod/rule-when rule) :rule rname :count count} :report-id id :rule rname}))))))))) diff --git a/lib/mod/policy.sx b/lib/mod/policy.sx index 2649864e..4c3ab90c 100644 --- a/lib/mod/policy.sx +++ b/lib/mod/policy.sx @@ -5,6 +5,10 @@ ;; pl-query-one, so the first clause that proves wins. The final default rule has ;; an empty body (true) so every report yields at least :keep — "no rule matched" ;; is a real result, not a query failure. +;; +;; cond->goal takes an id-term so the same condition can be compiled with the +;; head variable "Id" (for clause bodies) or a concrete report id (for proof-tree +;; goal-by-goal re-querying in the engine). (define mod/mk-rule (fn (name action conds) {:when conds :name name :action action})) @@ -15,6 +19,9 @@ (define mod/default-rules (list + (mod/mk-rule + "reviewer-remove" + :remove (list (list :evidence "confirmed-abuse"))) (mod/mk-rule "spam-hide" :hide (list (list :classification "spam"))) (mod/mk-rule "abuse-remove" @@ -27,31 +34,41 @@ ;; ── condition → Prolog goal ── ;; ;; (:classification "spam") → classification(Id, spam) +;; (:evidence "kind") → evidence(Id, 'kind', _) ;; (:count-at-least 3) → report(Id, B, S), report_count(S, N), N >= 3 (define mod/cond->goal (fn - (c) + (c idterm) (let ((tag (first c))) (cond ((= tag :classification) - (str "classification(Id, " (nth c 1) ")")) + (str "classification(" idterm ", " (nth c 1) ")")) + ((= tag :evidence) + (str + "evidence(" + idterm + ", " + (mod/pl-quote (nth c 1)) + ", _)")) ((= tag :count-at-least) (str - "report(Id, B, S), report_count(S, N), N >= " + "report(" + idterm + ", B, S), report_count(S, N), N >= " (nth c 1))) (true "true"))))) (define mod/conds->body (fn - (conds) + (conds idterm) (if (empty? conds) "true" - (mod/join-with ", " (map mod/cond->goal conds))))) + (mod/join-with ", " (map (fn (c) (mod/cond->goal c idterm)) conds))))) (define mod/rule->clause @@ -63,7 +80,7 @@ ", '" (mod/rule-name r) "') :- " - (mod/conds->body (mod/rule-when r)) + (mod/conds->body (mod/rule-when r) "Id") "."))) (define diff --git a/lib/mod/schema.sx b/lib/mod/schema.sx index c675a583..5db13a1b 100644 --- a/lib/mod/schema.sx +++ b/lib/mod/schema.sx @@ -1,16 +1,34 @@ ;; lib/mod/schema.sx — report representation + Prolog fact generation. ;; -;; A report is a dict {:id :by :about :reason}. The engine derives evidence -;; (classification kinds) from the reason text, then projects the report and its -;; evidence into Prolog facts that policy clauses can match against. +;; A report is a dict {:id :by :about :reason :evidence}. :evidence is a list of +;; accumulated evidence entries {:kind :val} (human review, automated scanners, +;; etc.). The engine derives keyword classifications from the reason text and +;; projects the report, its classifications, and its accumulated evidence into +;; Prolog facts that policy clauses match against. -(define mod/mk-report (fn (id by about reason) {:id id :by by :about about :reason reason})) +(define mod/mk-report (fn (id by about reason) {:id id :by by :evidence (list) :about about :reason reason})) (define mod/report-id (fn (r) (get r :id))) (define mod/report-by (fn (r) (get r :by))) (define mod/report-about (fn (r) (get r :about))) (define mod/report-reason (fn (r) (get r :reason))) +(define + mod/report-evidence + (fn (r) (let ((e (get r :evidence))) (if (nil? e) (list) e)))) + +(define mod/mk-evidence (fn (kind val) {:val val :kind kind})) +(define mod/evidence-kind (fn (e) (get e :kind))) +(define mod/evidence-val (fn (e) (get e :val))) + +(define mod/with-evidence (fn (r evs) {:id (mod/report-id r) :by (mod/report-by r) :evidence evs :about (mod/report-about r) :reason (mod/report-reason r)})) + +(define + mod/attach-evidence + (fn + (r e) + (mod/with-evidence r (append (mod/report-evidence r) (list e))))) + ;; ── substring search (the prolog-loaded env lacks includes?; slice/len do work) ── (define @@ -102,6 +120,25 @@ "\n" (map (fn (k) (str "classification(" id ", " k ").")) kinds)))) +(define + mod/evidence-facts + (fn + (id evs) + (mod/join-with + "\n" + (map + (fn + (e) + (str + "evidence(" + id + ", " + (mod/pl-quote (mod/evidence-kind e)) + ", " + (mod/pl-quote (str (mod/evidence-val e))) + ").")) + evs)))) + (define mod/report-facts (fn @@ -111,10 +148,12 @@ (by (mod/pl-quote (mod/report-by r))) (about (mod/pl-quote (mod/report-about r)))) (let - ((cls (mod/classification-facts id (mod/classify-keywords r)))) + ((cls (mod/classification-facts id (mod/classify-keywords r))) + (evs (mod/evidence-facts id (mod/report-evidence r)))) (mod/join-with "\n" (list (str "report(" id ", " by ", " about ").") (str "report_count(" about ", " count ").") - cls)))))) + cls + evs)))))) diff --git a/lib/mod/scoreboard.json b/lib/mod/scoreboard.json index d4374712..ce3a15b8 100644 --- a/lib/mod/scoreboard.json +++ b/lib/mod/scoreboard.json @@ -1,10 +1,11 @@ { "lang": "mod", - "total_passed": 31, + "total_passed": 60, "total_failed": 0, - "total": 31, + "total": 60, "suites": [ - {"name":"decide","passed":31,"failed":0,"total":31} + {"name":"decide","passed":31,"failed":0,"total":31}, + {"name":"audit","passed":29,"failed":0,"total":29} ], - "generated": "2026-06-06T17:30:06+00:00" + "generated": "2026-06-06T17:36:32+00:00" } diff --git a/lib/mod/scoreboard.md b/lib/mod/scoreboard.md index 36d7bba3..83cd88b1 100644 --- a/lib/mod/scoreboard.md +++ b/lib/mod/scoreboard.md @@ -1,7 +1,8 @@ # mod scoreboard -**31 / 31 passing** (0 failure(s)). +**60 / 60 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| | decide | 31 | 31 | ok | +| audit | 29 | 29 | ok | diff --git a/lib/mod/tests/audit.sx b/lib/mod/tests/audit.sx new file mode 100644 index 00000000..f92b2c50 --- /dev/null +++ b/lib/mod/tests/audit.sx @@ -0,0 +1,187 @@ +;; lib/mod/tests/audit.sx — Phase 2: evidence accumulation + proof tree + audit. + +(define mod-aud-count 0) +(define mod-aud-pass 0) +(define mod-aud-fail 0) +(define mod-aud-failures (list)) + +(define + mod-aud-test! + (fn + (name got expected) + (begin + (set! mod-aud-count (+ mod-aud-count 1)) + (if + (= got expected) + (set! mod-aud-pass (+ mod-aud-pass 1)) + (begin + (set! mod-aud-fail (+ mod-aud-fail 1)) + (append! + mod-aud-failures + (str name "\n expected: " expected "\n got: " got))))))) + +(define + mod-aud-decide1 + (fn (r) (mod/decide-report r (list r) mod/default-rules))) + +;; ── proof tree: keyword classification ── + +(define + mod-aud-spam + (mod-aud-decide1 (mod/mk-report "r1" "alice" "bob" "this is spam"))) +(define mod-aud-spam-goals (get (get mod-aud-spam :proof) :goals)) + +(mod-aud-test! "spam proof has one goal" (len mod-aud-spam-goals) 1) +(mod-aud-test! + "spam proof goal text" + (get (first mod-aud-spam-goals) :goal) + "classification(r1, spam)") +(mod-aud-test! + "spam proof goal solved" + (get (first mod-aud-spam-goals) :solved) + true) + +;; ── proof tree: count rule with real bindings ── + +(define mod-aud-rep-r (mod/mk-report "r3" "ann" "dave" "x")) +(define + mod-aud-rep + (mod/decide-report + mod-aud-rep-r + (list mod-aud-rep-r mod-aud-rep-r mod-aud-rep-r) + mod/default-rules)) +(define mod-aud-rep-goals (get (get mod-aud-rep :proof) :goals)) +(define mod-aud-rep-binds (get (first mod-aud-rep-goals) :bindings)) + +(mod-aud-test! + "count proof goal solved" + (get (first mod-aud-rep-goals) :solved) + true) +(mod-aud-test! "count proof binding N" (dict-get mod-aud-rep-binds "N") "3") +(mod-aud-test! + "count proof binding S (subject)" + (dict-get mod-aud-rep-binds "S") + "dave") + +;; ── proof tree: default keep has a 'true' goal ── + +(define + mod-aud-keep + (mod-aud-decide1 (mod/mk-report "rk" "a" "b" "a fine post"))) +(define mod-aud-keep-goals (get (get mod-aud-keep :proof) :goals)) + +(mod-aud-test! + "keep proof goal text true" + (get (first mod-aud-keep-goals) :goal) + "true") +(mod-aud-test! + "keep proof goal solved" + (get (first mod-aud-keep-goals) :solved) + true) + +;; ── evidence accumulation drives a rule ── + +(define + mod-aud-rev-r + (mod/attach-evidence + (mod/mk-report "re" "a" "carol" "neutral") + (mod/mk-evidence "confirmed-abuse" "human"))) +(define mod-aud-rev (mod-aud-decide1 mod-aud-rev-r)) + +(mod-aud-test! + "evidence has length 1" + (len (mod/report-evidence mod-aud-rev-r)) + 1) +(mod-aud-test! + "evidence reviewer-remove → remove" + (get mod-aud-rev :action) + "remove") +(mod-aud-test! + "evidence reviewer-remove rule" + (get mod-aud-rev :rule) + "reviewer-remove") +(mod-aud-test! + "evidence proof goal solved" + (get (first (get (get mod-aud-rev :proof) :goals)) :solved) + true) +(mod-aud-test! + "no evidence → not reviewer-remove" + (get (mod-aud-decide1 (mod/mk-report "rn" "a" "b" "neutral")) :rule) + "default-keep") + +;; ── append-only audit log via the api ── + +(mod/reset!) +(mod/report "alice" "bob" "this is spam") +(mod/report "carol" "eve" "fine post") +(define mod-aud-d1 (mod/decide "r1")) +(define mod-aud-d2 (mod/decide "r2")) + +(mod-aud-test! "two decisions logged" (mod/audit-count) 2) +(mod-aud-test! + "first entry seq 1" + (get (first (mod/audit-all)) :seq) + 1) +(mod-aud-test! + "audit r1 returns one entry" + (len (mod/audit "r1")) + 1) +(mod-aud-test! + "audit r1 action matches decision" + (get (first (mod/audit "r1")) :action) + (get mod-aud-d1 :action)) +(mod-aud-test! + "audit r1 rule matches decision" + (get (first (mod/audit "r1")) :rule) + "spam-hide") +(mod-aud-test! + "audit r1 entry carries proof goals" + (len (get (get (first (mod/audit "r1")) :proof) :goals)) + 1) +(mod-aud-test! + "audit r2 keep" + (get (first (mod/audit "r2")) :action) + "keep") +(mod-aud-test! "audit unknown report → empty" (mod/audit "r99") (list)) + +;; ── append-only: re-deciding appends, never mutates ── + +(define mod-aud-d1b (mod/decide "r1")) + +(mod-aud-test! "re-decide appends (count 3)" (mod/audit-count) 3) +(mod-aud-test! + "audit r1 now has 2 entries" + (len (mod/audit "r1")) + 2) +(mod-aud-test! + "audit r1 seqs monotonic" + (get (nth (mod/audit "r1") 1) :seq) + 3) +(mod-aud-test! + "audit-latest r1 is seq 3" + (get (mod/audit-latest "r1") :seq) + 3) +(mod-aud-test! + "first r1 entry unchanged (still seq 1)" + (get (first (mod/audit "r1")) :seq) + 1) + +;; ── evidence snapshot captured at decision time ── + +(mod/add-evidence "r2" "confirmed-abuse" "human") +(define mod-aud-d2b (mod/decide "r2")) + +(mod-aud-test! + "post-evidence decision flips to remove" + (get mod-aud-d2b :action) + "remove") +(mod-aud-test! + "audit snapshot records evidence kind" + (mod/evidence-kind (first (get (mod/audit-latest "r2") :evidence))) + "confirmed-abuse") +(mod-aud-test! + "earlier r2 entry had empty evidence snapshot" + (len (get (first (mod/audit "r2")) :evidence)) + 0) + +(define mod-audit-tests-run! (fn () {:failures mod-aud-failures :total mod-aud-count :passed mod-aud-pass :failed mod-aud-fail})) diff --git a/plans/mod-on-sx.md b/plans/mod-on-sx.md index 9f03ed8b..2128b4c2 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` → **31/31** (Phase 1 complete) +`bash lib/mod/conformance.sh` → **60/60** (Phases 1–2 complete) ## Ground rules @@ -82,11 +82,17 @@ lib/mod/fed.sx ## Phase 2 — Evidence + audit trail -- [ ] evidence accumulation — additional facts asserted before query -- [ ] proof tree from Prolog derivation tree -- [ ] `lib/mod/audit.sx` — append-only log (decision + proof + evidence snapshot) -- [ ] `(mod/audit id)` retrieval -- [ ] `lib/mod/tests/audit.sx` — proof correctness, trail completeness +- [x] evidence accumulation — `report :evidence` list; `mod/attach-evidence` + + api `mod/add-evidence`; asserted as `evidence(Id, 'kind', 'val')` facts; + new `:evidence` condition + `reviewer-remove` rule consume it +- [x] proof tree from Prolog derivation — `mod/proof-goals` re-queries each body + goal (id bound) against the same DB, recording goal text, solved?, and the + bindings that satisfied it (e.g. count goal yields N=3, S=subject) +- [x] `lib/mod/audit.sx` — append-only log: monotonic `:seq`, decision + proof + + evidence snapshot; never mutates prior entries +- [x] `(mod/audit id)` retrieval (+ `mod/audit-latest`, `mod/audit-all`, count) +- [x] `lib/mod/tests/audit.sx` — 29 cases: proof goal text/bindings, evidence-driven + decisions, append-only ordering, per-report retrieval, snapshot-at-decision-time ## Phase 3 — Escalation + lifecycle state machine @@ -107,6 +113,21 @@ lib/mod/fed.sx ## Progress log +- **Phase 2 complete — 60/60** (+29 audit). Evidence accumulation, constructive + proof trees, append-only audit log. A decision's `:proof :goals` is a real + derivation: each body goal is re-queried against the same Prolog DB with the + report id bound, so the count rule's proof carries `N=3, S=` straight + from unification — not a reconstruction. Evidence is asserted as + `evidence(Id, 'kind', 'val')`; the new `reviewer-remove` rule (placed first = + highest precedence) lets human review override automated classification. + `mod/decide` now commits each decision to the audit log with the evidence + snapshot in force at decision time. Unknown predicates in this Prolog fail + gracefully (verified) — so an evidence-less report safely falls through the + reviewer rule without an existence error. + - **Liftable (acl-sx watch):** the proof-tree builder (`mod/proof-goals` — + re-query-each-goal) and the append-only log shape are both generic. Both + subsystems are now past Phase 2; next time either touches plumbing, evaluate + lifting `proof-goals` + the audit-log primitives into `lib/guest/`. - **Phase 1 complete — 31/31.** Report schema, keyword classifier, policy DSL, engine, registry api, conformance harness. Decisions are proofs: each carries `:rule` (matching clause), `:proof {:rule :conditions :evidence :count}`.