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

lean_rs/module/
preflight.rs
