lean_rs/module/
preflight.rs

1//! Manifest-backed loader preflight for shipped Lean capabilities.
2//!
3//! This module turns avoidable loader failures into stable, actionable
4//! diagnostics before callers hit platform-specific dynamic-loader text. It
5//! does not expose `ldd`, `otool`, `readelf`, `nm`, loader flags, or raw object
6//! parser details. The public contract is a report: what failed, which artifact
7//! it concerned, and what the caller should rebuild or package.
8
9use std::collections::HashSet;
10use std::path::{Path, PathBuf};
11
12use object::{Object, ObjectSymbol};
13
14use super::initializer::InitializerName;
15use super::{LeanBuiltCapability, LeanLibraryDependency};
16use crate::error::{LeanError, bound_message};
17
18/// Stable preflight diagnostic codes for manifest-backed capability loading.
19#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash)]
20pub enum LeanLoaderDiagnosticCode {
21    /// The manifest path was absent, unreadable, or pointed at a missing file.
22    MissingManifest,
23    /// The manifest was not valid JSON or missed required fields.
24    MalformedManifest,
25    /// The manifest schema version is newer or otherwise unsupported.
26    UnsupportedManifestSchema,
27    /// The manifest's primary capability dylib is missing.
28    MissingPrimaryDylib,
29    /// A dependency dylib named by the manifest is missing.
30    MissingTransitiveDependency,
31    /// A dylib could not be parsed as a native object for this platform.
32    UnsupportedArchitecture,
33    /// The manifest was produced by an unsupported or mismatched Lean toolchain.
34    UnsupportedToolchainFingerprint,
35    /// A manifest appears older than the build artifact it describes.
36    StaleManifest,
37    /// The root module initializer named by the manifest is not exported.
38    MissingInitializer,
39    /// A Lean/imported symbol is not supplied by the manifest dependency set.
40    MissingImportedSymbol,
41}
42
43impl LeanLoaderDiagnosticCode {
44    /// Stable string identifier suitable for logs and support reports.
45    #[must_use]
46    pub const fn as_str(self) -> &'static str {
47        match self {
48            Self::MissingManifest => "lean_rs.loader.missing_manifest",
49            Self::MalformedManifest => "lean_rs.loader.malformed_manifest",
50            Self::UnsupportedManifestSchema => "lean_rs.loader.unsupported_manifest_schema",
51            Self::MissingPrimaryDylib => "lean_rs.loader.missing_primary_dylib",
52            Self::MissingTransitiveDependency => "lean_rs.loader.missing_transitive_dependency",
53            Self::UnsupportedArchitecture => "lean_rs.loader.unsupported_architecture",
54            Self::UnsupportedToolchainFingerprint => "lean_rs.loader.unsupported_toolchain_fingerprint",
55            Self::StaleManifest => "lean_rs.loader.stale_manifest",
56            Self::MissingInitializer => "lean_rs.loader.missing_initializer",
57            Self::MissingImportedSymbol => "lean_rs.loader.missing_imported_symbol",
58        }
59    }
60}
61
62impl std::fmt::Display for LeanLoaderDiagnosticCode {
63    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
64        f.write_str(self.as_str())
65    }
66}
67
68/// Severity of one loader preflight finding.
69#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash)]
70pub enum LeanLoaderSeverity {
71    /// Informational finding that does not block loading.
72    Info,
73    /// Suspicious state that may still load.
74    Warning,
75    /// The capability should not be opened until this is fixed.
76    Error,
77}
78
79/// One bounded preflight finding.
80#[derive(Clone, Debug, Eq, PartialEq)]
81pub struct LeanLoaderCheck {
82    code: LeanLoaderDiagnosticCode,
83    severity: LeanLoaderSeverity,
84    subject: String,
85    message: String,
86    repair_hint: String,
87}
88
89impl LeanLoaderCheck {
90    fn error(
91        code: LeanLoaderDiagnosticCode,
92        subject: impl Into<String>,
93        message: impl Into<String>,
94        repair_hint: impl Into<String>,
95    ) -> Self {
96        Self {
97            code,
98            severity: LeanLoaderSeverity::Error,
99            subject: bound_message(subject.into()),
100            message: bound_message(message.into()),
101            repair_hint: bound_message(repair_hint.into()),
102        }
103    }
104
105    /// Stable loader diagnostic code.
106    #[must_use]
107    pub fn code(&self) -> LeanLoaderDiagnosticCode {
108        self.code
109    }
110
111    /// Whether this finding blocks capability loading.
112    #[must_use]
113    pub fn severity(&self) -> LeanLoaderSeverity {
114        self.severity
115    }
116
117    /// Artifact, symbol, or manifest field this finding is about.
118    #[must_use]
119    pub fn subject(&self) -> &str {
120        &self.subject
121    }
122
123    /// Bounded explanation of the failure.
124    #[must_use]
125    pub fn message(&self) -> &str {
126        &self.message
127    }
128
129    /// Bounded repair hint for normal users.
130    #[must_use]
131    pub fn repair_hint(&self) -> &str {
132        &self.repair_hint
133    }
134}
135
136impl std::fmt::Display for LeanLoaderCheck {
137    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
138        write!(
139            f,
140            "{} [{:?}] {}: {} (repair: {})",
141            self.code.as_str(),
142            self.severity,
143            self.subject,
144            self.message,
145            self.repair_hint
146        )
147    }
148}
149
150/// Structured result of loader preflight for one capability manifest.
151#[derive(Clone, Debug, Eq, PartialEq)]
152pub struct LeanLoaderReport {
153    manifest_path: Option<PathBuf>,
154    checks: Vec<LeanLoaderCheck>,
155}
156
157impl LeanLoaderReport {
158    fn new(manifest_path: Option<PathBuf>, checks: Vec<LeanLoaderCheck>) -> Self {
159        Self { manifest_path, checks }
160    }
161
162    /// Manifest path checked, if the descriptor resolved one.
163    #[must_use]
164    pub fn manifest_path(&self) -> Option<&Path> {
165        self.manifest_path.as_deref()
166    }
167
168    /// All preflight findings.
169    #[must_use]
170    pub fn checks(&self) -> &[LeanLoaderCheck] {
171        &self.checks
172    }
173
174    /// Blocking findings only.
175    pub fn errors(&self) -> impl Iterator<Item = &LeanLoaderCheck> {
176        self.checks
177            .iter()
178            .filter(|check| check.severity == LeanLoaderSeverity::Error)
179    }
180
181    /// Whether preflight found no blocking findings.
182    #[must_use]
183    pub fn is_ok(&self) -> bool {
184        self.errors().next().is_none()
185    }
186
187    /// First blocking finding, if any.
188    #[must_use]
189    pub fn first_error(&self) -> Option<&LeanLoaderCheck> {
190        self.errors().next()
191    }
192
193    pub(crate) fn into_error(self) -> LeanError {
194        let Some(first) = self
195            .checks
196            .into_iter()
197            .find(|check| check.severity == LeanLoaderSeverity::Error)
198        else {
199            return LeanError::module_init("Lean capability preflight failed without a recorded finding");
200        };
201        LeanError::module_init(format!(
202            "{}: {}. repair: {}",
203            first.code.as_str(),
204            first.message,
205            first.repair_hint
206        ))
207    }
208}
209
210/// Preflight runner for manifest-backed Lean capabilities.
211#[derive(Clone, Debug, Eq, PartialEq)]
212pub struct LeanCapabilityPreflight {
213    spec: LeanBuiltCapability,
214}
215
216impl LeanCapabilityPreflight {
217    /// Create a preflight runner for a build-script capability descriptor.
218    #[must_use]
219    pub fn new(spec: LeanBuiltCapability) -> Self {
220        Self { spec }
221    }
222
223    /// Check manifest, artifact, toolchain, dependency, and initializer facts.
224    #[must_use]
225    pub fn check(&self) -> LeanLoaderReport {
226        let manifest_path = match self.spec.resolved_manifest_path() {
227            Ok(path) => path,
228            Err(err) => {
229                return LeanLoaderReport::new(
230                    None,
231                    vec![LeanLoaderCheck::error(
232                        LeanLoaderDiagnosticCode::MissingManifest,
233                        "manifest",
234                        err.to_string(),
235                        "rebuild the Lean capability through CargoLeanCapability and embed the manifest env var",
236                    )],
237                );
238            }
239        };
240
241        let manifest = match CapabilityManifest::read(&manifest_path) {
242            Ok(manifest) => manifest,
243            Err(check) => return LeanLoaderReport::new(Some(manifest_path), vec![check]),
244        };
245
246        let mut checks = Vec::new();
247        check_fingerprint(&manifest, &mut checks);
248        check_staleness(&manifest_path, &manifest, &mut checks);
249
250        let mut dependency_exports = HashSet::new();
251        for dependency in &manifest.dependencies {
252            match inspect_artifact(dependency.path_ref(), ArtifactRole::Dependency) {
253                Ok(info) => {
254                    dependency_exports.extend(info.defined_symbols);
255                }
256                Err(check) => checks.push(check),
257            }
258        }
259
260        match inspect_artifact(&manifest.primary_dylib, ArtifactRole::Primary) {
261            Ok(info) => {
262                check_initializer(&manifest, &info, &mut checks);
263                check_imported_symbols(&manifest, &info, &dependency_exports, &mut checks);
264            }
265            Err(check) => checks.push(check),
266        }
267
268        LeanLoaderReport::new(Some(manifest_path), checks)
269    }
270}
271
272#[derive(Clone, Debug, Eq, PartialEq)]
273pub(crate) struct CapabilityManifest {
274    pub(crate) primary_dylib: PathBuf,
275    pub(crate) package: String,
276    pub(crate) module: String,
277    pub(crate) dependencies: Vec<LeanLibraryDependency>,
278    pub(crate) lean_version: Option<String>,
279    pub(crate) resolved_lean_version: Option<String>,
280    pub(crate) lean_header_sha256: Option<String>,
281}
282
283impl CapabilityManifest {
284    pub(crate) fn read(path: &Path) -> Result<Self, LeanLoaderCheck> {
285        let bytes = std::fs::read(path).map_err(|err| {
286            let code = if err.kind() == std::io::ErrorKind::NotFound {
287                LeanLoaderDiagnosticCode::MissingManifest
288            } else {
289                LeanLoaderDiagnosticCode::MalformedManifest
290            };
291            LeanLoaderCheck::error(
292                code,
293                path.display().to_string(),
294                format!("failed to read Lean capability manifest '{}': {err}", path.display()),
295                "rebuild the Lean capability through CargoLeanCapability and ensure the manifest file is packaged",
296            )
297        })?;
298        let value: serde_json::Value = serde_json::from_slice(&bytes).map_err(|err| {
299            LeanLoaderCheck::error(
300                LeanLoaderDiagnosticCode::MalformedManifest,
301                path.display().to_string(),
302                format!("Lean capability manifest '{}' is not valid JSON: {err}", path.display()),
303                "rebuild the Lean capability through CargoLeanCapability",
304            )
305        })?;
306        let schema_version = required_u64(&value, "schema_version", path)?;
307        if schema_version != u64::from(lean_toolchain::CAPABILITY_MANIFEST_SCHEMA_VERSION) {
308            return Err(LeanLoaderCheck::error(
309                LeanLoaderDiagnosticCode::UnsupportedManifestSchema,
310                path.display().to_string(),
311                format!(
312                    "unsupported Lean capability manifest schema {schema_version}; supported schema is {}",
313                    lean_toolchain::CAPABILITY_MANIFEST_SCHEMA_VERSION
314                ),
315                "rebuild the Lean capability with the same lean-rs version as the runtime crate",
316            ));
317        }
318        let primary_dylib = PathBuf::from(required_string(&value, "primary_dylib", path)?);
319        let package = required_string(&value, "package", path)?;
320        let module = required_string(&value, "module", path)?;
321        let dependencies = dependencies_from_manifest(&value, path)?;
322        let fingerprint = value.get("toolchain_fingerprint").unwrap_or(&serde_json::Value::Null);
323        let lean_version =
324            optional_string(fingerprint, "lean_version").or_else(|| optional_string(&value, "lean_version"));
325        let resolved_lean_version = optional_string(fingerprint, "resolved_version")
326            .or_else(|| optional_string(&value, "resolved_lean_version"));
327        let lean_header_sha256 =
328            optional_string(fingerprint, "header_sha256").or_else(|| optional_string(&value, "lean_header_sha256"));
329        Ok(Self {
330            primary_dylib,
331            package,
332            module,
333            dependencies,
334            lean_version,
335            resolved_lean_version,
336            lean_header_sha256,
337        })
338    }
339}
340
341#[derive(Clone, Debug)]
342struct ArtifactInfo {
343    defined_symbols: HashSet<String>,
344    undefined_symbols: HashSet<String>,
345}
346
347#[derive(Copy, Clone, Debug, Eq, PartialEq)]
348enum ArtifactRole {
349    Primary,
350    Dependency,
351}
352
353fn inspect_artifact(path: &Path, role: ArtifactRole) -> Result<ArtifactInfo, LeanLoaderCheck> {
354    let missing_code = match role {
355        ArtifactRole::Primary => LeanLoaderDiagnosticCode::MissingPrimaryDylib,
356        ArtifactRole::Dependency => LeanLoaderDiagnosticCode::MissingTransitiveDependency,
357    };
358    let repair = match role {
359        ArtifactRole::Primary => {
360            "rebuild the Lean capability through CargoLeanCapability and package the primary dylib"
361        }
362        ArtifactRole::Dependency => {
363            "rebuild the Lean capability through CargoLeanCapability and package every manifest dependency"
364        }
365    };
366    let bytes = std::fs::read(path).map_err(|err| {
367        let code = if err.kind() == std::io::ErrorKind::NotFound {
368            missing_code
369        } else {
370            LeanLoaderDiagnosticCode::UnsupportedArchitecture
371        };
372        LeanLoaderCheck::error(
373            code,
374            path.display().to_string(),
375            format!("failed to read Lean dylib '{}': {err}", path.display()),
376            repair,
377        )
378    })?;
379    let file = object::File::parse(&*bytes).map_err(|err| {
380        LeanLoaderCheck::error(
381            LeanLoaderDiagnosticCode::UnsupportedArchitecture,
382            path.display().to_string(),
383            format!(
384                "Lean dylib '{}' is not a supported native object for this platform: {err}",
385                path.display()
386            ),
387            "rebuild the Lean capability for the current target architecture",
388        )
389    })?;
390    if !architecture_matches_host(file.architecture()) {
391        return Err(LeanLoaderCheck::error(
392            LeanLoaderDiagnosticCode::UnsupportedArchitecture,
393            path.display().to_string(),
394            format!(
395                "Lean dylib '{}' has architecture {:?}, but this process is {}",
396                path.display(),
397                file.architecture(),
398                std::env::consts::ARCH
399            ),
400            "rebuild the Lean capability for the current target architecture",
401        ));
402    }
403    let strip_underscore = matches!(file.format(), object::BinaryFormat::MachO | object::BinaryFormat::Wasm);
404    let mut defined_symbols = HashSet::new();
405    let mut undefined_symbols = HashSet::new();
406    for symbol in file.symbols().chain(file.dynamic_symbols()) {
407        let Ok(name) = symbol.name() else {
408            continue;
409        };
410        let normalised = normalise_symbol_name(name, strip_underscore);
411        if normalised.is_empty() {
412            continue;
413        }
414        if symbol.is_undefined() {
415            undefined_symbols.insert(normalised.to_owned());
416        } else if symbol.is_global() {
417            defined_symbols.insert(normalised.to_owned());
418        }
419    }
420    Ok(ArtifactInfo {
421        defined_symbols,
422        undefined_symbols,
423    })
424}
425
426fn check_initializer(manifest: &CapabilityManifest, primary: &ArtifactInfo, checks: &mut Vec<LeanLoaderCheck>) {
427    let initializer = match InitializerName::from_lake_names(&manifest.package, &manifest.module) {
428        Ok(initializer) => initializer,
429        Err(err) => {
430            checks.push(LeanLoaderCheck::error(
431                LeanLoaderDiagnosticCode::MalformedManifest,
432                format!("{}/{}", manifest.package, manifest.module),
433                err.to_string(),
434                "rebuild the manifest with valid Lake package and module names",
435            ));
436            return;
437        }
438    };
439    if primary.defined_symbols.contains(initializer.symbol_str())
440        || primary.defined_symbols.contains(initializer.legacy_symbol_str())
441    {
442        return;
443    }
444    checks.push(LeanLoaderCheck::error(
445        LeanLoaderDiagnosticCode::MissingInitializer,
446        format!("{}/{}", manifest.package, manifest.module),
447        format!(
448            "primary dylib '{}' does not export initializer '{}' or '{}'",
449            manifest.primary_dylib.display(),
450            initializer.symbol_str(),
451            initializer.legacy_symbol_str()
452        ),
453        "check the package/module names and rebuild the Lean capability shared target",
454    ));
455}
456
457fn check_imported_symbols(
458    manifest: &CapabilityManifest,
459    primary: &ArtifactInfo,
460    dependency_exports: &HashSet<String>,
461    checks: &mut Vec<LeanLoaderCheck>,
462) {
463    for symbol in primary
464        .undefined_symbols
465        .iter()
466        .filter(|symbol| is_lean_dependency_symbol(symbol))
467    {
468        if dependency_exports.contains(symbol) {
469            continue;
470        }
471        checks.push(LeanLoaderCheck::error(
472            LeanLoaderDiagnosticCode::MissingImportedSymbol,
473            symbol.clone(),
474            format!(
475                "primary dylib '{}' imports Lean symbol '{symbol}' that is not provided by the manifest dependencies",
476                manifest.primary_dylib.display()
477            ),
478            "rebuild the Lean capability through CargoLeanCapability so dependency dylibs are recorded in the manifest",
479        ));
480        return;
481    }
482}
483
484fn check_fingerprint(manifest: &CapabilityManifest, checks: &mut Vec<LeanLoaderCheck>) {
485    if let Some(version) = manifest.lean_version.as_deref()
486        && lean_rs_sys::supported_for(version).is_none()
487    {
488        checks.push(LeanLoaderCheck::error(
489            LeanLoaderDiagnosticCode::UnsupportedToolchainFingerprint,
490            version,
491            format!("manifest was built with unsupported Lean toolchain {version}"),
492            "rebuild the Lean capability with a Lean version supported by this lean-rs release",
493        ));
494        return;
495    }
496    if let Some(digest) = manifest.lean_header_sha256.as_deref()
497        && digest != lean_rs_sys::LEAN_HEADER_DIGEST
498    {
499        checks.push(LeanLoaderCheck::error(
500            LeanLoaderDiagnosticCode::UnsupportedToolchainFingerprint,
501            digest,
502            format!(
503                "manifest Lean header digest {digest} does not match this process digest {}",
504                lean_rs_sys::LEAN_HEADER_DIGEST
505            ),
506            "rebuild the Lean capability with the same Lean toolchain used by this Rust binary",
507        ));
508        return;
509    }
510    if let Some(resolved) = manifest.resolved_lean_version.as_deref()
511        && resolved != lean_rs_sys::LEAN_RESOLVED_VERSION
512    {
513        checks.push(LeanLoaderCheck::error(
514            LeanLoaderDiagnosticCode::UnsupportedToolchainFingerprint,
515            resolved,
516            format!(
517                "manifest resolved Lean version {resolved} does not match this process resolved version {}",
518                lean_rs_sys::LEAN_RESOLVED_VERSION
519            ),
520            "rebuild the Lean capability with the same Lean toolchain used by this Rust binary",
521        ));
522    }
523}
524
525fn check_staleness(manifest_path: &Path, manifest: &CapabilityManifest, checks: &mut Vec<LeanLoaderCheck>) {
526    let Ok(manifest_modified) = std::fs::metadata(manifest_path).and_then(|metadata| metadata.modified()) else {
527        return;
528    };
529    let Ok(primary_modified) = std::fs::metadata(&manifest.primary_dylib).and_then(|metadata| metadata.modified())
530    else {
531        return;
532    };
533    if primary_modified > manifest_modified {
534        checks.push(LeanLoaderCheck::error(
535            LeanLoaderDiagnosticCode::StaleManifest,
536            manifest_path.display().to_string(),
537            format!(
538                "manifest '{}' is older than primary dylib '{}'",
539                manifest_path.display(),
540                manifest.primary_dylib.display()
541            ),
542            "rebuild the Lean capability through CargoLeanCapability so the manifest matches the dylib",
543        ));
544    }
545}
546
547fn dependencies_from_manifest(
548    value: &serde_json::Value,
549    path: &Path,
550) -> Result<Vec<LeanLibraryDependency>, LeanLoaderCheck> {
551    let Some(raw_dependencies) = value.get("dependencies") else {
552        return Ok(Vec::new());
553    };
554    let dependencies = raw_dependencies.as_array().ok_or_else(|| {
555        LeanLoaderCheck::error(
556            LeanLoaderDiagnosticCode::MalformedManifest,
557            path.display().to_string(),
558            format!(
559                "Lean capability manifest '{}' field `dependencies` must be an array",
560                path.display()
561            ),
562            "rebuild the Lean capability through CargoLeanCapability",
563        )
564    })?;
565    let mut out = Vec::with_capacity(dependencies.len());
566    for dependency in dependencies {
567        let dylib = required_string(dependency, "dylib_path", path)?;
568        let mut descriptor = LeanLibraryDependency::path(dylib);
569        if dependency
570            .get("export_symbols_for_dependents")
571            .and_then(serde_json::Value::as_bool)
572            .unwrap_or(false)
573        {
574            descriptor = descriptor.export_symbols_for_dependents();
575        }
576        if let Some(initializer) = dependency.get("initializer") {
577            let package = required_string(initializer, "package", path)?;
578            let module = required_string(initializer, "module", path)?;
579            descriptor = descriptor.initializer(package, module);
580        }
581        out.push(descriptor);
582    }
583    Ok(out)
584}
585
586fn required_string(value: &serde_json::Value, field: &str, path: &Path) -> Result<String, LeanLoaderCheck> {
587    value
588        .get(field)
589        .and_then(serde_json::Value::as_str)
590        .filter(|value| !value.is_empty())
591        .map(str::to_owned)
592        .ok_or_else(|| {
593            LeanLoaderCheck::error(
594                LeanLoaderDiagnosticCode::MalformedManifest,
595                path.display().to_string(),
596                format!(
597                    "Lean capability manifest '{}' is missing non-empty string field `{field}`",
598                    path.display()
599                ),
600                "rebuild the Lean capability through CargoLeanCapability",
601            )
602        })
603}
604
605fn optional_string(value: &serde_json::Value, field: &str) -> Option<String> {
606    value
607        .get(field)
608        .and_then(serde_json::Value::as_str)
609        .filter(|value| !value.is_empty())
610        .map(str::to_owned)
611}
612
613fn required_u64(value: &serde_json::Value, field: &str, path: &Path) -> Result<u64, LeanLoaderCheck> {
614    value.get(field).and_then(serde_json::Value::as_u64).ok_or_else(|| {
615        LeanLoaderCheck::error(
616            LeanLoaderDiagnosticCode::MalformedManifest,
617            path.display().to_string(),
618            format!(
619                "Lean capability manifest '{}' is missing unsigned integer field `{field}`",
620                path.display()
621            ),
622            "rebuild the Lean capability through CargoLeanCapability",
623        )
624    })
625}
626
627fn architecture_matches_host(architecture: object::Architecture) -> bool {
628    matches!(
629        (std::env::consts::ARCH, architecture),
630        ("x86_64", object::Architecture::X86_64)
631            | ("aarch64", object::Architecture::Aarch64)
632            | ("arm", object::Architecture::Arm)
633            | ("x86", object::Architecture::I386)
634    )
635}
636
637fn normalise_symbol_name(name: &str, strip_underscore: bool) -> &str {
638    if strip_underscore {
639        name.strip_prefix('_').unwrap_or(name)
640    } else {
641        name
642    }
643}
644
645fn is_lean_dependency_symbol(symbol: &str) -> bool {
646    symbol.starts_with("LeanRs") || symbol.starts_with("lean_rs_") || symbol.starts_with("initialize_LeanRs")
647}
648
649pub(crate) fn manifest_error_to_lean_error(check: LeanLoaderCheck) -> LeanError {
650    LeanLoaderReport::new(None, vec![check]).into_error()
651}
652
653#[cfg(test)]
654#[allow(clippy::expect_used, clippy::panic)]
655mod tests {
656    use super::{
657        ArtifactInfo, CapabilityManifest, LeanCapabilityPreflight, LeanLoaderDiagnosticCode, check_imported_symbols,
658        check_staleness, inspect_artifact,
659    };
660    use crate::{LeanBuiltCapability, LeanCapability, LeanRuntime};
661    use std::collections::HashSet;
662    use std::fs;
663    use std::path::{Path, PathBuf};
664    use std::time::Duration;
665
666    #[test]
667    fn missing_manifest_reports_stable_code() {
668        let path = temp_dir("missing_manifest").join("missing.json");
669        let report = LeanCapabilityPreflight::new(LeanBuiltCapability::manifest_path(path)).check();
670
671        assert!(!report.is_ok());
672        assert_eq!(
673            report.first_error().map(crate::LeanLoaderCheck::code),
674            Some(LeanLoaderDiagnosticCode::MissingManifest)
675        );
676    }
677
678    #[test]
679    fn malformed_manifest_reports_stable_code() {
680        let dir = temp_dir("malformed_manifest");
681        let manifest = dir.join("capability.json");
682        fs::write(&manifest, "{").expect("write malformed manifest");
683
684        let report = LeanCapabilityPreflight::new(LeanBuiltCapability::manifest_path(&manifest)).check();
685
686        assert_eq!(
687            report.first_error().map(crate::LeanLoaderCheck::code),
688            Some(LeanLoaderDiagnosticCode::MalformedManifest)
689        );
690        assert_eq!(report.manifest_path(), Some(manifest.as_path()));
691    }
692
693    #[test]
694    fn unsupported_manifest_schema_reports_stable_code() {
695        let dir = temp_dir("unsupported_manifest_schema");
696        let manifest = dir.join("capability.json");
697        fs::write(
698            &manifest,
699            r#"{
700  "schema_version": 999,
701  "target_name": "Cap",
702  "package": "pkg",
703  "module": "Cap",
704  "primary_dylib": "/tmp/libcap.so"
705}"#,
706        )
707        .expect("write unsupported manifest schema");
708
709        let report = LeanCapabilityPreflight::new(LeanBuiltCapability::manifest_path(manifest)).check();
710
711        assert_eq!(
712            report.first_error().map(crate::LeanLoaderCheck::code),
713            Some(LeanLoaderDiagnosticCode::UnsupportedManifestSchema)
714        );
715    }
716
717    #[test]
718    fn missing_primary_dylib_reports_stable_code() {
719        let dir = temp_dir("missing_primary_dylib");
720        let missing = dir.join("missing-capability.dylib");
721        let manifest = write_manifest(&dir, &missing, "", "");
722
723        let report = LeanCapabilityPreflight::new(LeanBuiltCapability::manifest_path(manifest)).check();
724
725        assert!(contains_code(&report, LeanLoaderDiagnosticCode::MissingPrimaryDylib));
726    }
727
728    #[test]
729    fn missing_dependency_reports_stable_code() {
730        let dir = temp_dir("missing_dependency");
731        let missing = dir.join("missing-dependency.dylib");
732        let dependency = format!(
733            r#""dependencies":[{{"dylib_path":"{}","export_symbols_for_dependents":true}}],"#,
734            json_path(&missing)
735        );
736        let manifest = write_manifest(&dir, current_exe(), &dependency, "");
737
738        let report = LeanCapabilityPreflight::new(LeanBuiltCapability::manifest_path(manifest)).check();
739
740        assert!(contains_code(
741            &report,
742            LeanLoaderDiagnosticCode::MissingTransitiveDependency
743        ));
744    }
745
746    #[test]
747    fn invalid_object_reports_unsupported_architecture() {
748        let dir = temp_dir("invalid_object");
749        let bad = dir.join("not-a-dylib.so");
750        fs::write(&bad, b"not an object").expect("write invalid object");
751
752        let err = inspect_artifact(&bad, super::ArtifactRole::Primary).expect_err("invalid object should fail");
753
754        assert_eq!(err.code(), LeanLoaderDiagnosticCode::UnsupportedArchitecture);
755    }
756
757    #[test]
758    fn unsupported_toolchain_fingerprint_reports_stable_code() {
759        let dir = temp_dir("unsupported_toolchain_fingerprint");
760        let manifest = dir.join("capability.json");
761        fs::write(
762            &manifest,
763            format!(
764                r#"{{
765  "schema_version": 1,
766  "target_name": "Cap",
767  "package": "pkg",
768  "module": "Cap",
769  "primary_dylib": "{}",
770  "toolchain_fingerprint": {{
771    "lean_version": "0.0.0",
772    "resolved_version": "0.0.0",
773    "header_sha256": "0000"
774  }}
775}}"#,
776                json_path(&current_exe())
777            ),
778        )
779        .expect("write unsupported fingerprint manifest");
780
781        let report = LeanCapabilityPreflight::new(LeanBuiltCapability::manifest_path(manifest)).check();
782
783        assert!(contains_code(
784            &report,
785            LeanLoaderDiagnosticCode::UnsupportedToolchainFingerprint
786        ));
787    }
788
789    #[test]
790    fn stale_manifest_reports_stable_code() {
791        let dir = temp_dir("stale_manifest");
792        let primary = dir.join("libcap.so");
793        fs::write(&primary, b"old").expect("write old primary");
794        let manifest = write_manifest(&dir, &primary, "", "");
795        std::thread::sleep(Duration::from_millis(20));
796        fs::write(&primary, b"new").expect("write newer primary");
797        let parsed = CapabilityManifest::read(&manifest).expect("manifest parses");
798        let mut checks = Vec::new();
799
800        check_staleness(&manifest, &parsed, &mut checks);
801
802        assert!(
803            checks
804                .iter()
805                .any(|check| check.code() == LeanLoaderDiagnosticCode::StaleManifest)
806        );
807    }
808
809    #[test]
810    fn missing_initializer_reports_stable_code() {
811        let dir = temp_dir("missing_initializer");
812        let manifest = write_manifest(&dir, current_exe(), "", "");
813
814        let report = LeanCapabilityPreflight::new(LeanBuiltCapability::manifest_path(manifest)).check();
815
816        assert!(contains_code(&report, LeanLoaderDiagnosticCode::MissingInitializer));
817    }
818
819    #[test]
820    fn missing_imported_symbol_reports_stable_code() {
821        let primary = ArtifactInfo {
822            defined_symbols: HashSet::new(),
823            undefined_symbols: HashSet::from(["LeanRsInterop_missing".to_owned()]),
824        };
825        let manifest = CapabilityManifest {
826            primary_dylib: PathBuf::from("/tmp/libcap.so"),
827            package: "pkg".to_owned(),
828            module: "Cap".to_owned(),
829            dependencies: Vec::new(),
830            lean_version: None,
831            resolved_lean_version: None,
832            lean_header_sha256: None,
833        };
834        let mut checks = Vec::new();
835
836        check_imported_symbols(&manifest, &primary, &HashSet::new(), &mut checks);
837
838        assert!(
839            checks
840                .iter()
841                .any(|check| check.code() == LeanLoaderDiagnosticCode::MissingImportedSymbol)
842        );
843    }
844
845    #[test]
846    fn open_failure_uses_preflight_code_in_error_message() {
847        let dir = temp_dir("open_failure_preflight_code");
848        let missing = dir.join("missing-capability.dylib");
849        let manifest = write_manifest(&dir, &missing, "", "");
850        let runtime = LeanRuntime::init().expect("runtime init");
851
852        let Err(err) = LeanCapability::from_build_manifest(runtime, LeanBuiltCapability::manifest_path(manifest))
853        else {
854            panic!("missing primary should fail before open");
855        };
856
857        assert_eq!(err.code(), crate::LeanDiagnosticCode::ModuleInit);
858        assert!(
859            err.to_string()
860                .contains(LeanLoaderDiagnosticCode::MissingPrimaryDylib.as_str())
861        );
862    }
863
864    fn contains_code(report: &crate::LeanLoaderReport, code: LeanLoaderDiagnosticCode) -> bool {
865        report.checks().iter().any(|check| check.code() == code)
866    }
867
868    fn temp_dir(name: &str) -> PathBuf {
869        let dir = std::env::temp_dir().join(format!("lean-rs-preflight-{}-{name}", std::process::id()));
870        drop(fs::remove_dir_all(&dir));
871        fs::create_dir_all(&dir).expect("create preflight test dir");
872        dir
873    }
874
875    fn current_exe() -> PathBuf {
876        std::env::current_exe().expect("current test executable path")
877    }
878
879    fn write_manifest(dir: &Path, primary: impl AsRef<Path>, dependencies: &str, extra: &str) -> PathBuf {
880        let manifest = dir.join("capability.json");
881        let contents = format!(
882            r#"{{
883  {extra}
884  "schema_version": 1,
885  "target_name": "Cap",
886  "package": "pkg",
887  "module": "Cap",
888  "primary_dylib": "{}",
889  {dependencies}
890  "toolchain_fingerprint": {{
891    "lean_version": "{}",
892    "resolved_version": "{}",
893    "header_sha256": "{}"
894  }}
895}}"#,
896            json_path(primary.as_ref()),
897            lean_rs_sys::LEAN_VERSION,
898            lean_rs_sys::LEAN_RESOLVED_VERSION,
899            lean_rs_sys::LEAN_HEADER_DIGEST,
900        );
901        fs::write(&manifest, contents).expect("write manifest");
902        manifest
903    }
904
905    fn json_path(path: &Path) -> String {
906        path.display().to_string().replace('\\', "\\\\")
907    }
908}
lean_rs/module/preflight.rs

lean_rs/module/
preflight.rs
