Skip to content

Commit b660778

Browse files
hyperpolymathclaude
andcommitted
feat(api): N5 — /api/v1/proof_attempts/coverage cross-repo breakdown
Cross-repo transfer of learnings is already automatic: the mv_prover_success_by_class MV aggregates (class, prover) regardless of repo, so strategy recommendations implicitly fuse signal from all repos. This endpoint surfaces the per-class breakdown so callers can use n_repos as a confidence amplifier — 100 attempts across 10 repos is stronger signal than 100 attempts from one repo. GET /api/v1/proof_attempts/coverage returns: coverage: [ { obligation_class, n_repos, n_provers, n_attempts, n_success } ] Live snapshot (sorted by n_attempts): equiv n_repos=2 n_provers=3 n_attempts=452 (2 repos contributing) safety n_repos=3 n_provers=5 n_attempts=315 correctness n_repos=2 n_provers=4 n_attempts=204 totality n_repos=1 n_provers=1 n_attempts=87 (narrow signal) linearity n_repos=3 n_provers=3 ... Hypatia's ProofStrategySelection can now detect "narrow signal" classes (n_repos=1) and either boost exploration or flag low transfer-confidence in its recommendations. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent cb4ca76 commit b660778

2 files changed

Lines changed: 54 additions & 0 deletions

File tree

rust-core/verisim-api/src/lib.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -844,6 +844,10 @@ pub fn build_router(state: AppState) -> Router {
844844
"/api/v1/proof_attempts/certificates",
845845
get(proof_attempts::certificates_handler),
846846
)
847+
.route(
848+
"/api/v1/proof_attempts/coverage",
849+
get(proof_attempts::coverage_handler),
850+
)
847851
// Authentication middleware layer
848852
.layer(axum_middleware::from_fn_with_state(
849853
auth_state,

rust-core/verisim-api/src/proof_attempts.rs

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -251,6 +251,21 @@ pub struct StrategyResponse {
251251
pub recommendations: Vec<ProverRecommendation>,
252252
}
253253

254+
/// One row per obligation_class showing cross-repo coverage stats.
255+
#[derive(Debug, Serialize)]
256+
pub struct CoverageRow {
257+
pub obligation_class: String,
258+
pub n_repos: u64,
259+
pub n_provers: u64,
260+
pub n_attempts: u64,
261+
pub n_success: u64,
262+
}
263+
264+
#[derive(Debug, Serialize)]
265+
pub struct CoverageResponse {
266+
pub coverage: Vec<CoverageRow>,
267+
}
268+
254269
// ---------------------------------------------------------------------------
255270
// V4: Certificate types
256271
// ---------------------------------------------------------------------------
@@ -494,6 +509,41 @@ pub async fn insert_handler(
494509
))
495510
}
496511

512+
/// `GET /api/v1/proof_attempts/coverage`
513+
///
514+
/// Returns cross-repo coverage stats per obligation_class: how many distinct
515+
/// repos have contributed attempts, how many distinct provers, and total
516+
/// attempt count. Callers can use `n_repos` as a confidence amplifier —
517+
/// 100 attempts across 10 repos is stronger signal than 100 from one repo.
518+
#[instrument]
519+
pub async fn coverage_handler() -> Result<Json<CoverageResponse>, HandlerError> {
520+
let sql = "SELECT obligation_class, \
521+
countDistinct(repo) AS n_repos, \
522+
countDistinct(prover_used) AS n_provers, \
523+
count() AS n_attempts, \
524+
countIf(outcome = 'success') AS n_success \
525+
FROM verisim.proof_attempts \
526+
GROUP BY obligation_class \
527+
ORDER BY n_attempts DESC \
528+
FORMAT JSONEachRow";
529+
let rows = send_clickhouse_read(sql).await?;
530+
let coverage: Vec<CoverageRow> = rows
531+
.lines()
532+
.filter(|l| !l.trim().is_empty())
533+
.filter_map(|line| {
534+
let v: serde_json::Value = serde_json::from_str(line).ok()?;
535+
Some(CoverageRow {
536+
obligation_class: v["obligation_class"].as_str()?.to_string(),
537+
n_repos: u64_from_json(&v["n_repos"])?,
538+
n_provers: u64_from_json(&v["n_provers"])?,
539+
n_attempts: u64_from_json(&v["n_attempts"])?,
540+
n_success: u64_from_json(&v["n_success"])?,
541+
})
542+
})
543+
.collect();
544+
Ok(Json(CoverageResponse { coverage }))
545+
}
546+
497547
/// `GET /api/v1/proof_attempts/strategy?class=<class>&limit=<n>`
498548
///
499549
/// Queries `mv_prover_success_by_class` for the given `obligation_class` and

0 commit comments

Comments
 (0)