audit: routing/rule-engine recon, Logtalk quarantine; Agda proofs re-checked under PROOF-POLICY §2.1

.github/workflows/agda-meta-checker.yml

@@ -98,10 +98,43 @@ jobs:
           echo "/tmp/agda-stdlib-2.1/standard-library.agda-lib" > ~/.agda/libraries
           echo "standard-library" > ~/.agda/defaults
 
-      - name: Type-check meta-checker
+      - name: Type-check meta-checker (PROOF-POLICY §2.1 canonical invocation)
         if: steps.detect.outputs.relevant == 'true'
         run: |
           cd meta-checker
           echo "$PWD/echidna-meta.agda-lib" >> ~/.agda/libraries
+          # Canonical invocation, PROOF-POLICY §2.1. --safe is what excludes
+          # postulates, --type-in-type and primTrustMe; it is not a grep.
+          # NEVER weaken these flags to get a green run: a failing leg is the
+          # finding. Note --cubical-compatible is NOT --cubical: the
+          # -W[no]UnsupportedIndexedMatch warnings this emits mean the flagged
+          # functions do not compute under transports. Recorded as a limit in
+          # docs/PROOF-STATUS.adoc R4.
           agda --safe --without-K --cubical-compatible src/Echidna/MetaChecker.agda
-          echo "✓ Meta-checker passed with safe / without-K / cubical-compatible; proof assumptions require a separate audit"
+
+      - name: Assert the checked closure covers every module
+        if: steps.detect.outputs.relevant == 'true'
+        run: |
+          cd meta-checker
+          # A module that nothing imports gets no interface and is never
+          # type-checked — AxiomTrackerCompleteness.agda sat outside the
+          # closure, and did not parse, until 2026-11-01. Check each source
+          # against *its own* interface rather than comparing totals: a count
+          # can be offset by a stray interface elsewhere, and a non-recursive
+          # glob misses nested modules.
+          # Agda writes interfaces under _build/<version>/agda/ when a
+          # .agda-lib is present, so mirroring the source path is
+          # version-dependent; match on module basename instead.
+          ifaces=$(find . -name '*.agdai' -type f | sed 's#.*/##; s#\.agdai$##' | sort -u)
+          missing=0
+          total=0
+          while IFS= read -r f; do
+            total=$((total + 1))
+            mod=$(basename "${f%.agda}")
+            if ! printf '%s\n' "$ifaces" | grep -qx "$mod"; then
+              echo "::error::$f produced no interface — module is outside the checked closure"
+              missing=$((missing + 1))
+            fi
+          done < <(find src -name '*.agda' | sort)
+          echo "${total} source modules, $((total - missing)) with interfaces"
+          test "$missing" -eq 0

.machine_readable/descriptiles/META.a2ml

@@ -28,9 +28,16 @@ primary = ["Rust", "Julia", "AffineScript", "Idris2", "Zig"]
 secondary = ["Chapel", "Bun", "Guix"]
 
 [interfaces]
-graphql = 8081
-grpc = 50051
-rest = 8000
+# Four listeners, four binaries (recon 2026-11-01; see
+# docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc §1).
+core-server = 8081      # `echidna server` (--port default); routes /api/*
+graphql = 8081          # `echidna-graphql`; POST / = GraphQL, GET / = playground.
+                        # Collides with core-server above. Default kept for
+                        # client compatibility; ECHIDNA_GRAPHQL_ADDR overrides.
+grpc = 50051            # `echidna-grpc`; IPv6 loopback only
+rest = 8000             # `echidna-rest`; /api/v1/* + /health (ECHIDNA_REST_ADDR)
+# standards 0-canon/PORT-REGISTRY.adoc: one port per project, no sharing. The
+# 8081 duplication is open debt (docs/DEBT.adoc D8), not an allocation.
 
 # ─────────────────────────────────────────────────────────────────────────────
 # Saturation campaign 2026-06-01 — additive surface declaration

.machine_readable/root-allow.txt

@@ -1,3 +1,4 @@
 .hypatia-ignore
 CLAUDE.md
 build/                     # build orchestration: guix.scm relocated here (canon 1.2.1 guix-primary template_ref = "build/")
+archive/                   # quarantine for dead sources (2026-11-01; Logtalk, see archive/logtalk/README.adoc)

.reuse/dep5

@@ -29,7 +29,7 @@ Files: src/*
  docs-site/*
  generated/*
  schemas/*
- rules/*
+ archive/*
  training_data/*
  deploy/*
  container/*

CLAUDE.md

@@ -16,6 +16,14 @@ Guidelines and context for working with Claude Code on the ECHIDNA project.
 - **Known debt (licence, docs, code)**: [`docs/DEBT.adoc`](docs/DEBT.adoc)
 - **Environment variables**: [`docs/ENV-VARS.adoc`](docs/ENV-VARS.adoc)
 - **RSR / CCCP compliance statement**: [`RSR_COMPLIANCE.adoc`](RSR_COMPLIANCE.adoc)
+- **Proof and verification policy (normative)**: `3-practice/PROOF-POLICY.adoc`
+  in [hyperpolymath/standards](https://github.com/hyperpolymath/standards) —
+  which prover carries which obligation (Rust→Creusot, Ada→SPARK,
+  APIs/ABIs→Idris 2, theory→Agda rechecked in Rocq and Lean), and the closed
+  status vocabulary (`proven`, `proven-with-postulates`, `tested-only`,
+  `argued`, `open`). A change to the mapping is an owner ruling and requires
+  this pointer to move in the same change.
+- **This repo's proof-status ledger**: [`docs/PROOF-STATUS.adoc`](docs/PROOF-STATUS.adoc)
 - **Receipts for README claims**: [`EXPLAINME.adoc`](EXPLAINME.adoc)
 - **Contributor guide**: [`.github/CONTRIBUTING.md`](.github/CONTRIBUTING.md)
 

QUICKSTART-USER.adoc

@@ -133,8 +133,23 @@ curl -X POST http://127.0.0.1:8081/api/prove \
 
 The full route table is in `src/rust/server.rs`. Separate
 GraphQL / gRPC / REST interface crates live under `src/interfaces/`
-on dedicated ports (8081 / 50051 / 8000 respectively); they share
-the same dispatch path.
+(gRPC 50051, REST 8000, GraphQL 8081). They are independent binaries, not
+one service on four ports: a GraphQL proof does not take the same path as
+`/api/prove` here. The dispatcher is reached by `/api/prove` (only in a
+`--features verisim` build) *and* by `/api/verify_parallel`, which calls
+`ProverDispatcher::verify_proof_parallel` unconditionally.
+
+Note that `echidna-graphql` also defaults to 8081, the same port as
+`echidna server` above — whichever starts second cannot bind. Run one or
+the other, or give GraphQL its own address:
+
+[source,bash]
+----
+ECHIDNA_GRAPHQL_ADDR=127.0.0.1:8082 cargo run -p echidna-graphql
+----
+
+See `docs/ARCHITECTURE.adoc` §"Client-facing surfaces, and what VeriSimDB
+is not" and `docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc`.
 
 For a no-build browser UI, open `src/ui/public/prove.html` directly
 and point the "API base" field at the running server.

README.adoc

@@ -190,10 +190,17 @@ outputs.
 dispatch, including a per-prover cwd/filename-override hook in
 `+tryProver+` so each backend can be invoked with its required workspace
 shape (Idris2 / Agda case studies in link:src/chapel/[`+src/chapel/+`]).
-* *Three API surfaces*:
+* *Three interface binaries*, alongside the core server:
 ** GraphQL (async-graphql, port 8081)
 ** gRPC (tonic + Protocol Buffers, port 50051)
 ** REST (axum + OpenAPI/ReDoc, port 8000)
+
+These are separate processes with separate route tables, not one service on
+four ports. The core `echidna server` is a fourth listener (`/api/*`, port
+8081 by default) and the GraphQL binary's default is the same 8081 — start
+one or set `ECHIDNA_GRAPHQL_ADDR`. See
+link:docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc[the routing
+recon].
 * *AffineScript / AffineScript UI*: AffineScript components are being
 ported to AffineScript-TEA as the stdlib primitives needed for the port
 (Http / Promise / Json / Dict) land in

archive/logtalk/README.adoc

@@ -0,0 +1,68 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 ECHIDNA Project Contributors
+
+= Quarantine: Logtalk sources
+
+*Status*: dead source, retained as a record. *Quarantined*: 2026-11-01.
+*Read this first*: nothing here is built, imported, tested or shipped.
+
+== Contents
+
+[width="100%",cols="38%,62%",options="header"]
+|===
+|File |Status
+
+|`+security_learning.lgt+`
+|DEAD. Was `+rules/security_learning.lgt+`, the only Logtalk module in the
+tree (234 lines, two objects, dated 2025-12-29). Body unchanged; a
+`+DEAD SOURCE+` header records the evidence.
+|===
+
+== Why it is here and not in `+rules/+`
+
+Four questions decided it, and each one alone would have been enough:
+
+. *Nothing loaded it.* No test, workflow, Justfile recipe, A2ML manifest or
+  Cargo build step named the file. `+grep -rn '\.lgt' --exclude-dir=.git .+`
+  returned it and one self-reference inside it. No Logtalk runtime is
+  installed in CI, and none is declared anywhere.
+. *Its input was a machine-local path.* `+cicd_repo_path('~/repos/cicd-hyper-a/.audittraining')+`
+  — a literal `+~+` in a path the module opens.
+. *Its learning step cannot learn.* `+load_training_data/1+` reads Prolog
+  terms with `+read/2+`, but the catalog it is pointed at is Scheme
+  (`+ERROR-CATALOG.scm+`). Every term reaches the catch-all clause
+  `+process_training_term(_)+`, so `+learn_rules/0+` re-asserts the static
+  tables already in the file. The output is a transcript of the input
+  constants.
+. *The estate moved.* Rule authoring is Elixir in
+  https://github.com/hyperpolymath/hypatia[hypatia]. ECHIDNA is a Hypatia
+  *target* (`.hypatia-baseline.json`, `.hypatia-ignore`), never a Logtalk
+  rule producer. The prose that described Logtalk generation was retired in
+  `+docs/ECOSYSTEM-INTEGRATION.adoc+` and
+  `+echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml+` in the
+  same change.
+
+`+rules/+` was removed rather than left empty, so that the tree cannot imply
+by its shape that ECHIDNA carries rules in Logtalk.
+
+The full audit, including the path classification and the reproduction
+commands, is
+link:../../docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc[`+docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc+`]
+§4.
+
+== What it would take to revive this
+
+Not a rename and not a wrapper. All five, or it stays dead:
+
+. A Logtalk or compatible Prolog runtime in CI, pinned the way every other
+   toolchain in this repo is pinned.
+. A parameterised input path — no `+~+`, no home directory.
+. A real parser for whatever format the catalog actually is, with a fixture
+   test per term shape.
+. A named consumer in this repository or a sibling, with a contract.
+. A reason not to write it in Elixir like the rest of the estate's rules.
+
+== Licence
+
+MPL-2.0, unchanged, per the `+SPDX-License-Identifier+` header in the file
+and the `+Files: archive/*+` stanza in `+.reuse/dep5+`.

rules/security_learning.lgt → archive/logtalk/security_learning.lgt

@@ -1,4 +1,28 @@
 %% SPDX-License-Identifier: MPL-2.0
+%%
+%% ===========================================================================
+%% DEAD SOURCE — quarantined 2026-11-01, body unchanged.
+%%
+%% This file was `rules/security_learning.lgt`, the only Logtalk module in the
+%% ECHIDNA tree. Nothing loaded it: no test, workflow, Justfile recipe, A2ML
+%% manifest or Cargo build step referenced it, and no Logtalk runtime is
+%% installed anywhere in CI. Its input path was a literal `~/repos/...` on one
+%% machine, and its "learning" step reads Prolog terms from a Scheme catalog
+%% (ERROR-CATALOG.scm), so every term falls through to the catch-all clause and
+%% the learned rules are a re-assertion of the static tables below.
+%%
+%% Estate rule authoring moved to Elixir rule modules in Hypatia. ECHIDNA is a
+%% Hypatia *target* (.hypatia-baseline.json, .hypatia-ignore), not a rule
+%% producer — the cicd-hyper-a alert taxonomy this file encodes is no longer
+%% the path by which ECHIDNA-side rules reach the estate.
+%%
+%% Kept rather than deleted so the record is byte-recoverable. Do not add to
+%% it, do not wire it up. Reviving it needs, at minimum: a runtime in CI, a
+%% parameterised input path, a real parser for the catalog format, and a
+%% consumer. See ./README.adoc and
+%% docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc §4.
+%% ===========================================================================
+%%
 %% ECHIDNA Security Rule Learning Module
 %% Learns security patterns from cicd-hyper-a audit data
 

container/Containerfile

@@ -12,7 +12,7 @@
 # =============================================================================
 # Stage 1: Builder
 # =============================================================================
 FROM cgr.dev/chainguard/wolfi-base:latest@sha256:9c2092b053779e14c82fb50f77b37bcc38b7d2c83972352d5813280f9d035b03 AS builder
 
 RUN apk add --no-cache \
     rust \
@@ -32,7 +32,7 @@
 # =============================================================================
 # Stage 2: Runtime
 # =============================================================================
 FROM cgr.dev/chainguard/wolfi-base:latest@sha256:9c2092b053779e14c82fb50f77b37bcc38b7d2c83972352d5813280f9d035b03
 
 LABEL org.opencontainers.image.title="ECHIDNA" \
       org.opencontainers.image.description="Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance" \
@@ -75,6 +75,6 @@
 EXPOSE 8081
 
 HEALTHCHECK --interval=30s --timeout=5s --start-period=10s --retries=3 \
-    CMD curl -sf http://localhost:${APP_PORT}/health || exit 1
+    CMD curl -sf http://localhost:${APP_PORT}/api/health || exit 1
 
 ENTRYPOINT ["/app/entrypoint.sh"]

container/compose.toml

@@ -24,7 +24,7 @@ environment = {
 }
 volumes = ["echidna-data:/data"]
 restart = "always"
-healthcheck = { test = "curl -sf http://localhost:8081/health", interval = "30s", timeout = "5s", retries = 3 }
+healthcheck = { test = "curl -sf http://localhost:8081/api/health", interval = "30s", timeout = "5s", retries = 3 }
 
 [services.svalinn]
 image = "ghcr.io/hyperpolymath/svalinn:latest.ctp"

container/deploy.k9.ncl

@@ -70,8 +70,10 @@ let deployment = {
   container = {
     image = "ghcr.io/hyperpolymath/echidna",
     port = 8081,
-    health_check = "/health",
-    readiness_check = "/ready",
+    # The core server serves /api/health; there is no separate /ready or
+    # bare /health route (see src/rust/server.rs), so both probes use it.
+    health_check = "/api/health",
+    readiness_check = "/api/health",
   },
   strategy = {
     type = "rolling",

container/entrypoint.sh

@@ -22,4 +22,6 @@ if [ -d "${APP_DATA_DIR:-/data}" ]; then
     fi
 fi
 
-exec /app/bin/echidna serve --host "${APP_HOST:-[::]}" --port "${APP_PORT:-8081}" "$@"
+# Subcommand is `server`, not `serve` (clap enum in src/rust/main.rs; there is
+# no alias). Fixing this on 2026-11-01 — every container start failed at exec.
+exec /app/bin/echidna server --host "${APP_HOST:-[::]}" --port "${APP_PORT:-8081}" "$@"

container/vordr.toml

@@ -7,11 +7,11 @@ name = "echidna"
 version = "1.5.0"
 
 [health]
-endpoint = "http://localhost:8081/health"
+endpoint = "http://localhost:8081/api/health"
 interval = "30s"
 timeout = "5s"
 failure_threshold = 3
-readiness_endpoint = "http://localhost:8081/ready"
+readiness_endpoint = "http://localhost:8081/api/health"
 readiness_timeout = "10s"
 on_failure = "alert"
 

docs/ARCHITECTURE.adoc

@@ -15,9 +15,13 @@ Two non-negotiable invariants govern every design choice:
 . *ML suggests; provers verify.* Neural components rank, route, and
 propose; formal provers carry the trust. A wrong suggestion is a wasted
 CPU cycle, not a wrong proof.
-. *Trust is checked, not asserted.* Solver binaries are SHAKE3-512 /
-BLAKE3 integrity-checked before invocation; certificates are
-independently reproduced where formats allow (Alethe, DRAT/LRAT, TSTP).
+. *Trust is checked, not asserted.* Certificates are independently
+reproduced where formats allow (Alethe, DRAT/LRAT, TSTP) — that part is
+real. Solver *identity* is not checked today: the integrity step exists,
+nothing in the tree attaches a checker, so binaries are currently
+_assumed_ rather than verified. See the Integrity caveat below and
+link:DEBT.adoc[`+DEBT+`] D9. Do not read this list as a guarantee that
+the binary you invoked is the binary you pinned.
 
 === Component map
 
@@ -31,8 +35,8 @@ independently reproduced where formats allow (Alethe, DRAT/LRAT, TSTP).
 │                       Rust Core  (src/rust/, crates/)                   │
 │                                                                         │
 │  ┌──────────┐  ┌──────────────┐  ┌────────────────┐  ┌──────────────┐  │
-│  │ CLI/REPL │  │ REST / GraphQL│  │ gRPC          │  │ FFI (Zig)    │  │
-│  │ (main.rs)│  │ (axum :8000)  │  │ (tonic :50051)│  │ (16 exports) │  │
+│  │ CLI/REPL │  │ REST          │  │ gRPC          │  │ FFI (Zig)    │  │
+│  │ (main.rs)│  │ (axum :8081)  │  │ (tonic :50051)│  │ (16 exports) │  │
 │  └────┬─────┘  └──────┬────────┘  └──────┬────────┘  └──────┬───────┘  │
 │       └────────────────┴──────────────────┴────────────────┘            │
 │                                  │                                       │
@@ -103,7 +107,14 @@ link:handover/TODO.adoc[`+handover/TODO.adoc+`] for current state):
 
 [arabic]
 . *Integrity* (`+integrity/+`) — solver binary SHAKE3-512 + BLAKE3
-against `+config/solver-manifest.toml+`.
+against `+config/solver-manifest.toml+`. *Caveat, 2026-11-01*: this step
+runs only when a checker is attached, and nothing in the tree calls
+`+with_integrity_checker+`; unconfigured, the pipeline treats integrity as
+passing (`+dispatch.rs:632+`). The manifest also still holds
+`+PLACEHOLDER_COMPUTE_ON_FIRST_RUN+` for every solver. Treat this step as
+*not executed* until it is wired; see
+link:reports/2026-11-01-routing-and-rule-engine-recon.adoc[`+docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc+`]
+§6 RD5.
 . *Dispatch* (`+dispatch.rs+`) — `+ProverDispatcher::select_prover+`
 picks the backend; under `+with_verisim+`, `+VeriSimAdvisor+` queries
 `+mv_prover_success_by_class+` for historical success-rate hints.
@@ -127,6 +138,49 @@ updates.
 `+with_verisim_writer+`) — fire-and-forget write to VeriSimDB
 `+proof_attempts+`, closes the learning loop.
 
+=== Client-facing surfaces, and what VeriSimDB is not
+
+There are *four independent listeners*, not one service on four ports. Each is
+a separate binary with its own route table and its own path to the provers:
+
+[width="100%",cols="30%,16%,54%",options="header",]
+|===
+|Listener |Default bind |Route root
+
+|`+echidna server+` |`+127.0.0.1:8081+` |`+/api/*+` — `/api/health`,
+`+/api/provers+`, `/api/prove`, `/api/verify`, `/api/session/*`, …
+|`+echidna-rest+` |`+127.0.0.1:8000+` |`+/api/v1/*+` plus root `+/health+`
+|`+echidna-graphql+` |`+127.0.0.1:8081+` |`+POST /+` (GraphQL), `+GET /+`
+(playground), `+/health+`
+|`+echidna-grpc+` |`+[::1]:50051+` |`+ProofService+` over `+echidna.proto+`
+|===
+
+`+echidna server+` and `+echidna-graphql+` share a default port; start only one
+without setting `+ECHIDNA_GRAPHQL_ADDR+`. The one-port-per-project rule is
+`+0-canon/PORT-REGISTRY.adoc+` in hyperpolymath/standards; the collision is
+open debt.
+
+*VeriSimDB is a persistence and learning adapter, not a communication path.*
+It sits behind the non-default `+verisim+` Cargo feature, is written to
+fire-and-forget after a dispatch, and is never consulted to reach a prover.
+Clients do not route through it, and *must not* need to: the estate's
+`+3-practice/PROOF-POLICY.adoc+` §2.2 states that ECHIDNA is "`the
+longer-term automation destination, not a prerequisite for current independent
+checks`". A mandatory VCL hop would violate that. Two consequences worth
+knowing before you deploy:
+
+* Enabling `+verisim+` also moves `+POST /api/prove+` onto `+ProverDispatcher+`
+  (`+server.rs:423+`); without it, `/api/prove` goes to the backend factory
+  directly. A storage feature should not decide the verification route.
+* `/api/verify` never enters the dispatcher at all, and `/api/verify_raw`
+  executes the solver binary directly by design.
+
+So "which pipeline ran" depends on the surface and the feature set. If a client
+needs a machine-readable answer it can trust, use `+echidna prove <file>
+--output json+` — the documented
+link:PROVE-RESULT-CONTRACT.adoc[`+echidna.prove.result/1+`] contract — rather
+than inferring it from an HTTP response body.
+
 === Polyglot source layout
 
 `+src/+` holds one subdirectory per language. The split is intentional —