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 std::collections::HashSet;
11
12use crate::loader::{
13    LeanExportAbiRepr, LeanExportArgAbi, LeanExportOwnership, LeanExportResultConvention, LeanExportReturnAbi,
14    LeanExportSignature, LeanExportSymbolKind, LeanLibraryDependency, LeanLoaderCheck, LeanLoaderDiagnosticCode,
15    LeanLoaderReport,
16};
17
18/// Parsed Lean capability manifest.
19///
20/// The shape downstream `build.rs` emits through
21/// `lean-toolchain::CargoLeanCapability`. The parser performs only schema-shape
22/// validation; semantic checks live in [`check_static`] and the runtime
23/// preflight in `lean-rs`.
24#[derive(Clone, Debug, Eq, PartialEq)]
25pub struct CapabilityManifest {
26    /// Path to the primary capability dylib.
27    pub primary_dylib: PathBuf,
28    /// Lake package name used by the root module initializer.
29    pub package: String,
30    /// Root Lean module name initialized by Rust.
31    pub module: String,
32    /// Dependency dylibs that must be opened before the primary.
33    pub dependencies: Vec<LeanLibraryDependency>,
34    /// Lean version recorded by the build script, if any.
35    pub lean_version: Option<String>,
36    /// Resolved Lean toolchain version, if any.
37    pub resolved_lean_version: Option<String>,
38    /// SHA-256 of the Lean header used to build the capability, if any.
39    pub lean_header_sha256: Option<String>,
40    /// Trusted ABI signatures for safe exported-symbol lookup.
41    pub exports: Vec<LeanExportSignature>,
42}
43
44impl CapabilityManifest {
45    /// Parse a Lean capability manifest from disk.
46    ///
47    /// # Errors
48    ///
49    /// Returns a `LeanLoaderCheck` describing the first parsing failure.
50    pub fn read(path: &Path) -> Result<Self, LeanLoaderCheck> {
51        let bytes = std::fs::read(path).map_err(|err| {
52            let code = if err.kind() == std::io::ErrorKind::NotFound {
53                LeanLoaderDiagnosticCode::MissingManifest
54            } else {
55                LeanLoaderDiagnosticCode::MalformedManifest
56            };
57            LeanLoaderCheck::error(
58                code,
59                path.display().to_string(),
60                format!("failed to read Lean capability manifest '{}': {err}", path.display()),
61                "rebuild the Lean capability through CargoLeanCapability and ensure the manifest file is packaged",
62            )
63        })?;
64        let value: serde_json::Value = serde_json::from_slice(&bytes).map_err(|err| {
65            LeanLoaderCheck::error(
66                LeanLoaderDiagnosticCode::MalformedManifest,
67                path.display().to_string(),
68                format!("Lean capability manifest '{}' is not valid JSON: {err}", path.display()),
69                "rebuild the Lean capability through CargoLeanCapability",
70            )
71        })?;
72        let schema_version = required_u64(&value, "schema_version", path)?;
73        if schema_version != u64::from(crate::CAPABILITY_MANIFEST_SCHEMA_VERSION) {
74            return Err(LeanLoaderCheck::error(
75                LeanLoaderDiagnosticCode::UnsupportedManifestSchema,
76                path.display().to_string(),
77                format!(
78                    "unsupported Lean capability manifest schema {schema_version}; supported schema is {}",
79                    crate::CAPABILITY_MANIFEST_SCHEMA_VERSION
80                ),
81                "rebuild the Lean capability with the same lean-rs version as the runtime crate",
82            ));
83        }
84        let primary_dylib = PathBuf::from(required_string(&value, "primary_dylib", path)?);
85        let package = required_string(&value, "package", path)?;
86        let module = required_string(&value, "module", path)?;
87        let dependencies = dependencies_from_manifest(&value, path)?;
88        let exports = exports_from_manifest(&value, path)?;
89        let fingerprint = value.get("toolchain_fingerprint").unwrap_or(&serde_json::Value::Null);
90        let lean_version =
91            optional_string(fingerprint, "lean_version").or_else(|| optional_string(&value, "lean_version"));
92        let resolved_lean_version = optional_string(fingerprint, "resolved_version")
93            .or_else(|| optional_string(&value, "resolved_lean_version"));
94        let lean_header_sha256 =
95            optional_string(fingerprint, "header_sha256").or_else(|| optional_string(&value, "lean_header_sha256"));
96        Ok(Self {
97            primary_dylib,
98            package,
99            module,
100            dependencies,
101            lean_version,
102            resolved_lean_version,
103            lean_header_sha256,
104            exports,
105        })
106    }
107}
108
109/// Static manifest validation: file-exists, JSON parse, schema check,
110/// toolchain fingerprint match, and primary-dylib staleness.
111///
112/// This is the cheap, link-free preflight the worker parent runs before
113/// spawning a child. The runtime preflight in `lean-rs` also inspects
114/// the dylib's symbol table.
115#[must_use]
116pub fn check_static(manifest_path: &Path) -> LeanLoaderReport {
117    let manifest = match CapabilityManifest::read(manifest_path) {
118        Ok(manifest) => manifest,
119        Err(check) => return LeanLoaderReport::new(Some(manifest_path.to_path_buf()), vec![check]),
120    };
121
122    let mut checks = Vec::new();
123    check_fingerprint(&manifest, &mut checks);
124    check_staleness(manifest_path, &manifest, &mut checks);
125    check_dependency_paths(&manifest, &mut checks);
126    check_primary_dylib_present(&manifest, &mut checks);
127
128    LeanLoaderReport::new(Some(manifest_path.to_path_buf()), checks)
129}
130
131/// Validate the toolchain fingerprint against the current `lean-rs-sys` build.
132pub fn check_fingerprint(manifest: &CapabilityManifest, checks: &mut Vec<LeanLoaderCheck>) {
133    if let Some(version) = manifest.lean_version.as_deref()
134        && lean_rs_sys::supported_for(version).is_none()
135    {
136        checks.push(LeanLoaderCheck::error(
137            LeanLoaderDiagnosticCode::UnsupportedToolchainFingerprint,
138            version,
139            format!("manifest was built with unsupported Lean toolchain {version}"),
140            "rebuild the Lean capability with a Lean version supported by this lean-rs release",
141        ));
142        return;
143    }
144    if let Some(digest) = manifest.lean_header_sha256.as_deref()
145        && digest != lean_rs_sys::LEAN_HEADER_DIGEST
146    {
147        checks.push(LeanLoaderCheck::error(
148            LeanLoaderDiagnosticCode::UnsupportedToolchainFingerprint,
149            digest,
150            format!(
151                "manifest Lean header digest {digest} does not match this process digest {}",
152                lean_rs_sys::LEAN_HEADER_DIGEST
153            ),
154            "rebuild the Lean capability with the same Lean toolchain used by this Rust binary",
155        ));
156        return;
157    }
158    if let Some(resolved) = manifest.resolved_lean_version.as_deref()
159        && resolved != lean_rs_sys::LEAN_RESOLVED_VERSION
160    {
161        checks.push(LeanLoaderCheck::error(
162            LeanLoaderDiagnosticCode::UnsupportedToolchainFingerprint,
163            resolved,
164            format!(
165                "manifest resolved Lean version {resolved} does not match this process resolved version {}",
166                lean_rs_sys::LEAN_RESOLVED_VERSION
167            ),
168            "rebuild the Lean capability with the same Lean toolchain used by this Rust binary",
169        ));
170    }
171}
172
173/// Warn if the manifest is older than its primary dylib.
174pub fn check_staleness(manifest_path: &Path, manifest: &CapabilityManifest, checks: &mut Vec<LeanLoaderCheck>) {
175    let Ok(manifest_modified) = std::fs::metadata(manifest_path).and_then(|metadata| metadata.modified()) else {
176        return;
177    };
178    let Ok(primary_modified) = std::fs::metadata(&manifest.primary_dylib).and_then(|metadata| metadata.modified())
179    else {
180        return;
181    };
182    if primary_modified > manifest_modified {
183        checks.push(LeanLoaderCheck::error(
184            LeanLoaderDiagnosticCode::StaleManifest,
185            manifest_path.display().to_string(),
186            format!(
187                "manifest '{}' is older than primary dylib '{}'",
188                manifest_path.display(),
189                manifest.primary_dylib.display()
190            ),
191            "rebuild the Lean capability through CargoLeanCapability so the manifest matches the dylib",
192        ));
193    }
194}
195
196fn check_dependency_paths(manifest: &CapabilityManifest, checks: &mut Vec<LeanLoaderCheck>) {
197    for dependency in &manifest.dependencies {
198        if !dependency.path_ref().is_file() {
199            checks.push(LeanLoaderCheck::error(
200                LeanLoaderDiagnosticCode::MissingTransitiveDependency,
201                dependency.path_ref().display().to_string(),
202                format!(
203                    "Lean dependency dylib '{}' named by the manifest is missing",
204                    dependency.path_ref().display()
205                ),
206                "rebuild the Lean capability through CargoLeanCapability and package every manifest dependency",
207            ));
208        }
209    }
210}
211
212fn check_primary_dylib_present(manifest: &CapabilityManifest, checks: &mut Vec<LeanLoaderCheck>) {
213    if !manifest.primary_dylib.is_file() {
214        checks.push(LeanLoaderCheck::error(
215            LeanLoaderDiagnosticCode::MissingPrimaryDylib,
216            manifest.primary_dylib.display().to_string(),
217            format!(
218                "primary Lean capability dylib '{}' named by the manifest is missing",
219                manifest.primary_dylib.display()
220            ),
221            "rebuild the Lean capability through CargoLeanCapability and package the primary dylib",
222        ));
223    }
224}
225
226fn dependencies_from_manifest(
227    value: &serde_json::Value,
228    path: &Path,
229) -> Result<Vec<LeanLibraryDependency>, LeanLoaderCheck> {
230    let Some(raw_dependencies) = value.get("dependencies") else {
231        return Ok(Vec::new());
232    };
233    let dependencies = raw_dependencies.as_array().ok_or_else(|| {
234        LeanLoaderCheck::error(
235            LeanLoaderDiagnosticCode::MalformedManifest,
236            path.display().to_string(),
237            format!(
238                "Lean capability manifest '{}' field `dependencies` must be an array",
239                path.display()
240            ),
241            "rebuild the Lean capability through CargoLeanCapability",
242        )
243    })?;
244    let mut out = Vec::with_capacity(dependencies.len());
245    for dependency in dependencies {
246        let dylib = required_string(dependency, "dylib_path", path)?;
247        let mut descriptor = LeanLibraryDependency::path(dylib);
248        if dependency
249            .get("export_symbols_for_dependents")
250            .and_then(serde_json::Value::as_bool)
251            .unwrap_or(false)
252        {
253            descriptor = descriptor.export_symbols_for_dependents();
254        }
255        if let Some(initializer) = dependency.get("initializer") {
256            let package = required_string(initializer, "package", path)?;
257            let module = required_string(initializer, "module", path)?;
258            descriptor = descriptor.initializer(package, module);
259        }
260        out.push(descriptor);
261    }
262    Ok(out)
263}
264
265fn exports_from_manifest(value: &serde_json::Value, path: &Path) -> Result<Vec<LeanExportSignature>, LeanLoaderCheck> {
266    let raw_exports = value.get("exports").ok_or_else(|| {
267        LeanLoaderCheck::error(
268            LeanLoaderDiagnosticCode::MalformedManifest,
269            path.display().to_string(),
270            format!(
271                "Lean capability manifest '{}' is missing required array field `exports`",
272                path.display()
273            ),
274            "rebuild the Lean capability through CargoLeanCapability",
275        )
276    })?;
277    let exports = raw_exports.as_array().ok_or_else(|| {
278        LeanLoaderCheck::error(
279            LeanLoaderDiagnosticCode::MalformedManifest,
280            path.display().to_string(),
281            format!(
282                "Lean capability manifest '{}' field `exports` must be an array",
283                path.display()
284            ),
285            "rebuild the Lean capability through CargoLeanCapability",
286        )
287    })?;
288    let mut seen = HashSet::new();
289    let mut out = Vec::with_capacity(exports.len());
290    for export in exports {
291        let symbol = required_string(export, "symbol", path)?;
292        if !seen.insert(symbol.clone()) {
293            return Err(LeanLoaderCheck::error(
294                LeanLoaderDiagnosticCode::MalformedManifest,
295                symbol,
296                "Lean capability manifest contains duplicate export signature metadata",
297                "emit at most one signature entry for each exported symbol",
298            ));
299        }
300        let kind = parse_export_kind(export, path)?;
301        let args = export_args_from_manifest(export, path)?;
302        let result = export_return_from_manifest(export, path)?;
303        if kind == LeanExportSymbolKind::Global && !args.is_empty() {
304            return Err(LeanLoaderCheck::error(
305                LeanLoaderDiagnosticCode::MalformedManifest,
306                symbol,
307                "Lean capability manifest describes a global export with function arguments",
308                "record globals with an empty `args` array",
309            ));
310        }
311        if kind == LeanExportSymbolKind::Global && result.convention() == LeanExportResultConvention::IoResult {
312            return Err(LeanLoaderCheck::error(
313                LeanLoaderDiagnosticCode::MalformedManifest,
314                symbol,
315                "Lean capability manifest describes a global export as an IO result",
316                "record globals with a pure return convention",
317            ));
318        }
319        out.push(match kind {
320            LeanExportSymbolKind::Function => LeanExportSignature::function(symbol, args, result),
321            LeanExportSymbolKind::Global => LeanExportSignature::global(symbol, result),
322        });
323    }
324    Ok(out)
325}
326
327fn parse_export_kind(value: &serde_json::Value, path: &Path) -> Result<LeanExportSymbolKind, LeanLoaderCheck> {
328    let kind = required_string(value, "kind", path)?;
329    LeanExportSymbolKind::from_str(&kind).ok_or_else(|| {
330        LeanLoaderCheck::error(
331            LeanLoaderDiagnosticCode::MalformedManifest,
332            kind,
333            "Lean capability manifest export `kind` must be `function` or `global`",
334            "rebuild the Lean capability through CargoLeanCapability",
335        )
336    })
337}
338
339fn export_args_from_manifest(value: &serde_json::Value, path: &Path) -> Result<Vec<LeanExportArgAbi>, LeanLoaderCheck> {
340    let raw_args = value.get("args").ok_or_else(|| {
341        LeanLoaderCheck::error(
342            LeanLoaderDiagnosticCode::MalformedManifest,
343            path.display().to_string(),
344            "Lean capability manifest export is missing required array field `args`",
345            "rebuild the Lean capability through CargoLeanCapability",
346        )
347    })?;
348    let args = raw_args.as_array().ok_or_else(|| {
349        LeanLoaderCheck::error(
350            LeanLoaderDiagnosticCode::MalformedManifest,
351            path.display().to_string(),
352            "Lean capability manifest export field `args` must be an array",
353            "rebuild the Lean capability through CargoLeanCapability",
354        )
355    })?;
356    args.iter().map(|arg| export_arg_from_manifest(arg, path)).collect()
357}
358
359fn export_arg_from_manifest(value: &serde_json::Value, path: &Path) -> Result<LeanExportArgAbi, LeanLoaderCheck> {
360    let repr = parse_export_repr(value, path)?;
361    let ownership = parse_export_ownership(value, path)?;
362    validate_ownership(repr, ownership, path)?;
363    Ok(LeanExportArgAbi::new(repr, ownership))
364}
365
366fn export_return_from_manifest(value: &serde_json::Value, path: &Path) -> Result<LeanExportReturnAbi, LeanLoaderCheck> {
367    let raw_return = value.get("return").ok_or_else(|| {
368        LeanLoaderCheck::error(
369            LeanLoaderDiagnosticCode::MalformedManifest,
370            path.display().to_string(),
371            "Lean capability manifest export is missing required object field `return`",
372            "rebuild the Lean capability through CargoLeanCapability",
373        )
374    })?;
375    let repr = parse_export_repr(raw_return, path)?;
376    let ownership = parse_export_ownership(raw_return, path)?;
377    validate_ownership(repr, ownership, path)?;
378    let convention = parse_export_result_convention(raw_return, path)?;
379    if convention == LeanExportResultConvention::IoResult
380        && (repr != LeanExportAbiRepr::LeanObject || ownership != LeanExportOwnership::Owned)
381    {
382        return Err(LeanLoaderCheck::error(
383            LeanLoaderDiagnosticCode::MalformedManifest,
384            path.display().to_string(),
385            "Lean capability manifest IO result must use owned `lean_object` return ABI",
386            "record IO exports with `repr: lean_object`, `ownership: owned`, and `convention: io_result`",
387        ));
388    }
389    Ok(LeanExportReturnAbi::new(repr, ownership, convention))
390}
391
392fn parse_export_repr(value: &serde_json::Value, path: &Path) -> Result<LeanExportAbiRepr, LeanLoaderCheck> {
393    let repr = required_string(value, "repr", path)?;
394    LeanExportAbiRepr::from_str(&repr).ok_or_else(|| {
395        LeanLoaderCheck::error(
396            LeanLoaderDiagnosticCode::MalformedManifest,
397            repr,
398            "Lean capability manifest ABI `repr` is not supported",
399            "use a supported Lean export ABI representation",
400        )
401    })
402}
403
404fn parse_export_ownership(value: &serde_json::Value, path: &Path) -> Result<LeanExportOwnership, LeanLoaderCheck> {
405    let ownership = required_string(value, "ownership", path)?;
406    LeanExportOwnership::from_str(&ownership).ok_or_else(|| {
407        LeanLoaderCheck::error(
408            LeanLoaderDiagnosticCode::MalformedManifest,
409            ownership,
410            "Lean capability manifest ABI `ownership` must be `none` or `owned`",
411            "rebuild the Lean capability through CargoLeanCapability",
412        )
413    })
414}
415
416fn parse_export_result_convention(
417    value: &serde_json::Value,
418    path: &Path,
419) -> Result<LeanExportResultConvention, LeanLoaderCheck> {
420    let convention = required_string(value, "convention", path)?;
421    LeanExportResultConvention::from_str(&convention).ok_or_else(|| {
422        LeanLoaderCheck::error(
423            LeanLoaderDiagnosticCode::MalformedManifest,
424            convention,
425            "Lean capability manifest return `convention` must be `pure` or `io_result`",
426            "rebuild the Lean capability through CargoLeanCapability",
427        )
428    })
429}
430
431fn validate_ownership(
432    repr: LeanExportAbiRepr,
433    ownership: LeanExportOwnership,
434    path: &Path,
435) -> Result<(), LeanLoaderCheck> {
436    let expected = if repr == LeanExportAbiRepr::LeanObject {
437        LeanExportOwnership::Owned
438    } else {
439        LeanExportOwnership::None
440    };
441    if ownership == expected {
442        return Ok(());
443    }
444    Err(LeanLoaderCheck::error(
445        LeanLoaderDiagnosticCode::MalformedManifest,
446        path.display().to_string(),
447        format!(
448            "Lean capability manifest ABI ownership `{}` does not match representation `{}`",
449            ownership.as_str(),
450            repr.as_str()
451        ),
452        "use `owned` for `lean_object` slots and `none` for scalar slots",
453    ))
454}
455
456fn required_string(value: &serde_json::Value, field: &str, path: &Path) -> Result<String, LeanLoaderCheck> {
457    value
458        .get(field)
459        .and_then(serde_json::Value::as_str)
460        .filter(|value| !value.is_empty())
461        .map(str::to_owned)
462        .ok_or_else(|| {
463            LeanLoaderCheck::error(
464                LeanLoaderDiagnosticCode::MalformedManifest,
465                path.display().to_string(),
466                format!(
467                    "Lean capability manifest '{}' is missing non-empty string field `{field}`",
468                    path.display()
469                ),
470                "rebuild the Lean capability through CargoLeanCapability",
471            )
472        })
473}
474
475fn optional_string(value: &serde_json::Value, field: &str) -> Option<String> {
476    value
477        .get(field)
478        .and_then(serde_json::Value::as_str)
479        .filter(|value| !value.is_empty())
480        .map(str::to_owned)
481}
482
483fn required_u64(value: &serde_json::Value, field: &str, path: &Path) -> Result<u64, LeanLoaderCheck> {
484    value.get(field).and_then(serde_json::Value::as_u64).ok_or_else(|| {
485        LeanLoaderCheck::error(
486            LeanLoaderDiagnosticCode::MalformedManifest,
487            path.display().to_string(),
488            format!(
489                "Lean capability manifest '{}' is missing unsigned integer field `{field}`",
490                path.display()
491            ),
492            "rebuild the Lean capability through CargoLeanCapability",
493        )
494    })
495}
496
497#[cfg(test)]
498#[allow(clippy::expect_used, clippy::panic)]
499mod tests {
500    use super::CapabilityManifest;
501    use crate::{
502        CAPABILITY_MANIFEST_SCHEMA_VERSION, LeanExportAbiRepr, LeanExportArgAbi, LeanExportOwnership,
503        LeanExportResultConvention, LeanExportReturnAbi, LeanExportSignature, LeanExportSymbolKind,
504        LeanLoaderDiagnosticCode,
505    };
506    use std::path::{Path, PathBuf};
507
508    #[test]
509    fn manifest_round_trips_export_signatures() {
510        let path = temp_manifest_path("manifest_round_trips_export_signatures");
511        let signature = LeanExportSignature::function(
512            "cap_u8_identity",
513            vec![LeanExportArgAbi::new(LeanExportAbiRepr::U8, LeanExportOwnership::None)],
514            LeanExportReturnAbi::new(
515                LeanExportAbiRepr::U8,
516                LeanExportOwnership::None,
517                LeanExportResultConvention::Pure,
518            ),
519        );
520        write_manifest(&path, CAPABILITY_MANIFEST_SCHEMA_VERSION, &[signature.to_json()]);
521
522        let manifest = CapabilityManifest::read(&path).expect("manifest parses");
523
524        assert_eq!(manifest.exports, vec![signature]);
525        let Some(parsed) = manifest.exports.first() else {
526            panic!("expected export signature");
527        };
528        assert_eq!(parsed.symbol(), "cap_u8_identity");
529        assert_eq!(parsed.kind(), LeanExportSymbolKind::Function);
530        assert_eq!(parsed.args().len(), 1);
531    }
532
533    #[test]
534    fn old_manifest_schema_is_rejected() {
535        let path = temp_manifest_path("old_manifest_schema_is_rejected");
536        write_manifest(&path, 1, &[]);
537
538        let err = CapabilityManifest::read(&path).expect_err("schema v1 is obsolete");
539
540        assert_eq!(err.code(), LeanLoaderDiagnosticCode::UnsupportedManifestSchema);
541    }
542
543    fn temp_manifest_path(name: &str) -> PathBuf {
544        let dir = std::env::temp_dir().join(format!("lean-toolchain-manifest-{}-{name}", std::process::id()));
545        drop(std::fs::remove_dir_all(&dir));
546        std::fs::create_dir_all(&dir).expect("create manifest test dir");
547        dir.join("capability.json")
548    }
549
550    fn write_manifest(path: &Path, schema_version: u32, exports: &[serde_json::Value]) {
551        let manifest = serde_json::json!({
552            "schema_version": schema_version,
553            "target_name": "Cap",
554            "package": "pkg",
555            "module": "Cap",
556            "primary_dylib": "/tmp/libcap.so",
557            "dependencies": [],
558            "exports": exports,
559        });
560        std::fs::write(path, serde_json::to_vec_pretty(&manifest).expect("encode manifest")).expect("write manifest");
561    }
562}
lean_toolchain/manifest_validation.rs

lean_toolchain/
manifest_validation.rs
