@@ -14,7 +14,7 @@ use crate::dispatcher::{
1414} ;
1515use crate :: dispatcher:: echidna_client:: ProverStatus as CoreProverStatus ;
1616use crate :: scheduler:: { JobPriority , JobScheduler } ;
17- use crate :: store:: models:: { ProofJobRecord , Repository as StoreRepository } ;
17+ use crate :: store:: models:: { ProofJobRecord , ProofObligationRecord , Repository as StoreRepository } ;
1818use crate :: store:: Store ;
1919
2020/// GraphQL schema type
@@ -277,6 +277,30 @@ pub struct RegisterRepoInput {
277277 pub enabled_provers : Option < Vec < ProverKind > > ,
278278}
279279
280+ /// Input for submitting a proof obligation from an external scanner (e.g. hypatia)
281+ #[ derive( async_graphql:: InputObject ) ]
282+ pub struct ProofObligationInput {
283+ /// Repository in "owner/name" format
284+ pub repo : String ,
285+ /// Human-readable claim that must be proved
286+ pub claim : String ,
287+ /// Original context/description from pattern detection
288+ pub context : String ,
289+ /// Optional prover hint. When supplied (e.g. by hypatia's proof-strategy
290+ /// rule picking the historically-best prover for this obligation class),
291+ /// it overrides the default. Omitted → default Lean.
292+ pub prover : Option < ProverKind > ,
293+ }
294+
295+ /// Result of submitting a proof obligation
296+ #[ derive( SimpleObject , Clone ) ]
297+ pub struct ProofObligationResult {
298+ /// Whether the obligation was successfully recorded
299+ pub success : bool ,
300+ /// Scheduler job ID assigned to this obligation (UUID string), or empty on failure
301+ pub proof_id : String ,
302+ }
303+
280304/// Input for repository settings
281305#[ derive( async_graphql:: InputObject ) ]
282306pub struct RepoSettingsInput {
@@ -371,6 +395,114 @@ impl MutationRoot {
371395 Ok ( ProofJobRecord :: from ( job) . into ( ) )
372396 }
373397
398+ /// Record a proof obligation submitted by an external tool (e.g. hypatia fleet_dispatcher).
399+ ///
400+ /// This mutation RECORDS the obligation as a pending scheduler job — it does NOT immediately
401+ /// invoke a prover. The scheduler will pick it up on its normal cycle. The repo must already
402+ /// be registered with echidnabot; if it is not, this returns `success: false`.
403+ ///
404+ /// The `repo` argument must be in "owner/name" format. The mutation searches all platforms
405+ /// for a matching registered repository and uses the first match found.
406+ async fn submit_proof_obligation (
407+ & self ,
408+ ctx : & Context < ' _ > ,
409+ input : ProofObligationInput ,
410+ ) -> async_graphql:: Result < ProofObligationResult > {
411+ let state = ctx. data :: < GraphQLState > ( ) ?;
412+
413+ // Parse "owner/name" format
414+ let ( owner, name) = {
415+ let parts: Vec < & str > = input. repo . splitn ( 2 , '/' ) . collect ( ) ;
416+ if parts. len ( ) != 2 || parts[ 0 ] . is_empty ( ) || parts[ 1 ] . is_empty ( ) {
417+ return Ok ( ProofObligationResult {
418+ success : false ,
419+ proof_id : String :: new ( ) ,
420+ } ) ;
421+ }
422+ ( parts[ 0 ] . to_string ( ) , parts[ 1 ] . to_string ( ) )
423+ } ;
424+
425+ // Find a matching registered repository across all platforms
426+ let repos = state
427+ . store
428+ . list_repositories ( None )
429+ . await
430+ . map_err ( |e| async_graphql:: Error :: new ( e. to_string ( ) ) ) ?;
431+
432+ let repo = repos
433+ . into_iter ( )
434+ . find ( |r| r. owner == owner && r. name == name) ;
435+
436+ let repo = match repo {
437+ Some ( r) => r,
438+ None => {
439+ return Ok ( ProofObligationResult {
440+ success : false ,
441+ proof_id : String :: new ( ) ,
442+ } ) ;
443+ }
444+ } ;
445+
446+ let chosen_prover = input
447+ . prover
448+ . map ( map_prover_kind_to_core)
449+ . unwrap_or ( CoreProverKind :: Lean ) ;
450+
451+ // Derive a human-readable hint string from the chosen prover so that
452+ // the obligation row is self-contained (e.g. a future query can show
453+ // "which prover was requested" without joining proof_jobs).
454+ let prover_hint = Some ( format ! ( "{:?}" , chosen_prover) . to_lowercase ( ) ) ;
455+
456+ // 1. Persist the obligation FIRST — it is the source of truth for claim/context.
457+ let obligation = ProofObligationRecord :: new (
458+ repo. id ,
459+ input. claim ,
460+ input. context ,
461+ prover_hint,
462+ ) ;
463+ state
464+ . store
465+ . create_obligation ( & obligation)
466+ . await
467+ . map_err ( |e| async_graphql:: Error :: new ( e. to_string ( ) ) ) ?;
468+
469+ // 2. Create a scheduler job whose file_paths carry an opaque reference to the
470+ // obligation row. Nothing in file_paths encodes claim/context strings.
471+ let job = crate :: scheduler:: ProofJob :: new (
472+ repo. id ,
473+ "manual-obligation" . to_string ( ) ,
474+ chosen_prover,
475+ vec ! [ format!( "obligation:{}" , obligation. id) ] ,
476+ )
477+ . with_priority ( JobPriority :: Normal ) ;
478+
479+ // 3. Persist job record, then enqueue.
480+ let record = ProofJobRecord :: from ( job. clone ( ) ) ;
481+ state
482+ . store
483+ . create_job ( & record)
484+ . await
485+ . map_err ( |e| async_graphql:: Error :: new ( e. to_string ( ) ) ) ?;
486+
487+ let _ = state
488+ . scheduler
489+ . enqueue ( job. clone ( ) )
490+ . await
491+ . map_err ( |e| async_graphql:: Error :: new ( e. to_string ( ) ) ) ?;
492+
493+ // 4. Back-fill the job ID onto the obligation row so it can be followed.
494+ state
495+ . store
496+ . link_obligation_to_job ( & obligation. id . to_string ( ) , & job. id . 0 . to_string ( ) )
497+ . await
498+ . map_err ( |e| async_graphql:: Error :: new ( e. to_string ( ) ) ) ?;
499+
500+ Ok ( ProofObligationResult {
501+ success : true ,
502+ proof_id : job. id . 0 . to_string ( ) ,
503+ } )
504+ }
505+
374506 /// Request ML-powered tactic suggestions
375507 async fn request_suggestions (
376508 & self ,
0 commit comments