Skip to main content

aver_cert/
lib.rs

1//! Compiler-independent artifact certification for Aver WebAssembly.
2//!
3//! This crate owns the byte-derived certificate engine, the public certificate
4//! format, and the exact Lean soundness wall. It deliberately has no dependency
5//! on the Aver compiler, language runtime, or memory runtime.
6
7#![forbid(unsafe_code)]
8
9pub mod format;
10#[cfg(any(feature = "engine", feature = "verify"))]
11pub mod wall;
12
13#[cfg(feature = "engine")]
14mod engine;
15#[cfg(feature = "engine")]
16pub use engine::*;
17
18#[cfg(feature = "verify")]
19mod cache;
20#[cfg(feature = "verify")]
21mod lean_process;
22#[cfg(feature = "verify")]
23mod prelude_cache;
24#[cfg(feature = "verify")]
25mod verifier;
26#[cfg(feature = "verify")]
27pub use verifier::{
28    ARTIFACT_DECODE_LINE, CheckVerdict, Explanation, Verdict, check, explain, verify,
29};