mod: Phase 2 — evidence accumulation + proof trees + audit log, 60/60

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) <noreply@anthropic.com>

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=<subject>` 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}`.