acl: Phase 3 explanation + audit, 35 tests

explain.sx reconstructs a canonical proof tree (first-rule, first-solution)
by goal-directed search over the saturated db, since Datalog keeps no
provenance; depth-capped for cyclic safety. acl-explain returns
{:allowed? :proof :reason} with the blocking eff_deny proof on denial.
audit.sx is an append-only decision log (monotonic seq, disk serializer).
api gains acl/explain, acl/audit, acl/audit-tail.

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

plans/acl-on-sx.md

@@ -15,7 +15,7 @@ and federation extension. Reuses `lib/datalog/` evaluator and term model where p
 
 ## Status (rolling)
 
-`bash lib/acl/conformance.sh` → **54/54** (Phases 1-2 complete)
+`bash lib/acl/conformance.sh` → **89/89** (Phases 1-3 complete)
 
 ## Ground rules
 
@@ -98,11 +98,27 @@ cyclic membership/containment reaches a fixpoint rather than looping (tested).
 
 ## Phase 3 — Explanation + audit
 
-- [ ] `(acl/explain subj act res)` → `{:allowed? T :proof <tree>}`
-- [ ] proof tree extracts from Datalog's derivation
-- [ ] `lib/acl/audit.sx` — append-only decision log (in-memory + serializer for disk)
-- [ ] `(acl/audit-tail n)` for recent decisions
-- [ ] `lib/acl/tests/explain.sx` — proof correctness, audit completeness
+- [x] `(acl/explain subj act res)` → `{:allowed? T :proof <tree>}`
+- [x] proof tree extracts from Datalog's derivation
+- [x] `lib/acl/audit.sx` — append-only decision log (in-memory + serializer for disk)
+- [x] `(acl/audit-tail n)` for recent decisions
+- [x] `lib/acl/tests/explain.sx` — proof correctness, audit completeness
+
+### proof reconstruction (the choice)
+
+`lib/datalog/` records derived facts but not provenance, so `lib/acl/explain.sx`
+reconstructs the proof by goal-directed search over the *saturated* db: for a
+ground goal, find the first ACL rule (in `acl-rules` order) whose body holds,
+take the first `dl-query` solution binding the rest, recurse on each body
+literal; negated literals become verified `:neg-ok` leaves. The Datalog
+derivation graph is a DAG (a fact may hold many ways) — we pick ONE **canonical
+proof: first-rule, first-solution**, with EDB/direct rules ordered first so
+proofs bottom out quickly. A depth cap (64) guards pathological cyclic data.
+`acl-explain` returns `{:allowed? :proof :reason}`; on denial `:reason` carries
+the blocking `eff_deny` proof (explicit or inherited) when one exists, else nil
+(no grant). Audit log is append-only with monotonic seq numbers (no wall-clock,
+for determinism); `acl-audit-decide!` is the logged path, `acl-permit?` stays
+pure.
 
 ## Phase 4 — Federation
 
@@ -149,11 +165,23 @@ cyclic membership/containment reaches a fixpoint rather than looping (tested).
     ACL-specific (group/resource/role vocabulary); mod-sx will have its own. So
     the `lib/guest/rules/` extraction stays at the build/decide level, not the
     ruleset level.
+- **Phase 3 complete (89/89, +35 explain).** Added `explain.sx` (proof
+  reconstruction, see policy section above), `audit.sx` (append-only log), and
+  extended `api.sx` with `acl/explain`/`acl/audit`/`acl/audit-tail`. No engine
+  changes — explanation reads the same saturated db the decision uses.
+  - **Substrate gotcha:** the host `=` compares symbols by interned identity,
+    which is *unstable* across `dl-query` saturation/substitution within a
+    single image — the same two structurally-equal symbol-lists compared `=`
+    true once and false moments later in the REPL. Conformance runs in a fresh
+    process per suite so it's deterministic there, but test assertions now use a
+    name-based `acl-et-eq?` (compare symbols via `symbol->string`), matching the
+    datalog suite's `dl-api-deep=?` convention. Worth flagging to the kernel
+    owners but out of acl scope.
   - **Tooling note:** sx-tree path-based edit tools (`sx_replace_node`,
     `sx_read_subtree` with a path) ignored the path argument in this worktree
-    (always resolved to index 0 / `[0,..]`). `sx_write_file`, `sx_validate`,
-    `sx_find_all`, `sx_eval` all work; used full-file rewrites instead of path
-    edits.
+    (always resolved to index 0 / `[0,..]`), in BOTH `(a b c)` and `(a,b,c)`
+    forms. `sx_write_file`, `sx_validate`, `sx_find_all`, `sx_summarise`,
+    `sx_eval` all work; used full-file rewrites instead of path edits throughout.
 
 ## Blockers