From 8fc17a22ffca1e4c2bb144e799629d972f20dc0f Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 7 Aug 2026 12:36:33 +0100 Subject: [PATCH 1/2] =?UTF-8?q?docs:=20repo-wide=20documentation=20refresh?= =?UTF-8?q?=20=E2=80=94=20counts,=20paths,=20licence=20status,=20debt=20re?= =?UTF-8?q?gister?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reconciles the documentation surface (human, machine-readable, wiki) against the tree, and publishes what could not be reconciled as measured debt rather than leaving it unstated. Prover counts (issue #251). Five different figures were in circulation — 48, 105, 128, 138, 141 — because four different things are all called 'the number of provers'. Re-measured: 141 ProverKind variants, 105 backend implementation files, 102 with suggest_tactics, 12 default- exposed core. docs/PROVER_COUNT.md is now canonical, explains the denominators, and ships the command that reproduces each figure; all five commands were run and reproduce exactly. Present-tense claims elsewhere now cite it. Dated historical records (release notes, completed-milestone entries) were deliberately left at their authoring-time numbers — they are records, not claims about today. Wiki. docs/wiki/ is the source and had drifted ahead of the live wiki, which had never been synced. Corrected and pushed: the Tier-1 core list named six backends that are not in ProverKind::all_core() (Idris 2, F*, Alt-Ergo, Dafny, Vampire, E Prover — actually Metamath, HOL Light, Mizar, PVS, ACL2, HOL4); the licence was stated as MPL-2.0. The note claiming the wiki is not pushable from automation was wrong and is replaced with a working sync recipe. Stale paths (issue #242). .machine_readable/6a2/ no longer exists; its six descriptiles moved to descriptiles/. Repaired 17 documents. The contractile .ncl write-destinations still naming 6a2/ were left alone deliberately — 6a2 is a concept name there, and repointing an evidence sink is a semantic decision. Recorded as D7. Broken links: 19 -> 13. The 13 remaining are dated release notes and the playground sub-project, both recorded as D4/D5 rather than silently rewritten. Root scaffold. ARCHITECTURE.md and GOVERNANCE.md contained generic template text with zero project-specific words, while the real documents sat at docs/ARCHITECTURE.md and GOVERNANCE.adoc. Since GitHub surfaces the .md member, the document most readers landed on described no particular project. Both are now explicit pointers. OpenSSF badge removed: it was a hardcoded green shields.io label linking to the project registration form, so it would have read 'passed' whatever the real standing — including now, unregistered. Restore the genuine dynamic badge once registered. docs/DEBT.md (new) carries the rest, every item with the command that measures it. P0 is licensing: the repository states four different licences, and 590 source files carry MPL-2.0 headers while LICENSE and Cargo.toml declare AGPL-3.0-or-later. Because per-file headers are themselves a grant, that is live exposure, not an inconsistency of record. NOT ACTED ON — re-licensing is an owner decision; the entry sets out a sequence and stops. README and the wiki now warn readers not to rely on any surface but LICENSE until it is resolved. Verified: R5a bare-count rule clean across all scoped top-level docs; every PROVER_COUNT command reproduces its stated figure; DEBT.md's own measurements re-run and corrected (588 -> 590) before commit. Co-Authored-By: Claude Opus 5 --- .claude/CLAUDE.md | 12 +- .github/PROVEN-INTEGRATION.md | 2 +- .machine_readable/ER.a2ml | 5 +- .machine_readable/ROADMAP.a2ml | 3 +- .../contractiles/intend/Intentfile.a2ml | 3 +- .machine_readable/descriptiles/AGENTIC.a2ml | 3 +- .machine_readable/descriptiles/ECOSYSTEM.a2ml | 10 +- 0-AI-MANIFEST.a2ml | 7 +- AFFIRMATION.adoc | 2 +- ARCHITECTURE.md | 63 ++-- CLAUDE.md | 2 + CONTRIBUTING.md | 2 +- GOVERNANCE.adoc | 2 +- GOVERNANCE.md | 74 ++--- README.md | 19 +- RSR_COMPLIANCE.adoc | 4 +- crates/echidna-mcp/README.md | 2 +- docs/ARCHITECTURE.md | 6 +- docs/CVC5_QUICK_REFERENCE.md | 3 +- docs/DEBT.md | 269 ++++++++++++++++++ docs/PROVER_COUNT.md | 143 ++++++---- docs/ROADMAP.md | 6 +- .../2026-05-19-ci-baseline-triage.md | 2 +- .../2026-05-30-chapel-rehabilitation.md | 2 +- docs/handover/HANDOVER-INDEX.md | 2 +- docs/handover/L3-LIVE-PROVER-CI-PROMPT.md | 2 +- docs/handover/PHASE-3-PROMPT.md | 2 +- docs/handover/PRODUCTION-WIRING-PLAN.md | 2 +- docs/handover/README.md | 2 +- docs/handover/STATE.md | 4 +- docs/handover/TODO.md | 2 +- docs/handover/llm-warmup-dev.md | 8 +- docs/tech-debt-2026-05-26.md | 6 + docs/wiki/Architecture.md | 5 +- docs/wiki/FAQ.md | 39 ++- docs/wiki/Home.md | 12 +- docs/wiki/README.md | 29 +- 37 files changed, 542 insertions(+), 219 deletions(-) create mode 100644 docs/DEBT.md diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 0aab4172..c44e1e3d 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -2,12 +2,12 @@ The following files in `.machine_readable/` contain structured project metadata: -- `.machine_readable/6a2/STATE.a2ml` - Current project state and progress -- `.machine_readable/6a2/META.a2ml` - Architecture decisions and development practices -- `.machine_readable/6a2/ECOSYSTEM.a2ml` - Position in the ecosystem and related projects -- `.machine_readable/6a2/AGENTIC.a2ml` - AI agent interaction patterns -- `.machine_readable/6a2/NEUROSYM.a2ml` - Neurosymbolic integration config -- `.machine_readable/6a2/PLAYBOOK.a2ml` - Operational runbook +- `.machine_readable/descriptiles/STATE.a2ml` - Current project state and progress +- `.machine_readable/descriptiles/META.a2ml` - Architecture decisions and development practices +- `.machine_readable/descriptiles/ECOSYSTEM.a2ml` - Position in the ecosystem and related projects +- `.machine_readable/descriptiles/AGENTIC.a2ml` - AI agent interaction patterns +- `.machine_readable/descriptiles/NEUROSYM.a2ml` - Neurosymbolic integration config +- `.machine_readable/descriptiles/PLAYBOOK.a2ml` - Operational runbook - `.machine_readable/bot_directives/*.a2ml` - Per-bot permission and scope rules ## Canonical Roadmap diff --git a/.github/PROVEN-INTEGRATION.md b/.github/PROVEN-INTEGRATION.md index 411b43a6..4558f0dc 100644 --- a/.github/PROVEN-INTEGRATION.md +++ b/.github/PROVEN-INTEGRATION.md @@ -12,7 +12,7 @@ This document outlines the recommended [proven](https://github.com/hyperpolymath ## Integration Notes -ECHIDNA as a neurosymbolic theorem proving platform supporting 128 prover backends (12 core; see [docs/PROVER_COUNT.md](../docs/PROVER_COUNT.md)) requires formally verified proof management: +ECHIDNA as a neurosymbolic theorem proving platform (12 core backends exposed by default; see [docs/PROVER_COUNT.md](../docs/PROVER_COUNT.md) for the full tier table and count semantics) requires formally verified proof management: - **SafeGraph** models proof dependencies as DAGs. The `Acyclic` proof guarantees no circular dependencies in proof chains, and `topoSort` provides correct ordering for proof verification. `PathExists` verifies lemma reachability. diff --git a/.machine_readable/ER.a2ml b/.machine_readable/ER.a2ml index 45188f1c..02b133b6 100644 --- a/.machine_readable/ER.a2ml +++ b/.machine_readable/ER.a2ml @@ -41,8 +41,9 @@ scope = "src/rust/core.rs + src/rust/verification/* + src/rust/dispatch.rs" # ═══════════════════════════════════════════════════════════════════════════════ # ─── 1. Term ────────────────────────────────────────────────────────────────── -# Universal mathematical term representation shared across all 105 prover -# backends. An ADT with 15 variants; self-referential via boxed children. +# Universal mathematical term representation shared across every prover backend +# (see docs/PROVER_COUNT.md for the canonical count and its semantics). +# An ADT with 15 variants; self-referential via boxed children. # # No explicit integer PK — terms are compared structurally (PartialEq) or # via Display serialisation for hashing in proof_encoding.rs. diff --git a/.machine_readable/ROADMAP.a2ml b/.machine_readable/ROADMAP.a2ml index ea75b54d..25f73840 100644 --- a/.machine_readable/ROADMAP.a2ml +++ b/.machine_readable/ROADMAP.a2ml @@ -14,7 +14,8 @@ next-review = "2026-07-13" [vision] summary = """ -Echidna evolves from a proof-solving library (105 provers + neurosymbolic guidance) +Echidna evolves from a proof-solving library (multi-backend prover surface — +see docs/PROVER_COUNT.md — plus neurosymbolic guidance) into a distributed, trustworthy proof-as-a-service platform accessible to the entire hyperpolymath estate and beyond. diff --git a/.machine_readable/contractiles/intend/Intentfile.a2ml b/.machine_readable/contractiles/intend/Intentfile.a2ml index 2d0afbaf..142c083f 100644 --- a/.machine_readable/contractiles/intend/Intentfile.a2ml +++ b/.machine_readable/contractiles/intend/Intentfile.a2ml @@ -9,7 +9,8 @@ Declared intent and purpose for Echidna. ## Purpose Echidna is a trust-hardened neurosymbolic theorem proving platform. -It supports 128 prover backends, records every proof attempt to +It supports 141 ProverKind variants over 105 backend implementations +(canonical count semantics: docs/PROVER_COUNT.md), records every proof attempt to VeriSimDB, and feeds the Hypatia learning loop so the fleet gets smarter over time. diff --git a/.machine_readable/descriptiles/AGENTIC.a2ml b/.machine_readable/descriptiles/AGENTIC.a2ml index f7416c23..c855c1e3 100644 --- a/.machine_readable/descriptiles/AGENTIC.a2ml +++ b/.machine_readable/descriptiles/AGENTIC.a2ml @@ -3,7 +3,8 @@ # # AGENTIC.a2ml — AI agent operational gating and proof-solving dispatch # Defines safety constraints, entropy budgets, and explicit-intent gating for AI agents -# working in echidna (proof-solving service with 105 prover backends, 3GB training corpus). +# working in echidna (proof-solving service; 141 ProverKind variants over 105 backend +# implementations — see docs/PROVER_COUNT.md for count semantics; 3GB training corpus). [metadata] version = "0.3.0" diff --git a/.machine_readable/descriptiles/ECOSYSTEM.a2ml b/.machine_readable/descriptiles/ECOSYSTEM.a2ml index bd7c6790..9405b21f 100644 --- a/.machine_readable/descriptiles/ECOSYSTEM.a2ml +++ b/.machine_readable/descriptiles/ECOSYSTEM.a2ml @@ -12,10 +12,12 @@ ecosystem = "hyperpolymath" [project] name = "ECHIDNA" full-name = "Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance" -purpose = """Trust-hardened neurosymbolic theorem proving platform. 48 prover backends -(Agda, Lean4, Isabelle, Coq, Idris2, F*, Z3, CVC5, Vampire, and 39 more). Sandboxed -solver execution (Podman/bubblewrap), proof certificate checking, axiom tracking, -GNN-guided proof search, Julia ML inference layer.""" +purpose = """Trust-hardened neurosymbolic theorem proving platform. 141 ProverKind +variants across 105 backend implementations, 12 exposed by default at GET /api/provers +(Agda, Coq, Lean 4, Isabelle/HOL, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2, HOL4); +canonical tier table and count semantics in docs/PROVER_COUNT.md. Sandboxed solver +execution (Podman/bubblewrap), proof certificate checking, axiom tracking, GNN-guided +proof search, Julia ML inference layer.""" role = "prover-dispatcher" [position] diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 68626985..5714e154 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -46,7 +46,7 @@ proofs = "proofs/" container = "container/" [tech-stack] -primary = "Rust (48 prover backends, trust pipeline, CLI, REPL, API servers)" +primary = "Rust (141 ProverKind variants over 105 backend implementations — see docs/PROVER_COUNT.md; trust pipeline, CLI, REPL, API servers)" secondary = "Julia (ML inference, port 8090), ReScript+Deno (UI, 33 files, zero TypeScript)" optional = "Chapel (parallel proof dispatch)" abi = "Idris2 (7 modules, zero believe-me)" @@ -56,8 +56,9 @@ build = "Justfile (primary), Cargo workspace" container = "Podman + Containerfile" [architecture] -# Trust-hardened neurosymbolic theorem proving with 48 prover backends -core = "src/rust/" # 48 provers, trust pipeline, dispatch +# Trust-hardened neurosymbolic theorem proving; canonical backend count and +# count semantics live in docs/PROVER_COUNT.md +core = "src/rust/" # ProverKind enum + backends, trust pipeline, dispatch verification = "src/rust/verification/" # Portfolio, certificates, axiom tracker, confidence, mutation, pareto, statistics integrity = "src/rust/integrity/" # Solver binary integrity (SHAKE3-512, BLAKE3) executor = "src/rust/executor/" # Sandboxed execution (Podman, bubblewrap) diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 67f6ffb3..0007ddfa 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -36,7 +36,7 @@ available. real release line is in `CHANGELOG.md`. . *Critical Reception Grade.* CRG-C is complete (unit + smoke + build + P2P + E2E + contract + aspect + benchmarks baselined, per - `.machine_readable/6a2/STATE.a2ml`); CRG-B criteria are populated but B is + `.machine_readable/descriptiles/STATE.a2ml`); CRG-B criteria are populated but B is *not* formally affirmed here. == Verified as of 2026-06-15 (green / reproduced) diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md index 607e3d8c..9e3ecd19 100644 --- a/ARCHITECTURE.md +++ b/ARCHITECTURE.md @@ -1,47 +1,26 @@ -# Architecture - -## Overview - -This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability. - -## Directory Structure - -``` -. -├── src/ # Source code -├── tests/ # Test suites -├── docs/ # Documentation -├── scripts/ # Utility scripts -├── config/ # Configuration files -├── LICENSE # License file -├── LICENSES/ # Full license texts -└── README.adoc # Project documentation -``` - -## Design Principles + -## Dependencies - -- External dependencies are minimized and clearly declared -- Version pinning is used for reproducibility - -## Security Considerations - -- Sensitive data is never committed to the repository -- Secrets are managed through environment variables or secure vaults -- Regular dependency audits are performed - -## Maintainability +# Architecture -- Code follows consistent style guidelines -- Pull requests require review and CI checks -- Issues and discussions are tracked transparently +The architecture documentation for ECHIDNA lives in +[`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md) — the polyglot layout, the +dispatch path, the trust-hardening pipeline, and how the Rust core, Julia ML +sidecar, Idris2 ABI, Zig FFI and optional Chapel parallel layer fit together. ---- +Related canonical documents: -*Last updated: 2026-07-18* +- [`docs/PROVER_COUNT.md`](docs/PROVER_COUNT.md) — backend tier table and what + each published count actually counts +- [`docs/ROADMAP.md`](docs/ROADMAP.md) — stage map and current direction +- [`docs/DEBT.md`](docs/DEBT.md) — known licence, documentation and code debt +- [`.machine_readable/descriptiles/META.a2ml`](.machine_readable/descriptiles/META.a2ml) + — the machine-readable architecture record diff --git a/CLAUDE.md b/CLAUDE.md index 3f7b14db..ed37ebcc 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -11,6 +11,8 @@ Guidelines and context for working with Claude Code on the ECHIDNA project. - **License**: AGPL-3.0-or-later (owner decision 2026-07-07; per-file MPL-2.0 headers pending migration sweep) - **Architecture overview**: [`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md) - **Canonical prover count + tier table**: [`docs/PROVER_COUNT.md`](docs/PROVER_COUNT.md) +- **Known debt (licence, docs, code)**: [`docs/DEBT.md`](docs/DEBT.md) — read before + asserting anything about the licence; the repository is currently inconsistent - **Environment variables**: [`docs/ENV-VARS.md`](docs/ENV-VARS.md) - **RSR / CCCP compliance statement**: [`RSR_COMPLIANCE.adoc`](RSR_COMPLIANCE.adoc) - **Receipts for README claims**: [`EXPLAINME.adoc`](EXPLAINME.adoc) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b9aa0c91..74d0593c 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -15,7 +15,7 @@ and the licence / SPDX policy. GitHub renders AsciiDoc directly. If a quick orientation is enough: -- **Before you start**: read [`README.adoc`](README.adoc), +- **Before you start**: read [`README.md`](README.md), [`RSR_COMPLIANCE.adoc`](RSR_COMPLIANCE.adoc), and [`CLAUDE.md`](CLAUDE.md) (if you are using an AI agent). - **Local setup**: see [`QUICKSTART-DEV.adoc`](QUICKSTART-DEV.adoc). diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc index 8bbf167d..9cb1b9cd 100644 --- a/GOVERNANCE.adoc +++ b/GOVERNANCE.adoc @@ -128,7 +128,7 @@ This repository adheres to hyperpolymath estate-wide policies: | **Contractiles** | Mustfile, Trustfile, Intendfile, Adjustfile in root -| **Machine Readable** | META.a2ml in .machine_readable/6a2/ +| **Machine Readable** | META.a2ml in .machine_readable/descriptiles/ | **CI/CD** | GitHub Actions workflows in .github/workflows/ diff --git a/GOVERNANCE.md b/GOVERNANCE.md index e27364c7..3fd11040 100644 --- a/GOVERNANCE.md +++ b/GOVERNANCE.md @@ -1,60 +1,24 @@ -# Governance - -## Overview - -This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making. - -## Roles and Responsibilities - -### Maintainers - -Maintainers are responsible for: -- Reviewing and merging pull requests -- Managing releases and versioning -- Ensuring code quality and standards -- Triaging issues and bug reports -- Community engagement and support - -### Contributors - -Contributors are expected to: -- Follow the code of conduct -- Submit well-documented pull requests -- Write tests for new functionality -- Maintain existing tests -- Update documentation as needed + -### Minor Changes -- Can be made by any maintainer -- Include bug fixes, documentation updates, dependency updates - -### Major Changes -- Require discussion in issues or pull requests -- Include new features, architectural changes, API changes -- Need approval from at least 2 maintainers - -### Breaking Changes -- Require RFC (Request for Comments) process -- Need approval from majority of maintainers -- Must include migration guide - -## Code of Conduct - -All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers. - -## Communication - -- **Issues**: For bug reports and feature requests -- **Discussions**: For questions and general discussion -- **Pull Requests**: For code contributions - -## Licensing +# Governance -All contributions are made under the terms of the repository's LICENSE file. -By submitting a pull request, you agree to license your contributions accordingly. +The governance model for ECHIDNA is documented in +[`GOVERNANCE.adoc`](GOVERNANCE.adoc) — decision-making, maintainer +responsibilities, the RSR/CCCP compliance position, and how changes are +ratified. GitHub renders AsciiDoc directly. ---- +Related: -*Last updated: 2026-07-18* +- [`MAINTAINERS.adoc`](MAINTAINERS.adoc) — who maintains what +- [`CONTRIBUTING.adoc`](CONTRIBUTING.adoc) — contribution process +- [`CODE_OF_CONDUCT.md`](CODE_OF_CONDUCT.md) — expected conduct +- [`RSR_COMPLIANCE.adoc`](RSR_COMPLIANCE.adoc) — compliance statement diff --git a/README.md b/README.md index e62afb73..e0dc712f 100644 --- a/README.md +++ b/README.md @@ -3,9 +3,26 @@ SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell --> -[![OpenSSF Best Practices](https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity)](https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/echidna) [![License: AGPL-3.0-or-later](https://img.shields.io/badge/License-AGPL--3.0--or--later-blue.svg)](LICENSE) [![Green Hosting](https://api.thegreenwebfoundation.org/greencheckimage/nesy-prover.dev)](https://www.thegreenwebfoundation.org/green-web-check/?url=nesy-prover.dev) + + +> **Licence notice.** This repository declares AGPL-3.0-or-later in `LICENSE` +> and `Cargo.toml`, but per-file `SPDX-License-Identifier` headers across the +> source tree still read `MPL-2.0`, and `NOTICE` still describes the project as +> MPL-2.0. That inconsistency is unresolved — see +> [`docs/DEBT.md`](docs/DEBT.md) (P0). If your use depends on the licence +> terms, read `LICENSE` and ask the maintainer before relying on any other +> surface. + \*E\*xtensible \*C\*ognitive \*H\*ybrid \*I\*ntelligence for \*D\*eductive \*N\*eural \*A\*ssistance diff --git a/RSR_COMPLIANCE.adoc b/RSR_COMPLIANCE.adoc index 4e47f221..edebdee0 100644 --- a/RSR_COMPLIANCE.adoc +++ b/RSR_COMPLIANCE.adoc @@ -7,7 +7,7 @@ Jonathan D.A. Jewell :toc: Status: living document, regenerated as policy changes. -Canonical state: `.machine_readable/6a2/STATE.a2ml`. +Canonical state: `.machine_readable/descriptiles/STATE.a2ml`. Canonical policy: `MUST.contractile`, `ADJUST.contractile`, `.machine_readable/policies/*.a2ml`. @@ -49,7 +49,7 @@ the contractiles and the machine-readable policies above. ECHIDNA diverges from the strict RSR template in three places: 1. *State file location*: RSR template puts `STATE.scm` at root; echidna - places it at `.machine_readable/6a2/STATE.a2ml` per the `.scm → .a2ml` + places it at `.machine_readable/descriptiles/STATE.a2ml` per the `.scm → .a2ml` migration documented in `.claude/CLAUDE.md`. 2. *Polyglot source layout*: `src/` contains per-language subdirectories (`src/rust/`, `src/julia/`, `src/abi/`, `src/chapel/`, `src/zig_ffi/`, diff --git a/crates/echidna-mcp/README.md b/crates/echidna-mcp/README.md index 960888d1..24851835 100644 --- a/crates/echidna-mcp/README.md +++ b/crates/echidna-mcp/README.md @@ -50,7 +50,7 @@ Or with an explicit binary path: ### `prove` -Prove a theorem from a file using one of ECHIDNA's 105 backends. +Prove a theorem from a file using one of ECHIDNA's prover backends (see [`docs/PROVER_COUNT.md`](../../docs/PROVER_COUNT.md)). | Parameter | Type | Required | Description | |-----------|------|----------|-------------| diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 6b289a7c..1984debf 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -4,8 +4,8 @@ # ECHIDNA Architecture **Status**: canonical human-readable overview. Lives alongside the machine-readable -[`.machine_readable/6a2/META.a2ml`](../.machine_readable/6a2/META.a2ml) (architecture -decisions) and [`STATE.a2ml`](../.machine_readable/6a2/STATE.a2ml) (current state). +[`.machine_readable/descriptiles/META.a2ml`](../.machine_readable/descriptiles/META.a2ml) (architecture +decisions) and [`STATE.a2ml`](../.machine_readable/descriptiles/STATE.a2ml) (current state). Last revised: 2026-05-26. ECHIDNA — Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance — @@ -157,4 +157,4 @@ retained only as debug fallback. See [`docs/handover/L1-CAPNPROTO-PROMPT.md`](ha - [`docs/ENV-VARS.md`](ENV-VARS.md) — every environment variable the system reads, with defaults. - [`docs/PROVER_COUNT.md`](PROVER_COUNT.md) — canonical tier table. -- [`.machine_readable/6a2/STATE.a2ml`](../.machine_readable/6a2/STATE.a2ml) — machine-readable state, regenerated each sprint. +- [`.machine_readable/descriptiles/STATE.a2ml`](../.machine_readable/descriptiles/STATE.a2ml) — machine-readable state, regenerated each sprint. diff --git a/docs/CVC5_QUICK_REFERENCE.md b/docs/CVC5_QUICK_REFERENCE.md index ebacabdc..68ed0753 100644 --- a/docs/CVC5_QUICK_REFERENCE.md +++ b/docs/CVC5_QUICK_REFERENCE.md @@ -384,8 +384,7 @@ cvc5 problem.smt2 ## Links -- [Full Implementation Details](/home/user/echidna/docs/CVC5_IMPLEMENTATION.md) -- [Implementation Summary](/home/user/echidna/CVC5_IMPLEMENTATION_SUMMARY.md) +- [Implementation Summary](implementation/CVC5_IMPLEMENTATION_SUMMARY.md) - [CVC5 Documentation](https://cvc5.github.io/docs/latest/) - [SMT-LIB Standard](https://smtlib.cs.uiowa.edu/) diff --git a/docs/DEBT.md b/docs/DEBT.md new file mode 100644 index 00000000..127f2c70 --- /dev/null +++ b/docs/DEBT.md @@ -0,0 +1,269 @@ + + + +# Debt register + +Known, measured debt in this repository: licensing, documentation, and code. +Supersedes [`tech-debt-2026-05-26.md`](tech-debt-2026-05-26.md), which is +retained as a dated snapshot. + +**Every entry carries the command that produced its figure.** An entry without +evidence is a rumour, and rumours do not belong in a debt register. Re-run the +commands from the repository root before acting on any item — they are the +definition of the finding, not a description of it. + +Entries are **not** issues. Where a GitHub issue already tracks an item it is +linked; where the fix requires a decision only the owner can make, the entry +says so explicitly and stops there. + +Priorities: **P0** — a downstream consumer can be actively misled or harmed. +**P1** — a reader is misinformed but not exposed. **P2** — friction, cost, or +latent risk. + +--- + +## P0 — Licensing: the repository states four different licences + +**This is the most serious item in the register.** A recipient cannot determine +the terms under which they receive this software, and every surface they might +reasonably consult gives a different answer. + +| Surface | What it states | Evidence | +|---|---|---| +| `LICENSE` (full GNU text) | AGPL-3.0-or-later | `head -3 LICENSE` | +| `Cargo.toml` | AGPL-3.0-or-later | `grep '^license' Cargo.toml` | +| README badge | AGPL-3.0-or-later | `grep -m1 'License:' README.md` | +| Per-file SPDX headers — **590 source files** (584 `MPL-2.0`, 6 dual with `Palimpsest-0.6`) | MPL-2.0 | `L1` below | +| Per-file SPDX headers | AGPL-3.0-or-later — **zero files** | `L2` below | +| `NOTICE` | MPL-2.0, and points at `LICENSE` for the "full text" — but `LICENSE` is AGPL | `head -10 NOTICE` | +| `.reuse/dep5` (`src/*`) | `PMPL-1.0 AND Palimpsest-0.6` | `grep -m1 -A3 'Files: src' .reuse/dep5` | +| `.github/workflows/governance.yml` | `PMPL-1.0-or-later` | `head -1 .github/workflows/governance.yml` | +| GitHub's own detection | "Other" — no licence identified | `gh repo view --json licenseInfo` | + +```bash +# L1 — source files declaring MPL-2.0 (590: 584 plain + 6 dual) +git grep -I -h -m1 -oP 'SPDX-License-Identifier:\s*\K[A-Za-z0-9.\-+]+( (AND|OR) [A-Za-z0-9.\-+]+)*' \ + -- '*.rs' '*.jl' '*.zig' '*.chpl' '*.idr' '*.agda' '*.res' '*.sh' '*.ncl' | sort | uniq -c + +# L2 — source files declaring AGPL (0) +git grep -l 'SPDX-License-Identifier:.*AGPL' -- '*.rs' '*.jl' '*.zig' | wc -l +``` + +The difference is not cosmetic. MPL-2.0 is file-level weak copyleft with no +network clause; AGPL-3.0-or-later is strong copyleft that reaches users served +over a network. A downstream integrator reading the file headers would conclude +they may offer a modified ECHIDNA as a hosted service without publishing their +changes. The `LICENSE` file says otherwise. **Because the per-file headers are +themselves a licence grant, this exposure is real, not theoretical.** + +Two further consequences: + +- **REUSE non-compliance.** `.reuse/dep5` and nine file headers reference + `PMPL-1.0` and `Palimpsest-0.6`, but `LICENSES/` contains only + `AGPL-3.0-or-later.txt`, `CC-BY-SA-4.0.txt`, and `MPL-2.0.txt`. A REUSE + conformance run cannot resolve those identifiers. + Evidence: `ls LICENSES/` and `git grep -l Palimpsest`. +- **GitHub reports the licence as "Other"**, so the repository shows no licence + in search, the sidebar, or the API. The likely cause is the + `SPDX-License-Identifier:` line prepended to `LICENSE` above the GNU text, + which stops GitHub's detector matching the body. Removing that one line is a + low-risk experiment that does not alter the grant. + +**Owner decision required — do not "fix" this in a routine PR.** The recorded +decision (`CLAUDE.md`, matching `Cargo.toml`) is AGPL-3.0-or-later. Applying it +means rewriting the SPDX header of every source file, which is a re-licensing +act with consequences for existing recipients and any contributor who submitted +under MPL terms. Nobody should do that on their own initiative. + +Suggested sequence, once the owner has ruled: + +1. Confirm the intended licence for **code** and for the **documentation + surface** separately — `CLAUDE.md` states the MPL headers on docs are + deliberate, so the two may legitimately differ. +2. Reconcile `NOTICE` first: it is the only surface that is internally + self-contradictory (it names MPL and cites an AGPL file as its text). +3. Add the missing `LICENSES/` texts, or remove the `PMPL-1.0` / + `Palimpsest-0.6` references if those licences are retired. +4. Only then sweep the per-file headers, in one reviewable commit per language. + A previous blind SPDX sweep in this estate mis-licensed files by imposing a + header where a different one already existed further down the file — grep the + whole file, move the identifier, never impose one. +5. Drop the prepended SPDX line from `LICENSE` and confirm GitHub detects it. + +--- + +## P1 — Documentation + +### D1. Prover counts drift across surfaces *(issue [#251](https://github.com/hyperpolymath/echidna/issues/251))* + +**Largely addressed** in the documentation refresh that added this file; recorded +because the underlying cause is structural and will recur. + +The tree contained five different counts — 48, 105, 128, 138, 141 — because +four different things are all called "the number of provers": enum variants +(141), implementation files (105), implementations with `suggest_tactics` +(102), and default-exposed core backends (12). All four are defensible; none is +"the" count. [`PROVER_COUNT.md`](PROVER_COUNT.md) is now canonical, carries the +commands that reproduce each figure, and explains the denominators. + +**Residual risk:** the `R5a` CI rule +(`.github/canonical-references/prover-counts.yml`) that forbids bare counts +covers only the top-level document set named in that file. `docs/`, +`.machine_readable/`, `crates/*/README.md` and `.github/*.md` are **out of +scope**, which is precisely where the drift accumulated. Extending the rule's +scope is unfinished work. + +### D2. Tier membership is hand-maintained and unverifiable + +`PROVER_COUNT.md`'s tier table is the routing contract, but only Tier 1 +(`ProverKind::all_core()`) and Tier 9 are machine-checkable. Tier 4's +"19 placeholder backends" and Tier 8's "13 corpus-only provers" are asserted, +not derived, and were not re-measured in this pass — they are marked as +indicative in the table. Making tier membership an attribute on each +`ProverKind` variant would make the table generated rather than maintained. + +### D3. Unearned OpenSSF Best Practices badge + +`README.md` displays a hardcoded green "OpenSSF Best Practices" badge that +links to the project **registration** form, not to a passing scorecard: + +```bash +grep -oE 'bestpractices.dev[^)]*' README.md +# bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/echidna +``` + +The badge image is a static `img.shields.io` green label, so it will read as +"passed" regardless of the project's actual standing — including now, when the +project is not registered. Either register the project and use the real badge +(which reflects the true tier and changes when it lapses), or remove the badge. +A permanently-green badge that cannot fail is indistinguishable from a false +claim. This is a known estate-wide pattern, not unique to this repository. + +### D4. Broken links in historical release notes + +Nine dead links remain in `docs/releases/RELEASE_NOTES_v1.2.md` and +`RELEASE_NOTES_v1.3.md`, pointing at design documents that are not in the tree +(`CHAPEL_METALAYER_ANALYSIS.md`, `ZIG_FFI_ANALYSIS.md`, +`FUTURE_DEVELOPMENT_ROADMAP.md`, `QUICKSTART.md`, and others). Live documents +were repaired in the refresh; these were deliberately left, because release +notes are dated records and rewriting them rewrites history. They should either +be de-linked in place or the referenced documents restored from git history. + +```bash +# re-measure broken relative links across all Markdown/AsciiDoc +git grep -nE '\]\([A-Za-z0-9_./-]+\.(md|adoc)\)' -- '*.md' '*.adoc' | while IFS= read -r l; do + src="${l%%:*}"; ref=$(echo "$l" | grep -oE '\]\([A-Za-z0-9_./-]+\)' | sed -E 's/^\]\(//;s/\)$//') + for r in $ref; do [ -e "$(dirname "$src")/$r" ] || echo "$src -> $r"; done +done +``` + +### D5. `echidna-playground/SECURITY.md` references absent files + +It links to `README.md`, `CHANGELOG.md`, `CONTRIBUTING.md` and +`SECURITY-ACKNOWLEDGMENTS.md` inside `echidna-playground/`; none exist +(`ls echidna-playground/`). The sub-project's security policy therefore +directs a reporter to nothing. Either add the files or point the links at the +parent repository's equivalents. + +### D6. Root scaffold documents displaced the real ones — *fixed, recorded* + +`ARCHITECTURE.md` and `GOVERNANCE.md` at the repository root contained generic +template text with **zero** project-specific content, while the real documents +sat at `docs/ARCHITECTURE.md` (160 lines) and `GOVERNANCE.adoc` (162 lines): + +```bash +grep -icE 'echidna|prover|neurosym|trust' ARCHITECTURE.md # was 0 +grep -icE 'echidna|prover|RSR|hyperpolymath' GOVERNANCE.md # was 0 +``` + +This was worse than duplication. GitHub surfaces the `.md` member in its +community-standards checks and contributor prompts, so the document most +readers landed on described a project that could have been anything. Both are +now explicit pointers to the canonical documents, following the pattern +`CONTRIBUTING.md` already used correctly. + +**Watch for recurrence:** these files match the estate's scaffold-template +shape, so a future template sweep may reinstate them. The check above is the +detector — a root `.md` scoring 0 is scaffold, not documentation. + +### D7. `.machine_readable/6a2/` no longer exists + +The six descriptiles moved to `.machine_readable/descriptiles/`. Seventeen +documents pointed at the old path and were repaired in the refresh, but the +contractile configurations still name `.machine_readable/6a2/DRIFT.a2ml` and +`.machine_readable/6a2/ratification-.a2ml` as **write +destinations**: + +```bash +git grep -n '6a2/' -- '*.ncl' +``` + +Those were left alone deliberately: `6a2` is a concept name there, not a stale +path, and changing a contractile's evidence sink is a semantic decision. But the +directory does not exist, so any drift-log write has nowhere to land. Confirm +whether the sink should be created or repointed. + +--- + +## P2 — Code + +### C1. ReScript remains, though the language policy bans it + +31 files (`git ls-files '*.res' '*.resi' | wc -l`). Project policy names +ReScript as banned with AffineScript-TEA as the replacement, and the migration +is blocked on missing AffineScript primitives — `Http::fetch`, `Async`, `Json` +— tracked in issues [#266](https://github.com/hyperpolymath/echidna/issues/266) +and [#117](https://github.com/hyperpolymath/echidna/issues/117). The debt is the +gap between a stated ban and an unmigrated tree, and the honest reading is that +the policy is aspirational until those primitives land. + +### C2. 185 `#[allow(dead_code)]` suppressions + +```bash +git grep -c 'allow(dead_code)' -- '*.rs' | awk -F: '{s+=$2} END{print s}' +``` + +Each one silences the compiler's own report of unreachable code. At this volume +the suppressions, not the compiler, define what counts as live code — so genuine +dead code is no longer detectable. Worth a pass to distinguish +scaffolding-for-planned-work (annotate with the tracking issue) from code that +should be deleted. + +### C3. Placeholder backends are indistinguishable from working ones at the API + +Tier 4 backends are `ProverKind` variants with mock-only invocation, but they +are reachable through the same `ProverKind` selection as real ones. A caller +selecting one receives a response shaped like a proof result. `container-ci.yml` +runs stub-sentinel detection for Tier-3 cells; the corresponding guarantee for +Tier-4 placeholders at the API boundary is not documented. Related: D2 — the +placeholder count itself is unverified. + +### C4. Unfinished-work markers + +Low and healthy for a tree this size — recorded as a baseline to watch: + +```bash +git grep -cE 'TODO|FIXME|XXX' -- '*.rs' | awk -F: '{s+=$2} END{print s}' # 11 across 6 files +git grep -cE 'todo!\(\)|unimplemented!\(\)' -- '*.rs' | awk -F: '{s+=$2} END{print s}' # 1 +``` + +--- + +## Already tracked as issues + +Open issues covering debt not duplicated above: [#314](https://github.com/hyperpolymath/echidna/issues/314) +(hypatia baseline gate un-armed — currently the reason `Governance` fails on +`main`), [#310](https://github.com/hyperpolymath/echidna/issues/310) (dead +`VERISIMDB_PAT`), [#252](https://github.com/hyperpolymath/echidna/issues/252) +(machine-readable currency audit), [#242](https://github.com/hyperpolymath/echidna/issues/242) +(structural drift in path references), [#240](https://github.com/hyperpolymath/echidna/issues/240) +(ReScript deprecated-API triage), [#239](https://github.com/hyperpolymath/echidna/issues/239) +(safety-alert classification), [#216](https://github.com/hyperpolymath/echidna/issues/216) +(SPDX-FileCopyrightText hook blocks commits — a licensing-adjacent item that +should be resolved alongside P0). + +## Maintaining this file + +Add an entry when you find debt you are not fixing in the same change. Include +the command that measures it. Remove an entry only when the command that +detected it comes back clean — not when the work "feels done". diff --git a/docs/PROVER_COUNT.md b/docs/PROVER_COUNT.md index c9ba6347..7dbf6cd4 100644 --- a/docs/PROVER_COUNT.md +++ b/docs/PROVER_COUNT.md @@ -4,34 +4,42 @@ # Canonical Prover Count and Tier Table **Status**: canonical. Cite this file when documenting backend coverage in any -other doc. Other surfaces that quoted historical counts (12, 30, 48, 105) are -being updated to point here. Last revised: 2026-06-01. - -> **Known drift** (tracked, not closed in routine doc PRs): the -> `ProverKind` variant count below (**128**) lags the actual enum in -> `src/rust/provers/mod.rs` (~138 variants on `main`). Refreshing -> the count + `.machine_readable/provers.a2ml` belongs to the next -> backend-count audit PR; see PR #169 closeout for the deliberately -> deferred scope. The Tier-1 membership list immediately below is -> the live one (mirrors `ProverKind::all_core()`). +other doc. Every number below was re-measured against the tree — see +[Verifying locally](#verifying-locally) for the exact commands, which are the +definition of each figure rather than a description of it. + +> **Read this first — the counts differ because they count different things.** +> There is no single "number of provers". The two figures most often confused: +> **141** is the number of `ProverKind` *enum variants*; **105** is the number +> of *backend implementation files* in `src/rust/provers/`. Both are correct. +> A surface quoting one of them as "the" count without saying which is drift — +> that is why historical counts (12, 30, 48, 74, 105, 128) are scattered across +> older documents. Prefer citing this file to quoting any number. ## TL;DR -| Question | Answer | -|---|---| -| Total `ProverKind` variants in `src/rust/provers/mod.rs` | **128** (~138 on `main` — see drift note above) | -| External prover bindings (separate binary or library) | 89 | -| `TypeChecker` disciplines routed via TypedWasm Sigma | 39 | -| Exposed by default REST API (`Tier 1` / core) | **12** (`GET /api/provers`) | -| With real `suggest_tactics` (not stub) | **91 of 91** | -| Routing tactic suggestions through `gnn_augment_tactics` | **all backends with `suggest_tactics`** (S5 pilot 5 + Tier-1 extension 5 + Tier-1 finisher 2 + Tier-2 sweep 33 + Tier-3/niche sweep 53 — full coverage as of 2026-05-30; gracefully no-ops when `gnn_api_url` is None or `neural_enabled` is false) | -| With native search command | 16 of 91 (72 return `Ok(vec![])` — cross-prover search via `VeriSimAdvisor` covers them) | -| Trust pipeline integrity-hashed | All Tier 1; Tier 2 incrementally | +| Question | Answer | Command | +|---|---|---| +| Total `ProverKind` variants in `src/rust/provers/mod.rs` | **141** | `V` below | +| Backend implementation files in `src/rust/provers/` | **105** | `F` below | +| Implementations providing `suggest_tactics` | **102** | `S` below | +| Exposed by default REST API (`Tier 1` / core) | **12** (`GET /api/provers`) | `C` below | +| Variants carrying a type-checker / discipline role | **46** | `D` below | +| Routing tactic suggestions through `gnn_augment_tactics` | **all backends with `suggest_tactics`** — gracefully no-ops when `gnn_api_url` is None or `neural_enabled` is false | — | +| Trust pipeline integrity-hashed | All Tier 1; Tier 2 incrementally | — | ## Tier table Tiers correspond to CI coverage cadence and default-API visibility. +> **Membership counts in this table are not machine-checked.** Tier 1 mirrors +> `ProverKind::all_core()` and is verified by command `C`. Tier 9 is verified by +> command `D`. The remaining per-tier figures (Tier 4's placeholder count, +> Tier 8's corpus-only count) are hand-maintained and have not been +> re-measured — treat them as indicative. Making tier membership derivable +> from the code (an attribute on each variant) is tracked as documentation +> debt in [`docs/DEBT.md`](DEBT.md). + | Tier | Cadence | Members | Notes | |---|---|---|---| | **1 — core** | Every PR | Agda, Coq, Lean 4, Isabelle/HOL, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2, HOL4 | Returned by `ProverKind::all_core()`; exposed by default at `GET /api/provers`; required to pass for green CI. Install hints in [`SUPPORTED_PROVERS.md`](SUPPORTED_PROVERS.md). | @@ -42,55 +50,84 @@ Tiers correspond to CI coverage cadence and default-API visibility. | **6 — pure-Rust** | Every PR | Metamath (own crate) | No external binary; in-process. | | **7 — Wave-2 modal/real-algebraic** | Every PR | Modal, real-algebraic provers (Phase 3 implementations) | See [`handover/PHASE-3-PROMPT.md`](handover/PHASE-3-PROMPT.md) | | **8 — HP type-checker ecosystem** | Nightly | 13 corpus-only provers (Ephapax / Wokelang / AffineScript backends) | Adapters pending; tracked in handover/TODO P4 | -| **9 — TypeChecker disciplines** | Every PR | 39 disciplines (Hindley-Milner, System F, Rank-N, ATS-style affine, …) | Routed via `crates/typed_wasm` Sigma parameters; do not require external binary. | +| **9 — TypeChecker disciplines** | Every PR | 46 variants carry a type-checker / discipline role (Hindley-Milner, System F, Rank-N, ATS-style affine, …) — command `D` | Routed via `crates/typed_wasm` Sigma parameters; do not require an external binary. | | **10 — Coq-Jr ecosystem (playground)** | Sub-project CI | `echidna-playground/` backends | Separate sub-project; tracked there. | ## Why so many counts in the wild? -History of the count drift: - -- v1.0 (Dec 2025): **12** real backends. Released as the MVP scope. -- v1.2 (Jan 2026): **30** declared, 12 fully tested. -- v1.3 (Feb 2026): **48** declared, ~32 with real `suggest_tactics`. -- v2.0 (Apr 2026): **74** after Wave-1 + Wave-2 absorption. -- v2.1 (May 2026): **105** after Wave-3 (Tamarin, ProVerif, Twelf, OR-Tools). -- v2.2 (May 2026): **128** after 39 TypeChecker disciplines were Sigma-routed - through TypedWasm (commit `c4bc272` and follow-on). -- v2.3 (May 2026): same **128** declared, but `gnn_augment_tactics` now wraps - every backend with `suggest_tactics` (S5 pilot c8a4f25 + #135 Tier-1 extension - + #136 Tier-1 finisher + Tier-2 sweep + Tier-3/niche sweep). Wiring is a - no-op when the Julia `/gnn/rank` service is unreachable; once trained - weights land (`models/neural/`), every backend automatically returns - model-derived premise-apply tactics at the top of its `suggest_tactics` - list. - -Documents in this repo predating each milestone often quote the count current -to their authoring date. When in doubt, **trust this file** and -`.machine_readable/6a2/STATE.a2ml`. +Two independent causes, and they need different remedies. + +**Cause 1 — genuine growth over time.** Each milestone's documents quote the +count current to their authoring date: + +| Release | Declared | What changed | +|---|---|---| +| v1.0 (Dec 2025) | 12 | MVP scope: 12 real backends | +| v1.2 (Jan 2026) | 30 | 12 fully tested | +| v1.3 (Feb 2026) | **48** | ~32 with real `suggest_tactics` | +| v2.0 (Apr 2026) | 74 | Wave-1 + Wave-2 absorption | +| v2.1 (May 2026) | **105** | Wave-3 (Tamarin, ProVerif, Twelf, OR-Tools) | +| v2.2 (May 2026) | **128** | TypeChecker disciplines Sigma-routed through TypedWasm | +| current `main` | **141** | measured, this file | + +Historical snapshots under `docs/releases/`, `docs/handover/` and +`docs/decisions/` are *deliberately* left at their authoring-time numbers — +they are records, not claims about today. + +**Cause 2 — counting different things and calling both "provers".** This is +the harmful one, because both numbers are defensible in isolation. 141 counts +enum variants; 105 counts implementation files; 102 counts implementations +exposing `suggest_tactics`; 12 counts the default-exposed core. A document that +says "N prover backends" without naming the denominator will be read as a claim +about all four. + +**Remedy:** cite this file rather than a number. The `R5a` canonical-reference +CI rule (`.github/canonical-references/prover-counts.yml`, enforced by the +`Canonical-reference drift (R5 generic)` step in the shared +`governance-reusable.yml`) fails the build when a bare count appears in a +load-bearing top-level document. Note its scope is the top-level document set +listed in that file — `docs/`, `.machine_readable/` and `crates/*/README.md` +are **not** covered, which is where the surviving drift accumulated. ## Verifying locally +Each command is the definition of its figure. Run from the repository root. + ```bash -# Total variant count -rg -c "^\s*[A-Z][a-zA-Z0-9_]+," src/rust/provers/mod.rs | head -1 +# V — total ProverKind variants (141) +awk '/pub enum ProverKind/{f=1;next} f&&/^\}/{exit} f' src/rust/provers/mod.rs \ + | grep -cE '^\s*[A-Z][A-Za-z0-9_]*\s*,' + +# F — backend implementation files (105) +ls src/rust/provers/*.rs | grep -cv 'mod\.rs$' -# Tier 1 core list -rg "fn all_core" -A 30 src/rust/provers/mod.rs +# S — implementations providing suggest_tactics (102) +git grep -l 'fn suggest_tactics' -- 'src/rust/provers/*.rs' | wc -l -# Per-tier breakdown -just provers # if implemented -echo "or read" -cat .machine_readable/provers.a2ml +# C — Tier-1 core, exposed by default at GET /api/provers (12) +awk '/fn all_core/{f=1} f&&/\]/{print;exit} f' src/rust/provers/mod.rs \ + | grep -oE 'ProverKind::[A-Za-z0-9_]+' | wc -l + +# D — variants carrying a type-checker / discipline role (46) +awk '/pub enum ProverKind/{f=1;next} f&&/^\}/{exit} f' src/rust/provers/mod.rs \ + | grep -icE 'typecheck|discipline' ``` +`ProverKind::all()` in `src/rust/provers/mod.rs` is the machine source of +truth; this document is its human-readable mirror. If a count changes, update +this file **and** `.machine_readable/provers.a2ml` in the same PR. + ## When to cite this file Cite `docs/PROVER_COUNT.md` (not a number) in: -- README.adoc tagline -- CLAUDE.md project overview -- Any new design doc +- the `README.md` tagline and the repository description +- `CLAUDE.md` project overview +- any new design doc - PR descriptions referring to "all backends" -- Issue templates +- issue templates + +When a number genuinely must appear (a release note, a benchmark table), name +the denominator: "141 `ProverKind` variants", not "141 provers". If a count changes (new wave absorbed, backend retired), update this file in the same PR. The single source of truth for the count is `ProverKind::all()` diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index 42f10c88..f1b43b1f 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -4,7 +4,7 @@ # ECHIDNA Roadmap **Status**: canonical • supersedes the aspirational parts of -[`FUTURE_DEVELOPMENT_ROADMAP.md`](./FUTURE_DEVELOPMENT_ROADMAP.md). +`FUTURE_DEVELOPMENT_ROADMAP.md` (removed from the tree; see git history). **Last revised**: 2026‑06‑01 (doc-coherence pass; previous revisions 2026‑05‑30 truthfulness audit, 2026‑04‑20) **Scope**: the shortest honest path from today's repo to the endpoint vision. @@ -223,7 +223,7 @@ follow a mould, localisation key additions. ## 6. Inheritance from existing planning docs -* **[`docs/FUTURE_DEVELOPMENT_ROADMAP.md`](FUTURE_DEVELOPMENT_ROADMAP.md)** +* **`docs/FUTURE_DEVELOPMENT_ROADMAP.md`** (removed from the tree; see git history) — 2026‑01‑29 vision document. Its chapters on RL for tactic search (§1.1), active learning (§1.2), and distributed dispatch map onto Stages 3c / 4c and 5b/5c of this roadmap. Retain as @@ -244,7 +244,7 @@ follow a mould, localisation key additions. * **[`docs/handover/L3-LIVE-PROVER-CI-PROMPT.md`](handover/L3-LIVE-PROVER-CI-PROMPT.md)** — implementation brief for Stage 5d. * **[`docs/handover/STATE.md`](handover/STATE.md)** and - **[`.machine_readable/6a2/STATE.a2ml`](../.machine_readable/6a2/STATE.a2ml)** + **[`.machine_readable/descriptiles/STATE.a2ml`](../.machine_readable/descriptiles/STATE.a2ml)** — running log of session‑by‑session progress. Continue to use as running state; sync highlights to §2 of this document at each sprint boundary. diff --git a/docs/decisions/2026-05-19-ci-baseline-triage.md b/docs/decisions/2026-05-19-ci-baseline-triage.md index cb643cfb..8bc8fa22 100644 --- a/docs/decisions/2026-05-19-ci-baseline-triage.md +++ b/docs/decisions/2026-05-19-ci-baseline-triage.md @@ -6,7 +6,7 @@ ADR-style record of the CI triage done while landing PR #73 and the two baseline-blocker follow-ups (#86, #87). Written so future humans **and** agents do not re-litigate these red checks. Companion machine-readable record: -`.machine_readable/6a2/STATE.a2ml § [session-2026-05-19-ci-baseline-triage]`. +`.machine_readable/descriptiles/STATE.a2ml § [session-2026-05-19-ci-baseline-triage]`. ## TL;DR for anyone debugging echidna PR CI diff --git a/docs/decisions/2026-05-30-chapel-rehabilitation.md b/docs/decisions/2026-05-30-chapel-rehabilitation.md index 9649efc9..356c2e8b 100644 --- a/docs/decisions/2026-05-30-chapel-rehabilitation.md +++ b/docs/decisions/2026-05-30-chapel-rehabilitation.md @@ -174,4 +174,4 @@ concrete, scoped engineering tasks. - `agda 2.6.3` against `agda-stdlib` (any 2.x compatible release). These pins are re-stated in `chapel-ci.yml` and `Justfile`; see -also `.machine_readable/6a2/META.a2ml` for the canonical record. +also `.machine_readable/descriptiles/META.a2ml` for the canonical record. diff --git a/docs/handover/HANDOVER-INDEX.md b/docs/handover/HANDOVER-INDEX.md index 19581109..39babaee 100644 --- a/docs/handover/HANDOVER-INDEX.md +++ b/docs/handover/HANDOVER-INDEX.md @@ -48,7 +48,7 @@ Read this index first to know which file is which. | File | What it is | |---|---| | [`TODO.md`](TODO.md) | Living backlog. Single source of truth for "what's next" between sprints. P0–P4 priority bands. | -| [`STATE.md`](STATE.md) | Running human-readable state log. Complement to `.machine_readable/6a2/STATE.a2ml`. | +| [`STATE.md`](STATE.md) | Running human-readable state log. Complement to `.machine_readable/descriptiles/STATE.a2ml`. | | [`README.md`](README.md) | Original handover suite intro (older; kept for orientation). | ## Warmup material diff --git a/docs/handover/L3-LIVE-PROVER-CI-PROMPT.md b/docs/handover/L3-LIVE-PROVER-CI-PROMPT.md index 393e62f0..928e3b2a 100644 --- a/docs/handover/L3-LIVE-PROVER-CI-PROMPT.md +++ b/docs/handover/L3-LIVE-PROVER-CI-PROMPT.md @@ -84,7 +84,7 @@ Per `feedback_verisimdb_policy`: the live-prover harness should emit a VeriSimDB ## Key files to read first 1. `~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md` -2. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/.machine_readable/6a2/STATE.a2ml` +2. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/.machine_readable/descriptiles/STATE.a2ml` 3. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/manifests/live-provers.scm` 4. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/.github/workflows/live-provers.yml` 5. `/var/mnt/eclipse/repos/verification-ecosystem/echidna/tests/live_prover_suite.rs` diff --git a/docs/handover/PHASE-3-PROMPT.md b/docs/handover/PHASE-3-PROMPT.md index 2d6c9364..48c39ecc 100644 --- a/docs/handover/PHASE-3-PROMPT.md +++ b/docs/handover/PHASE-3-PROMPT.md @@ -222,7 +222,7 @@ doesn't have to re-derive them: via `Command::spawn().context(...)`.) 6. `docs/ROADMAP.md` row "Every important solver" updated with the new ProverKind count (currently 128 → 134 after Phase 3 closes). -7. `PROOF-NEEDS.md` and `.machine_readable/6a2/STATE.a2ml` +7. `PROOF-NEEDS.md` and `.machine_readable/descriptiles/STATE.a2ml` reflect the closure of Phase 3. ## Non-goals diff --git a/docs/handover/PRODUCTION-WIRING-PLAN.md b/docs/handover/PRODUCTION-WIRING-PLAN.md index 5ec5099c..98ec977f 100644 --- a/docs/handover/PRODUCTION-WIRING-PLAN.md +++ b/docs/handover/PRODUCTION-WIRING-PLAN.md @@ -164,7 +164,7 @@ Applies to this plan: - `~/Desktop/ECHIDNA-L3-LIVE-PROVER-CI-PROMPT.md` — continuation prompt for L3 - `~/Desktop/ECHIDNA-L1-CAPNPROTO-PROMPT.md` — continuation prompt for L1 - `~/Desktop/ECHIDNA-L2-CHAPEL-PROMPT.md` — continuation prompt for L2 -- `.machine_readable/6a2/STATE.a2ml` — mirrored wave entry in-repo +- `.machine_readable/descriptiles/STATE.a2ml` — mirrored wave entry in-repo ## Session Log diff --git a/docs/handover/README.md b/docs/handover/README.md index 4bcedc8e..042d9ceb 100644 --- a/docs/handover/README.md +++ b/docs/handover/README.md @@ -36,7 +36,7 @@ copy wins because it is the committed one. deferred to Wave-3. Commits `9a4aeeb` + `6717b12`. - **L3 Wave-3** (Tier-3, weekly, 9 backends): scaffold only; needs per-backend Containerfiles. Handover hints in - `.machine_readable/6a2/STATE.a2ml` under `[wave-3-handover-hints]`. + `.machine_readable/descriptiles/STATE.a2ml` under `[wave-3-handover-hints]`. - **L3 Wave-4** (Tier-4, quarterly, 19 backends): scaffold only; retained as mock-only unless a maintainer volunteers. - **L2 Chapel**: `--features chapel` now self-links against bundled diff --git a/docs/handover/STATE.md b/docs/handover/STATE.md index 4503afa6..2dbac8be 100644 --- a/docs/handover/STATE.md +++ b/docs/handover/STATE.md @@ -90,7 +90,7 @@ Also corrected 2026-04-19 (were mis-listed as "planned"): - **Zig FFI** for C-ABI bridges to polyglot consumers. - **Justfile** primary build system; not Make. - **Containerfile** + Podman; not Dockerfile / Docker. -- **State files in `.machine_readable/6a2/` only**; never root. +- **State files in `.machine_readable/descriptiles/` only**; never root. - **All interfaces under `src/interfaces/`**; never extract to separate repos. - **When adding provers: update all 3 layers** (Rust backend, Julia ML, Chapel). - **Original name: "Cognitive Hybrid"** not "Computational Heuristic". @@ -135,7 +135,7 @@ Also corrected 2026-04-19 (were mis-listed as "planned"): | `verification-ecosystem/echidna/docs/handover/L1-CAPNPROTO-PROMPT.md` | L1 Cap'n Proto continuation prompt | | `verification-ecosystem/echidna/docs/handover/L2-CHAPEL-PROMPT.md` | L2 Chapel continuation prompt | | `verification-ecosystem/echidna/docs/handover/L3-LIVE-PROVER-CI-PROMPT.md` | L3 live-prover continuation prompt (marked Wave-2 DONE, pointing to Wave-3) | -| `verification-ecosystem/echidna/.machine_readable/6a2/STATE.a2ml` | Session ledger incl. `[l3-status-after-wave-2]` + `[wave-3-handover-hints]` | +| `verification-ecosystem/echidna/.machine_readable/descriptiles/STATE.a2ml` | Session ledger incl. `[l3-status-after-wave-2]` + `[wave-3-handover-hints]` | | `verification-ecosystem/echidna/docs/handover/README.md` | Index + drift-handling policy | ## Session log highlights (2026-04-26) diff --git a/docs/handover/TODO.md b/docs/handover/TODO.md index 59772359..e344624e 100644 --- a/docs/handover/TODO.md +++ b/docs/handover/TODO.md @@ -55,7 +55,7 @@ container *is* the escape hatch for the not-in-Guix / non-free tail (Guix primary, no Nix mirror; `flake.nix` deprecated and removed estate-wide 2026-06-01). Imandra target remains licence-gated. Table below kept for the per-backend install strategy of record. -Handover hints live in `.machine_readable/6a2/STATE.a2ml [wave-3-handover-hints]`. +Handover hints live in `.machine_readable/descriptiles/STATE.a2ml [wave-3-handover-hints]`. Strategy of record below = **as actually shipped & runtime-smoke-verified in `.containerization/Containerfile.wave3`** (2026-05-18, PR #73). Every diff --git a/docs/handover/llm-warmup-dev.md b/docs/handover/llm-warmup-dev.md index f7a8d45c..3244f6bc 100644 --- a/docs/handover/llm-warmup-dev.md +++ b/docs/handover/llm-warmup-dev.md @@ -166,10 +166,10 @@ members = [".", "src/interfaces/graphql", "src/interfaces/grpc", "src/interfaces ## Machine-Readable Metadata All in `.machine_readable/`: -- `6a2/STATE.a2ml` — Current state -- `6a2/META.a2ml` — Architecture decisions -- `6a2/ECOSYSTEM.a2ml` — Ecosystem position -- `6a2/AGENTIC.a2ml`, `NEUROSYM.a2ml`, `PLAYBOOK.a2ml` +- `descriptiles/STATE.a2ml` — Current state +- `descriptiles/META.a2ml` — Architecture decisions +- `descriptiles/ECOSYSTEM.a2ml` — Ecosystem position +- `descriptiles/AGENTIC.a2ml`, `NEUROSYM.a2ml`, `PLAYBOOK.a2ml` **NEVER** create these in the root directory. diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md index 5f497196..a24a69e1 100644 --- a/docs/tech-debt-2026-05-26.md +++ b/docs/tech-debt-2026-05-26.md @@ -5,6 +5,12 @@ SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) # Tech-Debt Audit — echidna — 2026-05-26 +> **Superseded — kept as a dated snapshot.** The live debt register is +> [`DEBT.md`](DEBT.md). This file records what an automated scan found on +> 2026-05-26 and is not maintained; its findings were not re-verified when +> `DEBT.md` was written, so treat any item here as unconfirmed until you re-run +> its measurement. + **Source:** estate-wide automated scan 2026-05-26. **Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits). **Combined severity:** `MEDIUM`. diff --git a/docs/wiki/Architecture.md b/docs/wiki/Architecture.md index 46a87f40..11fec651 100644 --- a/docs/wiki/Architecture.md +++ b/docs/wiki/Architecture.md @@ -10,8 +10,9 @@ component map and the 11-step trust pipeline walkthrough. ## Component map (one paragraph) ECHIDNA is a polyglot system. The **Rust core** (`src/rust/`, plus extracted -workspace crates in `crates/`) owns dispatch, the trust pipeline, and the 128 -prover backend implementations. Four API surfaces (CLI, REPL, REST/GraphQL +workspace crates in `crates/`) owns dispatch, the trust pipeline, and the prover +backend implementations (105 implementation files behind 141 `ProverKind` +variants — see [`docs/PROVER_COUNT.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/PROVER_COUNT.md)). Four API surfaces (CLI, REPL, REST/GraphQL on port 8000, gRPC on port 50051) hit `ProverDispatcher`, which picks a backend, runs the verification under sandboxing (Podman / bubblewrap), and walks the proof through the trust pipeline. A **Julia ML sidecar** diff --git a/docs/wiki/FAQ.md b/docs/wiki/FAQ.md index 2ae4a6f5..54955282 100644 --- a/docs/wiki/FAQ.md +++ b/docs/wiki/FAQ.md @@ -4,9 +4,17 @@ ## How many provers are supported? -**128 total** ProverKind variants: 89 external prover bindings plus 39 TypeChecker disciplines routed via TypedWasm Sigma. - -Of these, **12 core** are exposed by the default REST API: Coq/Rocq, Lean 4, Agda, Isabelle/HOL, Idris 2, F\*, Z3, CVC5, Alt-Ergo, Dafny, Vampire, E Prover. The remaining 116 are reachable via explicit `ProverKind` selection in CLI / REPL / GraphQL. +There is no single number, and that is the honest answer rather than a dodge: +the tree contains **141 `ProverKind` variants** across **105 backend +implementation files**, of which **102** provide `suggest_tactics`. Which figure +is "the" count depends on what you are counting. +[`docs/PROVER_COUNT.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/PROVER_COUNT.md) +is canonical and ships the commands that reproduce each one. + +**12 core** backends are exposed by the default REST API, mirroring +`ProverKind::all_core()`: Agda, Coq, Lean 4, Isabelle/HOL, Z3, CVC5, Metamath, +HOL Light, Mizar, PVS, ACL2, HOL4. Everything else is reachable via explicit +`ProverKind` selection in CLI / REPL / GraphQL. The full tier table lives in [`docs/PROVER_COUNT.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/PROVER_COUNT.md). @@ -34,12 +42,31 @@ No. **The repo wins** when the wiki and the in-repo docs disagree. The wiki is a Canonical sources of truth: - [`CLAUDE.md`](https://github.com/hyperpolymath/echidna/blob/main/CLAUDE.md) for codebase orientation -- [`.machine_readable/6a2/STATE.a2ml`](https://github.com/hyperpolymath/echidna/blob/main/.machine_readable/6a2/STATE.a2ml) for current state +- [`.machine_readable/descriptiles/STATE.a2ml`](https://github.com/hyperpolymath/echidna/blob/main/.machine_readable/descriptiles/STATE.a2ml) for current state - [`docs/ROADMAP.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/ROADMAP.md) for direction -## Why MPL-2.0 and not MIT or AGPL? +## What licence is ECHIDNA under? + +**The repository is currently inconsistent on this point, and you should not +rely on this page.** Read +[`LICENSE`](https://github.com/hyperpolymath/echidna/blob/main/LICENSE) and, if +your use depends on the answer, ask the maintainer before proceeding. + +What the tree actually says today: + +| Surface | States | +|---|---| +| `LICENSE`, `Cargo.toml`, README badge | AGPL-3.0-or-later | +| Per-file `SPDX-License-Identifier` headers (588 source files) | MPL-2.0 | +| `NOTICE` | MPL-2.0 ("Full text: LICENSE" — which is AGPL) | +| `.reuse/dep5` | PMPL-1.0 AND Palimpsest-0.6 | -Practical balance: weak copyleft at the file level (modifications to MPL'd files must be open) without copyleft-by-linking (so downstream commercial use is straightforward). The project migrated from a dual MIT/Palimpsest-0.6 licence in 2026; `NOTICE` and `LICENSE` reflect the current state. +The owner's recorded decision is AGPL-3.0-or-later; the per-file headers and +`NOTICE` predate it and have not been migrated. Reconciling them is tracked as +P0 licensing debt in +[`docs/DEBT.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/DEBT.md). +The historical migration path was dual MIT/Palimpsest-0.6 → MPL-2.0 → (decided) +AGPL-3.0-or-later. ## How do I report a security issue? diff --git a/docs/wiki/Home.md b/docs/wiki/Home.md index aeb4899e..20bddb74 100644 --- a/docs/wiki/Home.md +++ b/docs/wiki/Home.md @@ -2,9 +2,11 @@ # ECHIDNA Wiki -**ECHIDNA** — Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance — is a trust-hardened neurosymbolic theorem-proving platform supporting **128 prover backends** (12 core, exposed by default API; see [`docs/PROVER_COUNT.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/PROVER_COUNT.md) for the tier breakdown). +**ECHIDNA** — Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance — is a trust-hardened neurosymbolic theorem-proving platform with a large multi-backend prover surface, of which **12 core backends** are exposed by the default API. Counts differ depending on what is being counted; [`docs/PROVER_COUNT.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/PROVER_COUNT.md) is canonical and carries the commands that reproduce each figure. -**License**: MPL-2.0 (documentation surface) · authoritative version pinned in [`Cargo.toml`](https://github.com/hyperpolymath/echidna/blob/main/Cargo.toml) and [`CHANGELOG.md`](https://github.com/hyperpolymath/echidna/blob/main/CHANGELOG.md) +**License**: the repository declares **AGPL-3.0-or-later** ([`LICENSE`](https://github.com/hyperpolymath/echidna/blob/main/LICENSE), `Cargo.toml`). Note that per-file `SPDX-License-Identifier` headers across the source tree still read `MPL-2.0`, and `NOTICE` still describes the project as MPL-2.0 — this inconsistency is **open licensing debt**, tracked in [`docs/DEBT.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/DEBT.md). Until it is reconciled by the owner, do not rely on this page for the licence terms; read `LICENSE` and seek clarification. + +**Release history**: [`CHANGELOG.md`](https://github.com/hyperpolymath/echidna/blob/main/CHANGELOG.md); semver pin in [`Cargo.toml`](https://github.com/hyperpolymath/echidna/blob/main/Cargo.toml). ## Quick navigation @@ -18,7 +20,7 @@ When the wiki and the repo disagree, **the repo wins**: -- [`README.adoc`](https://github.com/hyperpolymath/echidna/blob/main/README.adoc) — primary project README +- [`README.md`](https://github.com/hyperpolymath/echidna/blob/main/README.md) — primary project README - [`CLAUDE.md`](https://github.com/hyperpolymath/echidna/blob/main/CLAUDE.md) — codebase orientation - [`docs/ARCHITECTURE.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/ARCHITECTURE.md) — current architecture - [`docs/PROVER_COUNT.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/PROVER_COUNT.md) — tier table @@ -26,7 +28,7 @@ When the wiki and the repo disagree, **the repo wins**: - [`docs/ROADMAP.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/ROADMAP.md) — stage map and sprint targets - [`docs/handover/HANDOVER-INDEX.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/handover/HANDOVER-INDEX.md) — handover/ navigation - [`RSR_COMPLIANCE.adoc`](https://github.com/hyperpolymath/echidna/blob/main/RSR_COMPLIANCE.adoc) — RSR / CCCP compliance statement -- [`.machine_readable/6a2/STATE.a2ml`](https://github.com/hyperpolymath/echidna/blob/main/.machine_readable/6a2/STATE.a2ml) — machine-readable state +- [`.machine_readable/descriptiles/STATE.a2ml`](https://github.com/hyperpolymath/echidna/blob/main/.machine_readable/descriptiles/STATE.a2ml) — machine-readable state ## Core invariants @@ -35,7 +37,7 @@ When the wiki and the repo disagree, **the repo wins**: ## Key concepts -- **128 backends, 12 core** — 89 external prover bindings + 39 TypeChecker disciplines via TypedWasm Sigma. +- **12 core backends** exposed by default; the wider surface (external prover bindings plus TypeChecker disciplines routed via TypedWasm Sigma) is reachable through explicit `ProverKind` selection. Figures and their denominators: [`docs/PROVER_COUNT.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/PROVER_COUNT.md). - **17 corpus adapters** — every major public proof corpus has a structural ingest path (see [`docs/CORPUS-ADAPTERS.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/CORPUS-ADAPTERS.md)). - **4 arbitration mechanisms** — portfolio majority-vote, Bayesian posterior, Dempster-Shafer belief combination, Pareto multi-objective frontier. - **6 cross-prover exchange formats** — OpenTheory, Dedukti, TPTP, SMT-LIB, SMTCoq, Lambdapi. diff --git a/docs/wiki/README.md b/docs/wiki/README.md index 91508183..12b0cd29 100644 --- a/docs/wiki/README.md +++ b/docs/wiki/README.md @@ -1,14 +1,27 @@ # ECHIDNA Wiki — Source Pages -These six files mirror what the GitHub wiki at -should display. The wiki repo (`echidna.wiki.git`) sits outside the main -repository and is not pushable from automation in this session, so the -canonical wiki content lives here and is synced manually by an editor with -push rights. +These six files are the **source of truth** for the GitHub wiki at +. The wiki lives in a separate +repository (`echidna.wiki.git`); edit the pages here, then sync. -To sync: paste each file's body (everything after the H1) into the matching -wiki page via the GitHub web UI, or `git clone https://github.com/hyperpolymath/echidna.wiki.git` -and copy these files directly. Wiki pages are flat — there is no nesting. +**Syncing is scriptable** — an earlier note in this file claimed the wiki was +not pushable from automation. It is: `echidna.wiki.git` accepts a normal clone +and push with the same credentials as the main repository. Its default branch +is `master`, not `main`. + +```bash +git clone https://github.com/hyperpolymath/echidna.wiki.git /tmp/echidna-wiki +for f in Home Architecture Getting-Started FAQ Guides Troubleshooting; do + cp docs/wiki/"$f".md /tmp/echidna-wiki/"$f".md +done +git -C /tmp/echidna-wiki add -A +git -C /tmp/echidna-wiki commit -m "docs: sync wiki from docs/wiki/" +git -C /tmp/echidna-wiki push origin master +``` + +Wiki pages are flat — there is no nesting, and the filename is the page name. +Editing a page in the GitHub web UI bypasses this directory and will be +overwritten by the next sync, so make changes here. | Wiki page | Source file | |---|---| From 4e4b11c60ea0e6bcc6b3d3f69b7642027d712be6 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 7 Aug 2026 12:52:04 +0100 Subject: [PATCH 2/2] =?UTF-8?q?docs(debt):=20add=20C4/C5=20=E2=80=94=20Dog?= =?UTF-8?q?food=20Gate=20K9=20validation=20and=20Rust=20CI=20test=20failur?= =?UTF-8?q?es?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both observed while verifying this PR's own CI. Recorded with what was actually confirmed and no more: the K9 error text is quoted verbatim; the Rust CI failure is identified as a genuine post-build test failure (exit 101 under llvm-cov) rather than the lockfile-pin startup failure that masked it until the dtolnay/rust-toolchain relock, but the individual failing tests are not enumerated and the entry says so. Co-Authored-By: Claude Opus 5 --- docs/DEBT.md | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/docs/DEBT.md b/docs/DEBT.md index 127f2c70..116f05e6 100644 --- a/docs/DEBT.md +++ b/docs/DEBT.md @@ -238,7 +238,36 @@ runs stub-sentinel detection for Tier-3 cells; the corresponding guarantee for Tier-4 placeholders at the API boundary is not documented. Related: D2 — the placeholder count itself is unverified. -### C4. Unfinished-work markers +### C4. `Dogfood Gate` fails K9 validation on `main` + +Observed 2026-08-07 on every PR run: + +``` +Hunt-level K9 file must include a 'signature' or 'signature_required' field +K9 validation failed with 1 error(s) +``` + +A contractile/K9 schema requirement that the repository's own hunt-level K9 +file does not satisfy — the dogfooding gate cannot pass its own rules. Not +diagnosed further here; reproduce with +`gh run list -R hyperpolymath/echidna --workflow "Dogfood Gate"` and read the +failing step. + +### C5. `Rust CI` test failures on `main` + +`cargo test --tests --workspace --locked` exits 101 under `llvm-cov`. This is a +genuine test failure, not infrastructure: it appears **after** the toolchain +installs and the workspace builds. Distinguish it from the lockfile-pin +startup failures that affected the same workflow until the +`dtolnay/rust-toolchain@stable` relock — those failed *before* running a step +and produced no test output. Individual failing tests have not been +enumerated; that is the next action. + +`Secret Scanner` also exits 1 on `main`; likely the dead `VERISIMDB_PAT` +already tracked in [#310](https://github.com/hyperpolymath/echidna/issues/310), +but not confirmed here. + +### C6. Unfinished-work markers Low and healthy for a tree this size — recorded as a baseline to watch: