Module wall 

Checker-owned Lean soundness wall.

These sources are artifact-independent and embedded in the verifier. A certificate names the exact set through current_id; it never chooses a path, URL, or ambient installation from which the verifier loads code.

Re-exports

pub use crate::format::CURRENT_WALL_ID as CURRENT_ID;

pub use crate::format::FORMAT_VERSION;

Structs

Source

Wall

Constants

CERT_ACCEPTANCE_SOUNDNESS

CERT_ACCEPTANCE_SOUNDNESS_CORE

CERT_ACCEPTED_ARTIFACT

CERT_ACCEPTED_ARTIFACT_CORE

CERT_CLAIM_AXES

CERT_COMPOSITION_SOUNDNESS

CERT_CONSTRUCT_VERBATIM_SOUNDNESS

CERT_DECODE

CERT_DISCHARGE_COMPOSITION

CERT_DISCHARGE_CONSTRUCT

CERT_DISCHARGE_EXPR_FRAGMENT

CERT_DISCHARGE_FIELD_PROJECTION

CERT_DISCHARGE_INT_DISPATCH

CERT_DISCHARGE_RECURSION

CERT_DISCHARGE_STRING

CERT_DISCHARGE_VERBATIM

CERT_EXPR_FRAGMENT_ACCEPTED

CERT_EXPR_FRAGMENT_SEMANTICS

CERT_EXPR_FRAGMENT_SOUNDNESS

CERT_FIELD_PROJECTION_SOUNDNESS

CERT_INTERPRETER_SEQUENCING

CERT_INT_DISPATCH_SOUNDNESS

CERT_MUTUAL_RECURSION_SOUNDNESS

CERT_PLAN_BYTES

CERT_PLAN_CHECK

CERT_PLAN_LOWER

CERT_PRELUDE

CERT_RECURSION_SOUNDNESS

CERT_SCHEMA

CERT_SCHEMA_CORE

CERT_STANDARD_FACE

CERT_STRING_SOUNDNESS

CERT_WASM_SLICE

LEAN_TOOLCHAIN

PRISTINE_ROOTS

Roots whose complete import graph is artifact-independent and can therefore be cached before a certificate is seen.

SOURCES

Exact checker-owned source set. Ordering is not part of the identity: [compute_id] sorts by filename before hashing.

Statics

CURRENT

Functions

current_id

Identity of the one wall embedded in this pre-public verifier.

render_artifact_bytes

Checker-authored Lean module containing the exact artifact bytes. A certificate package never supplies this module; production verification and direct-Lake test harnesses materialize it from the .wasm under test.

resolve

Resolve only checker-embedded, byte-exact walls. There is intentionally no filesystem, environment, or network fallback.