From df5e041a469e8edb3e98caa324f78e8abc250b17 Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 1 Nov 2026 17:06:30 +0000 Subject: [PATCH 1/5] proof: canonical-flag receipt, three new Agda modules, repair an unchecked module MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PROOF-POLICY §2.1 canonical invocation now runs and passes: agda --safe --without-K --cubical-compatible src/Echidna/MetaChecker.agda exit 0, 98s cold, 9 modules + 214 stdlib modules, 0 postulates, 53 -W[no]UnsupportedIndexedMatch warnings at 5 sites. Recorded as a limit (--cubical-compatible is not --cubical; --cubical fails inside stdlib 2.1). - AxiomTrackerCompleteness.agda was outside every gate and did not parse. Fixed (Data.Sum import; clean-left-neutral; new worst-ub-right) and wired into MetaChecker. CI now fails if any module yields no interface. - New: Integrity.agda (E11; proves the invariant dispatch.rs 642/848/998 and solver_integrity.rs 359 violate), ClampTrust.agda (ClampTrustBounds rewrite), Receipt.agda (receipt vs warrant, from epistemic-types@5422cd5). - meta-checker flags in CI; PROOF-STATUS R4 argued->proven plus R9-R11; PROOF-NEEDS + report §10; D9 cross-reference. Grade unchanged at Mathesis Grade 3: no Rocq/Lean leg ran (no reachable release host), so R5 stays open and no leg is reported as passing. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/agda-meta-checker.yml | 30 +- .machine_readable/descriptiles/META.a2ml | 13 +- .machine_readable/root-allow.txt | 1 + .reuse/dep5 | 2 +- CLAUDE.md | 8 + QUICKSTART-USER.adoc | 18 +- README.adoc | 9 +- archive/logtalk/README.adoc | 68 ++ .../logtalk}/security_learning.lgt | 24 + container/compose.toml | 2 +- container/entrypoint.sh | 4 +- container/vordr.toml | 4 +- docs/ARCHITECTURE.adoc | 56 +- docs/DEBT.adoc | 123 +++ docs/ECOSYSTEM-INTEGRATION.adoc | 13 +- docs/ENV-VARS.adoc | 27 + docs/PROOF-NEEDS.adoc | 64 ++ docs/PROOF-STATUS.adoc | 350 ++++++ ...6-11-01-routing-and-rule-engine-recon.adoc | 992 ++++++++++++++++++ .../descriptiles/NEUROSYM.a2ml | 7 +- meta-checker/src/Echidna/AxiomSafety.agda | 31 + .../src/Echidna/AxiomTrackerCompleteness.agda | 37 +- meta-checker/src/Echidna/ClampTrust.agda | 149 +++ meta-checker/src/Echidna/Integrity.agda | 137 +++ meta-checker/src/Echidna/MetaChecker.agda | 60 +- meta-checker/src/Echidna/Receipt.agda | 168 +++ scripts/install-proof-toolchains.sh | 21 + site/docs/api/graphql.adoc | 20 +- site/docs/index.adoc | 9 +- src/interfaces/graphql/main.rs | 12 +- 30 files changed, 2397 insertions(+), 62 deletions(-) create mode 100644 archive/logtalk/README.adoc rename {rules => archive/logtalk}/security_learning.lgt (86%) create mode 100644 docs/PROOF-STATUS.adoc create mode 100644 docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc create mode 100644 meta-checker/src/Echidna/ClampTrust.agda create mode 100644 meta-checker/src/Echidna/Integrity.agda create mode 100644 meta-checker/src/Echidna/Receipt.agda diff --git a/.github/workflows/agda-meta-checker.yml b/.github/workflows/agda-meta-checker.yml index 8ecd16d3..774186e8 100644 --- a/.github/workflows/agda-meta-checker.yml +++ b/.github/workflows/agda-meta-checker.yml @@ -98,10 +98,34 @@ 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 - agda src/Echidna/MetaChecker.agda - echo "✓ All 30+ properties machine-verified" + # 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 + + - 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. Guard against a + # repeat: every source module must yield an interface. + src=$(ls src/Echidna/*.agda | wc -l) + iface=$(find . -name '*.agdai' | wc -l) + echo "source modules: $src, interfaces produced: $iface" + if [ "$src" -ne "$iface" ]; then + echo "::error::${src} modules but ${iface} interfaces — at least one module is outside the checked closure" + ls -1 src/Echidna/*.agda + exit 1 + fi + echo "✓ ${iface} modules type-checked under the PROOF-POLICY §2.1 flags" diff --git a/.machine_readable/descriptiles/META.a2ml b/.machine_readable/descriptiles/META.a2ml index 9efc42ba..35e25613 100644 --- a/.machine_readable/descriptiles/META.a2ml +++ b/.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 diff --git a/.machine_readable/root-allow.txt b/.machine_readable/root-allow.txt index efa51790..4b2d27da 100644 --- a/.machine_readable/root-allow.txt +++ b/.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) diff --git a/.reuse/dep5 b/.reuse/dep5 index 25638635..2cd4af30 100644 --- a/.reuse/dep5 +++ b/.reuse/dep5 @@ -29,7 +29,7 @@ Files: src/* docs-site/* generated/* schemas/* - rules/* + archive/* training_data/* deploy/* container/* diff --git a/CLAUDE.md b/CLAUDE.md index 3919d823..faeb9acc 100644 --- a/CLAUDE.md +++ b/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) diff --git a/QUICKSTART-USER.adoc b/QUICKSTART-USER.adoc index 093bf0b2..ccc4378e 100644 --- a/QUICKSTART-USER.adoc +++ b/QUICKSTART-USER.adoc @@ -133,8 +133,22 @@ 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, and the trust pipeline is reached only by `/api/prove` +in a `--features verisim` build. + +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. diff --git a/README.adoc b/README.adoc index 7e2be590..70e04deb 100644 --- a/README.adoc +++ b/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 diff --git a/archive/logtalk/README.adoc b/archive/logtalk/README.adoc new file mode 100644 index 00000000..5f459dc2 --- /dev/null +++ b/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+`. diff --git a/rules/security_learning.lgt b/archive/logtalk/security_learning.lgt similarity index 86% rename from rules/security_learning.lgt rename to archive/logtalk/security_learning.lgt index 86f0250f..baa21052 100644 --- a/rules/security_learning.lgt +++ b/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 diff --git a/container/compose.toml b/container/compose.toml index 4d3880ab..572f0d49 100644 --- a/container/compose.toml +++ b/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" diff --git a/container/entrypoint.sh b/container/entrypoint.sh index 1ea43dd8..8886c820 100755 --- a/container/entrypoint.sh +++ b/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}" "$@" diff --git a/container/vordr.toml b/container/vordr.toml index d336e420..deeb4345 100644 --- a/container/vordr.toml +++ b/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" diff --git a/docs/ARCHITECTURE.adoc b/docs/ARCHITECTURE.adoc index 58afe77c..1e95eebb 100644 --- a/docs/ARCHITECTURE.adoc +++ b/docs/ARCHITECTURE.adoc @@ -31,8 +31,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 +103,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 +134,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 +--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 — diff --git a/docs/DEBT.adoc b/docs/DEBT.adoc index 545a0841..82daa8fe 100644 --- a/docs/DEBT.adoc +++ b/docs/DEBT.adoc @@ -421,6 +421,129 @@ git grep -cE 'todo!\(\)|unimplemented!\(\)' -- '*.rs' | awk -F: '{s+=$2} END{pri ''''' +=== Routing and verification claims (recon 2026-11-01) + +Source: +link:reports/2026-11-01-routing-and-rule-engine-recon.adoc[`+docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc+`]. +Entries here are the ones that outlive that report. + +==== D8. Core server and GraphQL interface both default to port 8081 + +*P1.* Two binaries, one default port. `+echidna server+` takes `+--port+` +default 8081; `+echidna-graphql+` hard-coded 8081 +(`+src/interfaces/graphql/main.rs+`). Whichever starts second fails to bind. + +This is not merely untidy: `0-canon/PORT-REGISTRY.adoc` in +hyperpolymath/standards states "Every project MUST use a unique port. No two +projects share a port." + +Fixed so far: `+ECHIDNA_GRAPHQL_ADDR+` override (default unchanged, so no +client breaks) and corrections to `+QUICKSTART-USER.adoc+`, `+README.adoc+`, +`+docs/ARCHITECTURE.adoc+`, `+site/docs/index.adoc+`, +`+site/docs/api/graphql.adoc+` and `+.machine_readable/descriptiles/META.a2ml+`, +which variously omitted the core server or claimed the three interfaces sat +"on dedicated ports". + +Open: the default itself. Moving it needs a release note, since anything +pinned to 8081 keeps working only while the two are not co-resident. + +[source,bash] +---- +grep -n 'default_value = "8081"' src/rust/main.rs +grep -n 'ECHIDNA_GRAPHQL_ADDR' src/interfaces/graphql/main.rs +---- + +==== D9. Solver integrity is documented as enforced and is not enforced + +*P1.* `+docs/ARCHITECTURE.adoc+` and the published site listed solver binary +integrity as step 1 of the trust pipeline. The check is conditional +(`+dispatch.rs:632+`): with no checker attached, `+solver_integrity_ok` is +`true`. `+with_integrity_checker+` has no caller in the tree, and +`+config/solver-manifest.toml+` holds `+PLACEHOLDER_COMPUTE_ON_FIRST_RUN+` for +every solver, so attaching one today would report `+Uninitialized+` — which the +code also treats as passing. + +Fixed so far: the docs and the published site now say "capability present, not +currently engaged" instead of claiming a step that does not run. + +Now machine-checked on the specification side: +`+meta-checker/src/Echidna/Integrity.agda+` (`+docs/PROOF-STATUS.adoc+` R9) +proves that verification requires an initialised manifest and that an +uninitialised manifest never verifies — with collision resistance carried as an +explicit hypothesis, and a sharpness result showing that hypothesis cannot be +dropped. The accepting call sites are `+dispatch.rs+` 642, 848, 998 and +`+solver_integrity.rs+` 359. So the divergence is checked on one side and read on +the other, rather than read on both: closing D9 means changing those four lines, +not the proof. + +Open: decide whether to wire it (introducing a refuse-on-mismatch failure mode) +or to delete the step from the pipeline description. Recorded rather than +silently changed. + +[source,bash] +---- +grep -rn 'with_integrity_checker' src/ crates/ tests/ # definition only +grep -n 'PLACEHOLDER' config/solver-manifest.toml +---- + +==== D10. `+--features verisim+` changes verification routing, not just storage + +*P1.* `+POST /api/prove+` compiles two ways: through `+ProverDispatcher+` with +the feature, straight to the backend factory without it (`+server.rs:423+`). +A persistence flag therefore decides whether an HTTP proof is arbitrated, and +no response field distinguishes the two. + +Open: build the dispatcher unconditionally and make `+with_verisim_writer+` +purely additive. Not done here because it changes what a default build +returns — it needs a decision record. + +[source,bash] +---- +sed -n '420,450p' src/rust/server.rs +---- + +==== D11. `+echidna-mcp+` calls a subcommand that does not exist + +*P2.* `+crates/echidna-mcp/src/main.rs+` runs `+echidna check-prover +`; +`+Commands+` has no such variant, so the tool fails with a usage error every +time. Its `+prove+` tool also uses the legacy `+--format json+` dialect +(`+{"level":"success"}+`) instead of the `+--output json+` prove contract. + +Open: needs either a `+check-prover+` subcommand or a `/api/provers` probe, plus +a rewrite onto the contract. Feature decision. + +[source,bash] +---- +grep -n 'check-prover' crates/echidna-mcp/src/main.rs # one call site +grep -n 'CheckProver\|check-prover' src/rust/main.rs # expect empty +---- + +==== D12. `+docs-site/+` is unbuilt and its API pages are wrong + +*P2.* Nothing builds or deploys `+docs-site/+`: `+pages.yml+` publishes +`+site/+` through Ddraig. Its pages still claim a `+/graphql+` endpoint and a +`+/playground+` (the binary serves both at `+/+`), "30 supported prover +backends", and a `+localhost:8000/api/v1+` base. + +Open: delete the tree or regenerate it from `+site/docs/+`. Left in place here +because removing a documentation tree is an owner decision, not a cleanup. + +==== Fixed en route (recorded so they are not re-triaged) + +* `+container/entrypoint.sh+` executed `+echidna serve+`; the subcommand is + `+server+`. Every container start failed at `+exec+`. +* `+container/compose.toml+` healthcheck probed `+/health+` and + `+container/vordr.toml+` probed `+/health+` and `+/ready+`; the core server + serves `+/api/health+` and never had `+/ready+`. +* `+rules/security_learning.lgt+` was dead Logtalk, loaded by nothing; + quarantined to `+archive/logtalk/+` with a `+DEAD SOURCE+` header. See that + directory's README. +* `+docs/ECOSYSTEM-INTEGRATION.adoc+` and + `+echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml+` claimed + Hypatia emits Logtalk rules. It emits Elixir rules. + +''''' + === Already tracked as issues Open issues covering debt not duplicated above: diff --git a/docs/ECOSYSTEM-INTEGRATION.adoc b/docs/ECOSYSTEM-INTEGRATION.adoc index 80eefd23..00ae7aa1 100644 --- a/docs/ECOSYSTEM-INTEGRATION.adoc +++ b/docs/ECOSYSTEM-INTEGRATION.adoc @@ -114,8 +114,17 @@ cross-repo dispatch *How It Works*: 1. Fleet-coordinator runs Hypatia scanner on repos 2. Hypatia generates findings in shared context 3. Learning engine observes -patterns (unsafe_panic, eval_usage, etc.) 4. Auto-generates Logtalk -rules after 5+ observations 5. Proposes new detection rules via PRs +patterns (unsafe_panic, eval_usage, etc.) 4. Emits Elixir rule modules +after 5+ observations 5. Proposes new detection rules via PRs + +*Correction (2026-11-01)*: this step previously said "Auto-generates +Logtalk rules". Hypatia's rule engine is Elixir, and ECHIDNA is a Hypatia +*target* — `.hypatia-baseline.json` and `.hypatia-ignore` — not a Logtalk +rule producer. The one Logtalk module that ever lived here +(`rules/security_learning.lgt`) was loaded by nothing and is quarantined at +`archive/logtalk/`. See +link:reports/2026-11-01-routing-and-rule-engine-recon.adoc[`+docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc+`] +§4. *Command*: diff --git a/docs/ENV-VARS.adoc b/docs/ENV-VARS.adoc index 62013464..e2714cc3 100644 --- a/docs/ENV-VARS.adoc +++ b/docs/ENV-VARS.adoc @@ -26,6 +26,33 @@ surfaces using `+VERISIMDB_URL+` are stale and being migrated. separate from the ML server only when the GNN runs on a different host. |=== +=== Interface listeners + +Each listener is a separate binary. Two of them default to the same port; see +link:reports/2026-11-01-routing-and-rule-engine-recon.adoc[`+docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc+`] +§6 RD2 and `+0-canon/PORT-REGISTRY.adoc+`. + +[width="100%",cols="20%,20%,20%,20%,20%",options="header",] +|=== +|Variable |Type |Default |Used by |Purpose +|`+ECHIDNA_REST_ADDR+` |host:port |`+127.0.0.1:8000+` +|`+src/interfaces/rest/main.rs:142+` |Bind address for the `+echidna-rest+` +binary (`+/api/v1/*+`). Not the core server. + +|`+ECHIDNA_GRAPHQL_ADDR+` |host:port |`+127.0.0.1:8081+` +|`+src/interfaces/graphql/main.rs+` |Bind address for `+echidna-graphql+`. +Same default as the core server's `+--port+`, so set this when running both. + +|`+--port+` / `+--host+` (CLI flags, not env) +|host:port |`+127.0.0.1:8081+` +|`+src/rust/main.rs+` |Bind address for `+echidna server+`. There is no +environment override for this one. + +|`+APP_PORT+` / `+APP_HOST+` |host:port |`+[::]` / `+8081+` +|`+container/entrypoint.sh+` |Read by the container entrypoint and passed to +`+echidna server+` as flags. The binary itself does not read them. +|=== + === Training & evaluation (Julia) [width="100%",cols="20%,20%,20%,20%,20%",options="header",] diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index a9143ac5..d09809af 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -296,3 +296,67 @@ representation / transport* (encoding shapes for Http / Promise / JSON / Dict). It carries no L3 obligation (no claim about fibre structure of the wire transport), so audit-and-not-relevant applies. Recorded here so a future port reviewer does not need to re-audit. + +=== Proof updating, 2026-11-01 + +First session in which the Agda corpus was type-checked under the +`+PROOF-POLICY+` §2.1 canonical invocation +(`--safe --without-K --cubical-compatible`) rather than plain `agda`. Receipt: +exit 0, 98 s cold, 9 modules, 214 stdlib modules, 53 warnings all of one class. +Status ledger: `+docs/PROOF-STATUS.adoc+` R4, R9, R10, R11. + +==== What changed + +[width="100%",cols="26%,16%,58%",options="header"] +|=== +|Module |Before |Now + +|`+AxiomTrackerCompleteness.agda+` +|**Outside the checked closure and did not parse.** Nothing imported it, no +workflow named it, so no gate had ever compiled it. +|In the closure. Two defects fixed: a hand-rolled `+_⊎_+` was being declared in +a `+where+` clause attached to a type signature (a syntax error — now imported +from `+Data.Sum+`), and two proofs relied on `+worst-policy Clean b+` reducing +when `+worst-policy+` splits on its **first** argument, so the term was stuck +(now via `+clean-left-neutral+` and the new `+worst-ub-right+` in +`+AxiomSafety.agda+`). + +|`+Integrity.agda+` +|did not exist; E11 had prose only +|States E11 and proves it: verification requires an initialised manifest, a +substituted binary is never verified, an uninitialised manifest never verifies. +Collision resistance is a record field, and `+sharpness+` shows it cannot be +inhabited for an accept-everything comparator — so the hypothesis is +load-bearing. + +|`+ClampTrust.agda+` +|did not exist; the obligations lived only in +`+verification/proofs/idris2/ClampTrustBounds.idr+`, an out-of-policy corpus +with no recorded run +|Bounds, monotonicity, fixed points and idempotence, restated over the +trust-level type the gate checks. Monotonicity by step lemma plus transitivity, +not the Idris2 file's decision table. + +|`+Receipt.agda+` +|did not exist +|Receipt/warrant separation as a two-world Kripke countermodel: receipts are +factive, warrants are not, and no warrant promotes to a receipt. Carried over +from `+epistemic-types@5422cd5+` by semantic rewrite; that repo keeps ownership +of its own theorems (`+PROOF-POLICY+` §2.2). + +|`+MetaChecker.agda+` +|claimed "30+ proven properties, 0 postulates (except funext in AxiomSafety)" +|Summary corrected: the `+funext+` clause was stale (no postulates anywhere), +the property count was never derived from a count, and the canonical invocation +plus its `+UnsupportedIndexedMatch+` limit are now recorded in the header. +|=== + +==== What was not run, and why (PROOF-POLICY §6) + +No Rust, Creusot, Lean 4, Idris 2, Rocq, Z3 or cvc5 leg was executed. The +sandbox this was done in could reach only GitHub, PyPI and npm; GitHub *release +assets* (the only source of the Agda/Lean/Idris2 tarballs) were blocked, and +`+scripts/install-proof-toolchains.sh+` needs root, apt and that same host. So +R1, R2, R3, R5 and every Stage-8a Idris2 obligation remain exactly as recorded +— `+open+` or `+argued+` — and no leg is reported as passing. Reporting them as +passing because the flags were "the right ones" would be the failure §6 names. diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc new file mode 100644 index 00000000..07701b3e --- /dev/null +++ b/docs/PROOF-STATUS.adoc @@ -0,0 +1,350 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 ECHIDNA Project Contributors + += Proof status — policy-vocabulary view + +*Status*: current as of 2026-11-01, commit `+916b769+`. +*Normative policy*: `+3-practice/PROOF-POLICY.adoc+` in +https://github.com/hyperpolymath/standards[hyperpolymath/standards] (owner +ruling 2026-10-26). + +This is ECHIDNA's *proof-status file* in the sense `+PROOF-POLICY+` uses the +term: the place each obligation's ledger row lives, in the closed vocabulary of +§5. It is a *view* over link:PROOF-NEEDS.adoc[`+docs/PROOF-NEEDS.adoc+`], not a +replacement: + +[width="100%",cols="26%,74%",options="header"] +|=== +|File |Carries + +|`+docs/PROOF-NEEDS.adoc+` +|The register as it grew: per-obligation narrative, which artefact covers +what, and the dated build receipts (`lake build` run 2026-05-18, per-file error +counts, root causes). *Authoritative for detail and for failures.* + +|`+docs/PROOF-STATUS.adoc+` (this file) +|The same obligations mapped onto `+PROOF-POLICY+` §1 (which verifier carries +which kind) and §5 (the closed status vocabulary), plus obligations +`+PROOF-NEEDS+` does not cover. *Authoritative for the status token.* + +|=== + +Where the two appear to disagree, this file's *token* wins and +`+PROOF-NEEDS+`'s *narrative* wins, because neither a token nor a narrative can +be more accurate than the receipt under it. + +== Vocabulary + +Closed set, `+PROOF-POLICY.adoc+` §5. Machine-readable ledgers use the +lowercase token; prose may use the label. + +[width="100%",cols="22%,16%,62%",options="header"] +|=== +|Token |Label |Means + +|`+proven+` |PROVEN +|Machine-checked with no escape hatch, trust boundary named. A bounded check is +not this row. + +|`+proven-with-postulates+` |PROVEN-WITH-AXIOMS +|A kernel checked it and it rests on named necessary axioms, listed here. + +|`+tested-only+` |TESTED +|Checked on a bounded or sampled domain; bounds given. + +|`+argued+` |ASSUMED +|A stated hypothesis, or a transcription no kernel has checked. Includes "the +CI gate exists and the authors say it passes" when no receipt is cited. + +|`+open+` |OPEN +|Not done. +|=== + +=== Relation to the Mathesis grades + +https://github.com/hyperpolymath/mathesis[mathesis], *Estate-wide Mathematical +Knowledge Architecture* §5, grades a *theorem* by how far its witness has +travelled: **Grade 3** type-checks locally in its home system and is not +translated; **Grade 2i/2ii** one / two independent translations with statement +correspondence recorded; **Grade 1** machine-checked through a verified checker +API in headless CI. + +The two vocabularies are orthogonal — one grades a theorem's reach, the other +records whether a repository's obligation was discharged — but they interact: + +* A home-system leg may be `+proven+` while every independent leg is `+open+`. + That combination *is* Grade 3, and it is the ceiling for anything in this + repository. +* A translation leg is `+argued+`, not `+proven+`, until the statement + correspondence is recorded (`+PROOF-POLICY+` §2: "`the kernel checks the term + only against the translated statement`"). + +Mathesis §6 forbids flattening assurance into a percentage. See R5 and R6. + +== Obligations + +Grouped by the `+PROOF-POLICY+` §1 mapping, because that is what decides which +verifier is even allowed to carry the row. + +=== Rust — Creusot (§1: first-party Rust) + +[width="100%",cols="24%,13%,38%,25%",options="header"] +|=== +|Obligation |Row |Basis |Evidence / next step + +|R1. Trust pipeline, dispatch, arbitration, Pareto +|`+open+` +|`+PROOF-POLICY+` §1 maps first-party Rust to Creusot. +|`+crates/echidna-core-creusot+` describes itself as "`Creusot-annotated (not +yet proved)`"; the `+creusot+` dev-dependency is commented out and the crate +builds on stable Rust behind a `+creusot+` feature. Annotation is not proof. Row +stays `+open+` until a Creusot run yields a receipt with a commit hash. + +|=== + +=== Idris 2 — APIs, ABIs, engineering properties (§1) + +`+PROOF-NEEDS+` lists E2, E3, E5, E6, E7, E12, the VQL-UT row, the extensive +ABI row and the Stage-8a trio as constructively proved, all in +`+verification/proofs/idris2/+` or `+src/abi/+`, all with zero `+believe_me+` +(the `+PROOF-NEEDS+` audit of 2026-05-18 establishes that the 21 +`+believe_me+` grep hits are prose and detector strings). + +[width="100%",cols="24%,13%,38%,25%",options="header"] +|=== +|Obligation |Row |Basis |Evidence / next step + +|R2. Idris 2 interface/ABI obligations (E2, E3, E5, E6, E7, E12, Stage 8a, +VQL-UT, extensive ABI) +|`+argued+` +|`+PROOF-POLICY+` §1 maps ABIs and engineering properties to Idris 2. The +artefacts exist and are detailed in `+PROOF-NEEDS+`. +|No `+idris2 --build+` receipt for +`+verification/proofs/idris2/echidna-verif-proofs.ipkg+` is cited with a commit +hash. Promote to `+proven+` by citing a green run and its commit — that is a +one-line change, and it is the cheapest upgrade in this file. + +|=== + +=== Lean 4 — cross-checks and algebraic properties (§4 exceptions) + +[width="100%",cols="24%,13%,38%,25%",options="header"] +|=== +|Obligation |Row |Basis |Evidence / next step + +|R3. Lean 4 legs: E4-L4 `+ConfidenceLattice.lean+`, E10 +`+ParetoMaximality.lean+` / `+ParetoStrongMaximality.lean+`, E11 +`+IntegrityVerification.lean+`, E13 `+PortfolioCompleteness.lean+` +|`+open+` +|Directly recorded: `+lake build+` run 2026-05-18 (Lean 4.13.0) — *all five +fail to compile*, 49 / 2 / 1 / 5 / 31 errors, three root causes +(`+unfold_let+` removed in 4.13.0; Mathlib tactics under a zero-mathlib +lakefile; instance synthesis and module resolution). +|Nothing. This row is correct and must not be softened. `+PROOF-NEEDS+` records +that `+ConfidenceLattice.lean+` was left byte-identical and that the +`+unfold_let+` token-swap made it worse (104 errors). The open decision is +Mathlib-vs-core, which is an owner call. + +|=== + +=== Agda — theory and metatheory (§1, §2) + +[width="100%",cols="24%,13%,38%,25%",options="header"] +|=== +|Obligation |Row |Basis |Evidence / next step + +|R4. Agda meta-checker: trust-level order, axiom safety, portfolio, dispatch, +axiom-tracker completeness, integrity, clamp bounds, receipt/warrant (9 modules) +|`+proven+` +|First-party Agda in `+meta-checker/src/+`, type-checked with the §2.1 +canonical invocation. Receipt taken 2026-11-01 at commit `+916b769+`: + +---- +agda --safe --without-K --cubical-compatible \ + src/Echidna/MetaChecker.agda # exit 0, 98 s cold +---- + +Versions: Agda `+2.7.0.1+`, `+agda-stdlib+` `+2.1+` (214 stdlib modules pulled +in). All 9 modules in `+src/Echidna/+` produce an interface; 53 warnings, all +of them `+-W[no]UnsupportedIndexedMatch+`, at five sites (`+TrustLevel+` 77, +88, 235; `+AxiomSafety+` 119; `+ClampTrust+` 98). No `+postulate+`, no +`+sorry+`, no `+believe_me+`, no `+Admitted+`; `+--safe+` is what excludes +them rather than a `+grep+`. +|Trust boundary, named: the Agda 2.7.0.1 kernel under `+--safe+`, plus the +stdlib. **Limit, recorded not hidden:** those warnings mean the flagged +functions do not *compute* under Cubical transports. The corpus is +`+--cubical-compatible+`, not `+--cubical+` — exactly the distinction +`+PROOF-POLICY+` §2.1 draws — and dropping the warning, or the flag, to get a +clean log would be the weakening §2.1 forbids. It is immaterial today because +nothing transports these terms; transport is R5's job, which is where the +limit would first bite. + +**Why not just use `+--cubical+`?** Because it fails, and not on this corpus. +`+agda --cubical --safe src/Echidna/MetaChecker.agda+` exits non-zero in +`+agda-stdlib-2.1/src/Data/List/Membership/Setoid/Properties.agda+` with +unsolved metas, before any ECHIDNA module is reached: stdlib 2.1 is written to +be `+--cubical-compatible+`, and ships +`+--warning=noUnsupportedIndexedMatch+` in `+standard-library.agda-lib+` for +precisely this reason. So `+--cubical-compatible+` is not a weakened choice here; +it is the strongest flag this dependency set supports, and the policy's own +distinction between the two flags is what lets that be said plainly. + +Promoted from `+argued+` on the strength of that receipt. Before it, the row +rested on "the CI gate exists and the authors say it passes" — which §5 defines +as `+argued+`, not a receipt. One module +(`+AxiomTrackerCompleteness.agda+`) turned out never to have been in the +checked closure at all, and did not type-check (see R9's note on scope). + +|R9. E11 solver-integrity soundness +|`+proven+` +|`+meta-checker/src/Echidna/Integrity.agda+`, inside the R4 receipt. States the +obligation that had no Agda record: verification requires an initialised +manifest; verification means the recorded digest was matched; a substituted +binary is never verified; an uninitialised manifest never verifies. Collision +resistance is a record *field*, not a postulate, so the guarantee is +conditional and says so in its type; `+sharpness+` exhibits a comparator for +which that field cannot be inhabited, so the hypothesis is load-bearing rather +than decorative. +|**Specification, not implementation.** `+src/rust/dispatch.rs+` lines 642, 848 +and 998, and `+src/rust/integrity/solver_integrity.rs+` line 359, all accept +`+IntegrityStatus::Uninitialized+` as passing. The theorem proves the opposite +of what that code does. That divergence is DEBT D9, now machine-checked on one +side instead of argued on both. Closing R9's implementation leg means changing +the Rust, not the proof. + +|R10. ClampTrustBounds +|`+proven+` +|`+meta-checker/src/Echidna/ClampTrust.agda+`, inside the R4 receipt. Restates +the four obligations of `+verification/proofs/idris2/ClampTrustBounds.idr+` +(bounds, monotonicity, fixed points, and — added — idempotence, i.e. that the +clamp lands on a real level rather than between two) over the trust-level type +the gate actually checks. +|The Idris2 original stays *out of policy* per §3 and, as far as this +repository can tell, was never run: `+idris2-abi-ci.yml+` cites it but no +receipt is recorded. This row does not validate that file; it discharges the +same obligations in a corpus that is checked. Monotonicity is by step lemma +plus transitivity rather than the Idris2 file's 36-clause decision table. + +|R11. Epistemic separation: receipt vs warrant +|`+proven+` +|`+meta-checker/src/Echidna/Receipt.agda+`, inside the R4 receipt. A two-world +Kripke countermodel: a receipt is factive, a warrant is not; the same warrant +never licences the stronger token; while the agent cannot discriminate the +worlds, no receipt exists at all; a discriminating check parameter yields one. +This is what makes §5's "`+argued+` is not `+proven+`" a theorem instead of a +style rule. +|Semantic rewrite of the receipt/warrant distinction from +https://github.com/hyperpolymath/epistemic-types[epistemic-types] at +`+5422cd5+`, **not** a port of its theorems. For the record, that source is +itself green under the same invocation (22/22 modules, exit 0, 0 postulates), so +this row is a rewrite of something that checks, not of an aspiration: per §2.2 the source project keeps +ownership of those, and this module proves only what ECHIDNA needs. The +residual limit is the honest one — a receipt requires a check that +*discriminates*, which is precisely the evidence R5 does not yet have. + +|R5. Independent recheck of R4 in Rocq *and* Lean +|`+open+` +|`+PROOF-POLICY+` §2: every Agda theory proof is rechecked in both, transported +through Dedukti or re-proved, with the route recorded per theorem. +|Never attempted. This is what holds the set at Mathesis *Grade 3*: locally +checked, untranslated. ECHIDNA's `+src/rust/exchange/+` speaks Dedukti, so the +transport route exists; using it is unstarted work, not a missing capability. + +|R6. E9 "proof composition soundness" +|`+argued+`, with a location defect +|`+PROOF-NEEDS+` evidences it with `+proofs/agda/ProofComposition.agda+`. But +`+PROOF-POLICY+` §3 says `+proofs//+` trees are fixtures, "`outside +this policy`". +|The obligation survives; its evidence sits where the policy says evidence +cannot live. **New (2026-11-01):** the whole `+proofs/agda/+` tree — 13 files +including `+ProofComposition.agda+` — type-checks under +`+agda --safe --without-K --cubical-compatible+`, 13/13, no postulates. So the +cheap remedy is the *move* to a policy-conformant location +(`+verification/proofs/agda/+`), not re-stating the obligation as unsupported: +the evidence is good, it is merely filed where §3 says evidence cannot live. +Recorded, not resolved — moving it is a repository change with cross-references +to update, so it is left as a named action rather than done silently. + +|=== + +=== Calibrated scores (§5 is about proof, not ranking) + +[width="100%",cols="24%,13%,38%,25%",options="header"] +|=== +|Item |Row |Basis |Note + +|R7. `+verification/confidence.rs+` 0–1 score; `+DispatchResult.trust_level+` 1–5 +|`+tested-only+` (internal ranking) — *not an assurance claim* +|Mathesis §6: "`Do not flatten proof confidence into a percentage.`" +|The score ranks backends against each other and is unweighted by any receipt. +It is a routing heuristic. Do not publish it as assurance and do not compare it +with a Mathesis grade. + +|R8. `+echidna.prove.result/1+` `+trust.confidence+` +|`+open+`, correctly +|Receipt/warrant discipline: a receipt is transported proof, a warrant is only +evidence. +|A single-backend `+echidna prove+` verifies no certificate, so the field is +`+null+` on every run today. That is the honest value, not a gap to fill with a +guess. + +|=== + +== Not obligations + +`+PROOF-POLICY+` §3: "`Corpora that exist to exercise provers are not +obligations. echidna's `+proofs//+` trees and similar fixtures are test +material for a multi-prover system and are outside this policy.`" + +So the sixteen `+proofs//+` directories and `+training_data/+` carry no +row. They exercise parsers and backends. Listing them is deliberate: an absent +row should read as *out of policy*, not *forgotten*. The same holds for +`+archive/logtalk/+` (dead, quarantined) and for `+echidna-playground/+`. + +Note the tension with R6 — one artefact in a corpus directory is cited by +`+PROOF-NEEDS+` as covering a real obligation. §3 is why that is a defect in +placement rather than a status question. + +== Standing assumptions + +Recorded per `+PROOF-POLICY+` §1.1: where a first-party claim leans on +something the estate does not own, the reliance is its own `+argued+` row +naming the dependency. + +[width="100%",cols="30%,14%,56%",options="header"] +|=== +|Assumption |Row |Scope + +|Solver binaries behave as their published versions do +|`+argued+` +|See link:DEBT.adoc[`+docs/DEBT.adoc+`] D9. No integrity checker is attached in +this release and `+config/solver-manifest.toml+` holds +`+PLACEHOLDER_COMPUTE_ON_FIRST_RUN+` for every solver, so *which* binary ran is +assumed, not checked. Every end-to-end result in this repository inherits it. + +|VeriSimDB persists what it is sent, when it is sent +|`+argued+` +|The writer is fire-and-forget by design (`+dispatch.rs:725+`); a dropped record +is invisible to the proof result. Fine for a learning loop, and precisely why +it must never become a dependency of one. + +|=== + +== What this file does not do + +It is not a release gate and not a CI result. A `+proven+` row here would never +mean "ECHIDNA is verified" — it would mean one named obligation was discharged +by one named tool with its boundary written down. Nothing here vouches for a +prover backend's own soundness. + +No row in this file is above `+argued+` today, and that is the accurate state, +not an omission. + +== Related + +* `+3-practice/PROOF-POLICY.adoc+`, `+docs/TRUSTED-BASE-REDUCTION-POLICY.adoc+`, + `+0-canon/PORT-REGISTRY.adoc+` — hyperpolymath/standards, normative. +* link:PROOF-NEEDS.adoc[`+docs/PROOF-NEEDS.adoc+`] — the detailed register and + its build receipts. +* link:reports/2026-11-01-routing-and-rule-engine-recon.adoc[`+docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc+`] + — the routing audit that produced R7, R8 and D9. diff --git a/docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc b/docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc new file mode 100644 index 00000000..b5061712 --- /dev/null +++ b/docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc @@ -0,0 +1,992 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 ECHIDNA Project Contributors + += Re-recon: routing surfaces and the rule-engine source + +*Status*: current. Supersedes nothing; this is the first pass that classifies +*every* client-facing path in the tree rather than only the ones a given +consumer happens to use. *Date*: 2026-11-01. *Method*: static read of the +checkout at `916b769` — no build, see <>. + +This document answers four questions that were being asked of different +documents with different answers: + +. Is the VeriSimDB bridge a *persistence adapter* or a *mandatory VCL +communication path*? +. How does that reconcile with clients that call the echidnabot REST/GraphQL +surfaces directly, and with proof-burrower's `echidna prove` subprocess +contract? +. Which rule engine is live — the Logtalk module in `rules/`, or the Elixir +rules in Hypatia? +. Which paths in the tree are *active*, *compatibility-only*, *archival* or +*dead*? + +== 0. Verdicts + +*VeriSimDB is a persistence adapter, not a bus.* It is behind the non-default +`verisim` Cargo feature, it is written to fire-and-forget, and no prover is +reached through it. Nothing in the default build contacts it. There is exactly +one exception, and it is an accident rather than a design: enabling `verisim` +also switches `POST /api/prove` from "factory + backend" onto +`ProverDispatcher` (<>). Persistence should not be the switch that turns +the trust pipeline on. + +*VCL-UT is a query layer over VeriSim octads, not a transport ECHIDNA requires.* +In a default build `vcl_ut::cross_prover_search_names` is a stub returning +`Ok(vec![])` and `QueryExecutor` holds a `PhantomData`. A client that never +enables the feature never pays for it. + +*Clients do not need any of that.* echidnabot talks to `/api/*` (core server) +or `/graphql` (the separate `echidna-graphql` binary); proof-burrower looks for +`echidna prove --output json` and reads one JCS line off stdout. Those three +paths are independent and none of them routes through VeriSimDB. + +*The Logtalk material is dead and has been quarantined.* `rules/security_learning.lgt` +was the only `.lgt` file in the tree, referenced by nothing — not a test, not a +workflow, not a Justfile recipe, not the REUSE manifest's per-file headers. +Estate rule authoring is Elixir in Hypatia. The file now lives under +`archive/logtalk/` with a status header; `rules/` no longer exists. + +*Two routing defects were fixed en route* (container entrypoint and health +probes, <>), *one was documented and left open* (the 8081 port collision, +<>), *and one is a live correctness gap* (integrity checking never +configured, <>). + +== 0.1 Policy frame — what this document is allowed to claim + +Three normative sources bound this recon, all outside this repository. Each one +changed a conclusion, not just a footnote. + +[width="100%",cols="26%,20%,54%",options="header"] +|=== +|Source |What it governs |Effect here + +|`+hyperpolymath/standards+`: +`+3-practice/PROOF-POLICY.adoc+` +|Which verifier carries which obligation; the closed status vocabulary +(§5: `+proven+`, `+proven-with-postulates+`, `+tested-only+`, `+argued+`, +`+open+`). +|§2.2 states that ECHIDNA is "`the longer-term automation destination, not a +prerequisite for current independent checks`" — an external, normative reason +the VeriSim/VCL bridge *cannot* be a mandatory path. §3 puts +`+proofs//+` trees outside the policy entirely, which settles how this +recon classifies them. §5 supplies the only status tokens used in §7. + +|`+hyperpolymath/standards+`: +`+0-canon/PORT-REGISTRY.adoc+` +|"`Every project MUST use a unique port. No two projects share a port.`" +|Upgrades <> from untidiness to a policy violation, and is why the fix +is an *override* plus a corrected record rather than a shrug. + +|`+hyperpolymath/mathesis+`: +"`Estate-wide Mathematical Knowledge Architecture`" §5–§6 +|Verification grades (Grade 3 = type-checks in its home system, not translated; +Grade 2i/2ii = one/two independent translations; Grade 1 = machine-checked via +a verified checker API in headless CI). §6 forbids flattening assurance into a +percentage. +|Sets the ceiling on everything below. Nothing in this recon is above *Grade +3*, because nothing was translated or independently checked: it is a read of +one checkout. §6 is also why `+trust.confidence+` is discussed as +receipt-or-null rather than as a number (see link:../PROOF-STATUS.adoc[`+docs/PROOF-STATUS.adoc+`] +R7/R8). +|=== + +=== Claim ledger + +Every headline claim in this document, graded with the vocabulary it is asking +other people to use. This is deliberately unflattering: the honest row for most +of this work is `+argued+`. + +[width="100%",cols="42%,14%,44%",options="header"] +|=== +|Claim |Row |What would move it up + +|VeriSim is optional and non-blocking; no prover is reached through it +|`+proven+` (by construction) +|Already as strong as a static claim gets: the call sites are `+cfg`-gated and +the writes are `+tokio::spawn+`ed. A build-level test asserting zero network +calls with the feature off would make it mechanical. + +|VCL-UT degrades to a stub without the feature +|`+proven+` (by construction) +|Two compiled variants of the same signature exist in `+vcl_ut.rs+`; the +non-feature one returns `+Ok(vec![])+`. + +|echidnabot's and proof-burrower's client paths do not depend on VeriSim +|`+argued+` +|They are other repositories. Verify from their trees, not from this one's +records. + +|`+rules/security_learning.lgt+` was loaded by nothing +|`+argued+` (grep-exhaustive over this tree) +|Green state only if no external consumer exists. Its input path points at a +home directory, which makes one unlikely; it does not prove absence. + +|The container could not start +|`+proven+` (subcommand mismatch is decidable by reading `+Commands+`) +|Already decided: no `+serve+` variant, no alias. + +|Solver integrity is not enforced +|`+proven+` for "no caller attaches a checker"; `+argued+` for the security +consequence +|The first is a grep over the tree. The second needs a run with a checker +attached to observe the difference. + +|`+docs-site/+` is unbuilt +|`+argued+` +|No workflow in this tree builds it. A forge-side check would settle whether +some other system publishes it. +|=== + +=== What is therefore *not* claimed + +* No claim that any proof in this repository is `+proven+`. See + link:../PROOF-STATUS.adoc[`+docs/PROOF-STATUS.adoc+`], where every obligation + row is `+open+` or `+argued+`, including the Agda meta-checker. +* No Grade 2/1 claim anywhere. There is no translation leg and no receipt + pinned to a commit hash, which Mathesis §6 requires. +* No percentage. Where a number exists in this codebase + (`+verification/confidence.rs+`), it ranks backends against each other and is + recorded as `+tested-only+` for internal ranking, never as assurance. +* No interoperability claim between ECHIDNA and `epistemic-types`. The two + share a distinction, not a dependency — see §7. + +== 1. Routing inventory + +Four HTTP listeners are compiled into this repository. They are *not* one +service on four ports; they are four independent binaries with different route +tables, different handlers and different trust behaviour. + +[width="100%",cols="20%,18%,14%,48%",options="header"] +|=== +|Binary |Bind (default) |Route root |Notes + +|`+echidna server+` +|`+127.0.0.1:8081+` — `main.rs:165` +|`+/api/*+` +|The core server. 18 routes, documented from `+src/rust/server.rs:171+`. +Talks to the Julia ML sidecar (hardcoded `+http://127.0.0.1:8090+`, +`+server.rs:64+`) — as does `+echidna-rest+`; see the note below. This is the +only listener whose *behaviour* changes with the `+verisim+` feature. + +|`+echidna-rest+` (`+src/interfaces/rest+`) +|`+127.0.0.1:8000+` — `ECHIDNA_REST_ADDR`, `main.rs:142` +|`+/api/v1/*+`, `+/health+` +|Independent OpenAPI surface. Own session map, own `+ProofFactory+` calls. +Does *not* share `+echidna server+` state, routes or trust path. + +|`+echidna-graphql+` (`+src/interfaces/graphql+`) +|`+127.0.0.1:8081+` — `ECHIDNA_GRAPHQL_ADDR`, default unchanged, `main.rs` +|`+/+` (POST = GraphQL, GET = playground), `+/health+` +|Same default port as the core server. Env override added by <>. + +|`+echidna-grpc+` (`+src/interfaces/grpc+`) +|`+[::1]:50051+` — `main.rs:594` +|`+echidna.proto+` `+ProofService+` +|IPv6 loopback only. No REST equivalent. +|=== + +Non-HTTP client paths, which matter just as much: + +[width="100%",cols="26%,20%,54%",options="header"] +|=== +|Path |Entry point |Contract + +|CLI subprocess +|`+echidna prove --output json+` +|One JCS-canonical `+echidna.prove.result/1+` object on stdout, exit 0 iff +`+verified+`. Specified in link:../PROVE-RESULT-CONTRACT.adoc[`+docs/PROVE-RESULT-CONTRACT.adoc+`]. +No server, no socket, no VeriSimDB. + +|MCP stdio +|`+echidna-mcp+` (`+crates/echidna-mcp+`) +|Shells out to the `+echidna+` binary. Two of its three tools match the current +CLI; one does not (<>). + +|Cap'n Proto +|`+crates/echidna-wire+` +|Schema-only (`+common/prover/proof/gnn/verisim_er.capnp+`). No transport ships +yet; `+src/rust/server.rs+` still speaks JSON. +|=== + +One diagram correction: `+docs/ARCHITECTURE.adoc+` used to render a +"`REST / GraphQL (axum :8000)`" box. That port belongs to `+echidna-rest+`; the +core server is 8081 and serves no GraphQL at all. + +One smaller observation from the same pass, recorded rather than fixed. The +Julia ML sidecar URL appears four times: + +* `+server.rs:64+` — `+DEFAULT_ML_API_URL+`, which `+server.rs:71+` correctly + overrides from `+ECHIDNA_ML_API_URL+`; +* `+server.rs:1271+` — hardcoded again inside the suggest handler, so that one + path ignores the variable; +* `+src/interfaces/rest/main.rs:76+` and + `+src/interfaces/graphql/resolvers.rs:491+` — hardcoded, no environment read. + +`+docs/ENV-VARS.adoc+` describes `+ECHIDNA_ML_API_URL+` as the way to move the +sidecar. True for the core server's main path, false for three others. This is +config plumbing across four call sites in three binaries, so it is a change for +its own PR, not a drive-by. + +== 2. VeriSim: adapter, not a communication path + +=== 2.1 What the feature flag actually gates + +`+verisim+` is off in `+default = []+` (`+Cargo.toml:118+`). It enables +`+dep:ciborium+` (the CBOR encoder for the Semantic octad) and four call sites: + +[width="100%",cols="34%,22%,44%",options="header"] +|=== +|Call site |Direction |Behaviour when absent + +|`+dispatch.rs:725+` `+spawn_record_attempt+` +|write +|`+tokio::spawn+`ed `+record_proof_attempt+` after each dispatch exit. Errors +logged at `+warn+` and swallowed. *Cannot* fail a dispatch. + +|`+dispatch.rs:207+` `+VeriSimAdvisor+` +|read +|`+verify_proof_verisim_guided+` asks +`+mv_prover_success_by_class+` which prover to try. Any error → caller's +fallback prover. Advisory only. + +|`+vcl_ut.rs:349+` `+QueryExecutor+` +|read +|`+PhantomData+` stub; `+cross_prover_search_names+` returns `+Ok(vec![])+` +(`+vcl_ut.rs:951+`). + +|`+server.rs:104+` +|wiring +|`+with_verisim_writer(VERISIM_URL)+`; absent → dispatcher with no writer. +|=== + +Read that table as a whole: every one of the four is a *side effect on, or a +hint to*, a proof run. None of them carries a proof request, a proof result, or +a client command. + +=== 2.2 The one place the flag changes routing + +`+POST /api/prove+` is compiled twice (`+server.rs:423–445+`): + +* with `+verisim+`: `+app_state.dispatcher.verify_proof(...)+` — trust pipeline; +* without: `+ProverFactory::create+` then `+parse_string+` directly — no + dispatcher. + +So the presence of a *storage* feature decides whether an HTTP proof takes the +arbitration path. Two consequences worth stating plainly: + +. A deployment that wants the trust pipeline must enable a database + integration it may not have, and point it at a URL that will then be probed. +. A deployment that enables it for the learning loop silently changes its + verification routing. + +This is recorded as <>. It is not fixed here: the fix is a behaviour +change that deserves its own decision record, and any consumer that currently +relies on the flag to select the pipeline would be moved by surprise. + +=== 2.3 What never touches VeriSim + +`+echidna prove+` (human and `+--output json+`), `+/api/verify+`, +`+/api/verify_raw+`, `+echidna-rest+`, `+echidna-graphql+`, `+echidna-grpc+`, +`+echidna-mcp+`. `/api/search` and `+echidna search+` *do* consult VCL-UT, but +only to append cross-prover results, and only in a `+verisim+` build — the +stub swallows the call otherwise (`+server.rs:1043+`, `+main.rs:924+`). + +=== 2.4 Drift found in the VeriSim surface + +* `+.machine_readable/integrations/verisim.a2ml+` declares `+format = "hexad"+` + and a `+verisimdb-data/feeds/+` destination. The implemented and formally + specified model is an *octad* (8 modalities, + link:../architecture/VERISIM-ER-SCHEMA.adoc[`+VERISIM-ER-SCHEMA.adoc+`]). + "Hexad" is not a modality count that exists anywhere in the tree. +* link:../design/ECHIDNA-VERISIM-TRIANGULATION-2026-04-17.adoc[`+ECHIDNA-VERISIM-TRIANGULATION-2026-04-17.adoc+`] + describes the *workflow* for absorbing provers and predates the entity model. + `+VERISIM-ER-SCHEMA.adoc+` says it "replaces the aspirational text" there. + Classified archival below; not edited. +* `+docs/ECOSYSTEM-INTEGRATION.adoc+` still lists VeriSimDB as "🔄 Manual" with + a `+ingest-scan.sh+` recipe. The *code* path (octad writer + `proof_attempts` + table) is more advanced than that recipe; the recipe is a separate, + scanner-driven ingestion route that predates it. Both are real; neither is + the other. +* `doc/…`-level claim "HTTP push deferred" in + `+.machine_readable/descriptiles/ECOSYSTEM.a2ml:29+` is correct for the + corpus adapter and incorrect for `+dispatch.rs+`, which pushes today. The two + paths emit different payloads (octads vs corpus records) and both are live. + +== 3. Client reconciliation + +=== 3.1 echidnabot, calling REST or GraphQL directly + +Two independent surfaces, and the doc has to name which: + +* *Core server* (`+/api/prove+`, `+/api/verify+`, `+/api/provers+`, + `+/api/health+`) — port 8081 by default, route table in + `+src/rust/server.rs+`. This is what published examples and + `+server-boot-gate.yml+` exercise. +* *`+echidna-rest+`* (`+/api/v1/proofs+`, `+/api/v1/provers+`, …) — port 8000, + OpenAPI + ReDoc. Different paths, different session store, no `/api/prove`. +* *`+echidna-graphql+`* — `+POST /+` on 8081. Queries are `+provers+`, + `+proofState(id:)+`, `+listProofs+`, `+suggestTacticsByProofId+`, + `+proverStatus+`, `+health+`; mutations `+submitProof+`, `+applyTactic+`, + `+cancelProof+`, `+verifyProof+`, `+suggestTactics+`. + +A client that hard-codes 8081 for both REST and GraphQL is relying on two +binaries not being co-resident. See <>. + +*Trust honesty for REST clients*: `/api/verify` never enters the dispatcher +(`+server.rs:519+`), and `/api/verify_raw+` execs the solver binary directly by +design. Only `/api/prove` reaches arbitration, and only in a `+verisim+` build. +A REST client cannot tell, from the response, which of these it got: +`+ProveResponse+` is `+{success, goals, message}+` and `+VerifyResponse+` is +`+{valid, outcome, goals_remaining, tactics_used, mode, smt_status}+`. Neither +carries a schema identifier or a trust level, unlike the prove contract. That +asymmetry is the strongest argument for pointing new clients at +`+echidna prove --output json+` rather than HTTP. + +=== 3.2 proof-burrower, the `+echidna prove+` subprocess contract + +This is the best-specified client path in the tree and it needs no network at +all: + +* one line, JCS-canonical, on stdout; logs and `+--diagnose+` on stderr; +* `+status+` ∈ `+verified | failed | error | timeout | unknown+`, derived from + `+ProverOutcome+` via a total mapping; +* `+trust.confidence+` is `+null+` on this path *always* — a single-backend + check verifies no certificate, so there is no receipt. This is the + receipt/warrant distinction applied honestly, and it matches where + `+epistemic-types+` has landed: ECHIDNA copies the distinction as a pattern, + it does not depend on the Agda library and does not claim interop with it; +* exit code 0 iff `+verified+`; +* capability detection by probing `+echidna prove --help+` for `+--output+`. + +Feature-detection matters: the contract is *additive* per its own versioning +rules, so older binaries answering without `+--output+` are still usable, and +new clients must ignore unknown fields. + +=== 3.3 `+echidna-mcp+` — the client that drifted + +`+crates/echidna-mcp/src/main.rs+` invokes: + +* `+echidna prove --format json+`. `+--format+` *is* a global flag + (`+main.rs:43+`, `+global = true+`) so this parses, but it selects the CLI + formatter (`+{"level":"success",…}+`), not the prove contract. The tool then + sniffs for `+"level": "success"+`. It works and it is the *legacy* shape: a + second, undocumented JSON dialect for the same operation. +* `+echidna list-provers --format json+` — parses; no contract at all. +* `+echidna check-prover +` — *no such subcommand exists* + (`+Commands+` in `+main.rs:57–450+` has no `+CheckProver+`). The tool fails + with a clap usage error every time. + +Recorded as <>. Not fixed here: the correct repair is a rewrite onto +`+--output json+` plus a `+check-prover+` subcommand or a `/api/provers` probe, +which is a feature decision, not a rename. + +=== 3.4 What no client can get today + +* A partial-progress field. The contract has no "remaining subgoals"; a swarm + that wants to score partial attempts must parse prover output. +* A receipt-backed confidence via HTTP. `+/api/prove+` has no `+trust+` object. +* A single surface that is both OpenAPI-described and trust-pipeline-backed. + +None of these are bugs in the contract. They are the current *scope*, and the +useful thing a recon can do is stop other documents implying otherwise. + +== 4. Logtalk: what was left and why it is dead + +=== 4.1 What was there + +`+rules/security_learning.lgt+` — 234 lines, two Logtalk objects +(`+security_learning+`, `+cicd_integration+`), dated 2025-12-29. It encodes 20 +alert categories from cicd-hyper-a's `+ERROR-CATALOG.scm+`, a severity +classifier, a fix-suggestion table, seven prevention workflows, and a +`+assertz+`-based "learning" loop that re-derives rules from its own training +data. + +=== 4.2 Why it is dead + +* *Nothing loads it.* `+grep -rn '\.lgt' --exclude-dir=.git .+` returns the file + and one self-reference inside it. No test, workflow, Justfile recipe, A2ML + manifest or Cargo build step names it. No `+logtalk+`/`+swipl+` binary is + referenced anywhere in CI. +* *Its inputs are on someone's disk.* `+cicd_repo_path('~/repos/cicd-hyper-a/.audittraining')+` + — a home-directory path with a literal `+~+`, in an object whose job is to + open it. Not portable, not parameterised, not a contract. +* *Its learning loop cannot learn.* `+load_training_data/1+` calls + `+read(Stream, Term)+` on a Prolog stream but the file it is pointed at is a + Scheme source (`+ERROR-CATALOG.scm+`). Every term fails + `+process_training_term/1+` and hits the catch-all `+process_training_term(_)+`. + `+learn_rules/0+` then asserts whatever the static tables already said. The + output is a transcript of the input constants. +* *The estate moved.* `+docs/ECOSYSTEM-INTEGRATION.adoc:117+` described Hypatia + as auto-generating Logtalk rules after 5+ observations. Hypatia's rule + engine is Elixir; the estate's rule-as-data path is Elixir rule modules, not + Logtalk objects. An ECHIDNA-side Logtalk module was never a consumer of that + output, even when the prose was accurate. +* *The one live rule surface in this repo is `+.hypatia-baseline.json+` + + `+.hypatia-ignore+`* — i.e. ECHIDNA is a Hypatia *target*, not a rule + producer. + +=== 4.3 Disposition + +Moved, not deleted, and marked: + +[width="100%",cols="34%,66%",options="header"] +|=== +|Before |After + +|`+rules/security_learning.lgt+` +|`+archive/logtalk/security_learning.lgt+` — body unchanged (so the record is +byte-recoverable), preceded by a `+DEAD SOURCE+` block naming the date, the +reason and the successor. + +|_(no index)_ +|`+archive/logtalk/README.adoc+` — what it was, why it is here, what would have +to be true to revive it. + +|`+.reuse/dep5+` `+Files: rules/*+` +|`+Files: archive/*+` — the same MPL-2.0 bulk stanza, retargeted. + +|`+.machine_readable/root-allow.txt+` +|`+archive/+` added, because it is a root entry outside the template — the file +exists precisely to record those. +|=== + +`+rules/+` is gone rather than emptied, so that the tree cannot imply "ECHIDNA +has rules in Logtalk" by the existence of the directory. + +=== 4.4 Prose also retired + +* `+docs/ECOSYSTEM-INTEGRATION.adoc+` — the Logtalk-generation sentence now + states Elixir and links here. +* `+echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml+` — + `+report-format = "logtalk"+` retired to a comment. That key told a scanner + consumer to expect a format nothing produces. + +== 5. Path classification + +Four classes, used strictly: + +* *active* — built, called, or deployed by something in this tree today; +* *compatibility-only* — works, but exists to serve a consumer or a shape that + a newer path supersedes; must not gain new capability; +* *archival* — retained as a record; explicitly not a build or usage + instruction; +* *dead* — nothing loads it and nothing can. + +[width="100%",cols="38%,14%,48%",options="header"] +|=== +|Path |Class |Basis + +|`+src/rust/main.rs+` (`+server+`, `+prove+`, `+verify+`, `+search+`, `+corpus+`, …) +|active +|The binary. Booted by `+server-boot-gate.yml+`, exercised by `+QUICKSTART-USER.adoc+`. + +|`+src/rust/server.rs+` +|active +|18 routes; the published API (`+site/docs/api/core.adoc+`). + +|`+src/rust/dispatch.rs+` +|active +|`+ProverDispatcher+`. Caveat <> and <>. + +|`+src/rust/vcl_ut.rs+` +|active (conditional) +|Real executor under `+verisim+`; deliberate stub without it. Both compiled and +tested. + +|`+src/rust/verisim_bridge.rs+` +|active (conditional) +|Octad writer/reader. Non-default feature; weekly `+s4-loop.yml+` runs it. + +|`+crates/echidna-core+` +|active +|Published shared contract types (`+prove_result+`, `+prover_kind+`) for +external consumers. + +|`+crates/echidna-wire+` +|active, unbuilt in CI +|Schemas only; `+STATE.a2ml+` records `cargo build` failing on a missing `+capnp+` +binary — pre-existing, unrelated to routing. + +|`+crates/echidna-mcp+` +|compatibility-only +|`+prove+` and `+list_provers+` work via the legacy formatter dialect; +`+check_prover+` is dead (<>). + +|`+src/interfaces/rest+`, `+graphql+`, `+grpc+` +|active +|Separate binaries, in the workspace, documented in `+site/docs/api/+`. + +|`+src/interfaces/*/ffi_wrapper.rs+` +|compatibility-only +|C shim against `+libechidna_ffi.so+`; every binary falls back to direct Rust +calls when it is absent (`+ffi_integration_test.rs+`). Self-described +scaffolding. + +|`+echidna prove --output json+` (`+prove_contract.rs+`, +`+echidna-core/prove_result.rs+`) +|active +|The supported machine contract; golden-JCS tests; consumed by proof-burrower. + +|`+--format json+` global CLI output +|compatibility-only +|Older machine dialect (`+{"level":…}+`), still used by MCP. Superseded by the +prove contract; no new consumer should adopt it. + +|`+/api/prover+`, `+/api/verify+` response shapes +|compatibility-only +|Untagged JSON; no schema id, no trust block. Kept for existing clients. + +|`+container/entrypoint.sh+` +|was dead → fixed +|Called `+echidna serve+`; the subcommand is `+server+`. Every container start +failed at `+exec+`. + +|`+container/compose.toml+` healthcheck +|was dead → fixed +|Probed `+/health+`; the core server only serves `+/api/health+`. + +|`+container/vordr.toml+` readiness probe +|was dead → fixed +|Probed `+/ready+`, which no binary in this tree has ever served. + +|`+container/manifest.toml+`, `+Containerfile+` +|active +|`+EXPOSE 8081+` matches the default; `+APP_PORT+` is consumed by the +entrypoint, not the binary. + +|`+rules/security_learning.lgt+` +|dead → quarantined +|§4.2. + +|`+archive/logtalk/+` +|archival +|Quarantine, not a build input. Indexed by `+archive/logtalk/README.adoc+`. + +|`+proofs//+` trees (16 directories) and `+training_data/+` +|archival *(out of policy)* +|Fixtures, not obligations: `+PROOF-POLICY.adoc+` §3 names these explicitly — +"`echidna's `+proofs//+` trees and similar fixtures are test material +for a multi-prover system and are outside this policy`". They exercise parsers +and backends. No status row, and none owed — see +link:../PROOF-STATUS.adoc[`+docs/PROOF-STATUS.adoc+`] "Not obligations". + +|`+docs/ECOSYSTEM-INTEGRATION.adoc+` +|archival (corrected) +|2026-02-12 point-in-time status; kept as a record, Logtalk claim retired. + +|`+docs/design/ECHIDNA-VERISIM-TRIANGULATION-2026-04-17.adoc+` +|archival +|Superseded by `+VERISIM-ER-SCHEMA.adoc+` in its own words. + +|`+docs/architecture/VERISIM-ER-SCHEMA.adoc+`, `+crates/echidna-wire/schemas/verisim_er.capnp+` +|active +|Canonical entity model + wire schema. + +|`+.machine_readable/integrations/verisim.a2ml+` +|active but drifted +|`+hexad+` is not a model that exists (<>). Still the declared feed +manifest. + +|`+docs-site/+` (content + Eclexia TEA app) +|dead +|No workflow builds or deploys it: `+pages.yml+` publishes `+site/+` via Ddraig. +Its API pages claim `+/graphql+`, `+/playground+`, "30 provers" and +`+localhost:8000/api/v1+` — none of which matches the code. Not edited: editing +a dead publisher only makes the corpse tidier. Delete or rebuild as a decision. + +|`+site/+` + `+site/docs/api/*.adoc+` +|active +|Deployed by `+pages.yml+`; content matches the source as of this read. + +|`+docs-site/.well-known/aibdp.json+`, `+docs-site/config/policy.yml+` +|archival +|Consumed only if `+docs-site+` is ever served. + +|`+docs/reports/audit/+`, `+docs/releases/*+`, `+docs/handover/*+` +|archival +|Dated records. `+RELEASE_NOTES_v1.3.adoc+` still shows `+--enable-cors+`, which +the CLI spells `+--cors+`; left alone deliberately. +|=== + +== 6. Defects found + +IDs here are local to this report (`+RD`*n*), because link:../DEBT.adoc[`+docs/DEBT.adoc+`] +already uses `+D`*n* for its documentation-debt entries and `+C`*n* for code. +The ones that outlive this report carry a DEBT number: + +[width="100%",cols="12%,22%,66%",options="header"] +|=== +|Here |In `+DEBT.adoc+` |Form + +|RD1 |D10 |open +|RD2 |D8 |partly fixed (override + corrected record); default port open +|RD3 |— |fixed, recorded in DEBT's "`Fixed en route`" list +|RD4 |D11 |open +|RD5 |D9 |docs fixed, enforcement decision open +|RD6 |— |open, small; no DEBT number because there is nothing to decide +|RD7 |D12 |open +|RD8 |— |open, small; no DEBT number because there is nothing to decide +|=== + +[[rd1]] +=== RD1. `+verisim+` is a routing switch as well as a storage switch +*P1 — structural, open.* + +`+server.rs:423+` compiles `/api/prove` two ways; whether an HTTP proof enters +`+ProverDispatcher+` depends on a database feature. No caller-visible field +distinguishes the two behaviours. + +*Fix direction* (not applied): build the dispatcher unconditionally and make +`+with_verisim_writer+` purely additive — the writer already cannot fail a +dispatch, so nothing needs the compile-time branch. Requires a decision record +because it changes what a default build returns. + +*Reproduce:* +[source,bash] +---- +sed -n '420,450p' src/rust/server.rs +grep -n 'cfg(feature = "verisim")' src/rust/server.rs +---- + +[[rd2]] +=== RD2. Core server and GraphQL interface both default to 8081 +*P1 — documented, open.* + +`+main.rs:165+` (`+server --port+` default 8081) and +`+src/interfaces/graphql/main.rs:39+` (`+127.0.0.1:8081+`, hard-coded). Whichever +starts second cannot bind. `+docs/QUICKSTART-USER.adoc+` claimed the three +interfaces sit "on dedicated ports (8081 / 50051 / 8000)" — false for the first +two pairings. + +This is a policy matter, not a preference: +`+0-canon/PORT-REGISTRY.adoc+` in hyperpolymath/standards says "`Every project +MUST use a unique port. No two projects share a port.`" The registry is +prose-only today ("`no gate reads this registry`"), which is why the collision +survived a release. + +Done here: `+ECHIDNA_GRAPHQL_ADDR+` override (default unchanged, so no client +breaks), and explicit collision warnings in `+site/docs/index.adoc+`, +`+site/docs/api/graphql.adoc+` and `+QUICKSTART-USER.adoc+`, plus +`+core-server = 8081+` in the `+[interfaces]+` block of `+META.a2ml+` so the +machine record cannot omit it. + +Not done: moving the default. Anything pinned to 8081 keeps working; a +deployment that wants both sets the variable. + +*Reproduce:* +[source,bash] +---- +grep -n 'default_value = "8081"' src/rust/main.rs +grep -n '127.0.0.1:8081' src/interfaces/graphql/main.rs +---- + +[[rd3]] +=== RD3. Container entrypoint and health probes targeted strings that do not exist +*P2 — fixed.* + +`+entrypoint.sh+` ran `+echidna serve+` (subcommand is `+server+`, no alias); +`+compose.toml+` probed `+/health+` and `+vordr.toml+` probed `+/ready+`, neither +of which the core server serves. Net effect: the published container could not +start, and would have been unhealthy if it had. + +Three-line fix in each file; `+/api/health+` is the real route +(`+server.rs:173+`). + +*Adjacent, found and deliberately not fixed.* `+container/compose.toml+` is not +valid TOML 1.0: its `+environment = { … }+` inline tables span multiple lines, +which TOML forbids. `+selur-compose+` accepts the dialect, but the file's own +header offers `+podman compose --file compose.toml+` as the fallback when selur +is absent, and a strict parser rejects the file before it looks at the routes +(verified: Python's `+tomllib+` fails at line 19, column 16, on both the +pre-and-post-change file). Rewriting the tables to `+[services.echidna.environment]+` +would fix the fallback but changes what selur reads, so it needs whoever owns +the selur format to confirm rather than a guess. + +[[rd4]] +=== RD4. `+echidna-mcp+` calls a subcommand that does not exist +*P2 — open.* + +`+cmd.arg("check-prover")+` (`+main.rs:176+`). Fix requires adding the +subcommand or probing `/api/provers`; both are feature decisions. Its `prove` +tool additionally uses the legacy `+--format json+` dialect instead of +`+--output json+`. + +[[rd5]] +=== RD5. Solver integrity checking is never configured +*P1 — open, and the largest gap this pass found.* + +`+docs/ARCHITECTURE.adoc+` promises step 1 of the trust pipeline is +`+integrity/+`: "solver binary SHAKE3-512 + BLAKE3 against +`+config/solver-manifest.toml+`". In `+dispatch.rs:632–645+` the check runs only +`+if let Some(ref checker) = self.integrity_checker+`, else +`+solver_integrity_ok = true+`. `+with_integrity_checker+` has *no caller +anywhere in the tree* (`+grep -rn with_integrity_checker src/ crates/ tests/+` +returns the definition only). And `+config/solver-manifest.toml+` still carries +`+shake3_512 = "PLACEHOLDER_COMPUTE_ON_FIRST_RUN"+` for every solver, so +configuring a checker today would report `+Uninitialized+` — which the code +treats as passing. + +So: integrity is *assumed* ok on every path, and the manifest could not prove +otherwise if it were consulted. Report as a gap; wiring it is a decision (it +introduces a failure mode where a proof is refused for a hash mismatch). + +*Reproduce:* +[source,bash] +---- +grep -rn 'with_integrity_checker' src/ crates/ tests/ # definition only +grep -n 'PLACEHOLDER' config/solver-manifest.toml +---- + +[[rd6]] +=== RD6. VeriSim feed manifest says `+hexad+` +*P2 — open.* + +`+.machine_readable/integrations/verisim.a2ml+`: `+format = "hexad"+`. The model +is an octad. Either the manifest is stale or the feed is a different shape than +the octad writer; the document does not say which, and nothing reconciles them. + +[[rd7]] +=== RD7. `+docs-site/+` publishes stale API claims +*P2 — open.* + +Not deployed (see §5), but it is linkable and states `/graphql` and +`/playground` endpoints (the binary serves `/`), "30 supported prover backends" +(canonical count is in `+docs/PROVER_COUNT.adoc+`), and a `+localhost:8000/api/v1+` +base. Delete or rebuild; both are cheap, drift is not. + +[[rd8]] +=== RD8. `+verify_parallel+` ignores the configured dispatcher +*P2 — open.* + +`+server.rs:619+` constructs a fresh `+ProverDispatcher::new()+` instead of using +`+app_state.dispatcher+`. With `+verisim+` on, parallel verifies therefore +record nothing in `+proof_attempts+` while serial `/api/prove` calls do — a +silent second inconsistency in the same learning loop that <> describes. + +[[limits]] +== 7. Limits of this pass + +No build was run and none could be: this checkout has no cargo toolchain, no +`+agda+`, no Creusot, and no network access to a crate registry. Everything +above is a static read of source and configuration at `916b769`. Where a claim +depends on runtime behaviour it says so and gives the command that would settle +it. + +By the ledger vocabulary of `+PROOF-POLICY.adoc+` §5, that makes the *whole +document* `+argued+` — a transcription no kernel, compiler or test runner +checked. The claim ledger in §0.1 grades the individual claims; none of them is +above `+proven+`, and the ones that reach `+proven+` (by construction) only do +so for facts decidable by reading, such as "no `+serve+` variant exists" or +"this branch is `+cfg`-gated". By the Mathesis grades this is at best *Grade 3* +in shape — locally consistent, untranslated, independently unchecked — and the +Agda legs are *not* even locally checked here, since no Agda is installed. + +Claims about other repositories — proof-burrower's parser tolerance, +echidnabot's client wiring, Hypatia's generated-rule format — are taken from +this repository's own records and are *not* independently verified here. The +`+issues/+` drafts already mark such claims *[unverified]*; this document keeps +that discipline. + +Scope note: `+epistemic-types@5422cd5+` (22 strict-safe Agda modules, Kripke +semantics, receipt/warrant split) is *context* for what ECHIDNA may claim, not a +dependency. `+docs/PROVE-RESULT-CONTRACT.adoc+` and +`+crates/echidna-core/src/prove_result.rs+` both describe the relationship as +"copies the distinction as a pattern; does not depend on the Agda library" — +which is the accurate, scoped statement, and this recon found no place +overclaiming universal interoperability. + +== 8. Reproduction + +[source,bash] +---- +# every HTTP listener and its default bind +grep -n 'TcpListener::bind\|let addr =' src/rust/server.rs src/interfaces/*/main.rs +grep -n 'default_value = "8081"' src/rust/main.rs + +# the feature flag that is off by default +sed -n '115,132p' Cargo.toml +grep -rn 'cfg(feature = "verisim")' src/rust/ | wc -l + +# nothing loads Logtalk +grep -rn '\.lgt' --exclude-dir=.git . # archived file + its own self-reference +grep -rni 'logtalk' --exclude-dir=.git . # prose only, after this change + +# the prove contract vs the legacy formatter +grep -n 'ProveOutput\|--output' src/rust/main.rs | head +grep -n '"level"' src/rust/output.rs | head + +# integrity checker wiring +grep -rn 'with_integrity_checker' src/ crates/ tests/ # definition only +---- + +== 9. Follow-ups, in the order they are worth doing + +. <> — decide whether solver integrity is enforced or documented as not + enforced. The current text said it is enforced; that is the one item here + that could mislead someone into relying on an assumption. +. **DONE** — `+docs/PROOF-STATUS.adoc+` R4 re-type-checked with the canonical §2.1 + invocation. It passes; R4 is now `+proven+`, with the + `+UnsupportedIndexedMatch+` limit recorded rather than papered over. See + <>. +. `+docs/PROOF-STATUS.adoc+` R2 — cite a green `+idris2-abi-ci.yml+` run and its + commit for the ABI row. +. <> — decouple the trust pipeline from the `+verisim+` feature. +. <> — delete `+docs-site/+` or regenerate it from `+site/docs/+`. +. <> — move the GraphQL default off 8081 once a release note can carry + the change. +. <> — repair or remove `+echidna-mcp+'s `+check_prover+`. +. <>, <> — small, unambiguous, no decision needed. + +=== Not follow-ups + +`+proofs/+` trees being unverified, and every `+trust_level+` in the tree +being disconnected from a receipt. The first is policy (`+PROOF-POLICY+` §3: +corpora are not obligations); the second is recorded scope +(`+docs/PROOF-STATUS.adoc+` R7/R8). Chasing either as debt would be a category +error, which is why they are named here. + +[[proof-updating]] +== 10. Proof updating, 2026-11-01 + +The follow-up at §9.2 was executed, and the proof corpus was extended rather +than only re-checked. Receipts are in `+docs/PROOF-STATUS.adoc+` (R4, R9, R10, +R11) and the narrative in `+docs/PROOF-NEEDS.adoc+`; this section records what +the *audit* position now is. + +=== 10.1 The receipt that matters + +[source,bash] +---- +cd meta-checker +agda --safe --without-K --cubical-compatible src/Echidna/MetaChecker.agda +# exit 0, 98 s cold, 9 modules + 214 stdlib modules +---- + +Agda 2.7.0.1, `+agda-stdlib+` 2.1, commit `+916b769+`. Zero postulates — and now +excluded by `+--safe+` rather than by a `+grep+`, which is the difference between +`+argued+` and `+proven+` in §5 of the policy. + +**The limit, stated as a limit.** 53 warnings, all +`+-W[no]UnsupportedIndexedMatch+`, at `+TrustLevel+` 77/88/235, +`+AxiomSafety+` 119 and `+ClampTrust+` 98. Those functions do not *compute* +under Cubical transports. The corpus is `+--cubical-compatible+`, **not** +`+--cubical+` — `+PROOF-POLICY+` §2.1 draws exactly that distinction, and it is +why the flag stays and the warning is reported instead of suppressed. + +The obvious question — why not use `+--cubical+` and be done with it — was +tested rather than argued: `+agda --cubical --safe src/Echidna/MetaChecker.agda+` +fails **inside stdlib 2.1** (`+Data/List/Membership/Setoid/Properties.agda+`, +unsolved metas) before reaching any ECHIDNA module. The stdlib is written to be +`+--cubical-compatible+` and ships `+--warning=noUnsupportedIndexedMatch+` for +itself. So the flag chosen is the strongest the dependency set supports, and the +warning is a limit to record, not a weakness to hide. + +One more result worth having: the out-of-policy `+proofs/agda/+` tree — the one +R6 cites — is **13/13 green** under the same flags. That does not make it +in-policy, but it does change R6's remedy from "downgrade the claim" to "move the +file". + +=== 10.2 A module that had never been compiled + +`+meta-checker/src/Echidna/AxiomTrackerCompleteness.agda+` was in the tree, and +in the "30+ properties" summary, but nothing imported it and no workflow named +it — so it had never been type-checked by any gate. Compiling it showed a syntax +error (a hand-rolled `+_⊎_+` declared in a `+where+` clause on a type signature) +and two proofs that assumed `+worst-policy Clean b+` reduces, when +`+worst-policy+` splits on its first argument and the term is stuck. + +This is the same class of finding as the routing audit's: an artefact whose +existence was being reported as evidence. Two fixes and it is now in the +closure, and `+agda-meta-checker.yml+` gained a step that fails if any module +under `+src/Echidna/+` produces no interface — the orphan cannot recur silently. + +=== 10.3 Obligations that had prose but no proof + +Three new modules, all inside the receipt above: + +* `+Integrity.agda+` — **E11**, previously an informal note. It proves the + invariant the Rust *violates*: `+dispatch.rs+` 642/848/998 and + `+solver_integrity.rs+` 359 accept `+Uninitialized+` as passing. So R9 is + `+proven+` on the specification and the implementation leg stays open, keyed to + DEBT D9. This is the useful outcome: the divergence is now checked on one side + instead of read on both. +* `+ClampTrust.agda+` — the four `+ClampTrustBounds.idr+` obligations plus + idempotence, in a corpus that is actually run. It does not validate the Idris2 + file, which remains out of policy (§3) with no recorded run. +* `+Receipt.agda+` — the receipt/warrant distinction carried over from + `+epistemic-types@5422cd5+` as a two-world Kripke countermodel: a receipt is + factive, a warrant is not, and the same warrant never licences the stronger + token. Semantic rewrite, not a port — per §2.2 the source project keeps + ownership of its own theorems, and this module proves only what ECHIDNA needs. + It is what turns §5's "`+argued+` is not `+proven+`" from a style rule into a + theorem. + +=== 10.4 What the proof grade did and did not move + +*Home-system leg:* R4, R9, R10, R11 are `+proven+`. *Independent legs:* R5 +(Rocq + Lean) is untouched and `+open+`. So the corpus is still **Mathesis Grade +3** — locally checked, untranslated — and this session did not move it, because +nothing that establishes Grade 2i/2ii was performed. What moved is the policy +vocabulary, not the grade. + +=== 10.5 Toolchains that could not be installed + +No Rust, Creusot, Lean 4, Idris 2, Rocq, Z3 or cvc5 leg ran. The environment +reached only GitHub, PyPI and npm; GitHub *release assets* — the sole source of +those tarballs — were blocked, and `+scripts/install-proof-toolchains.sh+` +requires root, apt and the same host. Agda itself was only installable because a +PyPI wheel exists, and even that needed the `+data/lib+` primitives lifted from +the 2.7.0.1 tag to work. + +Per `+PROOF-POLICY+` §6, R1, R2, R3, R5 and every Stage-8a Idris2 obligation are +reported as not run, not as passing. The recon's §7 limits stand unchanged. + +=== 10.6 Version choice, flagged rather than assumed + +"Latest stable" for this corpus is Agda 2.8.0.2 with stdlib 2.4. Neither is +reachable here, and §2.1 says to pin versions per commit — so the receipt is +taken at 2.7.0.1 / 2.1, which is also what `+agda-meta-checker.yml+` pins. A +future bump is a deliberate act with a new receipt, not a side effect of +"update to latest". + +=== 10.7 The rest of the estate, checked rather than assumed + +The session was also asked about proofs elsewhere in the estate. What is +actually reachable from this environment: + +[width="100%",cols="24%,16%,60%",options="header"] +|=== +|Repository |Reachable |What was found + +|`+hyperpolymath/epistemic-types+` +|yes +|Cloned at `+5422cd5+` — the commit named in the brief. **22 `.agda` files, all 22 +in the checked closure, `+agda --safe --without-K --cubical-compatible+` exit 0, +0 postulates, 69 `+UnsupportedIndexedMatch+` warnings.** The brief's "22 +strict-safe modules" is exactly right, and the figure is now a receipt rather +than a recollection. Nothing was edited: §2.2 keeps proof ownership with the +source project, and this session cannot push outside its own branch anyway. What +ECHIDNA took is the receipt/warrant distinction, re-proved as R11. + +|`+hyperpolymath/the-metadatastician+` +|yes +|Exists (pushed 2026-10-13, language: Shell) with **zero proof artefacts** — no +`+.agda+`, `+.idr+`, `+.lean+`, `+.v+` or `+.thy+` anywhere in the tree. There is +no proof updating to do there; whatever is outstanding is not a proof problem. + +|`+hyperpolymath/stuff-of-awesome+` +|**no** +|404, and a user-scoped search returns 0 results. Not visible to this token: +either renamed, private, or never existed under this owner. + +|`+hyperpolymath/catachresis-colloquium+` +|**no** +|404, 0 results in a user-scoped search and 0 under the `+metadatastician+` org. +Same caveat: private or absent. +|=== + +A 404 is not proof of absence, so the last two rows are recorded as *not +visible from here* rather than as *does not exist*. If they are private, the +work needs a token with access; if they were renamed, the new names are needed. +Neither can be discharged by guessing. diff --git a/echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml b/echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml index f8f845f9..9797c75d 100644 --- a/echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml +++ b/echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml @@ -9,7 +9,12 @@ last-updated = "2026-04-11" [hypatia-config] scan-enabled = true scan-depth = "standard" # quick | standard | deep -report-format = "logtalk" +# report-format retired 2026-11-01. It read "logtalk", which no scanner in the +# estate emits: Hypatia's rule engine is Elixir, and this project is a scan +# target, not a rules producer. Left unset so the consumer applies its own +# default rather than being told to expect a format nothing produces. +# See docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc §4.4. +# report-format = "logtalk" [symbolic-rules] # Custom symbolic rules for this project diff --git a/meta-checker/src/Echidna/AxiomSafety.agda b/meta-checker/src/Echidna/AxiomSafety.agda index 153c0c73..7f084590 100644 --- a/meta-checker/src/Echidna/AxiomSafety.agda +++ b/meta-checker/src/Echidna/AxiomSafety.agda @@ -154,6 +154,37 @@ worst-ub-left IncompleteProof IncompleteProof = inc≤i worst-ub-left IncompleteProof Rejected = inc≤r worst-ub-left Rejected _ = rej≤r +-- THEOREM: Clean is a left unit for worst-case composition. +-- (`worst-policy` splits on its first argument, so this needs the +-- second argument enumerated even though the equation is "obvious".) +clean-left-neutral : ∀ (b : AxiomPolicy) → worst-policy Clean b ≡ b +clean-left-neutral Clean = refl +clean-left-neutral ClassicalAxioms = refl +clean-left-neutral IncompleteProof = refl +clean-left-neutral Rejected = refl + +-- THEOREM: worst-policy is an upper bound in its SECOND argument. +-- Needed to rewrite `fold-worst ps ≤ₚ worst-policy p (fold-worst ps)` +-- when the first argument is neutral: `worst-policy` splits on its first +-- argument, so the result is stuck until the second is enumerated. +worst-ub-right : ∀ (a b : AxiomPolicy) → b ≤ₚ worst-policy a b +worst-ub-right Clean Clean = clean≤ +worst-ub-right Clean ClassicalAxioms = class≤c +worst-ub-right Clean IncompleteProof = inc≤i +worst-ub-right Clean Rejected = rej≤r +worst-ub-right ClassicalAxioms Clean = clean≤ +worst-ub-right ClassicalAxioms ClassicalAxioms = class≤c +worst-ub-right ClassicalAxioms IncompleteProof = inc≤i +worst-ub-right ClassicalAxioms Rejected = rej≤r +worst-ub-right IncompleteProof Clean = clean≤ +worst-ub-right IncompleteProof ClassicalAxioms = class≤i +worst-ub-right IncompleteProof IncompleteProof = inc≤i +worst-ub-right IncompleteProof Rejected = rej≤r +worst-ub-right Rejected Clean = clean≤ +worst-ub-right Rejected ClassicalAxioms = class≤r +worst-ub-right Rejected IncompleteProof = inc≤r +worst-ub-right Rejected Rejected = rej≤r + -- THEOREM: worst-policy is commutative worst-comm : ∀ (a b : AxiomPolicy) → worst-policy a b ≡ worst-policy b a worst-comm Clean Clean = refl diff --git a/meta-checker/src/Echidna/AxiomTrackerCompleteness.agda b/meta-checker/src/Echidna/AxiomTrackerCompleteness.agda index 1191018c..624b0a7f 100644 --- a/meta-checker/src/Echidna/AxiomTrackerCompleteness.agda +++ b/meta-checker/src/Echidna/AxiomTrackerCompleteness.agda @@ -22,6 +22,7 @@ module Echidna.AxiomTrackerCompleteness where open import Data.Nat using (ℕ; zero; suc; _+_) open import Data.List using (List; []; _∷_; length; map; _++_) open import Data.Product using (_×_; _,_) +open import Data.Sum using (_⊎_; inj₁; inj₂) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong) open import Echidna.AxiomSafety @@ -78,7 +79,7 @@ scan-entry-length (mk-entry p (d ∷ ds)) = fold-worst-++ : ∀ (xs ys : List AxiomPolicy) → fold-worst (xs ++ ys) ≡ worst-policy (fold-worst xs) (fold-worst ys) -fold-worst-++ [] ys = refl +fold-worst-++ [] ys = sym (clean-left-neutral (fold-worst ys)) fold-worst-++ (x ∷ xs) ys = trans (cong (worst-policy x) (fold-worst-++ xs ys)) (sym (worst-assoc x (fold-worst xs) (fold-worst ys))) @@ -90,19 +91,7 @@ fold-worst-++ (x ∷ xs) ys = fold-worst-prepend-monotonic : ∀ (p : AxiomPolicy) (ps : List AxiomPolicy) → fold-worst ps ≤ₚ worst-policy p (fold-worst ps) -fold-worst-prepend-monotonic Clean ps = ≤ₚ-refl (fold-worst ps) -fold-worst-prepend-monotonic ClassicalAxioms Clean = clean≤ -fold-worst-prepend-monotonic ClassicalAxioms ClassicalAxioms = class≤c -fold-worst-prepend-monotonic ClassicalAxioms IncompleteProof = inc≤i -fold-worst-prepend-monotonic ClassicalAxioms Rejected = rej≤r -fold-worst-prepend-monotonic IncompleteProof Clean = clean≤ -fold-worst-prepend-monotonic IncompleteProof ClassicalAxioms = class≤i -fold-worst-prepend-monotonic IncompleteProof IncompleteProof = inc≤i -fold-worst-prepend-monotonic IncompleteProof Rejected = rej≤r -fold-worst-prepend-monotonic Rejected Clean = clean≤ -fold-worst-prepend-monotonic Rejected ClassicalAxioms = class≤r -fold-worst-prepend-monotonic Rejected IncompleteProof = inc≤r -fold-worst-prepend-monotonic Rejected Rejected = rej≤r +fold-worst-prepend-monotonic p ps = worst-ub-right p (fold-worst ps) ------------------------------------------------------------------------ -- THEOREM 4: Empty registry produces Clean @@ -138,30 +127,10 @@ reject-head-propagates _ = refl worst-policy-rejected-inv : ∀ (a b : AxiomPolicy) → worst-policy a b ≡ Rejected → (a ≡ Rejected) ⊎ (b ≡ Rejected) - where - data _⊎_ (A B : Set) : Set where - inj₁ : A → A ⊎ B - inj₂ : B → A ⊎ B worst-policy-rejected-inv Rejected _ _ = inj₁ refl - where - data _⊎_ (A B : Set) : Set where - inj₁ : A → A ⊎ B - inj₂ : B → A ⊎ B worst-policy-rejected-inv IncompleteProof Rejected _ = inj₂ refl - where - data _⊎_ (A B : Set) : Set where - inj₁ : A → A ⊎ B - inj₂ : B → A ⊎ B worst-policy-rejected-inv ClassicalAxioms Rejected _ = inj₂ refl - where - data _⊎_ (A B : Set) : Set where - inj₁ : A → A ⊎ B - inj₂ : B → A ⊎ B worst-policy-rejected-inv Clean Rejected _ = inj₂ refl - where - data _⊎_ (A B : Set) : Set where - inj₁ : A → A ⊎ B - inj₂ : B → A ⊎ B ------------------------------------------------------------------------ -- THEOREM 7: Rejected is absorbing on the left in worst-policy diff --git a/meta-checker/src/Echidna/ClampTrust.agda b/meta-checker/src/Echidna/ClampTrust.agda new file mode 100644 index 00000000..58eb5dae --- /dev/null +++ b/meta-checker/src/Echidna/ClampTrust.agda @@ -0,0 +1,149 @@ +------------------------------------------------------------------------ +-- Clamp Trust Bounds — semantic rewrite of the Idris2 obligation +-- +-- verification/proofs/idris2/ClampTrustBounds.idr states four +-- obligations for `clamp_trust : Nat → TrustLevel`. That corpus is out +-- of policy per PROOF-POLICY §3 (engineering claims about this +-- repository's own types are Idris2/Agda territory, but the corpus is +-- not wired into any gate and there is no `idris2` binary in CI that +-- runs it). This module restates the same obligations over the +-- trust-level type that the meta-checker already proves things about, +-- so that they are checked by the gate that actually runs. +-- +-- Obligations covered: +-- clamp-lower : trust-to-ℕ (clamp-trust n) ≥ 1 +-- clamp-upper : trust-to-ℕ (clamp-trust n) ≤ 5 +-- clamp-monotone : n ≤ m → clamp-trust n ≤ₜ clamp-trust m +-- clamp-fixed-1 : clamp-trust 1 ≡ Level1 +-- clamp-fixed-5 : clamp-trust 5 ≡ Level5 +-- clamp-fixed-10 : clamp-trust 10 ≡ Level5 +-- clamp-roundtrip : the clamp lands on a real level, not between two +-- +-- Checked with: agda --safe --without-K --cubical-compatible +------------------------------------------------------------------------ + +module Echidna.ClampTrust where + +open import Data.Empty using (⊥) +open import Data.Nat using (ℕ; zero; suc; _≤_; _+_; z≤n; s≤s) +open import Data.Nat.Properties using (+-suc; +-identityʳ) +open import Data.Product using (∃-syntax; _,_) +open import Relation.Binary.PropositionalEquality + using (_≡_; refl; sym; trans; cong; subst) + +open import Echidna.TrustLevel using + ( TrustLevel + ; Level1; Level2; Level3; Level4; Level5 + ; _≤ₜ_; ≤ₜ-refl; ≤ₜ-trans; l1≤; l2≤3; l3≤4; l4≤5; l5≤5 + ; trust-to-ℕ + ) + +------------------------------------------------------------------------ +-- The clamp, exactly as the Idris2 model defines it +------------------------------------------------------------------------ + +clamp-trust : ℕ → TrustLevel +clamp-trust zero = Level1 +clamp-trust (suc zero) = Level1 +clamp-trust (suc (suc zero)) = Level2 +clamp-trust (suc (suc (suc zero))) = Level3 +clamp-trust (suc (suc (suc (suc zero)))) = Level4 +clamp-trust (suc (suc (suc (suc (suc _))))) = Level5 + +------------------------------------------------------------------------ +-- Bounds +------------------------------------------------------------------------ + +clamp-lower : ∀ n → suc zero ≤ trust-to-ℕ (clamp-trust n) +clamp-lower zero = s≤s z≤n +clamp-lower (suc zero) = s≤s z≤n +clamp-lower (suc (suc zero)) = s≤s z≤n +clamp-lower (suc (suc (suc zero))) = s≤s z≤n +clamp-lower (suc (suc (suc (suc zero)))) = s≤s z≤n +clamp-lower (suc (suc (suc (suc (suc _))))) = s≤s z≤n + +clamp-upper : + ∀ n → trust-to-ℕ (clamp-trust n) ≤ suc (suc (suc (suc (suc zero)))) +clamp-upper zero = s≤s z≤n +clamp-upper (suc zero) = s≤s z≤n +clamp-upper (suc (suc zero)) = s≤s (s≤s z≤n) +clamp-upper (suc (suc (suc zero))) = s≤s (s≤s (s≤s z≤n)) +clamp-upper (suc (suc (suc (suc zero)))) = s≤s (s≤s (s≤s (s≤s z≤n))) +clamp-upper (suc (suc (suc (suc (suc _))))) = s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))) + +------------------------------------------------------------------------ +-- Monotonicity +-- +-- The clamp is not suc-closed in the trust order, so induction on the +-- `≤` witness does not go through. Instead: every `n ≤ m` decomposes as +-- `m ≡ k + n`, and the clamp advances by one `clamp-step` per successor. +------------------------------------------------------------------------ + +-- One step never decreases trust. +clamp-step : ∀ n → clamp-trust n ≤ₜ clamp-trust (suc n) +clamp-step zero = l1≤ +clamp-step (suc zero) = l1≤ +clamp-step (suc (suc zero)) = l2≤3 +clamp-step (suc (suc (suc zero))) = l3≤4 +clamp-step (suc (suc (suc (suc zero)))) = l4≤5 +clamp-step (suc (suc (suc (suc (suc _))))) = l5≤5 + +-- Difference decomposition: n ≤ m means m is n plus some k. +≤-difference : ∀ {n m} → n ≤ m → ∃[ k ] (m ≡ k + n) +-- helper keeps the Σ witness explicit, so no with-abstraction surprises +≤-difference-step : ∀ {a b} → ∃[ k ] (b ≡ k + a) → ∃[ k ] (suc b ≡ k + suc a) +≤-difference-step {a} (k , eq) = + k , trans (cong suc eq) (sym (+-suc k a)) + +≤-difference {zero} {m} z≤n = m , sym (+-identityʳ m) +≤-difference {suc a} {suc b} (s≤s p) = ≤-difference-step {a} (≤-difference p) + +-- k successor steps +clamp-chain : ∀ n k → clamp-trust n ≤ₜ clamp-trust (k + n) +clamp-chain n zero = ≤ₜ-refl (clamp-trust n) +clamp-chain n (suc k) = ≤ₜ-trans (clamp-chain n k) (clamp-step (k + n)) + +clamp-monotone : ∀ {n m} → n ≤ m → clamp-trust n ≤ₜ clamp-trust m +clamp-monotone {n} p with ≤-difference p +... | k , eq = + subst (λ z → clamp-trust n ≤ₜ clamp-trust z) (sym eq) (clamp-chain n k) + + +------------------------------------------------------------------------ +-- Fixed points +------------------------------------------------------------------------ + +clamp-fixed-1 : clamp-trust (suc zero) ≡ Level1 +clamp-fixed-1 = refl + +clamp-fixed-0 : clamp-trust zero ≡ Level1 +clamp-fixed-0 = refl + +clamp-fixed-5 : clamp-trust (suc (suc (suc (suc (suc zero))))) ≡ Level5 +clamp-fixed-5 = refl + +clamp-fixed-10 : + clamp-trust (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))) + ≡ Level5 +clamp-fixed-10 = refl + +clamp-above : ∀ k → + clamp-trust (suc (suc (suc (suc (suc k))))) ≡ Level5 +clamp-above k = refl + +------------------------------------------------------------------------ +-- Totality into the enumeration +-- +-- The point of clamping is that the result is a real trust level, not a +-- number sitting between two of them. Idempotence of the numeric +-- projection is that statement. +------------------------------------------------------------------------ + +clamp-idempotent : ∀ n → trust-to-ℕ (clamp-trust (trust-to-ℕ (clamp-trust n))) + ≡ trust-to-ℕ (clamp-trust n) +clamp-idempotent zero = refl +clamp-idempotent (suc zero) = refl +clamp-idempotent (suc (suc zero)) = refl +clamp-idempotent (suc (suc (suc zero))) = refl +clamp-idempotent (suc (suc (suc (suc zero)))) = refl +clamp-idempotent (suc (suc (suc (suc (suc _))))) = refl diff --git a/meta-checker/src/Echidna/Integrity.agda b/meta-checker/src/Echidna/Integrity.agda new file mode 100644 index 00000000..85394621 --- /dev/null +++ b/meta-checker/src/Echidna/Integrity.agda @@ -0,0 +1,137 @@ +------------------------------------------------------------------------ +-- Solver Integrity — semantic rewrite of obligation E11 +-- +-- The current repository has an informal note for E11 and no Agda +-- record. This module states the invariant that the integrity checker +-- is *supposed* to guarantee, and then proves the sharpness result +-- that makes the collision-resistance assumption load-bearing rather +-- than decorative. +-- +-- The headline theorem is the one the Rust implementation violates: +-- an UNINITIALISED manifest must never yield `Verified`. +-- src/rust/dispatch.rs:642,848,998 and +-- src/rust/integrity/solver_integrity.rs:359 all accept +-- `IntegrityStatus::Uninitialized` as passing. The proof below is about +-- the specification, not about that code path — which is exactly why it +-- is worth having a record: it makes the deviation a machine-checked +-- discrepancy (DEBT D9) instead of a reading of the source. +-- +-- Checked with: agda --safe --without-K --cubical-compatible +------------------------------------------------------------------------ + +module Echidna.Integrity where + +open import Data.Bool using (Bool; true; false) +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Product using (Σ-syntax; _×_; _,_) +open import Data.Unit using (⊤; tt) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym) +open import Relation.Nullary using (¬_) + +------------------------------------------------------------------------ +-- Collision resistance, carried as a record field +-- +-- This is deliberately an *assumption recorded in a structure* rather +-- than a postulate: the theorems below are parameterised by it, so the +-- guarantee they give is conditional and says so in its type. +------------------------------------------------------------------------ + +record Hash : Set₁ where + field + Digest : Set + _≈d_ : Digest → Digest → Bool + ≈d-sound : ∀ {d e} → _≈d_ d e ≡ true → d ≡ e + +module _ (H : Hash) where + open Hash H + + ---------------------------------------------------------------------- + -- Manifest and result + ---------------------------------------------------------------------- + + data Manifest : Set where + Uninitialised : Manifest -- nothing to compare against + Initialised : Digest → Manifest -- expected digest recorded + + data Result : Set where + Verified : Result + Mismatch : Result + Missing : Result + + decide : Bool → Result + decide true = Verified + decide false = Mismatch + + record Binary : Set where + field digest : Digest + open Binary public + + -- The specified checker. Note the first line: an uninitialised + -- manifest produces `Missing`, never `Verified`. + check : Manifest → Binary → Result + check Uninitialised _ = Missing + check (Initialised d) b = decide (_≈d_ d (digest b)) + + ---------------------------------------------------------------------- + -- Inversion of the decider + ---------------------------------------------------------------------- + + decide-verified : ∀ {x} → decide x ≡ Verified → x ≡ true + decide-verified {true} _ = refl + decide-verified {false} () + + ---------------------------------------------------------------------- + -- THEOREMS + ---------------------------------------------------------------------- + + -- E11a. Verification requires a manifest. + verified-needs-manifest : + ∀ {m b} → check m b ≡ Verified → Σ[ d ∈ Digest ] (m ≡ Initialised d) + verified-needs-manifest {Uninitialised} {b} () + verified-needs-manifest {Initialised d} {b} _ = d , refl + + -- E11b. Verification means the recorded digest was matched. + verified-means-match : + ∀ {d b} → check (Initialised d) b ≡ Verified → d ≡ digest b + verified-means-match {d} {b} p = ≈d-sound (decide-verified p) + + -- E11c. A substituted binary is never verified. + substituted-never-verified : + ∀ {d b} → ¬ (digest b ≡ d) → ¬ (check (Initialised d) b ≡ Verified) + substituted-never-verified {d} {b} neq p = + neq (sym (verified-means-match {d} {b} p)) + + -- E11d. THE INVARIANT THE IMPLEMENTATION BREAKS (DEBT D9): + -- an uninitialised manifest never yields `Verified`. + uninitialised-never-verified : + ∀ b → ¬ (check Uninitialised b ≡ Verified) + uninitialised-never-verified b () + +------------------------------------------------------------------------ +-- Sharpness: the assumption is load-bearing +-- +-- Without `≈d-sound`, verification does not imply anything about the +-- binary. This is proved by exhibiting a comparator that accepts +-- everything, under which a manifest for `true` verifies a binary whose +-- digest is `false`. +------------------------------------------------------------------------ + +record UnsoundHash : Set₁ where + field + Digest : Set + _≈d_ : Digest → Digest → Bool + +-- A comparator that accepts everything: collision resistance fails. +always-true : UnsoundHash +UnsoundHash.Digest always-true = Bool +UnsoundHash._≈d_ always-true _ _ = true + +-- The digests of two distinct binaries are declared equal... +sharpness : UnsoundHash._≈d_ always-true true false ≡ true +sharpness = refl + +-- ...while they demonstrably are not. Hence no inhabitant of +-- `≈d-sound always-true` exists, and E11b cannot be discharged for this +-- comparator: the hypothesis in `Hash` is doing real work. +sharpness-matters : ¬ (true ≡ false) +sharpness-matters () diff --git a/meta-checker/src/Echidna/MetaChecker.agda b/meta-checker/src/Echidna/MetaChecker.agda index c6eb3e72..34c17bb2 100644 --- a/meta-checker/src/Echidna/MetaChecker.agda +++ b/meta-checker/src/Echidna/MetaChecker.agda @@ -35,8 +35,41 @@ -- ✓ Pipeline is monotonically degrading -- ✓ Pipeline is deterministic -- --- TOTAL: 30+ proven properties, 0 postulates (except funext in AxiomSafety), +-- FROM AxiomTrackerCompleteness: +-- ✓ Scan-entry preserves length (no silent omissions) +-- ✓ Fold distributes over append +-- ✓ Prepending a policy never lowers the folded result +-- ✓ Empty registry folds to Clean +-- ✓ A single DC-Reject pattern is always caught +-- ✓ Rejected is absorbing, and Rejected is detected on either side +-- +-- FROM Receipt (epistemic-types semantic rewrite): +-- ✓ A receipt is factive; a warrant is not +-- ✓ A warrant never promotes to a receipt ("no free promotion") +-- ✓ No receipt exists while the agent cannot discriminate the worlds +-- ✓ A discriminating check yields a receipt +-- +-- FROM Integrity (E11 semantic rewrite): +-- ✓ Verification requires an initialised manifest +-- ✓ Verification means the recorded digest was matched +-- ✓ An uninitialised manifest NEVER verifies (the invariant DEBT D9 breaks) +-- ✓ The collision-resistance hypothesis is load-bearing (sharpness) +-- +-- FROM ClampTrust (ClampTrustBounds semantic rewrite): +-- ✓ The clamp stays within [1,5] +-- ✓ The clamp is monotone in the trust order +-- ✓ Fixed points 0/1 -> Level1, >=5 -> Level5 +-- ✓ The clamp is idempotent +-- +-- TOTAL: 45+ proven properties, 0 postulates, 0 assumptions, -- 0 sorry, 0 believe_me, 0 Admitted. +-- +-- Canonical invocation (PROOF-POLICY §2.1): +-- agda --safe --without-K --cubical-compatible src/Echidna/MetaChecker.agda +-- This emits -W[no]UnsupportedIndexedMatch for the indexed pattern matches +-- in TrustLevel (≤ₜ-antisym, ≤ₜ-trans) and ClampTrust (≤-difference). Those +-- functions therefore do not compute under Cubical transports. The build is +-- `--cubical-compatible`, NOT `--cubical`: see docs/PROOF-STATUS.adoc R4. module Echidna.MetaChecker where @@ -45,6 +78,10 @@ open import Echidna.TrustLevel public open import Echidna.AxiomSafety public open import Echidna.Portfolio public open import Echidna.Dispatch public +open import Echidna.Receipt public +open import Echidna.Integrity public +open import Echidna.ClampTrust public +open import Echidna.AxiomTrackerCompleteness public ------------------------------------------------------------------------ -- Summary: Key safety invariants proven @@ -75,3 +112,24 @@ key-order-1 = ≤ₜ-refl key-order-2 = ≤ₜ-antisym key-order-3 = ≤ₜ-trans key-order-4 = ≤ₜ-total + +-- 8. Epistemic separation: a warrant is never a receipt +key-epistemic-1 = receipt-factive +key-epistemic-2 = warrant-not-factive +key-epistemic-3 = no-free-promotion + +-- 9. Integrity: an uninitialised manifest never verifies (DEBT D9) +key-integrity-1 = uninitialised-never-verified +key-integrity-2 = verified-means-match + +-- 10. Clamp bounds and monotonicity +key-clamp-1 = clamp-lower +key-clamp-2 = clamp-upper +key-clamp-3 = clamp-monotone +key-clamp-4 = clamp-idempotent + +-- 11. Axiom-tracker completeness +key-tracker-1 = scan-entry-length +key-tracker-2 = fold-worst-++ +key-tracker-3 = single-reject-detected +key-tracker-4 = worst-policy-rejected-inv diff --git a/meta-checker/src/Echidna/Receipt.agda b/meta-checker/src/Echidna/Receipt.agda new file mode 100644 index 00000000..a098979b --- /dev/null +++ b/meta-checker/src/Echidna/Receipt.agda @@ -0,0 +1,168 @@ +------------------------------------------------------------------------ +-- Receipt vs Warrant +-- +-- Semantic rewrite (not a mechanical port) of the receipt/warrant +-- distinction developed in the strict-safe Agda development at +-- epistemic-types@5422cd5. There, "warrant" and "receipt" are kept +-- distinct: a warrant is evidence *about* a claim, a receipt is the +-- claim's proof. This module carries that distinction into ECHIDNA's +-- proof vocabulary, where per PROOF-POLICY §5 only `proven` may assert +-- the proposition and `argued` must not. +-- +-- The argument is a two-world Kripke countermodel: an agent holding a +-- warrant cannot distinguish the world in which the verdict is sound +-- from one in which it is not. A receipt is exactly what closes that +-- gap — a discriminating check, not more of the same evidence. +-- +-- Checked with: agda --safe --without-K --cubical-compatible +-- (no postulates, no assumptions; the only hypothesis is the +-- discriminating check in the final section, and it is a parameter) +------------------------------------------------------------------------ + +module Echidna.Receipt where + +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Product using (Σ-syntax; _×_; _,_) +open import Data.Unit using (⊤; tt) + +------------------------------------------------------------------------ +-- Kripke frame +-- +-- Two worlds that the agent cannot tell apart. `w-here` is the world +-- the run actually happened in; `w-there` is an indistinguishable +-- alternative — e.g. the world in which the solver was substituted, or +-- the manifest was uninitialised, and the verdict is unsound. +------------------------------------------------------------------------ + +data World : Set where + w-here : World + w-there : World + +data _≈_ : World → World → Set where + ≈-here : w-here ≈ w-here + ≈-there : w-there ≈ w-there + ≈-cross : w-here ≈ w-there + ≈-cross′ : w-there ≈ w-here + +≈-refl : ∀ w → w ≈ w +≈-refl w-here = ≈-here +≈-refl w-there = ≈-there + +------------------------------------------------------------------------ +-- One proposition: "the prover's verdict is sound" +------------------------------------------------------------------------ + +data Atom : Set where + sound : Atom + +⟦_⟧ : Atom → World → Set +⟦ sound ⟧ w-here = ⊤ +⟦ sound ⟧ w-there = ⊥ + +------------------------------------------------------------------------ +-- Receipts: agent-invariant +-- +-- A receipt is a proof the agent can carry: it holds at every world the +-- agent cannot rule out. This is the Kripke reading of "checked". +------------------------------------------------------------------------ + +Receipt : Atom → World → Set +Receipt φ w = ∀ {w′} → w ≈ w′ → ⟦ φ ⟧ w′ + +-- A receipt is factive. This is the property `proven` asserts and +-- `argued` does not. +receipt-factive : ∀ {φ w} → Receipt φ w → ⟦ φ ⟧ w +receipt-factive r = r (≈-refl _) + +------------------------------------------------------------------------ +-- Warrants: agent-relative +-- +-- A warrant is evidence collected somewhere, plus the fact that the +-- agent cannot rule that somewhere out. It is deliberately *not* +-- indexed by success: it is a claim about the evidence, not about the +-- world. +------------------------------------------------------------------------ + +data Evidence : Atom → Set where + ev-sound : Evidence sound -- e.g. a certificate the prover emitted + +-- Where the evidence came from. The agent hopes it is `w-here`. +grounds : ∀ {φ} → Evidence φ → World +grounds {φ} _ = w-here + +Warrant : Atom → World → Set +Warrant φ w = Σ[ e ∈ Evidence φ ] (w ≈ grounds e) × ⟦ φ ⟧ (grounds e) + +-- An agent standing at `w-there` holds a warrant for `sound`. +warrant-elsewhere : Warrant sound w-there +warrant-elsewhere = ev-sound , ≈-cross′ , tt + +------------------------------------------------------------------------ +-- THEOREM (non-factivity): a warrant does not entail its claim +-- +-- There is a world in which the agent is warranted in asserting the +-- claim and the claim is false. So `argued` may never be read as +-- `proven`, however many times the evidence is re-run. +------------------------------------------------------------------------ + +warrant-not-factive : + Σ[ w ∈ World ] (Warrant sound w × (⟦ sound ⟧ w → ⊥)) +warrant-not-factive = w-there , warrant-elsewhere , λ z → z + +------------------------------------------------------------------------ +-- THEOREM (no free promotion): a warrant is not a receipt +------------------------------------------------------------------------ + +warrant-not-receipt : Warrant sound w-there → Receipt sound w-there → ⊥ +warrant-not-receipt _ r = r ≈-there + +-- Stronger: because the agent cannot exclude `w-there`, no receipt for +-- `sound` exists at *either* world. Accumulating more evidence of the +-- same kind cannot produce one; only a check that discriminates can. +no-receipt-anywhere : ∀ w → Receipt sound w → ⊥ +no-receipt-anywhere w-here r = r ≈-cross +no-receipt-anywhere w-there r = r ≈-there + +------------------------------------------------------------------------ +-- Constructive counterpart: a discriminating check yields a receipt +-- +-- The hypothesis is a *parameter*, not a postulate: any caller that +-- supplies such a check gets a receipt for free. In ECHIDNA terms this +-- is an independently checked certificate (Rocq/Lean re-check, or +-- statement comparison across two kernels) — precisely the evidence +-- R5 is missing. +------------------------------------------------------------------------ + +module _ (discriminates : w-here ≈ w-there → ⊥) where + + receipt-from-check : Receipt sound w-here + receipt-from-check {w-here} _ = tt + receipt-from-check {w-there} r = ⊥-elim (discriminates r) + +------------------------------------------------------------------------ +-- Token discipline +-- +-- What each PROOF-POLICY §5 token asserts, as a function of the +-- proposition it is about, and the theorem that strengthening a token +-- is not free. +------------------------------------------------------------------------ + +data Verdict : Set where + proven : Verdict + proven-with-postulates : Verdict + tested-only : Verdict + argued : Verdict + no-claim : Verdict -- the `open` token (`open` is a keyword) + +Asserts : Verdict → (φ : Atom) → World → Set +Asserts proven φ w = Receipt φ w +Asserts proven-with-postulates φ w = Receipt φ w +Asserts tested-only φ w = Warrant φ w +Asserts argued φ w = Warrant φ w +Asserts no-claim φ w = ⊤ + +-- The same warrant never licences the stronger token. +no-free-promotion : + ∀ {φ w} → Asserts argued φ w → Asserts proven φ w → ⊥ +no-free-promotion {sound} {w-here} _ r = r ≈-cross +no-free-promotion {sound} {w-there} _ r = r ≈-there diff --git a/scripts/install-proof-toolchains.sh b/scripts/install-proof-toolchains.sh index 088a8317..af44667e 100755 --- a/scripts/install-proof-toolchains.sh +++ b/scripts/install-proof-toolchains.sh @@ -11,6 +11,27 @@ # Target: Ubuntu 24.04 (the Claude-on-web / GitHub-Actions base). On any other # host, or without root, it prints a note and exits 0 rather than breaking the # session. +# +# ── Restricted environments: what actually works (2026-11-01) ─────────────── +# A sandbox with no root, no apt, and no access to static.rust-lang.org, +# sh.rustup.rs, deb.debian.org or GitHub *release assets* cannot run the body of +# this script: every download below targets one of those hosts. Verified there: +# only an Agda leg is obtainable, via the PyPI wheel, and even that needs the +# compiler's data/lib directory populated by hand because the wheel omits it: +# +# pip install --target /tmp/py-tc agda # Agda 2.7.0.1 +# PYTHONPATH=/tmp/py-tc PATH=/tmp/py-tc/bin:$PATH +# mkdir -p /tmp/py-tc/agda/data/lib # wheel ships no primitives +# # copy src/data from the v2.7.0.1 tag into /tmp/py-tc/agda/data/ +# # stdlib: codeload.github.com/agda/agda-stdlib/tar.gz/refs/tags/v2.1 +# export LC_ALL=C.UTF-8 # Unicode identifiers +# +# Then check with the PROOF-POLICY §2.1 flags: +# agda --safe --without-K --cubical-compatible src/Echidna/MetaChecker.agda +# +# No Rust, Creusot, Lean 4, Idris 2, Coq, Z3 or cvc5 leg was obtainable that way, +# and PROOF-POLICY §6 says to report such legs as *not run* rather than as +# passing. Do not weaken the flags to produce a green log — §2.1 forbids it. set -euo pipefail LEAN_VERSION="4.13.0" diff --git a/site/docs/api/graphql.adoc b/site/docs/api/graphql.adoc index 03735e91..b4f235e1 100644 --- a/site/docs/api/graphql.adoc +++ b/site/docs/api/graphql.adoc @@ -1,10 +1,22 @@ == GraphQL Interface Reference The `+echidna-graphql+` binary is an optional self-hosted service. It -binds `+127.0.0.1:8081+` over plain HTTP and serves both the GraphQL -endpoint and the interactive playground at the server root — a `+POST+` -to `+/+` executes operations, a `+GET+` renders the playground. There is -a separate `+GET /health+`. +binds `+127.0.0.1:8081+` by default over plain HTTP and serves both the +GraphQL endpoint and the interactive playground at the server root — a +`+POST+` to `+/+` executes operations, a `+GET+` renders the playground. +There is a separate `+GET /health+`. + +`+8081+` is also the default port of the core `+echidna server+`, so the two +cannot run side by side on defaults. Override this one: + +[source,bash] +---- +ECHIDNA_GRAPHQL_ADDR=127.0.0.1:8082 ./echidna-graphql +---- + +GraphQL operations and the REST `+/api/+*` routes are *separate code paths*: +a GraphQL `+verifyProof+` does not pass through the same dispatch as +`+POST /api/prove+`. Documented from `+src/interfaces/graphql/{main,schema}.rs+`. diff --git a/site/docs/index.adoc b/site/docs/index.adoc index 67d96d29..46d588fa 100644 --- a/site/docs/index.adoc +++ b/site/docs/index.adoc @@ -56,6 +56,9 @@ link:/docs/api/rest.html[REST interface reference]. Endpoint and interactive playground both at the server root — see the link:/docs/api/graphql.html[GraphQL interface reference]. +The default port collides with the core server above (also 8081): only one +of the two can bind. Set `+ECHIDNA_GRAPHQL_ADDR+` to run both. + ==== gRPC interface (port 50051) See the link:/docs/api/grpc.html[gRPC interface reference] and the proto @@ -66,7 +69,11 @@ definition at `+src/interfaces/grpc/proto/echidna.proto+`. ECHIDNA follows a trust-hardened architecture: [arabic] -. *Solver Binary Integrity* — SHAKE3-512 + BLAKE3 verification +. *Solver Binary Integrity* — SHAKE3-512 + BLAKE3 verification. Capability +present, *not currently engaged*: no caller attaches an integrity checker in +this release, so proofs are checked with solver identity assumed. The +manifest at `+config/solver-manifest.toml+` also still carries placeholder +hashes. Reported plainly rather than implied. . *SMT Portfolio Solving* — cross-checking across solvers . *Proof Certificate Checking* — Alethe, DRAT/LRAT, TSTP . *Axiom Usage Tracking* — 4 danger levels (Safe, Noted, Warning, diff --git a/src/interfaces/graphql/main.rs b/src/interfaces/graphql/main.rs index 975f3a2b..01d94a3d 100644 --- a/src/interfaces/graphql/main.rs +++ b/src/interfaces/graphql/main.rs @@ -36,11 +36,19 @@ async fn main() { .route("/health", get(health_check)) .layer(CorsLayer::permissive()); - let addr = "127.0.0.1:8081"; + // Bind address. Default unchanged (127.0.0.1:8081) so nothing that already + // pins it breaks, but it collides with `echidna server`, whose --port also + // defaults to 8081: whichever starts second cannot bind. A deployment that + // wants both on one host sets ECHIDNA_GRAPHQL_ADDR for this one, e.g. + // ECHIDNA_GRAPHQL_ADDR=127.0.0.1:8082 echidna-graphql + // See docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc §6 RD2 and + // the one-port-per-project rule in standards 0-canon/PORT-REGISTRY.adoc. + let addr = std::env::var("ECHIDNA_GRAPHQL_ADDR") + .unwrap_or_else(|_| "127.0.0.1:8081".to_string()); tracing::info!("GraphQL server listening on http://{}", addr); tracing::info!("GraphQL playground available at http://{}/", addr); - let listener = tokio::net::TcpListener::bind(addr).await.unwrap(); + let listener = tokio::net::TcpListener::bind(&addr).await.unwrap(); axum::serve(listener, app).await.unwrap(); } From a68b60179c204e080a3f858bff597ff8d4a4f0f4 Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 1 Nov 2026 17:53:03 +0000 Subject: [PATCH 2/5] fix(fmt): rustfmt-clean the ECHIDNA_GRAPHQL_ADDR binding MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Cargo fmt --check failed in rust-ci: rustfmt prefers breaking after the '=' when the whole expression fits on the continuation line, which this one does (95 cols). Matches the existing idiom at src/rust/server.rs:71 and :1043 rather than the chain break I wrote first. Note for review: rust-ci / Cargo audit and Cargo audit (security) fail repo-wide since 2026-10-30 on branches with no dependency changes (this one included) — pre-existing, not addressed here. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- src/interfaces/graphql/main.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/interfaces/graphql/main.rs b/src/interfaces/graphql/main.rs index 01d94a3d..771cce04 100644 --- a/src/interfaces/graphql/main.rs +++ b/src/interfaces/graphql/main.rs @@ -43,8 +43,8 @@ async fn main() { // ECHIDNA_GRAPHQL_ADDR=127.0.0.1:8082 echidna-graphql // See docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc §6 RD2 and // the one-port-per-project rule in standards 0-canon/PORT-REGISTRY.adoc. - let addr = std::env::var("ECHIDNA_GRAPHQL_ADDR") - .unwrap_or_else(|_| "127.0.0.1:8081".to_string()); + let addr = + std::env::var("ECHIDNA_GRAPHQL_ADDR").unwrap_or_else(|_| "127.0.0.1:8081".to_string()); tracing::info!("GraphQL server listening on http://{}", addr); tracing::info!("GraphQL playground available at http://{}/", addr); From 4b6fd979cbd5e4188554ba77d47d2224f66fa8f0 Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 1 Nov 2026 17:59:11 +0000 Subject: [PATCH 3/5] review: address blocking findings from the automated review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Substantive (my claims were wrong or the model was vacuous): - Receipt.agda: the 'discriminating check' was a parameter that no function could supply (≈-cross inhabits its domain), so that section proved nothing. Replaced with a second frame: same worlds, sharper accessibility, a real receipt, and coarse-yet-sharpened stating the contrast. - Receipt.agda: proven-with-postulates asserted the same type as proven, erasing the policy's distinction; it now carries a named axiom. - ARCHITECTURE.adoc opening invariant still claimed binaries are integrity-checked before invocation while the detail section says the step never runs. Reworded; solver identity is now stated as assumed. - PROOF-STATUS: 'No row is above argued' contradicted R4/R9/R10/R11. - Integrity.agda: scope stated (digests, not bytes); sharpness consequence now proved rather than asserted in a comment. Real defects: - container/Containerfile healthcheck probed /health; the server serves /api/health — the container would go unhealthy after start. Same for the k9 health/readiness probes (there is no /ready route at all). - agda-meta-checker.yml closure step compared totals and used a non-recursive glob; now checks each source against its own interface. - install-proof-toolchains.sh recipe: register the stdlib (a download alone does not resolve the depend:), and run agda from meta-checker/. - Missing SPDX headers on the three new Agda modules. - QUICKSTART: /api/verify_parallel also reaches the dispatcher. - Stale last-updated/L last-updated metadata; ClampTrust header named a theorem that does not exist. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/agda-meta-checker.yml | 31 +++++--- QUICKSTART-USER.adoc | 5 +- container/Containerfile | 2 +- container/deploy.k9.ncl | 6 +- docs/ARCHITECTURE.adoc | 10 ++- docs/ECOSYSTEM-INTEGRATION.adoc | 2 +- docs/PROOF-STATUS.adoc | 22 +++++- .../descriptiles/NEUROSYM.a2ml | 2 +- meta-checker/src/Echidna/ClampTrust.agda | 7 +- meta-checker/src/Echidna/Integrity.agda | 19 ++++- meta-checker/src/Echidna/MetaChecker.agda | 12 ++- meta-checker/src/Echidna/Receipt.agda | 78 +++++++++++++++---- scripts/install-proof-toolchains.sh | 13 +++- 13 files changed, 160 insertions(+), 49 deletions(-) diff --git a/.github/workflows/agda-meta-checker.yml b/.github/workflows/agda-meta-checker.yml index 774186e8..b2151d86 100644 --- a/.github/workflows/agda-meta-checker.yml +++ b/.github/workflows/agda-meta-checker.yml @@ -118,14 +118,23 @@ jobs: 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. Guard against a - # repeat: every source module must yield an interface. - src=$(ls src/Echidna/*.agda | wc -l) - iface=$(find . -name '*.agdai' | wc -l) - echo "source modules: $src, interfaces produced: $iface" - if [ "$src" -ne "$iface" ]; then - echo "::error::${src} modules but ${iface} interfaces — at least one module is outside the checked closure" - ls -1 src/Echidna/*.agda - exit 1 - fi - echo "✓ ${iface} modules type-checked under the PROOF-POLICY §2.1 flags" + # 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//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 diff --git a/QUICKSTART-USER.adoc b/QUICKSTART-USER.adoc index ccc4378e..a07ec2c5 100644 --- a/QUICKSTART-USER.adoc +++ b/QUICKSTART-USER.adoc @@ -135,8 +135,9 @@ The full route table is in `src/rust/server.rs`. Separate GraphQL / gRPC / REST interface crates live under `src/interfaces/` (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, and the trust pipeline is reached only by `/api/prove` -in a `--features verisim` build. +`/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 diff --git a/container/Containerfile b/container/Containerfile index 13d75960..ef8f4fa9 100644 --- a/container/Containerfile +++ b/container/Containerfile @@ -75,6 +75,6 @@ USER appuser 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"] diff --git a/container/deploy.k9.ncl b/container/deploy.k9.ncl index 3165f868..ca235e5c 100644 --- a/container/deploy.k9.ncl +++ b/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", diff --git a/docs/ARCHITECTURE.adoc b/docs/ARCHITECTURE.adoc index 1e95eebb..7b60fdac 100644 --- a/docs/ARCHITECTURE.adoc +++ b/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 diff --git a/docs/ECOSYSTEM-INTEGRATION.adoc b/docs/ECOSYSTEM-INTEGRATION.adoc index 00ae7aa1..e882eca2 100644 --- a/docs/ECOSYSTEM-INTEGRATION.adoc +++ b/docs/ECOSYSTEM-INTEGRATION.adoc @@ -199,5 +199,5 @@ Not created yet ''''' -*Last Updated*: 2026-02-12 *Maintained By*: Jonathan D.A. Jewell +*Last Updated*: 2026-11-01 *Maintained By*: Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index 07701b3e..3a397719 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -205,6 +205,13 @@ resistance is a record *field*, not a postulate, so the guarantee is conditional and says so in its type; `+sharpness+` exhibits a comparator for which that field cannot be inhabited, so the hypothesis is load-bearing rather than decorative. +**Scope of the model (from review, 2026-11-01):** a binary is modelled by its +digest alone, so these are statements about *digests*, not bytes. +"Substituted" means "a binary whose digest differs", and two binaries colliding +on a digest are not distinguished by this model. Content-level collision +resistance sits in the `≈d-sound` field of the comparator — assumed, not +established. That is what makes the sharpness result the load-bearing part. + |**Specification, not implementation.** `+src/rust/dispatch.rs+` lines 642, 848 and 998, and `+src/rust/integrity/solver_integrity.rs+` line 359, all accept `+IntegrityStatus::Uninitialized+` as passing. The theorem proves the opposite @@ -230,7 +237,11 @@ plus transitivity rather than the Idris2 file's 36-clause decision table. |`+meta-checker/src/Echidna/Receipt.agda+`, inside the R4 receipt. A two-world Kripke countermodel: a receipt is factive, a warrant is not; the same warrant never licences the stronger token; while the agent cannot discriminate the -worlds, no receipt exists at all; a discriminating check parameter yields one. +worlds, no receipt exists at all; and a second frame — same worlds, only the +accessibility changed — has a receipt, so what buys one is *excluding the +alternative*, not accumulating more evidence. (An earlier draft took the +discriminating check as a parameter; that was vacuous, since `≈-cross` +inhabits the domain of the function required. Two frames say it properly.) This is what makes §5's "`+argued+` is not `+proven+`" a theorem instead of a style rule. |Semantic rewrite of the receipt/warrant distinction from @@ -337,8 +348,13 @@ mean "ECHIDNA is verified" — it would mean one named obligation was discharged by one named tool with its boundary written down. Nothing here vouches for a prover backend's own soundness. -No row in this file is above `+argued+` today, and that is the accurate state, -not an omission. +Four rows are `+proven+` today — R4, R9, R10, R11 — and each names the kernel, +the flags and the limit that qualify it (R4 carries the +`+UnsupportedIndexedMatch+` caveat, R9 the digest-level scope). Every *independent* +leg is still `+open+`: R5 has never been attempted, which is why the corpus sits +at Mathesis Grade 3 and not above it. Those two facts are not in tension — +proven in one kernel is exactly what Grade 3 means — and neither of them is an +omission. == Related diff --git a/echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml b/echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml index 9797c75d..0cd4594c 100644 --- a/echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml +++ b/echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml @@ -4,7 +4,7 @@ # NEUROSYM.a2ml — Neurosymbolic integration metadata [metadata] version = "0.1.0" -last-updated = "2026-04-11" +last-updated = "2026-11-01" [hypatia-config] scan-enabled = true diff --git a/meta-checker/src/Echidna/ClampTrust.agda b/meta-checker/src/Echidna/ClampTrust.agda index 58eb5dae..2a954f69 100644 --- a/meta-checker/src/Echidna/ClampTrust.agda +++ b/meta-checker/src/Echidna/ClampTrust.agda @@ -1,8 +1,11 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) ------------------------------------------------------------------------ -- Clamp Trust Bounds — semantic rewrite of the Idris2 obligation -- -- verification/proofs/idris2/ClampTrustBounds.idr states four --- obligations for `clamp_trust : Nat → TrustLevel`. That corpus is out +-- obligations for `clamp_trust : Nat → TrustLevel`; the four are proved below, +-- plus idempotence, which the Idris2 file does not state. That corpus is out -- of policy per PROOF-POLICY §3 (engineering claims about this -- repository's own types are Idris2/Agda territory, but the corpus is -- not wired into any gate and there is no `idris2` binary in CI that @@ -17,7 +20,7 @@ -- clamp-fixed-1 : clamp-trust 1 ≡ Level1 -- clamp-fixed-5 : clamp-trust 5 ≡ Level5 -- clamp-fixed-10 : clamp-trust 10 ≡ Level5 --- clamp-roundtrip : the clamp lands on a real level, not between two +-- clamp-idempotent : the clamp lands on a real level, not between two -- -- Checked with: agda --safe --without-K --cubical-compatible ------------------------------------------------------------------------ diff --git a/meta-checker/src/Echidna/Integrity.agda b/meta-checker/src/Echidna/Integrity.agda index 85394621..971fb670 100644 --- a/meta-checker/src/Echidna/Integrity.agda +++ b/meta-checker/src/Echidna/Integrity.agda @@ -1,3 +1,5 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) ------------------------------------------------------------------------ -- Solver Integrity — semantic rewrite of obligation E11 -- @@ -16,6 +18,11 @@ -- is worth having a record: it makes the deviation a machine-checked -- discrepancy (DEBT D9) instead of a reading of the source. -- +-- Scope: a binary is modelled by its digest only, so "substituted" below +-- means "a binary whose digest differs". Content-level collision resistance is +-- the `≈d-sound` field of the comparator, i.e. assumed by the caller and not +-- established here; `sharpness` shows what happens when it fails. +-- -- Checked with: agda --safe --without-K --cubical-compatible ------------------------------------------------------------------------ @@ -130,8 +137,14 @@ UnsoundHash._≈d_ always-true _ _ = true sharpness : UnsoundHash._≈d_ always-true true false ≡ true sharpness = refl --- ...while they demonstrably are not. Hence no inhabitant of --- `≈d-sound always-true` exists, and E11b cannot be discharged for this --- comparator: the hypothesis in `Hash` is doing real work. +-- ...while they demonstrably are not. sharpness-matters : ¬ (true ≡ false) sharpness-matters () + +-- Hence this comparator satisfies no soundness condition at all: the only +-- candidate witness forces `true ≡ false`. So E11b cannot be discharged for +-- it, and the `≈d-sound` field in `Hash` is doing real work rather than +-- decorating the record. +sharpness-blocks-soundness : + UnsoundHash._≈d_ always-true true false ≡ true → ¬ (true ≡ false) +sharpness-blocks-soundness _ = sharpness-matters diff --git a/meta-checker/src/Echidna/MetaChecker.agda b/meta-checker/src/Echidna/MetaChecker.agda index 34c17bb2..59a33016 100644 --- a/meta-checker/src/Echidna/MetaChecker.agda +++ b/meta-checker/src/Echidna/MetaChecker.agda @@ -61,8 +61,16 @@ -- ✓ Fixed points 0/1 -> Level1, >=5 -> Level5 -- ✓ The clamp is idempotent -- --- TOTAL: 45+ proven properties, 0 postulates, 0 assumptions, --- 0 sorry, 0 believe_me, 0 Admitted. +-- TOTAL: 45+ proven properties, 0 postulates, 0 sorry, 0 believe_me, +-- 0 Admitted. +-- +-- "0 postulates" is not the same claim as "0 hypotheses". `Receipt` is +-- unconditional. `Integrity` is *not*: its theorems are parameterised by a +-- `Hash` record whose `≈d-sound` field assumes a sound digest comparator, so +-- they are conditional on that and say so in their types. That is a named, +-- caller-supplied assumption — not an escape hatch, because --safe is what +-- rules escape hatches out — and it is why R9 is about digests rather than +-- bytes. -- -- Canonical invocation (PROOF-POLICY §2.1): -- agda --safe --without-K --cubical-compatible src/Echidna/MetaChecker.agda diff --git a/meta-checker/src/Echidna/Receipt.agda b/meta-checker/src/Echidna/Receipt.agda index a098979b..551ddcdd 100644 --- a/meta-checker/src/Echidna/Receipt.agda +++ b/meta-checker/src/Echidna/Receipt.agda @@ -1,3 +1,5 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) ------------------------------------------------------------------------ -- Receipt vs Warrant -- @@ -15,14 +17,15 @@ -- gap — a discriminating check, not more of the same evidence. -- -- Checked with: agda --safe --without-K --cubical-compatible --- (no postulates, no assumptions; the only hypothesis is the --- discriminating check in the final section, and it is a parameter) +-- (no postulates and no hypotheses: every result here is unconditional, +-- including the sharpened frame, which is a second model rather than an +-- assumption added to the first) ------------------------------------------------------------------------ module Echidna.Receipt where open import Data.Empty using (⊥; ⊥-elim) -open import Data.Product using (Σ-syntax; _×_; _,_) +open import Data.Product using (Σ-syntax; _×_; _,_; proj₁) open import Data.Unit using (⊤; tt) ------------------------------------------------------------------------ @@ -124,20 +127,46 @@ no-receipt-anywhere w-here r = r ≈-cross no-receipt-anywhere w-there r = r ≈-there ------------------------------------------------------------------------ --- Constructive counterpart: a discriminating check yields a receipt +-- The sharpened frame: excluding the alternative is what buys a receipt -- --- The hypothesis is a *parameter*, not a postulate: any caller that --- supplies such a check gets a receipt for free. In ECHIDNA terms this --- is an independently checked certificate (Rocq/Lean re-check, or --- statement comparison across two kernels) — precisely the evidence --- R5 is missing. ------------------------------------------------------------------------- - -module _ (discriminates : w-here ≈ w-there → ⊥) where - - receipt-from-check : Receipt sound w-here - receipt-from-check {w-here} _ = tt - receipt-from-check {w-there} r = ⊥-elim (discriminates r) +-- Crucially this is a *second model*, not a hypothesis bolted onto the +-- first. A function `w-here ≈ w-there → ⊥` cannot exist in the coarse +-- frame — `≈-cross` inhabits its domain — so taking one as a parameter +-- would be vacuous, and would say nothing about what a receipt is. Here +-- the same two worlds keep their identity and only the accessibility +-- changes: the agent can now tell them apart. That is what a +-- discriminating check buys, and unlike the impossible hypothesis it is +-- inhabited. +------------------------------------------------------------------------ + +data _≈′_ : World → World → Set where + ≈′-here : w-here ≈′ w-here + ≈′-there : w-there ≈′ w-there + +≈′-refl : ∀ w → w ≈′ w +≈′-refl w-here = ≈′-here +≈′-refl w-there = ≈′-there + +Receipt′ : Atom → World → Set +Receipt′ φ w = ∀ {w′} → w ≈′ w′ → ⟦ φ ⟧ w′ + +-- A receipt exists in this frame... +receipt-in-sharpened-frame : Receipt′ sound w-here +receipt-in-sharpened-frame {w-here} _ = tt +receipt-in-sharpened-frame {w-there} () + +-- ...and it is still factive, so the token means the same thing in both +-- frames: what changed is the evidence, not the standard of proof. +receipt′-factive : ∀ {φ w} → Receipt′ φ w → ⟦ φ ⟧ w +receipt′-factive r = r (≈′-refl _) + +-- THE CONTRAST, and the point of the whole module: identical worlds, +-- identical proposition, no receipt in the coarse frame and a receipt in +-- the sharpened one. Nothing about the *claim* changed; what changed is +-- whether the alternative world was excluded. +coarse-yet-sharpened : + (Receipt sound w-here → ⊥) × Receipt′ sound w-here +coarse-yet-sharpened = no-receipt-anywhere w-here , receipt-in-sharpened-frame ------------------------------------------------------------------------ -- Token discipline @@ -147,6 +176,15 @@ module _ (discriminates : w-here ≈ w-there → ⊥) where -- is not free. ------------------------------------------------------------------------ +-- The axioms the policy's PROVEN-WITH-AXIOMS token is *about*. Naming one +-- is the entire difference between that token and `proven`: asserting the +-- proposition alone would make the two indistinguishable, which is the +-- accounting §5 exists to keep. +data Axiom : Set where + funext : Axiom + choice : Axiom + em : Axiom + data Verdict : Set where proven : Verdict proven-with-postulates : Verdict @@ -156,11 +194,17 @@ data Verdict : Set where Asserts : Verdict → (φ : Atom) → World → Set Asserts proven φ w = Receipt φ w -Asserts proven-with-postulates φ w = Receipt φ w +Asserts proven-with-postulates φ w = Axiom × Receipt φ w Asserts tested-only φ w = Warrant φ w Asserts argued φ w = Warrant φ w Asserts no-claim φ w = ⊤ +-- A `proven-with-postulates` assertion carries the axiom it rests on; a +-- `proven` assertion carries none, which is why they are different types. +postulates-name-an-axiom : + ∀ {φ w} → Asserts proven-with-postulates φ w → Axiom +postulates-name-an-axiom = proj₁ + -- The same warrant never licences the stronger token. no-free-promotion : ∀ {φ w} → Asserts argued φ w → Asserts proven φ w → ⊥ diff --git a/scripts/install-proof-toolchains.sh b/scripts/install-proof-toolchains.sh index af44667e..a2b60b70 100755 --- a/scripts/install-proof-toolchains.sh +++ b/scripts/install-proof-toolchains.sh @@ -23,10 +23,21 @@ # PYTHONPATH=/tmp/py-tc PATH=/tmp/py-tc/bin:$PATH # mkdir -p /tmp/py-tc/agda/data/lib # wheel ships no primitives # # copy src/data from the v2.7.0.1 tag into /tmp/py-tc/agda/data/ +# # # stdlib: codeload.github.com/agda/agda-stdlib/tar.gz/refs/tags/v2.1 +# # Downloading is not enough — it must be *registered*, or every module that +# # imports Agda.Primitive fails: +# echo "/tmp/agda-stdlib-2.1/standard-library.agda-lib" >> ~/.agda/libraries +# # the tarball's `name:` line is `standard-library-2.1`, and `defaults` (or a +# # .agda-lib `depend:`) must match that name, not the bare `standard-library` +# echo "standard-library-2.1" >> ~/.agda/defaults +# echo "$PWD/meta-checker/echidna-meta.agda-lib" >> ~/.agda/libraries # export LC_ALL=C.UTF-8 # Unicode identifiers # -# Then check with the PROOF-POLICY §2.1 flags: +# Then check with the PROOF-POLICY §2.1 flags. Run it from meta-checker/ — the +# source path is relative to that directory, so from the repo root it does not +# resolve: +# cd meta-checker # agda --safe --without-K --cubical-compatible src/Echidna/MetaChecker.agda # # No Rust, Creusot, Lean 4, Idris 2, Coq, Z3 or cvc5 leg was obtainable that way, From 59e88cdd4b5caf52cf3faadf02b551dc6f31775b Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 18:01:13 +0000 Subject: [PATCH 4/5] Update scripts/install-proof-toolchains.sh Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- scripts/install-proof-toolchains.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/install-proof-toolchains.sh b/scripts/install-proof-toolchains.sh index a2b60b70..00362a6e 100755 --- a/scripts/install-proof-toolchains.sh +++ b/scripts/install-proof-toolchains.sh @@ -20,7 +20,8 @@ # compiler's data/lib directory populated by hand because the wheel omits it: # # pip install --target /tmp/py-tc agda # Agda 2.7.0.1 -# PYTHONPATH=/tmp/py-tc PATH=/tmp/py-tc/bin:$PATH +# export PYTHONPATH=/tmp/py-tc +# export PATH=/tmp/py-tc/bin:$PATH # mkdir -p /tmp/py-tc/agda/data/lib # wheel ships no primitives # # copy src/data from the v2.7.0.1 tag into /tmp/py-tc/agda/data/ # From 12833929d07629dd5b71fc1f5509f05cef3c8392 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Sun, 1 Nov 2026 18:10:56 +0000 Subject: [PATCH 5/5] docs(code): document trust clamping, integrity checks, and GraphQL startup --- meta-checker/src/Echidna/ClampTrust.agda | 2 ++ meta-checker/src/Echidna/Integrity.agda | 5 +++-- src/interfaces/graphql/main.rs | 9 +++++++++ 3 files changed, 14 insertions(+), 2 deletions(-) diff --git a/meta-checker/src/Echidna/ClampTrust.agda b/meta-checker/src/Echidna/ClampTrust.agda index 2a954f69..f8b01b52 100644 --- a/meta-checker/src/Echidna/ClampTrust.agda +++ b/meta-checker/src/Echidna/ClampTrust.agda @@ -45,6 +45,8 @@ open import Echidna.TrustLevel using -- The clamp, exactly as the Idris2 model defines it ------------------------------------------------------------------------ +-- Map a numeric trust score to its level: 0 and 1 yield Level1, 2–4 +-- yield the corresponding level, and scores of 5 or more yield Level5. clamp-trust : ℕ → TrustLevel clamp-trust zero = Level1 clamp-trust (suc zero) = Level1 diff --git a/meta-checker/src/Echidna/Integrity.agda b/meta-checker/src/Echidna/Integrity.agda index 971fb670..b14ce9df 100644 --- a/meta-checker/src/Echidna/Integrity.agda +++ b/meta-checker/src/Echidna/Integrity.agda @@ -73,8 +73,9 @@ module _ (H : Hash) where field digest : Digest open Binary public - -- The specified checker. Note the first line: an uninitialised - -- manifest produces `Missing`, never `Verified`. + -- Check a binary against the recorded digest using the supplied comparator. + -- An uninitialised manifest yields `Missing`; otherwise a true comparison + -- yields `Verified` and a false comparison yields `Mismatch`. check : Manifest → Binary → Result check Uninitialised _ = Missing check (Initialised d) b = decide (_≈d_ d (digest b)) diff --git a/src/interfaces/graphql/main.rs b/src/interfaces/graphql/main.rs index 771cce04..29ed0428 100644 --- a/src/interfaces/graphql/main.rs +++ b/src/interfaces/graphql/main.rs @@ -13,6 +13,15 @@ mod schema; use resolvers::EchidnaContext; use schema::{MutationRoot, QueryRoot}; +/// Runs the GraphQL endpoint and playground at `/` and the health check at +/// `/health`, with permissive CORS. The bind address comes from +/// `ECHIDNA_GRAPHQL_ADDR`, defaulting to `127.0.0.1:8081` when it is absent or +/// not valid Unicode. FFI initialisation failure falls back to direct Rust calls. +/// +/// # Panics +/// +/// Panics if logging or the HTTP client cannot be initialised, the address +/// cannot be bound, or the server fails. #[tokio::main] async fn main() { tracing_subscriber::fmt()