lean_toolchain/
manifest_validation.rs

1//! Static, link-free validation of Lean capability manifests.
2//!
3//! Lives in `lean-toolchain` so the worker parent crate can fast-fail bad
4//! manifests on the client side without re-linking `libleanshared` through
5//! `lean-rs`. The runtime preflight in `lean-rs` reuses the same parser and
6//! diagnostic shapes and layers symbol-table inspection on top.
7
8use std::path::{Path, PathBuf};
9
10use crate::loader::{LeanLibraryDependency, LeanLoaderCheck, LeanLoaderDiagnosticCode, LeanLoaderReport};
11
12/// Parsed Lean capability manifest.
13///
14/// The shape downstream `build.rs` emits through
15/// `lean-toolchain::CargoLeanCapability`. The parser performs only schema-shape
16/// validation; semantic checks live in [`check_static`] and the runtime
17/// preflight in `lean-rs`.
18#[derive(Clone, Debug, Eq, PartialEq)]
19pub struct CapabilityManifest {
20    /// Path to the primary capability dylib.
21    pub primary_dylib: PathBuf,
22    /// Lake package name used by the root module initializer.
23    pub package: String,
24    /// Root Lean module name initialized by Rust.
25    pub module: String,
26    /// Dependency dylibs that must be opened before the primary.
27    pub dependencies: Vec<LeanLibraryDependency>,
28    /// Lean version recorded by the build script, if any.
29    pub lean_version: Option<String>,
30    /// Resolved Lean toolchain version, if any.
31    pub resolved_lean_version: Option<String>,
32    /// SHA-256 of the Lean header used to build the capability, if any.
33    pub lean_header_sha256: Option<String>,
34}
35
36impl CapabilityManifest {
37    /// Parse a Lean capability manifest from disk.
38    ///
39    /// # Errors
40    ///
41    /// Returns a `LeanLoaderCheck` describing the first parsing failure.
42    pub fn read(path: &Path) -> Result<Self, LeanLoaderCheck> {
43        let bytes = std::fs::read(path).map_err(|err| {
44            let code = if err.kind() == std::io::ErrorKind::NotFound {
45                LeanLoaderDiagnosticCode::MissingManifest
46            } else {
47                LeanLoaderDiagnosticCode::MalformedManifest
48            };
49            LeanLoaderCheck::error(
50                code,
51                path.display().to_string(),
52                format!("failed to read Lean capability manifest '{}': {err}", path.display()),
53                "rebuild the Lean capability through CargoLeanCapability and ensure the manifest file is packaged",
54            )
55        })?;
56        let value: serde_json::Value = serde_json::from_slice(&bytes).map_err(|err| {
57            LeanLoaderCheck::error(
58                LeanLoaderDiagnosticCode::MalformedManifest,
59                path.display().to_string(),
60                format!("Lean capability manifest '{}' is not valid JSON: {err}", path.display()),
61                "rebuild the Lean capability through CargoLeanCapability",
62            )
63        })?;
64        let schema_version = required_u64(&value, "schema_version", path)?;
65        if schema_version != u64::from(crate::CAPABILITY_MANIFEST_SCHEMA_VERSION) {
66            return Err(LeanLoaderCheck::error(
67                LeanLoaderDiagnosticCode::UnsupportedManifestSchema,
68                path.display().to_string(),
69                format!(
70                    "unsupported Lean capability manifest schema {schema_version}; supported schema is {}",
71                    crate::CAPABILITY_MANIFEST_SCHEMA_VERSION
72                ),
73                "rebuild the Lean capability with the same lean-rs version as the runtime crate",
74            ));
75        }
76        let primary_dylib = PathBuf::from(required_string(&value, "primary_dylib", path)?);
77        let package = required_string(&value, "package", path)?;
78        let module = required_string(&value, "module", path)?;
79        let dependencies = dependencies_from_manifest(&value, path)?;
80        let fingerprint = value.get("toolchain_fingerprint").unwrap_or(&serde_json::Value::Null);
81        let lean_version =
82            optional_string(fingerprint, "lean_version").or_else(|| optional_string(&value, "lean_version"));
83        let resolved_lean_version = optional_string(fingerprint, "resolved_version")
84            .or_else(|| optional_string(&value, "resolved_lean_version"));
85        let lean_header_sha256 =
86            optional_string(fingerprint, "header_sha256").or_else(|| optional_string(&value, "lean_header_sha256"));
87        Ok(Self {
88            primary_dylib,
89            package,
90            module,
91            dependencies,
92            lean_version,
93            resolved_lean_version,
94            lean_header_sha256,
95        })
96    }
97}
98
99/// Static manifest validation: file-exists, JSON parse, schema check,
100/// toolchain fingerprint match, and primary-dylib staleness.
101///
102/// This is the cheap, link-free preflight the worker parent runs before
103/// spawning a child. The runtime preflight in `lean-rs` additionally inspects
104/// the dylib's symbol table.
105#[must_use]
106pub fn check_static(manifest_path: &Path) -> LeanLoaderReport {
107    let manifest = match CapabilityManifest::read(manifest_path) {
108        Ok(manifest) => manifest,
109        Err(check) => return LeanLoaderReport::new(Some(manifest_path.to_path_buf()), vec![check]),
110    };
111
112    let mut checks = Vec::new();
113    check_fingerprint(&manifest, &mut checks);
114    check_staleness(manifest_path, &manifest, &mut checks);
115    check_dependency_paths(&manifest, &mut checks);
116    check_primary_dylib_present(&manifest, &mut checks);
117
118    LeanLoaderReport::new(Some(manifest_path.to_path_buf()), checks)
119}
120
121/// Validate the toolchain fingerprint against the current `lean-rs-sys` build.
122pub fn check_fingerprint(manifest: &CapabilityManifest, checks: &mut Vec<LeanLoaderCheck>) {
123    if let Some(version) = manifest.lean_version.as_deref()
124        && lean_rs_sys::supported_for(version).is_none()
125    {
126        checks.push(LeanLoaderCheck::error(
127            LeanLoaderDiagnosticCode::UnsupportedToolchainFingerprint,
128            version,
129            format!("manifest was built with unsupported Lean toolchain {version}"),
130            "rebuild the Lean capability with a Lean version supported by this lean-rs release",
131        ));
132        return;
133    }
134    if let Some(digest) = manifest.lean_header_sha256.as_deref()
135        && digest != lean_rs_sys::LEAN_HEADER_DIGEST
136    {
137        checks.push(LeanLoaderCheck::error(
138            LeanLoaderDiagnosticCode::UnsupportedToolchainFingerprint,
139            digest,
140            format!(
141                "manifest Lean header digest {digest} does not match this process digest {}",
142                lean_rs_sys::LEAN_HEADER_DIGEST
143            ),
144            "rebuild the Lean capability with the same Lean toolchain used by this Rust binary",
145        ));
146        return;
147    }
148    if let Some(resolved) = manifest.resolved_lean_version.as_deref()
149        && resolved != lean_rs_sys::LEAN_RESOLVED_VERSION
150    {
151        checks.push(LeanLoaderCheck::error(
152            LeanLoaderDiagnosticCode::UnsupportedToolchainFingerprint,
153            resolved,
154            format!(
155                "manifest resolved Lean version {resolved} does not match this process resolved version {}",
156                lean_rs_sys::LEAN_RESOLVED_VERSION
157            ),
158            "rebuild the Lean capability with the same Lean toolchain used by this Rust binary",
159        ));
160    }
161}
162
163/// Warn if the manifest is older than its primary dylib.
164pub fn check_staleness(manifest_path: &Path, manifest: &CapabilityManifest, checks: &mut Vec<LeanLoaderCheck>) {
165    let Ok(manifest_modified) = std::fs::metadata(manifest_path).and_then(|metadata| metadata.modified()) else {
166        return;
167    };
168    let Ok(primary_modified) = std::fs::metadata(&manifest.primary_dylib).and_then(|metadata| metadata.modified())
169    else {
170        return;
171    };
172    if primary_modified > manifest_modified {
173        checks.push(LeanLoaderCheck::error(
174            LeanLoaderDiagnosticCode::StaleManifest,
175            manifest_path.display().to_string(),
176            format!(
177                "manifest '{}' is older than primary dylib '{}'",
178                manifest_path.display(),
179                manifest.primary_dylib.display()
180            ),
181            "rebuild the Lean capability through CargoLeanCapability so the manifest matches the dylib",
182        ));
183    }
184}
185
186fn check_dependency_paths(manifest: &CapabilityManifest, checks: &mut Vec<LeanLoaderCheck>) {
187    for dependency in &manifest.dependencies {
188        if !dependency.path_ref().is_file() {
189            checks.push(LeanLoaderCheck::error(
190                LeanLoaderDiagnosticCode::MissingTransitiveDependency,
191                dependency.path_ref().display().to_string(),
192                format!(
193                    "Lean dependency dylib '{}' named by the manifest is missing",
194                    dependency.path_ref().display()
195                ),
196                "rebuild the Lean capability through CargoLeanCapability and package every manifest dependency",
197            ));
198        }
199    }
200}
201
202fn check_primary_dylib_present(manifest: &CapabilityManifest, checks: &mut Vec<LeanLoaderCheck>) {
203    if !manifest.primary_dylib.is_file() {
204        checks.push(LeanLoaderCheck::error(
205            LeanLoaderDiagnosticCode::MissingPrimaryDylib,
206            manifest.primary_dylib.display().to_string(),
207            format!(
208                "primary Lean capability dylib '{}' named by the manifest is missing",
209                manifest.primary_dylib.display()
210            ),
211            "rebuild the Lean capability through CargoLeanCapability and package the primary dylib",
212        ));
213    }
214}
215
216fn dependencies_from_manifest(
217    value: &serde_json::Value,
218    path: &Path,
219) -> Result<Vec<LeanLibraryDependency>, LeanLoaderCheck> {
220    let Some(raw_dependencies) = value.get("dependencies") else {
221        return Ok(Vec::new());
222    };
223    let dependencies = raw_dependencies.as_array().ok_or_else(|| {
224        LeanLoaderCheck::error(
225            LeanLoaderDiagnosticCode::MalformedManifest,
226            path.display().to_string(),
227            format!(
228                "Lean capability manifest '{}' field `dependencies` must be an array",
229                path.display()
230            ),
231            "rebuild the Lean capability through CargoLeanCapability",
232        )
233    })?;
234    let mut out = Vec::with_capacity(dependencies.len());
235    for dependency in dependencies {
236        let dylib = required_string(dependency, "dylib_path", path)?;
237        let mut descriptor = LeanLibraryDependency::path(dylib);
238        if dependency
239            .get("export_symbols_for_dependents")
240            .and_then(serde_json::Value::as_bool)
241            .unwrap_or(false)
242        {
243            descriptor = descriptor.export_symbols_for_dependents();
244        }
245        if let Some(initializer) = dependency.get("initializer") {
246            let package = required_string(initializer, "package", path)?;
247            let module = required_string(initializer, "module", path)?;
248            descriptor = descriptor.initializer(package, module);
249        }
250        out.push(descriptor);
251    }
252    Ok(out)
253}
254
255fn required_string(value: &serde_json::Value, field: &str, path: &Path) -> Result<String, LeanLoaderCheck> {
256    value
257        .get(field)
258        .and_then(serde_json::Value::as_str)
259        .filter(|value| !value.is_empty())
260        .map(str::to_owned)
261        .ok_or_else(|| {
262            LeanLoaderCheck::error(
263                LeanLoaderDiagnosticCode::MalformedManifest,
264                path.display().to_string(),
265                format!(
266                    "Lean capability manifest '{}' is missing non-empty string field `{field}`",
267                    path.display()
268                ),
269                "rebuild the Lean capability through CargoLeanCapability",
270            )
271        })
272}
273
274fn optional_string(value: &serde_json::Value, field: &str) -> Option<String> {
275    value
276        .get(field)
277        .and_then(serde_json::Value::as_str)
278        .filter(|value| !value.is_empty())
279        .map(str::to_owned)
280}
281
282fn required_u64(value: &serde_json::Value, field: &str, path: &Path) -> Result<u64, LeanLoaderCheck> {
283    value.get(field).and_then(serde_json::Value::as_u64).ok_or_else(|| {
284        LeanLoaderCheck::error(
285            LeanLoaderDiagnosticCode::MalformedManifest,
286            path.display().to_string(),
287            format!(
288                "Lean capability manifest '{}' is missing unsigned integer field `{field}`",
289                path.display()
290            ),
291            "rebuild the Lean capability through CargoLeanCapability",
292        )
293    })
294}
lean_toolchain/manifest_validation.rs

lean_toolchain/
manifest_validation.rs
