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

bots/echidnabot/Cargo.toml

@@ -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/FLEET-SYNC.json

@@ -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/README.adoc

@@ -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/benches/echidnabot_bench.rs

@@ -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/config/echidnabot.ncl

@@ -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/echidnabot.example.toml

@@ -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/migrations/20261008000001_proof_obligations.sql

@@ -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/src/api/graphql.rs

@@ -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 {