diff --git a/docs/content/api.adoc b/docs/content/api.adoc index 4dc224a..07896c0 100644 --- a/docs/content/api.adoc +++ b/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 diff --git a/migrations/20261008000001_proof_obligations.sql b/migrations/20261008000001_proof_obligations.sql new file mode 100644 index 0000000..3b423f6 --- /dev/null +++ b/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 +); diff --git a/src/api/graphql.rs b/src/api/graphql.rs index f26f842..9b6b0a1 100644 --- a/src/api/graphql.rs +++ b/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, } +/// 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, + /// Sender asks for inline verification. Recorded, NOT acted on yet + pub inline: Option, +} + +/// 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 { + let state = ctx.data::()?; + + 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 for Repository { diff --git a/src/store/mod.rs b/src/store/mod.rs index b26a819..11a77fe 100644 --- a/src/store/mod.rs +++ b/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>; + // 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; + /// Fetch one obligation by its content id. + async fn get_proof_obligation(&self, id: Uuid) -> Result>; + // Utility async fn health_check(&self) -> Result; } diff --git a/src/store/models.rs b/src/store/models.rs index 6164316..c32d567 100644 --- a/src/store/models.rs +++ b/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, + pub claim: String, + pub context: String, + pub prover: Option, + pub inline_requested: bool, + pub status: String, + pub created_at: DateTime, +} + +impl ProofObligationRecord { + /// New `PENDING` obligation whose id is the content id of its fields. + pub fn new( + repo_slug: String, + repo_id: Option, + claim: String, + context: String, + prover: Option, + 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(), + } + } +} diff --git a/src/store/sqlite.rs b/src/store/sqlite.rs index 946f017..8cb699b 100644 --- a/src/store/sqlite.rs +++ b/src/store/sqlite.rs @@ -195,6 +195,26 @@ impl SqliteStore { .execute(&self.pool) .await?; + // Proof obligations from `submitProofObligation`. `repo_id` is nullable: + // the sender names a repo slug that need not be registered here. + sqlx::query( + r#" + 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 + ) + "#, + ) + .execute(&self.pool) + .await?; + Ok(()) } } @@ -540,6 +560,42 @@ impl Store for SqliteStore { rows.into_iter().map(|r| r.try_into()).collect() } + /// Insert-or-ignore on the content id; `true` only for a new row. + async fn record_proof_obligation(&self, obligation: &ProofObligationRecord) -> Result { + let done = sqlx::query( + r#" + INSERT OR IGNORE INTO proof_obligations ( + id, repo_slug, repo_id, claim, context, prover, + inline_requested, status, created_at + ) VALUES (?, ?, ?, ?, ?, ?, ?, ?, ?) + "#, + ) + .bind(obligation.id.to_string()) + .bind(&obligation.repo_slug) + .bind(obligation.repo_id.map(|id| id.to_string())) + .bind(&obligation.claim) + .bind(&obligation.context) + .bind(obligation.prover.as_ref().map(|p| p.to_string())) + .bind(obligation.inline_requested) + .bind(&obligation.status) + .bind(obligation.created_at.to_rfc3339()) + .execute(&self.pool) + .await?; + + Ok(done.rows_affected() == 1) + } + + /// Look up one obligation by content id. + async fn get_proof_obligation(&self, id: Uuid) -> Result> { + let row: Option = + sqlx::query_as("SELECT * FROM proof_obligations WHERE id = ?") + .bind(id.to_string()) + .fetch_optional(&self.pool) + .await?; + + row.map(|r| r.try_into()).transpose() + } + async fn health_check(&self) -> Result { let result: (i32,) = sqlx::query_as("SELECT 1").fetch_one(&self.pool).await?; Ok(result.0 == 1) @@ -778,6 +834,41 @@ impl TryFrom for TacticOutcomeRecord { } } +#[derive(sqlx::FromRow)] +struct ObligationRow { + id: String, + repo_slug: String, + repo_id: Option, + claim: String, + context: String, + prover: Option, + inline_requested: bool, + status: String, + created_at: String, +} + +impl TryFrom for ProofObligationRecord { + type Error = Error; + + /// Decode a stored row; the prover column holds the slug (`Display`). + fn try_from(row: ObligationRow) -> Result { + let parse = |s: &str| Uuid::parse_str(s).map_err(|e| Error::Internal(e.to_string())); + Ok(ProofObligationRecord { + id: parse(&row.id)?, + repo_slug: row.repo_slug, + repo_id: row.repo_id.as_deref().map(parse).transpose()?, + claim: row.claim, + context: row.context, + prover: row.prover.map(|s| ProverKind::new(s.as_str())), + inline_requested: row.inline_requested, + status: row.status, + created_at: chrono::DateTime::parse_from_rfc3339(&row.created_at) + .map_err(|e| Error::Internal(e.to_string()))? + .with_timezone(&chrono::Utc), + }) + } +} + fn parse_prover(s: &str) -> Result { match s { "Agda" => Ok(ProverKind::new("agda")), @@ -933,4 +1024,31 @@ mod tests { let _ = std::fs::remove_file(&path); } + + #[tokio::test] + async fn proof_obligation_round_trips_and_resubmission_is_idempotent() { + use crate::store::models::ProofObligationRecord; + let (store, path) = fresh_store().await; + + let ob = ProofObligationRecord::new( + "hyperpolymath/requeue".into(), + None, + "requeue-of-1".into(), + "strategy-shift".into(), + Some(ProverKind::new("hol-light")), + true, + ); + assert_eq!(ob.id.get_version_num(), 8); + assert!(store.record_proof_obligation(&ob).await.unwrap()); + assert!(!store.record_proof_obligation(&ob).await.unwrap()); + + let back = store.get_proof_obligation(ob.id).await.unwrap().unwrap(); + assert_eq!(back.claim, "requeue-of-1"); + assert_eq!(back.prover, Some(ProverKind::new("hol-light"))); + assert!(back.inline_requested); + assert_eq!(back.status, "PENDING"); + assert!(back.repo_id.is_none()); + + let _ = std::fs::remove_file(&path); + } } diff --git a/tests/protocol_contract.rs b/tests/protocol_contract.rs index c61100b..ca7478b 100644 --- a/tests/protocol_contract.rs +++ b/tests/protocol_contract.rs @@ -137,3 +137,138 @@ async fn graphql_uses_slug_for_verification_suggestions_and_status() { ); server.abort(); } + +// --------------------------------------------------------------------------- +// submitProofObligation — the wire contract hypatia sends (inbound). +// The query strings below are byte-for-byte what hypatia builds: +// FleetDispatcher.build_proof_obligation_mutation/4 (with and without a +// prover line) and LearningScheduler.submit_requeue/4 (with `inline: true`). +// --------------------------------------------------------------------------- + +/// Schema over an in-memory store, for executing inbound GraphQL directly. +async fn obligation_schema() -> echidnabot::api::graphql::EchidnabotSchema { + use echidnabot::api::graphql::GraphQLState; + use echidnabot::scheduler::JobScheduler; + use echidnabot::store::SqliteStore; + use std::sync::Arc; + + let config = echidnabot::config::Config::default(); + echidnabot::api::create_schema(GraphQLState { + store: Arc::new(SqliteStore::new("sqlite::memory:").await.unwrap()), + scheduler: Arc::new(JobScheduler::new(2, 10)), + echidna: Arc::new(EchidnaClient::new(&config.echidna)), + }) +} + +/// Execute `query` and return the response as JSON (data + errors). +async fn run(schema: &echidnabot::api::graphql::EchidnabotSchema, query: &str) -> Value { + serde_json::to_value(schema.execute(query).await).unwrap() +} + +/// FleetDispatcher's mutation; `prover_line` is "" or " prover: X,\n". +fn fleet_mutation(repo: &str, claim: &str, context: &str, prover_line: &str) -> String { + format!( + "mutation {{\n submitProofObligation(input: {{\n repo: \"{repo}\",\n \ + claim: \"{claim}\",\n context: \"{context}\",\n{prover_line} }}) {{\n \ + success\n proofId\n }}\n}}\n" + ) +} + +const LEARNING_SCHEDULER_MUTATION: &str = r#"mutation { + submitProofObligation(input: { + repo: "hyperpolymath/requeue", + claim: "requeue-of-attempt-42", + context: "strategy-shift class=lemma", + prover: LEAN, + inline: true + }) { success proofId } +} +"#; + +/// Assert a response has no errors and `success: true`; return the proofId. +fn accepted(resp: &Value) -> String { + assert!( + resp.get("errors") + .is_none_or(|e| e.as_array().unwrap().is_empty()), + "{resp}" + ); + let payload = &resp["data"]["submitProofObligation"]; + assert_eq!(payload["success"], json!(true), "{resp}"); + payload["proofId"].as_str().unwrap().to_string() +} + +#[tokio::test] +async fn fleet_dispatcher_obligation_with_prover_is_accepted_with_v8_id() { + let schema = obligation_schema().await; + let q = fleet_mutation( + "hyperpolymath/echidnabot", + "forall x, x = x", + "pattern P1", + " prover: COQ,\n", + ); + let id = uuid::Uuid::parse_str(&accepted(&run(&schema, &q).await)).unwrap(); + assert_eq!( + id.get_version_num(), + 8, + "proofId must be a UUIDv8 content id" + ); +} + +#[tokio::test] +async fn fleet_dispatcher_obligation_without_prover_is_accepted() { + let schema = obligation_schema().await; + let q = fleet_mutation( + "hyperpolymath/echidnabot", + "forall x, x = x", + "pattern P1", + "", + ); + accepted(&run(&schema, &q).await); +} + +#[tokio::test] +async fn learning_scheduler_inline_requeue_is_accepted() { + let schema = obligation_schema().await; + accepted(&run(&schema, LEARNING_SCHEDULER_MUTATION).await); +} + +#[tokio::test] +async fn resubmitting_an_obligation_is_idempotent() { + let schema = obligation_schema().await; + let q = + "mutation { submitProofObligation(input: { repo: \"a/b\", claim: \"c\", context: \"d\" }) \ + { success proofId status newlyRecorded repoRegistered } }"; + let first = run(&schema, q).await; + let second = run(&schema, q).await; + assert_eq!(accepted(&first), accepted(&second)); + let p1 = &first["data"]["submitProofObligation"]; + let p2 = &second["data"]["submitProofObligation"]; + assert_eq!(p1["status"], json!("PENDING")); + assert_eq!(p1["newlyRecorded"], json!(true)); + assert_eq!(p2["newlyRecorded"], json!(false)); + assert_eq!(p1["repoRegistered"], json!(false)); +} + +#[tokio::test] +async fn invalid_obligations_are_graphql_errors_not_success_false() { + let schema = obligation_schema().await; + let big = "x".repeat(echidnabot::api::graphql::MAX_OBLIGATION_FIELD_BYTES + 1); + for q in [ + // Unknown prover enum value: rejected at validation. + fleet_mutation("a/b", "c", "d", " prover: LEAN4,\n"), + // Not an owner/name slug. + fleet_mutation("no-slash", "c", "d", ""), + fleet_mutation("a/b/c", "c", "d", ""), + // Empty claim. + fleet_mutation("a/b", " ", "d", ""), + // Over the size cap. + fleet_mutation("a/b", &big, "d", ""), + ] { + let resp = run(&schema, &q).await; + let errors = resp["errors"].as_array().cloned().unwrap_or_default(); + assert!( + !errors.is_empty(), + "expected a GraphQL error for {q:.80}: {resp}" + ); + } +}