Skip to content

Commit 24a8105

Browse files
hyperpolymathclaude
andcommitted
feat(echidnabot): add inline-claim mode (A5)
ProofObligationInput gains optional `inline: Bool` flag. When true, the obligation's claim text IS the proof content: process_job short-circuits before clone_repo, fetches the obligation, and calls echidna.verify_proof directly with the claim. No git clone, no file walk. Sentinel `inline:<obligation_id>` distinguishes inline jobs from the legacy `obligation:<id>` clone path in ProofJob.file_paths. Tested end-to-end: provable claim → success=1, duration=1ms, "Inline proof verified" unsat claim → success=0, duration=20ms, "Inline proof verification failed" Unblocks batch drivers and test harnesses that hold proofs in-memory. Useful for the Phase E playground (nesy-solver.dev) where users submit ad-hoc SMT-LIB/Lean/Coq without any repo context. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 55fa9ef commit 24a8105

2 files changed

Lines changed: 49 additions & 1 deletion

File tree

bots/echidnabot/src/api/graphql.rs

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -290,6 +290,12 @@ pub struct ProofObligationInput {
290290
/// rule picking the historically-best prover for this obligation class),
291291
/// it overrides the default. Omitted → default Lean.
292292
pub prover: Option<ProverKind>,
293+
/// When `true`, treat `claim` as the proof content itself and verify it
294+
/// directly against echidna, skipping the clone-first pipeline. Useful
295+
/// for batch drivers and test harnesses that hold proofs in-memory and
296+
/// don't want echidnabot to git-clone a whole repo just to read one file.
297+
/// When omitted or false, the legacy clone+walk pipeline is used.
298+
pub inline: Option<bool>,
293299
}
294300

295301
/// Result of submitting a proof obligation
@@ -468,11 +474,18 @@ impl MutationRoot {
468474

469475
// 2. Create a scheduler job whose file_paths carry an opaque reference to the
470476
// obligation row. Nothing in file_paths encodes claim/context strings.
477+
// When `inline` is set, prefix the sentinel so process_job skips the
478+
// clone pipeline and verifies the obligation's claim directly.
479+
let sentinel = if input.inline.unwrap_or(false) {
480+
format!("inline:{}", obligation.id)
481+
} else {
482+
format!("obligation:{}", obligation.id)
483+
};
471484
let job = crate::scheduler::ProofJob::new(
472485
repo.id,
473486
"manual-obligation".to_string(),
474487
chosen_prover,
475-
vec![format!("obligation:{}", obligation.id)],
488+
vec![sentinel],
476489
)
477490
.with_priority(JobPriority::Normal);
478491

bots/echidnabot/src/main.rs

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -533,6 +533,41 @@ async fn process_job(
533533
)));
534534
}
535535

536+
// Inline-claim shortcut (A5): sentinel `inline:<obligation_id>` means the
537+
// obligation's `claim` column *is* the proof content to verify. Skip clone,
538+
// skip file walk, call echidna once with the claim text.
539+
if let Some(first) = job.file_paths.first() {
540+
if let Some(obligation_id) = first.strip_prefix("inline:") {
541+
let obligation = store
542+
.get_obligation(obligation_id)
543+
.await?
544+
.ok_or_else(|| {
545+
echidnabot::Error::Echidna(format!(
546+
"inline obligation {} not found in store",
547+
obligation_id
548+
))
549+
})?;
550+
let verify = echidna
551+
.verify_proof(job.prover, &obligation.claim)
552+
.await?;
553+
let success =
554+
verify.status == echidnabot::dispatcher::ProofStatus::Verified;
555+
let tag = format!("inline:{}", obligation_id);
556+
return Ok(echidnabot::scheduler::JobResult {
557+
success,
558+
message: if success {
559+
"Inline proof verified".to_string()
560+
} else {
561+
"Inline proof verification failed".to_string()
562+
},
563+
prover_output: verify.prover_output,
564+
duration_ms: start.elapsed().as_millis() as u64,
565+
verified_files: if success { vec![tag.clone()] } else { vec![] },
566+
failed_files: if success { vec![] } else { vec![tag] },
567+
});
568+
}
569+
}
570+
536571
let repo = store
537572
.get_repository(job.repo_id)
538573
.await?

0 commit comments

Comments
 (0)