chore(echidnabot): bump vendored copy to faeb280 (#168, #169) (#603)

## Summary

Re-pins the vendored `bots/echidnabot` copy to
`hyperpolymath/echidnabot` `main` @ `faeb2808` (was `bf2c0ffc`, 2
commits behind), using the repo's own `scripts/sync-vendored-bot.sh
echidnabot --sync --rev faeb2808efcf1fc8149afc5811182cb14bf79091`.

It brings in:
- **hyperpolymath/echidnabot#168:** echidna integration, the
prove-result contract, UUID minting (`src/ids.rs`: v7 records, v8
content ids) and a CI repair.
- **hyperpolymath/echidnabot#169:** the `submitProofObligation` GraphQL
mutation. hypatia's FleetDispatcher and LearningScheduler send this
contract (hyperpolymath/hypatia#911). Until this bump lands, a
fleet-deployed echidnabot rejects every hypatia dispatch as an unknown
field.

Scope:
- Only `bots/echidnabot/**` changes (34 files, +2065/−241).
- `FLEET-SYNC.json` changes `rev` only.
- 0 files deleted, so the Repo Integrity Guard needs no
`[mass-delete-ok]`.
- 4 files added: `migrations/20261008000001_proof_obligations.sql`,
`src/dispatcher/prove_result.rs`, `src/ids.rs`, `tests/live_echidna.rs`.

No issue to close. This is the follow-up to
hyperpolymath/echidnabot#169.

## Type of change

- [ ] 🐛 Bug fix — not a fix in this repo; it re-pins vendored upstream
code.
- [ ] ✨ New feature — the feature (`submitProofObligation`) was built
and reviewed upstream in hyperpolymath/echidnabot#169; this PR only
re-vendors it.
- [ ] 💥 Breaking change — no existing fleet behaviour changes. The
upstream GraphQL change is additive.
- [ ] 🕳️ Soundness fix — not applicable.
- [ ] 📖 Documentation — no fleet docs change. The vendored copy carries
no `docs/` (not in `include`).
- [ ] 🧹 Refactor / tech debt — not applicable.
- [ ] ⚡ Performance — not applicable.
- [x] 🔧 Build / CI / tooling — a vendored-dependency pin bump
(`FLEET-SYNC.json` rev plus the synced tree).

## 📌 New pins

- **PR head SHA: `cdfa0b813f44a46be8dd149edd02d32f65cbe1d8`**
- **`bots/echidnabot/FLEET-SYNC.json` `rev`:
`bf2c0ffc9f5faee3c2072b516855a045400ac247` →
`faeb2808efcf1fc8149afc5811182cb14bf79091`** (`hyperpolymath/echidnabot`
`main` head, the signed squash merge of #169).
- Vendored `bots/echidnabot/Cargo.lock` records, as resolved upstream:
- **added `echidna-core-spark` 0.1.0**, git
`https://github.com/hyperpolymath/echidna` **rev
`b761b3a832981be51d4e88076ef1b90fe5037e9c`**
  - **added `serde_json_canonicalizer` 0.3.2**
  - **added `ryu-js` 1.0.3**
  - **`async-trait` 0.1.89 → 0.1.92**
  - **`rustls` 0.23.40 → 0.23.45**
  - **`rustls-webpki` 0.103.13 → 0.103.15**
- No action `uses:` SHAs, `actions.lock` entries or container digests
change.

## How has this been verified?

All commands were run in the PR worktree at the head above:
- `scripts/sync-vendored-bot.sh echidnabot --check` printed
"bots/echidnabot matches
https://github.com/hyperpolymath/echidnabot@faeb2808… (79 entries)" and
exited **0**.
- `bash scripts/tests/sync-vendored-bot.sh` reported **21 passed, 0
failed**.
- `jq -cS . bots/echidnabot/FLEET-SYNC.json` is byte-identical to the
file, so the lock stays in canonical form.
- `git diff --cached --name-only | grep -v '^bots/echidnabot/'` printed
nothing. `git diff --cached --diff-filter=D` lists 0 files.
- `git log -1 --show-signature` reports a good ED25519 signature, as
`required_signatures` on `main` needs.
- **Not built here.** Fleet CI does not compile `bots/echidnabot`:
`rust.yml` builds robot-repo-automaton, shared-context, dashboard and
rhodibot; CodeQL is `actions` / `build-mode: none`. The build evidence
for this tree is therefore upstream CI on `faeb2808`, which is green
apart from skipped deploy/automerge/coverage jobs. `squabble
verify-satisfied hyperpolymath/echidnabot 169` returned `done: true`.

## Checklist

- [x] My commits are **signed**: SSH ED25519 key, verified locally with
`git log --show-signature`.
- [x] I ran the project's own checks/tests locally and they pass: the
drift `--check` and the sync script's planted-control suite, as above.
- [x] New files carry the correct `SPDX-License-Identifier`: all 4 added
vendored files are `MPL-2.0`, as written upstream. Nothing was
relicensed.
- [x] Docs are updated, and no public claim now overstates what the code
does. No fleet doc describes the vendored version. Upstream's `api.adoc`
says `submitProofObligation` stores an obligation and does not prove it
(`status` is always `PENDING`).
- [x] I have not introduced a soundness hole. This is a byte-for-byte
re-vendor of reviewed upstream code, and the drift gate enforces that.

## Notes for reviewers

- `.github/dependabot.yml` deliberately leaves out `/bots/echidnabot`.
Dependency bumps for it land upstream and arrive here by re-pinning, as
in this PR.
- The new git dependency `echidna-core-spark` is pinned by full rev in
both the vendored `Cargo.toml` and `Cargo.lock`.

### Deferred red checks (none required; all also red on `main` @
`72970698`)

This PR touches no workflow and no `actions.lock`. Each red below fails
identically on `main`:
- `actions.lock is in sync with the workflow YAML`: deferred to #604.
#595 bumped `smtp-notify-action` to v0.5.0 without relocking.
- `governance / Actions lockfile verify`: deferred to #604, same cause.
- `scorecard / Run Scorecard PR`: deferred to #604, same cause.
Reconciliation fails on `push-email-notify.yml`.
- `Codeac analyze results` (legacy status): deferred to #590. The
service cannot analyse the repo.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_015bTuGfwCcvjrmNFejydTML

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Author: hyperpolymath

bots/echidnabot/Cargo.lock

@@ -28,6 +28,19 @@ path = "src/main.rs"
 # Fleet coordination
 gitbot-shared-context = { version = "0.1.0", git = "https://github.com/hyperpolymath/gitbot-fleet", rev = "40ef6bf1a43813948476d33c764e3405adc950c2" }
 
+# ECHIDNA trust kernel. Canonical trust-level algorithm and source-level
+# axiom scanner, shared with ECHIDNA so echidnabot no longer re-implements
+# them. Pinned by full rev (immutable). At this rev the crate is still named
+# `echidna-core-spark`; it is being renamed `echidna-core-creusot` upstream,
+# and the trust types are meant to move into `echidna-core` proper. Follow-up:
+# re-point this line once that lands on echidna `main` (see
+# docs/ECHIDNA-INTEGRATION.adoc).
+echidna-core-spark = { git = "https://github.com/hyperpolymath/echidna", rev = "b761b3a832981be51d4e88076ef1b90fe5037e9c" }
+
+# Minimum-version handshake with the ECHIDNA server.
+semver = "1"
+
+
 # Async runtime
 tokio = { version = "1", features = ["full"] }
 
@@ -70,7 +83,12 @@ reqwest = { version = "0.12", default-features = false, features = ["json", "rus
 
 # Utilities
 async-trait = "0.1"
-uuid = { version = "1", features = ["v4", "serde"] }
+# v7 for records, v8 for content ids; minted only in src/ids.rs.
+uuid = { version = "1.10", features = ["v7", "v8", "serde"] }
+# RFC 8785 (JCS) canonical bytes for src/ids.rs content ids. The estate
+# crate hyperpolymath/ijson-jcs is not public, so a public build cannot
+# depend on it; swap once it is (docs/ECHIDNA-INTEGRATION.adoc).
+serde_json_canonicalizer = "0.3"
 chrono = { version = "0.4", features = ["serde"] }
 thiserror = "2"
 anyhow = "1"

bots/echidnabot/Cargo.toml

@@ -1 +1 @@
-{"fleet_owned":["CANONICAL_SOURCE.adoc","FLEET-SYNC.json"],"include":[".cargo","Cargo.lock","Cargo.toml","Containerfile","LICENSE","LICENSES","README.adoc","benches","config","echidnabot.example.toml","fuzz","migrations","proofs","src","tests"],"repo":"https://github.com/hyperpolymath/echidnabot","rev":"bf2c0ffc9f5faee3c2072b516855a045400ac247","schema":"gitbot-fleet.vendor-sync/1","upstream_branch":"main"}
+{"fleet_owned":["CANONICAL_SOURCE.adoc","FLEET-SYNC.json"],"include":[".cargo","Cargo.lock","Cargo.toml","Containerfile","LICENSE","LICENSES","README.adoc","benches","config","echidnabot.example.toml","fuzz","migrations","proofs","src","tests"],"repo":"https://github.com/hyperpolymath/echidnabot","rev":"faeb2808efcf1fc8149afc5811182cb14bf79091","schema":"gitbot-fleet.vendor-sync/1","upstream_branch":"main"}

bots/echidnabot/FLEET-SYNC.json

@@ -72,7 +72,7 @@ echidnabot init-db
 
 # Start the webhook server
 export DATABASE_URL=sqlite:echidnabot.db
-export ECHIDNA_URL=http://localhost:8080
+export ECHIDNA_URL=http://127.0.0.1:8081
 echidnabot serve --port 8080
 ----
 

bots/echidnabot/README.adoc

@@ -24,7 +24,6 @@ use sha2::Sha256;
 // one; CI runs clippy with `-D warnings`, so the re-export is an error here.
 use std::hint::black_box;
 use std::net::{IpAddr, Ipv4Addr};
-use uuid::Uuid;
 
 // ──────────────────────────────────────────────────────────────────────────────
 // HMAC-SHA256 webhook signature verification
@@ -158,7 +157,7 @@ fn bench_goal_fingerprint(c: &mut Criterion) {
 // ──────────────────────────────────────────────────────────────────────────────
 
 fn bench_proof_job_new(c: &mut Criterion) {
-    let repo = Uuid::new_v4();
+    let repo = echidnabot::ids::new_record_id();
     let prover = ProverKind::new("coq");
     let files = vec![
         "theories/Main.v".to_string(),

bots/echidnabot/benches/echidnabot_bench.rs

@@ -91,8 +91,8 @@ let Config = {
     max_connections = 5,
   },
   echidna = {
-    endpoint = "http://localhost:8080/graphql",
-    rest_endpoint = "http://localhost:8080",
+    endpoint = "http://127.0.0.1:8081/",
+    rest_endpoint = "http://127.0.0.1:8081",
     mode = 'auto,
     timeout_seconds = 120,
   },

bots/echidnabot/config/echidnabot.ncl

@@ -17,9 +17,9 @@ max_connections = 5
 
 [echidna]
 # ECHIDNA Core GraphQL endpoint
-endpoint = "http://localhost:8080/graphql"
+endpoint = "http://127.0.0.1:8081/"
 # ECHIDNA Core REST endpoint
-rest_endpoint = "http://localhost:8080"
+rest_endpoint = "http://127.0.0.1:8081"
 # API mode: auto, graphql, rest
 mode = "auto"
 # Timeout for proof verification (seconds)

bots/echidnabot/echidnabot.example.toml

@@ -0,0 +1,19 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+--
+-- proof_obligations — obligations received via the `submitProofObligation`
+-- GraphQL mutation (hypatia FleetDispatcher / LearningScheduler).
+-- Mirrors the SQLite DDL emitted at runtime by `SqliteStore::run_migrations`.
+-- `id` is a UUIDv8 content id; `repo_id` is nullable because the sender
+-- names a repo slug that need not be registered with echidnabot.
+CREATE TABLE IF NOT EXISTS proof_obligations (
+    id                  TEXT PRIMARY KEY,
+    repo_slug           TEXT NOT NULL,
+    repo_id             TEXT REFERENCES repositories(id),
+    claim               TEXT NOT NULL,
+    context             TEXT NOT NULL,
+    prover              TEXT,
+    inline_requested    INTEGER NOT NULL,
+    status              TEXT NOT NULL,
+    created_at          TEXT NOT NULL
+);

bots/echidnabot/migrations/20261008000001_proof_obligations.sql

@@ -14,7 +14,8 @@ use crate::dispatcher::{
 };
 use crate::scheduler::{JobPriority, JobScheduler};
 use crate::store::models::{
-    goal_fingerprint, ProofJobRecord, Repository as StoreRepository, TacticOutcomeRecord,
+    goal_fingerprint, ProofJobRecord, ProofObligationRecord, Repository as StoreRepository,
+    TacticOutcomeRecord,
 };
 use crate::store::Store;
 
@@ -385,6 +386,41 @@ pub struct RepoSettingsInput {
     pub auto_comment: Option<bool>,
 }
 
+/// Upper bound on `claim` and `context`, in bytes. The endpoint has no auth,
+/// so a cap keeps one request from writing an unbounded row.
+pub const MAX_OBLIGATION_FIELD_BYTES: usize = 64 * 1024;
+
+/// Input for submitting a proof obligation (hypatia's wire contract)
+#[derive(async_graphql::InputObject)]
+pub struct SubmitProofObligationInput {
+    /// Repository slug `owner/name`; it need not be registered here
+    pub repo: String,
+    /// The claim to be proved, as prover-agnostic text
+    pub claim: String,
+    /// Free-text context for the claim
+    pub context: String,
+    /// Prover hint; absent means "echidnabot chooses"
+    pub prover: Option<ProverKind>,
+    /// Sender asks for inline verification. Recorded, NOT acted on yet
+    pub inline: Option<bool>,
+}
+
+/// Result of `submitProofObligation`
+#[derive(SimpleObject, Clone)]
+pub struct ProofObligationPayload {
+    /// `true` means the obligation is persisted. It does NOT mean proved:
+    /// failures are GraphQL errors, never `success: false`
+    pub success: bool,
+    /// UUIDv8 content id of the obligation (stable across resubmission)
+    pub proof_id: ID,
+    /// Always `PENDING` today: no dispatcher consumes obligations yet
+    pub status: String,
+    /// `false` when an identical obligation was already stored
+    pub newly_recorded: bool,
+    /// Whether `repo` matched a repository registered on GitHub here
+    pub repo_registered: bool,
+}
+
 #[Object]
 impl MutationRoot {
     /// Register a repository for monitoring
@@ -585,6 +621,69 @@ impl MutationRoot {
             .map_err(|e| async_graphql::Error::new(e.to_string()))?;
         Ok(TacticOutcome::from(record))
     }
+
+    /// Accept a proof obligation from hypatia and persist it as `PENDING`.
+    ///
+    /// Accepted is not proved: nothing dispatches stored obligations to a
+    /// prover yet, and `inline: true` is recorded but not honoured. Invalid
+    /// input or a store failure is returned as a GraphQL error, because one of
+    /// the two senders reads only `errors` and ignores `success`.
+    async fn submit_proof_obligation(
+        &self,
+        ctx: &Context<'_>,
+        input: SubmitProofObligationInput,
+    ) -> async_graphql::Result<ProofObligationPayload> {
+        let state = ctx.data::<GraphQLState>()?;
+
+        let (owner, name) = match input.repo.split_once('/') {
+            Some((o, n)) if !o.is_empty() && !n.is_empty() && !n.contains('/') => (o, n),
+            _ => {
+                return Err(async_graphql::Error::new(format!(
+                    "repo must be an owner/name slug, got {:?}",
+                    input.repo
+                )))
+            }
+        };
+        if input.claim.trim().is_empty() {
+            return Err(async_graphql::Error::new("claim must not be empty"));
+        }
+        for (field, value) in [("claim", &input.claim), ("context", &input.context)] {
+            if value.len() > MAX_OBLIGATION_FIELD_BYTES {
+                return Err(async_graphql::Error::new(format!(
+                    "{field} exceeds {MAX_OBLIGATION_FIELD_BYTES} bytes"
+                )));
+            }
+        }
+
+        let repo_id = state
+            .store
+            .get_repository_by_name(crate::adapters::Platform::GitHub, owner, name)
+            .await
+            .map_err(|e| async_graphql::Error::new(e.to_string()))?
+            .map(|r| r.id);
+
+        let record = ProofObligationRecord::new(
+            input.repo.clone(),
+            repo_id,
+            input.claim,
+            input.context,
+            input.prover.map(map_prover_kind_to_core),
+            input.inline.unwrap_or(false),
+        );
+        let newly_recorded = state
+            .store
+            .record_proof_obligation(&record)
+            .await
+            .map_err(|e| async_graphql::Error::new(e.to_string()))?;
+
+        Ok(ProofObligationPayload {
+            success: true,
+            proof_id: ID::from(record.id.to_string()),
+            status: record.status,
+            newly_recorded,
+            repo_registered: repo_id.is_some(),
+        })
+    }
 }
 
 impl From<StoreRepository> for Repository {