Expand description
Stable, compiler-independent certificate format declarations.
The producer imports this module from aver-cert; there is intentionally
no separate format crate. The verifier is the authority for this surface,
and the compiler depends on it in the non-trust-bearing direction.
Constantsยง
- ARTIFACT_
CERTIFICATE_ ROOT - Named theorem audited by the checker-owned witness.
- CERT_
SCHEMA_ VERSION - First public schema accepted by the standalone verifier.
- CURRENT_
WALL_ ID - Identity of the exact checker-owned Lean wall shipped by this release.
- FORMAT_
VERSION - Public certificate-package layout understood by this verifier.
- WASM_
GC_ CAPABILITIES - Complete host-import surface admitted by the wasm-gc certificate format.