From 19f05114e73699ccf7023ac5efbd341942734e59 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 23 Aug 2026 20:04:23 +0100 Subject: [PATCH 1/2] chore: global textual eradication of Nix and ReScript --- .claude/CLAUDE.md | 4 ++-- .machine_readable/contractiles/Justfile | 10 +++++----- .well-known/humans.txt | 2 +- 0-AI-MANIFEST.a2ml | 2 +- CANONICAL_SOURCE.md | 4 ++-- CONTRIBUTING.md | 2 +- Justfile | 10 +++++----- RELEASE_CHECKLIST.md | 2 +- RSR_COMPLIANCE.adoc | 4 ++-- RSR_OUTLINE.adoc | 6 +++--- examples/web-project-deno.json | 16 ++++++++-------- 11 files changed, 31 insertions(+), 31 deletions(-) diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index e70e536..c024ea7 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -76,8 +76,8 @@ Both are FOSS with independent governance (no Big Tech). ### Package Management -- **Sole primary**: Guix (guix.scm) — nix is deprecated estate-wide - 2026-06-01; do NOT add flake.nix/flake.lock back +- **Sole primary**: Guix (guix.scm) — guix is deprecated estate-wide + 2026-06-01; do NOT add flake.guix/flake.lock back - **JS deps**: Deno (deno.json imports) ### Security Requirements diff --git a/.machine_readable/contractiles/Justfile b/.machine_readable/contractiles/Justfile index 2db3d94..a339fff 100644 --- a/.machine_readable/contractiles/Justfile +++ b/.machine_readable/contractiles/Justfile @@ -88,7 +88,7 @@ build *args: # cargo build {{args}} # Rust # mix compile {{args}} # Elixir # zig build {{args}} # Zig - # deno task build {{args}} # Deno/ReScript + # deno task build {{args}} # Deno/AffineScript @echo "Build complete" # Build in release mode with optimizations @@ -559,7 +559,7 @@ state-phase: @grep -oP 'phase\s*=\s*"\K[^"]+' .machine_readable/STATE.a2ml 2>/dev/null | head -1 || echo "unknown" # ═══════════════════════════════════════════════════════════════════════════════ -# GUIX & NIX +# GUIX & GUIX # ═══════════════════════════════════════════════════════════════════════════════ # Enter Guix development shell (primary) @@ -570,9 +570,9 @@ guix-shell: guix-build: guix build -f guix.scm -# Enter Nix development shell (fallback) -nix-shell: - @if [ -f "flake.nix" ]; then nix develop; else echo "No flake.nix"; fi +# Enter Guix development shell (fallback) +guix-shell: + @if [ -f "flake.guix" ]; then guix develop; else echo "No flake.guix"; fi # ═══════════════════════════════════════════════════════════════════════════════ # HYBRID AUTOMATION diff --git a/.well-known/humans.txt b/.well-known/humans.txt index c95d4fe..e503a45 100644 --- a/.well-known/humans.txt +++ b/.well-known/humans.txt @@ -18,4 +18,4 @@ Standards: Consent-Aware HTTP, RSR /* PHILOSOPHY */ Design: Reversibility-first Ethics: Consent-aware -Language: Tier 1 RSR (Rust, Elixir, Zig, Ada, Haskell, ReScript) +Language: Tier 1 RSR (Rust, Elixir, Zig, Ada, Haskell, AffineScript) diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 5d48c1b..fe9caa7 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -41,4 +41,4 @@ respect-claude-md = true # .claude/CLAUDE.md is binding for AI assistants 2026-04-17 = "migrated from Guile Scheme (`.machine_readable/6scm/*.scm`) to TOML-flavoured A2ML (`.machine_readable/6a2/*.a2ml`)" 2026-04-25 = "bot_directives extended with [bot] mode-resolver block" 2026-04-26 = "test suite reached 184/184 passing" -2026-05-30 = ".claude/CLAUDE.md flipped ReScript→AffineScript per estate policy" +2026-05-30 = ".claude/CLAUDE.md flipped AffineScript→AffineScript per estate policy" diff --git a/CANONICAL_SOURCE.md b/CANONICAL_SOURCE.md index f25283c..ab58c8e 100644 --- a/CANONICAL_SOURCE.md +++ b/CANONICAL_SOURCE.md @@ -74,9 +74,9 @@ The **fleet copy** is the **deployed production bot**: | `tests/webhook_e2e_test.rs` | **fleet** | fleet → standalone (recommended) | End-to-end webhook test was added during fleet deployment hardening; should be promoted back to standalone. | | `fuzz/fuzz_targets/fuzz_hmac.rs`, `fuzz_webhook_json.rs` | **standalone** | standalone → fleet (on demand) | Fuzz target expansion lives in standalone (also `.clusterfuzzlite/`). | | `examples/*.affine` (e.g. `SafeDOMExample.affine`) | **fleet** | fleet → standalone (on `.affine` migration) | Estate `.affine` migration touched the fleet copy first; will reach standalone when the SafeDOM stdlib lands (`affinescript#56`). | -| `examples/*.json`, `examples/*.ts`, `examples/*.rescript` | **standalone** | standalone → fleet | Reference examples for SDK users. | +| `examples/*.json`, `examples/*.ts`, `examples/*.affinescript` | **standalone** | standalone → fleet | Reference examples for SDK users. | | `echidnabot.example.toml`, `echidnabot.toml` | **standalone** | standalone → fleet | Configuration *schema* is SDK surface; fleet should mirror schema and only override defaults. | -| `Containerfile`, `flake.nix`, `guix.scm` | **standalone** | standalone → fleet | Reproducible-build manifests are SDK surface. Fleet may override base image for deploy. | +| `Containerfile`, `flake.guix`, `guix.scm` | **standalone** | standalone → fleet | Reproducible-build manifests are SDK surface. Fleet may override base image for deploy. | | `packaging/**` (debian/, rpm/, arch/, aur/, chocolatey/, macports/, scoop/) | **standalone** | standalone → fleet (when versions bump) | Distribution packaging is release-process artefact. | | `hooks/**` (git hooks: SPDX, SHA-pins, CodeQL, permissions, tsjs-blocker) | **standalone** | standalone → fleet | Governance hooks; standalone is the source of truth. | | `README.adoc`, `README.md`, `CHANGELOG.md` (vs `CHANGELOG.adoc`), `ROADMAP.adoc`, `CITATION.cff`, `codemeta.json`, `PALIMPSEST.adoc` | **standalone** | standalone → fleet | Doc canon. The `.md` vs `.adoc` CHANGELOG split is a long-standing inconsistency; standalone uses both. | diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index d1a8605..b2b02c7 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -24,7 +24,7 @@ This document covers the practicalities. For project conduct, see git clone https://github.com/hyperpolymath/echidnabot.git cd echidnabot -# Reproducible environment (Guix is the estate primary; nix is deprecated 2026-06-01) +# Reproducible environment (Guix is the estate primary; guix is deprecated 2026-06-01) guix shell -D -f guix.scm # Guix package (guix.scm) # Or bring your own toolchain (Rust 1.75+, SQLite, podman/bwrap) diff --git a/Justfile b/Justfile index bd72caa..9d376e2 100644 --- a/Justfile +++ b/Justfile @@ -89,7 +89,7 @@ build *args: # cargo build {{args}} # Rust # mix compile {{args}} # Elixir # zig build {{args}} # Zig - # deno task build {{args}} # Deno/ReScript + # deno task build {{args}} # Deno/AffineScript @echo "Build complete" # Build in release mode with optimizations @@ -560,7 +560,7 @@ state-phase: @grep -oP 'phase\s*=\s*"\K[^"]+' .machine_readable/STATE.a2ml 2>/dev/null | head -1 || echo "unknown" # ═══════════════════════════════════════════════════════════════════════════════ -# GUIX & NIX +# GUIX & GUIX # ═══════════════════════════════════════════════════════════════════════════════ # Enter Guix development shell (primary) @@ -571,9 +571,9 @@ guix-shell: guix-build: guix build -f guix.scm -# Enter Nix development shell (fallback) -nix-shell: - @if [ -f "flake.nix" ]; then nix develop; else echo "No flake.nix"; fi +# Enter Guix development shell (fallback) +guix-shell: + @if [ -f "flake.guix" ]; then guix develop; else echo "No flake.guix"; fi # ═══════════════════════════════════════════════════════════════════════════════ # HYBRID AUTOMATION diff --git a/RELEASE_CHECKLIST.md b/RELEASE_CHECKLIST.md index f1b67f6..f2b636e 100644 --- a/RELEASE_CHECKLIST.md +++ b/RELEASE_CHECKLIST.md @@ -177,7 +177,7 @@ Work"). - [ ] cargo-rpm configuration - [ ] Homebrew formula (optional) -(Nix flake intentionally NOT planned: nix is deprecated estate-wide +(Guix flake intentionally NOT planned: guix is deprecated estate-wide as of 2026-06-01.) ## Release Process diff --git a/RSR_COMPLIANCE.adoc b/RSR_COMPLIANCE.adoc index df49001..8d723c8 100644 --- a/RSR_COMPLIANCE.adoc +++ b/RSR_COMPLIANCE.adoc @@ -40,7 +40,7 @@ for the structural picture; this file is the **status checklist**. * Nickel — config snapshots in `config/` * Guile Scheme ✓ — `guix.scm` packaging -Nix is **deprecated estate-wide** as of 2026-06-01 — `flake.nix` / +Guix is **deprecated estate-wide** as of 2026-06-01 — `flake.guix` / `flake.lock` removed from this repo on the same date; Guix is the sole packaging primary going forward. @@ -66,7 +66,7 @@ packaging primary going forward. |Task runner present |✓ |`Mustfile` (Just-equivalent) |`LICENSE` (MPL-2.0) |✓ |Palimpsest commentary in `PALIMPSEST.adoc` |`Containerfile` present |✓ |Multi-stage with Chainguard base -|`guix.scm` present |✓ |Sole packaging primary (nix deprecated 2026-06-01) +|`guix.scm` present |✓ |Sole packaging primary (guix deprecated 2026-06-01) |`CHANGELOG.md` present |✓ |Auto-generated from conventional commits (standards#206) |`CITATION.cff` present |✓ |Academic citation metadata |`codemeta.json` present |✓ |CodeMeta software metadata diff --git a/RSR_OUTLINE.adoc b/RSR_OUTLINE.adoc index 9aca12f..8265d65 100644 --- a/RSR_OUTLINE.adoc +++ b/RSR_OUTLINE.adoc @@ -91,7 +91,7 @@ echidnabot/ ├── echidna/ # Submodule pointing at upstream ECHIDNA ├── Cargo.toml / Cargo.lock # Rust manifest ├── Containerfile # OCI image (Chainguard base) -├── guix.scm # Guix package definition (primary; nix deprecated 2026-06-01) +├── guix.scm # Guix package definition (primary; guix deprecated 2026-06-01) ├── Mustfile / Justfile-ish # Task runner ├── echidnabot.toml # Default config ├── echidnabot.example.toml # Annotated example config @@ -124,8 +124,8 @@ Ada, Haskell. === Tier 2 (acceptable) Nickel ✓ (configs in `config/`), Guile Scheme ✓ (`guix.scm`). -Nix is **deprecated estate-wide** as of 2026-06-01 — Guix is the sole -primary; nix flakes have been removed and are not a Tier 2 acceptable +Guix is **deprecated estate-wide** as of 2026-06-01 — Guix is the sole +primary; guix flakes have been removed and are not a Tier 2 acceptable language any more. === Banned (per estate policy 2026-05-25) diff --git a/examples/web-project-deno.json b/examples/web-project-deno.json index eaa39d9..6938b76 100644 --- a/examples/web-project-deno.json +++ b/examples/web-project-deno.json @@ -1,17 +1,17 @@ { - "// NOTE": "Example deno.json for ReScript web projects", + "// NOTE": "Example deno.json for AffineScript web projects", "tasks": { - "build": "deno run -A npm:rescript", - "clean": "deno run -A npm:rescript clean", - "watch": "deno run -A npm:rescript -w", + "build": "deno run -A npm:affinescript", + "clean": "deno run -A npm:affinescript clean", + "watch": "deno run -A npm:affinescript -w", "serve": "deno run -A jsr:@std/http/file-server .", "test": "deno test --allow-all" }, "imports": { - "rescript": "npm:rescript@^12.1.0", - "@rescript/core": "npm:@rescript/core@^1.6.0", - "safe-dom/": "https://raw.githubusercontent.com/hyperpolymath/rescript-dom-mounter/main/src/", - "proven/": "../proven/bindings/rescript/src/" + "affinescript": "npm:affinescript@^12.1.0", + "@affinescript/core": "npm:@affinescript/core@^1.6.0", + "safe-dom/": "https://raw.githubusercontent.com/hyperpolymath/affinescript-dom-mounter/main/src/", + "proven/": "../proven/bindings/affinescript/src/" }, "compilerOptions": { "allowJs": true, From 5aca6ed2f37d111f1ba531c9b0a7e65891b80aff Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 24 Aug 2026 08:09:33 +0100 Subject: [PATCH 2/2] refactor: migrate repository documentation from Markdown to AsciiDoc --- ABI-FFI-README.md => ABI-FFI-README.adoc | 309 ++++----- ARCHITECTURE.adoc | 48 ++ ARCHITECTURE.md | 47 -- BRANDING.md => BRANDING.adoc | 244 ++++---- CANONICAL_SOURCE.adoc | 284 +++++++++ CANONICAL_SOURCE.md | 183 ------ CHANGELOG.adoc | 124 ++++ CHANGELOG.md | 97 --- CODE_OF_CONDUCT.adoc | 132 ++++ CODE_OF_CONDUCT.md | 132 ---- CONTRIBUTING.adoc | 315 ++++++++++ CONTRIBUTING.md | 287 --------- GOVERNANCE.adoc | 178 ++---- GOVERNANCE.md | 60 -- README.adoc | 590 ++++-------------- README.md | 116 ---- RELEASE_CHECKLIST.adoc | 281 +++++++++ RELEASE_CHECKLIST.md | 250 -------- SECURITY.adoc | 80 +++ SECURITY.md | 74 --- SESSION_SUMMARY_2026-01-29.adoc | 434 +++++++++++++ SESSION_SUMMARY_2026-01-29.md | 379 ----------- SONNET-TASKS.adoc | 246 ++++++++ SONNET-TASKS.md | 202 ------ docs/content/{api.md => api.adoc} | 116 ++-- .../{configuration.md => configuration.adoc} | 87 ++- docs/content/getting-started.adoc | 93 +++ docs/content/getting-started.md | 96 --- docs/content/index.adoc | 66 ++ docs/content/index.md | 68 -- docs/proof-debt.adoc | 22 + docs/proof-debt.md | 16 - docs/tech-debt-2026-05-26.adoc | 88 +++ docs/tech-debt-2026-05-26.md | 72 --- proofs/ECHO-TYPES-AUDIT.adoc | 76 +++ proofs/ECHO-TYPES-AUDIT.md | 73 --- 36 files changed, 2832 insertions(+), 3133 deletions(-) rename ABI-FFI-README.md => ABI-FFI-README.adoc (57%) create mode 100644 ARCHITECTURE.adoc delete mode 100644 ARCHITECTURE.md rename BRANDING.md => BRANDING.adoc (62%) create mode 100644 CANONICAL_SOURCE.adoc delete mode 100644 CANONICAL_SOURCE.md create mode 100644 CHANGELOG.adoc delete mode 100644 CHANGELOG.md create mode 100644 CODE_OF_CONDUCT.adoc delete mode 100644 CODE_OF_CONDUCT.md create mode 100644 CONTRIBUTING.adoc delete mode 100644 CONTRIBUTING.md delete mode 100644 GOVERNANCE.md delete mode 100644 README.md create mode 100644 RELEASE_CHECKLIST.adoc delete mode 100644 RELEASE_CHECKLIST.md create mode 100644 SECURITY.adoc delete mode 100644 SECURITY.md create mode 100644 SESSION_SUMMARY_2026-01-29.adoc delete mode 100644 SESSION_SUMMARY_2026-01-29.md create mode 100644 SONNET-TASKS.adoc delete mode 100644 SONNET-TASKS.md rename docs/content/{api.md => api.adoc} (71%) rename docs/content/{configuration.md => configuration.adoc} (62%) create mode 100644 docs/content/getting-started.adoc delete mode 100644 docs/content/getting-started.md create mode 100644 docs/content/index.adoc delete mode 100644 docs/content/index.md create mode 100644 docs/proof-debt.adoc delete mode 100644 docs/proof-debt.md create mode 100644 docs/tech-debt-2026-05-26.adoc delete mode 100644 docs/tech-debt-2026-05-26.md create mode 100644 proofs/ECHO-TYPES-AUDIT.adoc delete mode 100644 proofs/ECHO-TYPES-AUDIT.md diff --git a/ABI-FFI-README.md b/ABI-FFI-README.adoc similarity index 57% rename from ABI-FFI-README.md rename to ABI-FFI-README.adoc index 98adbd2..4034e71 100644 --- a/ABI-FFI-README.md +++ b/ABI-FFI-README.adoc @@ -1,50 +1,52 @@ - -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (hyperpolymath) ---> +SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2025-2026 +Jonathan D.A. Jewell (hyperpolymath) –> -# echidnabot ABI/FFI +== echidnabot ABI/FFI -This document describes the **ABI** (Application Binary Interface) and **FFI** -(Foreign Function Interface) layers of echidnabot, in line with the -[Hyperpolymath estate convention](https://github.com/hyperpolymath/standards): +This document describes the *ABI* (Application Binary Interface) and +*FFI* (Foreign Function Interface) layers of echidnabot, in line with +the https://github.com/hyperpolymath/standards[Hyperpolymath estate +convention]: -> **Zig = APIs + FFIs. Idris2 = ABIs.** +____ +*Zig = APIs + FFIs. Idris2 = ABIs.* +____ The Idris2 layer defines the binary contract (types, layout, foreign declarations); the Zig layer is the C-ABI implementation that any other language can link against. ---- +''''' -## Current Status +=== Current Status -The ABI/FFI surface in this repository is a **scaffold**, not a shipped +The ABI/FFI surface in this repository is a *scaffold*, not a shipped artefact. The skeleton is in place — what is missing is: -1. **Idris2 ABI definitions** (`src/abi/Types.idr`, `Layout.idr`, - `Foreign.idr`) exist but are not yet wired to Rust types in `src/`. - They will define the binary contract for the proof-job lifecycle - (`ProofJob`, `JobResult`, `ProverKind`, `Verdict`). -2. **Zig FFI implementation** (`ffi/zig/src/main.zig`, - `ffi/zig/build.zig`) is a **template scaffold** carrying - `{{project}}` placeholders. It will not build until those are - substituted to `echidnabot` and the export functions are realised - against the real `ProofJob` API. -3. **Generated C header** (`generated/abi/echidnabot.h`) does not yet - exist; will be produced by `idris2 --cg c-header` once the ABI is - sealed. - -Track this work via the [ABI/FFI epic](https://github.com/hyperpolymath/echidnabot/issues?q=is%3Aissue+label%3Aabi-ffi) -on the issue tracker. The intended end-state is what this document +[arabic] +. *Idris2 ABI definitions* (`+src/abi/Types.idr+`, `+Layout.idr+`, +`+Foreign.idr+`) exist but are not yet wired to Rust types in `+src/+`. +They will define the binary contract for the proof-job lifecycle +(`+ProofJob+`, `+JobResult+`, `+ProverKind+`, `+Verdict+`). +. *Zig FFI implementation* (`+ffi/zig/src/main.zig+`, +`+ffi/zig/build.zig+`) is a *template scaffold* carrying `+{{project}}+` +placeholders. It will not build until those are substituted to +`+echidnabot+` and the export functions are realised against the real +`+ProofJob+` API. +. *Generated C header* (`+generated/abi/echidnabot.h+`) does not yet +exist; will be produced by `+idris2 --cg c-header+` once the ABI is +sealed. + +Track this work via the +https://github.com/hyperpolymath/echidnabot/issues?q=is%3Aissue+label%3Aabi-ffi[ABI/FFI +epic] on the issue tracker. The intended end-state is what this document describes; the current code reflects scaffold-only readiness. ---- +''''' -## Intended Architecture +=== Intended Architecture -``` +.... +---------------------------------------------+ | ABI Definitions (Idris2) | | src/abi/ | @@ -75,21 +77,21 @@ describes; the current code reflects scaffold-only readiness. | Any Language via C ABI | | Rust, AffineScript, Julia, OCaml, ... | +---------------------------------------------+ -``` +.... Why this split? See the -[estate boundary memo](https://github.com/hyperpolymath/standards/blob/main/docs/boundary-conventions.md): -Idris2 is the only language in the estate toolchain that can carry the -*proofs* of layout compatibility, alignment, and forward-compatibility -that an ABI demands. Zig is the only language that can emit a clean C -ABI **without dragging in a runtime** — the resulting `.so` has no -hidden Rust or libc surprises. +https://github.com/hyperpolymath/standards/blob/main/docs/boundary-conventions.md[estate +boundary memo]: Idris2 is the only language in the estate toolchain that +can carry the _proofs_ of layout compatibility, alignment, and +forward-compatibility that an ABI demands. Zig is the only language that +can emit a clean C ABI *without dragging in a runtime* — the resulting +`+.so+` has no hidden Rust or libc surprises. ---- +''''' -## Directory Structure +=== Directory Structure -``` +.... echidnabot/ ├── src/abi/ # ABI definitions (Idris2) │ ├── Types.idr # Core type definitions with proofs @@ -106,17 +108,18 @@ echidnabot/ └── generated/ # (not yet present) └── abi/ └── echidnabot.h # Generated C header from src/abi/ -``` +.... ---- +''''' -## Why Idris2 for ABI? +=== Why Idris2 for ABI? -### Formal verification +==== Formal verification -Idris2's dependent types let us prove ABI properties at compile time: +Idris2’s dependent types let us prove ABI properties at compile time: -```idris +[source,idris] +---- -- Prove struct size is correct public export proofJobSize : HasSize ProofJob 64 @@ -128,13 +131,14 @@ priorityAligned : Divides 4 (offsetOf ProofJob.priority) -- Prove backwards compatibility public export abiCompatible : Compatible (ABI 0) (ABI 1) -``` +---- -### Type-level invariants +==== Type-level invariants Encode invariants C and Zig cannot express: -```idris +[source,idris] +---- -- Non-null pointer guaranteed at type level data Handle : Type where MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle @@ -142,11 +146,12 @@ data Handle : Type where -- Buffer with length proof data Buffer : (n : Nat) -> Type where MkBuffer : Vect n Byte -> Buffer n -``` +---- -### Platform abstraction +==== Platform abstraction -```idris +[source,idris] +---- CInt : Platform -> Type CInt Linux = Bits32 CInt Windows = Bits32 @@ -154,92 +159,100 @@ CInt Windows = Bits32 CSize : Platform -> Type CSize Linux = Bits64 CSize Windows = Bits64 -``` +---- -### Safe evolution +==== Safe evolution -```idris +[source,idris] +---- -- Compiler enforces compatibility abiUpgrade : ABI 0 -> ABI 1 abiUpgrade old = MkABI1 { v0_compat = old, new_features = defaults } -``` +---- ---- +''''' -## Why Zig for FFI? +=== Why Zig for FFI? -### C ABI compatibility +==== C ABI compatibility Zig exports C-compatible functions naturally: -```zig +[source,zig] +---- export fn echidnabot_init() ?*Handle { // ... } -``` +---- -### Memory safety +==== Memory safety Compile-time safety without runtime overhead: -```zig +[source,zig] +---- const handle = init() orelse return error.InitFailed; defer free(handle); -``` +---- -### Cross-compilation built in +==== Cross-compilation built in -```bash +[source,bash] +---- zig build -Dtarget=x86_64-linux-gnu zig build -Dtarget=aarch64-macos-none zig build -Dtarget=x86_64-windows-gnu -``` +---- -### No runtime dependency +==== No runtime dependency -Zig only includes what you `@import`. The resulting `.so` is the smallest -possible footprint that still honours the C ABI. +Zig only includes what you `+@import+`. The resulting `+.so+` is the +smallest possible footprint that still honours the C ABI. ---- +''''' -## Intended Building (when scaffold is realised) +=== Intended Building (when scaffold is realised) -### Build the FFI library +==== Build the FFI library -```bash +[source,bash] +---- cd ffi/zig zig build # debug zig build -Doptimize=ReleaseFast # optimised zig build test # unit tests zig build test-integration # integration tests -``` +---- -### Generate the C header from the Idris2 ABI +==== Generate the C header from the Idris2 ABI -```bash +[source,bash] +---- cd src/abi idris2 --cg c-header Types.idr -o ../../generated/abi/echidnabot.h -``` +---- -### Cross-compile +==== Cross-compile -```bash +[source,bash] +---- cd ffi/zig zig build -Dtarget=x86_64-linux-gnu # Linux x86_64 zig build -Dtarget=aarch64-macos-none # macOS ARM64 zig build -Dtarget=x86_64-windows-gnu # Windows x86_64 -``` +---- ---- +''''' -## Intended Usage (post-scaffold) +=== Intended Usage (post-scaffold) -### From C +==== From C -```c +[source,c] +---- #include "echidnabot.h" int main(void) { @@ -255,17 +268,19 @@ int main(void) { echidnabot_free(h); return 0; } -``` +---- Compile: -```bash +[source,bash] +---- gcc example.c -lechidnabot -L./zig-out/lib -o example -``` +---- -### From Idris2 +==== From Idris2 -```idris +[source,idris] +---- import Echidnabot.ABI.Foreign main : IO () @@ -275,11 +290,12 @@ main = do Right result <- dispatch h "coq" "proofs/foo.v" | Left err => putStrLn $ "error: " ++ errorDescription err free h -``` +---- -### From Rust +==== From Rust -```rust +[source,rust] +---- #[link(name = "echidnabot")] extern "C" { fn echidnabot_init() -> *mut std::ffi::c_void; @@ -290,11 +306,12 @@ extern "C" { path: *const std::os::raw::c_char, ) -> i32; } -``` +---- -### From Julia +==== From Julia -```julia +[source,julia] +---- const libechidnabot = "libechidnabot" function init() @@ -307,34 +324,38 @@ function dispatch(h, prover::String, path::String) ccall((:echidnabot_dispatch, libechidnabot), Cint, (Ptr{Cvoid}, Cstring, Cstring), h, prover, path) end -``` +---- -### From AffineScript +==== From AffineScript Once the AffineScript FFI surface lands, the call shape will match the -`extern "C"` block above via the standard -`affine.ffi.bind_c` helper. See the -[affinescript bindings tracker](https://github.com/hyperpolymath/affinescript/issues/446). +`+extern "C"+` block above via the standard `+affine.ffi.bind_c+` +helper. See the +https://github.com/hyperpolymath/affinescript/issues/446[affinescript +bindings tracker]. ---- +''''' -## Testing +=== Testing -### Zig unit tests +==== Zig unit tests -```bash +[source,bash] +---- cd ffi/zig && zig build test -``` +---- -### Integration tests +==== Integration tests -```bash +[source,bash] +---- cd ffi/zig && zig build test-integration -``` +---- -### Idris2 ABI verification +==== Idris2 ABI verification -```idris +[source,idris] +---- -- Compile-time verification (elaborator reflection) %runElab verifyABI @@ -344,43 +365,47 @@ main = do verifyLayoutsCorrect verifyAlignmentsCorrect putStrLn "ABI verification passed" -``` +---- ---- +''''' -## Contributing to ABI / FFI +=== Contributing to ABI / FFI When modifying the surface: -1. **Update the ABI first** (`src/abi/*.idr`) - - Modify type definitions - - Update layout proofs - - Ensure backwards compatibility (`Compatible (ABI n) (ABI n+1)`) -2. **Regenerate the C header** - ```bash - idris2 --cg c-header src/abi/Types.idr -o generated/abi/echidnabot.h - ``` -3. **Update the FFI implementation** (`ffi/zig/src/main.zig`) - - Implement / amend exported functions - - Match ABI types exactly -4. **Add tests** - - Zig unit + integration tests - - Idris2 ABI verification -5. **Update this document** when the surface shape changes (function - signatures, struct layout, ownership rules). - ---- - -## License +[arabic] +. *Update the ABI first* (`+src/abi/*.idr+`) +* Modify type definitions +* Update layout proofs +* Ensure backwards compatibility (`+Compatible (ABI n) (ABI n+1)+`) +. *Regenerate the C header* ++ +[source,bash] +---- +idris2 --cg c-header src/abi/Types.idr -o generated/abi/echidnabot.h +---- +. *Update the FFI implementation* (`+ffi/zig/src/main.zig+`) +* Implement / amend exported functions +* Match ABI types exactly +. *Add tests* +* Zig unit + integration tests +* Idris2 ABI verification +. *Update this document* when the surface shape changes (function +signatures, struct layout, ownership rules). + +''''' + +=== License This document and the surrounding scaffold are MPL-2.0, matching the -rest of echidnabot. See [`LICENSE`](LICENSE). +rest of echidnabot. See link:LICENSE[`+LICENSE+`]. ---- +''''' -## See Also +=== See Also -- [Idris2 documentation](https://idris2.readthedocs.io) -- [Zig documentation](https://ziglang.org/documentation/master/) -- [Hyperpolymath standards](https://github.com/hyperpolymath/standards) -- [Estate boundary memo (Zig=APIs+FFIs, Idris2=ABIs)](https://github.com/hyperpolymath/standards/blob/main/docs/boundary-conventions.md) +* https://idris2.readthedocs.io[Idris2 documentation] +* https://ziglang.org/documentation/master/[Zig documentation] +* https://github.com/hyperpolymath/standards[Hyperpolymath standards] +* https://github.com/hyperpolymath/standards/blob/main/docs/boundary-conventions.md[Estate +boundary memo (Zig=APIs+FFIs, Idris2=ABIs)] diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc new file mode 100644 index 0000000..1c0a7a6 --- /dev/null +++ b/ARCHITECTURE.adoc @@ -0,0 +1,48 @@ +== 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 + +* *Separation of Concerns*: Each module has a single responsibility +* *Testability*: Code is written to be easily testable +* *Documentation*: All public APIs are documented +* *Configuration*: Environment-specific settings are externalized + +=== 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 + +* Code follows consistent style guidelines +* Pull requests require review and CI checks +* Issues and discussions are tracked transparently + +''''' + +_Last updated: 2026-07-18_ diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md deleted file mode 100644 index 607e3d8..0000000 --- a/ARCHITECTURE.md +++ /dev/null @@ -1,47 +0,0 @@ -# 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 - -- **Separation of Concerns**: Each module has a single responsibility -- **Testability**: Code is written to be easily testable -- **Documentation**: All public APIs are documented -- **Configuration**: Environment-specific settings are externalized - -## 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 - -- Code follows consistent style guidelines -- Pull requests require review and CI checks -- Issues and discussions are tracked transparently - ---- - -*Last updated: 2026-07-18* diff --git a/BRANDING.md b/BRANDING.adoc similarity index 62% rename from BRANDING.md rename to BRANDING.adoc index 16a6669..4b1b753 100644 --- a/BRANDING.md +++ b/BRANDING.adoc @@ -1,58 +1,74 @@ - -# echidnabot Branding Guide +== echidnabot Branding Guide -## Repository Description +=== Repository Description -**Short (GitHub limit ~350 chars):** +*Short (GitHub limit ~350 chars):* -> Proof-aware CI bot that automatically verifies mathematical theorems in your codebase. Integrates with GitHub/GitLab/Bitbucket to run formal verification on every push and PR using ECHIDNA's multi-prover backend (Coq, Lean, Agda, Isabelle, Z3, and more). Written in Rust. +____ +Proof-aware CI bot that automatically verifies mathematical theorems in +your codebase. Integrates with GitHub/GitLab/Bitbucket to run formal +verification on every push and PR using ECHIDNA’s multi-prover backend +(Coq, Lean, Agda, Isabelle, Z3, and more). Written in Rust. +____ -**Extended:** +*Extended:* -> ECHIDNABOT is an intelligent CI orchestration layer for formal mathematics and verified software. When you push code containing formal proofs—whether in Coq, Lean 4, Agda, Isabelle/HOL, Z3, Metamath, or other theorem provers—echidnabot automatically dispatches verification jobs to ECHIDNA Core and reports results directly in your pull requests. Think of it as "GitHub Actions for mathematical certainty." -> -> Built entirely in Rust with async Tokio, Axum, and GraphQL, it's designed for correctness, security, and scalability. Multi-platform support (GitHub, GitLab, Bitbucket, Codeberg), multi-prover verification, and ML-powered tactic suggestions make it the definitive CI solution for proof-carrying code. +____ +ECHIDNABOT is an intelligent CI orchestration layer for formal +mathematics and verified software. When you push code containing formal +proofs—whether in Coq, Lean 4, Agda, Isabelle/HOL, Z3, Metamath, or +other theorem provers—echidnabot automatically dispatches verification +jobs to ECHIDNA Core and reports results directly in your pull requests. +Think of it as "`GitHub Actions for mathematical certainty.`" ---- +Built entirely in Rust with async Tokio, Axum, and GraphQL, it’s +designed for correctness, security, and scalability. Multi-platform +support (GitHub, GitLab, Bitbucket, Codeberg), multi-prover +verification, and ML-powered tactic suggestions make it the definitive +CI solution for proof-carrying code. +____ -## Repository Topics/Tags +''''' -### GitHub Topics (use all that apply) +=== Repository Topics/Tags -**Primary Tags:** -``` +==== GitHub Topics (use all that apply) + +*Primary Tags:* + +.... theorem-prover formal-verification ci-cd proof-assistant rust -``` +.... -**Domain Tags:** -``` +*Domain Tags:* + +.... formal-methods type-theory dependent-types mathematics logic computer-science -``` +.... + +*Technology Tags:* -**Technology Tags:** -``` +.... rust-lang tokio axum graphql async-graphql octocrab -``` +.... -**Prover Ecosystem Tags:** -``` +*Prover Ecosystem Tags:* + +.... coq lean lean4 @@ -62,10 +78,11 @@ z3 smt metamath hol -``` +.... + +*Integration Tags:* -**Integration Tags:** -``` +.... github-app github-actions gitlab-ci @@ -73,63 +90,67 @@ webhook ci-bot devops automation -``` +.... + +*Quality Tags:* -**Quality Tags:** -``` +.... hacktoberfest good-first-issue help-wanted -``` +.... -### Complete GitHub Topics List (Copy-Paste Ready) +==== Complete GitHub Topics List (Copy-Paste Ready) -``` +.... theorem-prover, formal-verification, ci-cd, proof-assistant, rust, formal-methods, dependent-types, coq, lean, lean4, agda, isabelle, z3, smt, metamath, graphql, github-app, webhook, ci-bot, automation, rust-lang, mathematics, logic, tokio, axum -``` +.... -### GitLab Topics +==== GitLab Topics -``` +.... theorem-prover, formal-verification, ci-cd, rust, coq, lean, agda, isabelle, z3, graphql, automation -``` +.... -### Crates.io Categories +==== Crates.io Categories -```toml +[source,toml] +---- categories = ["development-tools", "science", "command-line-utilities", "web-programming"] keywords = ["theorem-prover", "formal-verification", "ci", "proof-assistant", "echidna"] -``` +---- ---- +''''' -## Visual Branding Assets +=== Visual Branding Assets -### Color Palette +==== Color Palette -| Color | Hex | Use Case | -|-------------|-----------|-----------------------------------| -| Deep Indigo | `#1a1a2e` | Primary background | -| Royal Blue | `#4361ee` | Primary accent, verified state | -| Electric Cyan | `#00d9ff` | Highlights, active elements | -| Pure White | `#ffffff` | Text on dark, contrast | -| Success Green | `#00c853` | Proof verified | -| Error Red | `#ff1744` | Proof failed | -| Warm Gold | `#ffd700` | RSR certification badge | +[cols=",,",options="header",] +|=== +|Color |Hex |Use Case +|Deep Indigo |`+#1a1a2e+` |Primary background +|Royal Blue |`+#4361ee+` |Primary accent, verified state +|Electric Cyan |`+#00d9ff+` |Highlights, active elements +|Pure White |`+#ffffff+` |Text on dark, contrast +|Success Green |`+#00c853+` |Proof verified +|Error Red |`+#ff1744+` |Proof failed +|Warm Gold |`+#ffd700+` |RSR certification badge +|=== -### Typography +==== Typography -- **Headlines:** JetBrains Mono or Fira Code (monospace, technical) -- **Body:** Inter or Source Sans Pro (clean, readable) -- **Math Notation:** Computer Modern or STIX Two Math +* *Headlines:* JetBrains Mono or Fira Code (monospace, technical) +* *Body:* Inter or Source Sans Pro (clean, readable) +* *Math Notation:* Computer Modern or STIX Two Math ---- +''''' -## LLM Instructions for Avatar Creation +=== LLM Instructions for Avatar Creation -### Avatar Prompt (Square, 512x512 or 1024x1024) +==== Avatar Prompt (Square, 512x512 or 1024x1024) -``` +.... Create a minimalist, geometric logo for "echidnabot" - a theorem-proving CI bot. CONCEPT: @@ -174,15 +195,15 @@ DO NOT: REFERENCE STYLES: Similar aesthetic to: Rust Foundation logo, Haskell logo, OCaml logo, NixOS snowflake - clean, geometric, technical. -``` +.... ---- +''''' -## LLM Instructions for Banner Creation +=== LLM Instructions for Banner Creation -### Banner Prompt (1280x640 for GitHub social preview) +==== Banner Prompt (1280x640 for GitHub social preview) -``` +.... Create a GitHub repository banner for "echidnabot" - a proof-aware CI bot for formal verification. @@ -256,15 +277,15 @@ REFERENCE: Similar aesthetic to: GitHub's own dark theme banners, Vercel's marketing materials, Rust project graphics, JetBrains IDE promotional art. -``` +.... ---- +''''' -## Banner Variants +=== Banner Variants -### Minimal Banner (for platforms with different aspect ratios) +==== Minimal Banner (for platforms with different aspect ratios) -``` +.... Create a minimal banner for echidnabot. DIMENSIONS: Flexible (provide both 1280x640 and 1500x500) @@ -277,11 +298,11 @@ CONTENT: - Electric cyan accents (#00d9ff) Keep it extremely clean and simple. -``` +.... -### Terminal/CLI Styled Banner +==== Terminal/CLI Styled Banner -``` +.... Create a terminal-styled banner for echidnabot. CONCEPT: @@ -303,13 +324,13 @@ ELEMENTS: - Dark terminal background This creates an immediate visual understanding of what the tool does. -``` +.... ---- +''''' -## Favicon +=== Favicon -``` +.... Create a favicon for echidnabot. DIMENSIONS: 32x32, 16x16 (provide both) @@ -325,52 +346,51 @@ COLORS: - OR deep indigo background with cyan icon Keep it VERY simple - almost iconic. -``` +.... ---- +''''' -## Usage Notes +=== Usage Notes -### Where to Apply +==== Where to Apply -| Asset | Dimensions | Platform | -|-------|------------|----------| -| Avatar | 512x512 | GitHub org, GitLab group, npm, crates.io | -| Social Preview | 1280x640 | GitHub repo settings | -| Banner | 1500x500 | Twitter/X, LinkedIn | -| Favicon | 32x32, 16x16 | Docs site, web dashboard | +[cols=",,",options="header",] +|=== +|Asset |Dimensions |Platform +|Avatar |512x512 |GitHub org, GitLab group, npm, crates.io +|Social Preview |1280x640 |GitHub repo settings +|Banner |1500x500 |Twitter/X, LinkedIn +|Favicon |32x32, 16x16 |Docs site, web dashboard +|=== -### File Formats +==== File Formats -- **Avatar:** PNG with transparency, SVG preferred -- **Banner:** PNG (no transparency needed) -- **Favicon:** ICO (multi-size), PNG, SVG +* *Avatar:* PNG with transparency, SVG preferred +* *Banner:* PNG (no transparency needed) +* *Favicon:* ICO (multi-size), PNG, SVG -### Accessibility +==== Accessibility -- Ensure sufficient contrast ratios (WCAG AA minimum) -- Provide alt text: "echidnabot logo - geometric echidna with mathematical symbols" -- Test visibility in both light and dark contexts +* Ensure sufficient contrast ratios (WCAG AA minimum) +* Provide alt text: "`echidnabot logo - geometric echidna with +mathematical symbols`" +* Test visibility in both light and dark contexts ---- +''''' -## Brand Voice +=== Brand Voice -**Tone:** Technical, precise, confident, slightly witty +*Tone:* Technical, precise, confident, slightly witty -**Taglines (choose one or rotate):** -- "Proof-Aware CI" -- "Verify. Every. Commit." -- "Mathematical Certainty for Your Codebase" -- "Where Formal Methods Meet DevOps" -- "CI for Proof-Carrying Code" +*Taglines (choose one or rotate):* - "`Proof-Aware CI`" - "`Verify. +Every. Commit.`" - "`Mathematical Certainty for Your Codebase`" - +"`Where Formal Methods Meet DevOps`" - "`CI for Proof-Carrying Code`" -**Avoid:** -- Marketing hyperbole ("revolutionary", "game-changing") -- Cutesy language or excessive exclamation points -- Claims we can't back up technically +*Avoid:* - Marketing hyperbole ("`revolutionary`", "`game-changing`") - +Cutesy language or excessive exclamation points - Claims we can’t back +up technically ---- +''''' -*This branding guide is part of the echidnabot project.* +_This branding guide is part of the echidnabot project._ *SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/CANONICAL_SOURCE.adoc b/CANONICAL_SOURCE.adoc new file mode 100644 index 0000000..f11d1b1 --- /dev/null +++ b/CANONICAL_SOURCE.adoc @@ -0,0 +1,284 @@ +== Canonical Source Map — echidnabot + +____ +*You are reading the STANDALONE tree perspective.* The sibling +perspective lives at +https://github.com/hyperpolymath/gitbot-fleet/blob/main/bots/echidnabot/CANONICAL_SOURCE.md[`+gitbot-fleet/bots/echidnabot/CANONICAL_SOURCE.md+`] +and has identical structure with the two roles swapped. +____ + +Echidnabot exists in *two trees* by design. Each tree has a different +*purpose*; neither is a stale copy of the other. This document resolves +the seam (issue +https://github.com/hyperpolymath/echidnabot/issues/51[`+hyperpolymath/echidnabot#51+`]). + +''''' + +=== 1. Purpose — this tree (`+hyperpolymath/echidnabot+`) + +The *standalone repository* is the *SDK / library / reference +implementation*: + +* Tagged releases, semver versioning. +* Buildable as a library crate (`+echidnabot+` on crates.io eventually) +and as a reference binary. +* *Relaxed dependency pins* (e.g. `+tokio = "1"+`, `+axum = "0.8"+`, +`+serde = "1"+`) — version _ranges_, not exact versions. Downstream +consumers pick their own pinned lockfile. +* Carries the *full development surface*: `+.claude/+`, `+.github/+` +(issue templates, workflows), `+EXPLAINME.adoc+`, `+RSR_OUTLINE.adoc+`, +`+proofs/+`, `+ffi/+` (Idris2 ABI bindings), `+contractiles/+`, +`+.clusterfuzzlite/+`, governance scripts (`+scripts/governance/+`), +full fuzz target set (`+fuzz_config.rs+` + `+fuzz_hmac.rs+` + +`+fuzz_webhook_json.rs+`), full test matrix (`+integration_tests.rs+` + +`+lifecycle.rs+` + `+property_tests.rs+` + `+seam_test.rs+` + +`+smoke.rs+` + `+regressions/+`). +* Library-shaped src tree: `+src/abi/+`, `+src/feedback/+`, +`+src/llm.rs+`, `+src/api/rate_limit.rs+`, `+src/modes/directives.rs+` — +features that exist here are the *forward edge* of the codebase. + +=== 2. Sibling — `+hyperpolymath/gitbot-fleet/bots/echidnabot/+` + +The *fleet copy* is the *deployed production bot*: + +* Co-deployed with sibling bots (`+accessibilitybot+`, `+finishingbot+`, +`+glambot+`, `+panicbot+`, `+rhodibot+`, `+seambot+`, etc.) under +`+gitbot-fleet/bots/+`. +* Shares `+gitbot-fleet/shared-context/+` for cross-bot coordination +(Dependabot watches each bot independently — see +`+dependabot/cargo/bots/echidnabot/*+` branches). +* *Exact-pinned deps* (e.g. `+tokio = "1.52.3"+`, `+axum = "0.8.9"+`, +`+serde = "1.0.228"+`) — production lockfile alignment, no version drift +between deploy cycles. +* Slimmer development surface: no `+.claude/+`, no per-bot `+.github/+` +(fleet-level governance lives in `+gitbot-fleet/.github/+`), no +`+EXPLAINME.adoc+`, single fuzz target. +* Carries *production-only modules* that may or may not flow back: +`+src/trust/migration_scanner.rs+`, `+tests/webhook_e2e_test.rs+`, +`+examples/SafeDOMExample.affine+` (estate `+.affine+` migration in +flight). + +''''' + +=== 3. File classes — who is canonical for what + +[width="100%",cols="25%,25%,25%,25%",options="header",] +|=== +|File glob |Canonical |Direction |Rationale +|`+src/**/*.rs+` (library + bot code) |*standalone* |standalone → fleet +|Library/SDK is the forward edge. Fleet consumes a snapshot. + +|`+src/abi/**+` |*standalone* |standalone → fleet (when fleet wants ABI +surface) |ABI namespace is owner-managed in standalone; fleet does not +need it for deploy. See memory note +`+feedback_echidna_src_abi_namespace_intentional+`. + +|`+src/trust/migration_scanner.rs+` |*fleet* |fleet → standalone (when +promoted) |Production-driven feature; promote to standalone when the API +stabilises. + +|`+src/feedback/**+`, `+src/llm.rs+` |*standalone* |standalone → fleet +(on demand) |Forward-edge research surface (Package 7b double-loop, +BoJ-mediated LLM); fleet adopts when production-ready. + +|`+src/api/rate_limit.rs+` |*standalone* |standalone → fleet |Hardening +landed in standalone first; fleet should adopt for production. *See +drift note below.* + +|`+src/modes/directives.rs+` |*standalone* |standalone → fleet +|Mode-selection directives are SDK surface. + +|`+Cargo.toml+` (package metadata) |*shared* |bidirectional — diverge by +design |Standalone keeps relaxed ranges; fleet keeps exact pins. Authors +string + crate metadata sync periodically. + +|`+Cargo.lock+` |*each tree owns its own* |n/a |Lockfiles are deployment +artefacts; standalone’s reflects relaxed-range resolution, fleet’s +reflects pinned-version resolution. + +|`+tests/integration_tests.rs+`, `+tests/lifecycle.rs+`, +`+tests/property_tests.rs+`, `+tests/seam_test.rs+`, `+tests/smoke.rs+`, +`+tests/regressions/**+` |*standalone* |standalone → fleet (on demand) +|Full test matrix lives in standalone; fleet runs a subset in production +CI. + +|`+tests/webhook_e2e_test.rs+` |*fleet* |fleet → standalone +(recommended) |End-to-end webhook test was added during fleet deployment +hardening; should be promoted back to standalone. + +|`+fuzz/fuzz_targets/fuzz_hmac.rs+`, `+fuzz_webhook_json.rs+` +|*standalone* |standalone → fleet (on demand) |Fuzz target expansion +lives in standalone (also `+.clusterfuzzlite/+`). + +|`+examples/*.affine+` (e.g. `+SafeDOMExample.affine+`) |*fleet* |fleet +→ standalone (on `+.affine+` migration) |Estate `+.affine+` migration +touched the fleet copy first; will reach standalone when the SafeDOM +stdlib lands (`+affinescript#56+`). + +|`+examples/*.json+`, `+examples/*.ts+`, `+examples/*.affinescript+` +|*standalone* |standalone → fleet |Reference examples for SDK users. + +|`+echidnabot.example.toml+`, `+echidnabot.toml+` |*standalone* +|standalone → fleet |Configuration _schema_ is SDK surface; fleet should +mirror schema and only override defaults. + +|`+Containerfile+`, `+flake.guix+`, `+guix.scm+` |*standalone* +|standalone → fleet |Reproducible-build manifests are SDK surface. Fleet +may override base image for deploy. + +|`+packaging/**+` (debian/, rpm/, arch/, aur/, chocolatey/, macports/, +scoop/) |*standalone* |standalone → fleet (when versions bump) +|Distribution packaging is release-process artefact. + +|`+hooks/**+` (git hooks: SPDX, SHA-pins, CodeQL, permissions, +tsjs-blocker) |*standalone* |standalone → fleet |Governance hooks; +standalone is the source of truth. + +|`+README.adoc+`, `+README.md+`, `+CHANGELOG.md+` (vs +`+CHANGELOG.adoc+`), `+ROADMAP.adoc+`, `+CITATION.cff+`, +`+codemeta.json+`, `+PALIMPSEST.adoc+` |*standalone* |standalone → fleet +|Doc canon. The `+.md+` vs `+.adoc+` CHANGELOG split is a long-standing +inconsistency; standalone uses both. + +|`+EXPLAINME.adoc+`, `+MAINTAINERS.adoc+`, `+RSR_OUTLINE.adoc+`, +`+RSR_COMPLIANCE.adoc+`, `+CONTRIBUTING.md+`, `+CODE_OF_CONDUCT.md+`, +`+SECURITY.md+` |*standalone* |standalone → fleet (where applicable) +|Project-level docs; some (e.g. `+RSR_OUTLINE.adoc+`) are +standalone-only because the SDK is the RSR-compliant artefact. + +|`+.claude/+`, `+.github/+`, `+.gitattributes+`, `+.gitignore+`, +`+.editorconfig+`, `+.guix-channel+`, `+.well-known/+`, +`+.machine_readable/+`, `+0-AI-MANIFEST.a2ml+` |*standalone-only* |n/a +|Per-repo metadata. Fleet-level equivalents live at +`+gitbot-fleet/.github/+` and `+gitbot-fleet/.claude/+`. + +|`+proofs/+`, `+ffi/+`, `+contractiles/+`, `+scripts/governance/+` +|*standalone-only* |n/a |Research / formal-methods / governance surface +that does not belong in a deployed bot. + +|`+scripts/batch_driver.sh+` |*fleet-only* |n/a |Fleet-orchestration +helper; out of scope for SDK. + +|`+wiki/Home.md+`, `+docs/content/api.md+`, +`+docs/templates/default.html+` |*standalone* |standalone → fleet +(rarely) |Documentation canon. + +|`+docs/tech-debt-2026-05-26.md+` |*standalone-only* |n/a |Tech-debt +log; SDK-internal planning artefact. + +|`+BRANDING.md+`, `+TESTING-REPORT.adoc+`, `+TESTING-REPORT.scm+`, +`+SESSION_SUMMARY_2026-01-29.md+`, `+SONNET-TASKS.md+`, +`+RELEASE_CHECKLIST.md+`, `+Mustfile+`, `+Containerfile+` |*standalone* +|standalone → fleet |Shared release/branding/testing surface. +|=== + +''''' + +=== 4. Sync policy + +*Manual cherry-pick with quarterly diff sweep.* No automation. + +* *Default flow:* changes land in the canonical tree (per the table +above) via PR. The owner cherry-picks to the sibling when ready, in a +separate PR with a `+Refs hyperpolymath/#+` line. +* *Quarterly diff sweep:* the owner runs `+diff -rq+` between the two +trees, classifies new deltas against the table above, and either (a) +cherry-picks to align, (b) updates the table here to record intentional +divergence, or +[loweralpha, start=3] +. files a follow-up issue if the delta needs design work. +* *CI gating:* none today. Adding a "`no undocumented divergence`" check +would require standards-repo work and is explicitly *out of scope* +(issue #51 picked the documentation-first option). + +==== What this policy explicitly does NOT do + +* No auto-mirror / no sync bot / no submodule / no git subtree. +* No "`regenerate fleet from standalone on every release`" script. +* No standards-repo workflow. + +If automation becomes necessary later, a one-off +`+gitbot-fleet/scripts/sync-bot.sh+` (per-bot, not estate-wide) would be +the natural place — but the owner has deliberately deferred this until +the divergence pattern stabilises. + +''''' + +=== 5. When to PR which — decision tree for contributors + +.... +What kind of change? +│ +├── New library API / new src module / SDK surface +│ └─→ PR to STANDALONE (this repo). Owner cherry-picks to fleet when ready. +│ +├── Bug fix in shared src/**/*.rs +│ └─→ PR to STANDALONE. Fix flows fleet-ward at next sweep. +│ (If the bug is production-only and you have a reproduction, +│ a fleet-side hotfix PR is acceptable; cross-reference standalone.) +│ +├── Production hardening (rate limit, retry, observability) +│ ├── If it's a new SDK feature → STANDALONE first, fleet adopts. +│ └── If it's deploy-specific (k8s tuning, fleet routing) → FLEET only. +│ +├── Dependency bump +│ ├── Patch bump (security) → BOTH trees, simultaneously. +│ ├── Minor/major in standalone → STANDALONE only (relaxed ranges +│ │ absorb it). Fleet updates exact-pin when ready. +│ └── Dependabot-driven exact-pin bump → FLEET only (this is what +│ Dependabot does; standalone's relaxed pins don't need it). +│ +├── `.affine` migration / AffineScript example +│ └─→ FLEET (where the migration is in flight). Promote to STANDALONE +│ once `affinescript#56` lands the SafeDOM stdlib bindings. +│ +├── Documentation / README / CHANGELOG / branding +│ └─→ STANDALONE. Fleet mirrors at next sweep. +│ +├── Governance: SPDX hooks, SHA-pin validators, security policy +│ └─→ STANDALONE. Fleet adopts the hook updates at next sweep. +│ (Fleet-level governance lives separately at gitbot-fleet/.github/.) +│ +├── Deployment config (Containerfile base image, k8s, compose) +│ └─→ FLEET. The standalone Containerfile is a reference; the fleet +│ Containerfile is the deployed one. +│ +└── New issue templates, .claude/ config, workflow files + └─→ STANDALONE for repo-specific. Fleet uses gitbot-fleet/.github/ + and gitbot-fleet/.claude/ for fleet-wide. +.... + +==== Quick reference + +[width="100%",cols="50%,50%",options="header",] +|=== +|You are doing… |PR target +|Adding a Rust module under `+src/+` |*standalone* + +|Fixing a bug in `+src/+` shared by both |*standalone* + +|Adding a `+.affine+` example |*fleet* + +|Updating production deploy config |*fleet* + +|Promoting a fleet hotfix back to SDK |*standalone* (then close fleet +hotfix) + +|Security patch bump on a transitive dep |*both* + +|Tagging a release |*standalone* + +|Rolling out a release to production |*fleet* +|=== + +''''' + +=== See also + +* Issue +https://github.com/hyperpolymath/echidnabot/issues/51[`+hyperpolymath/echidnabot#51+`] +— diagnosis of the 109-file divergence. +* Memory note `+feedback_echidna_license_docs_mpl_intentional+` — docs +stay MPL-2.0 despite AGPL `+LICENSE+`; do not reconcile. +* Memory note `+feedback_echidna_src_abi_namespace_intentional+` — +`+src/abi/+` dual-tree layout is owner-managed. diff --git a/CANONICAL_SOURCE.md b/CANONICAL_SOURCE.md deleted file mode 100644 index ab58c8e..0000000 --- a/CANONICAL_SOURCE.md +++ /dev/null @@ -1,183 +0,0 @@ - - - - -# Canonical Source Map — echidnabot - -> **You are reading the STANDALONE tree perspective.** The sibling perspective -> lives at [`gitbot-fleet/bots/echidnabot/CANONICAL_SOURCE.md`](https://github.com/hyperpolymath/gitbot-fleet/blob/main/bots/echidnabot/CANONICAL_SOURCE.md) -> and has identical structure with the two roles swapped. - -Echidnabot exists in **two trees** by design. Each tree has a different -**purpose**; neither is a stale copy of the other. This document resolves the -seam (issue [`hyperpolymath/echidnabot#51`](https://github.com/hyperpolymath/echidnabot/issues/51)). - ---- - -## 1. Purpose — this tree (`hyperpolymath/echidnabot`) - -The **standalone repository** is the **SDK / library / reference -implementation**: - -- Tagged releases, semver versioning. -- Buildable as a library crate (`echidnabot` on crates.io eventually) and as a - reference binary. -- **Relaxed dependency pins** (e.g. `tokio = "1"`, `axum = "0.8"`, - `serde = "1"`) — version *ranges*, not exact versions. Downstream consumers - pick their own pinned lockfile. -- Carries the **full development surface**: `.claude/`, `.github/` (issue - templates, workflows), `EXPLAINME.adoc`, `RSR_OUTLINE.adoc`, `proofs/`, - `ffi/` (Idris2 ABI bindings), `contractiles/`, `.clusterfuzzlite/`, - governance scripts (`scripts/governance/`), full fuzz target set - (`fuzz_config.rs` + `fuzz_hmac.rs` + `fuzz_webhook_json.rs`), full test - matrix (`integration_tests.rs` + `lifecycle.rs` + `property_tests.rs` + - `seam_test.rs` + `smoke.rs` + `regressions/`). -- Library-shaped src tree: `src/abi/`, `src/feedback/`, `src/llm.rs`, - `src/api/rate_limit.rs`, `src/modes/directives.rs` — features that exist - here are the **forward edge** of the codebase. - -## 2. Sibling — `hyperpolymath/gitbot-fleet/bots/echidnabot/` - -The **fleet copy** is the **deployed production bot**: - -- Co-deployed with sibling bots (`accessibilitybot`, `finishingbot`, - `glambot`, `panicbot`, `rhodibot`, `seambot`, etc.) under - `gitbot-fleet/bots/`. -- Shares `gitbot-fleet/shared-context/` for cross-bot coordination - (Dependabot watches each bot independently — see - `dependabot/cargo/bots/echidnabot/*` branches). -- **Exact-pinned deps** (e.g. `tokio = "1.52.3"`, `axum = "0.8.9"`, - `serde = "1.0.228"`) — production lockfile alignment, no version drift - between deploy cycles. -- Slimmer development surface: no `.claude/`, no per-bot `.github/` - (fleet-level governance lives in `gitbot-fleet/.github/`), no - `EXPLAINME.adoc`, single fuzz target. -- Carries **production-only modules** that may or may not flow back: - `src/trust/migration_scanner.rs`, `tests/webhook_e2e_test.rs`, - `examples/SafeDOMExample.affine` (estate `.affine` migration in flight). - ---- - -## 3. File classes — who is canonical for what - -| File glob | Canonical | Direction | Rationale | -|---|---|---|---| -| `src/**/*.rs` (library + bot code) | **standalone** | standalone → fleet | Library/SDK is the forward edge. Fleet consumes a snapshot. | -| `src/abi/**` | **standalone** | standalone → fleet (when fleet wants ABI surface) | ABI namespace is owner-managed in standalone; fleet does not need it for deploy. See memory note `feedback_echidna_src_abi_namespace_intentional`. | -| `src/trust/migration_scanner.rs` | **fleet** | fleet → standalone (when promoted) | Production-driven feature; promote to standalone when the API stabilises. | -| `src/feedback/**`, `src/llm.rs` | **standalone** | standalone → fleet (on demand) | Forward-edge research surface (Package 7b double-loop, BoJ-mediated LLM); fleet adopts when production-ready. | -| `src/api/rate_limit.rs` | **standalone** | standalone → fleet | Hardening landed in standalone first; fleet should adopt for production. **See drift note below.** | -| `src/modes/directives.rs` | **standalone** | standalone → fleet | Mode-selection directives are SDK surface. | -| `Cargo.toml` (package metadata) | **shared** | bidirectional — diverge by design | Standalone keeps relaxed ranges; fleet keeps exact pins. Authors string + crate metadata sync periodically. | -| `Cargo.lock` | **each tree owns its own** | n/a | Lockfiles are deployment artefacts; standalone's reflects relaxed-range resolution, fleet's reflects pinned-version resolution. | -| `tests/integration_tests.rs`, `tests/lifecycle.rs`, `tests/property_tests.rs`, `tests/seam_test.rs`, `tests/smoke.rs`, `tests/regressions/**` | **standalone** | standalone → fleet (on demand) | Full test matrix lives in standalone; fleet runs a subset in production CI. | -| `tests/webhook_e2e_test.rs` | **fleet** | fleet → standalone (recommended) | End-to-end webhook test was added during fleet deployment hardening; should be promoted back to standalone. | -| `fuzz/fuzz_targets/fuzz_hmac.rs`, `fuzz_webhook_json.rs` | **standalone** | standalone → fleet (on demand) | Fuzz target expansion lives in standalone (also `.clusterfuzzlite/`). | -| `examples/*.affine` (e.g. `SafeDOMExample.affine`) | **fleet** | fleet → standalone (on `.affine` migration) | Estate `.affine` migration touched the fleet copy first; will reach standalone when the SafeDOM stdlib lands (`affinescript#56`). | -| `examples/*.json`, `examples/*.ts`, `examples/*.affinescript` | **standalone** | standalone → fleet | Reference examples for SDK users. | -| `echidnabot.example.toml`, `echidnabot.toml` | **standalone** | standalone → fleet | Configuration *schema* is SDK surface; fleet should mirror schema and only override defaults. | -| `Containerfile`, `flake.guix`, `guix.scm` | **standalone** | standalone → fleet | Reproducible-build manifests are SDK surface. Fleet may override base image for deploy. | -| `packaging/**` (debian/, rpm/, arch/, aur/, chocolatey/, macports/, scoop/) | **standalone** | standalone → fleet (when versions bump) | Distribution packaging is release-process artefact. | -| `hooks/**` (git hooks: SPDX, SHA-pins, CodeQL, permissions, tsjs-blocker) | **standalone** | standalone → fleet | Governance hooks; standalone is the source of truth. | -| `README.adoc`, `README.md`, `CHANGELOG.md` (vs `CHANGELOG.adoc`), `ROADMAP.adoc`, `CITATION.cff`, `codemeta.json`, `PALIMPSEST.adoc` | **standalone** | standalone → fleet | Doc canon. The `.md` vs `.adoc` CHANGELOG split is a long-standing inconsistency; standalone uses both. | -| `EXPLAINME.adoc`, `MAINTAINERS.adoc`, `RSR_OUTLINE.adoc`, `RSR_COMPLIANCE.adoc`, `CONTRIBUTING.md`, `CODE_OF_CONDUCT.md`, `SECURITY.md` | **standalone** | standalone → fleet (where applicable) | Project-level docs; some (e.g. `RSR_OUTLINE.adoc`) are standalone-only because the SDK is the RSR-compliant artefact. | -| `.claude/`, `.github/`, `.gitattributes`, `.gitignore`, `.editorconfig`, `.guix-channel`, `.well-known/`, `.machine_readable/`, `0-AI-MANIFEST.a2ml` | **standalone-only** | n/a | Per-repo metadata. Fleet-level equivalents live at `gitbot-fleet/.github/` and `gitbot-fleet/.claude/`. | -| `proofs/`, `ffi/`, `contractiles/`, `scripts/governance/` | **standalone-only** | n/a | Research / formal-methods / governance surface that does not belong in a deployed bot. | -| `scripts/batch_driver.sh` | **fleet-only** | n/a | Fleet-orchestration helper; out of scope for SDK. | -| `wiki/Home.md`, `docs/content/api.md`, `docs/templates/default.html` | **standalone** | standalone → fleet (rarely) | Documentation canon. | -| `docs/tech-debt-2026-05-26.md` | **standalone-only** | n/a | Tech-debt log; SDK-internal planning artefact. | -| `BRANDING.md`, `TESTING-REPORT.adoc`, `TESTING-REPORT.scm`, `SESSION_SUMMARY_2026-01-29.md`, `SONNET-TASKS.md`, `RELEASE_CHECKLIST.md`, `Mustfile`, `Containerfile` | **standalone** | standalone → fleet | Shared release/branding/testing surface. | - ---- - -## 4. Sync policy - -**Manual cherry-pick with quarterly diff sweep.** No automation. - -- **Default flow:** changes land in the canonical tree (per the table above) - via PR. The owner cherry-picks to the sibling when ready, in a separate PR - with a `Refs hyperpolymath/#` line. -- **Quarterly diff sweep:** the owner runs `diff -rq` between the two trees, - classifies new deltas against the table above, and either (a) cherry-picks - to align, (b) updates the table here to record intentional divergence, or - (c) files a follow-up issue if the delta needs design work. -- **CI gating:** none today. Adding a "no undocumented divergence" check - would require standards-repo work and is explicitly **out of scope** - (issue #51 picked the documentation-first option). - -### What this policy explicitly does NOT do - -- No auto-mirror / no sync bot / no submodule / no git subtree. -- No "regenerate fleet from standalone on every release" script. -- No standards-repo workflow. - -If automation becomes necessary later, a one-off `gitbot-fleet/scripts/sync-bot.sh` -(per-bot, not estate-wide) would be the natural place — but the owner has -deliberately deferred this until the divergence pattern stabilises. - ---- - -## 5. When to PR which — decision tree for contributors - -``` -What kind of change? -│ -├── New library API / new src module / SDK surface -│ └─→ PR to STANDALONE (this repo). Owner cherry-picks to fleet when ready. -│ -├── Bug fix in shared src/**/*.rs -│ └─→ PR to STANDALONE. Fix flows fleet-ward at next sweep. -│ (If the bug is production-only and you have a reproduction, -│ a fleet-side hotfix PR is acceptable; cross-reference standalone.) -│ -├── Production hardening (rate limit, retry, observability) -│ ├── If it's a new SDK feature → STANDALONE first, fleet adopts. -│ └── If it's deploy-specific (k8s tuning, fleet routing) → FLEET only. -│ -├── Dependency bump -│ ├── Patch bump (security) → BOTH trees, simultaneously. -│ ├── Minor/major in standalone → STANDALONE only (relaxed ranges -│ │ absorb it). Fleet updates exact-pin when ready. -│ └── Dependabot-driven exact-pin bump → FLEET only (this is what -│ Dependabot does; standalone's relaxed pins don't need it). -│ -├── `.affine` migration / AffineScript example -│ └─→ FLEET (where the migration is in flight). Promote to STANDALONE -│ once `affinescript#56` lands the SafeDOM stdlib bindings. -│ -├── Documentation / README / CHANGELOG / branding -│ └─→ STANDALONE. Fleet mirrors at next sweep. -│ -├── Governance: SPDX hooks, SHA-pin validators, security policy -│ └─→ STANDALONE. Fleet adopts the hook updates at next sweep. -│ (Fleet-level governance lives separately at gitbot-fleet/.github/.) -│ -├── Deployment config (Containerfile base image, k8s, compose) -│ └─→ FLEET. The standalone Containerfile is a reference; the fleet -│ Containerfile is the deployed one. -│ -└── New issue templates, .claude/ config, workflow files - └─→ STANDALONE for repo-specific. Fleet uses gitbot-fleet/.github/ - and gitbot-fleet/.claude/ for fleet-wide. -``` - -### Quick reference - -| You are doing... | PR target | -|---|---| -| Adding a Rust module under `src/` | **standalone** | -| Fixing a bug in `src/` shared by both | **standalone** | -| Adding a `.affine` example | **fleet** | -| Updating production deploy config | **fleet** | -| Promoting a fleet hotfix back to SDK | **standalone** (then close fleet hotfix) | -| Security patch bump on a transitive dep | **both** | -| Tagging a release | **standalone** | -| Rolling out a release to production | **fleet** | - ---- - -## See also - -- Issue [`hyperpolymath/echidnabot#51`](https://github.com/hyperpolymath/echidnabot/issues/51) — diagnosis of the 109-file divergence. -- Memory note `feedback_echidna_license_docs_mpl_intentional` — docs stay MPL-2.0 despite AGPL `LICENSE`; do not reconcile. -- Memory note `feedback_echidna_src_abi_namespace_intentional` — `src/abi/` dual-tree layout is owner-managed. diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc new file mode 100644 index 0000000..c0539ad --- /dev/null +++ b/CHANGELOG.adoc @@ -0,0 +1,124 @@ +== Changelog + +All notable changes to `+echidnabot+` will be documented in this file. + +This file is generated from conventional commits by the +https://github.com/hyperpolymath/standards/blob/main/.github/workflows/changelog-reusable.yml[`+changelog-reusable.yml+`] +workflow (`+hyperpolymath/standards#206+`). Adopt the workflow in this +repo’s CI to keep this file in sync automatically — see +https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml[`+templates/cliff.toml+`] +for the canonical config. + +The format follows https://keepachangelog.com/en/1.1.0/[Keep a +Changelog]; this project aims to follow +https://semver.org/spec/v2.0.0.html[Semantic Versioning]. + +=== [Unreleased] + +==== Added + +* feat(observability): OpenTelemetry distributed tracing via OTLP — +spans propagate from webhook receipt → dispatcher → executor → echidna +call → feedback; configurable endpoint via +`+[observability] otlp_endpoint+` or the standard +`+OTEL_EXPORTER_OTLP_ENDPOINT+` env var +* feat(observability): structured JSON logging via +`+tracing-subscriber+` — new `+src/observability.rs+` module + +`+ECHIDNABOT_LOG_FORMAT=text|json+` env var (default `+text+`); shared +init point for CLI, server, and future OpenTelemetry layer +* feat(lifecycle): graceful shutdown — drain in-flight + close DB + +flush observability ([ROADMAP "`Graceful shutdown (finish in-progress +jobs)`" item]) +** On `+SIGTERM+` / `+SIGINT+`: webhooks stop accepting, scheduler stops +dispatching, in-flight jobs drain (default 30s deadline), SQLite pool +closes cleanly, OpenTelemetry tracer flush hook fires (stub until the +observability agent’s PR lands). +** New module `+echidnabot::shutdown+` exposes `+ShutdownCoordinator+`, +`+ShutdownSignal+`, `+ShutdownTrigger+`, `+wait_for_termination+`, +`+resolve_shutdown_timeout+`. +** New config block `+[lifecycle] shutdown_timeout_secs = 30+` and env +override `+ECHIDNABOT_SHUTDOWN_TIMEOUT_SECS+` (env wins). +** New `+SqliteStore::close()+` for explicit pool drain (idempotent). +* feat(deployment): Docker Compose + PostgreSQL stack with optional +ECHIDNA REST stub under `+--profile dev+`; initial Postgres migration; +`+docs/deployment.adoc+` quickstart (closes #60) +* feat(trust+executor): Tier-3 prover coverage +(idris2/fstar/ATPs/protocol-checkers) +* feat(T3): wire bot modes into webhook response pipeline +* feat(feedback+graphql): double-loop write path, tactic GraphQL API, +ProverKind fixes +* feat(hardening): per-IP webhook rate limiting + ROADMAP/STATE updates +* feat(Task E): Begin ProverKind enum→slug migration for 113-prover +support +* feat(trust): wire trust bridge into dispatcher/scheduler pipeline +* feat(contractiles): add intend, bust, adjust verbs (6/6 complete) +* feat(governance): branch-protection script per estate memory rule +* feat(ci): add cargo-audit + db-checks workflows +* feat(ci): adopt 8 RSR-template workflows missing from echidnabot (#8) + +==== Fixed + +* fix(ci): sync hypatia-scan.yml to canonical (413: +env.HOME+Phase-2+SARIF) (#10) +* fix(ci): bump a2ml/k9-validate-action pins to canonical (standards#85) +(#9) +* fix(ci): adopt canonical hypatia-scan.yml (env.HOME/scanner-layout + +Comment-step gate) (#6) +* fix(rhodibot): automated RSR compliance fixes +* fix(corpus-delta): wire 7b-3 schema bridge — proof successes now reach +training corpus +* fix(echidnabot): resolve 25 compile errors from ProverKind→ProverSlug +migration +* fix(serve): warn at startup when webhook_secret is unset +* fix(serve): honour [server] section in echidnabot.toml +* fix(proofs): drop Coq .aux artefacts + gitignore build outputs +* fix(cargo): update gitbot-shared-context path after gitbot-fleet +relocation +* fix(openssf-compliance): provide top-level STATE.a2ml pointer for +literal-path check (#66) +* ci(cflite_pr): mark continue-on-error pending sibling-crate vendoring +(#66; follow-up #67) + +==== Changed + +* refactor(Task E): Continue ProverKind→ProverSlug migration integration +* refactor: eliminate all 13 production .unwrap() sites (#7) + +==== Documentation + +* docs(proof-debt): placeholder doc to satisfy governance/trusted-base +(#66; follow-up #68 for real rationale) +* docs(flake): annotate KEEP+DEP rationale per standards#102 rule 3 +(#16) +* docs(flake): annotate KEEP+DEP rationale per standards#102 rule 3 +(#15) +* docs(flake): annotate KEEP+DEP rationale per standards#102 rule 3 +(#13) +* docs(Task E): Document ProverKind→ProverSlug migration in STATE.a2ml +* docs(agentic): sunset BoJ-only-MCP exception — BoJ revived 2026-04-25 +* docs(bot-directives): extend self-directive with mode block (Phase 7) +* docs(crg): populate external-targets / issues-fed-back / field-signal +* docs(mcp): fix stale STATE.scm reference in schema-gap caveat +* docs: cascade .scm→.a2ml refs across release/template/k9 docs +* docs(claude): update .machine_readable/ path table post .scm→.a2ml +migration + +==== CI + +* ci(stress-test): SHA-pin dtolnay/rust-toolchain (#66) +* ci(rust): convert rust-ci.yml to thin wrapper (standards#174) (#19) +* ci: redistribute concurrency-cancel guard to read-only check workflows +(#12) +* ci: bump actions/upload-artifact SHA to current v4 (#5) +* ci: bump actions/upload-artifact SHA to current v4 (#4) +* ci: fix workflow-linter YAML parse error + self-flag bug + +=== Pre-history + +Prior commits to this file’s introduction are recorded in git history +but not formally classified into Keep-a-Changelog sections. To backfill, +run `+git cliff -o CHANGELOG.md+` locally using the canonical +https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml[`+cliff.toml+`] +— this is one-shot mechanical work. + +''''' diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 index be91496..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,97 +0,0 @@ - -# Changelog - -All notable changes to `echidnabot` will be documented in this file. - -This file is generated from conventional commits by the -[`changelog-reusable.yml`](https://github.com/hyperpolymath/standards/blob/main/.github/workflows/changelog-reusable.yml) -workflow (`hyperpolymath/standards#206`). Adopt the workflow in this repo's CI to keep this file in sync automatically — see -[`templates/cliff.toml`](https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml) -for the canonical config. - -The format follows [Keep a Changelog](https://keepachangelog.com/en/1.1.0/); -this project aims to follow [Semantic Versioning](https://semver.org/spec/v2.0.0.html). - -## [Unreleased] - -### Added - -- feat(observability): OpenTelemetry distributed tracing via OTLP — spans propagate from webhook receipt → dispatcher → executor → echidna call → feedback; configurable endpoint via `[observability] otlp_endpoint` or the standard `OTEL_EXPORTER_OTLP_ENDPOINT` env var -- feat(observability): structured JSON logging via `tracing-subscriber` — new `src/observability.rs` module + `ECHIDNABOT_LOG_FORMAT=text|json` env var (default `text`); shared init point for CLI, server, and future OpenTelemetry layer -- feat(lifecycle): graceful shutdown — drain in-flight + close DB + flush observability - ([ROADMAP "Graceful shutdown (finish in-progress jobs)" item]) - - On `SIGTERM` / `SIGINT`: webhooks stop accepting, scheduler stops - dispatching, in-flight jobs drain (default 30s deadline), SQLite - pool closes cleanly, OpenTelemetry tracer flush hook fires (stub - until the observability agent's PR lands). - - New module `echidnabot::shutdown` exposes `ShutdownCoordinator`, - `ShutdownSignal`, `ShutdownTrigger`, `wait_for_termination`, - `resolve_shutdown_timeout`. - - New config block `[lifecycle] shutdown_timeout_secs = 30` and env - override `ECHIDNABOT_SHUTDOWN_TIMEOUT_SECS` (env wins). - - New `SqliteStore::close()` for explicit pool drain (idempotent). -- feat(deployment): Docker Compose + PostgreSQL stack with optional ECHIDNA REST stub under `--profile dev`; initial Postgres migration; `docs/deployment.adoc` quickstart (closes #60) -- feat(trust+executor): Tier-3 prover coverage (idris2/fstar/ATPs/protocol-checkers) -- feat(T3): wire bot modes into webhook response pipeline -- feat(feedback+graphql): double-loop write path, tactic GraphQL API, ProverKind fixes -- feat(hardening): per-IP webhook rate limiting + ROADMAP/STATE updates -- feat(Task E): Begin ProverKind enum→slug migration for 113-prover support -- feat(trust): wire trust bridge into dispatcher/scheduler pipeline -- feat(contractiles): add intend, bust, adjust verbs (6/6 complete) -- feat(governance): branch-protection script per estate memory rule -- feat(ci): add cargo-audit + db-checks workflows -- feat(ci): adopt 8 RSR-template workflows missing from echidnabot (#8) - -### Fixed - -- fix(ci): sync hypatia-scan.yml to canonical (413: env.HOME+Phase-2+SARIF) (#10) -- fix(ci): bump a2ml/k9-validate-action pins to canonical (standards#85) (#9) -- fix(ci): adopt canonical hypatia-scan.yml (env.HOME/scanner-layout + Comment-step gate) (#6) -- fix(rhodibot): automated RSR compliance fixes -- fix(corpus-delta): wire 7b-3 schema bridge — proof successes now reach training corpus -- fix(echidnabot): resolve 25 compile errors from ProverKind→ProverSlug migration -- fix(serve): warn at startup when webhook_secret is unset -- fix(serve): honour [server] section in echidnabot.toml -- fix(proofs): drop Coq .aux artefacts + gitignore build outputs -- fix(cargo): update gitbot-shared-context path after gitbot-fleet relocation -- fix(openssf-compliance): provide top-level STATE.a2ml pointer for literal-path check (#66) -- ci(cflite_pr): mark continue-on-error pending sibling-crate vendoring (#66; follow-up #67) - -### Changed - -- refactor(Task E): Continue ProverKind→ProverSlug migration integration -- refactor: eliminate all 13 production .unwrap() sites (#7) - -### Documentation - -- docs(proof-debt): placeholder doc to satisfy governance/trusted-base (#66; follow-up #68 for real rationale) -- docs(flake): annotate KEEP+DEP rationale per standards#102 rule 3 (#16) -- docs(flake): annotate KEEP+DEP rationale per standards#102 rule 3 (#15) -- docs(flake): annotate KEEP+DEP rationale per standards#102 rule 3 (#13) -- docs(Task E): Document ProverKind→ProverSlug migration in STATE.a2ml -- docs(agentic): sunset BoJ-only-MCP exception — BoJ revived 2026-04-25 -- docs(bot-directives): extend self-directive with mode block (Phase 7) -- docs(crg): populate external-targets / issues-fed-back / field-signal -- docs(mcp): fix stale STATE.scm reference in schema-gap caveat -- docs: cascade .scm→.a2ml refs across release/template/k9 docs -- docs(claude): update .machine_readable/ path table post .scm→.a2ml migration - -### CI - -- ci(stress-test): SHA-pin dtolnay/rust-toolchain (#66) -- ci(rust): convert rust-ci.yml to thin wrapper (standards#174) (#19) -- ci: redistribute concurrency-cancel guard to read-only check workflows (#12) -- ci: bump actions/upload-artifact SHA to current v4 (#5) -- ci: bump actions/upload-artifact SHA to current v4 (#4) -- ci: fix workflow-linter YAML parse error + self-flag bug - -## Pre-history - -Prior commits to this file's introduction are recorded in git history but not formally classified into Keep-a-Changelog sections. To backfill, run `git cliff -o CHANGELOG.md` locally using the canonical [`cliff.toml`](https://github.com/hyperpolymath/standards/blob/main/templates/cliff.toml) — this is one-shot mechanical work. - ---- - - diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..f39d9ca --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,132 @@ +== Contributor Covenant Code of Conduct + +=== Our Pledge + +We as members, contributors, and leaders pledge to make participation in +our community a harassment-free experience for everyone, regardless of +age, body size, visible or invisible disability, ethnicity, sex +characteristics, gender identity and expression, level of experience, +education, socio-economic status, nationality, personal appearance, +race, religion, or sexual identity and orientation. + +We pledge to act and interact in ways that contribute to an open, +welcoming, diverse, inclusive, and healthy community. + +=== Our Standards + +Examples of behavior that contributes to a positive environment for our +community include: + +* Demonstrating empathy and kindness toward other people +* Being respectful of differing opinions, viewpoints, and experiences +* Giving and gracefully accepting constructive feedback +* Accepting responsibility and apologizing to those affected by our +mistakes, and learning from the experience +* Focusing on what is best not just for us as individuals, but for the +overall community + +Examples of unacceptable behavior include: + +* The use of sexualized language or imagery, and sexual attention or +advances of any kind +* Trolling, insulting or derogatory comments, and personal or political +attacks +* Public or private harassment +* Publishing others’ private information, such as a physical or email +address, without their explicit permission +* Other conduct which could reasonably be considered inappropriate in a +professional setting + +=== Enforcement Responsibilities + +Community leaders are responsible for clarifying and enforcing our +standards of acceptable behavior and will take appropriate and fair +corrective action in response to any behavior that they deem +inappropriate, threatening, offensive, or harmful. + +Community leaders have the right and responsibility to remove, edit, or +reject comments, commits, code, wiki edits, issues, and other +contributions that are not aligned to this Code of Conduct, and will +communicate reasons for moderation decisions when appropriate. + +=== Scope + +This Code of Conduct applies within all community spaces, and also +applies when an individual is officially representing the community in +public spaces. Examples of representing our community include using an +official e-mail address, posting via an official social media account, +or acting as an appointed representative at an online or offline event. + +=== Enforcement + +Instances of abusive, harassing, or otherwise unacceptable behavior may +be reported to the community leaders responsible for enforcement at . +All complaints will be reviewed and investigated promptly and fairly. + +All community leaders are obligated to respect the privacy and security +of the reporter of any incident. + +=== Enforcement Guidelines + +Community leaders will follow these Community Impact Guidelines in +determining the consequences for any action they deem in violation of +this Code of Conduct: + +==== 1. Correction + +*Community Impact*: Use of inappropriate language or other behavior +deemed unprofessional or unwelcome in the community. + +*Consequence*: A private, written warning from community leaders, +providing clarity around the nature of the violation and an explanation +of why the behavior was inappropriate. A public apology may be +requested. + +==== 2. Warning + +*Community Impact*: A violation through a single incident or series of +actions. + +*Consequence*: A warning with consequences for continued behavior. No +interaction with the people involved, including unsolicited interaction +with those enforcing the Code of Conduct, for a specified period of +time. This includes avoiding interactions in community spaces as well as +external channels like social media. Violating these terms may lead to a +temporary or permanent ban. + +==== 3. Temporary Ban + +*Community Impact*: A serious violation of community standards, +including sustained inappropriate behavior. + +*Consequence*: A temporary ban from any sort of interaction or public +communication with the community for a specified period of time. No +public or private interaction with the people involved, including +unsolicited interaction with those enforcing the Code of Conduct, is +allowed during this period. Violating these terms may lead to a +permanent ban. + +==== 4. Permanent Ban + +*Community Impact*: Demonstrating a pattern of violation of community +standards, including sustained inappropriate behavior, harassment of an +individual, or aggression toward or disparagement of classes of +individuals. + +*Consequence*: A permanent ban from any sort of public interaction +within the community. + +=== Attribution + +This Code of Conduct is adapted from the +https://www.contributor-covenant.org[Contributor Covenant], version 2.0, +available at +https://www.contributor-covenant.org/version/2/0/code_of_conduct.html. + +Community Impact Guidelines were inspired by +https://github.com/mozilla/diversity[Mozilla’s code of conduct +enforcement ladder]. + +For answers to common questions about this code of conduct, see the FAQ +at https://www.contributor-covenant.org/faq. Translations are available +at https://www.contributor-covenant.org/translations. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index e06b1e3..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,132 +0,0 @@ - -# Contributor Covenant Code of Conduct - -## Our Pledge - -We as members, contributors, and leaders pledge to make participation in our -community a harassment-free experience for everyone, regardless of age, body -size, visible or invisible disability, ethnicity, sex characteristics, gender -identity and expression, level of experience, education, socio-economic status, -nationality, personal appearance, race, religion, or sexual identity -and orientation. - -We pledge to act and interact in ways that contribute to an open, welcoming, -diverse, inclusive, and healthy community. - -## Our Standards - -Examples of behavior that contributes to a positive environment for our -community include: - -* Demonstrating empathy and kindness toward other people -* Being respectful of differing opinions, viewpoints, and experiences -* Giving and gracefully accepting constructive feedback -* Accepting responsibility and apologizing to those affected by our mistakes, - and learning from the experience -* Focusing on what is best not just for us as individuals, but for the - overall community - -Examples of unacceptable behavior include: - -* The use of sexualized language or imagery, and sexual attention or - advances of any kind -* Trolling, insulting or derogatory comments, and personal or political attacks -* Public or private harassment -* Publishing others' private information, such as a physical or email - address, without their explicit permission -* Other conduct which could reasonably be considered inappropriate in a - professional setting - -## Enforcement Responsibilities - -Community leaders are responsible for clarifying and enforcing our standards of -acceptable behavior and will take appropriate and fair corrective action in -response to any behavior that they deem inappropriate, threatening, offensive, -or harmful. - -Community leaders have the right and responsibility to remove, edit, or reject -comments, commits, code, wiki edits, issues, and other contributions that are -not aligned to this Code of Conduct, and will communicate reasons for moderation -decisions when appropriate. - -## Scope - -This Code of Conduct applies within all community spaces, and also applies when -an individual is officially representing the community in public spaces. -Examples of representing our community include using an official e-mail address, -posting via an official social media account, or acting as an appointed -representative at an online or offline event. - -## Enforcement - -Instances of abusive, harassing, or otherwise unacceptable behavior may be -reported to the community leaders responsible for enforcement at -. -All complaints will be reviewed and investigated promptly and fairly. - -All community leaders are obligated to respect the privacy and security of the -reporter of any incident. - -## Enforcement Guidelines - -Community leaders will follow these Community Impact Guidelines in determining -the consequences for any action they deem in violation of this Code of Conduct: - -### 1. Correction - -**Community Impact**: Use of inappropriate language or other behavior deemed -unprofessional or unwelcome in the community. - -**Consequence**: A private, written warning from community leaders, providing -clarity around the nature of the violation and an explanation of why the -behavior was inappropriate. A public apology may be requested. - -### 2. Warning - -**Community Impact**: A violation through a single incident or series -of actions. - -**Consequence**: A warning with consequences for continued behavior. No -interaction with the people involved, including unsolicited interaction with -those enforcing the Code of Conduct, for a specified period of time. This -includes avoiding interactions in community spaces as well as external channels -like social media. Violating these terms may lead to a temporary or -permanent ban. - -### 3. Temporary Ban - -**Community Impact**: A serious violation of community standards, including -sustained inappropriate behavior. - -**Consequence**: A temporary ban from any sort of interaction or public -communication with the community for a specified period of time. No public or -private interaction with the people involved, including unsolicited interaction -with those enforcing the Code of Conduct, is allowed during this period. -Violating these terms may lead to a permanent ban. - -### 4. Permanent Ban - -**Community Impact**: Demonstrating a pattern of violation of community -standards, including sustained inappropriate behavior, harassment of an -individual, or aggression toward or disparagement of classes of individuals. - -**Consequence**: A permanent ban from any sort of public interaction within -the community. - -## Attribution - -This Code of Conduct is adapted from the [Contributor Covenant][homepage], -version 2.0, available at -https://www.contributor-covenant.org/version/2/0/code_of_conduct.html. - -Community Impact Guidelines were inspired by [Mozilla's code of conduct -enforcement ladder](https://github.com/mozilla/diversity). - -[homepage]: https://www.contributor-covenant.org - -For answers to common questions about this code of conduct, see the FAQ at -https://www.contributor-covenant.org/faq. Translations are available at -https://www.contributor-covenant.org/translations. diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..8bc5c2e --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,315 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2025-2026 +Jonathan D.A. Jewell (hyperpolymath) –> + +== Contributing to echidnabot + +Thanks for your interest in contributing to *echidnabot* — the +proof-aware CI bot that bridges code platforms (GitHub / GitLab / +Bitbucket) and the https://github.com/hyperpolymath/echidna[ECHIDNA] +theorem-proving platform. + +This document covers the practicalities. For project conduct, see +link:CODE_OF_CONDUCT.md[`+CODE_OF_CONDUCT.md+`]; for security reports, +see link:SECURITY.md[`+SECURITY.md+`]; for maintainership and decision +rights, see link:MAINTAINERS.adoc[`+MAINTAINERS.adoc+`]. + +''''' + +=== Quick Start + +[source,bash] +---- +# Clone the repository +git clone https://github.com/hyperpolymath/echidnabot.git +cd echidnabot + +# Reproducible environment (Guix is the estate primary; guix is deprecated 2026-06-01) +guix shell -D -f guix.scm # Guix package (guix.scm) + +# Or bring your own toolchain (Rust 1.75+, SQLite, podman/bwrap) + +# Verify +cargo check +cargo test +---- + +==== Workspace caveat — `+gitbot-shared-context+` + +echidnabot’s `+Cargo.toml+` carries a *path dependency* on +`+gitbot-shared-context+` that assumes the +https://github.com/hyperpolymath/gitbot-fleet[gitbot-fleet] monorepo +layout (sibling directory `+../../shared-context+`). Building from a +bare clone of `+echidnabot+` alone therefore fails at the +dependency-resolution step. This is *acknowledged tech debt* — see issue +https://github.com/hyperpolymath/echidnabot/issues/18[#18]. Until that +is resolved, contributors who want a building tree should either: + +[arabic] +. Clone the parent +https://github.com/hyperpolymath/gitbot-fleet[`+gitbot-fleet+`] and work +from `+gitbot-fleet/bots/echidnabot/+`, *or* +. Provide a local checkout of `+shared-context+` at +`+../../shared-context+` relative to this clone, *or* +. Limit your changes to *documentation* (which is what this PR-class +covers — no build required). + +''''' + +=== Repository Layout + +.... +echidnabot/ +├── src/ # Rust source +│ ├── adapters/ # Platform adapters (GitHub, GitLab, Bitbucket) +│ ├── api/ # GraphQL + webhook handlers (axum) +│ ├── dispatcher/ # ECHIDNA HTTP client + prover enumeration +│ ├── scheduler/ # Job queue, retry, circuit breaker +│ ├── executor/ # Container isolation (podman + bwrap) +│ ├── modes/ # Bot modes (Verifier/Advisor/Consultant/Regulator) +│ ├── trust/ # Confidence levels, solver integrity, axiom tracking +│ ├── store/ # SQLite/PostgreSQL persistence +│ ├── feedback/ # Double-loop tactic-outcome recording +│ ├── fleet/ # Shared-context integration with gitbot-fleet +│ ├── abi/ # Idris2 ABI definitions (Types/Layout/Foreign) +│ ├── config.rs / error.rs / lib.rs / main.rs +├── ffi/zig/ # Zig FFI scaffold (see ABI-FFI-README.md) +├── tests/ # Integration + property + smoke + seam test suites +├── proofs/ # Dogfood proofs (Coq + Lean) — INCLUDES failing stubs +├── benches/ # cargo-criterion benchmarks +├── docs/ # Long-form documentation (casket-ssg) +├── wiki/ # Wiki source (mirrored to GitHub wiki) +├── packaging/ # Container/Guix packaging +├── .machine_readable/ # A2ML state, bot directives, contractiles +├── .well-known/ # security.txt / ai.txt / humans.txt +└── .github/workflows/ # CI — quality, codeql, scorecard, hypatia-scan +.... + +''''' + +=== How to Contribute + +==== Reporting Bugs + +[arabic] +. Search https://github.com/hyperpolymath/echidnabot/issues[existing +issues] to avoid duplicates. +. Check whether the bug is already fixed on `+main+`. +. Open a bug report using the +link:.github/ISSUE_TEMPLATE/bug_report.yml[bug_report.yml template] and +include: +* Environment (OS, Rust version, podman/bwrap version) +* Steps to reproduce +* Expected vs actual behaviour +* Logs (`+RUST_LOG=debug+` output if relevant) + +==== Suggesting Features + +[arabic] +. Check link:ROADMAP.adoc[`+ROADMAP.adoc+`] — your idea may already be +tracked. +. Open a feature request using the +link:.github/ISSUE_TEMPLATE/feature_request.yml[feature_request.yml +template]. +. Include a problem statement, not just a solution. + +==== Good-first-issue Labels + +* https://github.com/hyperpolymath/echidnabot/issues?q=is%3Aopen+label%3A%22good+first+issue%22[`+good first issue+`] +* https://github.com/hyperpolymath/echidnabot/issues?q=is%3Aopen+label%3A%22help+wanted%22[`+help wanted+`] +* https://github.com/hyperpolymath/echidnabot/issues?q=is%3Aopen+label%3Adocumentation[`+documentation+`] + +''''' + +=== Development Workflow + +==== Branch Naming + +.... +feat/ # New features +fix/- # Bug fixes +docs/ # Documentation only +refactor/ # Code improvement without behaviour change +test/ # Test additions +ci/ # CI / workflow changes +chore/ # Tooling / deps / housekeeping +security/ # Security fixes +.... + +==== Commit Messages + +We follow https://www.conventionalcommits.org/[Conventional Commits]: + +.... +(): + +[optional body explaining the why] + +[optional footer with Closes #N, Signed-off-by:, Co-Authored-By:] +.... + +Allowed types: `+feat+`, `+fix+`, `+docs+`, `+style+`, `+refactor+`, +`+perf+`, `+test+`, `+build+`, `+ci+`, `+chore+`, `+revert+`, +`+security+`. + +==== Commit Signing + +All commits *must be GPG-signed*. Configure: + +[source,bash] +---- +git config commit.gpgsign true +git config user.signingkey +---- + +Unsigned commits will fail the `+commit-signing+` enforcement check. + +==== Pull Request Checklist + +Before opening a PR: + +* [ ] `+cargo fmt --check+` is clean +* [ ] `+cargo clippy --all-targets -- -D warnings+` is clean +* [ ] `+cargo test+` passes (caveat: requires gitbot-fleet layout — see +above) +* [ ] New behaviour has tests (unit + integration where appropriate) +* [ ] Docs updated when touching public surface (README / wiki / CLI +help) +* [ ] `+CHANGELOG.md+` is *not* edited by hand — it regenerates from +conventional commits via +https://github.com/hyperpolymath/standards/blob/main/.github/workflows/changelog-reusable.yml[`+standards/changelog-reusable.yml+`] +* [ ] SPDX header on every new source file +(`+// SPDX-License-Identifier: CC-BY-SA-4.0+`) +* [ ] Commits GPG-signed + +When opening the PR: + +* Title matches conventional-commits style (`+feat(scheduler): ...+`). +* Description references closed issues (`+Closes #N+`). +* Auto-merge `+--squash --delete-branch+` is preferred for clean +history. + +''''' + +=== Language and Tooling Policy + +Per the https://github.com/hyperpolymath/standards[Hyperpolymath estate +policy]: + +[cols=",",options="header",] +|=== +|Allowed |Banned (replacement) +|Rust (primary) |TypeScript (use AffineScript) +|AffineScript |Node.js / npm / Bun (use Deno) +|Zig (FFI) |Python (use Julia/Rust) +|Idris2 (ABI proofs) |Go (use Rust) +|Guile Scheme (Guix) |Java/Kotlin/Swift (use Tauri/Dioxus) +|Nickel (config) |Jekyll (use casket-ssg) +|Julia (ML/data) |Dockerfile (use Containerfile) +|=== + +See link:.claude/CLAUDE.md[`+.claude/CLAUDE.md+`] for the full table and +enforcement rules. + +==== Security Defaults + +* SHA-256 or stronger only (no MD5/SHA1 for integrity) +* HTTPS / WSS / SSH only — never plain HTTP in code or docs +* SHA-pinned GitHub Action dependencies +* SPDX license headers on every source file + +''''' + +=== Testing + +[source,bash] +---- +cargo test # Full suite +cargo test --lib # Unit tests only +cargo test --test seam_test # Specific integration test +cargo test -- --nocapture # See println! output +---- + +The suite is currently *184 tests* (per `+STATE.a2ml+` last-updated +`+2026-04-26+`): + +* 137 lib unit tests +* 17 lifecycle integration tests +* 32 integration tests +* 12 property tests +* 15 seam tests +* 8 smoke tests + +==== Fuzzing + +[source,bash] +---- +cd fuzz +cargo +nightly fuzz run webhook_parse +---- + +ClusterFuzzLite runs continuous fuzzing in CI; see +`+.clusterfuzzlite/+`. + +''''' + +=== Documentation + +==== Files to keep in sync when touching public surface + +[width="100%",cols="44%,56%",options="header",] +|=== +|Change |Update +|New CLI flag / subcommand |`+README.adoc+` Usage section + +`+wiki/Getting-Started.md+` + +|New configuration option |`+echidnabot.example.toml+` + +`+docs/content/configuration.md+` + `+wiki/Getting-Started.md+` + +|New prover support |`+wiki/Supported-Provers.md+` + `+src/dispatcher/+` + +|New bot mode behaviour |`+wiki/FAQ.md+` + +`+.machine_readable/bot_directives/echidnabot.a2ml+` + +|ABI/FFI surface change |`+src/abi/*.idr+` + `+ffi/zig/src/main.zig+` + +`+ABI-FFI-README.md+` + +|Roadmap item closed |`+ROADMAP.adoc+` + +`+.machine_readable/6a2/STATE.a2ml+` +|=== + +==== Wiki + +Wiki source lives in `+wiki/+` in this repo. The GitHub wiki at +`+https://github.com/hyperpolymath/echidnabot.wiki.git+` is the rendered +mirror — push there directly when the wiki is enabled. See +link:RELEASE_CHECKLIST.md[`+RELEASE_CHECKLIST.md+`] for the push +procedure. + +==== Machine-readable state + +`+.machine_readable/6a2/+` holds A2ML descriptors consumed by Hypatia +and sibling bots. When a contribution lands a substantive change (new +external target, closed-issue feedback loop, completion-percentage +shift), update `+STATE.a2ml+` in the same commit. + +''''' + +=== Releasing + +Release procedure lives in +link:RELEASE_CHECKLIST.md[`+RELEASE_CHECKLIST.md+`]. Contributors do not +need to drive releases — flag readiness in a comment on the relevant +milestone issue. + +''''' + +=== Getting Help + +* *Code-level questions:* open a discussion at +https://github.com/hyperpolymath/echidnabot/discussions[hyperpolymath/echidnabot/discussions]. +* *Bugs:* https://github.com/hyperpolymath/echidnabot/issues[GitHub +Issues]. +* *Security:* see link:SECURITY.md[`+SECURITY.md+`] — do *not* open +public issues for vulnerabilities. + +Thanks for contributing! diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index b2b02c7..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,287 +0,0 @@ - -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (hyperpolymath) ---> - -# Contributing to echidnabot - -Thanks for your interest in contributing to **echidnabot** — the proof-aware -CI bot that bridges code platforms (GitHub / GitLab / Bitbucket) and the -[ECHIDNA](https://github.com/hyperpolymath/echidna) theorem-proving platform. - -This document covers the practicalities. For project conduct, see -[`CODE_OF_CONDUCT.md`](CODE_OF_CONDUCT.md); for security reports, see -[`SECURITY.md`](SECURITY.md); for maintainership and decision rights, see -[`MAINTAINERS.adoc`](MAINTAINERS.adoc). - ---- - -## Quick Start - -```bash -# Clone the repository -git clone https://github.com/hyperpolymath/echidnabot.git -cd echidnabot - -# Reproducible environment (Guix is the estate primary; guix is deprecated 2026-06-01) -guix shell -D -f guix.scm # Guix package (guix.scm) - -# Or bring your own toolchain (Rust 1.75+, SQLite, podman/bwrap) - -# Verify -cargo check -cargo test -``` - -### Workspace caveat — `gitbot-shared-context` - -echidnabot's `Cargo.toml` carries a **path dependency** on -`gitbot-shared-context` that assumes the -[gitbot-fleet](https://github.com/hyperpolymath/gitbot-fleet) monorepo -layout (sibling directory `../../shared-context`). Building from a bare -clone of `echidnabot` alone therefore fails at the dependency-resolution -step. This is **acknowledged tech debt** — see issue -[#18](https://github.com/hyperpolymath/echidnabot/issues/18). Until that -is resolved, contributors who want a building tree should either: - -1. Clone the parent - [`gitbot-fleet`](https://github.com/hyperpolymath/gitbot-fleet) and - work from `gitbot-fleet/bots/echidnabot/`, **or** -2. Provide a local checkout of `shared-context` at `../../shared-context` - relative to this clone, **or** -3. Limit your changes to **documentation** (which is what this PR-class - covers — no build required). - ---- - -## Repository Layout - -``` -echidnabot/ -├── src/ # Rust source -│ ├── adapters/ # Platform adapters (GitHub, GitLab, Bitbucket) -│ ├── api/ # GraphQL + webhook handlers (axum) -│ ├── dispatcher/ # ECHIDNA HTTP client + prover enumeration -│ ├── scheduler/ # Job queue, retry, circuit breaker -│ ├── executor/ # Container isolation (podman + bwrap) -│ ├── modes/ # Bot modes (Verifier/Advisor/Consultant/Regulator) -│ ├── trust/ # Confidence levels, solver integrity, axiom tracking -│ ├── store/ # SQLite/PostgreSQL persistence -│ ├── feedback/ # Double-loop tactic-outcome recording -│ ├── fleet/ # Shared-context integration with gitbot-fleet -│ ├── abi/ # Idris2 ABI definitions (Types/Layout/Foreign) -│ ├── config.rs / error.rs / lib.rs / main.rs -├── ffi/zig/ # Zig FFI scaffold (see ABI-FFI-README.md) -├── tests/ # Integration + property + smoke + seam test suites -├── proofs/ # Dogfood proofs (Coq + Lean) — INCLUDES failing stubs -├── benches/ # cargo-criterion benchmarks -├── docs/ # Long-form documentation (casket-ssg) -├── wiki/ # Wiki source (mirrored to GitHub wiki) -├── packaging/ # Container/Guix packaging -├── .machine_readable/ # A2ML state, bot directives, contractiles -├── .well-known/ # security.txt / ai.txt / humans.txt -└── .github/workflows/ # CI — quality, codeql, scorecard, hypatia-scan -``` - ---- - -## How to Contribute - -### Reporting Bugs - -1. Search [existing issues](https://github.com/hyperpolymath/echidnabot/issues) - to avoid duplicates. -2. Check whether the bug is already fixed on `main`. -3. Open a bug report using the - [bug_report.yml template](.github/ISSUE_TEMPLATE/bug_report.yml) and - include: - - Environment (OS, Rust version, podman/bwrap version) - - Steps to reproduce - - Expected vs actual behaviour - - Logs (`RUST_LOG=debug` output if relevant) - -### Suggesting Features - -1. Check [`ROADMAP.adoc`](ROADMAP.adoc) — your idea may already be tracked. -2. Open a feature request using the - [feature_request.yml template](.github/ISSUE_TEMPLATE/feature_request.yml). -3. Include a problem statement, not just a solution. - -### Good-first-issue Labels - -- [`good first issue`](https://github.com/hyperpolymath/echidnabot/issues?q=is%3Aopen+label%3A%22good+first+issue%22) -- [`help wanted`](https://github.com/hyperpolymath/echidnabot/issues?q=is%3Aopen+label%3A%22help+wanted%22) -- [`documentation`](https://github.com/hyperpolymath/echidnabot/issues?q=is%3Aopen+label%3Adocumentation) - ---- - -## Development Workflow - -### Branch Naming - -``` -feat/ # New features -fix/- # Bug fixes -docs/ # Documentation only -refactor/ # Code improvement without behaviour change -test/ # Test additions -ci/ # CI / workflow changes -chore/ # Tooling / deps / housekeeping -security/ # Security fixes -``` - -### Commit Messages - -We follow [Conventional Commits](https://www.conventionalcommits.org/): - -``` -(): - -[optional body explaining the why] - -[optional footer with Closes #N, Signed-off-by:, Co-Authored-By:] -``` - -Allowed types: `feat`, `fix`, `docs`, `style`, `refactor`, `perf`, `test`, -`build`, `ci`, `chore`, `revert`, `security`. - -### Commit Signing - -All commits **must be GPG-signed**. Configure: - -```bash -git config commit.gpgsign true -git config user.signingkey -``` - -Unsigned commits will fail the `commit-signing` enforcement check. - -### Pull Request Checklist - -Before opening a PR: - -- [ ] `cargo fmt --check` is clean -- [ ] `cargo clippy --all-targets -- -D warnings` is clean -- [ ] `cargo test` passes (caveat: requires gitbot-fleet layout — see above) -- [ ] New behaviour has tests (unit + integration where appropriate) -- [ ] Docs updated when touching public surface (README / wiki / CLI help) -- [ ] `CHANGELOG.md` is **not** edited by hand — it regenerates from - conventional commits via - [`standards/changelog-reusable.yml`](https://github.com/hyperpolymath/standards/blob/main/.github/workflows/changelog-reusable.yml) -- [ ] SPDX header on every new source file - (`// SPDX-License-Identifier: CC-BY-SA-4.0`) -- [ ] Commits GPG-signed - -When opening the PR: - -- Title matches conventional-commits style (`feat(scheduler): ...`). -- Description references closed issues (`Closes #N`). -- Auto-merge `--squash --delete-branch` is preferred for clean history. - ---- - -## Language and Tooling Policy - -Per the -[Hyperpolymath estate policy](https://github.com/hyperpolymath/standards): - -| Allowed | Banned (replacement) | -| ---------------------- | --------------------------------- | -| Rust (primary) | TypeScript (use AffineScript) | -| AffineScript | Node.js / npm / Bun (use Deno) | -| Zig (FFI) | Python (use Julia/Rust) | -| Idris2 (ABI proofs) | Go (use Rust) | -| Guile Scheme (Guix) | Java/Kotlin/Swift (use Tauri/Dioxus) | -| Nickel (config) | Jekyll (use casket-ssg) | -| Julia (ML/data) | Dockerfile (use Containerfile) | - -See [`.claude/CLAUDE.md`](.claude/CLAUDE.md) for the full table and -enforcement rules. - -### Security Defaults - -- SHA-256 or stronger only (no MD5/SHA1 for integrity) -- HTTPS / WSS / SSH only — never plain HTTP in code or docs -- SHA-pinned GitHub Action dependencies -- SPDX license headers on every source file - ---- - -## Testing - -```bash -cargo test # Full suite -cargo test --lib # Unit tests only -cargo test --test seam_test # Specific integration test -cargo test -- --nocapture # See println! output -``` - -The suite is currently **184 tests** (per `STATE.a2ml` last-updated -`2026-04-26`): - -- 137 lib unit tests -- 17 lifecycle integration tests -- 32 integration tests -- 12 property tests -- 15 seam tests -- 8 smoke tests - -### Fuzzing - -```bash -cd fuzz -cargo +nightly fuzz run webhook_parse -``` - -ClusterFuzzLite runs continuous fuzzing in CI; see -`.clusterfuzzlite/`. - ---- - -## Documentation - -### Files to keep in sync when touching public surface - -| Change | Update | -| ------------------------------------------- | ------------------------------------------------------- | -| New CLI flag / subcommand | `README.adoc` Usage section + `wiki/Getting-Started.md` | -| New configuration option | `echidnabot.example.toml` + `docs/content/configuration.md` + `wiki/Getting-Started.md` | -| New prover support | `wiki/Supported-Provers.md` + `src/dispatcher/` | -| New bot mode behaviour | `wiki/FAQ.md` + `.machine_readable/bot_directives/echidnabot.a2ml` | -| ABI/FFI surface change | `src/abi/*.idr` + `ffi/zig/src/main.zig` + `ABI-FFI-README.md` | -| Roadmap item closed | `ROADMAP.adoc` + `.machine_readable/6a2/STATE.a2ml` | - -### Wiki - -Wiki source lives in `wiki/` in this repo. The GitHub wiki at -`https://github.com/hyperpolymath/echidnabot.wiki.git` is the rendered -mirror — push there directly when the wiki is enabled. See -[`RELEASE_CHECKLIST.md`](RELEASE_CHECKLIST.md) for the push procedure. - -### Machine-readable state - -`.machine_readable/6a2/` holds A2ML descriptors consumed by Hypatia and -sibling bots. When a contribution lands a substantive change (new -external target, closed-issue feedback loop, completion-percentage -shift), update `STATE.a2ml` in the same commit. - ---- - -## Releasing - -Release procedure lives in [`RELEASE_CHECKLIST.md`](RELEASE_CHECKLIST.md). -Contributors do not need to drive releases — flag readiness in a comment -on the relevant milestone issue. - ---- - -## Getting Help - -- **Code-level questions:** open a discussion at - [hyperpolymath/echidnabot/discussions](https://github.com/hyperpolymath/echidnabot/discussions). -- **Bugs:** [GitHub Issues](https://github.com/hyperpolymath/echidnabot/issues). -- **Security:** see [`SECURITY.md`](SECURITY.md) — do **not** open public - issues for vulnerabilities. - -Thanks for contributing! diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc index e41020d..9b836fb 100644 --- a/GOVERNANCE.adoc +++ b/GOVERNANCE.adoc @@ -1,162 +1,60 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= Governance Model -:toc: preamble +== Governance -This document describes the governance model for this repository. +=== Overview -== Overview +This project is governed by the following principles and structures to +ensure transparent, inclusive, and effective decision-making. -This repository follows a **Sole Maintainer Governance Model**: +=== Roles and Responsibilities -* Single maintainer (@hyperpolymath) has full authority over the project -* All contributions are welcome and reviewed by the maintainer -* Decisions are made transparently through GitHub issues and discussions -* The project adheres to the hyperpolymath estate policies where applicable +==== Maintainers -== Core Principles +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 -[cols="1,2"] -|=== -| Principle | Description +==== Contributors -| **Benevolent Dictatorship** | Maintainer has final decision authority but seeks community input +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 -| **Meritocracy** | Contributions are judged on technical merit, not contributor identity +=== Decision Making -| **Transparency** | All significant decisions are documented publicly +==== Minor Changes -| **Consensus-Seeking** | Maintainer prefers consensus but will decide when necessary +* Can be made by any maintainer +* Include bug fixes, documentation updates, dependency updates -| **Open Contribution** | Anyone can contribute via fork and pull request +==== Major Changes -|=== +* Require discussion in issues or pull requests +* Include new features, architectural changes, API changes +* Need approval from at least 2 maintainers -== Roles and Permissions +==== Breaking Changes -[cols="1,2,2"] -|=== -| Role | Permissions | Assignment +* Require RFC (Request for Comments) process +* Need approval from majority of maintainers +* Must include migration guide -| **Maintainer** | Write access, merge rights, admin | @hyperpolymath -| **Contributors** | Read access, fork, submit PRs | All GitHub users -| **Users** | Use the software, report issues | All GitHub users +=== Code of Conduct -|=== +All participants are expected to follow our Code of Conduct. Violations +can be reported to the maintainers. -== Decision Making Framework +=== Communication -=== Routine Decisions +* *Issues*: For bug reports and feature requests +* *Discussions*: For questions and general discussion +* *Pull Requests*: For code contributions -* Bug fixes -* Documentation improvements -* Minor feature additions -* Dependency updates +=== Licensing -**Process**: Maintainer reviews and merges PRs that meet quality standards. +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. -=== Significant Changes +''''' -* New major features -* API changes -* Architecture modifications -* Breaking changes - -**Process**: -. Open issue describing the change -. Discuss with community (minimum 72 hours) -. Maintainer makes final decision -. Document rationale in issue/PR - -=== Structural Decisions - -* Repository purpose/renaming -* License changes -* Ownership transfer -* Deprecation/archival - -**Process**: -. Extended discussion (minimum 1 week) -. Maintainer makes final decision -. Document in CHANGELOG and governance docs - -== Contribution Lifecycle - -[cols="1,2"] -|=== -| Stage | Process - -| **Ideation** | Open issue, discuss feasibility - -| **Development** | Fork, implement, test thoroughly - -| **Review** | Submit PR, maintainer reviews within 7 days - -| **Merge** | Maintainer merges or requests changes - -| **Release** | Maintainer publishes according to project conventions - -|=== - -== Conflict Resolution - -In case of disagreements: - -. Discuss in the relevant GitHub issue or PR -. Provide technical justification for positions -. Maintainer mediates and makes final decision -. Decision is documented and can be revisited later - -== Project Policies - -This repository adheres to hyperpolymath estate-wide policies: - -* **License**: MPL-2.0 for code, CC-BY-SA-4.0 for prose (per standards/LICENCE-POLICY.adoc) -* **Code of Conduct**: Follows hyperpolymath CODE_OF_CONDUCT.md -* **Security**: Follows hyperpolymath SECURITY.md -* **Contributing**: Follows hyperpolymath CONTRIBUTING.adoc conventions - -== Repository-Specific Conventions - -[cols="1,2"] -|=== -| Convention | Description - -| **Signing** | All commits must be signed (SSH or GPG) - -| **SPDX Headers** | All source files must have SPDX license identifiers - -| **Contractiles** | Mustfile, Trustfile, Intendfile, Adjustfile in root - -| **Machine Readable** | META.a2ml in .machine_readable/6a2/ - -| **CI/CD** | GitHub Actions workflows in .github/workflows/ - -|=== - -== Governance Evolution - -As the project grows, this governance model may evolve: - -* **Adding Co-Maintainers**: When contribution volume warrants it -* **Forming a Team**: For complex multi-maintainer projects -* **Adopting TPCF**: For large, multi-repository projects (see rhodium-standard-repositories) - -Changes to this document require the same process as Significant Changes above. - -== See Also - -* link:MAINTAINERS.adoc[Maintainers] -* link:CODE_OF_CONDUCT.md[Code of Conduct] -* link:CONTRIBUTING.adoc[Contributing Guide] -* link:https://github.com/hyperpolymath/standards/blob/main/LICENCE-POLICY.adoc[Estate License Policy] -* link:https://github.com/hyperpolymath/standards[rhodium-standard-repositories (TPCF)] - -== Changelog - -[cols="1,1,1"] -|=== -| Date | Change | By - -| 2026-06-07 | Initial governance model established | @hyperpolymath -|=== +_Last updated: 2026-07-18_ diff --git a/GOVERNANCE.md b/GOVERNANCE.md deleted file mode 100644 index e27364c..0000000 --- a/GOVERNANCE.md +++ /dev/null @@ -1,60 +0,0 @@ -# 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 - -## Decision Making - -### 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 - -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. - ---- - -*Last updated: 2026-07-18* diff --git a/README.adoc b/README.adoc index 4006efd..8ec330c 100644 --- a/README.adoc +++ b/README.adoc @@ -1,520 +1,140 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -image:https://img.shields.io/badge/License-MPL_2.0--1.0-blue.svg[License: MPL-2.0,link="https://github.com/hyperpolymath/palimpsest-license"] -image:https://img.shields.io/github/v/release/hyperpolymath/echidnabot?include_prereleases[GitHub Release] - - -= echidnabot: Proof-Aware CI Bot -image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=openssourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/echidnabot"] - - -:toc: macro -:toclevels: 3 -:icons: font -:source-highlighter: pygments - -_Formal verification CI bot that orchestrates ECHIDNA for automatic theorem proof verification on every push._ - -NOTE: Echidnabot exists in two trees by design — this **standalone** repo (SDK / library / reference implementation) and the **fleet copy** at `gitbot-fleet/bots/echidnabot/` (deployed production bot). See link:CANONICAL_SOURCE.md[CANONICAL_SOURCE.md] for the file-class canonical map and contributor decision tree. - -toc::[] - -== Overview - -**echidnabot** bridges code platforms (GitHub, GitLab, Bitbucket) and the ECHIDNA theorem proving platform. -Every push, every PR -- proofs get verified automatically and results appear in your CI checks. - -It is part of the https://github.com/hyperpolymath/gitbot-fleet[gitbot-fleet] ecosystem, -coordinated by https://github.com/hyperpolymath/hypatia[Hypatia]. - -=== The Problem - -You are writing formally verified software -- proofs in Coq, Lean, Agda, or Isabelle. -But your CI pipeline does not understand proofs: - -* Tests pass, but **proofs are broken** -* PRs merge with **unverified theorems** -* No one notices until a dependent build fails -* Manual verification is **slow and error-prone** - -=== The Solution - -[source] ----- - GitHub/GitLab/Bitbucket - | - | webhook (push/PR) - v - +-------------------+ - | echidnabot | <-- Rust, Tokio, Axum - | +--------------+ | - | | Scheduler |--+---> ECHIDNA Core (Agda, Coq, Lean, Z3...) - | | Bot Modes | | - | | Trust Bridge | | - | | GraphQL API | | - | +--------------+ | - +-------------------+ - | - | Check Runs / Comments - v - v Proof verified - x Proof failed (line 42: goal not discharged) ----- - -== Current Status (v0.1.0) - -**Overall completion: ~90%** -- Core infrastructure, platform adapters, ECHIDNA integration, container isolation, bot modes, retry/circuit breaker, and trust bridge are implemented. 184 automated tests across lib, lifecycle, integration, property, seam, and smoke suites. Production hardening (observability, rate limiting, deployment automation) remains. - -=== What Is Implemented - -[cols="2,1,3"] -|=== -|Component |Status |Details - -|Core Infrastructure -|Complete -|Axum HTTP server, webhook signature verification (HMAC-SHA256), GraphQL API (async-graphql), SQLite/PostgreSQL persistence (sqlx), configuration system, structured error handling - -|Platform Adapters -|Complete -|`PlatformAdapter` trait with GitHub (octocrab), GitLab, and Bitbucket implementations; webhook receivers for all three; check run/commit status creation; PR/MR comments - -|ECHIDNA Integration -|Complete -|HTTP client (reqwest) for ECHIDNA REST API, `ProverSlug`-based prover addressing (String newtype, 12 backends wired by default), tier classification, job dispatch, result parsing, prover health checking - -|Job Scheduler -|Complete -|Priority queue, PostgreSQL/SQLite persistence, job status tracking, retry logic with exponential backoff and jitter, circuit breaker (opens after 5 failures, auto-resets after 5 min), concurrent job limits via semaphores (global + per-repo) - -|Container Isolation -|Complete -|Podman rootless containers with bwrap fallback; `--network=none`, `--cap-drop=ALL`, `--security-opt=no-new-privileges`, `--read-only` filesystem (writable `/tmp`), CPU/memory/pids limits, timeout enforcement with SIGKILL; fail-safe policy (refuses to run proofs if no isolation backend available) - -|Bot Modes -|Complete -|Four modes: Verifier (silent pass/fail), Advisor (tactic suggestions via ECHIDNA ML), Consultant (interactive Q&A on explicit `@echidnabot check` mention), Regulator (merge blocking); mode parsing from `.bot_directives/echidnabot.scm`; mode-dependent auto-trigger logic; result formatting bridge - -|ECHIDNA Trust Bridge -|Complete -|5-level proof confidence assessment (cross-checked small-kernel = Level 5, large-TCB = Level 1); solver integrity verification against SHA-256 manifest with constant-time comparison; axiom usage tracking (sorry, Admitted, postulate, oops, type-in-type, axiom of choice, classical axioms) with 3-tier severity - -|CLI -|Complete -|Subcommands: `serve`, `register`, `check`, `status`, `init-db`; auto-detection of prover from file extension - -|Tests -|Complete -|184 tests across lib, lifecycle, integration, property, seam, and smoke suites covering webhook verification, ECHIDNA client, bot modes, job lifecycle, database models, circuit breaker, container executor, trust bridge, axiom tracking, result formatting -|=== - -=== What Is Not Yet Implemented - -* **Observability** -- Prometheus metrics endpoint at `/metrics` (basic counters); OpenTelemetry distributed tracing wired via OTLP — see <> -* **Rate limiting** -- Webhook endpoints accept unlimited requests -* **Deployment automation** -- Compose stack landed (issue #60, see <>); Kubernetes manifests and Helm charts still TODO -* **Pre-built prover images** -- Container startup requires prover binaries in the image -* **Trust bridge not wired into main pipeline** -- Trust modules exist but are not yet called from the scheduler loop - -== Features - -=== Multi-Prover Support (12 Provers via ECHIDNA) - -[cols="1,1,2"] -|=== -|Tier |Provers |Notes - -|**Tier 1** -|Coq, Lean 4, Agda, Isabelle/HOL, Z3, CVC5 -|Small-kernel systems (except Z3/CVC5) with highest trust - -|**Tier 2** -|Metamath, HOL Light, Mizar -|Stable provers - -|**Tier 3** -|PVS, ACL2, HOL4 -|Supported via ECHIDNA -|=== - -All proof verification is delegated to ECHIDNA. echidnabot is an orchestrator, not a prover. - -=== Multi-Platform Integration - -* **GitHub** -- Check Runs, PR comments, webhook receiver (octocrab) -* **GitLab** -- Commit statuses, MR notes, webhook receiver -* **Bitbucket** -- Build statuses, PR comments, webhook receiver -* **Codeberg** -- Platform enum defined, adapter not yet implemented - -All platforms use a unified `PlatformAdapter` trait for consistent behavior. - -=== Bot Modes - -[cols="1,2,1"] -|=== -|Mode |Behavior |Auto-triggers? - -|**Verifier** -|Silent pass/fail on proof files (minimal output) -|Yes - -|**Advisor** -|Detailed failure output with tactic suggestions via ECHIDNA ML -|Yes - -|**Consultant** -|Interactive Q&A; responds only to `@echidnabot check` mentions -|No - -|**Regulator** -|Blocks PR merges when proofs fail; enforcement mode -|Yes -|=== - -Mode is configured per-repository via `.bot_directives/echidnabot.scm`: - -[source,scheme] ----- -(echidnabot (mode "advisor")) ----- - -Default mode is Verifier. - -=== Container Isolation - -Proof verification runs in isolated environments to prevent arbitrary code execution: - -* **Primary:** Podman rootless containers -* **Fallback:** bubblewrap (bwrap) lightweight sandbox -* **Fail-safe:** Refuses to run proofs if neither is available - -Security controls: - -* `--network=none` (no network access) -* `--cap-drop=ALL` (drop all capabilities) -* `--security-opt=no-new-privileges` -* `--read-only` root filesystem (writable `/tmp` only) -* CPU, memory, and PID limits -* Timeout enforcement with SIGKILL - -=== Retry Logic and Circuit Breaker - -* **Exponential backoff** with jitter: 1s, 2s, 4s (configurable) -* **Transient vs permanent** error classification (timeouts retry, config errors do not) -* **Circuit breaker** for ECHIDNA API protection: opens after 5 consecutive failures, auto-resets after 5 minutes, half-open state for recovery testing - -=== ECHIDNA Trust Bridge - -Three trust mechanisms: - -1. **Confidence Levels (1-5):** Assess proof trust based on prover kernel size, certificate presence, and cross-checking count -2. **Solver Integrity:** SHA-256 manifest verification of solver binaries with constant-time comparison -3. **Axiom Tracking:** Detects `sorry`, `Admitted`, `postulate`, `oops`, `--type-in-type`, axiom of choice, classical axioms; 3-tier severity (unsound / warning / informational) - -[[enable-distributed-tracing]] -=== Enable Distributed Tracing (OpenTelemetry) - -Spans propagate through the full pipeline -- webhook receipt -> dispatcher -> executor -> ECHIDNA call -> feedback publish -- and export to any OTLP-compatible collector (Jaeger, Tempo, Honeycomb, etc.) over gRPC. - -Two ways to configure the OTLP endpoint: - -. **Environment variable** (standard `OTEL_*` env): -+ -[source,sh] ----- -export OTEL_EXPORTER_OTLP_ENDPOINT="http://localhost:4317" -echidnabot serve ----- - -. **TOML config** (`echidnabot.toml`): -+ -[source,toml] ----- -[observability] -otlp_endpoint = "http://localhost:4317" -service_name = "echidnabot" # used as service.name resource attr ----- - -The environment variable takes precedence over the TOML value. When neither is set, span data is not exported -- the local fmt-layer logs remain active. - -Resource attributes set on every span: `service.name`, `service.version` (from `CARGO_PKG_VERSION`). - -Instrumented operations: - -* `webhook.github` / `webhook.gitlab` / `webhook.bitbucket` -- payload bytes + event type + delivery id -* `dispatch.job` -- platform, repo, commit, PR number, priority -* `echidna.verify` / `echidna.suggest` / `echidna.status` -- prover slug + API mode -* `executor.run` -- prover, isolation backend, proof bytes -* `feedback.publish` -- prover, tactic, succeeded, source - -In-flight spans are flushed on clean process exit via `TracerShutdown::shutdown()` (called from `main`). - -== Installation - -=== Prerequisites - -* Rust 1.75+ -* SQLite (development) or PostgreSQL (production) -* Podman or bubblewrap for container isolation -* Access to an ECHIDNA instance (or run locally) - -=== From Source +SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2025-2026 +Jonathan D.A. Jewell (hyperpolymath) –> + +== echidnabot — Proof-Aware CI Bot + +https://github.com/sponsors/hyperpolymath[image:https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github[Sponsor]] +https://github.com/hyperpolymath/palimpsest-license[image:https://img.shields.io/badge/License-MPL--2.0-blue.svg[License: +PMPL-1.0]] +https://github.com/hyperpolymath/echidnabot/releases[image:https://img.shields.io/github/v/release/hyperpolymath/echidnabot?include_prereleases[GitHub +Release]] + +____ +*The canonical README is link:README.adoc[`+README.adoc+`].* This +Markdown file exists for renderers that prefer `+.md+` (some package +indexes, some doc tooling); it is a thin summary that links into the +AsciiDoc version for the full story. +____ + +''''' + +=== What is it? + +A formal-verification CI bot that orchestrates the +https://github.com/hyperpolymath/echidna[ECHIDNA] theorem-proving +platform for automatic proof verification on every push and pull +request. Written in Rust on Tokio/Axum. + +Part of the https://github.com/hyperpolymath/gitbot-fleet[gitbot-fleet] +(Tier-1 Verifier role), coordinated by +https://github.com/hyperpolymath/hypatia[Hypatia]. + +=== Why does it exist? + +You’re writing formally verified software — proofs in Coq, Lean, Agda, +or Isabelle. But your CI pipeline doesn’t understand proofs: + +* Tests pass, but *proofs are broken*. +* PRs merge with *unverified theorems*. +* No one notices until a dependent build fails. +* Manual verification is *slow and error-prone*. + +echidnabot bridges the gap. Push proof files; get verified. + +=== Features (high-level) + +* *12 provers via ECHIDNA* — Coq, Lean 4, Agda, Isabelle/HOL, Z3, CVC5, +Metamath, HOL Light, Mizar, PVS, ACL2, HOL4 (see +link:wiki/Supported-Provers.md[`+wiki/Supported-Provers.md+`]; upstream +supports 113, drift documented in +link:EXPLAINME.adoc[`+EXPLAINME.adoc+`]). +* *3 platforms* — GitHub, GitLab, Bitbucket (Codeberg planned). +* *4 bot modes* — Verifier / Advisor / Consultant / Regulator +(configured via `+.machine_readable/bot_directives/echidnabot.a2ml+`). +* *Container isolation* — podman rootless with bwrap fallback; fail-safe +(refuses to run proofs without isolation). +* *Trust bridge* — 5-level confidence, SHA-256 solver-integrity +verification, axiom-usage tracking. +* *Retry + circuit breaker* — exponential backoff, opens after 5 +failures, auto-resets after 5 minutes. +* *184 tests* (137 lib + 17 lifecycle + 32 integration + 12 property +** 15 seam + 8 smoke). + +=== Install / configure / run [source,bash] ---- -git clone https://github.com/hyperpolymath/echidnabot.git -cd echidnabot +# Build (requires gitbot-fleet layout — see CONTRIBUTING.md) cargo build --release ----- -=== Database Setup - -[source,bash] ----- -# Initialize SQLite (development) +# Initialise database echidnabot init-db -# Or use PostgreSQL (production) -export DATABASE_URL=postgres://localhost/echidnabot ----- - -== Usage - -=== Server Mode (Webhook Receiver) - -[source,bash] ----- -# Set environment variables +# Start the webhook server export DATABASE_URL=sqlite:echidnabot.db export ECHIDNA_URL=http://localhost:8080 - -# Start the server echidnabot serve --port 8080 ---- -==== API Endpoints - -* `GET /` -- Service info and endpoint listing -* `GET /health` -- Health check -* `GET /graphql` -- GraphQL Playground -* `POST /graphql` -- GraphQL API for queries and mutations -* `POST /webhooks/github` -- GitHub webhook receiver -* `POST /webhooks/gitlab` -- GitLab webhook receiver -* `POST /webhooks/bitbucket` -- Bitbucket webhook receiver - -=== CLI Mode (Manual Verification) - -[source,bash] ----- -# Register a repository -echidnabot register --repo owner/name --platform github --provers lean,coq - -# Verify a specific proof file -echidnabot check --repo ./path/to/proof.lean --prover lean - -# Check status -echidnabot status --target job-uuid-here -echidnabot status --target owner/name ----- - -=== GraphQL API - -Query verification job status: - -[source,graphql] ----- -query { - verificationJob(id: "job-123") { - id - status - prover - repository - commitSha - results { - theorem - status - message - } - } -} ----- - -Submit a verification job: - -[source,graphql] ----- -mutation { - submitVerification( - repository: "owner/repo" - commitSha: "abc123" - prover: LEAN4 - files: ["src/Theorems.lean"] - ) { - id - status - } -} ----- - -== Configuration - -See `echidnabot.example.toml` for a complete configuration reference. +Full instructions: +link:wiki/Getting-Started.md[`+wiki/Getting-Started.md+`] and +link:docs/content/configuration.md[`+docs/content/configuration.md+`]. -Key environment variables: +=== Documentation map -[source,bash] ----- -# Database -DATABASE_URL=sqlite:echidnabot.db # or postgres://... - -# GitHub App -GITHUB_APP_ID=123456 -GITHUB_PRIVATE_KEY_PATH=/path/to/key.pem -GITHUB_WEBHOOK_SECRET=your-secret - -# ECHIDNA -ECHIDNA_URL=http://localhost:8080 - -# Server -PORT=8080 -RUST_LOG=info ----- - -=== Logging - -`echidnabot` emits all logs through the `tracing` ecosystem. Two output -formats are supported, selected via environment variable: - -[cols="1,1,3"] -|=== -|Env var |Value |Effect - -|`ECHIDNABOT_LOG_FORMAT` -|`text` (default) -|Human-friendly, colour-aware compact output. Suitable for local dev and -terminal sessions. - -|`ECHIDNABOT_LOG_FORMAT` -|`json` -|Structured JSON, one event per line, with span/event fields flattened -to top-level keys. Suitable for log aggregators (Loki, Elasticsearch, -CloudWatch, etc.). - -|`RUST_LOG` -|standard `tracing` filter directive -|Per-target log levels (e.g. `RUST_LOG=echidnabot=debug,axum=info`). -When unset, falls back to `info` (or `debug` when `--verbose` is passed). +[width="100%",cols="21%,79%",options="header",] |=== +|Audience |File +|Users (overview) |link:README.adoc[`+README.adoc+`] — full canonical +README -Examples: - -[source,bash] ----- -# Local development — text output, debug level for echidnabot -RUST_LOG=echidnabot=debug echidnabot serve - -# Production — JSON for log aggregators -ECHIDNABOT_LOG_FORMAT=json RUST_LOG=info echidnabot serve - -# CI / container — JSON + verbose -ECHIDNABOT_LOG_FORMAT=json RUST_LOG=debug echidnabot serve ----- - -JSON output looks roughly like: - -[source,json] ----- -{"timestamp":"2026-06-01T12:34:56.789Z","level":"INFO","fields":{"message":"Listening on http://0.0.0.0:8080"},"target":"echidnabot"} ----- - -== Deployment - -A reproducible Compose-based local + CI stack (PostgreSQL + echidnabot, -plus an optional canned-JSON ECHIDNA stub under `--profile dev`) ships -with the repo. Quickstart: - -[source,bash] ----- -cp .env.example .env && $EDITOR .env -docker compose up -d # core stack -docker compose --profile dev up -d # + echidna-server stub ----- +|Users (setup) +|link:wiki/Getting-Started.md[`+wiki/Getting-Started.md+`] -Full details — service topology, healthchecks, validation, CI integration, -and current limitations — live in link:docs/deployment.adoc[`docs/deployment.adoc`] -(closes issue #60). +|Users (config) +|link:docs/content/configuration.md[`+docs/content/configuration.md+`] -== Development +|Users (FAQ) |link:wiki/FAQ.md[`+wiki/FAQ.md+`] -=== Building and Testing +|Devs (architecture) +|link:wiki/Architecture.md[`+wiki/Architecture.md+`] -[source,bash] ----- -cargo build -cargo test # Run all 184 tests -cargo test -- --nocapture # With output ----- +|Devs (contrib) |link:CONTRIBUTING.md[`+CONTRIBUTING.md+`] -=== Architecture +|Devs (ABI/FFI) |link:ABI-FFI-README.md[`+ABI-FFI-README.md+`] -Key modules: +|Devs (roadmap) |link:ROADMAP.adoc[`+ROADMAP.adoc+`] -* `src/main.rs` -- Server entry point, CLI, webhook routes, scheduler loop -* `src/lib.rs` -- Crate root, module declarations -* `src/adapters/` -- `PlatformAdapter` trait + GitHub/GitLab/Bitbucket implementations -* `src/api/` -- GraphQL schema and webhook handlers -* `src/dispatcher/` -- ECHIDNA HTTP client, prover enumeration -* `src/scheduler/` -- Job queue, retry policy, circuit breaker, concurrency limiter -* `src/executor/` -- Container isolation (Podman + bubblewrap) -* `src/modes/` -- Bot modes (Verifier/Advisor/Consultant/Regulator) -* `src/trust/` -- Trust bridge (confidence levels, solver integrity, axiom tracking) -* `src/result_formatter.rs` -- Result formatting bridge between dispatcher and bot modes -* `src/store/` -- Database models (SQLite/PostgreSQL) -* `src/config.rs` -- Configuration system (TOML + environment) -* `src/error.rs` -- Error types +|Devs (claims) |link:EXPLAINME.adoc[`+EXPLAINME.adoc+`] — receipts +behind README claims -== Integration with Gitbot Fleet +|AI assistants |link:.claude/CLAUDE.md[`+.claude/CLAUDE.md+`] + +link:0-AI-MANIFEST.a2ml[`+0-AI-MANIFEST.a2ml+`] -echidnabot is part of the https://github.com/hyperpolymath/gitbot-fleet[Gitbot Fleet]: +|Security |link:SECURITY.md[`+SECURITY.md+`] + +link:.well-known/security.txt[`+.well-known/security.txt+`] -* **https://github.com/hyperpolymath/rhodibot[rhodibot]** -- RSR structural compliance -* **https://github.com/hyperpolymath/seambot[seambot]** -- Architectural seam hygiene -* **echidnabot** (this bot) -- Formal verification orchestration -* **https://github.com/hyperpolymath/finishingbot[finishingbot]** -- Release readiness -* **glambot** -- Presentation quality +|Releases |link:RELEASE_CHECKLIST.md[`+RELEASE_CHECKLIST.md+`] -Bots coordinate through a shared context layer managed by https://github.com/hyperpolymath/hypatia[hypatia]. - -== Security - -=== Webhook Verification - -All incoming webhooks are verified: - -* **GitHub** -- HMAC-SHA256 signature verification -* **GitLab** -- Secret token verification -* **Bitbucket** -- HMAC-SHA256 signature verification - -=== Proof Isolation - -Proof verification runs in isolated containers (see <>). - -=== Solver Integrity - -Before dispatching proofs, solver binaries can be verified against a SHA-256 manifest to detect tampering. +|Compliance |link:RSR_COMPLIANCE.adoc[`+RSR_COMPLIANCE.adoc+`] +|=== -== License +=== License -This project is licensed under MPL-2.0 (MPL-2.0). +MPL-2.0 (Palimpsest License). See link:LICENSE[`+LICENSE+`] and +link:PALIMPSEST.adoc[`+PALIMPSEST.adoc+`]. -See link:LICENSE[LICENSE] for details. +=== Contributing -**Author:** Jonathan D.A. Jewell +See link:CONTRIBUTING.md[`+CONTRIBUTING.md+`] and +link:CODE_OF_CONDUCT.md[`+CODE_OF_CONDUCT.md+`]. -== Contributing +=== Security -Contributions welcome! Please see link:CONTRIBUTING.adoc[CONTRIBUTING.adoc] for guidelines. +Vulnerabilities → link:SECURITY.md[`+SECURITY.md+`]. *Do not* open +public issues for security reports. -== Security +''''' -For security issues, please see link:SECURITY.md[SECURITY.md]. +*Maintainer:* Jonathan D.A. Jewell — +https://github.com/hyperpolymath[hyperpolymath] diff --git a/README.md b/README.md deleted file mode 100644 index 17ac512..0000000 --- a/README.md +++ /dev/null @@ -1,116 +0,0 @@ - -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (hyperpolymath) ---> - -# echidnabot — Proof-Aware CI Bot - -[![Sponsor](https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github)](https://github.com/sponsors/hyperpolymath) -[![License: PMPL-1.0](https://img.shields.io/badge/License-MPL--2.0-blue.svg)](https://github.com/hyperpolymath/palimpsest-license) -[![GitHub Release](https://img.shields.io/github/v/release/hyperpolymath/echidnabot?include_prereleases)](https://github.com/hyperpolymath/echidnabot/releases) - -> **The canonical README is [`README.adoc`](README.adoc).** This Markdown -> file exists for renderers that prefer `.md` (some package indexes, some -> doc tooling); it is a thin summary that links into the AsciiDoc -> version for the full story. - ---- - -## What is it? - -A formal-verification CI bot that orchestrates the -[ECHIDNA](https://github.com/hyperpolymath/echidna) theorem-proving -platform for automatic proof verification on every push and pull -request. Written in Rust on Tokio/Axum. - -Part of the [gitbot-fleet](https://github.com/hyperpolymath/gitbot-fleet) -(Tier-1 Verifier role), coordinated by -[Hypatia](https://github.com/hyperpolymath/hypatia). - -## Why does it exist? - -You're writing formally verified software — proofs in Coq, Lean, Agda, -or Isabelle. But your CI pipeline doesn't understand proofs: - -- Tests pass, but **proofs are broken**. -- PRs merge with **unverified theorems**. -- No one notices until a dependent build fails. -- Manual verification is **slow and error-prone**. - -echidnabot bridges the gap. Push proof files; get verified. - -## Features (high-level) - -- **12 provers via ECHIDNA** — Coq, Lean 4, Agda, Isabelle/HOL, Z3, - CVC5, Metamath, HOL Light, Mizar, PVS, ACL2, HOL4 - (see [`wiki/Supported-Provers.md`](wiki/Supported-Provers.md); - upstream supports 113, drift documented in - [`EXPLAINME.adoc`](EXPLAINME.adoc)). -- **3 platforms** — GitHub, GitLab, Bitbucket (Codeberg planned). -- **4 bot modes** — Verifier / Advisor / Consultant / Regulator - (configured via `.machine_readable/bot_directives/echidnabot.a2ml`). -- **Container isolation** — podman rootless with bwrap fallback; - fail-safe (refuses to run proofs without isolation). -- **Trust bridge** — 5-level confidence, SHA-256 solver-integrity - verification, axiom-usage tracking. -- **Retry + circuit breaker** — exponential backoff, opens after - 5 failures, auto-resets after 5 minutes. -- **184 tests** (137 lib + 17 lifecycle + 32 integration + 12 property - + 15 seam + 8 smoke). - -## Install / configure / run - -```bash -# Build (requires gitbot-fleet layout — see CONTRIBUTING.md) -cargo build --release - -# Initialise database -echidnabot init-db - -# Start the webhook server -export DATABASE_URL=sqlite:echidnabot.db -export ECHIDNA_URL=http://localhost:8080 -echidnabot serve --port 8080 -``` - -Full instructions: [`wiki/Getting-Started.md`](wiki/Getting-Started.md) -and [`docs/content/configuration.md`](docs/content/configuration.md). - -## Documentation map - -| Audience | File | -| ------------------ | --------------------------------------------------------------------- | -| Users (overview) | [`README.adoc`](README.adoc) — full canonical README | -| Users (setup) | [`wiki/Getting-Started.md`](wiki/Getting-Started.md) | -| Users (config) | [`docs/content/configuration.md`](docs/content/configuration.md) | -| Users (FAQ) | [`wiki/FAQ.md`](wiki/FAQ.md) | -| Devs (architecture)| [`wiki/Architecture.md`](wiki/Architecture.md) | -| Devs (contrib) | [`CONTRIBUTING.md`](CONTRIBUTING.md) | -| Devs (ABI/FFI) | [`ABI-FFI-README.md`](ABI-FFI-README.md) | -| Devs (roadmap) | [`ROADMAP.adoc`](ROADMAP.adoc) | -| Devs (claims) | [`EXPLAINME.adoc`](EXPLAINME.adoc) — receipts behind README claims | -| AI assistants | [`.claude/CLAUDE.md`](.claude/CLAUDE.md) + [`0-AI-MANIFEST.a2ml`](0-AI-MANIFEST.a2ml) | -| Security | [`SECURITY.md`](SECURITY.md) + [`.well-known/security.txt`](.well-known/security.txt) | -| Releases | [`RELEASE_CHECKLIST.md`](RELEASE_CHECKLIST.md) | -| Compliance | [`RSR_COMPLIANCE.adoc`](RSR_COMPLIANCE.adoc) | - -## License - -MPL-2.0 (Palimpsest License). See [`LICENSE`](LICENSE) and -[`PALIMPSEST.adoc`](PALIMPSEST.adoc). - -## Contributing - -See [`CONTRIBUTING.md`](CONTRIBUTING.md) and -[`CODE_OF_CONDUCT.md`](CODE_OF_CONDUCT.md). - -## Security - -Vulnerabilities → [`SECURITY.md`](SECURITY.md). **Do not** open public -issues for security reports. - ---- - -**Maintainer:** Jonathan D.A. Jewell — -[hyperpolymath](https://github.com/hyperpolymath) diff --git a/RELEASE_CHECKLIST.adoc b/RELEASE_CHECKLIST.adoc new file mode 100644 index 0000000..899a993 --- /dev/null +++ b/RELEASE_CHECKLIST.adoc @@ -0,0 +1,281 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2025-2026 +Jonathan D.A. Jewell (hyperpolymath) –> + +== echidnabot Release Checklist + +Procedure for cutting a release of echidnabot, plus standing checklist +of items that should already be in place before any release ships. + +*Current target:* v0.2.0 (production hardening — observability, +deployment automation; see link:ROADMAP.adoc[`+ROADMAP.adoc+`] +"`Remaining Work`"). + +*Last reviewed:* 2026-06-01 + +=== Repository Setup + +==== Done + +* [x] README.adoc - SEO-optimized, project-focused +* [x] BRANDING.md - Visual identity and LLM art prompts +* [x] Justfile - RSR canonical task runner +* [x] Nickel configuration (config/echidnabot.ncl) +* [x] MCP configuration (.claude/settings/mcp.json) +* [x] STATE.a2ml - Project checkpoint +* [x] META.a2ml - Dublin Core metadata +* [x] ECOSYSTEM.a2ml - Dependency graph +* [x] GitHub topics file (.github/topics.txt) + +==== To Apply Manually + +* [ ] *Apply GitHub Topics* - Go to repo Settings → About → Topics and +add: ++ +.... +theorem-prover, formal-verification, proof-assistant, ci-cd, rust, coq, +lean4, agda, isabelle, z3, smt, formal-methods, type-theory, github-app, +automation, mathematics, logic, webhooks, hacktoberfest +.... +* [ ] *Update GitHub Description* - Set to: > Proof-aware CI bot that +verifies mathematical theorems on every push. Coq, Lean, Agda, Isabelle, +Z3 support. Rust + Tokio + GraphQL. + +=== Wiki ✅ + +==== Done + +* [x] wiki/Home.md +* [x] wiki/Getting-Started.md +* [x] wiki/Architecture.md +* [x] wiki/Supported-Provers.md +* [x] wiki/FAQ.md + +==== To Add + +* [ ] wiki/Configuration-Reference.md - All config options +* [ ] wiki/API-Reference.md - GraphQL schema documentation +* [ ] wiki/Platform-Integration.md - GitHub/GitLab/Bitbucket setup +* [ ] wiki/Troubleshooting.md - Common issues +* [ ] wiki/Changelog.md - Version history +* [ ] wiki/Roadmap.md - Future plans + +==== To Do Manually + +* [ ] *Enable Wiki* in GitHub repo settings +* [ ] *Push wiki/* to the wiki repo: ++ +[source,bash] +---- +git clone https://github.com/hyperpolymath/echidnabot.wiki.git +cp wiki/*.md echidnabot.wiki/ +cd echidnabot.wiki && git add . && git commit -m "Initial wiki" && git push +---- + +=== CI/CD ✅ + +==== Done + +* [x] .github/workflows/quality.yml - Rust build/test/lint +* [x] .github/workflows/docs.yml - casket-ssg documentation +* [x] .github/workflows/echidnabot.yml - Self-referential proof checking +* [x] .github/workflows/codeql.yml - Security scanning +* [x] .github/workflows/scorecard.yml - OSSF Scorecard + +==== To Add/Verify + +* [ ] Ensure all workflows pass on main branch +* [ ] Add release workflow for crates.io publishing +* [ ] Add container publishing to ghcr.io + +=== Documentation + +==== Done + +* [x] README.adoc + README.md (Markdown summary linking into .adoc) +* [x] EXPLAINME.adoc — receipts behind README claims +* [x] ROADMAP.adoc — phases + completion +* [x] CONTRIBUTING.md +* [x] SECURITY.md +* [x] CODE_OF_CONDUCT.md +* [x] MAINTAINERS.adoc +* [x] CHANGELOG.md (auto-generated from conventional commits) +* [x] CITATION.cff + codemeta.json +* [x] ABI-FFI-README.md — Zig FFI + Idris2 ABI boundary +* [x] 0-AI-MANIFEST.a2ml + .claude/CLAUDE.md — AI assistant pointers +* [x] RSR_OUTLINE.adoc + RSR_COMPLIANCE.adoc +* [x] docs/content/\{index,getting-started,configuration,api}.md +(casket-ssg) + +==== To Add + +* [ ] docs/DEPLOYMENT.md — Production deployment guide (k8s, helm, +docker-compose) +* [ ] Man pages (docs/man/echidnabot.1) via Mustfile recipe + +=== Branding Assets 📝 + +==== To Create (using LLM prompts in BRANDING.md) + +* [ ] *Avatar* (512x512) - Geometric echidna logo +* [ ] *Banner* (1280x640) - GitHub social preview +* [ ] *Favicon* (32x32, 16x16) - For docs site + +==== To Apply + +* [ ] Upload avatar to GitHub org/repo +* [ ] Set social preview image in repo settings +* [ ] Add favicon to docs site + +=== Code Quality 🔄 + +==== To Complete + +* [ ] Run `+cargo fmt+` on all files +* [ ] Run `+cargo clippy+` and fix all warnings +* [ ] Achieve 50%+ test coverage +* [ ] Add integration tests +* [ ] Run `+cargo audit+` and fix vulnerabilities +* [ ] Run `+cargo deny check+` for license compliance + +=== Core Functionality + +==== Phase 1 (MVP) — landed in v0.1.0 + +* [x] GitHub webhook handler with signature verification (HMAC-SHA256) +* [x] GitLab + Bitbucket webhook handlers +* [x] Proof file detection (by extension across 7 file types) +* [x] ECHIDNA Core dispatcher client (REST + GraphQL) +* [x] GitHub Check Run reporter +* [x] SQLite + PostgreSQL persistence +* [x] CLI: `+serve+`, `+register+`, `+check+`, `+status+`, `+init-db+` + +==== Phase 2 (Multi-Prover) — landed in v0.1.0 + +* [x] Auto-detect prover from file extension +* [x] 12-prover surface (Coq, Lean 4, Agda, Isabelle, Z3, CVC5, +Metamath, HOL Light, Mizar, PVS, ACL2, HOL4) +* [x] `+ProverKind+` slug newtype — open-ended for 113 upstream provers +* [x] Parallel proof checking (semaphore-bounded) +* [x] Aggregated results + +==== Phase 3 (Hardening) — see ROADMAP.adoc + +* [x] Container isolation (podman + bwrap, fail-safe) +* [x] Retry + circuit breaker (5-failures-then-open, 5-min reset) +* [x] Trust bridge (confidence levels, solver integrity, axiom tracking) +* [x] Per-IP webhook rate limiting +* [x] Prometheus `+/metrics+` endpoint +* [x] Double-loop feedback (tactic-outcome recording + corpus delta) +* [ ] OpenTelemetry distributed tracing +* [ ] Structured JSON logging end-to-end +* [ ] Graceful shutdown (finish in-progress jobs before exit) + +=== Security ✅ + +==== Done + +* [x] SECURITY.md policy +* [x] .well-known/security.txt +* [x] HMAC-SHA256 webhook verification (code exists) +* [x] No hardcoded secrets +* [x] SHA-pinned GitHub Actions + +==== To Verify + +* [ ] Run TruffleHog scan: no secrets in history +* [ ] Run CodeQL: no critical findings +* [ ] OSSF Scorecard: 7+ score + +=== Packaging 🔄 + +==== Done + +* [x] Cargo.toml metadata complete +* [x] guix.scm package definition +* [x] Containerfile for Docker/Podman +* [x] Justfile for task automation + +==== To Add + +* [ ] cargo-deb configuration +* [ ] cargo-rpm configuration +* [ ] Homebrew formula (optional) + +(Guix flake intentionally NOT planned: guix is deprecated estate-wide as +of 2026-06-01.) + +=== Release Process + +==== Pre-Release + +[arabic] +. ☐ All tests passing +. ☐ Changelog updated +. ☐ Version bumped in Cargo.toml +. ☐ STATE.a2ml updated +. ☐ Documentation reviewed + +==== Release + +[arabic] +. ☐ Create git tag: `+git tag -s v0.1.0 -m "Release 0.1.0"+` +. ☐ Push tag: `+git push origin v0.1.0+` +. ☐ GitHub release created with notes +. ☐ Publish to crates.io: `+cargo publish+` +. ☐ Container pushed to ghcr.io +. ☐ Announce on relevant channels + +==== Post-Release + +[arabic] +. ☐ Verify crates.io page +. ☐ Verify container works +. ☐ Update roadmap +. ☐ Start next milestone + +=== External Integration + +==== GitHub + +* [ ] Enable GitHub Discussions +* [ ] Set up issue templates (if not present) +* [ ] Configure branch protection rules +* [ ] Enable Dependabot + +==== Marketing + +* [ ] Post to Hacker News (when ready) +* [ ] Post to r/rust, r/programming +* [ ] Post to Coq, Lean, Agda communities +* [ ] Add to Awesome lists (awesome-rust, etc.) + +=== Metrics + +==== Success Criteria for v1.0 + +* [ ] 100+ GitHub stars +* [ ] 5+ external contributors +* [ ] 3+ production users +* [ ] 80%+ test coverage +* [ ] OSSF Scorecard 8+ + +''''' + +=== Priority Order + +[arabic] +. *Immediate* (before merge) +* Apply GitHub topics manually +* Update GitHub description +* Enable wiki and push content +. *This Week* +* Create branding assets +* Add missing wiki pages +* Complete Phase 1 functionality +. *This Month* +* Achieve MVP release (v0.2) +* 50% test coverage +. *Next Quarter* +* v1.0 production release +* Multi-platform support +* ML tactic suggestions diff --git a/RELEASE_CHECKLIST.md b/RELEASE_CHECKLIST.md deleted file mode 100644 index f2b636e..0000000 --- a/RELEASE_CHECKLIST.md +++ /dev/null @@ -1,250 +0,0 @@ - -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (hyperpolymath) ---> - -# echidnabot Release Checklist - -Procedure for cutting a release of echidnabot, plus standing checklist -of items that should already be in place before any release ships. - -**Current target:** v0.2.0 (production hardening — observability, -deployment automation; see [`ROADMAP.adoc`](ROADMAP.adoc) "Remaining -Work"). - -**Last reviewed:** 2026-06-01 - -## Repository Setup - -### Done -- [x] README.adoc - SEO-optimized, project-focused -- [x] BRANDING.md - Visual identity and LLM art prompts -- [x] Justfile - RSR canonical task runner -- [x] Nickel configuration (config/echidnabot.ncl) -- [x] MCP configuration (.claude/settings/mcp.json) -- [x] STATE.a2ml - Project checkpoint -- [x] META.a2ml - Dublin Core metadata -- [x] ECOSYSTEM.a2ml - Dependency graph -- [x] GitHub topics file (.github/topics.txt) - -### To Apply Manually -- [ ] **Apply GitHub Topics** - Go to repo Settings → About → Topics and add: - ``` - theorem-prover, formal-verification, proof-assistant, ci-cd, rust, coq, - lean4, agda, isabelle, z3, smt, formal-methods, type-theory, github-app, - automation, mathematics, logic, webhooks, hacktoberfest - ``` -- [ ] **Update GitHub Description** - Set to: - > Proof-aware CI bot that verifies mathematical theorems on every push. Coq, Lean, Agda, Isabelle, Z3 support. Rust + Tokio + GraphQL. - -## Wiki ✅ - -### Done -- [x] wiki/Home.md -- [x] wiki/Getting-Started.md -- [x] wiki/Architecture.md -- [x] wiki/Supported-Provers.md -- [x] wiki/FAQ.md - -### To Add -- [ ] wiki/Configuration-Reference.md - All config options -- [ ] wiki/API-Reference.md - GraphQL schema documentation -- [ ] wiki/Platform-Integration.md - GitHub/GitLab/Bitbucket setup -- [ ] wiki/Troubleshooting.md - Common issues -- [ ] wiki/Changelog.md - Version history -- [ ] wiki/Roadmap.md - Future plans - -### To Do Manually -- [ ] **Enable Wiki** in GitHub repo settings -- [ ] **Push wiki/** to the wiki repo: - ```bash - git clone https://github.com/hyperpolymath/echidnabot.wiki.git - cp wiki/*.md echidnabot.wiki/ - cd echidnabot.wiki && git add . && git commit -m "Initial wiki" && git push - ``` - -## CI/CD ✅ - -### Done -- [x] .github/workflows/quality.yml - Rust build/test/lint -- [x] .github/workflows/docs.yml - casket-ssg documentation -- [x] .github/workflows/echidnabot.yml - Self-referential proof checking -- [x] .github/workflows/codeql.yml - Security scanning -- [x] .github/workflows/scorecard.yml - OSSF Scorecard - -### To Add/Verify -- [ ] Ensure all workflows pass on main branch -- [ ] Add release workflow for crates.io publishing -- [ ] Add container publishing to ghcr.io - -## Documentation - -### Done -- [x] README.adoc + README.md (Markdown summary linking into .adoc) -- [x] EXPLAINME.adoc — receipts behind README claims -- [x] ROADMAP.adoc — phases + completion -- [x] CONTRIBUTING.md -- [x] SECURITY.md -- [x] CODE_OF_CONDUCT.md -- [x] MAINTAINERS.adoc -- [x] CHANGELOG.md (auto-generated from conventional commits) -- [x] CITATION.cff + codemeta.json -- [x] ABI-FFI-README.md — Zig FFI + Idris2 ABI boundary -- [x] 0-AI-MANIFEST.a2ml + .claude/CLAUDE.md — AI assistant pointers -- [x] RSR_OUTLINE.adoc + RSR_COMPLIANCE.adoc -- [x] docs/content/{index,getting-started,configuration,api}.md (casket-ssg) - -### To Add -- [ ] docs/DEPLOYMENT.md — Production deployment guide (k8s, helm, docker-compose) -- [ ] Man pages (docs/man/echidnabot.1) via Mustfile recipe - -## Branding Assets 📝 - -### To Create (using LLM prompts in BRANDING.md) -- [ ] **Avatar** (512x512) - Geometric echidna logo -- [ ] **Banner** (1280x640) - GitHub social preview -- [ ] **Favicon** (32x32, 16x16) - For docs site - -### To Apply -- [ ] Upload avatar to GitHub org/repo -- [ ] Set social preview image in repo settings -- [ ] Add favicon to docs site - -## Code Quality 🔄 - -### To Complete -- [ ] Run `cargo fmt` on all files -- [ ] Run `cargo clippy` and fix all warnings -- [ ] Achieve 50%+ test coverage -- [ ] Add integration tests -- [ ] Run `cargo audit` and fix vulnerabilities -- [ ] Run `cargo deny check` for license compliance - -## Core Functionality - -### Phase 1 (MVP) — landed in v0.1.0 -- [x] GitHub webhook handler with signature verification (HMAC-SHA256) -- [x] GitLab + Bitbucket webhook handlers -- [x] Proof file detection (by extension across 7 file types) -- [x] ECHIDNA Core dispatcher client (REST + GraphQL) -- [x] GitHub Check Run reporter -- [x] SQLite + PostgreSQL persistence -- [x] CLI: `serve`, `register`, `check`, `status`, `init-db` - -### Phase 2 (Multi-Prover) — landed in v0.1.0 -- [x] Auto-detect prover from file extension -- [x] 12-prover surface (Coq, Lean 4, Agda, Isabelle, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2, HOL4) -- [x] `ProverKind` slug newtype — open-ended for 113 upstream provers -- [x] Parallel proof checking (semaphore-bounded) -- [x] Aggregated results - -### Phase 3 (Hardening) — see ROADMAP.adoc -- [x] Container isolation (podman + bwrap, fail-safe) -- [x] Retry + circuit breaker (5-failures-then-open, 5-min reset) -- [x] Trust bridge (confidence levels, solver integrity, axiom tracking) -- [x] Per-IP webhook rate limiting -- [x] Prometheus `/metrics` endpoint -- [x] Double-loop feedback (tactic-outcome recording + corpus delta) -- [ ] OpenTelemetry distributed tracing -- [ ] Structured JSON logging end-to-end -- [ ] Graceful shutdown (finish in-progress jobs before exit) - -## Security ✅ - -### Done -- [x] SECURITY.md policy -- [x] .well-known/security.txt -- [x] HMAC-SHA256 webhook verification (code exists) -- [x] No hardcoded secrets -- [x] SHA-pinned GitHub Actions - -### To Verify -- [ ] Run TruffleHog scan: no secrets in history -- [ ] Run CodeQL: no critical findings -- [ ] OSSF Scorecard: 7+ score - -## Packaging 🔄 - -### Done -- [x] Cargo.toml metadata complete -- [x] guix.scm package definition -- [x] Containerfile for Docker/Podman -- [x] Justfile for task automation - -### To Add -- [ ] cargo-deb configuration -- [ ] cargo-rpm configuration -- [ ] Homebrew formula (optional) - -(Guix flake intentionally NOT planned: guix is deprecated estate-wide -as of 2026-06-01.) - -## Release Process - -### Pre-Release -1. [ ] All tests passing -2. [ ] Changelog updated -3. [ ] Version bumped in Cargo.toml -4. [ ] STATE.a2ml updated -5. [ ] Documentation reviewed - -### Release -1. [ ] Create git tag: `git tag -s v0.1.0 -m "Release 0.1.0"` -2. [ ] Push tag: `git push origin v0.1.0` -3. [ ] GitHub release created with notes -4. [ ] Publish to crates.io: `cargo publish` -5. [ ] Container pushed to ghcr.io -6. [ ] Announce on relevant channels - -### Post-Release -1. [ ] Verify crates.io page -2. [ ] Verify container works -3. [ ] Update roadmap -4. [ ] Start next milestone - -## External Integration - -### GitHub -- [ ] Enable GitHub Discussions -- [ ] Set up issue templates (if not present) -- [ ] Configure branch protection rules -- [ ] Enable Dependabot - -### Marketing -- [ ] Post to Hacker News (when ready) -- [ ] Post to r/rust, r/programming -- [ ] Post to Coq, Lean, Agda communities -- [ ] Add to Awesome lists (awesome-rust, etc.) - -## Metrics - -### Success Criteria for v1.0 -- [ ] 100+ GitHub stars -- [ ] 5+ external contributors -- [ ] 3+ production users -- [ ] 80%+ test coverage -- [ ] OSSF Scorecard 8+ - ---- - -## Priority Order - -1. **Immediate** (before merge) - - Apply GitHub topics manually - - Update GitHub description - - Enable wiki and push content - -2. **This Week** - - Create branding assets - - Add missing wiki pages - - Complete Phase 1 functionality - -3. **This Month** - - Achieve MVP release (v0.2) - - 50% test coverage - -4. **Next Quarter** - - v1.0 production release - - Multi-platform support - - ML tactic suggestions diff --git a/SECURITY.adoc b/SECURITY.adoc new file mode 100644 index 0000000..ee9b120 --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,80 @@ +== Security Policy + +=== Supported Versions + +The following versions of echidnabot are currently supported with +security updates: + +[cols=",",options="header",] +|=== +|Version |Supported +|0.1.x |:white_check_mark: +|=== + +=== Reporting a Vulnerability + +We take security seriously. If you discover a security vulnerability in +echidnabot, please report it responsibly: + +==== How to Report + +[arabic] +. *Email*: Send details to security@hyperpolymath.org +. *Encryption*: Use our GPG key at +https://hyperpolymath.org/gpg/security.asc +. *Do NOT* open a public GitHub issue for security vulnerabilities + +==== What to Include + +* Description of the vulnerability +* Steps to reproduce +* Potential impact assessment +* Suggested fix (if any) + +==== Response Timeline + +* *Initial acknowledgment*: Within 48 hours +* *Status update*: Within 7 days +* *Resolution target*: Within 30 days for critical issues + +==== What to Expect + +* If the vulnerability is accepted, we will: +** Work on a fix and coordinate disclosure timing with you +** Credit you in the security advisory (unless you prefer anonymity) +** Release a patched version as soon as practical +* If the vulnerability is declined, we will: +** Provide a clear explanation of why +** Suggest alternative resources if applicable + +=== Security Measures + +echidnabot implements the following security measures: + +* *Webhook Verification*: HMAC-SHA256 signature verification for all +webhooks +* *Least-Privilege Access*: Read-only repository access for cloning, +minimal write access for check runs +* *Sandboxed Execution*: echidnabot delegates proof verification to +ECHIDNA Core; it never executes provers directly +* *Secrets Management*: Integration with Vault/SOPS for secure secret +handling +* *No Weak Cryptography*: SHA-256+ only; no MD5 or SHA-1 for security +purposes +* *TLS Everywhere*: All external communications use HTTPS/TLS + +=== Security Scanning + +This project uses: - CodeQL for static analysis - TruffleHog for secret +detection - OpenSSF Scorecard for security metrics - ClusterFuzzLite for +fuzzing + +=== References + +* link:.well-known/security.txt[security.txt] +* link:wiki/Architecture.md[Architecture (wiki)] — Security model +section +* CODE_OF_CONDUCT.md +* MAINTAINERS.adoc — disclosure contacts +* https://github.com/hyperpolymath/standards[hyperpolymath/standards] — +estate-wide security policy diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index 65949c2..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,74 +0,0 @@ - -# Security Policy - -## Supported Versions - -The following versions of echidnabot are currently supported with security updates: - -| Version | Supported | -| ------- | ------------------ | -| 0.1.x | :white_check_mark: | - -## Reporting a Vulnerability - -We take security seriously. If you discover a security vulnerability in echidnabot, please report it responsibly: - -### How to Report - -1. **Email**: Send details to security@hyperpolymath.org -2. **Encryption**: Use our GPG key at https://hyperpolymath.org/gpg/security.asc -3. **Do NOT** open a public GitHub issue for security vulnerabilities - -### What to Include - -- Description of the vulnerability -- Steps to reproduce -- Potential impact assessment -- Suggested fix (if any) - -### Response Timeline - -- **Initial acknowledgment**: Within 48 hours -- **Status update**: Within 7 days -- **Resolution target**: Within 30 days for critical issues - -### What to Expect - -- If the vulnerability is accepted, we will: - - Work on a fix and coordinate disclosure timing with you - - Credit you in the security advisory (unless you prefer anonymity) - - Release a patched version as soon as practical - -- If the vulnerability is declined, we will: - - Provide a clear explanation of why - - Suggest alternative resources if applicable - -## Security Measures - -echidnabot implements the following security measures: - -- **Webhook Verification**: HMAC-SHA256 signature verification for all webhooks -- **Least-Privilege Access**: Read-only repository access for cloning, minimal write access for check runs -- **Sandboxed Execution**: echidnabot delegates proof verification to ECHIDNA Core; it never executes provers directly -- **Secrets Management**: Integration with Vault/SOPS for secure secret handling -- **No Weak Cryptography**: SHA-256+ only; no MD5 or SHA-1 for security purposes -- **TLS Everywhere**: All external communications use HTTPS/TLS - -## Security Scanning - -This project uses: -- CodeQL for static analysis -- TruffleHog for secret detection -- OpenSSF Scorecard for security metrics -- ClusterFuzzLite for fuzzing - -## References - -- [security.txt](.well-known/security.txt) -- [Architecture (wiki)](wiki/Architecture.md) — Security model section -- [CODE_OF_CONDUCT.md](CODE_OF_CONDUCT.md) -- [MAINTAINERS.adoc](MAINTAINERS.adoc) — disclosure contacts -- [hyperpolymath/standards](https://github.com/hyperpolymath/standards) — estate-wide security policy diff --git a/SESSION_SUMMARY_2026-01-29.adoc b/SESSION_SUMMARY_2026-01-29.adoc new file mode 100644 index 0000000..7c25326 --- /dev/null +++ b/SESSION_SUMMARY_2026-01-29.adoc @@ -0,0 +1,434 @@ +== echidnabot Session Summary - 2026-01-29 + +=== Overview + +This session focused on bringing echidnabot up to the same comprehensive +documentation standard as ECHIDNA v1.3.0, fixing build issues, and +establishing the roadmap for production readiness. + +''''' + +=== Accomplishments + +==== 1. Build System Fixes ✓ + +*Problem:* Repository had deleted source files and build errors - +`+src/main.rs+` deleted but still referenced in Cargo.toml - +`+src/api/graphql.rs+`, `+src/dispatcher/echidna_client.rs+`, +`+src/store/sqlite.rs+` also deleted - Build failed with missing file +errors + +*Solution:* + +[source,bash] +---- +git restore src/main.rs src/api/graphql.rs src/dispatcher/echidna_client.rs src/store/sqlite.rs +cargo clean && cargo build +---- + +*Result:* Clean build with 0 errors, all 7 unit tests passing + +==== 2. Author Attribution Fix ✓ + +*Problem:* Cargo.toml had incorrect author email + +[source,toml] +---- +authors = ["Jonathan D.A. Jewell "] # WRONG +---- + +*Solution:* + +[source,toml] +---- +authors = ["Jonathan D.A. Jewell "] # CORRECT +---- + +*Compliance:* Follows CRITICAL attribution requirements from global +CLAUDE.md + +==== 3. Comprehensive META.scm ✓ + +Created comprehensive architecture documentation with *8 Architecture +Decision Records (ADRs)*: + +[width="100%",cols="25%,35%,40%",options="header",] +|=== +|ADR |Title |Status +|ADR-001 |Multi-Platform Adapter Pattern |Accepted +|ADR-002 |GraphQL API for Job Management |Accepted +|ADR-003 |PostgreSQL for Job Queue and State |Accepted +|ADR-004 |Webhook-Driven Architecture |Accepted +|ADR-005 |Integration with ECHIDNA Core |Accepted +|ADR-006 |Container Isolation for Proof Verification |Accepted +|ADR-007 |Multi-Prover Support via ECHIDNA |Accepted +|ADR-008 |Bot Modes: Verifier/Advisor/Consultant/Regulator |Accepted +|=== + +*Key Decisions:* - *Platform Abstraction:* `+PlatformAdapter+` trait for +GitHub/GitLab/Bitbucket - *API Choice:* async-graphql for type-safe, +self-documenting API - *Database:* PostgreSQL with sqlx compile-time +query checking - *Security:* Docker container isolation with resource +limits - *Integration:* HTTP client to ECHIDNA API (clear separation of +concerns) + +==== 4. Comprehensive ECOSYSTEM.scm ✓ + +Documented echidnabot’s position in the formal verification ecosystem: + +*Relationships:* - *Core Dependency:* ECHIDNA (required backend for 12 +prover verification) - *Code Platforms:* GitHub, GitLab, Bitbucket +(webhook integration) - *Theorem Provers:* All 12 supported by ECHIDNA +(Coq, Lean, Isabelle, Agda, Z3, CVC5, Metamath, HOL Light, PVS, ACL2, +HOL4, Mizar) - *Rust Ecosystem:* Tokio, Axum, async-graphql, sqlx, +reqwest, octocrab - *Gitbot Fleet:* rhodibot, seambot, finishingbot, +glambot (coordinated via hypatia) + +*Position Statement:* > echidnabot bridges code hosting platforms +(GitHub, GitLab, Bitbucket) and the ECHIDNA neurosymbolic theorem +prover. It acts as a CI/CD orchestrator for formal verification, +automatically checking proofs on every push and PR. + +==== 5. Comprehensive STATE.scm ✓ + +*Current Progress: 75% Complete* + +*Completed Milestones (3/7):* 1. ✅ Core Infrastructure (100%) - Axum +server, webhooks, database, GraphQL 2. ✅ Platform Integration (100%) - +GitHub/GitLab/Bitbucket adapters 3. ✅ ECHIDNA Integration (100%) - HTTP +client, job dispatch, result parsing + +*In Progress (1/7):* 4. 🔄 Job Scheduler and Queue (60%) - Basic queue +works, need retry logic + concurrency limits + +*Planned (3/7):* 5. 📋 Container Isolation (0%) - Docker spawning, +resource limits, network isolation 6. 📋 Bot Modes Implementation (0%) - +Verifier/Advisor/Consultant/Regulator 7. 📋 Production Hardening (0%) - +Error recovery, observability, rate limiting + +*Working Features:* - ✅ HTTP server with health checks - ✅ Webhook +receivers for GitHub/GitLab/Bitbucket with signature verification - ✅ +Platform adapter abstraction for multi-platform support - ✅ GraphQL API +for job queries and mutations - ✅ PostgreSQL database with sqlx +migrations - ✅ Integration with ECHIDNA API for proof verification - ✅ +Repository registration and configuration - ✅ Job status tracking + +''''' + +=== Critical Next Actions + +==== Immediate (This Week) + +[arabic] +. *Container Isolation (High Priority - Security)* +* Implement Docker container spawning for proof verification +* Add resource limits (CPU, memory, timeout) +* Read-only filesystem setup +* Network isolation +* *Why Critical:* Without isolation, running untrusted code from PRs is +a security risk +. *Retry Logic with Backoff (High Priority - Reliability)* +* Add exponential backoff for failed jobs +* Distinguish transient vs permanent failures +* Configurable retry limits +* *Why Critical:* Temporary failures (network issues, ECHIDNA busy) +currently become permanent +. *Concurrent Job Execution Limits (High Priority - Stability)* +* Implement job concurrency limits +* Priority queue for urgent jobs +* Fair scheduling across repositories +* *Why Critical:* Unlimited concurrency can exhaust resources + +==== This Week + +[arabic, start=4] +. *Verifier Mode Implementation* +* Silent pass/fail checks (basic bot mode) +* Check run / commit status creation +* Basic PR comments on failure +* *First bot mode to implement* (simplest, highest value) +. *Docker Compose Setup* +* PostgreSQL + echidnabot + ECHIDNA in one command +* Easy local development +* Production-like environment +. *Integration Tests* +* End-to-end webhook → verification → result flow +* Test with real GitHub webhook payloads +* Mock ECHIDNA API responses + +==== This Month + +[arabic, start=7] +. *Advisor Mode* - Tactic suggestions via ECHIDNA ML on proof failure +. *Observability* - Prometheus metrics, OpenTelemetry tracing +. *Pre-Built Prover Images* - Docker images for all 12 provers +. *Regulator Mode* - PR merge blocking when proofs fail +. *Production Deployment Guide* - Kubernetes, security hardening +. *GitHub App Distribution* - Easy installation for users + +''''' + +=== Architecture Overview + +.... +┌─────────────────────────────────────────────────────────────┐ +│ GitHub / GitLab / Bitbucket │ +│ (Push, PR events) │ +└────────────────────────┬────────────────────────────────────┘ + │ Webhooks (verified HMAC) + ▼ +┌─────────────────────────────────────────────────────────────┐ +│ echidnabot │ +│ ┌──────────────┐ ┌──────────────┐ ┌──────────────┐ │ +│ │ Webhook │ │ GraphQL │ │ Platform │ │ +│ │ Receivers │ │ API │ │ Adapters │ │ +│ └──────────────┘ └──────────────┘ └──────────────┘ │ +│ │ +│ ┌──────────────────────────────────────────────────┐ │ +│ │ Job Scheduler & Queue │ │ +│ │ (PostgreSQL persistence) │ │ +│ └──────────────────────────────────────────────────┘ │ +│ │ │ +│ │ HTTP API calls │ +│ ▼ │ +│ ┌──────────────────────┐ │ +│ │ Container Spawner │ │ +│ │ (Docker isolation) │ │ +│ └──────────────────────┘ │ +└──────────────────────┬──────────────────────────────────────┘ + │ HTTP to ECHIDNA + ▼ +┌─────────────────────────────────────────────────────────────┐ +│ ECHIDNA Core │ +│ ┌─────────────┐ ┌─────────────┐ ┌─────────────┐ │ +│ │ Julia ML │ │ Rust │ │ 12 Prover │ │ +│ │ Backend │ │ Backend │ │ Backends │ │ +│ └─────────────┘ └─────────────┘ └─────────────┘ │ +└─────────────────────────────────────────────────────────────┘ + │ Verification results + ▼ +┌─────────────────────────────────────────────────────────────┐ +│ GitHub Check Runs / PR Comments │ +│ GitLab Commit Statuses / MR Notes │ +│ Bitbucket Build Statuses / PR Comments │ +└─────────────────────────────────────────────────────────────┘ +.... + +''''' + +=== Technology Stack + +[width="100%",cols="26%,42%,32%",options="header",] +|=== +|Layer |Technology |Purpose +|*Runtime* |Rust 1.75+ |Memory-safe systems programming + +|*Async* |Tokio |Async runtime for concurrent webhook handling + +|*Web* |Axum 0.8 |Ergonomic web framework for HTTP/webhooks + +|*API* |async-graphql 7 |Type-safe GraphQL API for job management + +|*Database* |PostgreSQL (sqlx 0.8) |Job queue, verification results, +config + +|*GitHub* |octocrab 0.49 |GitHub API client for Check Runs + +|*HTTP Client* |reqwest 0.11 |Calls to ECHIDNA API and platform APIs + +|*Isolation* |Docker |Security isolation for proof execution + +|*Crypto* |hmac + sha2 |Webhook signature verification +|=== + +''''' + +=== Blockers Identified + +==== High Priority + +[arabic] +. *Container Isolation Not Implemented* - Security risk from running +untrusted code +. *No Retry Logic* - Temporary failures become permanent (bad UX) +. *Unlimited Concurrent Jobs* - Risk of resource exhaustion + +==== Medium Priority + +[arabic] +. *Bot Modes Not Implemented* - Only basic verification works, no tactic +suggestions +. *No Observability* - Hard to debug production issues +. *No Rate Limiting* - Vulnerable to webhook spam + +==== Low Priority + +[arabic] +. *Docker Compose Not Set Up* - Manual PostgreSQL setup required +. *No Pre-Built Prover Images* - Container startup slow + +''''' + +=== Testing Status + +*Unit Tests:* ✅ 7/7 passing + +.... +test dispatcher::echidna_client::tests::test_prover_from_extension ... ok +test api::webhooks::tests::test_verify_github_signature ... ok +test dispatcher::echidna_client::tests::test_prover_tier ... ok +test dispatcher::echidna_client::tests::test_prover_file_extensions ... ok +test scheduler::job_queue::tests::test_duplicate_detection ... ok +test scheduler::job_queue::tests::test_priority_ordering ... ok +test scheduler::job_queue::tests::test_enqueue_and_start ... ok +.... + +*Integration Tests:* ⏳ TODO (webhook → verification → result flow) + +''''' + +=== Files Modified + +[width="100%",cols="24%,24%,52%",options="header",] +|=== +|File |Type |Description +|`+Cargo.toml+` |Fix |Correct author email attribution + +|`+src/main.rs+` |Restore |CLI and server entry point + +|`+src/api/graphql.rs+` |Restore |GraphQL schema and resolvers + +|`+src/dispatcher/echidna_client.rs+` |Restore |ECHIDNA HTTP client + +|`+src/store/sqlite.rs+` |Restore |Database models and queries + +|`+.machine_readable/META.scm+` |Docs |8 ADRs + design rationale (377 +lines) + +|`+.machine_readable/ECOSYSTEM.scm+` |Docs |Ecosystem positioning (221 +lines) + +|`+.machine_readable/STATE.scm+` |Docs |Current progress + milestones +(178 lines) +|=== + +''''' + +=== Commit Summary + +.... +fix: restore source files and update comprehensive documentation + +- fix: correct author email to jonathan.jewell@open.ac.uk (was gmail) +- fix: restore deleted src/main.rs, graphql.rs, echidna_client.rs, sqlite.rs +- docs: comprehensive META.scm with 8 Architecture Decision Records +- docs: comprehensive ECOSYSTEM.scm with position and relationships +- docs: comprehensive STATE.scm with 75% completion tracking + +Closes: Build errors, missing files, incomplete documentation +Related: ECHIDNA v1.3.0 integration +.... + +*Commit Hash:* `+d09ae35+` + +''''' + +=== Production Readiness Checklist + +==== Infrastructure ✅ + +* [x] Build system working +* [x] Tests passing +* [x] Dependencies managed with Cargo +* [ ] Docker Compose setup (TODO) +* [ ] Kubernetes deployment (TODO) + +==== Documentation ✅ + +* [x] README.adoc comprehensive +* [x] META.scm with ADRs +* [x] ECOSYSTEM.scm with positioning +* [x] STATE.scm with progress tracking +* [ ] API documentation (GraphQL introspection exists) +* [ ] Deployment guide (TODO) + +==== Security ⚠️ + +* [x] Webhook signature verification +* [ ] Container isolation (TODO - HIGH PRIORITY) +* [ ] Resource limits (TODO - HIGH PRIORITY) +* [ ] Rate limiting (TODO) +* [ ] Security audit (TODO) + +==== Reliability ⚠️ + +* [x] Database persistence (PostgreSQL) +* [ ] Retry logic with backoff (TODO - HIGH PRIORITY) +* [ ] Error recovery (TODO) +* [ ] Health checks (basic exists, needs improvement) +* [ ] Observability (TODO) + +==== Features 🔄 + +* [x] GitHub/GitLab/Bitbucket webhooks +* [x] GraphQL API +* [x] ECHIDNA integration +* [ ] Container isolation (TODO - blocks Verifier mode) +* [ ] Verifier mode (TODO - simplest bot mode) +* [ ] Advisor mode (TODO) +* [ ] Consultant mode (TODO) +* [ ] Regulator mode (TODO) + +*Overall Status:* 75% complete, active development phase + +''''' + +=== Relationship to ECHIDNA v1.3.0 + +echidnabot is a *companion project* to ECHIDNA: + +[cols=",",options="header",] +|=== +|ECHIDNA v1.3.0 |echidnabot v0.1.0 +|*Proof verification* |*CI/CD orchestration* +|12 theorem prover backends |Webhook receivers for 3 platforms +|Julia ML tactic prediction |Job scheduling and queuing +|Rust REST API |GraphQL API for job management +|Neurosymbolic AI |Platform adapter abstraction +|Formal soundness guarantees |Container security isolation +|Production-ready (100%) |Active development (75%) +|=== + +*Integration:* echidnabot calls ECHIDNA HTTP API for all proof +verification. ECHIDNA can run standalone (via CLI/REPL/UI), echidnabot +adds CI/CD automation. + +''''' + +=== Next Session Focus + +[arabic] +. Implement container isolation with Docker (security critical) +. Add retry logic with exponential backoff (reliability critical) +. Implement concurrent job execution limits (stability critical) +. Begin Verifier mode implementation (first bot mode) + +''''' + +=== Lessons Learned + +[arabic] +. *Comprehensive Documentation Pays Off* - +META.scm/ECOSYSTEM.scm/STATE.scm provide clear context for contributors +. *Build System Must Be Solid* - cargo clean && cargo build resolved +stale artifact issues +. *Author Attribution Matters* - Consistent email across all repos +(jonathan.jewell@open.ac.uk) +. *Tests Are Green Light* - 7/7 passing tests give confidence to proceed +. *Clear Milestones Enable Progress Tracking* - 75% completion clearly +communicated via STATE.scm + +''''' + +*Session Date:* 2026-01-29 *Session Duration:* ~2 hours *Status:* ✅ +Complete - Ready for container isolation implementation diff --git a/SESSION_SUMMARY_2026-01-29.md b/SESSION_SUMMARY_2026-01-29.md deleted file mode 100644 index 78884c0..0000000 --- a/SESSION_SUMMARY_2026-01-29.md +++ /dev/null @@ -1,379 +0,0 @@ - -# echidnabot Session Summary - 2026-01-29 - -## Overview - -This session focused on bringing echidnabot up to the same comprehensive documentation standard as ECHIDNA v1.3.0, fixing build issues, and establishing the roadmap for production readiness. - ---- - -## Accomplishments - -### 1. Build System Fixes ✓ - -**Problem:** Repository had deleted source files and build errors -- `src/main.rs` deleted but still referenced in Cargo.toml -- `src/api/graphql.rs`, `src/dispatcher/echidna_client.rs`, `src/store/sqlite.rs` also deleted -- Build failed with missing file errors - -**Solution:** -```bash -git restore src/main.rs src/api/graphql.rs src/dispatcher/echidna_client.rs src/store/sqlite.rs -cargo clean && cargo build -``` - -**Result:** Clean build with 0 errors, all 7 unit tests passing - -### 2. Author Attribution Fix ✓ - -**Problem:** Cargo.toml had incorrect author email -```toml -authors = ["Jonathan D.A. Jewell "] # WRONG -``` - -**Solution:** -```toml -authors = ["Jonathan D.A. Jewell "] # CORRECT -``` - -**Compliance:** Follows CRITICAL attribution requirements from global CLAUDE.md - -### 3. Comprehensive META.scm ✓ - -Created comprehensive architecture documentation with **8 Architecture Decision Records (ADRs)**: - -| ADR | Title | Status | -|-----|-------|--------| -| ADR-001 | Multi-Platform Adapter Pattern | Accepted | -| ADR-002 | GraphQL API for Job Management | Accepted | -| ADR-003 | PostgreSQL for Job Queue and State | Accepted | -| ADR-004 | Webhook-Driven Architecture | Accepted | -| ADR-005 | Integration with ECHIDNA Core | Accepted | -| ADR-006 | Container Isolation for Proof Verification | Accepted | -| ADR-007 | Multi-Prover Support via ECHIDNA | Accepted | -| ADR-008 | Bot Modes: Verifier/Advisor/Consultant/Regulator | Accepted | - -**Key Decisions:** -- **Platform Abstraction:** `PlatformAdapter` trait for GitHub/GitLab/Bitbucket -- **API Choice:** async-graphql for type-safe, self-documenting API -- **Database:** PostgreSQL with sqlx compile-time query checking -- **Security:** Docker container isolation with resource limits -- **Integration:** HTTP client to ECHIDNA API (clear separation of concerns) - -### 4. Comprehensive ECOSYSTEM.scm ✓ - -Documented echidnabot's position in the formal verification ecosystem: - -**Relationships:** -- **Core Dependency:** ECHIDNA (required backend for 12 prover verification) -- **Code Platforms:** GitHub, GitLab, Bitbucket (webhook integration) -- **Theorem Provers:** All 12 supported by ECHIDNA (Coq, Lean, Isabelle, Agda, Z3, CVC5, Metamath, HOL Light, PVS, ACL2, HOL4, Mizar) -- **Rust Ecosystem:** Tokio, Axum, async-graphql, sqlx, reqwest, octocrab -- **Gitbot Fleet:** rhodibot, seambot, finishingbot, glambot (coordinated via hypatia) - -**Position Statement:** -> echidnabot bridges code hosting platforms (GitHub, GitLab, Bitbucket) and the ECHIDNA neurosymbolic theorem prover. It acts as a CI/CD orchestrator for formal verification, automatically checking proofs on every push and PR. - -### 5. Comprehensive STATE.scm ✓ - -**Current Progress: 75% Complete** - -**Completed Milestones (3/7):** -1. ✅ Core Infrastructure (100%) - Axum server, webhooks, database, GraphQL -2. ✅ Platform Integration (100%) - GitHub/GitLab/Bitbucket adapters -3. ✅ ECHIDNA Integration (100%) - HTTP client, job dispatch, result parsing - -**In Progress (1/7):** -4. 🔄 Job Scheduler and Queue (60%) - Basic queue works, need retry logic + concurrency limits - -**Planned (3/7):** -5. 📋 Container Isolation (0%) - Docker spawning, resource limits, network isolation -6. 📋 Bot Modes Implementation (0%) - Verifier/Advisor/Consultant/Regulator -7. 📋 Production Hardening (0%) - Error recovery, observability, rate limiting - -**Working Features:** -- ✅ HTTP server with health checks -- ✅ Webhook receivers for GitHub/GitLab/Bitbucket with signature verification -- ✅ Platform adapter abstraction for multi-platform support -- ✅ GraphQL API for job queries and mutations -- ✅ PostgreSQL database with sqlx migrations -- ✅ Integration with ECHIDNA API for proof verification -- ✅ Repository registration and configuration -- ✅ Job status tracking - ---- - -## Critical Next Actions - -### Immediate (This Week) - -1. **Container Isolation (High Priority - Security)** - - Implement Docker container spawning for proof verification - - Add resource limits (CPU, memory, timeout) - - Read-only filesystem setup - - Network isolation - - **Why Critical:** Without isolation, running untrusted code from PRs is a security risk - -2. **Retry Logic with Backoff (High Priority - Reliability)** - - Add exponential backoff for failed jobs - - Distinguish transient vs permanent failures - - Configurable retry limits - - **Why Critical:** Temporary failures (network issues, ECHIDNA busy) currently become permanent - -3. **Concurrent Job Execution Limits (High Priority - Stability)** - - Implement job concurrency limits - - Priority queue for urgent jobs - - Fair scheduling across repositories - - **Why Critical:** Unlimited concurrency can exhaust resources - -### This Week - -4. **Verifier Mode Implementation** - - Silent pass/fail checks (basic bot mode) - - Check run / commit status creation - - Basic PR comments on failure - - **First bot mode to implement** (simplest, highest value) - -5. **Docker Compose Setup** - - PostgreSQL + echidnabot + ECHIDNA in one command - - Easy local development - - Production-like environment - -6. **Integration Tests** - - End-to-end webhook → verification → result flow - - Test with real GitHub webhook payloads - - Mock ECHIDNA API responses - -### This Month - -7. **Advisor Mode** - Tactic suggestions via ECHIDNA ML on proof failure -8. **Observability** - Prometheus metrics, OpenTelemetry tracing -9. **Pre-Built Prover Images** - Docker images for all 12 provers -10. **Regulator Mode** - PR merge blocking when proofs fail -11. **Production Deployment Guide** - Kubernetes, security hardening -12. **GitHub App Distribution** - Easy installation for users - ---- - -## Architecture Overview - -``` -┌─────────────────────────────────────────────────────────────┐ -│ GitHub / GitLab / Bitbucket │ -│ (Push, PR events) │ -└────────────────────────┬────────────────────────────────────┘ - │ Webhooks (verified HMAC) - ▼ -┌─────────────────────────────────────────────────────────────┐ -│ echidnabot │ -│ ┌──────────────┐ ┌──────────────┐ ┌──────────────┐ │ -│ │ Webhook │ │ GraphQL │ │ Platform │ │ -│ │ Receivers │ │ API │ │ Adapters │ │ -│ └──────────────┘ └──────────────┘ └──────────────┘ │ -│ │ -│ ┌──────────────────────────────────────────────────┐ │ -│ │ Job Scheduler & Queue │ │ -│ │ (PostgreSQL persistence) │ │ -│ └──────────────────────────────────────────────────┘ │ -│ │ │ -│ │ HTTP API calls │ -│ ▼ │ -│ ┌──────────────────────┐ │ -│ │ Container Spawner │ │ -│ │ (Docker isolation) │ │ -│ └──────────────────────┘ │ -└──────────────────────┬──────────────────────────────────────┘ - │ HTTP to ECHIDNA - ▼ -┌─────────────────────────────────────────────────────────────┐ -│ ECHIDNA Core │ -│ ┌─────────────┐ ┌─────────────┐ ┌─────────────┐ │ -│ │ Julia ML │ │ Rust │ │ 12 Prover │ │ -│ │ Backend │ │ Backend │ │ Backends │ │ -│ └─────────────┘ └─────────────┘ └─────────────┘ │ -└─────────────────────────────────────────────────────────────┘ - │ Verification results - ▼ -┌─────────────────────────────────────────────────────────────┐ -│ GitHub Check Runs / PR Comments │ -│ GitLab Commit Statuses / MR Notes │ -│ Bitbucket Build Statuses / PR Comments │ -└─────────────────────────────────────────────────────────────┘ -``` - ---- - -## Technology Stack - -| Layer | Technology | Purpose | -|-------|------------|---------| -| **Runtime** | Rust 1.75+ | Memory-safe systems programming | -| **Async** | Tokio | Async runtime for concurrent webhook handling | -| **Web** | Axum 0.8 | Ergonomic web framework for HTTP/webhooks | -| **API** | async-graphql 7 | Type-safe GraphQL API for job management | -| **Database** | PostgreSQL (sqlx 0.8) | Job queue, verification results, config | -| **GitHub** | octocrab 0.49 | GitHub API client for Check Runs | -| **HTTP Client** | reqwest 0.11 | Calls to ECHIDNA API and platform APIs | -| **Isolation** | Docker | Security isolation for proof execution | -| **Crypto** | hmac + sha2 | Webhook signature verification | - ---- - -## Blockers Identified - -### High Priority -1. **Container Isolation Not Implemented** - Security risk from running untrusted code -2. **No Retry Logic** - Temporary failures become permanent (bad UX) -3. **Unlimited Concurrent Jobs** - Risk of resource exhaustion - -### Medium Priority -1. **Bot Modes Not Implemented** - Only basic verification works, no tactic suggestions -2. **No Observability** - Hard to debug production issues -3. **No Rate Limiting** - Vulnerable to webhook spam - -### Low Priority -1. **Docker Compose Not Set Up** - Manual PostgreSQL setup required -2. **No Pre-Built Prover Images** - Container startup slow - ---- - -## Testing Status - -**Unit Tests:** ✅ 7/7 passing - -``` -test dispatcher::echidna_client::tests::test_prover_from_extension ... ok -test api::webhooks::tests::test_verify_github_signature ... ok -test dispatcher::echidna_client::tests::test_prover_tier ... ok -test dispatcher::echidna_client::tests::test_prover_file_extensions ... ok -test scheduler::job_queue::tests::test_duplicate_detection ... ok -test scheduler::job_queue::tests::test_priority_ordering ... ok -test scheduler::job_queue::tests::test_enqueue_and_start ... ok -``` - -**Integration Tests:** ⏳ TODO (webhook → verification → result flow) - ---- - -## Files Modified - -| File | Type | Description | -|------|------|-------------| -| `Cargo.toml` | Fix | Correct author email attribution | -| `src/main.rs` | Restore | CLI and server entry point | -| `src/api/graphql.rs` | Restore | GraphQL schema and resolvers | -| `src/dispatcher/echidna_client.rs` | Restore | ECHIDNA HTTP client | -| `src/store/sqlite.rs` | Restore | Database models and queries | -| `.machine_readable/META.scm` | Docs | 8 ADRs + design rationale (377 lines) | -| `.machine_readable/ECOSYSTEM.scm` | Docs | Ecosystem positioning (221 lines) | -| `.machine_readable/STATE.scm` | Docs | Current progress + milestones (178 lines) | - ---- - -## Commit Summary - -``` -fix: restore source files and update comprehensive documentation - -- fix: correct author email to jonathan.jewell@open.ac.uk (was gmail) -- fix: restore deleted src/main.rs, graphql.rs, echidna_client.rs, sqlite.rs -- docs: comprehensive META.scm with 8 Architecture Decision Records -- docs: comprehensive ECOSYSTEM.scm with position and relationships -- docs: comprehensive STATE.scm with 75% completion tracking - -Closes: Build errors, missing files, incomplete documentation -Related: ECHIDNA v1.3.0 integration -``` - -**Commit Hash:** `d09ae35` - ---- - -## Production Readiness Checklist - -### Infrastructure ✅ -- [x] Build system working -- [x] Tests passing -- [x] Dependencies managed with Cargo -- [ ] Docker Compose setup (TODO) -- [ ] Kubernetes deployment (TODO) - -### Documentation ✅ -- [x] README.adoc comprehensive -- [x] META.scm with ADRs -- [x] ECOSYSTEM.scm with positioning -- [x] STATE.scm with progress tracking -- [ ] API documentation (GraphQL introspection exists) -- [ ] Deployment guide (TODO) - -### Security ⚠️ -- [x] Webhook signature verification -- [ ] Container isolation (TODO - HIGH PRIORITY) -- [ ] Resource limits (TODO - HIGH PRIORITY) -- [ ] Rate limiting (TODO) -- [ ] Security audit (TODO) - -### Reliability ⚠️ -- [x] Database persistence (PostgreSQL) -- [ ] Retry logic with backoff (TODO - HIGH PRIORITY) -- [ ] Error recovery (TODO) -- [ ] Health checks (basic exists, needs improvement) -- [ ] Observability (TODO) - -### Features 🔄 -- [x] GitHub/GitLab/Bitbucket webhooks -- [x] GraphQL API -- [x] ECHIDNA integration -- [ ] Container isolation (TODO - blocks Verifier mode) -- [ ] Verifier mode (TODO - simplest bot mode) -- [ ] Advisor mode (TODO) -- [ ] Consultant mode (TODO) -- [ ] Regulator mode (TODO) - -**Overall Status:** 75% complete, active development phase - ---- - -## Relationship to ECHIDNA v1.3.0 - -echidnabot is a **companion project** to ECHIDNA: - -| ECHIDNA v1.3.0 | echidnabot v0.1.0 | -|----------------|-------------------| -| **Proof verification** | **CI/CD orchestration** | -| 12 theorem prover backends | Webhook receivers for 3 platforms | -| Julia ML tactic prediction | Job scheduling and queuing | -| Rust REST API | GraphQL API for job management | -| Neurosymbolic AI | Platform adapter abstraction | -| Formal soundness guarantees | Container security isolation | -| Production-ready (100%) | Active development (75%) | - -**Integration:** echidnabot calls ECHIDNA HTTP API for all proof verification. ECHIDNA can run standalone (via CLI/REPL/UI), echidnabot adds CI/CD automation. - ---- - -## Next Session Focus - -1. Implement container isolation with Docker (security critical) -2. Add retry logic with exponential backoff (reliability critical) -3. Implement concurrent job execution limits (stability critical) -4. Begin Verifier mode implementation (first bot mode) - ---- - -## Lessons Learned - -1. **Comprehensive Documentation Pays Off** - META.scm/ECOSYSTEM.scm/STATE.scm provide clear context for contributors -2. **Build System Must Be Solid** - cargo clean && cargo build resolved stale artifact issues -3. **Author Attribution Matters** - Consistent email across all repos (jonathan.jewell@open.ac.uk) -4. **Tests Are Green Light** - 7/7 passing tests give confidence to proceed -5. **Clear Milestones Enable Progress Tracking** - 75% completion clearly communicated via STATE.scm - ---- - -**Session Date:** 2026-01-29 -**Session Duration:** ~2 hours -**Status:** ✅ Complete - Ready for container isolation implementation diff --git a/SONNET-TASKS.adoc b/SONNET-TASKS.adoc new file mode 100644 index 0000000..16596e9 --- /dev/null +++ b/SONNET-TASKS.adoc @@ -0,0 +1,246 @@ +== Echidnabot — Sonnet Task Plan + +=== Context + +Echidnabot is a Tier 1 (Verifier) bot in the gitbot-fleet ecosystem. It +acts as the bridge between the ECHIDNA neurosymbolic theorem proving +platform and the gitbot-fleet orchestration layer. It receives webhook +events, dispatches verification requests to ECHIDNA, and reports +findings back to the fleet. + +*Current state*: ~65-70% actual completion (claims 75%). Core +infrastructure complete (Axum server, webhooks, database, GraphQL, +ECHIDNA HTTP client). Critical gaps: container isolation is EMPTY, bot +modes not wired into handlers, retry logic not integrated, ZERO +automated tests. + +''''' + +=== Task 1: Implement Container Isolation (CRITICAL SECURITY) + +*File*: `+src/executor/container.rs+` + +This file is EMPTY. Proofs currently run without any isolation — a +malicious proof could execute arbitrary code on the host. + +==== 1.1 Implement PodmanExecutor + +[source,rust] +---- +pub struct PodmanExecutor { + image: String, + timeout: Duration, + memory_limit: String, + network: bool, // should be false for proof checking +} +---- + +==== 1.2 Core isolation features + +* Run proof-checking in Podman containers (rootless) +* No network access (`+--network=none+`) +* Memory limit (`+--memory=512m+` default, configurable) +* CPU limit (`+--cpus=2+` default, configurable) +* Timeout with SIGKILL (`+--timeout+`) +* Read-only filesystem except `+/tmp+` for proof artifacts +* Drop ALL capabilities (`+--cap-drop=ALL+`) +* No new privileges (`+--security-opt=no-new-privileges+`) + +==== 1.3 Input/output handling + +* Mount proof files as read-only volume +* Capture stdout/stderr for proof results +* Parse exit code: 0 = verified, non-zero = failed/timeout +* Clean up containers after completion + +==== 1.4 Fallback for systems without Podman + +* Check if Podman is available at startup +* If not: log warning, use `+bubblewrap+` (bwrap) as lighter alternative +* If neither: refuse to run proofs (fail-safe, not fail-open) + +==== Verification + +* Unit test: PodmanExecutor creates correct command line args +* Integration test: run a trivial proof in container, verify result +* Test: malicious proof attempt (e.g., `+rm -rf /+`) is contained +* Test: timeout kills container after configured duration + +''''' + +=== Task 2: Wire Bot Modes into Webhook Handlers + +*Files*: `+src/webhook/+` handlers, `+src/bot/modes.rs+` or equivalent + +Bot modes are defined (Verifier, Advisor, Consultant, Regulator) but NOT +connected to the webhook handlers. + +==== 2.1 Mode selection logic + +* Read bot mode from `+.bot_directives/echidnabot.scm+` in the target +repo +* Default to `+Verifier+` mode if no directive found +* Mode determines: +** *Verifier*: Full proof checking, block PR on failure +** *Advisor*: Check proofs, comment results, don’t block +** *Consultant*: Only analyze when explicitly requested (@echidnabot +check) +** *Regulator*: Enforce minimum proof coverage thresholds + +==== 2.2 Wire into PR webhook handler + +* On PR open/update: determine mode → dispatch appropriate action +* Verifier/Advisor: automatically trigger proof checking +* Consultant: only respond to explicit mentions +* Regulator: check proof coverage metrics + +==== 2.3 Wire into push webhook handler + +* On push to main: determine mode → dispatch appropriate action +* All modes: update proof status dashboard + +==== Verification + +* Test: webhook with Verifier mode triggers proof checking +* Test: webhook with Consultant mode does NOT auto-trigger +* Test: missing directive defaults to Verifier + +''''' + +=== Task 3: Integrate Retry Logic + +*Files*: `+src/scheduler/+` or `+src/executor/+` + +Retry logic is defined somewhere in the codebase but NOT integrated into +the actual execution pipeline. + +==== 3.1 Find and wire retry logic + +* Locate the retry/backoff implementation +* Wire it into the proof execution pipeline: +** Container startup failure → retry with backoff +** ECHIDNA API timeout → retry up to 3 times +** Transient network errors → retry with exponential backoff +** Proof timeout → do NOT retry (intentional, resource-saving) + +==== 3.2 Circuit breaker + +* If ECHIDNA API fails 5 consecutive times → circuit breaker opens +* Log error, notify fleet coordinator +* Auto-reset after 5 minutes + +==== Verification + +* Test: transient failure retries and succeeds on second attempt +* Test: permanent failure stops after max retries +* Test: circuit breaker opens after consecutive failures + +''''' + +=== Task 4: Add Automated Tests (CRITICAL) + +The repo has ZERO tests despite importing test libraries. + +==== 4.1 Unit tests for ECHIDNA client + +* Test: HTTP client constructs correct API requests +* Test: response parsing handles success case +* Test: response parsing handles error case +* Test: timeout handling + +==== 4.2 Unit tests for webhook verification + +* Test: valid HMAC-SHA256 signature passes +* Test: invalid signature is rejected +* Test: missing signature header is rejected + +==== 4.3 Unit tests for GraphQL API + +* Test: query resolves proof status +* Test: mutation triggers proof check +* Test: authentication required for mutations + +==== 4.4 Unit tests for database models + +* Test: proof result CRUD operations +* Test: concurrent access handling + +==== 4.5 Integration test + +* Test: full webhook → dispatch → (mock) ECHIDNA → finding → fleet +context flow +* Use mock ECHIDNA server (axum test server) + +==== Verification + +* `+cargo test+` — minimum 20 tests, all passing +* No test requires actual ECHIDNA instance (use mocks) + +''''' + +=== Task 5: Fix Metadata + +==== 5.1 Cargo.toml + +* License: must be `+MPL-2.0+` (not AGPL) +* Author: must be +`+"Jonathan D.A. Jewell "+` + +==== 5.2 SPDX headers + +* Every `+.rs+` file needs: ++ +[source,rust] +---- +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell +---- + +==== 5.3 STATE.a2ml update + +* Update completion to actual percentage +* Fix tech-stack if inaccurate +* Add session history entry + +==== Verification + +* `+grep -r "AGPL" .+` returns nothing +* All `+.rs+` files have SPDX headers + +''''' + +=== Task 6: ECHIDNA Trust Bridge + +Connect echidnabot to echidna’s trust verification mechanisms. + +==== 6.1 Proof confidence reporting + +* When ECHIDNA returns a proof result, include the confidence level in +the Finding: +** Level 5: Cross-checked by 2+ independent small-kernel systems +** Level 4: Checked by small-kernel system (Lean4, Coq, Isabelle) with +certificate +** Level 3: Single prover with proof certificate (Alethe, DRAT/LRAT) +** Level 2: Single prover result without certificate +** Level 1: Large-TCB system or unchecked result +* Map confidence to Finding severity and metadata + +==== 6.2 Solver integrity verification + +* Before dispatching to ECHIDNA, verify that the solver binaries haven’t +been tampered with +* Check SHA256 manifest (see echidna SONNET-TASKS.md Task 2) +* Report integrity status in Finding metadata + +==== 6.3 Axiom usage tracking + +* Parse ECHIDNA proof results for axiom usage +* Flag proofs using `+sorry+`, `+Admitted+`, `+postulate+`, `+choice+`, +`+--type-in-type+` +* Report axiom reliance as separate Finding with Warning severity + +==== Verification + +* Test: confidence level correctly mapped for each prover type +* Test: axiom usage detected and reported +* Test: solver integrity check included in results diff --git a/SONNET-TASKS.md b/SONNET-TASKS.md deleted file mode 100644 index 60b3a90..0000000 --- a/SONNET-TASKS.md +++ /dev/null @@ -1,202 +0,0 @@ - -# Echidnabot — Sonnet Task Plan - -## Context - -Echidnabot is a Tier 1 (Verifier) bot in the gitbot-fleet ecosystem. It acts as the bridge between the ECHIDNA neurosymbolic theorem proving platform and the gitbot-fleet orchestration layer. It receives webhook events, dispatches verification requests to ECHIDNA, and reports findings back to the fleet. - -**Current state**: ~65-70% actual completion (claims 75%). Core infrastructure complete (Axum server, webhooks, database, GraphQL, ECHIDNA HTTP client). Critical gaps: container isolation is EMPTY, bot modes not wired into handlers, retry logic not integrated, ZERO automated tests. - ---- - -## Task 1: Implement Container Isolation (CRITICAL SECURITY) - -**File**: `src/executor/container.rs` - -This file is EMPTY. Proofs currently run without any isolation — a malicious proof could execute arbitrary code on the host. - -### 1.1 Implement PodmanExecutor -```rust -pub struct PodmanExecutor { - image: String, - timeout: Duration, - memory_limit: String, - network: bool, // should be false for proof checking -} -``` - -### 1.2 Core isolation features -- Run proof-checking in Podman containers (rootless) -- No network access (`--network=none`) -- Memory limit (`--memory=512m` default, configurable) -- CPU limit (`--cpus=2` default, configurable) -- Timeout with SIGKILL (`--timeout`) -- Read-only filesystem except `/tmp` for proof artifacts -- Drop ALL capabilities (`--cap-drop=ALL`) -- No new privileges (`--security-opt=no-new-privileges`) - -### 1.3 Input/output handling -- Mount proof files as read-only volume -- Capture stdout/stderr for proof results -- Parse exit code: 0 = verified, non-zero = failed/timeout -- Clean up containers after completion - -### 1.4 Fallback for systems without Podman -- Check if Podman is available at startup -- If not: log warning, use `bubblewrap` (bwrap) as lighter alternative -- If neither: refuse to run proofs (fail-safe, not fail-open) - -### Verification -- Unit test: PodmanExecutor creates correct command line args -- Integration test: run a trivial proof in container, verify result -- Test: malicious proof attempt (e.g., `rm -rf /`) is contained -- Test: timeout kills container after configured duration - ---- - -## Task 2: Wire Bot Modes into Webhook Handlers - -**Files**: `src/webhook/` handlers, `src/bot/modes.rs` or equivalent - -Bot modes are defined (Verifier, Advisor, Consultant, Regulator) but NOT connected to the webhook handlers. - -### 2.1 Mode selection logic -- Read bot mode from `.bot_directives/echidnabot.scm` in the target repo -- Default to `Verifier` mode if no directive found -- Mode determines: - - **Verifier**: Full proof checking, block PR on failure - - **Advisor**: Check proofs, comment results, don't block - - **Consultant**: Only analyze when explicitly requested (@echidnabot check) - - **Regulator**: Enforce minimum proof coverage thresholds - -### 2.2 Wire into PR webhook handler -- On PR open/update: determine mode → dispatch appropriate action -- Verifier/Advisor: automatically trigger proof checking -- Consultant: only respond to explicit mentions -- Regulator: check proof coverage metrics - -### 2.3 Wire into push webhook handler -- On push to main: determine mode → dispatch appropriate action -- All modes: update proof status dashboard - -### Verification -- Test: webhook with Verifier mode triggers proof checking -- Test: webhook with Consultant mode does NOT auto-trigger -- Test: missing directive defaults to Verifier - ---- - -## Task 3: Integrate Retry Logic - -**Files**: `src/scheduler/` or `src/executor/` - -Retry logic is defined somewhere in the codebase but NOT integrated into the actual execution pipeline. - -### 3.1 Find and wire retry logic -- Locate the retry/backoff implementation -- Wire it into the proof execution pipeline: - - Container startup failure → retry with backoff - - ECHIDNA API timeout → retry up to 3 times - - Transient network errors → retry with exponential backoff - - Proof timeout → do NOT retry (intentional, resource-saving) - -### 3.2 Circuit breaker -- If ECHIDNA API fails 5 consecutive times → circuit breaker opens -- Log error, notify fleet coordinator -- Auto-reset after 5 minutes - -### Verification -- Test: transient failure retries and succeeds on second attempt -- Test: permanent failure stops after max retries -- Test: circuit breaker opens after consecutive failures - ---- - -## Task 4: Add Automated Tests (CRITICAL) - -The repo has ZERO tests despite importing test libraries. - -### 4.1 Unit tests for ECHIDNA client -- Test: HTTP client constructs correct API requests -- Test: response parsing handles success case -- Test: response parsing handles error case -- Test: timeout handling - -### 4.2 Unit tests for webhook verification -- Test: valid HMAC-SHA256 signature passes -- Test: invalid signature is rejected -- Test: missing signature header is rejected - -### 4.3 Unit tests for GraphQL API -- Test: query resolves proof status -- Test: mutation triggers proof check -- Test: authentication required for mutations - -### 4.4 Unit tests for database models -- Test: proof result CRUD operations -- Test: concurrent access handling - -### 4.5 Integration test -- Test: full webhook → dispatch → (mock) ECHIDNA → finding → fleet context flow -- Use mock ECHIDNA server (axum test server) - -### Verification -- `cargo test` — minimum 20 tests, all passing -- No test requires actual ECHIDNA instance (use mocks) - ---- - -## Task 5: Fix Metadata - -### 5.1 Cargo.toml -- License: must be `MPL-2.0` (not AGPL) -- Author: must be `"Jonathan D.A. Jewell "` - -### 5.2 SPDX headers -- Every `.rs` file needs: - ```rust - // SPDX-License-Identifier: CC-BY-SA-4.0 - // SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell - ``` - -### 5.3 STATE.a2ml update -- Update completion to actual percentage -- Fix tech-stack if inaccurate -- Add session history entry - -### Verification -- `grep -r "AGPL" .` returns nothing -- All `.rs` files have SPDX headers - ---- - -## Task 6: ECHIDNA Trust Bridge - -Connect echidnabot to echidna's trust verification mechanisms. - -### 6.1 Proof confidence reporting -- When ECHIDNA returns a proof result, include the confidence level in the Finding: - - Level 5: Cross-checked by 2+ independent small-kernel systems - - Level 4: Checked by small-kernel system (Lean4, Coq, Isabelle) with certificate - - Level 3: Single prover with proof certificate (Alethe, DRAT/LRAT) - - Level 2: Single prover result without certificate - - Level 1: Large-TCB system or unchecked result -- Map confidence to Finding severity and metadata - -### 6.2 Solver integrity verification -- Before dispatching to ECHIDNA, verify that the solver binaries haven't been tampered with -- Check SHA256 manifest (see echidna SONNET-TASKS.md Task 2) -- Report integrity status in Finding metadata - -### 6.3 Axiom usage tracking -- Parse ECHIDNA proof results for axiom usage -- Flag proofs using `sorry`, `Admitted`, `postulate`, `choice`, `--type-in-type` -- Report axiom reliance as separate Finding with Warning severity - -### Verification -- Test: confidence level correctly mapped for each prover type -- Test: axiom usage detected and reported -- Test: solver integrity check included in results diff --git a/docs/content/api.md b/docs/content/api.adoc similarity index 71% rename from docs/content/api.md rename to docs/content/api.adoc index b796149..29838f5 100644 --- a/docs/content/api.md +++ b/docs/content/api.adoc @@ -1,30 +1,22 @@ - ---- -title: API Reference -date: 2025-01-01 -template: default ---- +== GraphQL API Reference -# GraphQL API Reference +echidnabot exposes a GraphQL API for querying and controlling proof +verification. -echidnabot exposes a GraphQL API for querying and controlling proof verification. +=== Endpoint -## Endpoint - -``` +.... POST /graphql -``` +.... -## Queries +=== Queries -### repository +==== repository Fetch a registered repository. -```graphql +[source,graphql] +---- query { repository(platform: GITHUB, owner: "org", name: "repo") { id @@ -35,13 +27,14 @@ query { webhookConfigured } } -``` +---- -### repositories +==== repositories List all registered repositories. -```graphql +[source,graphql] +---- query { repositories(platform: GITHUB) { id @@ -50,13 +43,14 @@ query { enabledProvers } } -``` +---- -### job +==== job Fetch a specific proof job. -```graphql +[source,graphql] +---- query { job(id: "uuid-here") { id @@ -73,13 +67,14 @@ query { } } } -``` +---- -### jobsForRepo +==== jobsForRepo List jobs for a repository. -```graphql +[source,graphql] +---- query { jobsForRepo(repoId: "uuid-here", limit: 10) { id @@ -89,13 +84,14 @@ query { queuedAt } } -``` +---- -### availableProvers +==== availableProvers List available theorem provers. -```graphql +[source,graphql] +---- query { availableProvers { kind @@ -104,15 +100,16 @@ query { tier } } -``` +---- -## Mutations +=== Mutations -### registerRepository +==== registerRepository Register a new repository for proof verification. -```graphql +[source,graphql] +---- mutation { registerRepository(input: { platform: GITHUB @@ -125,13 +122,14 @@ mutation { webhookUrl } } -``` +---- -### triggerCheck +==== triggerCheck Manually trigger proof verification. -```graphql +[source,graphql] +---- mutation { triggerCheck( repoId: "uuid-here" @@ -143,13 +141,14 @@ mutation { queuedAt } } -``` +---- -### updateRepoSettings +==== updateRepoSettings Update repository settings. -```graphql +[source,graphql] +---- mutation { updateRepoSettings( repoId: "uuid-here" @@ -162,24 +161,26 @@ mutation { enabledProvers } } -``` +---- -## Types +=== Types -### Platform +==== Platform -```graphql +[source,graphql] +---- enum Platform { GITHUB GITLAB BITBUCKET CODEBERG } -``` +---- -### ProverKind +==== ProverKind -```graphql +[source,graphql] +---- enum ProverKind { COQ LEAN4 @@ -191,11 +192,12 @@ enum ProverKind { HOL_LIGHT MIZAR } -``` +---- -### JobStatus +==== JobStatus -```graphql +[source,graphql] +---- enum JobStatus { QUEUED RUNNING @@ -203,17 +205,17 @@ enum JobStatus { FAILED CANCELLED } -``` +---- -## Authentication +=== Authentication Include your API token in the Authorization header: -``` +.... Authorization: Bearer -``` +.... -## Rate Limits +=== Rate Limits -- 1000 requests per hour per token -- 10 concurrent proof jobs per repository +* 1000 requests per hour per token +* 10 concurrent proof jobs per repository diff --git a/docs/content/configuration.md b/docs/content/configuration.adoc similarity index 62% rename from docs/content/configuration.md rename to docs/content/configuration.adoc index 6c267ce..95dffc6 100644 --- a/docs/content/configuration.md +++ b/docs/content/configuration.adoc @@ -1,24 +1,16 @@ - ---- -title: Configuration Reference -date: 2025-01-01 -template: default ---- - -# Configuration Reference +== Configuration Reference echidnabot is configured via TOML files and environment variables. -## Configuration Files +=== Configuration Files -### echidnabot.toml +==== echidnabot.toml -The main configuration file, located in your repository root or at `~/.config/echidnabot/config.toml`. +The main configuration file, located in your repository root or at +`+~/.config/echidnabot/config.toml+`. -```toml +[source,toml] +---- # Server configuration [server] host = "0.0.0.0" @@ -62,29 +54,32 @@ webhook_secret = "${GITHUB_WEBHOOK_SECRET}" [gitlab] token = "${GITLAB_TOKEN}" webhook_secret = "${GITLAB_WEBHOOK_SECRET}" -``` - -## Environment Variables - -| Variable | Description | Required | -|----------|-------------|----------| -| `ECHIDNABOT_CONFIG` | Path to config file | No | -| `ECHIDNABOT_DATABASE_URL` | Database connection URL | Yes | -| `ECHIDNABOT_ECHIDNA_ENDPOINT` | ECHIDNA Core GraphQL endpoint | Yes | -| `ECHIDNABOT_ECHIDNA_REST_ENDPOINT` | ECHIDNA Core REST endpoint | No | -| `ECHIDNABOT_ECHIDNA_MODE` | ECHIDNA API mode (auto/graphql/rest) | No | -| `GITHUB_WEBHOOK_SECRET` | GitHub webhook secret | For GitHub | -| `GITHUB_APP_ID` | GitHub App ID | For GitHub | -| `GITHUB_PRIVATE_KEY` | GitHub App private key (PEM) | For GitHub | -| `GITLAB_TOKEN` | GitLab access token | For GitLab | -| `GITLAB_WEBHOOK_SECRET` | GitLab webhook secret | For GitLab | -| `RUST_LOG` | Log level override | No | - -## Repository Configuration - -Per-repository configuration in `.echidnabot.toml`: - -```toml +---- + +=== Environment Variables + +[width="100%",cols="31%,39%,30%",options="header",] +|=== +|Variable |Description |Required +|`+ECHIDNABOT_CONFIG+` |Path to config file |No +|`+ECHIDNABOT_DATABASE_URL+` |Database connection URL |Yes +|`+ECHIDNABOT_ECHIDNA_ENDPOINT+` |ECHIDNA Core GraphQL endpoint |Yes +|`+ECHIDNABOT_ECHIDNA_REST_ENDPOINT+` |ECHIDNA Core REST endpoint |No +|`+ECHIDNABOT_ECHIDNA_MODE+` |ECHIDNA API mode (auto/graphql/rest) |No +|`+GITHUB_WEBHOOK_SECRET+` |GitHub webhook secret |For GitHub +|`+GITHUB_APP_ID+` |GitHub App ID |For GitHub +|`+GITHUB_PRIVATE_KEY+` |GitHub App private key (PEM) |For GitHub +|`+GITLAB_TOKEN+` |GitLab access token |For GitLab +|`+GITLAB_WEBHOOK_SECRET+` |GitLab webhook secret |For GitLab +|`+RUST_LOG+` |Log level override |No +|=== + +=== Repository Configuration + +Per-repository configuration in `+.echidnabot.toml+`: + +[source,toml] +---- # Enabled provers for this repository [provers] enabled = ["coq", "lean4", "agda"] @@ -115,21 +110,23 @@ branches = ["main", "develop"] [notify] on_failure = true on_success = false -``` +---- -## CLI Configuration +=== CLI Configuration -```bash +[source,bash] +---- # Set config path export ECHIDNABOT_CONFIG=/path/to/config.toml # Or pass directly echidnabot --config /path/to/config.toml serve -``` +---- -## Docker Configuration +=== Docker Configuration -```yaml +[source,yaml] +---- version: "3.8" services: echidnabot: @@ -142,4 +139,4 @@ services: - "8080:8080" volumes: - ./config:/etc/echidnabot -``` +---- diff --git a/docs/content/getting-started.adoc b/docs/content/getting-started.adoc new file mode 100644 index 0000000..a3e61be --- /dev/null +++ b/docs/content/getting-started.adoc @@ -0,0 +1,93 @@ +== Getting Started with echidnabot + +This guide walks you through setting up echidnabot for your repository. + +=== Prerequisites + +* A GitHub, GitLab, or Bitbucket repository +* Proof files in a supported format (Coq, Lean, Agda, etc.) +* Access to an ECHIDNA Core instance + +=== Installation + +==== From Cargo + +[source,bash] +---- +cargo install echidnabot +---- + +==== From Source + +[source,bash] +---- +git clone https://github.com/hyperpolymath/echidnabot +cd echidnabot +cargo build --release +---- + +==== Using Guix + +[source,bash] +---- +guix install echidnabot +---- + +=== Configuration + +Create an `+echidnabot.toml+` in your repository root: + +[source,toml] +---- +[repository] +platform = "github" +owner = "your-org" +name = "your-repo" + +[provers] +enabled = ["coq", "lean4", "agda"] + +[webhook] +secret = "${ECHIDNABOT_WEBHOOK_SECRET}" + +[echidna] +endpoint = "https://echidna.example.com/graphql" +rest_endpoint = "https://echidna.example.com" +mode = "auto" +---- + +=== Setting Up Webhooks + +==== GitHub + +[arabic] +. Go to Repository Settings → Webhooks +. Add webhook URL: `+https://your-echidnabot-instance/webhooks/github+` +. Content type: `+application/json+` +. Secret: Your configured webhook secret +. Events: Push, Pull Request + +==== GitLab + +[arabic] +. Go to Settings → Webhooks +. URL: `+https://your-echidnabot-instance/webhooks/gitlab+` +. Secret token: Your configured webhook secret +. Triggers: Push events, Merge request events + +=== Verifying Setup + +[source,bash] +---- +# Check echidnabot status +echidnabot status + +# Trigger a test verification +echidnabot check --commit HEAD --dry-run +---- + +=== Next Steps + +* link:./configuration.md[Configuration Reference] +* link:./api.md[API Documentation] +* link:./provers.md[Prover Setup] diff --git a/docs/content/getting-started.md b/docs/content/getting-started.md deleted file mode 100644 index b947371..0000000 --- a/docs/content/getting-started.md +++ /dev/null @@ -1,96 +0,0 @@ - ---- -title: Getting Started -date: 2025-01-01 -template: default ---- - -# Getting Started with echidnabot - -This guide walks you through setting up echidnabot for your repository. - -## Prerequisites - -- A GitHub, GitLab, or Bitbucket repository -- Proof files in a supported format (Coq, Lean, Agda, etc.) -- Access to an ECHIDNA Core instance - -## Installation - -### From Cargo - -```bash -cargo install echidnabot -``` - -### From Source - -```bash -git clone https://github.com/hyperpolymath/echidnabot -cd echidnabot -cargo build --release -``` - -### Using Guix - -```bash -guix install echidnabot -``` - -## Configuration - -Create an `echidnabot.toml` in your repository root: - -```toml -[repository] -platform = "github" -owner = "your-org" -name = "your-repo" - -[provers] -enabled = ["coq", "lean4", "agda"] - -[webhook] -secret = "${ECHIDNABOT_WEBHOOK_SECRET}" - -[echidna] -endpoint = "https://echidna.example.com/graphql" -rest_endpoint = "https://echidna.example.com" -mode = "auto" -``` - -## Setting Up Webhooks - -### GitHub - -1. Go to Repository Settings → Webhooks -2. Add webhook URL: `https://your-echidnabot-instance/webhooks/github` -3. Content type: `application/json` -4. Secret: Your configured webhook secret -5. Events: Push, Pull Request - -### GitLab - -1. Go to Settings → Webhooks -2. URL: `https://your-echidnabot-instance/webhooks/gitlab` -3. Secret token: Your configured webhook secret -4. Triggers: Push events, Merge request events - -## Verifying Setup - -```bash -# Check echidnabot status -echidnabot status - -# Trigger a test verification -echidnabot check --commit HEAD --dry-run -``` - -## Next Steps - -- [Configuration Reference](./configuration.md) -- [API Documentation](./api.md) -- [Prover Setup](./provers.md) diff --git a/docs/content/index.adoc b/docs/content/index.adoc new file mode 100644 index 0000000..45430fd --- /dev/null +++ b/docs/content/index.adoc @@ -0,0 +1,66 @@ +== echidnabot + +Proof-aware CI bot that automatically verifies mathematical theorems in +your codebase. + +=== What is echidnabot? + +echidnabot is an intelligent CI orchestration layer for formal +mathematics and verified software. When you push code containing formal +proofs—whether in Coq, Lean 4, Agda, Isabelle/HOL, Z3, Metamath, or +other theorem provers—echidnabot automatically dispatches verification +jobs to ECHIDNA Core and reports results directly in your pull requests. + +Think of it as *GitHub Actions for mathematical certainty*. + +=== Key Features + +* *Multi-Platform*: GitHub, GitLab, Bitbucket, Codeberg +* *Multi-Prover*: Coq, Lean, Agda, Isabelle, Z3, Metamath, and more +* *Type-Safe*: Written entirely in Rust with async Tokio +* *GraphQL API*: Query and control via modern API +* *ML-Powered*: Tactic suggestions via ECHIDNA’s Julia ML backend + +=== Quick Start + +[source,bash] +---- +# Install echidnabot +cargo install echidnabot + +# Register a repository +echidnabot register --platform github --repo owner/name + +# Trigger a manual check +echidnabot check --commit HEAD +---- + +=== Architecture + +.... +GitHub/GitLab/Bitbucket + ↓ webhooks + echidnabot (Rust) + ↓ GraphQL + ECHIDNA Core + ├→ Coq, Lean, Agda... + └→ Julia ML + ↓ results + echidnabot + ↓ Check Runs + Platform +.... + +=== Supported Provers + +[cols=",,",options="header",] +|=== +|Tier |Provers |Status +|1 |Agda, Coq, Lean 4, Isabelle/HOL, Z3, CVC5 |Ready +|2 |Metamath, HOL Light, Mizar |MVP +|3 |PVS, ACL2, HOL4 |Planned +|=== + +=== License + +MPL-2.0 OR LicenseRef-Palimpsest-0.5 diff --git a/docs/content/index.md b/docs/content/index.md deleted file mode 100644 index 661b056..0000000 --- a/docs/content/index.md +++ /dev/null @@ -1,68 +0,0 @@ - ---- -title: echidnabot Documentation -date: 2025-01-01 -template: default ---- - -# echidnabot - -Proof-aware CI bot that automatically verifies mathematical theorems in your codebase. - -## What is echidnabot? - -echidnabot is an intelligent CI orchestration layer for formal mathematics and verified software. When you push code containing formal proofs—whether in Coq, Lean 4, Agda, Isabelle/HOL, Z3, Metamath, or other theorem provers—echidnabot automatically dispatches verification jobs to ECHIDNA Core and reports results directly in your pull requests. - -Think of it as **GitHub Actions for mathematical certainty**. - -## Key Features - -- **Multi-Platform**: GitHub, GitLab, Bitbucket, Codeberg -- **Multi-Prover**: Coq, Lean, Agda, Isabelle, Z3, Metamath, and more -- **Type-Safe**: Written entirely in Rust with async Tokio -- **GraphQL API**: Query and control via modern API -- **ML-Powered**: Tactic suggestions via ECHIDNA's Julia ML backend - -## Quick Start - -```bash -# Install echidnabot -cargo install echidnabot - -# Register a repository -echidnabot register --platform github --repo owner/name - -# Trigger a manual check -echidnabot check --commit HEAD -``` - -## Architecture - -``` -GitHub/GitLab/Bitbucket - ↓ webhooks - echidnabot (Rust) - ↓ GraphQL - ECHIDNA Core - ├→ Coq, Lean, Agda... - └→ Julia ML - ↓ results - echidnabot - ↓ Check Runs - Platform -``` - -## Supported Provers - -| Tier | Provers | Status | -|------|---------|--------| -| 1 | Agda, Coq, Lean 4, Isabelle/HOL, Z3, CVC5 | Ready | -| 2 | Metamath, HOL Light, Mizar | MVP | -| 3 | PVS, ACL2, HOL4 | Planned | - -## License - -MPL-2.0 OR LicenseRef-Palimpsest-0.5 diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc new file mode 100644 index 0000000..a61d06b --- /dev/null +++ b/docs/proof-debt.adoc @@ -0,0 +1,22 @@ +== Proof Debt + +Tracks soundness-relevant escape hatches in `+echidnabot+` that the +trusted-base reducer flags as undocumented. Each is retained pending +dedicated cleanup; new occurrences should land with an inline +`+// TRUSTED:+` annotation or an entry below. + +=== Current entries (placeholder) + +The current 2 escape hatches were inherited from earlier scaffolding and +have not yet been individually classified. Tracking issue: filed +alongside this PR. + +* Hatch 1: TBD (file:line) +* Hatch 2: TBD (file:line) + +=== How to populate + +Run the standards trusted-base reducer locally; it lists the offending +file:line tuples. Move each from "`TBD`" to a real entry with a one-line +rationale. When all entries have rationale + cleanup-issue link, this +file is fully load-bearing instead of a placeholder. diff --git a/docs/proof-debt.md b/docs/proof-debt.md deleted file mode 100644 index 4d2624e..0000000 --- a/docs/proof-debt.md +++ /dev/null @@ -1,16 +0,0 @@ - - -# Proof Debt - -Tracks soundness-relevant escape hatches in `echidnabot` that the trusted-base reducer flags as undocumented. Each is retained pending dedicated cleanup; new occurrences should land with an inline `// TRUSTED:` annotation or an entry below. - -## Current entries (placeholder) - -The current 2 escape hatches were inherited from earlier scaffolding and have not yet been individually classified. Tracking issue: filed alongside this PR. - -- Hatch 1: TBD (file:line) -- Hatch 2: TBD (file:line) - -## How to populate - -Run the standards trusted-base reducer locally; it lists the offending file:line tuples. Move each from "TBD" to a real entry with a one-line rationale. When all entries have rationale + cleanup-issue link, this file is fully load-bearing instead of a placeholder. diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc new file mode 100644 index 0000000..f2d56aa --- /dev/null +++ b/docs/tech-debt-2026-05-26.adoc @@ -0,0 +1,88 @@ +== Tech-Debt Audit — echidnabot — 2026-05-26 + +*Source:* estate-wide automated scan 2026-05-26. *Companion:* +https://github.com/hyperpolymath/standards/tree/main/docs/audits[`+hyperpolymath/standards+` +2026-05-26-estate-*-debt audits]. *Combined severity:* `+MEDIUM+`. + +This file records the _raw findings_ — it does not by itself fix the +debt. Each section ends with a '`Recommended next move`' line; closing +the debt is follow-up work. + +=== 1. Proof debt + +Scanner counted the following markers in proof-bearing files of this +repo: + +.... +files= 7 | Coq-Axm/Adm= 1 | Lean-srry/ax= 4 | Agda-pst= 0 | Idr-blv= 1 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 +.... + +*Total markers:* 6. *Severity:* `+>06+`. + +*Marker types* (any non-zero counts above): - Coq `+Axiom+`/`+Admitted+` +— unconditional proof escapes. - Lean `+sorry+`/`+axiom+` — Lean’s +equivalent. - Agda `+postulate+` — accepted axiomatically. - Idris2 +`+believe_me+`/`+assert_total+` — runtime-safe coercion / totality +assumption. - Idris2 top-level `+partial+` — totality-check waived. - F* +`+assume val+`/`+admit_p+` — F* admit. - `+TODO PROOF+` / `+OWED:+` — +self-documented debt markers. - `+unsafePerformIO+`/`+unsafeCoerce+` — +soundness-relevant escape hatches in Haskell/Rust source. + +*Recommended next move:* triage each finding into one of: (a) discharge +by proof, (b) cover with property-tests + a documented refutation +budget, or (c) annotate as a known/necessary axiom (e.g. `+funExt+`) in +`+docs/proof-debt.md+`. + +=== 2. Licence debt + +[cols=",",options="header",] +|=== +|Field |Value +|LICENSE file |`+LICENSE+` +|SPDX header |`+MPL-2.0+` +|Manifest licence |`+MPL-2.0+` +|Body classifier |`+MPL-some+` +|Severity |`+ok+` +|=== + +*Recommended next move:* none for licence. + +=== 3. Documentation debt + +[cols=",",options="header",] +|=== +|Field |Value +|README lines |414 +|`+docs/+` files |5 +|`+docs/+` LoC |548 +|CHANGELOG.md |N +|CONTRIBUTING.md |Y +|CODE_OF_CONDUCT.md |Y +|SECURITY.md |Y +|Severity |`+MEDIUM+` +|=== + +*Recommended next move:* introduce a `+docs/+` directory. The README at +414 lines has likely grown to do the work of `+docs/+` — split it into a +thin README + `+docs/architecture.md+`, `+docs/usage.md+`, etc. +Heavy-wiki exemplars to copy from: `+affinescript+`, `+boj-server+`, +`+echidna+`, `+hypatia+`. + +Additionally: *CHANGELOG.md is missing.* 65% of estate repos lack one — +adopting a CHANGELOG (or auto-generating via `+git-cliff+`) is a +recommended estate-wide follow-up. + +=== Cross-references + +* Estate proof-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md+` +* Estate licence-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md+` +* Estate documentation-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md+` + +''''' + +🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). +This file is informational — closing the debt is follow-up work owned by +the maintainer. diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md deleted file mode 100644 index 0d28f00..0000000 --- a/docs/tech-debt-2026-05-26.md +++ /dev/null @@ -1,72 +0,0 @@ - -# Tech-Debt Audit — echidnabot — 2026-05-26 - -**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`. - -This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work. - -## 1. Proof debt - -Scanner counted the following markers in proof-bearing files of this repo: - -``` -files= 7 | Coq-Axm/Adm= 1 | Lean-srry/ax= 4 | Agda-pst= 0 | Idr-blv= 1 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 -``` - -**Total markers:** 6. **Severity:** `>06`. - -**Marker types** (any non-zero counts above): -- Coq `Axiom`/`Admitted` — unconditional proof escapes. -- Lean `sorry`/`axiom` — Lean's equivalent. -- Agda `postulate` — accepted axiomatically. -- Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality assumption. -- Idris2 top-level `partial` — totality-check waived. -- F\* `assume val`/`admit_p` — F\* admit. -- `TODO PROOF` / `OWED:` — self-documented debt markers. -- `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches in Haskell/Rust source. - -**Recommended next move:** triage each finding into one of: (a) discharge by proof, (b) cover with property-tests + a documented refutation budget, or (c) annotate as a known/necessary axiom (e.g. `funExt`) in `docs/proof-debt.md`. - -## 2. Licence debt - -| Field | Value | -|---|---| -| LICENSE file | `LICENSE` | -| SPDX header | `MPL-2.0` | -| Manifest licence | `MPL-2.0` | -| Body classifier | `MPL-some` | -| Severity | `ok` | - -**Recommended next move:** none for licence. - -## 3. Documentation debt - -| Field | Value | -|---|---| -| README lines | 414 | -| `docs/` files | 5 | -| `docs/` LoC | 548 | -| CHANGELOG.md | N | -| CONTRIBUTING.md | Y | -| CODE_OF_CONDUCT.md | Y | -| SECURITY.md | Y | -| Severity | `MEDIUM` | - -**Recommended next move:** introduce a `docs/` directory. The README at 414 lines has likely grown to do the work of `docs/` — split it into a thin README + `docs/architecture.md`, `docs/usage.md`, etc. Heavy-wiki exemplars to copy from: `affinescript`, `boj-server`, `echidna`, `hypatia`. - -Additionally: **CHANGELOG.md is missing.** 65% of estate repos lack one — adopting a CHANGELOG (or auto-generating via `git-cliff`) is a recommended estate-wide follow-up. - -## Cross-references - -- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` -- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` -- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` - ---- - -🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer. diff --git a/proofs/ECHO-TYPES-AUDIT.adoc b/proofs/ECHO-TYPES-AUDIT.adoc new file mode 100644 index 0000000..0f2277a --- /dev/null +++ b/proofs/ECHO-TYPES-AUDIT.adoc @@ -0,0 +1,76 @@ +== Echo-types audit (2026-06-01) + +Per the estate-wide standing directive: every proof in any sibling repo +with an echo-types link must first audit `+hyperpolymath/echo-types+`, +reuse if applicable, extend upstream WITH proofs if not, then +cross-document. L3 (echo) obligations are load-bearing; L1/L4-only +obligations audit-and-record-as-not-relevant. + +Echo-types layer scheme: *L1* regions / *L2* modality / *L3* echo +(structured residue / fibre shape) / *L4* dyadic (orders, products, +predicates, exhaustivity, monotonicity). + +=== Surface audited + +Four files under `+proofs/+`: + +* `+proofs/coq/trivial_ok.v+` — +`+Theorem identity : forall (A : Prop), A -> A+`. +* `+proofs/coq/admitted_stub.v+` — `+Theorem unproven+` left +`+Admitted.+`, intentionally — fixture for the axiom-scanner CI path. +* `+proofs/lean/trivial_ok.lean+` — +`+theorem identity (A : Prop) (h : A) : A := h+`. +* `+proofs/lean/sorry_stub.lean+` — body `+:= sorry+`, intentionally — +fixture for the Regulator-mode `+sorry+` detection path. + +JSON test fixtures under `+proofs/test_fixtures/+` are CI test inputs, +not obligations. + +`+src/abi/+` (Idris2) is owner-intentional broken (RSR template +scaffold; see estate memo `+echidna_src_abi_namespace_intentional+`) and +out of scope. + +=== Classification + +All four files are *CI dogfood fixtures*, not proof obligations. Two are +trivial L4 identity proofs; two are deliberately incomplete to exercise +the axiom-tracker / Regulator-mode detection of `+Admitted.+` and +`+sorry+` respectively. + +[width="100%",cols="33%,31%,36%",options="header",] +|=== +|Layer |Count |Status +|L1 (regions) |0 |n/a — echidnabot is a CI bot, not a typed-substrate +project + +|L2 (modality) |0 |n/a + +|L3 (echo) |0 |n/a — no fibre / residue / image-factorisation content + +|L4 (dyadic) |2 |trivial identities; fixture purpose only + +|Negative fixtures |2 |`+Admitted.+` / `+sorry+` traps, not obligations +|=== + +=== Echo-types relevance + +*None.* Echidnabot’s proof surface is dogfood for its own proof-aware CI +runners; there is no content that could reuse or extend echo-types’ echo +/ loss-taxonomy / residue / image- factorisation / canonical-identity +stack. + +Audit-and-record-as-not-relevant is discharged by this file. + +=== Cross-doc echo + +* Echidnabot → echo-types: this file. +* Echo-types → echidnabot: not owed (no proof-relevant content flows +back upstream). + +=== Related obligation + +Sibling repo `+echidna+` carries the substantive proof surface; its +echo-types audit lives at `+echidna/docs/PROOF-NEEDS.md+` § "`Echo-types +audit (2026-06-01)`". Two L3-shape obligations are cross-referenced +there (`+ProofStateSerialisation+` roundtrip = EQUIV; +`+ProverKindInjectivity+` = INJ); none flow through echidnabot. diff --git a/proofs/ECHO-TYPES-AUDIT.md b/proofs/ECHO-TYPES-AUDIT.md deleted file mode 100644 index 4c0374c..0000000 --- a/proofs/ECHO-TYPES-AUDIT.md +++ /dev/null @@ -1,73 +0,0 @@ - - -# Echo-types audit (2026-06-01) - -Per the estate-wide standing directive: every proof in any sibling -repo with an echo-types link must first audit -`hyperpolymath/echo-types`, reuse if applicable, extend upstream WITH -proofs if not, then cross-document. L3 (echo) obligations are -load-bearing; L1/L4-only obligations audit-and-record-as-not-relevant. - -Echo-types layer scheme: **L1** regions / **L2** modality / **L3** -echo (structured residue / fibre shape) / **L4** dyadic (orders, -products, predicates, exhaustivity, monotonicity). - -## Surface audited - -Four files under `proofs/`: - -* `proofs/coq/trivial_ok.v` — `Theorem identity : forall (A : Prop), A -> A`. -* `proofs/coq/admitted_stub.v` — `Theorem unproven` left `Admitted.`, - intentionally — fixture for the axiom-scanner CI path. -* `proofs/lean/trivial_ok.lean` — `theorem identity (A : Prop) (h : A) : A := h`. -* `proofs/lean/sorry_stub.lean` — body `:= sorry`, intentionally — - fixture for the Regulator-mode `sorry` detection path. - -JSON test fixtures under `proofs/test_fixtures/` are CI test inputs, -not obligations. - -`src/abi/` (Idris2) is owner-intentional broken (RSR template -scaffold; see estate memo `echidna_src_abi_namespace_intentional`) -and out of scope. - -## Classification - -All four files are **CI dogfood fixtures**, not proof obligations. -Two are trivial L4 identity proofs; two are deliberately incomplete -to exercise the axiom-tracker / Regulator-mode detection of -`Admitted.` and `sorry` respectively. - -| Layer | Count | Status | -|-------|-------|--------| -| L1 (regions) | 0 | n/a — echidnabot is a CI bot, not a typed-substrate project | -| L2 (modality) | 0 | n/a | -| L3 (echo) | 0 | n/a — no fibre / residue / image-factorisation content | -| L4 (dyadic) | 2 | trivial identities; fixture purpose only | -| Negative fixtures | 2 | `Admitted.` / `sorry` traps, not obligations | - -## Echo-types relevance - -**None.** Echidnabot's proof surface is dogfood for its own -proof-aware CI runners; there is no content that could reuse or -extend echo-types' echo / loss-taxonomy / residue / image- -factorisation / canonical-identity stack. - -Audit-and-record-as-not-relevant is discharged by this file. - -## Cross-doc echo - -* Echidnabot → echo-types: this file. -* Echo-types → echidnabot: not owed (no proof-relevant content - flows back upstream). - -## Related obligation - -Sibling repo `echidna` carries the substantive proof surface; its -echo-types audit lives at `echidna/docs/PROOF-NEEDS.md` § "Echo-types -audit (2026-06-01)". Two L3-shape obligations are cross-referenced -there (`ProofStateSerialisation` roundtrip = EQUIV; -`ProverKindInjectivity` = INJ); none flow through echidnabot.