Merge branch 'main' into dependabot/cargo/bots/glambot/html5ever-0.39.0

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -8,7 +8,7 @@
     (version "2.0")
     (schema-version "RSR-2026")
     (created "2026-01-04")
-    (updated "2026-04-04T19:00:00Z")
+    (updated "2026-04-05T22:00:00Z")
     (project "gitbot-fleet")
     (repo "https://github.com/hyperpolymath/gitbot-fleet"))
 
@@ -100,6 +100,13 @@
       ("Replace tests/fuzz/placeholder.txt with real libFuzzer harness")))
 
   (session-history
+    (snapshot "2026-04-05-evening"
+      (accomplishments
+        ("Echidnabot: inline-claim mode (A5) — ProofObligationInput.inline=true bypasses clone, verifies claim text directly via echidna /api/verify")
+        ("batch_driver.sh: direct-binary invocation across 16 provers (z3, cvc5, alt-ergo, coq, lean, agda, idris2, vampire, eprover, metamath, cadical, kissat, dafny, why3, fstar, acl2-deferred)")
+        ("batch_driver auto-discovers .ipkg roots for Idris2 project-relative imports")
+        ("Ecosystem VQL->VCL + verisimdb->verisim rename applied (config.rs, fleet-coordinator, dispatch-runner, robot-repo-automaton hypatia client)")
+        ("Live learning loop: 8 PROVEN certs + 2 SANCTIFIED classes over ~1200 proof_attempts rows")))
     (snapshot "2026-04-04"
       (accomplishments
         ("CRG C blitz: added 50+ new tests across robot-repo-automaton + shared-context")

EXPLAINME.adoc

@@ -151,7 +151,7 @@ Additional bots present in `bots/`: `accessibilitybot`, `cipherbot`, `panicbot`
 
 | *Rust* (rhodibot, echidnabot, sustainabot, shared-context, robot-repo-automaton)
 | Primary implementation language for all bots
-| protocol-squisher, verisimdb, ephapax, Stapeln FFI
+| protocol-squisher, verisim, ephapax, Stapeln FFI
 
 | *Hypatia*
 | External scanner whose JSONL findings feed fleet-coordinator.sh

READINESS.md

@@ -65,7 +65,7 @@ These bots are wired in the OTP supervision tree but have limited external valid
 1. **PAT token**: Automated cross-repo dispatch requires a PAT with `repo` scope — currently missing
 2. **Fix scripts**: 310/600 auto-execute entries have null fix_script — recipes exist but no executable
 3. **False positive rate**: ~8% on some pattern categories; kanren context-facts would reduce to ~2-3%
-4. **VQL federation**: Local-only; multi-store federation not implemented
+4. **VCL federation**: Local-only; multi-store federation not implemented
 5. **Neural state persistence**: State dir exists but coordinator hasn't persisted to disk
 
 ---

bots/echidnabot/CHANGELOG.adoc

@@ -0,0 +1,81 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+= Echidnabot Changelog
+:toc: left
+:toclevels: 2
+
+All notable changes to echidnabot are documented here.
+
+== [Unreleased]
+
+=== Changed
+
+==== VQL → VCL + verisimdb → verisim Rename (2026-04-05)
+
+Matches the ecosystem-wide rename. Internal identifiers updated,
+`github.com/hyperpolymath/verisimdb` URLs preserved.
+
+=== Added
+
+==== Inline-Claim Mode (A5, 2026-04-05)
+
+`ProofObligationInput` gains an optional `inline: Bool` flag. When
+`true`, the obligation's `claim` text IS the proof content: `process_job`
+short-circuits before `clone_repo`, fetches the obligation from the
+store, and calls `echidna.verify_proof` directly with the claim text.
+No git clone, no file walk.
+
+Sentinel `inline:<obligation_id>` distinguishes inline jobs from the
+legacy `obligation:<id>` clone path in `ProofJob.file_paths`.
+
+Tested end-to-end against live echidna server:
+  provable Z3 claim  → success=1, 1ms,  "Inline proof verified"
+  unsat Z3 claim     → success=0, 20ms, "Inline proof verification failed"
+
+Unblocks batch drivers and test harnesses that hold proofs in-memory
+and don't want echidnabot to git-clone a repo just to verify one file.
+Used by the Phase E playground at nesy-solver.dev.
+
+==== `batch_driver.sh` — Direct-Binary Prover Invocation
+
+A standalone bash script that walks local proof trees, invokes prover
+binaries directly (bypassing echidna's `/api/verify`, which has a
+parse+export round-trip bug that produces false positives), and POSTs
+outcomes to verisim-api's `/api/v1/proof_attempts`.
+
+Active runners as of 2026-04-05 (**16 provers**): z3, cvc5, alt-ergo,
+coq, lean, agda, idris2, vampire, eprover, metamath, cadical, kissat,
+dafny, why3, fstar, acl2 (runner present, podman wrapper deferred).
+
+Per-prover logic:
+
+* SMT solvers (`z3`, `cvc5`, `alt-ergo`): parse `sat`/`unsat`/`unknown`
+  from output.
+* Interactive provers (`coq`, `lean`, `agda`, `idris2`, `fstar`): cd to
+  file's source root, invoke binary, interpret exit code.
+* Idris2: walks up to find nearest `.ipkg` and uses that as
+  `--source-dir` so project-relative imports resolve.
+* ATPs (`vampire`, `eprover`): parse `% SZS status Theorem|
+  Unsatisfiable|CounterSatisfiable|Timeout`.
+* SAT solvers (`cadical`, `kissat`): exit codes 10=SAT, 20=UNSAT.
+* `metamath`: pipes `read "file"; verify proof *; exit` via stdin,
+  parses `?Error` / "were not proved".
+* `dafny`: parses "finished with N verified, M errors".
+* `why3`: invoked with `-P z3`, parses "Prover result is: Valid".
+
+Environment configuration: `VERISIM_URL`, `VERISIM_TOKEN`, `NOTIFY`
+(notify-send per result), `DRY_RUN`, `MAX_FILES`, `RATE_MS`,
+`TIMEOUT_SEC`, `STRATEGY_TAG`.
+
+Desktop notifications fire on every result (notify-send): urgency
+`critical` on failures, `normal` on success, `low` on unknown.
+
+=== Certificate Landscape (2026-04-05)
+
+After ~1,200 proof_attempts rows across 16 active provers:
+
+* *8 PROVEN* pairs: `safety/{z3,cvc5,vampire,eprover}`,
+  `correctness/{z3,cvc5}`, `linearity/idris2`, `model-check/cadical`.
+* *2 SANCTIFIED* classes: `safety` (4 provers, 282 attempts),
+  `correctness` (2 provers, 198 attempts).

bots/echidnabot/Cargo.lock

@@ -56,7 +56,7 @@ thiserror = "2"
 anyhow = "1"
 tracing = "0.1"
 tracing-subscriber = { version = "0.3", features = ["env-filter", "json"] }
-rand = "0.8"
+rand = "0.9"
 
 # Crypto for webhook verification
 hmac = "0.12"