Skip to content

EXPLAINME.adoc

Latest commit

 

History

History
166 lines (134 loc) · 7.28 KB

EXPLAINME.adoc

File metadata and controls

166 lines (134 loc) · 7.28 KB
Raw

echidnabot — Show Me The Receipts

Table of Contents

The README makes claims. This file backs them up with evidence, with caveats where evidence is partial.

Key Claims From README

Production-hardened bridge to ECHIDNA with structured logging, OpenTelemetry tracing, graceful shutdown, and Docker Compose deployment.

— README "Current Status"

Evidence — test count: as of 2026-06-02, cargo test --lib reports 142+ passing (137 pre-existing baseline + 6 new observability + scattered adds from #46/#47/#48/#49/#50/#53/#54/#55/#63/#64/#65/#69/#72/#74/#77/#78). The May-era figure of "129 / 133" is superseded.

Evidence — production hardening, all landed 2026-06-02:

  • Structured JSON logging (#63): ECHIDNABOT_LOG_FORMAT={text,json} env selector; new src/observability.rs module; entire codebase already 100% on tracing (no eprintln!/println! migration required).

  • Graceful shutdown (#64): SIGTERM/SIGINT → axum with_graceful_shutdown → scheduler stop-dispatch → drain in-flight with deadline → registered hooks for db-pool-close + tracer-flush. New src/shutdown.rs (343 lines); 12 tests added. ECHIDNABOT_SHUTDOWN_TIMEOUT_SECS (default 30).

  • OpenTelemetry distributed tracing (#65): OTEL_EXPORTER_OTLP_ENDPOINT env override; 9 spans across webhook/dispatch/echidna-client/executor/ feedback; tracer-shutdown integrated with graceful-shutdown coordinator.

  • Docker Compose stack (#69): compose.yml v2 + Containerfile
    PostgreSQL 16-alpine + optional echidna-stub service; migrations/ scaffolded; docs/deployment.adoc. Closes #60.

  • Codeberg/Forgejo adapter scaffold (#74): new src/adapters/codeberg.rs with PlatformAdapter trait impl, X-Gitea-Signature webhook verification, reqwest + serde_json direct. Refs #62.

  • Canonical-source two-purpose split (#55): documents standalone vs gitbot-fleet/bots/echidnabot/ divergence (109 file delta as of 2026-06-02). Closes #51.

  • Contractile family (#77 + #78): full must|adjust|trust|bust|dust coverage. 15 Must / 11 Adjust / 17 Bust / 13 Dust / 10 Trust checks with probe + severity + recovery. Mirrors echidna#214 pattern.

Evidence — completion percentage: as of 2026-06-02 the core verifier loop + structured-logging + tracing + graceful-shutdown + adapter set + container deployment are all in main. Remaining roadmap items (#57 proof caching / #58 multi-prover consensus / #59 K8s distributed) are explicitly long-term per the roadmap audit. Reading "production-hardened bridge" as the current claim, evidence is full; the older 90% figure was an aggregate across uneven dimensions and is superseded.

Four bot modes: Verifier (block on failure), Advisor (comment only), Consultant (on-demand), Regulator (coverage thresholds).

— README "Bot Modes"

Evidence: the BotMode enum is defined with all four variants (src/modes/mod.rs). Only Verifier is actively wired into the webhook handlers. Advisor / Consultant / Regulator are defined but their webhook-handler dispatch paths were not implemented at last audit — they are selectable via config but do not change behaviour. Session B’s SONNET-TASKS.md Task 2 is the remaining wiring work.

Caveat: do not rely on mode selection for production gating until Task 2 ships. Set mode = "verifier" in .bot_directives/echidnabot.a2ml to match actual behaviour.

12-prover enumeration with tier classification, job dispatch, result parsing, prover health checking.

— README "ECHIDNA Integration"

Evidence: src/dispatcher/echidna_client.rs implements HTTP client against ECHIDNA’s REST + GraphQL APIs. The enum covers 12 provers.

GraphQL contract update 2026-06-02: the seam audit (echidna#180) identified that 3 GraphQL ops echidnabot’s client issued (verifyProof, suggestTactics(prover,context,goalState), proverStatus) were absent from echidna’s server schema. Resolved by echidna#188 which added those ops to MutationRoot/QueryRoot. The existing suggestTactics(proofId, limit) was renamed to suggestTacticsByProofId as part of that work. Echidnabot’s client may benefit from consuming the new typed outcome / mode / smtStatus fields (gitbot-fleet#245 follow-up).

Caveat — upstream prover-count drift: upstream echidna supports many more backends than echidnabot’s ProverKind enum sees (canonical count at echidna/docs/PROVER_COUNT.md). Consumers who need the full surface today should go through the BoJ-only-MCP cartridge at boj-server/cartridges/echidna-llm-mcp. Drift tracked in docs/handover/ and in AGENTIC.a2ml [exceptions.boj-only-mcp].

Check Runs / Comments ← echidnabot ← webhook (push/PR)

— README "The Solution" diagram

Evidence: .github/workflows/echidnabot.yml triggers on proof-file changes across 7 extensions (.v, .lean, .agda, .lagda*, .smt2, .mm, *.thy). PR comments via octocrab GitHub adapter.

Caveat — dogfood proofs missing: echidnabot’s own proofs/ directory is currently empty, so the dogfood CI path exists but is unexercised against real proof files. Session B’s 7b-5 (dogfood proofs Coq/Lean) is the fix.

What Exists But Is Not Yet In README

2026-06-02 production-hardening wave

See "Key Claims From README" §1 above for the full list.

Double-loop learning (Package 7b, landed 2026-04-24)

  • TacticOutcomeRecord table + CRUD (src/store/models.rs, src/store/sqlite.rs)

  • History-weighted tactic reranker (0cc4b4a, b6ef652, 1e26340)

  • Corpus-update writer emitting both delta_*.jsonl (audit) and proof_states_echidnabot_*.jsonl (echidna ingest schema)

Contractile family (2026-06-02)

contractiles/ directory carries five operational contracts with their own error-code namespaces:

  • Mustfile (M###) — physical-state invariants (15 checks)

  • Adjustfile (A###) — adaptive maintenance / migrations (11)

  • Bustfile (B###) — breakage / rollback recipes (17)

  • Dustfile (D###) — fine-grained cleanup (13)

  • Trustfile.hs (T###) — integrity / provenance verification (10)

Run just must-check etc.; each check has a probe + severity + recovery (or adjust / dust action) cross-referenced to sibling recipes for self-healing cascades.

BoJ-only-MCP exception

A documented carve-out from the estate-wide "all MCP through BoJ" rule. See .machine_readable/6a2/AGENTIC.a2ml [exceptions.boj-only-mcp]. Scope: this repo only. Sunset: when BoJ cartridge supports the double-loop feedback protocol.

Dual-truth: monorepo + standalone

echidnabot is registered in the parent echidna repo’s .gitmodules but checked in as regular files (dual-truth pattern, see project_gitbot_fleet_dual_truth_pattern memory). Changes to .machine_readable/ must land in both the standalone repo (this one) and the monorepo copy at echidna/echidnabot/. Proper fix (promote to real submodule, or delete the .gitmodules entry) is tracked in STATE.a2ml’s known-drift section.

What The README Doesn’t Claim

Echidnabot does not itself verify proofs — it dispatches to echidna and reports back. Proof correctness is echidna’s responsibility. If echidna’s /api/verify is down or misconfigured, echidnabot will report "unavailable", never "verified".