diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc new file mode 100644 index 0000000..cf07739 --- /dev/null +++ b/AFFIRMATION.adoc @@ -0,0 +1,84 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + += ECHIDNA — Affirmation of Honest State +Jonathan D.A. Jewell +:revdate: 2026-06-15 +:toc: + +A point-in-time honesty attestation, per the RSR / CCCP audit gate +(`AUDIT.adoc` in `rsr-template-repo`): an affirmation that ECHIDNA's public +claims do not outrun the proofs, tests, and artefacts that back them, with a +plain disclosure of what is verified, what is aspirational, and what is +known-debt as of the date above. + +Companion to `RSR_COMPLIANCE.adoc` (hard-rule compliance) and `EXPLAINME.adoc` +(receipts for README claims). Canonical live state: `CHANGELOG.md` + the git +log + open issues. + +[NOTE] +==== +The canonical standards AFFIRMATION template was not reachable from the +authoring session (outside repo scope at the time). This document follows the +audit-gate rules in `rsr-template-repo/AUDIT.adoc` and the conventions of +`RSR_COMPLIANCE.adoc`; reconcile it against the canonical template when +available. +==== + +== Affirmations + +. *Claims do not outrun artefacts.* Every "verified" item below is reproduced in + CI or by a named test/proof. Direction-of-travel items are labelled + aspirational and make no readiness claim. +. *No hidden proof debt.* Known gaps are disclosed under "Known debt" below, not + buried; where stubs exist they are named. +. *Stability discipline.* ECHIDNA is *not* affirmed `stable` or `v1.0.0`; the + real release line is in `CHANGELOG.md`. +. *Critical Reception Grade.* CRG-C is complete (unit + smoke + build + P2P + + E2E + contract + aspect + benchmarks baselined, per + `.machine_readable/6a2/STATE.a2ml`); CRG-B criteria are populated but B is + *not* formally affirmed here. + +== Verified as of 2026-06-15 (green / reproduced) + +* Multi-language dogfood proof corpus — Coq, Lean 4, Agda, Idris2 — type-checks + in CI (`dogfood-proofs-ci.yml` + `idris2-abi-ci.yml`); merged via #234 / #244. +* Idris2 ABI carries zero `believe_me` / `assert_total` / `postulate` + (enforced by `idris2-abi-ci.yml`). +* Every CI workflow job carries an explicit `timeout-minutes` bound (#247). +* Governance gates green on `main`: REUSE/SPDX, workflow-linter, A2ML manifest + validation, K9 contracts, SPARK theatre gate. + +== Aspirational (direction of travel — NOT done) + +* ML-at-scale: GNN/Transformer training on the real corpus (scaffolds present, + weights not trained on real data). +* Cap'n Proto IPC; full Chapel-parallel dispatch; coprocessor hardware paths. +* Stages 5–8 of `docs/ROADMAP.md` (distributed, cross-prover semantics, + sovereign tooling, self-verified kernel). + +== Known debt (disclosed, not hidden) + +* `--features verisim`: 22 compile errors; feature gated off by default (#245). +* `formal-verification.yml` `creusot-verify` red — `alt-ergo` not + apt-installable (#250). +* `src/rust/main.rs` SPDX-FileCopyrightText hook blocks commits to that file + (#216) — owner-only fix; gates the 13-adapter dispatcher branch. +* Prover-count drift across surfaces vs `docs/PROVER_COUNT.md` (#251). +* RSR divergences vs the standards repo: stale `salt/` Python wording, and the + polyglot language set not yet declared as an out-of-template adaptation + (#254). The RSR `hooks/` requirement is addressed in the change that + introduces this file. + +== Scope + +This affirmation covers `hyperpolymath/echidna`. `echidnabot` maintains its own +state; its `proofs/coq/admitted_stub.v` and `proofs/lean/sorry_stub.lean` are +*intentional* dogfood-CI failures, disclosed in its `CLAUDE.md`. + +== Affirmed + +Affirmed during the 2026-06-13/15 estate-maintenance session (Claude Code), +pending owner counter-sign. + +Owner: Jonathan D.A. Jewell . diff --git a/docs/handover/SESSION-HANDOFF-2026-06-15.md b/docs/handover/SESSION-HANDOFF-2026-06-15.md new file mode 100644 index 0000000..481c2e6 --- /dev/null +++ b/docs/handover/SESSION-HANDOFF-2026-06-15.md @@ -0,0 +1,72 @@ + + +# Session handoff — 2026-06-15 + +Snapshot of the estate-reconciliation work (echidna + echidnabot) for the next +session. Master tracker **echidna#238 is closed**; remaining work is split into +discrete issues, captured below by normative tier (MUST / INTEND / WISH). + +Legend: **done** = merged this campaign · **open** = tracked issue · **owner** = +needs the repo owner (policy/SPDX/branch-delete) · **blocked** = gated on another item. + +## Status — ECHIDNA + +| Tier | Item | Status | Ref | +|------|------|--------|-----| +| MUST | Proof corpus repaired + CI-gated (Coq/Lean/Agda/Idris2) | done | #234 / #244 | +| MUST | Every workflow job has `timeout-minutes` | done | #247 (closed #241) | +| MUST | `hooks/` dir (RSR pre-commit-enforcement requirement) | this PR | #254·2 | +| MUST | `src/rust/main.rs` SPDX hook blocks *all* commits to it | open · owner 1-liner | #216 | +| MUST | `creusot-verify` CI red (`alt-ergo` not apt-installable) | open | #250 | +| MUST | `salt/`/Python rule stale vs standards (no `salt/` exists) | open · owner doc | #254·1 | +| MUST | Prover-count drift (48/105/113/128 vs `PROVER_COUNT.md`) | open · owner (R5a) | #251 | +| INTEND | `--features verisim` 22 compile errors | open | #245 | +| INTEND | machine_readable + contractile currency audit | open | #252 | +| INTEND | Reconcile remaining RSR divergences (lang-tier undeclared) | open | #254·3 | +| INTEND | Delete 6 reconciled stale branches | open · owner (proxy 403) | #253 | +| INTEND | Wire 13 dispatcher adapters | blocked by #216 | `feat/corpus-dispatcher-all-17-adapters` | +| INTEND | Structural-drift stale paths; ReScript→AffineScript migration | open | #242, #240, #266 | +| WISH | Split Rust/FFI/proof safety alerts by risk class | open | #239 | +| WISH | GNN-at-scale; Cap'n Proto / Chapel-full / coprocessors; 8-stage endpoint | aspirational | `docs/ROADMAP.md` | + +## Status — ECHIDNABOT + +| Tier | Item | Status | Ref | +|------|------|--------|-----| +| MUST | README test-count 129→184 + ProverSlug | done | #86 | +| MUST | `echidna-fuzz` rate-limit-check timeout | done | #89 | +| MUST | `LICENSE` missing SPDX header (Licence-consistency fails every PR) | open · owner-only | #87 | +| MUST | `.gitignore`/`.gitattributes` PMPL→MPL SPDX drift | open · owner-only | #83 | +| MUST | `gitbot-shared-context` path dep (no bare-clone build) | accepted debt — do not fix | #18 | +| MUST-NOT | `admitted_stub.v` / `sorry_stub.lean` | intentional dogfood failures — leave | — | +| INTEND | Post-checkpoint hygiene (STATE dual-truth, SESSION_SUMMARY, contractiles, `.scm`, SONNET-TASKS, `curl\|sh`) | open | #88 | +| INTEND | `proof-debt.md` TBD→rationale; cflite shared-context vendoring | open | #68, #67 | +| WISH | Codeberg adapter; pre-built Podman images; K8s distributed; full bot-modes | aspirational | #62, #61, #59 | + +## Hard constraints (carry forward — these OVERRIDE defaults) +- **Languages:** no Python (the `salt/` exception was removed upstream), no TypeScript, no Go. Use Rust / Julia / Idris2 / Agda / Zig / Chapel / AffineScript / Nickel per `CLAUDE.md`. +- **Build:** Justfile primary (RSR-H14). **Containers:** Podman + `Containerfile`, never Docker/`Dockerfile` (RSR-H15). **Packaging:** Guix; **no Nix** (`flake.nix`/`flake.lock` banned estate-wide). +- **SPDX / LICENSE edits are owner-only, manual, file-by-file** (#216 / #83 / #87) — never automate; automated sweeps must not touch licence headers. +- **echidnabot dogfood stubs** (`admitted_stub.v`, `sorry_stub.lean`) are intentional failures — never "fix". +- **echidnabot** cannot `cargo build` from a bare clone (path-dep #18) — for code work use a `gitbot-fleet` monorepo checkout; doc work is fine standalone. +- **Branch ref-deletes return HTTP 403** via the session git proxy and the GitHub MCP has no delete-branch tool, so branch cleanup (#253) is **owner-only**. +- Develop on `claude/` branches; open **draft** PRs; be **frugal** with GitHub comments. + +## Prompt for the next session + +Copy-paste the block below to the next Claude: + +> Continue estate maintenance on `hyperpolymath/echidna` + `hyperpolymath/echidnabot`. +> +> **First read:** echidna issue #238 (closed master checkpoint), `docs/handover/SESSION-HANDOFF-2026-06-15.md`, `AFFIRMATION.adoc`, and both repos' `CLAUDE.md` (their rules OVERRIDE defaults). +> +> **Where things stand:** the multi-language proof corpus is repaired, CI-gated, and green on `main`; the master checkpoint is closed; all this campaign's PRs merged. Remaining work is in discrete issues, grouped MUST / INTEND / WISH in the handoff doc. +> +> **Pick up in this order:** +> 1. *Flag to the owner (don't auto-do — SPDX/policy/branch-delete):* #216 (main.rs SPDX hook — unblocks the `feat/corpus-dispatcher-all-17-adapters` branch), echidnabot #87 + #83 (LICENSE/SPDX), #251 (prover-count — fix the GitHub repo description first), #253 (delete the 6 stale branches). +> 2. *Doable now, as draft PRs:* #250 (install `alt-ergo` via opam in `formal-verification.yml`), #245 (`--features verisim` — 22 compile errors), #252 (machine_readable + contractile currency audit — run a Haiku scout before bulk edits), #254 (reconcile the RSR divergences: drop the stale `salt/` wording, declare the polyglot language set as an out-of-template adaptation), echidnabot #88 (hygiene). +> +> **Honor the hard constraints** in the handoff doc (SPDX = owner-only; dogfood stubs intentional; Podman/Justfile/Guix; no Python/TS/Go). Develop on `claude/` branches, open draft PRs, keep GitHub comments frugal. + +--- +_Generated 2026-06-15. Source of truth for status: the linked issues + `CHANGELOG.md` + git log; this snapshot drifts._ diff --git a/hooks/README.md b/hooks/README.md new file mode 100644 index 0000000..e3af2e6 --- /dev/null +++ b/hooks/README.md @@ -0,0 +1,24 @@ + + +# Git hooks + +Governance hooks for ECHIDNA — the RSR `hooks/` requirement (pre-commit +enforcement). Each wraps the same `just` gate CI runs, so commits and pushes +fail fast on the same checks. + +| Hook | Runs | Covers | +|------|------|--------| +| `pre-commit` | `just pre-commit` | fmt-check + lint (REUSE/SPDX + rustfmt + clippy) + test | +| `pre-push` | `just validate-rsr` | RSR compliance gate (RSR-H12) | + +## Enable + +Hooks are opt-in. Point git at this directory once per clone: + +```bash +git config core.hooksPath hooks +``` + +Disable with `git config --unset core.hooksPath`. Each hook no-ops with a +warning if `just` is not on PATH, so a missing toolchain never hard-blocks a +commit. diff --git a/hooks/pre-commit b/hooks/pre-commit new file mode 100755 index 0000000..db881a8 --- /dev/null +++ b/hooks/pre-commit @@ -0,0 +1,16 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# ECHIDNA pre-commit hook — satisfies the RSR hooks/ requirement +# (pre-commit enforcement). Wraps the same fast gate CI runs. +# Enable per clone: git config core.hooksPath hooks +set -euo pipefail + +if ! command -v just >/dev/null 2>&1; then + echo "pre-commit: 'just' not on PATH (RSR-H14 build tool); skipping gate." >&2 + exit 0 +fi + +# fmt-check + lint (REUSE/SPDX + rustfmt + clippy) + test — Justfile `pre-commit`. +exec just pre-commit diff --git a/hooks/pre-push b/hooks/pre-push new file mode 100755 index 0000000..5ca7b02 --- /dev/null +++ b/hooks/pre-push @@ -0,0 +1,14 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# ECHIDNA pre-push hook — RSR compliance gate (RSR-H12). +# Enable per clone: git config core.hooksPath hooks +set -euo pipefail + +if ! command -v just >/dev/null 2>&1; then + echo "pre-push: 'just' not on PATH; skipping RSR gate." >&2 + exit 0 +fi + +exec just validate-rsr