Skip to content

Commit d01a33b

Browse files
hyperpolymathclaude
andcommitted
feat(dispatch): wire ChapelParallelSearch into ProverDispatcher (L2.1)
Activates L2 Wave 1 of the Chapel integration plan (docs/handover/TODO.md). Adds `ProverDispatcher::verify_proof_parallel(content)` which, under `--features chapel` plus a live Chapel runtime, fans out to up to 30 prover backends via the Zig FFI bridge (echidna_prove_parallel) and routes the first successful result through the standard trust pipeline (axiom tracker, integrity check, trust-level scoring) before returning a DispatchResult. Falls back to the sequential `verify_proof` path (selected by the existing content-sniff heuristic) whenever: - the `chapel` Cargo feature is not compiled in, or - `ChapelParallelSearch::new()` reports the runtime unavailable, or - the parallel search errors out, or - parallel search returns no winner (so callers still get a real pipeline answer instead of a bare failure). Trust level for a Chapel-parallel win is computed as a single confirming prover (PortfolioConfidence::SingleSolver) — parallel first-wins is a dispatch speedup, not cross-checking. Cross-checked portfolios remain on `verify_proof_cross_checked`; Wave 2 will extend Chapel to portfolio quorum. Tests: - `test_verify_proof_parallel_falls_back_without_chapel` exercises the no-feature path end-to-end (runs in default CI). - `test_verify_proof_parallel_chapel_path` exercises the feature-gated path; runs under `cargo test --features chapel` (chapel-ci.yml job 3). Verified: - `cargo check --lib` clean on pristine main + this change. - `cargo check --lib --features chapel` clean (one pre-existing dead_code warning on echidna_chapel_is_prover_available, unrelated). - `cargo test --lib dispatch::` — 15/15 pass including the new fallback test. Per the Hyperpolymath "wire everything" rule, this removes the ChapelParallelSearch orphan code path: proof_search.rs had the strategy implemented but nothing in dispatch.rs called it. The L2.1 gap identified in TODO.md ("dispatch.rs still bypasses the feature-gated ChapelParallelSearch strategy") is now closed. SPDX-License-Identifier: PMPL-1.0-or-later Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 5f0f289 commit d01a33b

1 file changed

Lines changed: 206 additions & 0 deletions

File tree

src/rust/dispatch.rs

Lines changed: 206 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,9 @@ use crate::provers::{ProverConfig, ProverFactory, ProverKind};
1919
use crate::verification::axiom_tracker::{AxiomTracker, AxiomUsage, DangerLevel};
2020
use crate::verification::confidence::{compute_trust_level, TrustFactors, TrustLevel};
2121

22+
#[cfg(feature = "chapel")]
23+
use crate::proof_search::{ChapelParallelSearch, ProofSearchStrategy};
24+
2225
/// Per-prover record inside `RunDiagnostics`. Captures what a single
2326
/// backend returned during a dispatch run — used by the sanity suite and
2427
/// by the Julia ML arbiter to reason about why a prover ruled one way.
@@ -464,6 +467,176 @@ impl ProverDispatcher {
464467
Ok(primary_result)
465468
}
466469

470+
/// Dispatch a proof through Chapel's parallel prover search (L2 Wave 1).
471+
///
472+
/// With `--features chapel` **and** the Chapel runtime available, fans out
473+
/// to up to 30 prover backends in parallel via the Zig FFI bridge and
474+
/// returns the first successful result through the standard trust pipeline
475+
/// (axiom tracking, integrity check, trust-level scoring).
476+
///
477+
/// Falls back to sequential `verify_proof` (with `select_prover` heuristic)
478+
/// when:
479+
/// - the `chapel` Cargo feature is not compiled in, or
480+
/// - `ChapelParallelSearch::new()` reports the runtime unavailable, or
481+
/// - the parallel search returns a non-verified result (so the caller
482+
/// still gets a real pipeline answer rather than a bare failure).
483+
///
484+
/// The trust level for a Chapel-parallel win is computed as a single
485+
/// confirming prover — parallel-first-wins is a dispatch speedup, **not**
486+
/// cross-checking. Callers wanting cross-checking should use
487+
/// `verify_proof_cross_checked` (Wave-2 territory will extend Chapel to
488+
/// portfolio quorum).
489+
pub async fn verify_proof_parallel(&self, content: &str) -> Result<DispatchResult> {
490+
#[cfg(feature = "chapel")]
491+
{
492+
let chapel = match ChapelParallelSearch::new() {
493+
Ok(c) => c,
494+
Err(e) => {
495+
warn!(
496+
"Chapel parallel search unavailable ({}); falling back to sequential",
497+
e
498+
);
499+
let fallback_kind = Self::select_prover(content, None);
500+
return self.verify_proof(fallback_kind, content).await;
501+
},
502+
};
503+
504+
if !chapel.available() {
505+
warn!("Chapel runtime reported unavailable; falling back to sequential");
506+
let fallback_kind = Self::select_prover(content, None);
507+
return self.verify_proof(fallback_kind, content).await;
508+
}
509+
510+
let start = Instant::now();
511+
let timeout = std::time::Duration::from_secs(self.config.timeout);
512+
513+
let parallel = match chapel.search(content, timeout) {
514+
Ok(r) => r,
515+
Err(e) => {
516+
warn!(
517+
"Chapel parallel search errored ({}); falling back to sequential",
518+
e
519+
);
520+
let fallback_kind = Self::select_prover(content, None);
521+
return self.verify_proof(fallback_kind, content).await;
522+
},
523+
};
524+
525+
if !parallel.success {
526+
info!("Chapel parallel search returned no winner; sequential fallback");
527+
let fallback_kind = Self::select_prover(content, None);
528+
return self.verify_proof(fallback_kind, content).await;
529+
}
530+
531+
let winning_kind: ProverKind = parallel
532+
.prover_name
533+
.as_deref()
534+
.and_then(|n| n.parse().ok())
535+
.unwrap_or_else(|| Self::select_prover(content, None));
536+
537+
let axiom_usages = if self.config.track_axioms {
538+
Some(AxiomTracker::new().scan(winning_kind, content))
539+
} else {
540+
None
541+
};
542+
543+
let worst_danger = axiom_usages
544+
.as_ref()
545+
.map(|u| {
546+
u.iter()
547+
.map(|x| x.danger_level)
548+
.max()
549+
.unwrap_or(DangerLevel::Safe)
550+
})
551+
.unwrap_or(DangerLevel::Safe);
552+
553+
let axiom_report = axiom_usages.as_ref().and_then(|u| u.first().cloned());
554+
555+
let solver_integrity_ok = if let Some(ref checker) = self.integrity_checker {
556+
let reports = checker.verify_all().await.unwrap_or_default();
557+
let prover_name = format!("{:?}", winning_kind).to_lowercase();
558+
reports
559+
.iter()
560+
.find(|r| r.name.to_lowercase() == prover_name)
561+
.map(|r| {
562+
r.status == IntegrityStatus::Verified
563+
|| r.status == IntegrityStatus::Uninitialized
564+
})
565+
.unwrap_or(true)
566+
} else {
567+
true
568+
};
569+
570+
let trust_factors = TrustFactors {
571+
prover: winning_kind,
572+
confirming_provers: 1,
573+
has_certificate: false,
574+
certificate_verified: false,
575+
worst_axiom_danger: worst_danger,
576+
solver_integrity_ok,
577+
portfolio_confidence: Some(
578+
crate::verification::portfolio::PortfolioConfidence::SingleSolver,
579+
),
580+
};
581+
582+
let trust_level = compute_trust_level(&trust_factors);
583+
let meets_minimum = trust_level >= self.config.min_trust_level;
584+
let elapsed = start.elapsed().as_millis() as u64;
585+
586+
let prover_elapsed_ms = (parallel.time_seconds * 1000.0) as u64;
587+
let outcome = ProverOutcome::Proved {
588+
elapsed_ms: prover_elapsed_ms,
589+
};
590+
591+
let diagnostics = if self.config.diagnostics {
592+
Some(RunDiagnostics {
593+
normalized_input: content.trim().to_string(),
594+
provers_selected: vec![format!("{:?}", winning_kind)],
595+
per_prover: vec![PerProverRecord {
596+
prover: format!("{:?}", winning_kind),
597+
outcome: outcome.clone(),
598+
elapsed_ms: prover_elapsed_ms,
599+
}],
600+
})
601+
} else {
602+
None
603+
};
604+
605+
let message = if !meets_minimum {
606+
format!(
607+
"Chapel parallel proof verified but trust level {} below minimum {}",
608+
trust_level, self.config.min_trust_level
609+
)
610+
} else {
611+
format!(
612+
"Chapel parallel proof verified by {:?} with {}",
613+
winning_kind, trust_level
614+
)
615+
};
616+
617+
return Ok(DispatchResult {
618+
verified: meets_minimum,
619+
trust_level,
620+
provers_used: vec![format!("{:?}", winning_kind)],
621+
proof_time_ms: elapsed,
622+
goals_remaining: 0,
623+
axiom_report,
624+
certificate_hash: None,
625+
message,
626+
cross_checked: false,
627+
outcome,
628+
diagnostics,
629+
});
630+
}
631+
632+
#[cfg(not(feature = "chapel"))]
633+
{
634+
info!("Chapel feature not compiled in; dispatching sequentially");
635+
let fallback_kind = Self::select_prover(content, None);
636+
self.verify_proof(fallback_kind, content).await
637+
}
638+
}
639+
467640
/// Select the best prover for a given proof type
468641
pub fn select_prover(content: &str, file_extension: Option<&str>) -> ProverKind {
469642
// Try to detect from file extension first
@@ -635,4 +808,37 @@ mod tests {
635808
let dispatcher = ProverDispatcher::with_config(config);
636809
assert!(dispatcher.config.cross_check);
637810
}
811+
812+
#[cfg(not(feature = "chapel"))]
813+
#[tokio::test]
814+
async fn test_verify_proof_parallel_falls_back_without_chapel() {
815+
// Without the chapel feature the parallel entry point must still
816+
// return a DispatchResult via the sequential path. We only assert
817+
// the call returns Ok — prover execution itself is exercised in
818+
// other tests.
819+
let dispatcher = ProverDispatcher::new();
820+
let result = dispatcher
821+
.verify_proof_parallel("(set-logic QF_LIA)\n(assert (> x 0))")
822+
.await;
823+
assert!(
824+
result.is_ok(),
825+
"parallel dispatch should fall back cleanly without chapel feature"
826+
);
827+
}
828+
829+
#[cfg(feature = "chapel")]
830+
#[tokio::test]
831+
async fn test_verify_proof_parallel_chapel_path() {
832+
// With the chapel feature enabled, the parallel entry point should
833+
// reach either the Chapel runtime (30-prover fanout) or the
834+
// sequential fallback — both must yield a DispatchResult.
835+
let dispatcher = ProverDispatcher::new();
836+
let result = dispatcher
837+
.verify_proof_parallel("(set-logic QF_LIA)\n(assert (> x 0))")
838+
.await;
839+
assert!(
840+
result.is_ok(),
841+
"Chapel parallel dispatch must return Ok (either Chapel or fallback)"
842+
);
843+
}
638844
}

0 commit comments

Comments
 (0)