feat(api): W6+W7 — row-level GET /proof_attempts with filters

Adds GET /api/v1/proof_attempts returning individual attempt rows
(vs aggregates from /strategy or /certificates/evidence cursors).

Query params (all optional):
  class=X        — filter by obligation_class
  prover=Y       — filter by prover_used
  outcome=Z      — filter by outcome (success|failure|timeout|unknown)
  repo=W         — filter by repo
  limit=N        — cap at 1000, default 100
  offset=M       — pagination

Returns AttemptsResponse { attempts: [AttemptRow], total_returned,
offset, limit }. Each row carries attempt_id, obligation_id, repo,
file, obligation_class, prover_used, outcome, duration_ms, confidence,
strategy_tag, started_at (ISO-8601).

Unblocks two downstream consumers:
  * Hypatia.Neural.ProverRecommender can now train on real feature
    vectors extracted from individual attempts, rather than unfolding
    synthetic rows from /strategy aggregates.
  * Hypatia.Rules.StrategyDrift can fetch the complete failed-attempt
    set for (class, old_prover) via outcome=failure, replacing the
    ≤100-row evidence-cursor approximation that used /certificates.
    Subsumes the separate /failed_attempts endpoint entirely.

Verified live:
  ?class=equiv&prover=coq&outcome=failure  → 3 rows, first attempt_id
                                             077962cf, ephapax/Semantics.v
  ?class=safety&limit=2                    → 2 rows, provers=[cvc5,eprover]

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

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

@@ -834,7 +834,8 @@ pub fn build_router(state: AppState) -> Router {
         // Proof-attempts endpoints — ClickHouse-backed, no AppState required
         .route(
             "/api/v1/proof_attempts",
-            post(proof_attempts::insert_handler),
+            post(proof_attempts::insert_handler)
+                .get(proof_attempts::list_attempts_handler),
         )
         .route(
             "/api/v1/proof_attempts/strategy",

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

@@ -221,6 +221,49 @@ pub struct InsertResponse {
     pub attempt_id: String,
 }
 
+/// Query parameters for `GET /api/v1/proof_attempts` (row-level).
+#[derive(Debug, Deserialize)]
+pub struct AttemptsQuery {
+    /// Optional filter: obligation class
+    #[serde(rename = "class")]
+    pub obligation_class: Option<String>,
+    /// Optional filter: prover
+    pub prover: Option<String>,
+    /// Optional filter: outcome (success/failure/timeout/unknown)
+    pub outcome: Option<String>,
+    /// Optional filter: repo
+    pub repo: Option<String>,
+    /// Max rows to return (default 100, cap 1000)
+    pub limit: Option<u32>,
+    /// Skip this many rows (for pagination)
+    pub offset: Option<u32>,
+}
+
+/// Row-level view of a single proof attempt, suitable for training
+/// feature vectors or client-side inspection.
+#[derive(Debug, Serialize)]
+pub struct AttemptRow {
+    pub attempt_id: String,
+    pub obligation_id: String,
+    pub repo: String,
+    pub file: String,
+    pub obligation_class: String,
+    pub prover_used: String,
+    pub outcome: String,
+    pub duration_ms: u64,
+    pub confidence: f64,
+    pub strategy_tag: String,
+    pub started_at: String,
+}
+
+#[derive(Debug, Serialize)]
+pub struct AttemptsResponse {
+    pub attempts: Vec<AttemptRow>,
+    pub total_returned: usize,
+    pub offset: u32,
+    pub limit: u32,
+}
+
 /// Query parameters for `GET /api/v1/proof_attempts/strategy`.
 #[derive(Debug, Deserialize)]
 pub struct StrategyQuery {
@@ -509,6 +552,91 @@ pub async fn insert_handler(
     ))
 }
 
+/// `GET /api/v1/proof_attempts` (row-level query)
+///
+/// Returns individual attempt rows with optional filters. Useful for
+/// RBF training (real feature vectors instead of unfolded aggregates)
+/// and for the StrategyDrift candidate query (`outcome=failure`
+/// + `class=X` + `prover=Y` returns exactly the re-queue candidate
+/// set, no 100-row cap from the certificates evidence path).
+#[instrument]
+pub async fn list_attempts_handler(
+    Query(params): Query<AttemptsQuery>,
+) -> Result<Json<AttemptsResponse>, HandlerError> {
+    let limit = params.limit.unwrap_or(100).min(1000);
+    let offset = params.offset.unwrap_or(0);
+
+    let mut wheres: Vec<String> = Vec::new();
+    if let Some(c) = &params.obligation_class {
+        require_non_empty(c, "class")?;
+        wheres.push(format!("obligation_class = '{}'", escape_sql_str(c)));
+    }
+    if let Some(p) = &params.prover {
+        require_non_empty(p, "prover")?;
+        wheres.push(format!("prover_used = '{}'", escape_sql_str(p)));
+    }
+    if let Some(o) = &params.outcome {
+        require_non_empty(o, "outcome")?;
+        wheres.push(format!("outcome = '{}'", escape_sql_str(o)));
+    }
+    if let Some(r) = &params.repo {
+        require_non_empty(r, "repo")?;
+        wheres.push(format!("repo = '{}'", escape_sql_str(r)));
+    }
+    let where_clause = if wheres.is_empty() {
+        String::new()
+    } else {
+        format!("WHERE {}", wheres.join(" AND "))
+    };
+
+    let sql = format!(
+        "SELECT attempt_id, obligation_id, repo, file, obligation_class, \
+                toString(prover_used) AS prover_used, \
+                toString(outcome) AS outcome, duration_ms, \
+                toFloat64(confidence) AS confidence, strategy_tag, \
+                toString(started_at) AS started_at \
+         FROM verisim.proof_attempts \
+         {} \
+         ORDER BY started_at DESC \
+         LIMIT {} OFFSET {} \
+         FORMAT JSONEachRow",
+        where_clause, limit, offset
+    );
+
+    let body = send_clickhouse_read(&sql).await?;
+    let attempts: Vec<AttemptRow> = body
+        .lines()
+        .filter(|l| !l.trim().is_empty())
+        .filter_map(|line| {
+            let v: serde_json::Value = serde_json::from_str(line).ok()?;
+            Some(AttemptRow {
+                attempt_id: v["attempt_id"].as_str()?.to_string(),
+                obligation_id: v["obligation_id"].as_str()?.to_string(),
+                repo: v["repo"].as_str()?.to_string(),
+                file: v["file"].as_str()?.to_string(),
+                obligation_class: v["obligation_class"].as_str()?.to_string(),
+                prover_used: v["prover_used"].as_str()?.to_string(),
+                outcome: v["outcome"].as_str()?.to_string(),
+                duration_ms: u64_from_json(&v["duration_ms"])?,
+                confidence: v["confidence"].as_f64().unwrap_or(0.5),
+                strategy_tag: v["strategy_tag"].as_str()?.to_string(),
+                started_at: v["started_at"]
+                    .as_str()
+                    .unwrap_or_default()
+                    .replacen(' ', "T", 1),
+            })
+        })
+        .collect();
+
+    let total_returned = attempts.len();
+    Ok(Json(AttemptsResponse {
+        attempts,
+        total_returned,
+        offset,
+        limit,
+    }))
+}
+
 /// `GET /api/v1/proof_attempts/coverage`
 ///
 /// Returns cross-repo coverage stats per obligation_class: how many distinct