Crate aver_cert 

Compiler-independent artifact certification for Aver WebAssembly.

This crate owns the byte-derived certificate engine, the public certificate format, and the exact Lean soundness wall. It deliberately has no dependency on the Aver compiler, language runtime, or memory runtime.

Modules

format

Stable, compiler-independent certificate format declarations.

wall

Checker-owned Lean soundness wall.

Enums

CheckVerdict

Developer preflight result. A green value means the checker-owned witness elaborated successfully while trusting the local Lake .olean graph. It is deliberately distinct from Verdict: only verify performs the final fresh-environment replay required for certification.

Explanation

Verdict

Constants

ARTIFACT_DECODE_LINE

Emitted on a green verdict. All trust-bearing byte facts and claim metadata are checked by the embedded Lean wall; Rust performs no parallel verdict reconstruction.

Functions

check

Fast developer/CI preflight which trusts locally built or explicitly cached .olean imports. Rust validation, lake build, and fresh elaboration of the checker-owned witness still run; only the final leanchecker --fresh whole-closure replay is omitted.

explain

verify