Module format 

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

Manifest schema accepted by the standalone verifier. Version 2 made the subject’s hostRoleTable optional: modules without the Int box helper declare null, pinned against a byte-derived proof of the helper’s absence, while modules with the helper pin the exact decoded table. A module whose role scan the decoder cannot complete matches no manifest value. The declared arith helper indices (carrier, limb, and the decompose/normalize/strip/umagCmp sub-routines) are proof-term data in the generated Lean certificate, not public JSON, so the acceptance pin can confirm each declared add/sub/mul helper body byte-for-byte without moving the public schema.

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.