hyperpolymath
diff --git a/‎AUTHORS.md‎
Lines changed: 47 additions & 71 deletions b/‎AUTHORS.md‎
Lines changed: 47 additions & 71 deletions
diff --git a/‎CLAUDE.md‎
Lines changed: 39 additions & 2 deletions b/‎CLAUDE.md‎
Lines changed: 39 additions & 2 deletions
diff --git a/‎CODE_OF_CONDUCT.md‎
Lines changed: 14 additions & 5 deletions b/‎CODE_OF_CONDUCT.md‎
Lines changed: 14 additions & 5 deletions
diff --git a/‎MAINTAINERS.adoc‎
Lines changed: 15 additions & 1 deletion b/‎MAINTAINERS.adoc‎
Lines changed: 15 additions & 1 deletion
diff --git a/‎QUICKSTART-DEV.adoc‎
Lines changed: 49 additions & 8 deletions b/‎QUICKSTART-DEV.adoc‎
Lines changed: 49 additions & 8 deletions
@@ -1,54 +1,33 @@
 <!--
 SPDX-License-Identifier: MPL-2.0
-SPDX-FileCopyrightText: 2024-2025 ECHIDNA Project Contributors
+SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 
 # Authors and Contributors
 
-This file lists the authors and contributors to the ECHIDNA project. We are grateful to everyone who has contributed to making ECHIDNA a reality.
+This file lists the authors and contributors to the ECHIDNA project.
+The authoritative running list lives in the git history — `git shortlog
+-sne` will produce a deduplicated, frequency-sorted view at any commit.
 
-## Project Maintainers
+## Maintainers
 
-The following individuals are the core maintainers of ECHIDNA:
+| Name | Role | Contact |
+|---|---|---|
+| Jonathan D.A. Jewell | Lead Maintainer | [@hyperpolymath](https://github.com/hyperpolymath), `j.d.a.jewell@open.ac.uk` |
 
-- **ECHIDNA Project Team** - Project coordination and oversight
+See [`MAINTAINERS.adoc`](MAINTAINERS.adoc) for the maintainer
+responsibility model and the path to becoming a maintainer.
 
-## Core Contributors
+## Contributors
 
-Contributors who have made significant contributions to the codebase:
+Code, documentation, infrastructure, review, issue triage. The
+deduplicated running list is in the git history:
 
-<!-- Contributors will be added here as they make contributions -->
+```bash
+git shortlog -sne
+```
 
-## Code Contributors
-
-All contributors to the ECHIDNA codebase (in alphabetical order):
-
-<!-- This section will be automatically updated based on git history -->
-
-## Documentation Contributors
-
-Contributors who have improved documentation:
-
-<!-- Documentation contributors will be listed here -->
-
-## Special Thanks
-
-We would like to extend special thanks to:
-
-- **Theorem Proving Community** - For foundations and inspiration
-- **Theorem Prover Communities** - For developing and maintaining the 12 provers we integrate
-- **Rhodium Standard Repository (RSR/CCCP)** - For compliance guidelines
-- **Palimpsest License** - For ethical licensing framework
-
-## How to Be Added
-
-If you've contributed to ECHIDNA and your name isn't listed here, please:
-
-1. Open an issue or merge request on GitLab
-2. Provide a brief description of your contribution
-3. Indicate how you'd like to be credited
-
-We recognize all forms of contribution, including but not limited to:
+We recognise all forms of contribution including but not limited to:
 
 - Code contributions
 - Documentation improvements
@@ -59,48 +38,45 @@ We recognize all forms of contribution, including but not limited to:
 - Design and artwork
 - Infrastructure and tooling
 
-## Contribution Statistics
-
-<!-- Generated statistics will appear here -->
-
-### By Component
-
-- **Rust Core**: TBD contributors
-- **Julia ML**: TBD contributors
-- **ReScript UI**: TBD contributors
-- **Documentation**: TBD contributors
-- **Tests**: TBD contributors
-- **Infrastructure**: TBD contributors
-
-### By Prover Backend
-
-- **Tier 1 (Agda, Coq, Lean, Isabelle, Z3, CVC5)**: TBD contributors
-- **Tier 2 (Metamath, HOL Light, Mizar)**: TBD contributors
-- **Tier 3 (PVS, ACL2)**: TBD contributors
-- **Tier 4 (HOL4)**: TBD contributors
+## Special Thanks
 
-## Institutional Support
+- **The theorem-proving community** — for the foundations and the
+  ongoing maintenance of the backends ECHIDNA integrates with
+  (Coq/Rocq, Lean, Agda, Isabelle, Idris2, F*, HOL Light, Mizar,
+  PVS, ACL2, HOL4, Z3, CVC5, Vampire, E Prover, and the long tail
+  in [`docs/PROVER_COUNT.md`](docs/PROVER_COUNT.md)).
+- **The Rhodium Standard Repository (RSR/CCCP)** — for the
+  compliance template that this repo extends; see
+  [`RSR_COMPLIANCE.adoc`](RSR_COMPLIANCE.adoc).
 
-Organizations and institutions that have supported ECHIDNA development:
+## How to be added
 
-<!-- Institutional supporters will be listed here -->
+If you've contributed to ECHIDNA and would like to be acknowledged
+beyond the git history, open an issue or PR on
+[GitHub](https://github.com/hyperpolymath/echidna/issues) with the
+attribution you would like.
 
-## License
+## License of contributions
 
-All contributions to ECHIDNA are licensed under the dual license:
-- MIT License
-- Palimpsest License v0.6
+Source files are licensed per the SPDX header at the top of each
+file; the project root [`LICENSE`](LICENSE) and the per-tree
+[`.reuse/dep5`](.reuse/dep5) catalogue together describe the
+authoritative position. By contributing you agree to license your
+contribution under the licence noted on the file you touch (or the
+project default for new files).
 
-By contributing to ECHIDNA, you agree to license your contributions under these terms.
+The documentation surface is intentionally `MPL-2.0` — see
+[`feedback_echidna_license_docs_mpl_intentional`](https://github.com/hyperpolymath/echidna/issues?q=license)
+for the deliberation.
 
 ## Contact
 
-For questions about attribution or contributions:
-- GitLab Issues: https://github.com/hyperpolymath/echidna/-/issues
-- Email: contributors@echidna-project.org (when available)
+- **GitHub Issues**: <https://github.com/hyperpolymath/echidna/issues>
+- **Security**: see [`SECURITY.md`](SECURITY.md) — use GitHub
+  Security Advisories for vulnerabilities, not public issues.
 
 ---
 
-**Last Updated**: 2025-11-22
-
-*This file is maintained by the ECHIDNA Project Team. If you notice any errors or omissions, please let us know.*
+*This file is intentionally count-free and date-free in prose. The
+git history is the running timeline; the canonical attribution
+surface is `git shortlog -sne`.*
@@ -139,10 +139,14 @@ Shape, by area:
 # Build System (Justfile is PRIMARY — RSR-H14)
 just build              # Build the project
 just test               # Run tests
-just check              # Run all quality checkers
+just check              # Roll-up: fmt-check + lint + test
+just lint               # REUSE + rustfmt + clippy
+just pre-commit         # fmt-check + lint + test (use in git hooks)
 just doctor             # Verify toolchain
-just heal               # Auto-install missing tools
+just heal               # Offer to install missing tools
 just tour               # Codebase tour
+just help-me            # Onboarding subset of recipes
+just --list             # Every recipe in the Justfile
 
 # Cargo
 cargo build             # Build Rust code
@@ -153,6 +157,16 @@ cargo bench             # Criterion benchmarks
 cargo clippy            # Rust lints
 cargo fmt --check       # Format check
 
+# CLI entry points (clap-routed in src/rust/main.rs)
+cargo run -- interactive          # Launch interactive REPL
+cargo run -- server --cors        # Launch HTTP API server (port 8081)
+cargo run -- list-provers         # List ProverKind variants on this build
+cargo run -- info <PROVER>        # Show backend metadata
+cargo run -- prove <file>         # Prove a theorem from file
+cargo run -- verify <file>        # Verify an existing proof
+cargo run -- search <pattern>     # Search theorem libraries
+cargo run -- diagnostics          # Interactive diagnostics REPL
+
 # Idris2 ABI
 idris2 --build src/abi/echidnaabi.ipkg   # Type-check the ABI package
 
@@ -162,6 +176,29 @@ podman run echidna                        # Run minimal image
 # Per-prover images live under .containerization/Containerfile.wave3
 ```
 
+## Governance gates
+
+CI enforces estate-wide governance through reusable workflows pinned
+in `.github/workflows/`:
+
+- **R5a** (echidna-local, post-#174): doc canonical-reference drift
+  for prover counts; canonical refs live under
+  `.github/canonical-references/`.
+- **R5b** (estate-wide, consumed via standards SHA pin per #172):
+  `Version: x.y.z` strings in docs are scanned for drift against
+  `Cargo.toml`. **`CHANGELOG.md` and `Cargo.toml` are exempt;
+  everything else is not.** Keep this file (and any new doc) prose
+  count-free and version-free unless the number is sourced
+  authoritatively elsewhere.
+- **MVP smoke** (#167): just-pinned smoke harness on every PR;
+  reports missing prover binaries non-fatally.
+- **Idris2 ABI type-check**: `idris2-abi-ci.yml` enforces zero
+  `believe_me` / `assert_total` / `postulate` in `src/abi/`.
+- **Chapel CI**: `chapel-ci.yml` builds the static lib + Zig FFI
+  strict on every PR.
+- **Container CI**: `container-ci.yml` weekly cron builds each
+  Tier-3 cell with stub-sentinel detection.
+
 ## Critical Constraints
 
 - **No Python** outside `salt/` (RSR-H4) — Julia for ML, Rust for systems, AffineScript/ReScript for UI.
 
@@ -56,9 +56,14 @@ It also applies when an individual is officially representing the project in pub
 
 ### Reporting
 
-Instances of abusive, harassing, or otherwise unacceptable behavior may be reported to the project team at:
+Instances of abusive, harassing, or otherwise unacceptable behaviour may be reported through either of the following channels:
 
-**echidna-conduct@example.org** (Replace with actual contact)
+- **GitHub Security Advisories** (preferred — private, encrypted,
+  auditable): <https://github.com/hyperpolymath/echidna/security/advisories/new>
+  Tag the report as a conduct matter.
+- **Email** (fallback): `j.d.a.jewell@open.ac.uk` — maintainer;
+  PGP key `4A03639C1EB1F86C7F0C97A91835A14A2867091E` published on
+  https://keys.openpgp.org.
 
 All complaints will be reviewed and investigated promptly and fairly.
 
@@ -106,6 +111,10 @@ For answers to common questions about this code of conduct, see the FAQ at https
 
 ---
 
-**Version**: 1.0
-**Last Updated**: 2025-11-22
-**Contact**: echidna-conduct@example.org (Replace with actual contact)
+**Lineage**: Adapted from the [Contributor Covenant](https://www.contributor-covenant.org/)
+v2.1. Revisions tracked via `git log CODE_OF_CONDUCT.md`. This file
+is intentionally version-free and date-free in prose to avoid R5b
+drift.
+
+**Contact**: <https://github.com/hyperpolymath/echidna/security/advisories/new>
+(preferred) or `j.d.a.jewell@open.ac.uk` (fallback).
@@ -44,4 +44,18 @@ May be invited to become maintainers at the discretion of existing maintainers.
 
 == Contact
 
-For questions about project governance, open an issue or contact the maintainers listed above.
+For questions about project governance, open an issue or contact
+the maintainers listed above. For security disclosures, use the
+GitHub Security Advisories route documented in
+link:SECURITY.md[`SECURITY.md`] — do NOT open public issues for
+vulnerabilities.
+
+For high-level direction the canonical surfaces are:
+
+* link:README.adoc[`README.adoc`] — overview, distinguishing features
+* link:docs/ROADMAP.md[`docs/ROADMAP.md`] — stage map + sprint plan
+* link:CHANGELOG.md[`CHANGELOG.md`] — release history
+* link:docs/PROVER_COUNT.md[`docs/PROVER_COUNT.md`] — canonical
+  backend tier table
+* link:RSR_COMPLIANCE.adoc[`RSR_COMPLIANCE.adoc`] — hard-rule
+  compliance and out-of-template adaptations
@@ -1,32 +1,48 @@
 = Echidna — Developer Quickstart
 :toc: preamble
 
-Clone, build, test, contribute.
+Clone, build, test, contribute. The user-facing analogue lives in
+link:QUICKSTART-USER.adoc[`QUICKSTART-USER.adoc`]; release / packaging
+is in link:QUICKSTART-MAINTAINER.adoc[`QUICKSTART-MAINTAINER.adoc`].
 
 == Prerequisites
 
 * Git 2.40+
-* just (command runner)
+* just (command runner) — `cargo install just`
 * See `just doctor` output for language-specific requirements
 
+For the full optional toolchain (Julia, Idris2, Zig, Chapel, Deno) see
+link:QUICKSTART-USER.adoc[`QUICKSTART-USER.adoc`]; only Rust + just +
+pkg-config + openssl-devel are mandatory.
+
 == Setup
 
 [source,bash]
 ----
 git clone https://github.com/hyperpolymath/echidna
 cd echidna
 just doctor    # verify toolchain
-just heal      # auto-install missing tools
+just heal      # offer to install missing tools (non-destructive)
+just tour      # guided codebase walkthrough
+just help-me   # onboarding subset of recipes
 ----
 
 == Development Workflow
 
 [source,bash]
 ----
-just tour      # understand the codebase
-just help-me   # see available commands
+just build              # debug build
+just test               # all Rust tests
+just lint               # REUSE + rustfmt + clippy
+just pre-commit         # fmt-check + lint + test
+just check              # roll-up: fmt-check + lint + test
+cargo run -- interactive    # launch the REPL
+cargo run -- server --cors  # launch the API server on 8081
 ----
 
+The full recipe set is in `Justfile`; `just --list` enumerates
+every recipe.
+
 == Optional: Chapel Parallel Proof Search
 
 The Rust core exposes an optional parallel-search path that calls into
@@ -43,17 +59,42 @@ cargo test  --features chapel --lib proof_search
 ----
 
 With Chapel actually installed and `libechidna_chapel.so` built from
-`chapel_poc/`, pass `-Dstubs=false` to the Zig build and link the
+`src/chapel/`, pass `-Dstubs=false` to the Zig build and link the
 Chapel library alongside. Stubs return "Chapel unavailable" at runtime
 so `cargo test --features chapel` still passes on hosts without Chapel.
 
+The Justfile wrappers (`just build-chapel`, `just chapel-build`,
+`just chapel-smoke`, `just chapel-test`, `just bench-chapel-mrr`,
+`just test-chapel-ffi`) cover the common flows; `just --list | grep chapel`
+shows them all.
+
+== Idris2 ABI
+
+The on-wire contract between the Rust dispatcher, the Julia GNN
+ranker, and the Chapel parallel rank-merge is pinned in `src/abi/`.
+Type-check before pushing if you touched anything that touches the
+ABI surface:
+
+[source,bash]
+----
+idris2 --build src/abi/echidnaabi.ipkg
+----
+
+CI enforces zero `believe_me` / `assert_total` / `postulate` in the
+ABI modules via `.github/workflows/idris2-abi-ci.yml`.
+
 == Before Committing
 
 [source,bash]
 ----
-just assail    # run panic-attacker security scan
+just pre-commit    # fmt-check + lint + test
+just assail        # panic-attacker security scan (requires panic-attack CLI)
 ----
 
+All commits must be GPG-signed and follow Conventional Commits — see
+link:CONTRIBUTING.adoc[`CONTRIBUTING.adoc`] for the full policy.
+
 == Contributing
 
-See link:CONTRIBUTING.md[CONTRIBUTING.md] for guidelines.
+See link:CONTRIBUTING.adoc[CONTRIBUTING.adoc] for guidelines (the
+canonical, AsciiDoc version). `CONTRIBUTING.md` is a thin pointer.