feat(api): add submitProofObligation mutation for hypatia

docs/content/api.adoc

@@ -164,6 +164,39 @@ mutation {
 }
 ----
 
+==== submitProofObligation
+
+Record a free-standing proof obligation. This is the contract hypatia's
+FleetDispatcher and LearningScheduler send. `repo` is an `owner/name` slug
+and need not be registered here. `prover` and `inline` are optional.
+
+[source,graphql]
+----
+mutation {
+  submitProofObligation(input: {
+    repo: "hyperpolymath/echidnabot"
+    claim: "forall x, x = x"
+    context: "pattern P1"
+    prover: COQ
+    inline: true
+  }) {
+    success
+    proofId
+    status
+    newlyRecorded
+    repoRegistered
+  }
+}
+----
+
+`success: true` means the obligation is *stored*, not *proved*. Nothing
+dispatches stored obligations to a prover yet, so `status` is always `PENDING`,
+and `inline` is recorded but not honoured. `proofId` is a UUIDv8 content id
+over `{repo, claim, context, prover}`, so resubmitting the same obligation
+returns the same id with `newlyRecorded: false`. Invalid input (a non-slug
+`repo`, an empty `claim`, a `claim` or `context` over 64 KiB, an unknown
+prover) is a GraphQL error, never `success: false`.
+
 === Types
 
 ==== Platform

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
+);

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 {

src/store/mod.rs

@@ -15,7 +15,9 @@ use crate::adapters::Platform;
 use crate::dispatcher::ProverKind;
 use crate::error::Result;
 use crate::scheduler::JobId;
-use models::{ProofJobRecord, ProofResultRecord, Repository, TacticOutcomeRecord};
+use models::{
+    ProofJobRecord, ProofObligationRecord, ProofResultRecord, Repository, TacticOutcomeRecord,
+};
 
 /// Per-commit coverage view — total proof attempts vs successful ones.
 /// Empty results means no jobs run yet for that commit.
@@ -86,6 +88,13 @@ pub trait Store: Send + Sync {
         limit: usize,
     ) -> Result<Vec<TacticOutcomeRecord>>;
 
+    // Proof obligations (submitProofObligation)
+    /// Persist an obligation; returns `false` if one with the same content id
+    /// already existed (resubmission is idempotent, the first row is kept).
+    async fn record_proof_obligation(&self, obligation: &ProofObligationRecord) -> Result<bool>;
+    /// Fetch one obligation by its content id.
+    async fn get_proof_obligation(&self, id: Uuid) -> Result<Option<ProofObligationRecord>>;
+
     // Utility
     async fn health_check(&self) -> Result<bool>;
 }

src/store/models.rs

@@ -275,3 +275,57 @@ mod tests {
         assert_eq!(goal_fingerprint("any").len(), 64);
     }
 }
+
+/// A proof obligation submitted over GraphQL (`submitProofObligation`).
+///
+/// Obligations come from hypatia's FleetDispatcher and LearningScheduler as
+/// free-standing claim text: no commit and no file, and the repo is a slug
+/// that need not be registered here. That is why this is its own record rather
+/// than a [`ProofJobRecord`], whose `repo_id` must be a registered repository.
+///
+/// The id is a UUIDv8 *content* id over `{repo, claim, context, prover}`, so
+/// resubmitting the same obligation yields the same id. Nothing consumes
+/// stored obligations yet: `status` stays `PENDING` until a dispatcher exists.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct ProofObligationRecord {
+    pub id: Uuid,
+    pub repo_slug: String,
+    pub repo_id: Option<Uuid>,
+    pub claim: String,
+    pub context: String,
+    pub prover: Option<ProverKind>,
+    pub inline_requested: bool,
+    pub status: String,
+    pub created_at: DateTime<Utc>,
+}
+
+impl ProofObligationRecord {
+    /// New `PENDING` obligation whose id is the content id of its fields.
+    pub fn new(
+        repo_slug: String,
+        repo_id: Option<Uuid>,
+        claim: String,
+        context: String,
+        prover: Option<ProverKind>,
+        inline_requested: bool,
+    ) -> Self {
+        let id = crate::ids::content_id(&serde_json::json!({
+            "repo": repo_slug,
+            "claim": claim,
+            "context": context,
+            "prover": prover.as_ref().map(|p| p.to_string()),
+        }))
+        .unwrap_or_else(|_| Uuid::nil());
+        Self {
+            id,
+            repo_slug,
+            repo_id,
+            claim,
+            context,
+            prover,
+            inline_requested,
+            status: "PENDING".to_string(),
+            created_at: Utc::now(),
+        }
+    }
+}