lean-host-mcp 0.5.0

//! Pure data-shuffle projections from `lean-rs-worker` types into the
//! MCP-stable wire shapes.
//!
//! No Lean dependency past `Serialize + Deserialize` round-trips, no
//! `LeanRuntime` handle—these can be called from any thread and
//! serialise straight into the JSON envelope.
//!
//! All projection *types* and *helper functions* live here. Tool handlers
//! import the wire types from this module. Worker lifecycle/error
//! classification belongs in the runtime boundary, not in projection code.
#![allow(clippy::needless_pass_by_value)]

use lean_rs_worker_parent::{
    LeanWorkerDeclarationFlags, LeanWorkerDeclarationInspection as WorkerDeclarationInspection,
    LeanWorkerDeclarationInspectionResult, LeanWorkerDeclarationProofSearchFacts, LeanWorkerDeclarationRow,
    LeanWorkerDeclarationSearchFacts, LeanWorkerDeclarationSearchPruning, LeanWorkerDeclarationSearchResult,
    LeanWorkerDeclarationSearchRow, LeanWorkerDeclarationSearchTimings, LeanWorkerDeclarationTargetInfo,
    LeanWorkerDeclarationVerificationFacts, LeanWorkerDeclarationVerificationResult,
    LeanWorkerDeclarationVerificationStatus, LeanWorkerDiagnostic, LeanWorkerElabFailure, LeanWorkerElabResult,
    LeanWorkerKernelResult, LeanWorkerKernelStatus, LeanWorkerMetaResult, LeanWorkerModuleSourceSpan,
    LeanWorkerProofAttemptEnvelope, LeanWorkerProofAttemptResult, LeanWorkerProofAttemptRow,
    LeanWorkerProofAttemptStatus, LeanWorkerRendered, LeanWorkerRenderedInfo, LeanWorkerRendering,
    LeanWorkerSourceCoordinateSpace, LeanWorkerSourceRange,
};

/// Source-range projection with public fields mirroring `LeanWorkerSourceRange`.
#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct SourceRange {
    pub file: String,
    pub start_line: u32,
    pub start_column: u32,
    pub end_line: u32,
    pub end_column: u32,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct Position {
    pub line: u32,
    pub column: u32,
    pub end_line: Option<u32>,
    pub end_column: Option<u32>,
}

/// Coordinate space for a Lean diagnostic position.
#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, schemars::JsonSchema)]
#[serde(rename_all = "snake_case")]
pub enum CoordinateSpace {
    OriginalSource,
    SyntheticBuffer,
    Unknown,
}

/// Wire-stable severity classification. The three Lean severities map to
/// `snake_case` strings so the field is uniform with every other status
/// discriminant in the server.
#[derive(Debug, Clone, Copy, serde::Serialize, schemars::JsonSchema)]
#[serde(rename_all = "snake_case")]
pub enum Severity {
    Error,
    Warning,
    Info,
}

impl Severity {
    /// The worker layer emits severity as a snake-case string; unknown
    /// values map to `Info` rather than blocking the response.
    fn from_worker(s: &str) -> Self {
        match s {
            "error" => Self::Error,
            "warning" => Self::Warning,
            _ => Self::Info,
        }
    }
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct Diagnostic {
    pub severity: Severity,
    pub message: String,
    pub coordinate_space: CoordinateSpace,
    pub position: Option<Position>,
    /// Original source range when the worker can map this diagnostic back to
    /// the caller's file.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub original_range: Option<SourceRange>,
    /// Range in the synthetic buffer used for a trial overlay. Present only
    /// when the buffer-local coordinates are the honest coordinates.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub synthetic_range: Option<Position>,
    /// Real source path when Lean attached one. Omitted for the synthetic
    /// `<elaborate>` label that elaboration-buffer calls always produce;
    /// the caller already knows which file they asked about.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub file: Option<String>,
    /// Short mapping note for diagnostics whose coordinate space is unknown.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub coordinate_note: Option<String>,
}

/// Structured failure payload: the projection of `LeanWorkerElabFailure`
/// sent over JSON. Failure is part of a successful tool call; this is never
/// an MCP error.
#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct ElabFailure {
    pub diagnostics: Vec<Diagnostic>,
    pub truncated: bool,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct ElabSuccess {
    pub ok: bool,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct KernelOutcome {
    /// One of `Checked`, `Rejected`, `Unavailable`, or `Unsupported`.
    pub status: String,
    pub summary: Option<KernelSummary>,
    pub failure: Option<ElabFailure>,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct KernelSummary {
    pub declaration_name: String,
    pub kind: String,
    /// Pretty-printed declaration type via Lean's `PrettyPrinter`
    /// (notation-aware), as the worker's `LeanWorkerKernelSummary` reports
    /// it.
    pub type_signature: String,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct MetaOutcome {
    /// One of `Ok`, `Failed`, `TimeoutOrHeartbeat`, or `Unsupported`.
    pub status: String,
    pub rendered: Option<String>,
    pub definitionally_equal: Option<bool>,
    pub failure: Option<ElabFailure>,
    /// Set when the worker reported `LeanWorkerRendering::Raw`: the
    /// optional `meta_pp_expr` shim was missing or reported `Unsupported`,
    /// and the rendering fell back to `Expr.toString`. Internal; tool
    /// handlers translate this into an envelope warning, and the field
    /// never serialises.
    #[serde(skip)]
    #[schemars(skip)]
    pub raw_fallback_used: bool,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct DeclarationRow {
    pub name: String,
    pub kind: String,
    /// Pretty-printed type signature as the worker's
    /// `LeanWorkerDeclarationRow` reports it. `None` only when the
    /// declaration has no recoverable type (typically internal artifacts).
    pub type_signature: Option<String>,
    pub source: Option<SourceRange>,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct RenderedText {
    pub value: String,
    pub truncated: bool,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct ModuleSourceSpan {
    pub start_line: u32,
    pub start_column: u32,
    pub end_line: u32,
    pub end_column: u32,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct ProofActionDeclarationTarget {
    pub short_name: String,
    pub declaration_name: String,
    pub namespace_name: String,
    pub declaration_kind: String,
    pub declaration_span: ModuleSourceSpan,
    pub name_span: ModuleSourceSpan,
    pub body_span: ModuleSourceSpan,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct DeclarationFlags {
    pub is_private: bool,
    pub is_generated: bool,
    pub is_internal: bool,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct DeclarationSummary {
    pub name: String,
    pub kind: String,
    pub module: Option<String>,
    pub source: Option<SourceRange>,
    pub match_reason: String,
    pub score: i32,
    pub rank: usize,
    pub flags: DeclarationFlags,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct DeclarationSearchPruning {
    pub stage: String,
    pub reason: String,
    pub count: usize,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct DeclarationSearchTimings {
    pub scan_micros: u64,
    pub rank_micros: u64,
    pub source_micros: u64,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct DeclarationSearchFacts {
    pub declarations_scanned: usize,
    pub after_name_filter: usize,
    pub after_kind_filter: usize,
    pub after_required_constants_filter: usize,
    pub after_conclusion_filter: usize,
    pub after_scope_filter: usize,
    pub source_lookups: usize,
    pub broad_pruning: Vec<DeclarationSearchPruning>,
    pub truncated: bool,
    pub timings: DeclarationSearchTimings,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct DeclarationSearchResult {
    pub declarations: Vec<DeclarationSummary>,
    pub truncated: bool,
    pub facts: DeclarationSearchFacts,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
#[allow(
    clippy::struct_excessive_bools,
    reason = "proof-search booleans mirror independent lean-rs wire facts"
)]
pub struct DeclarationProofSearchFacts {
    pub is_simp: bool,
    pub is_rw_candidate: bool,
    pub is_instance: bool,
    pub is_class: bool,
    pub class_name: Option<String>,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct DeclarationInspection {
    pub name: String,
    pub kind: String,
    pub module: Option<String>,
    pub source: Option<SourceRange>,
    pub statement: Option<RenderedText>,
    /// How `statement` was rendered: `"pretty"` (notation-aware) or `"raw"`
    /// (fully-elaborated `Expr.toString`). `"raw"` when `Pretty` was requested
    /// but the pretty-printer could not render the term and fell back. `None`
    /// when no statement was requested.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub statement_rendering: Option<String>,
    pub docstring: Option<RenderedText>,
    pub attributes: Vec<String>,
    pub proof_search: DeclarationProofSearchFacts,
    pub flags: DeclarationFlags,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
#[serde(tag = "status", rename_all = "snake_case")]
pub enum DeclarationInspectionResult {
    Found {
        declaration: Box<DeclarationInspection>,
    },
    NotFound {
        name: Option<String>,
    },
    /// The declaration's import closure reached an unbuilt `.olean`, so the
    /// name could not be resolved against a complete environment. Distinct from
    /// `not_found` (which would falsely claim the declaration does not exist):
    /// it may resolve once the project is built. The envelope carries the
    /// `lake build` warning. Shares the `needs_build` status token with the
    /// other resolution-bearing tools.
    NeedsBuild,
    Unsupported,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct ProofAttemptCandidate {
    pub id: String,
    pub status: String,
    pub snippet: RenderedText,
    pub diagnostics: ElabFailure,
    pub downstream_diagnostics: ElabFailure,
    pub goals: Vec<RenderedText>,
    pub declaration: Option<ProofActionDeclarationTarget>,
    pub proof_position: Option<ProofPositionSummary>,
    pub output_truncated: bool,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
#[allow(
    clippy::struct_excessive_bools,
    reason = "summary exposes independent proof-attempt batch facts for agents"
)]
pub struct ProofAttemptSummary {
    pub requested_candidates: u32,
    pub returned_candidates: u32,
    pub candidate_limit: u32,
    pub candidates_truncated: bool,
    pub partial: bool,
    pub closed: u32,
    pub progressed: u32,
    pub failed: u32,
    pub timeout: u32,
    pub budget_exceeded: u32,
    pub not_attempted: u32,
    pub unsupported: u32,
    pub output_truncated: u32,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct ProofPositionSummary {
    pub index: u32,
    pub tactic: RenderedText,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
pub struct ProofAttemptEnvelope {
    pub candidates: Vec<ProofAttemptCandidate>,
    pub candidate_limit: u32,
    pub candidates_truncated: bool,
    pub summary: ProofAttemptSummary,
}

impl ProofAttemptEnvelope {
    pub(crate) fn refresh_summary(&mut self, requested_candidates: usize) {
        self.summary = proof_attempt_summary(
            &self.candidates,
            self.candidate_limit,
            self.candidates_truncated,
            requested_candidates,
        );
    }
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
#[serde(tag = "status", rename_all = "snake_case")]
pub enum ProofAttemptResult {
    Ok {
        result: ProofAttemptEnvelope,
        imports: Vec<String>,
    },
    MissingImports {
        result: ProofAttemptEnvelope,
        imports: Vec<String>,
        missing: Vec<String>,
    },
    HeaderParseFailed {
        diagnostics: ElabFailure,
    },
    Unsupported,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
#[allow(
    clippy::struct_excessive_bools,
    reason = "verification booleans mirror independent lean-rs wire facts for proof policy decisions"
)]
pub struct DeclarationVerificationFacts {
    #[serde(skip_serializing_if = "Option::is_none")]
    pub target: Option<ProofActionDeclarationTarget>,
    pub diagnostics: ElabFailure,
    pub unresolved_goals: Vec<RenderedText>,
    pub contains_sorry: bool,
    pub contains_admit: bool,
    pub contains_sorry_ax: bool,
    pub axioms: Vec<String>,
    pub axioms_truncated: bool,
    /// `false` when the axiom dependency set could not be computed (target
    /// unresolved, or `report_axioms` not requested): an empty `axioms` then
    /// means "not computed", not "no axioms". `true` with empty `axioms` is a
    /// genuine no-nontrivial-axioms result.
    pub axioms_available: bool,
    pub output_truncated: bool,
    /// Competing declarations when `verification_status` is `ambiguous`; empty
    /// otherwise. The fully-qualified names to disambiguate between.
    #[serde(skip_serializing_if = "Vec::is_empty")]
    pub candidates: Vec<ProofActionDeclarationTarget>,
    /// `false` when the verdict was computed against an incomplete or
    /// unresolved environment (`needs_build` or `ambiguous`). The other facts
    /// in this block are then unreliable: a clean `contains_sorry:false` /
    /// `unresolved_goals:[]` does not mean the declaration verified — the
    /// environment could not be assembled, or the name did not resolve, to
    /// check it. Always serialized; an absent trust flag is worse than present.
    pub facts_trustworthy: bool,
}

#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
#[serde(tag = "status", rename_all = "snake_case")]
pub enum DeclarationVerificationResult {
    Ok {
        verification_status: String,
        facts: Box<DeclarationVerificationFacts>,
        imports: Vec<String>,
    },
    MissingImports {
        verification_status: String,
        facts: Box<DeclarationVerificationFacts>,
        imports: Vec<String>,
        missing: Vec<String>,
    },
    HeaderParseFailed {
        diagnostics: ElabFailure,
    },
    Unsupported,
}

// --- projection helpers -------------------------------------------------

pub fn project_diagnostic(d: &LeanWorkerDiagnostic) -> Diagnostic {
    let position = d.line.map(|line| Position {
        line,
        column: d.column.unwrap_or(0),
        end_line: d.end_line,
        end_column: d.end_column,
    });
    let coordinate_space = project_coordinate_space(d.coordinate_space);
    let synthetic_range = match coordinate_space {
        CoordinateSpace::SyntheticBuffer => position.clone(),
        CoordinateSpace::OriginalSource | CoordinateSpace::Unknown => None,
    };
    let coordinate_note = match coordinate_space {
        CoordinateSpace::Unknown => {
            Some("worker did not report whether this diagnostic uses original source or a synthetic buffer".to_owned())
        }
        CoordinateSpace::OriginalSource | CoordinateSpace::SyntheticBuffer => None,
    };
    Diagnostic {
        severity: Severity::from_worker(&d.severity),
        message: d.message.clone(),
        coordinate_space,
        position,
        original_range: d.original_range.clone().map(project_source_range),
        synthetic_range,
        file: meaningful_file_label(&d.file_label),
        coordinate_note,
    }
}

fn project_coordinate_space(space: LeanWorkerSourceCoordinateSpace) -> CoordinateSpace {
    match space {
        LeanWorkerSourceCoordinateSpace::OriginalSource => CoordinateSpace::OriginalSource,
        LeanWorkerSourceCoordinateSpace::SyntheticBuffer => CoordinateSpace::SyntheticBuffer,
        LeanWorkerSourceCoordinateSpace::Unknown => CoordinateSpace::Unknown,
        // `LeanWorkerSourceCoordinateSpace` is non-exhaustive. Unknown future
        // variants degrade to the explicit unknown label until the host learns
        // how to present them.
        _ => CoordinateSpace::Unknown,
    }
}

pub fn project_failure(failure: &LeanWorkerElabFailure) -> ElabFailure {
    ElabFailure {
        diagnostics: failure.diagnostics.iter().map(project_diagnostic).collect(),
        truncated: failure.truncated,
    }
}

pub(crate) fn project_source_range(range: LeanWorkerSourceRange) -> SourceRange {
    SourceRange {
        file: range.file,
        start_line: range.start_line,
        start_column: range.start_column,
        end_line: range.end_line,
        end_column: range.end_column,
    }
}

/// Strip Lean's synthetic source label so it never reaches the wire. Every
/// call that elaborates a string buffer (rather than a file on disk) gets
/// labelled `<elaborate>`, which is never actionable for the caller.
fn meaningful_file_label(label: &str) -> Option<String> {
    if label.is_empty() || label == "<elaborate>" || label.starts_with('<') {
        None
    } else {
        Some(label.to_owned())
    }
}

/// # Errors
///
/// Returns the projected [`ElabFailure`] in the error arm when the
/// upstream `LeanWorkerElabResult.success` is `false`. Never an
/// infrastructure error.
pub fn project_elab_result(result: LeanWorkerElabResult) -> std::result::Result<ElabSuccess, ElabFailure> {
    if result.success {
        Ok(ElabSuccess { ok: true })
    } else {
        Err(ElabFailure {
            diagnostics: result.diagnostics.iter().map(project_diagnostic).collect(),
            truncated: result.truncated,
        })
    }
}

pub fn project_kernel_result(result: LeanWorkerKernelResult) -> KernelOutcome {
    let status = match result.status {
        LeanWorkerKernelStatus::Checked => "Checked",
        LeanWorkerKernelStatus::Rejected => "Rejected",
        LeanWorkerKernelStatus::Unavailable => "Unavailable",
        LeanWorkerKernelStatus::Unsupported => "Unsupported",
        _ => "Unsupported",
    };
    let summary = result.summary.map(|s| KernelSummary {
        declaration_name: s.declaration_name,
        kind: s.kind,
        type_signature: s.type_signature,
    });
    let failure = if matches!(result.status, LeanWorkerKernelStatus::Checked) {
        None
    } else {
        Some(ElabFailure {
            diagnostics: result.diagnostics.iter().map(project_diagnostic).collect(),
            truncated: result.truncated,
        })
    };
    KernelOutcome {
        status: status.to_owned(),
        summary,
        failure,
    }
}

pub fn project_meta_rendered(result: LeanWorkerMetaResult<LeanWorkerRendered>) -> MetaOutcome {
    match result {
        LeanWorkerMetaResult::Ok { value } => MetaOutcome {
            status: "Ok".into(),
            rendered: Some(value.value),
            definitionally_equal: None,
            failure: None,
            raw_fallback_used: matches!(value.rendering, LeanWorkerRendering::Raw),
        },
        LeanWorkerMetaResult::Failed { failure } => meta_failure("Failed", &failure),
        LeanWorkerMetaResult::TimeoutOrHeartbeat { failure } => meta_failure("TimeoutOrHeartbeat", &failure),
        LeanWorkerMetaResult::Unsupported { failure } => meta_failure("Unsupported", &failure),
        _ => MetaOutcome {
            status: "Unsupported".into(),
            rendered: None,
            definitionally_equal: None,
            failure: None,
            raw_fallback_used: false,
        },
    }
}

pub fn project_meta_bool(result: LeanWorkerMetaResult<bool>) -> MetaOutcome {
    match result {
        LeanWorkerMetaResult::Ok { value } => MetaOutcome {
            status: "Ok".into(),
            rendered: None,
            definitionally_equal: Some(value),
            failure: None,
            raw_fallback_used: false,
        },
        LeanWorkerMetaResult::Failed { failure } => meta_failure("Failed", &failure),
        LeanWorkerMetaResult::TimeoutOrHeartbeat { failure } => meta_failure("TimeoutOrHeartbeat", &failure),
        LeanWorkerMetaResult::Unsupported { failure } => meta_failure("Unsupported", &failure),
        _ => MetaOutcome {
            status: "Unsupported".into(),
            rendered: None,
            definitionally_equal: None,
            failure: None,
            raw_fallback_used: false,
        },
    }
}

fn meta_failure(status: &str, failure: &LeanWorkerElabFailure) -> MetaOutcome {
    MetaOutcome {
        status: status.to_owned(),
        rendered: None,
        definitionally_equal: None,
        failure: Some(project_failure(failure)),
        raw_fallback_used: false,
    }
}

pub fn project_declaration_row(row: LeanWorkerDeclarationRow) -> DeclarationRow {
    DeclarationRow {
        name: row.name,
        kind: row.kind,
        type_signature: row.type_signature,
        source: row.source.map(project_source_range),
    }
}

pub(crate) fn project_rendered_info(info: LeanWorkerRenderedInfo) -> RenderedText {
    RenderedText {
        value: info.value,
        truncated: info.truncated,
    }
}

fn rendering_label(rendering: LeanWorkerRendering) -> String {
    match rendering {
        LeanWorkerRendering::Pretty => "pretty".to_owned(),
        LeanWorkerRendering::Raw => "raw".to_owned(),
        // `LeanWorkerRendering` is `#[non_exhaustive]`. An unknown future
        // variant falls back to "raw" (least surprising to a reader expecting
        // elaborated output); re-check this label when bumping lean-rs.
        _ => "raw".to_owned(),
    }
}

pub(crate) fn project_module_source_span(span: LeanWorkerModuleSourceSpan) -> ModuleSourceSpan {
    ModuleSourceSpan {
        start_line: span.start_line,
        start_column: span.start_column,
        end_line: span.end_line,
        end_column: span.end_column,
    }
}

pub(crate) fn project_proof_action_target(info: LeanWorkerDeclarationTargetInfo) -> ProofActionDeclarationTarget {
    ProofActionDeclarationTarget {
        short_name: info.short_name,
        declaration_name: info.declaration_name,
        namespace_name: info.namespace_name,
        declaration_kind: info.declaration_kind,
        declaration_span: project_module_source_span(info.declaration_span),
        name_span: project_module_source_span(info.name_span),
        body_span: project_module_source_span(info.body_span),
    }
}

pub(crate) fn project_declaration_flags(flags: LeanWorkerDeclarationFlags) -> DeclarationFlags {
    DeclarationFlags {
        is_private: flags.is_private,
        is_generated: flags.is_generated,
        is_internal: flags.is_internal,
    }
}

fn project_declaration_summary(row: LeanWorkerDeclarationSearchRow) -> DeclarationSummary {
    DeclarationSummary {
        name: row.name,
        kind: row.kind,
        module: row.module,
        source: row.source.map(project_source_range),
        match_reason: row.match_reason,
        score: row.score,
        rank: row.rank,
        flags: project_declaration_flags(row.flags),
    }
}

fn project_declaration_search_pruning(row: LeanWorkerDeclarationSearchPruning) -> DeclarationSearchPruning {
    DeclarationSearchPruning {
        stage: row.stage,
        reason: row.reason,
        count: row.count,
    }
}

fn project_declaration_search_timings(timings: LeanWorkerDeclarationSearchTimings) -> DeclarationSearchTimings {
    DeclarationSearchTimings {
        scan_micros: timings.scan_micros,
        rank_micros: timings.rank_micros,
        source_micros: timings.source_micros,
    }
}

fn project_declaration_search_facts(facts: LeanWorkerDeclarationSearchFacts) -> DeclarationSearchFacts {
    DeclarationSearchFacts {
        declarations_scanned: facts.declarations_scanned,
        after_name_filter: facts.after_name_filter,
        after_kind_filter: facts.after_kind_filter,
        after_required_constants_filter: facts.after_required_constants_filter,
        after_conclusion_filter: facts.after_conclusion_filter,
        after_scope_filter: facts.after_scope_filter,
        source_lookups: facts.source_lookups,
        broad_pruning: facts
            .broad_pruning
            .into_iter()
            .map(project_declaration_search_pruning)
            .collect(),
        truncated: facts.truncated,
        timings: project_declaration_search_timings(facts.timings),
    }
}

pub fn project_declaration_search(result: LeanWorkerDeclarationSearchResult) -> DeclarationSearchResult {
    DeclarationSearchResult {
        declarations: result
            .declarations
            .into_iter()
            .map(project_declaration_summary)
            .collect(),
        truncated: result.truncated,
        facts: project_declaration_search_facts(result.facts),
    }
}

pub fn project_declaration_inspection(result: LeanWorkerDeclarationInspectionResult) -> DeclarationInspectionResult {
    match result {
        LeanWorkerDeclarationInspectionResult::Found { declaration } => DeclarationInspectionResult::Found {
            declaration: Box::new(project_inspection(*declaration)),
        },
        LeanWorkerDeclarationInspectionResult::NotFound { name } => {
            DeclarationInspectionResult::NotFound { name: Some(name) }
        }
        LeanWorkerDeclarationInspectionResult::Unsupported => DeclarationInspectionResult::Unsupported,
        // `LeanWorkerDeclarationInspectionResult` is `Found | NotFound |
        // Unsupported` on the current worker (the enum is `#[non_exhaustive]`,
        // hence this arm). It has no `Ambiguous`/incomplete-build variant, so
        // unlike `verify_declaration` there is no `needs_build` case to
        // reclassify here. If the worker gains one (see
        // ~/Code/prompts/lean-rs/12-*.md), route it through `crate::diagnosis`.
        _ => DeclarationInspectionResult::Unsupported,
    }
}

pub fn project_proof_attempt(result: LeanWorkerProofAttemptResult) -> ProofAttemptResult {
    match result {
        LeanWorkerProofAttemptResult::Ok { result, imports } => ProofAttemptResult::Ok {
            result: project_proof_attempt_envelope(result),
            imports,
        },
        LeanWorkerProofAttemptResult::MissingImports {
            result,
            imports,
            missing,
        } => ProofAttemptResult::MissingImports {
            result: project_proof_attempt_envelope(result),
            imports,
            missing,
        },
        LeanWorkerProofAttemptResult::HeaderParseFailed { diagnostics } => ProofAttemptResult::HeaderParseFailed {
            diagnostics: project_failure(&diagnostics),
        },
        LeanWorkerProofAttemptResult::Unsupported => ProofAttemptResult::Unsupported,
        _ => ProofAttemptResult::Unsupported,
    }
}

pub(crate) fn project_proof_attempt_envelope(envelope: LeanWorkerProofAttemptEnvelope) -> ProofAttemptEnvelope {
    let candidates: Vec<_> = envelope.candidates.into_iter().map(project_proof_attempt_row).collect();
    let summary = proof_attempt_summary(
        &candidates,
        envelope.candidate_limit,
        envelope.candidates_truncated,
        candidates.len(),
    );
    ProofAttemptEnvelope {
        candidates,
        candidate_limit: envelope.candidate_limit,
        candidates_truncated: envelope.candidates_truncated,
        summary,
    }
}

pub(crate) fn project_proof_attempt_row(row: LeanWorkerProofAttemptRow) -> ProofAttemptCandidate {
    ProofAttemptCandidate {
        id: row.id,
        status: proof_attempt_status(row.status).to_owned(),
        snippet: project_rendered_info(row.candidate_text),
        diagnostics: project_failure(&row.diagnostics),
        downstream_diagnostics: project_failure(&row.downstream_diagnostics),
        goals: row.goals.into_iter().map(project_rendered_info).collect(),
        declaration: row.declaration.map(project_proof_action_target),
        proof_position: row.proof_position.map(|position| ProofPositionSummary {
            index: position.index,
            tactic: project_rendered_info(position.tactic),
        }),
        output_truncated: row.output_truncated,
    }
}

fn proof_attempt_status(status: LeanWorkerProofAttemptStatus) -> &'static str {
    match status {
        LeanWorkerProofAttemptStatus::Closed => "closed",
        LeanWorkerProofAttemptStatus::Progressed => "progressed",
        LeanWorkerProofAttemptStatus::Failed => "failed",
        LeanWorkerProofAttemptStatus::Timeout => "timeout",
        LeanWorkerProofAttemptStatus::BudgetExceeded => "budget_exceeded",
        LeanWorkerProofAttemptStatus::NotAttempted => "not_attempted",
        LeanWorkerProofAttemptStatus::Unsupported => "unsupported",
        _ => "unsupported",
    }
}

fn proof_attempt_summary(
    candidates: &[ProofAttemptCandidate],
    candidate_limit: u32,
    candidates_truncated: bool,
    requested_candidates: usize,
) -> ProofAttemptSummary {
    let mut summary = ProofAttemptSummary {
        requested_candidates: requested_candidates.try_into().unwrap_or(u32::MAX),
        returned_candidates: candidates.len().try_into().unwrap_or(u32::MAX),
        candidate_limit,
        candidates_truncated,
        partial: candidates_truncated,
        closed: 0,
        progressed: 0,
        failed: 0,
        timeout: 0,
        budget_exceeded: 0,
        not_attempted: 0,
        unsupported: 0,
        output_truncated: 0,
    };
    for candidate in candidates {
        match candidate.status.as_str() {
            "closed" => summary.closed = summary.closed.saturating_add(1),
            "progressed" => summary.progressed = summary.progressed.saturating_add(1),
            "failed" => summary.failed = summary.failed.saturating_add(1),
            "timeout" => {
                summary.timeout = summary.timeout.saturating_add(1);
                summary.partial = true;
            }
            "budget_exceeded" => {
                summary.budget_exceeded = summary.budget_exceeded.saturating_add(1);
                summary.partial = true;
            }
            "not_attempted" => {
                summary.not_attempted = summary.not_attempted.saturating_add(1);
                summary.partial = true;
            }
            _ => summary.unsupported = summary.unsupported.saturating_add(1),
        }
        if candidate.output_truncated {
            summary.output_truncated = summary.output_truncated.saturating_add(1);
            summary.partial = true;
        }
    }
    summary
}

pub fn project_declaration_verification(
    result: LeanWorkerDeclarationVerificationResult,
) -> DeclarationVerificationResult {
    match result {
        LeanWorkerDeclarationVerificationResult::Ok {
            verification_status,
            facts,
            imports,
        } => {
            let label = verification_status_label(verification_status, &facts);
            // `needs_build` (incomplete environment) and `ambiguous` (no single
            // resolved target) both mean the facts describe nothing checked, so
            // they are not trustworthy.
            let trustworthy = label != crate::diagnosis::NEEDS_BUILD_STATUS && label != "ambiguous";
            DeclarationVerificationResult::Ok {
                verification_status: label.to_owned(),
                facts: Box::new(project_declaration_verification_facts(*facts, trustworthy)),
                imports,
            }
        }
        LeanWorkerDeclarationVerificationResult::MissingImports {
            verification_status,
            facts,
            imports,
            missing,
        } => DeclarationVerificationResult::MissingImports {
            verification_status: verification_status_label(verification_status, &facts).to_owned(),
            // Imports the worker could not load: the environment is incomplete,
            // so the verdict's facts are not trustworthy.
            facts: Box::new(project_declaration_verification_facts(*facts, false)),
            imports,
            missing,
        },
        LeanWorkerDeclarationVerificationResult::HeaderParseFailed { diagnostics } => {
            DeclarationVerificationResult::HeaderParseFailed {
                diagnostics: project_failure(&diagnostics),
            }
        }
        LeanWorkerDeclarationVerificationResult::Unsupported => DeclarationVerificationResult::Unsupported,
        _ => DeclarationVerificationResult::Unsupported,
    }
}

fn project_declaration_verification_facts(
    facts: LeanWorkerDeclarationVerificationFacts,
    facts_trustworthy: bool,
) -> DeclarationVerificationFacts {
    DeclarationVerificationFacts {
        target: facts.target.map(project_proof_action_target),
        diagnostics: project_failure(&facts.diagnostics),
        unresolved_goals: facts.unresolved_goals.into_iter().map(project_rendered_info).collect(),
        contains_sorry: facts.contains_sorry,
        contains_admit: facts.contains_admit,
        contains_sorry_ax: facts.contains_sorry_ax,
        axioms: facts.axioms,
        axioms_truncated: facts.axioms_truncated,
        axioms_available: facts.axioms_available,
        output_truncated: facts.output_truncated,
        candidates: facts.candidates.into_iter().map(project_proof_action_target).collect(),
        facts_trustworthy,
    }
}

fn verification_status_label(
    status: LeanWorkerDeclarationVerificationStatus,
    facts: &LeanWorkerDeclarationVerificationFacts,
) -> &'static str {
    match status {
        LeanWorkerDeclarationVerificationStatus::Accepted => "verified",
        LeanWorkerDeclarationVerificationStatus::Rejected if facts.contains_sorry => "has_sorry",
        LeanWorkerDeclarationVerificationStatus::Rejected if !facts.unresolved_goals.is_empty() => {
            "has_unresolved_goals"
        }
        LeanWorkerDeclarationVerificationStatus::Rejected if !facts.diagnostics.diagnostics.is_empty() => {
            "has_diagnostics"
        }
        LeanWorkerDeclarationVerificationStatus::Rejected => "has_diagnostics",
        LeanWorkerDeclarationVerificationStatus::NotFound => "not_found",
        // Genuine multiple-resolution: the worker (protocol 8) attaches the
        // competing declarations in `facts.candidates`.
        LeanWorkerDeclarationVerificationStatus::Ambiguous => "ambiguous",
        // The name did not resolve because the open environment is incomplete;
        // the enclosing `MissingImports` outcome names the unbuilt modules.
        LeanWorkerDeclarationVerificationStatus::NeedsBuild => crate::diagnosis::NEEDS_BUILD_STATUS,
        LeanWorkerDeclarationVerificationStatus::Timeout => "timeout",
        LeanWorkerDeclarationVerificationStatus::BudgetExceeded => "budget_exceeded",
        LeanWorkerDeclarationVerificationStatus::Unsupported => "unsupported",
        _ => "unsupported",
    }
}

pub(crate) fn project_inspection(declaration: WorkerDeclarationInspection) -> DeclarationInspection {
    DeclarationInspection {
        name: declaration.name,
        kind: declaration.kind,
        module: declaration.module,
        source: declaration.source.map(project_source_range),
        statement: declaration.statement.map(project_rendered_info),
        statement_rendering: declaration.statement_rendering.map(rendering_label),
        docstring: declaration.docstring.map(project_rendered_info),
        attributes: declaration.attributes,
        proof_search: project_proof_search_facts(declaration.proof_search),
        flags: project_declaration_flags(declaration.flags),
    }
}

fn project_proof_search_facts(facts: LeanWorkerDeclarationProofSearchFacts) -> DeclarationProofSearchFacts {
    DeclarationProofSearchFacts {
        is_simp: facts.is_simp,
        is_rw_candidate: facts.is_rw_candidate,
        is_instance: facts.is_instance,
        is_class: facts.is_class,
        class_name: facts.class_name,
    }
}

#[cfg(test)]
#[allow(
    clippy::unwrap_used,
    clippy::panic,
    reason = "unit tests fail directly on the wrong variant"
)]
mod tests {
    use super::*;

    fn clean_facts() -> LeanWorkerDeclarationVerificationFacts {
        LeanWorkerDeclarationVerificationFacts {
            target: None,
            diagnostics: LeanWorkerElabFailure {
                diagnostics: Vec::new(),
                truncated: false,
            },
            unresolved_goals: Vec::new(),
            contains_sorry: false,
            contains_admit: false,
            contains_sorry_ax: false,
            axioms: Vec::new(),
            axioms_truncated: false,
            axioms_available: true,
            output_truncated: false,
            candidates: Vec::new(),
        }
    }

    fn target_info(name: &str) -> LeanWorkerDeclarationTargetInfo {
        let span = lean_rs_worker_parent::LeanWorkerModuleSourceSpan {
            start_line: 0,
            start_column: 0,
            end_line: 0,
            end_column: 0,
        };
        LeanWorkerDeclarationTargetInfo {
            short_name: name.rsplit('.').next().unwrap_or(name).to_owned(),
            declaration_name: name.to_owned(),
            namespace_name: name.rsplit_once('.').map(|(ns, _)| ns.to_owned()).unwrap_or_default(),
            declaration_kind: "theorem".to_owned(),
            declaration_span: span.clone(),
            name_span: span.clone(),
            body_span: span,
        }
    }

    fn rendered(value: &str) -> LeanWorkerRenderedInfo {
        LeanWorkerRenderedInfo {
            value: value.to_owned(),
            truncated: false,
        }
    }

    fn no_failure() -> LeanWorkerElabFailure {
        LeanWorkerElabFailure {
            diagnostics: Vec::new(),
            truncated: false,
        }
    }

    #[test]
    fn proof_attempt_projection_preserves_not_attempted_status_and_summary() {
        let envelope = project_proof_attempt_envelope(LeanWorkerProofAttemptEnvelope {
            candidates: vec![
                LeanWorkerProofAttemptRow {
                    id: "candidate_1".to_owned(),
                    status: LeanWorkerProofAttemptStatus::Closed,
                    candidate_text: rendered("trivial"),
                    diagnostics: no_failure(),
                    downstream_diagnostics: no_failure(),
                    goals: Vec::new(),
                    declaration: None,
                    proof_position: None,
                    output_truncated: false,
                },
                LeanWorkerProofAttemptRow {
                    id: "candidate_2".to_owned(),
                    status: LeanWorkerProofAttemptStatus::NotAttempted,
                    candidate_text: rendered("exact later"),
                    diagnostics: no_failure(),
                    downstream_diagnostics: no_failure(),
                    goals: Vec::new(),
                    declaration: None,
                    proof_position: None,
                    output_truncated: false,
                },
            ],
            candidate_limit: 16,
            candidates_truncated: false,
        });
        assert_eq!(
            envelope.candidates.get(1).map(|candidate| candidate.status.as_str()),
            Some("not_attempted")
        );
        assert_eq!(envelope.summary.closed, 1);
        assert_eq!(envelope.summary.not_attempted, 1);
        assert!(envelope.summary.partial);
    }

    #[test]
    fn diagnostic_projection_labels_coordinate_spaces() {
        let original = project_diagnostic(&LeanWorkerDiagnostic {
            severity: "error".to_owned(),
            message: "unknown identifier".to_owned(),
            file_label: "/tmp/Demo.lean".to_owned(),
            line: Some(2),
            column: Some(9),
            end_line: Some(2),
            end_column: Some(16),
            coordinate_space: LeanWorkerSourceCoordinateSpace::OriginalSource,
            original_range: Some(LeanWorkerSourceRange {
                file: "/tmp/Demo.lean".to_owned(),
                start_line: 2,
                start_column: 9,
                end_line: 2,
                end_column: 16,
            }),
        });
        assert_eq!(original.coordinate_space, CoordinateSpace::OriginalSource);
        assert_eq!(
            original.original_range.as_ref().map(|range| range.file.as_str()),
            Some("/tmp/Demo.lean")
        );
        assert!(original.synthetic_range.is_none());

        let synthetic = project_diagnostic(&LeanWorkerDiagnostic {
            severity: "error".to_owned(),
            message: "unknown tactic".to_owned(),
            file_label: "<proof-step>".to_owned(),
            line: Some(82),
            column: Some(3),
            end_line: Some(82),
            end_column: Some(12),
            coordinate_space: LeanWorkerSourceCoordinateSpace::SyntheticBuffer,
            original_range: None,
        });
        assert_eq!(synthetic.coordinate_space, CoordinateSpace::SyntheticBuffer);
        assert!(synthetic.original_range.is_none());
        assert_eq!(synthetic.synthetic_range.as_ref().map(|range| range.line), Some(82));

        let unknown = project_diagnostic(&LeanWorkerDiagnostic {
            severity: "warning".to_owned(),
            message: "mapping unavailable".to_owned(),
            file_label: String::new(),
            line: None,
            column: None,
            end_line: None,
            end_column: None,
            coordinate_space: LeanWorkerSourceCoordinateSpace::Unknown,
            original_range: None,
        });
        assert_eq!(unknown.coordinate_space, CoordinateSpace::Unknown);
        assert!(unknown.coordinate_note.is_some());
    }

    #[test]
    fn needs_build_verification_is_labeled_needs_build_with_untrustworthy_facts() {
        let result = project_declaration_verification(LeanWorkerDeclarationVerificationResult::Ok {
            verification_status: LeanWorkerDeclarationVerificationStatus::NeedsBuild,
            facts: Box::new(clean_facts()),
            imports: Vec::new(),
        });
        let DeclarationVerificationResult::Ok {
            verification_status,
            facts,
            ..
        } = result
        else {
            panic!("expected an Ok verdict");
        };
        assert_eq!(verification_status, "needs_build");
        // Facts retained (not nulled) but flagged untrustworthy so a reader
        // can't take the clean `contains_sorry:false` at face value when the
        // environment was incomplete.
        assert!(!facts.facts_trustworthy);
        assert!(!facts.contains_sorry);
    }

    #[test]
    fn ambiguous_verification_surfaces_candidates_with_untrustworthy_facts() {
        let mut facts = clean_facts();
        facts.candidates = vec![target_info("A.foo"), target_info("B.foo")];
        let result = project_declaration_verification(LeanWorkerDeclarationVerificationResult::Ok {
            verification_status: LeanWorkerDeclarationVerificationStatus::Ambiguous,
            facts: Box::new(facts),
            imports: Vec::new(),
        });
        let DeclarationVerificationResult::Ok {
            verification_status,
            facts,
            ..
        } = result
        else {
            panic!("expected an Ok verdict");
        };
        // Genuine ambiguity keeps the "ambiguous" verdict (it is actionable now
        // that competitors are named) and is not relabeled to needs_build.
        assert_eq!(verification_status, "ambiguous");
        assert_eq!(facts.candidates.len(), 2);
        assert!(!facts.facts_trustworthy);
    }

    #[test]
    fn accepted_verification_keeps_facts_trustworthy() {
        let result = project_declaration_verification(LeanWorkerDeclarationVerificationResult::Ok {
            verification_status: LeanWorkerDeclarationVerificationStatus::Accepted,
            facts: Box::new(clean_facts()),
            imports: Vec::new(),
        });
        let DeclarationVerificationResult::Ok {
            verification_status,
            facts,
            ..
        } = result
        else {
            panic!("expected an Ok verdict");
        };
        assert_eq!(verification_status, "verified");
        assert!(facts.facts_trustworthy);
    }
}