certificate-format.md

Aver Artifact Certificate Format Specification

This document is the normative specification of the Aver artifact certificate format: the on-disk cert/ package emitted by aver compile --target wasm-gc --certify and the acceptance behavior required of a verifier that consumes it, together with the trust inventory (section 10) and the versioning and freeze policy (section 11). The intended audience is an independent reimplementor of the verifier. The reference implementation is the standalone aver-cert crate. This document separates what acceptance requires (enforced by the reference implementation and normative for any reimplementation) from what the producer emits (layout and naming conventions a verifier MUST NOT rely on); places where the reference implementation enforces less than a reader might expect are flagged inline as known gap. An appendix maps each section to the source files that define the behavior. This is the reference, the third tier of the certification documentation: certification.md is the user guide (what a certificate is and how to produce and verify one), and certification-architecture.md is the architecture document (how the verifier reaches its verdict and why the trust boundary sits where it does).

The key words MUST, MUST NOT, and MAY are normative. Wherever this document says a value is kernel-pinned, the reference verifier proves the stated equality inside the Lean kernel (by rfl in a checker-authored witness or as a conjunct of the accepted-artifact proposition); a conforming verifier MUST NOT accept a package for which any pinned equality fails. Wherever this document says a value is declared-only, the value is transported for display and is deliberately not part of the verified claim; a conforming verifier MUST NOT present declared-only values as verified facts.

TODO-decision: format name. The format has no frozen public name. This document uses the descriptive phrase "Aver artifact certificate format"; a short stable name (for registries, media types, file signatures) is an open decision and MUST be settled before the format is declared frozen.

1. Versioning and identity

Three version-like identities govern acceptance:

Identity	Current value	Where it lives	What it versions
Package layout version	1 (FORMAT_VERSION)	cert-manifest.json format.version	The cert/ directory layout and the transport envelope
Statement schema version	3 (CERT_SCHEMA_VERSION)	cert-manifest.json schema_version	The certificate statement schema: manifest fields, obligation shapes, plan grammars
Wall identity	sha256:<64 lowercase hex>	cert-manifest.json format.wall_id	The exact checker-owned Lean soundness wall plus its pinned Lean toolchain

A conforming verifier MUST reject a package whose schema_version is not exactly the schema version it implements, whose format.version is not exactly 1, or whose format.wall_id does not name a wall embedded in the verifier itself. There is no version negotiation, no downgrade path, and no filesystem, environment, or network fallback for resolving a wall.

Schema version 2 differed from version 1 in exactly one point: the subject's hostRoleTable became optional. A module may declare null, and the acceptance proof pins that declaration against a byte-derived proof that the module's export section decodes strictly and contains no function export named __rt_aint_from_i64 — exactly that fact and nothing stronger (see section 4.3 for what this does and does not prove). A version-2 verifier MUST NOT accept a schema_version: 1 package.

Schema version 3 differs from version 2 in exactly one point: the object form of hostRoleTable gained the required toIndex key. The fused vector-read face binds the __aint_to_index helper by its named function export, exactly like box (see section 4.3); because the nested role-table object is matched exactly, a version-2 verifier would reject every manifest carrying the new key, so the extension is a version bump rather than an additive field. A version-3 verifier MUST NOT accept a schema_version: 2 package.

The wall identity is computed, not assigned. It is the SHA-256 of a domain-separated, sorted, length-framed encoding of every wall source file plus the Lean toolchain pin, formatted as sha256: followed by 64 lowercase hex digits. The exact encoding: the ASCII bytes aver-certificate-wall\0v1\0, then the file count as a big-endian u64, then for each file in ascending filename order: the filename length as big-endian u64, the filename bytes, the contents length as big-endian u64, the contents bytes. The file set is the 38 embedded .lean wall sources plus one synthetic file named lean-toolchain whose contents are the embedded toolchain file hashed verbatim — currently the ASCII bytes leanprover/lean4:v4.32.0 followed by one trailing newline (the file is embedded with include_str!, so the newline byte is part of the hashed contents; a reimplementation that hashes the trimmed pin computes a different identity). The current embedded wall identity is sha256:796f325112054542d62878cf9b1df754fa71a88bb64f61c28145cd464239266e (CURRENT_WALL_ID in format.rs). The reference verifier recomputes this digest over its own embedded sources on first use and aborts if it disagrees with the compiled-in constant, so a verifier binary cannot silently ship a wall that does not match its advertised identity. A reimplementation MUST resolve format.wall_id only against wall source sets whose recomputed identity is byte-exact; it MUST NOT resolve a wall by name, path, or prefix.

TODO-decision: freeze criteria. Neither format.version = 1 nor schema_version = 3 is declared frozen yet. The criteria for freezing (what constitutes a compatible extension versus a version bump, and whether a frozen schema admits additive optional fields) are an open decision; section 11 states what bumps each identity today, the certificate-lifetime consequences, and the freeze proposal on the table. Until freeze, every schema change bumps schema_version and verifiers reject non-matching versions exactly.

TODO-decision: wall registry policy. The reference verifier embeds exactly one wall and resolves only that identity. Whether a released verifier may embed several walls (for grace-window verification of older packages), and the deprecation policy for retired walls, is an open decision; section 11 describes the re-certification path this forces today.

2. Package layout

2.1 What the producer emits (convention, not acceptance)

A certificate package is one directory, conventionally named cert/, emitted next to <name>.wasm. The producer removes any pre-existing cert/ directory before writing, so an emitted package is always a complete, self-consistent emission. The table below is the producer's layout convention: it documents what aver compile --certify writes and where an auditor should look. Except for cert-manifest.json, no row of it is an acceptance invariant — section 2.2 states the (much smaller) file-level contract acceptance actually imposes. The emission contains:

File	Role
cert-manifest.json	Transport and reporting envelope (section 4). The only non-Lean file.
Plans.lean	The producer's canonical plan serialization: every plan as a Lean value, plus redundant rfl examples binding each plan through the audited checkers/lowerers to exact code-entry bytes (section 6). Convention only — acceptance requires neither this file nor its examples (section 2.2).
Manifest.lean	The Lean manifest literal (AverCert.manifest : Schema.Manifest): subject data, per-export obligation definitions, and the plan lists (section 5).
Module.lean	Certified function bodies re-rendered as CertPrelude.WInstr data (CertModule.*Code), host tables, and the pinned CertModule.wasmSha256 string. Of these names the wall references only CertModule.wasmSha256 (in Schema.Holds); the CertModule.*Code naming is convention (section 2.2).
Contracts.lean	Human-auditable restatement of the named runtime contracts. Contracts enter the certificate theorems as hypotheses, not as Lean axioms. Note the staging scan of section 9 does not ban the axiom keyword; the guarantee that no extra axiom is used comes from the axiom guard over the accepted root's closure (section 8) — an unused axiom elsewhere in package files does not reject.
Certificate.lean	Per-export simulation proofs and their composition into the schema obligations.
Final.lean	The single final schema theorem AverCert.Final.cert : AverCert.Schema.Holds manifest.
Artifact.lean	The artifact claim data (AverCert.Artifact.data : ArtifactData), the per-family acceptance proof bundles, and acceptedWithFinal.
ArtifactSoundness.lean	Per-artifact glue instantiating the artifact-independent acceptance-soundness wall at the real module hash.
ArtifactCertificate.lean	The public proof root: theorem AverCert.Artifact.certificate : AverCert.AcceptedArtifact.accepted AverCert.Artifact.data, followed by #print axioms.
Model modules (AverCommon.lean, <Module>.lean, ...)	The aver proof Lean model emission, copied with every deriving line stripped (the staging token scan rejects deriving). These carry the source-model definitions the obligations reference. A dotted module dependency (Data.Fibonacci) ships its model at the corresponding nested path (Data/Fibonacci.lean) and is imported by Manifest.lean and Certificate.lean under its dotted module name (import Data.Fibonacci).

The producer never emits — and MUST NOT emit — ArtifactBytes.lean (checker-generated from the actual .wasm, section 7), CheckerWitness.lean (checker-authored, section 8), lakefile.lean, lean-toolchain, any wall source file, any build cache, or plan sidecar files (*.plan, JSON plan ASTs).

2.2 What acceptance requires of the file set

Acceptance is deliberately indifferent to layout. The staging rules of section 9 (stages 4–6) are the complete file-level contract: every regular file directly in the package directory whose name ends in .lean (case-sensitively) is staged, unless its exact name is checker-owned — then it is silently ignored. A .lean file in a subdirectory (a nested model module such as Apps/Notepad/Store.lean) is staged at its relative path exactly when the staged top-level Manifest.lean or Certificate.lean carries an import line naming its dotted module name (import Apps.Notepad.Store) — the producer imports every model root from those two files, so admission is a one-level check with no transitive closure. That admission list is authored by the untrusted producer: it is build-set minimization, not a security boundary — every staged file, flat or nested, passes the same stage-5/6 gates, and the verdict rests on the checker-authored witness of section 8 (see stage 4 for the literal, comment-blind import-line scan a reimplementor must match). Every path segment of a nested file must pass the stage-5 identifier rule, dot-directories (.lake, .git) are skipped entirely at every depth, nesting is capped at 16 directory levels, and two staged paths equal ASCII-case-insensitively are rejected outright. Everything else (unimported nested .lean files, non-.lean files, sidecars) is ignored outright. Consequences a reimplementor MUST NOT get wrong:

• No closed file set. Extra .lean roots beyond the conventional table are staged and built like any other package file, and a missing conventional file is not itself an error. The verdict comes from whether the staged set elaborates and the accepted root holds at its pinned type — not from which files exist.
• Plans.lean is not load-bearing. The checker witness imports AcceptedArtifact, ArtifactBytes, Manifest, Artifact, and ArtifactCertificate — never Plans directly. The plan values the manifest and claims reference may be defined in any staged file, and the emitted rfl examples may be omitted: the acceptance predicates state the same equalities themselves (section 6.4).
• Module.lean names are not load-bearing. Acceptance binds each lowered body to the obligation's code table and to the artifact bytes (section 6.4), not to definitions named CertModule.*Code; the wall references CertModule only for wasmSha256 (Schema.Holds, section 5).
• Every staged .lean file is untrusted data. It participates in the verdict only after the staging gates of section 9 and only because the Lean kernel accepts the resulting proof against checker-pinned facts.

Module roots that case-insensitively collide with a toolchain root, a wall source root, or a checker-owned root are rejected at staging (section 9, stage 5); for a nested file the check covers the dotted module name and every dotted prefix of it (Lean/Extra.lean is rejected like a flat Lean.lean). Two staged package paths that are equal ASCII-case-insensitively (Foo.lean and foo.lean, Apps/Store.lean and apps/Store.lean) are rejected outright, so the staged tree is identical on case-sensitive and case-insensitive filesystems. Known gap: the .lean suffix test itself is case-sensitive, so a file named ArtifactBytes.LEAN is silently ignored rather than rejected.

3. Trust vocabulary: kernel-pinned versus declared-only

The manifest JSON is a transport envelope. The authoritative statement is the Lean value AverCert.manifest in Manifest.lean together with the claim data in Artifact.lean, and the verifier's checker witness pins the JSON's trust-bearing fields to that Lean value by rfl (section 8). Consequently every cert-manifest.json field is in one of two base classes (a few rows in section 4 carry a noted refinement: a pinned string whose value is not validated against any expected identifier, or a pinned pair whose name is byte-accounted while its prose is not):

• Kernel-pinned: the witness (or the accepted-artifact proposition itself) states an equality between the JSON-derived value and the Lean manifest/claim data, and the wall further binds that Lean data to the artifact bytes. Tampering with the JSON, the Lean data, or the bytes independently makes elaboration fail.
• Declared-only: transported for reporting. The reference verifier either never reads the field on the acceptance path or reads it only to print it with an explicit "declared" label. The certified[].dom / certified[].cod strings are the deliberate example: the source-facing domain/codomain prose is display-only and unpinned by design, because the pinned semantic face lives in the typed Obligation (Dom/Cod types and representation relations) and in StandardFace, not in a string. The CERTIFIED/CHECKED report MUST print only kernel-pinned facts; explain MAY print declared-only values with an explicit label.

4. cert-manifest.json, schema version 2

The manifest is a single JSON object. The reference parser is strict about the fields it reads: a missing or mistyped required field is a hard error. String fields that are later interpolated into the checker witness pass a candidate gate first: at most 200 bytes, every byte in 0x20..=0x7E, and neither " nor \ (this makes Lean string-literal injection unrepresentable). The gated strings are: each certified export's name, class, dom, cod; every runtime_contracts entry; every declaredUncertified name and reason; every capabilities module and name; profile; and abi.

TODO-decision: top-level strictness. Nested objects are matched exactly (an unexpected or missing key inside start, hostRoleTable, stringHostRoles[], declaredUncertified[], or capabilities[] is an error), but unknown top-level members are currently ignored by the reference verifier. Whether a frozen schema requires rejecting unknown top-level members is an open decision; producers MUST NOT rely on the current leniency.

4.1 Top-level fields

Field	Type	Trust class	Meaning and constraints
schema_version	integer	verifier-checked	MUST be exactly 3.
format	object {version, wall_id}	verifier-checked	version MUST be exactly 1; wall_id MUST resolve to an embedded wall (section 1).
wasm	string	declared-only	The artifact filename the producer emitted next to the package. Never read on the acceptance path; the artifact identity is the file the caller passes to the verifier.
wasm_sha256	string, 64 lowercase hex	kernel-pinned	SHA-256 of the exact artifact bytes. The verifier MUST recompute the hash of the supplied .wasm and reject on mismatch; the witness additionally pins manifest.subject.artifactHash to the recomputed hash, and Schema.Holds conjoins artifactHash = CertModule.wasmSha256 (section 7).
level	string	declared-only	"L1", "L3", or "mixed L1/L3". The verifier computes its own level banner from the pinned policies and never reads this field.
profile	string	kernel-pinned, value-unvalidated	Emitted-fragment profile identifier; the producer writes "AverUserProfile/v1". The witness pins the JSON string to subject.profile by rfl, but no acceptance check compares the value against any fixed identifier: any string passing the candidate gate is accepted, and explain prints it unqualified. Known gap — the identifier constant exists only on the producer side (PROFILE_ID in engine/mod.rs).
abi	string	kernel-pinned, value-unvalidated	Runtime ABI identifier; the producer writes "aver-wasm-gc/0". Same status as profile: pinned to subject.abi by rfl, not validated against any fixed identifier. Known gap — the constant exists only on the producer side (RUNTIME_ABI in engine/mod.rs).
final_theorem	string	declared-only	"AverCert.Final.cert". Informational; the checker consumes the artifact root below, not this name.
artifact_certificate_root	string	verifier-checked and kernel-pinned	MUST be exactly "AverCert.Artifact.certificate". Checked in Rust, pinned to subject.artifactRoot by the witness, and re-checked in-kernel by subjectMatchesArtifactRoot.
carrier_type_index	integer or null	declared-only	The wasm type index of the Int carrier struct, null for carrierless modules. The kernel derives the carrier independently via CertDecode.carrierState; this field is reporting convenience.
runtime_contracts	array of strings	kernel-pinned	The named runtime contracts every certificate is conditional on. Pinned to subject.contracts. This is an ordered list, not a set: the in-kernel ClaimAxes check independently derives the exact required contract list from the checked claims — assembled in the canonical order box, add, sub, mul, String.eq, String.concat, add-total, sub-total, mul-total — and compares by exact list equality, so permuting the same strings rejects.
declaredUncertified	array of {name, reason}	kernel-pinned (names); reasons pinned but unvalidated	Exports outside the claimed obligations, each with a reason. The {name, reason} pairs are pinned JSON-to-Lean to subject.declaredUncertified, but the byte-level accounting consumes only the names: the in-kernel exportsAccounted check requires that every byte-derived module export is either a claimed obligation (matching name, kind, and function index) or listed here by name, with both lists duplicate-free, disjoint, and free of phantom names. Each reason is transported prose — printable-gated and equality-pinned, but neither byte-derived nor semantically validated.
capabilities	array of {module, name}	kernel-pinned	The exact effect-import surface, in import-section order. Pinned to subject.capabilities; the in-kernel importsWithinCapabilities check requires the byte-derived import section to equal this list exactly and every pair to be a member of the kernel-owned CAPABILITY_REGISTRY (the closed list of ("aver", ...) host imports; the verifier crate carries the same list as WASM_GC_CAPABILITIES so the compiler cannot silently broaden it).
start	object {present, function_index}	kernel-pinned	Exactly these two keys. present: false MUST pair with function_index: null; present: true MUST pair with a u32. Pinned to subject.start; the in-kernel startAccounted check equates it with the byte-derived start-section decode.
hostRoleTable	null or object {box, add, mul, sub, toIndex}	kernel-pinned	See section 4.3.
stringHostRoles	array of {function_index, role}	kernel-pinned	role MUST be "stringEq" or "stringConcat"; function_index a u32. Pinned to subject.stringHostRoles and bound in-kernel to CertDecode.StringHost.roleTable recomputed from the bytes. The decode classifies every defined function independently and emits matches in defined-function order, retaining duplicate roles at distinct indices; the bind is exact list equality, order and multiplicity included.
certified	array of objects	mixed; see 4.2	One entry per certified export, in manifest-obligation order.
source_level_only	array of {name, reason}	declared-only	Functions the producer declined to certify, with reasons. Never read on the acceptance path. explain prints it under an explicit informational heading, but only for packages with at least one certified export, and from a second manifest read performed after the verdict (see the known gap in section 9, stage 11). The fail-closed emission policy — a declined function gets an entry here rather than a weaker theorem — is producer behavior, not an acceptance-checked fact; whole-module accounting relies on declaredUncertified, not on this list.

Declared-only rows describe producer output. The reference verifier never reads wasm, level, final_theorem, carrier_type_index, certified[].level, certified[].theorem, or source_level_only on the acceptance path — and therefore does not type-check them either. Their tabulated types and example values are producer conventions, not acceptance requirements; a package in which they are missing or mistyped still verifies.

4.2 certified[] entries

Field	Type	Trust class	Meaning and constraints
name	string	kernel-pinned	The export name. Pinned three ways: manifest.obligations.map export_, subject.exports, and the first component of the StandardFace.reportEntries pairs.
class	string	kernel-pinned	The admitted family label. Pinned as the second component of StandardFace.reportEntries, which the wall derives from the checked claim family and plan — the producer cannot choose a more favourable label. Current labels: expr-fragment-v1, verbatim-string-eq, verbatim-string-concat, adt-constructor, self-recursive, multi-argument self-recursive, mutual-recursive, verbatim-dispatch, int-dispatch, field-projection, cross-function-composition.
policy	string	kernel-pinned	MUST be "simulatesModel" or "simulatesModelTotally"; anything else is rejected in Rust. Pinned to manifest.obligations.map policy and independently re-derived in-kernel by ClaimAxes.
level	string	declared-only	"L1" for simulatesModel, "L3" for simulatesModelTotally. Redundant with policy; not read by the verifier.
dom, cod	strings	declared-only by design	Source-facing domain/codomain prose. Never pinned by any witness line and MUST NOT appear on the CERTIFIED/CHECKED report; explain prints them labeled manifest face (declared, not kernel-pinned). The verified face is the typed Obligation.Dom/Cod with their representation relations, enforced by StandardFace.
theorem	string	declared-only	The discharge theorem the producer used (e.g. AcceptanceSoundness.exprFragment_claim_discharges). Informational; acceptance consumes the single artifact root, not per-export theorem names.
termination_witness	object, optional	kernel-pinned	MUST be absent when policy is "simulatesModel" and present when "simulatesModelTotally" (both directions are hard errors). Shape: {"measure": {"kind": "intNatAbs", "param_index": <u32>}, "descent": <i64>}; kind MUST be "intNatAbs". Pinned to manifest.obligations.map termination?. In-kernel, ClaimAxes accepts only the canonical witness {measure := .intNatAbs 0, descent := -1} and Schema.checkTerm/checkTermMutual verify it against the byte-bound recursion plan (floor guard at n ≤ 0, recursive argument exactly sub(n, box 1)).

4.3 hostRoleTable: the declare-and-confirm host-helper pin

hostRoleTable declares the module-wide box/add/mul/sub/toIndex host-helper table used by plan lowering. Its JSON forms are: null, or an object with exactly the keys box, add, mul, sub, toIndex, each a u32 or null. The transport parser accepts all five members as nullable, but in an accepted package the object form always has box bound: the object branch of the strict decode below is reachable only when the box-helper function export exists, so only add, mul, sub, and toIndex may be null (an individual role may be unbound while the table as a whole exists). toIndex binds like box: by its named function export — __aint_to_index, the fused vector-read index helper — null exactly when no such export exists, and, like every other role, by an equality against the helper's actual code bytes. This maps to Subject.hostRoleTable : Option CertDecode.AddSub.Roles in the Lean manifest.

The kernel binds the declaration to the module bytes with AcceptedArtifact.arithTableCheck — declare-and-confirm, not a byte fingerprint and not a role scan. The manifest states which function index carries each role; the wall synthesizes the canonical helper body from the declaration and pins the real code bytes equal to it, and for the two roles that also have a fixed runtime export name (box, toIndex) it re-derives the index from the export section as well. Exactly two shapes close the pin, and mixing null with an object across hostRoleTable/arithParams fails closed.

Note for reimplementors: unlike hostRoleTable, arithParams has no JSON transport form. It is ArithTemplateDerisk.ArithHostParams in the Lean manifest only — six declared indices (carrier, limb, decompose, normalize, strip, umagCmp) that the wall synthesizes helper bodies from. Nothing in it is computed from bytes; it is a declaration the template equality then confirms against the real code. arithParams.carrier carries one further pin of its own: a declared table requires CertDecode.carrierState = some (some arithParams.carrier), so an admitted arith table implies the type section really holds an Int-carrier struct at exactly the index the synthesized helper bodies splice. Every other conjunct of this pin reads the export section or the code section, so without this one the declared carrier would be confirmed only by the bytes the wall itself synthesized from it, and a module whose type section holds no carrier-shaped struct at all could still present a table. That is reachable, not hypothetical: isCarrier requires the third field's storage tag to be 0x7f, so a working carrier whose flag field is a packed i8 (tag 0x78) is invisible to it. A reimplementation MUST NOT drop this conjunct on the grounds that the template equality already constrains carrier — it constrains the helper bodies, not the type section.

• Carrierless — hostRoleTable: null and arithParams: null, pinned by CertDecode.AddSub.carrierHelperAbsent: the export section decodes strictly and no function export is named __rt_aint_from_i64. A malformed or undecodable export section never certifies absence. This function-export-name absence is exactly what the pinned fact proves — no more. It does not by itself prove "the module has no Int carrier type" or "no Int runtime": an Int-carrier struct type, an unexported helper function, a differently named helper, or a non-function export bearing this name are all outside the pinned fact. A report or reimplementation MUST NOT present hostRoleTable: null as anything stronger; the operative consequence is the claim-matching rule below (no box/add/mul/sub/toIndex role can be cited by any claim in such a module).
• Carriered — hostRoleTable present as an object, arithParams present, the __rt_aint_from_i64 function export present, and all of:
  • box equals the function index of the __rt_aint_from_i64 export (bound by export name) and the code entry at that index equals the canonical box helper body synthesized from arithParams (bound by template equality, the same mechanism as add/sub/mul);
  • toIndex equals the function index of the __aint_to_index export, and is null exactly when that export is absent (bound by export name, the same rule as box), and the code entry at that index equals the canonical toIndex helper body (bound by template equality). Unlike box, a carriered module may legitimately declare toIndex: null, because the producer emits that export only when a vector or list index extraction instantiated the helper. Both pins are kept because they answer different questions: the template equality is vacuous on null, so only the name binding makes null mean "the export is genuinely absent" rather than "no body was checked";
  • a note on what the template equality does and does not buy, since it is easy to read as more: it fixes WHICH code runs at those indices, not what that code computes. The wall never interprets these bodies. The runtime contracts for box and toIndex remain assumptions, disclosed through the claim axes exactly as before — what changes is that they now attach to a fixed, auditable constant instead of to whatever function the producer chose to export under that name;
  • the arithParams indices lie inside the LEB regime the templates are written for (checkArithHostParams): all six indices are < 2^32, the whole u32 index space the wasm binary format admits. The template synthesis splices every index through the canonical LEB128 encoding wasm uses at that position — call targets and struct.new/struct.get/array-op type indices as unsigned u32 LEB (CertPrelude.uleb32Bytes), ref.null and (ref null _) heap-type positions as signed s33 LEB (CertPrelude.s33Bytes), where the sign bit makes 64 the first two-byte value (64 encodes as c0 00, not 40; unsigned positions grow their second byte at 128). Both encoders are total, fuel-bounded functions that are exact strictly beyond the u32 bound (unsigned below 2^35, signed below 2^41), so within the checked band every synthesized hole is the byte sequence a wasm encoder would emit. An earlier wall revision spliced each index as a single raw byte and bounded function indices below 128 and limb below 64; that made the synthesized body one byte short for any module whose helper indices need a two-byte LEB, i.e. large honest programs could not certify (a false negative, never a false accept);
  • each non-null role — box, toIndex, add, sub, mul — is pinned by template equality: the real code-section body at the declared function index equals the canonical helper body synthesized from arithParams alone. For add/sub/mul this is the whole binding; for box/toIndex it is a second, independent pin on top of the export-name equality above. A null role is vacuously pinned — no claim can cite an unbound role, so no plan can use it.

box and toIndex therefore carry two pins, and a reimplementation MUST enforce both, because they constrain different things and neither implies the other:

• the export-name equality says at which index the role may be declared. It is the only pin with any force on a null declaration, since the template equality is vacuous there by construction. Drop it and "this module exports no __aint_to_index" stops being a byte-proved fact and becomes a producer's free choice.
• the template equality says which bytes sit at that index. The export-name equality never reads the code behind the export, so without this a package could ship an honestly named __rt_aint_from_i64 or __aint_to_index whose body is not the canonical helper at all.

What the template equality does not establish is what that code computes. It identifies the code behind a role, never its meaning: the box, index-extraction and arithmetic contracts remain explicit hypotheses of Obligation.holds and remain disclosed by ClaimAxes (section 5.2). Pinning bytes narrows the artifact, not the trusted-computing base.

Reimplementor note: no byte is scanned to discover any role. A wrong declaration synthesizes different bytes and fails the equality. Earlier revisions of this document described the pin as an equality against a module-wide role scan (roleTableStrict); that scanner has been deleted from the wall, and only the three decoders named above (boxIdx, toIndexIdx, carrierHelperAbsent) participate in binding this table.

For claim matching, an absent table binds no roles at all (Subject.hostRoles maps none to the all-none table), so any claim citing a box/add/mul/sub/toIndex role in a carrierless module fails to match — strictly fail-closed, never a default index.

4.4 Target scoping: core fields versus the wasm envelope

The subject fields split along one criterion: what their kernel pin is stated against. Fields pinned against fixed constants or against other manifest data — wasm_sha256/artifactHash (the pin shape; the hash function itself is a target choice), profile, abi, artifact_certificate_root, the certified export names, declaredUncertified, and runtime_contracts — are target-generic core: they describe the claim structure, not WebAssembly. Fields pinned against byte decoders over the artifact — capabilities, start, hostRoleTable, and stringHostRoles — are the wasm envelope: facts about wasm sections (the import section, the start section, the Int-carrier helper exports, the string-helper function bodies) that only exist because the target is WebAssembly. Section 4.3 and the decode-bound rows above are envelope material, as are the byte-level mechanisms of sections 6–7 (the fragment IR, the byte lowering, the section framing and closure scan). A future non-wasm target would keep the core — obligations, policies, plan-claim agreement, faces, axes, the whole-module accounting principles — and replace the envelope with its own decoder-pinned facts, specified as an added envelope section of this document rather than a rewrite. This seam is currently descriptive: schema version 2 transports core and envelope fields as siblings in one flat manifest object, and no non-wasm envelope exists.

5. Obligations, claims, and policies

The Lean manifest (Schema.Manifest) carries the subject, eleven per-family plan association lists keyed by export name (symFragmentPlans, stringEqPlans, stringConcatPlans, constructPlans, exprFragmentPlans, recursionPlans, mutualPlans, compositionPlans, verbatimPlans, intDispatchPlans, fieldProjectionPlans), and obligations : List Obligation.

An Obligation is the typed statement unit: export name, policy, optional termination? witness, totalityRole (default .addSub), the carrier type index, the emitted code table code : CodeTbl and host-table builder host, the export's own function index self, the source types Dom/Cod, the representation relations domRepr : CarrierSpec carrier → Dom → List WVal → Prop and codRepr : CarrierSpec carrier → Cod → WVal → Prop, and the source model model : Dom → Cod.

simulatesModel (level L1, partial simulation). Obligation.holds states: for every carrier specification S, every host implementation of add/sub/mul/String.eq/String.concat satisfying the named contract laws (integer add/sub/mul preserve representation; String.eq computes byte equality; String.concat computes byte concatenation), every fuel, and every represented domain value — if the emitted body evaluates to a result, that result represents model x. Vacuous on trap or fuel exhaustion. The contracts are explicit hypotheses of the theorem, never axioms.

simulatesModelTotally (level L3, total simulation). Obligation.holdsTotal additionally assumes totality of the host helpers selected by the obligation's totalityRole (.addSub: add and sub total on represented operands; .mul: additionally mul total, admitted only for a byte-pinned unary recursion whose combine role is mul) and promises an actual result at fuel n.natAbs + 1, where n is the checked integer counter (the first domain argument). The termination evidence is the canonical witness of section 4.2, checked against the byte-bound plan by Schema.checkTerm (unary and accumulator recursion) or Schema.checkTermMutual (mutual SCC members, whose recursive edge is a tail call pinned to the byte-derived SCC member set — not to the member's own index; the member's own index is in that set, so a legitimate two-cycle back-edge is admitted, and the byte-equality gate then forces the call to the member's actual target).

The artifact-independent proposition is HoldsCore m: every obligation satisfies the denotation selected by its policy. The full schema proposition, Schema.Holds m, conjoins m.subject.artifactHash = CertModule.wasmSha256, binding the statement to the artifact hash literal carried in Module.lean (which the witness in turn pins to the recomputed hash of the actual bytes).

The public proof root accepted by the verifier is AverCert.Artifact.certificate : AverCert.AcceptedArtifact.accepted AverCert.Artifact.data, where accepted conjoins: Schema.Holds of the manifest; subjectMatchesArtifactRoot; fragmentClaimObligationsInManifest (every claim's obligation literal is found in the manifest by export name); claimsMatchManifest (full plan-pair equality exactly where plans are claim-side data: the sym-plan pairs of the sym-fragment, String.eq, String.concat, and constructor claims — concatenated in that order — must equal symFragmentPlans, the encoder output of the sym-fragment claims must equal exprFragmentPlans, and the composition member pairs must equal compositionPlans; every other family is equated by its ordered export-name list only, with the plans themselves then looked up in the manifest lists and checked by that family's acceptance predicate); StandardFace.checkedFaces (section 5.1); ClaimAxes.checked = true (section 5.2); decodedNonExprFacts (module-wide host-role and string-role decodes plus per-claim code/carrier/struct-field decodes recomputed from bytes); and acceptedFragments (per-family byte acceptance plus the whole-module accounting of section 5.3).

5.1 StandardFace: the admitted semantic face

StandardFace.checkedFaces requires, per claim family, that the obligation's carrier, Dom, Cod, domRepr, codRepr, complete host builder, and (for reconstructible families) model equal the standard face selected by the checked family and plan. Faces bind the whole host function, not probe points, so an unmentioned input cannot turn a contract into a trap. Every role/index pair a claim cites must agree with the byte-decoded role table (hostTableBound), with pairwise-distinct indices. claimExportsUnique requires that one export is claimed by exactly one family across all families. User-ADT domain meaning, representation interpretation, and models that cannot be reconstructed from Wasm remain explicit read declarations: for those faces only the reconstructible parts are forced, and the theorem is conditional on the declared meaning (see section 10).

StandardFace.reportEntries derives the public (export, class) report pairs in manifest-obligation order from the checked claims — the class labels of section 4.2 are outputs of this function, and the checker witness pins the JSON report to them.

5.2 ClaimAxes: policy, termination, totality, contracts

ClaimAxes.checked recomputes, from the checked plans alone, the axis triple (policy, termination witness, totality role) each obligation must carry — every non-recursive family is forced to the partial axis; recursion families are forced to total with the role classified from the byte-bound plan shape — and the exact ordered runtime-contract list the manifest must disclose, assembled in the canonical order of section 4.1 and compared by exact list equality. A totality claim can therefore never be smuggled in through a JSON label, and a contract can never be omitted from (or reordered within) the disclosure.

5.3 Whole-module accounting

acceptedWholeModule conjoins byte-derived checks over the entire module: moduleFramingValid (strict section framing); exportsAccounted and importsWithinCapabilities and startAccounted (section 4.1); and closureIsolation — the direct-call closure of all certified roots, recomputed from the code section by an in-kernel scanner, must equal the declared root/helper partition, with no imports reachable, no instruction channels outside the certified profile, and no shared memory declared. manifestObligationsClaimed and manifestObligationExportsUnique close the coverage direction: every manifest obligation is claimed by some family and obligation export names are pairwise distinct, so an unclaimed obligation cannot ride into the accepted artifact unchecked.

6. Plan grammar and the canonical byte-lowering contract

Plans are the producer's untrusted explanation of why a function body has its certified meaning. They are Lean values referenced by the manifest plan lists and the artifact claims; the producer serializes them once, in Plans.lean (namespace AverCert.Plans), but that location is convention — acceptance requires only that the referenced plan values are defined in some staged file (section 2.2). There is no JSON plan AST in the package; a JSON projection would be a second authority that must agree with the first, so it is deliberately absent.

6.1 Plan profiles

Every raw-plan structure carries a profile string that MUST match the value its checker expects:

Profile string	Lean type	Family
sym-fragment-v1	SymRawPlan	Source-level symbolic plan (SymPlan), the portable source-meaning IR
expr-fragment-v1	ExprFragmentRawPlan	Representation-level ANF fragment
recursion-plan-v1	RecursionRawPlan	Unary / accumulator integer fuel-recursion
mutual-plan-v1	MutualRawPlan	One member of a mutually-recursive integer SCC
composition-plan-v1	CompositionRawPlan	Cross-function direct-call composition shape
verbatim-plan-v1	VerbatimRawPlan	Verbatim ref.test-dispatch (Cod := WVal)
int-dispatch-v1	IntDispatchRawPlan	Int-valued ADT dispatch (Cod := Int)
string-eq-v1	StringEqRawPlan	One-literal String.eq match
string-concat-v1	StringConcatRawPlan	Literal-affix String.concat
construct-v1	ConstructRawPlan	ADT constructor struct.new witness
field-projection-v1	FieldProjectionRawPlan	Bare tuple/record field projection

6.2 SymPlan: the source-level grammar

SymRawPlan is {profile, params : List SymTy, result : SymTy, body : SymBlock}. A SymBlock is an ordered ANF node list plus a result node id; each SymNode is {id, ty : SymTy, kind} where id must equal the node's position in the block (checked before lowering). SymTy is int | float | bool | string | named name | app1 name arg | app2 name left right — deliberately with no raw-WVal escape hatch. SymNodeKind is: param index, constBool, constInt, constFloatBits, constStringBytes, prim op args (with SymPrim = floatAdd | floatMul | floatLe | floatGe | floatLt | floatGt | floatEq | intAdd | stringEq | stringConcat), construct typeName ctorName args, emptyList elemTy, projectField typeName field fieldTy value, intConstCmp op value constant (with SymIntCmp = eq | lt | le | ge | gt), and ifElse cond thenBlock elseBlock.

A SymPlan carries no wasm-level indices. For the generic sym-fragment family, the audited in-wall encoder PlanCheck.encodeSymRawPlanToExprFragmentRawPlan maps it to an ExprFragmentRawPlan under the byte-derived host-role and struct tables, and acceptance equates the encoder output with the manifest's exprFragmentPlans entry, so the source-level claim and the byte-level plan cannot drift apart. Two precision points a reimplementor MUST honor:

• The encoder is only the generic-fragment bridge. It fail-closes (returns none) on constStringBytes, construct, emptyList, the stringEq/stringConcat primitives, and any projectField whose encoded type is not an opaque reference. Those SymPlan shapes are not encoded at all; each is bound to its representation-level plan by a separate matching predicate checked inside the family acceptance: stringEqPlanMatchesSymRawPlan (one-literal String.eq match), stringConcatPlanMatchesSymRawPlan (literal-affix String.concat), and constructPlanMatchesSymRawPlan (ADT constructors, whose field matching also admits emptyList nodes — empty-list construction rides this family). Treating the encoder as the universal SymPlan semantics would wrongly reject valid packages in these families.
• Index provenance splits by level. Wasm-level indices — host-helper function indices (hostRoleIdx?) and struct type indices (structTyIdx?) — are always drawn from the byte-derived tables; the plan cannot cite them. Source-level ordinals remain plan data: parameter indices, the positional node ids, and the projected field ordinal (projectField.field is copied verbatim into the encoded structGetUser node). Those plan-supplied ordinals are subsequently forced by the byte-equality gate of section 6.4, not by the encoder.

6.3 Fragment IR: the representation-level grammar

ExprFragmentRawPlan is {profile, params : List FragTy, result : FragTy, body : FragBlock} with the same positional-id ANF discipline. FragTy is f64 | boolI32 | intCarrier | i64 | rawI32 | ref | adtRef; FragTy.sourceTy? projects only f64/boolI32/intCarrier to source types, so raw limbs cannot silently acquire source meaning. FragNodeKind is: local index, constBool, constI64, constI32, constF64Bits, structGet field receiver (Int-carrier limb reads), structGetUser tyIdx field value (whole user-struct projection; the type index is node data bound to the bytes, mirroring hostCall), refIsNull, prim op args (with FragPrim = f64Add | f64Mul | f64Le | f64Ge | f64Lt | f64Gt | f64Eq | i64Eq | i64LeS | i64LtS | i64GeS | i64GtS | i32Eq | i32LtS | i32GtS | i32And), hostCall role funcIdx args (with HostRole = box | add | mul | sub | toIndex, the last consumed only by the fused vector-read node; the resolved index is bound both to the bytes and to the decoded role table), selfCall tail funcIdx args (recursion families only; in the ordinary recursion family every self-call is bound to the current function's byte-derived index, while in the mutual family the recursive edge must be a tail call whose target is bound to the byte-derived SCC member set, the byte-equality gate then forcing the actual target), and ifElse.

The dispatch-family grammars (verbatim-plan-v1, int-dispatch-v1) are separate because their multi-use scrutinee spills through scratch locals, which pure ANF cannot express; their leaf/cascade constructors, and the remaining per-family plan structures, are defined in SchemaCore.lean and are the normative reference for field-level detail. Two representative invariants: IntDispatchRawPlan arms name host helpers by role only (the byte-derived role table parameterizes the lowerers, so a plan cannot cite an index), and scratch-local numbering is a fixed function of the arm count rather than plan data.

6.4 The canonical byte-lowering contract

The load-bearing invariant of the whole format is: the certified function's bytes are the canonical lowering of its checked plan, and both sides of that equality are computed inside the Lean kernel. For every accepted plan the wall establishes, by definitional reduction (rfl):

1. Structural check: the family checker in PlanCheck accepts the raw plan (checkSymRawPlan, checkExprFragmentRawPlan, checkRecursionRawPlan + the context-sensitive checkRecursionPlanShape against the byte-derived self index and role table, checkMutualRawPlan + checkMutualPlanShape against the byte-derived SCC member set, checkVerbatimPlan, checkIntDispatchRawPlan, checkStringEqRawPlan, checkStringConcatRawPlan, checkConstructRawPlan, checkFieldProjectionRawPlan, checkCompositionRawPlan).

2. Semantic lowering: PlanLower.lower*Body maps the plan to the exact CertPrelude.WInstr body the obligation's code table must return at the bound function index — so the proved simulation is about precisely the lowered semantics. (The producer conventionally names these body literals CertModule.*Code in Module.lean; acceptance binds obligation.code, not any named definition — section 2.2.)

3. Byte lowering: PlanBytes.lower*CodeEntry maps the plan to the exact Wasm code-entry byte sequence (local declarations + expression body + ULEB128 body-size prefix; ULEB/SLEB encoders are defined in-wall). This is a plan-first byte encoder for the checked profiles, not a general Wasm assembler.

4. Byte-origin binding: WasmSlice.exactFuncBindingForExport modBytes modLen exportNameBytes codeEntry finds, in the actual artifact bytes, the export with that exact name and requires its code entry to equal the lowered bytes, returning the pinned FuncBinding {funcIdx, typeIdx, codeEntry}. Where the family needs signature or type facts, additional byte-derived matchers pin them (funcTypeMatches, projectionStructTypeMatches, projectionFuncTypeMatches, listConstructStructTypeMatches, ...). Every family whose claim carries a host-role table (sym-fragment, recursion, mutual recursion, Int-face dispatch, composition) additionally requires WasmSlice.hostTableFuncTypesMatch: each (role, funcIdx) entry's declared function type — resolved through the function section, imports failing closed — must be exactly the signature its role fixes over the claimed carrier (box: [i64] → [(ref null carrier)], toIndex: [(ref null carrier)] → [i32], add/sub/mul: the canonical two-argument carrier signature). Helper bodies are pinned by template byte equality elsewhere, but the body equality does not constrain the declared type: without this conjunct a helper declared at a strict supertype of the carrier reference still wasm-validates by subtyping while the proof faces model the exact claimed carrier. A reimplementation MUST NOT drop this conjunct on the grounds that the helper bodies are already byte-pinned.

   The expression-fragment family carries a second, complementary conjunct at the same site, AcceptedArtifact.symFragmentCarrierBound, and a reimplementation MUST NOT drop it either. The declared-type pin above compares each helper's declared type against the claimed carrier, and for expression fragments that carrier is claim data no decoder constrains (section 4.3's decodedStrictCarrierIndex scope note: sym-fragment claims are absent from the decoded-claim bindings). On that family the pin alone is therefore circular — a producer that declares the box helper AT a fake supertype and claims that same fake index satisfies it, while the template-pinned helper body still builds structs at the real carrier. symFragmentCarrierBound removes the free reference point: whenever the claim's own data can make a proof face read the carrier, CertDecode.carrierState modBytes modLen MUST equal some (some carrier) — a byte-provably carrierless module (some none) and an undecodable type section (none) both reject.

   The trigger is derived from the claim, not from a family list. The binding applies when the claim's hostTable is non-empty OR the encoded ExprFragmentRawPlan names intCarrier anywhere — in the parameter list, in the result, or as the type of any node in the body or in any nested block. Keying it on the host table alone is unsound and MUST NOT be done: StandardFace.fragment states domRepr := args = FragParams.encodeArgs carrier params values, and FragTy.encodeArg sends an intCarrier parameter to carrierSmall carrier value, the concrete three-field struct structv carrier [i64v k, null, i32v 0] at the claimed index. A generic Int -> Bool fragment (the integer-versus-constant comparison shape) asserts that layout while citing no host role at all, so an empty table would exempt a carrier-sensitive face and admit a claim naming a struct the module declares with a different field count — a theorem quantified over states the module's own type section forbids, reported as a certified export. The residual permissive case is exactly "no role cited AND no intCarrier in the encoded plan", where no face can mention the index: that is what keeps projection and float/string-boundary fragments certifiable in carrierless modules.

   The two conjuncts are complementary, and neither subsumes the other. The declared-type pin catches "claimed carrier right, helper type wrong", which no carrier equality can see; the carrier binding catches "both consistently fake" and the role-free claims whose plan names intCarrier — not every role-free claim, only those the trigger above selects — which no declared-type comparison can see (on an empty table it is vacuously true). A reimplementation that ships one without the other has exactly one of these two holes open.

   Known gap: the carrier layout itself is pinned one field short of what the faces assert. CertDecode.TypeEntry.isCarrier — the predicate behind carrierState, and so behind both the binding above and every other family's carrier equality — requires exactly three fields with field 0 tagged i64 and field 2 tagged i32, and says nothing about field 1, while carrierSmall C k = structv C [i64v k, null, i32v 0] places a null reference there. A module declaring (struct (field i64) (field i32) (field i32)) therefore satisfies isCarrier, the binding accepts it, and the face still asserts a value no machine state of that type can hold — the vacuity this section's arity rule exists to prevent, surviving one field over. Closing it means deciding exactly which storage tags admit a null, which is a cross-family change; a reimplementation SHOULD pin field 1 to a nullable reference storage type and MUST NOT read the current predicate as confirming the full carrier layout.

   Faces that assert a fixed value layout carry a matching arity pin. Where a standard face states its domRepr as a literal struct value, the field count in that literal is part of the claim and MUST be confirmed against the type section, or the obligation is quantified over states the module forbids while the report calls the export certified. Three faces are in this shape and all three are pinned, each by a different mechanism, and a reimplementation MUST supply all three: the field-projection face (vs = [structv structIdx [p.1, p.2]], pinned by fields.length == 2 in checkExprProjectionTypes); the tag-dispatch face (vs = [structv optIdx [i32v tag, payload]], pinned by fields.length == 2 in checkTagDispatchTypes alongside the i32 tag-field check); and the generic fragment face, whose intCarrier parameters encode to the three-field carrierSmall carrier value — pinned not by a dedicated arity term but by isCarrier inside the carrier binding above, which admits only a three-field struct, so a claim naming a struct of any other width is rejected there. That indirection is the whole reason the binding's trigger must follow the plan rather than the host table: drop the trigger and this face loses its only width pin. The fused vector-read face is deliberately NOT in this shape — its vecDomRepr quantifies the element list existentially, so it asserts no width and pins the element type instead.

   Known gap, same rule, different fact: the tag-dispatch face is the one ADT face whose scrutinee type index is not tied to the certified function's declared parameter type. Its two siblings do exactly that (checkExprProjectionTypes requires the parameter to be nullableRefType structIdx; checkVectorGetTypes requires it to be nullableRefType arrTy), while exprTagDispatchTypesMatch never receives the function's typeIdx. The face's width and tag-field type are confirmed; which nominal type the scrutinee is remains claim data. A reimplementation SHOULD add the parameter-type equality its siblings carry, and MUST NOT read the arity rule above as confirming the whole scrutinee shape for this face.

The locals prelude is a fact about the module, not a plan choice. Most families lower to a code entry whose locals vector declares exactly one nullable Int-carrier reference, and the carrier type index inside it is claim data confirmed by the step-4 byte equality. string-concat-v1 is the one family that also lowers in a module with no Int carrier struct at all: the compiler emits the carrier struct and its helpers only when some function touches Int, and in a module without them the emitted concatenation body opens with an empty locals vector. PlanBytes.lowerStringConcatCodeEntry therefore takes the module's carrier state (Option Nat) rather than an index, and carrierLocalsBodyBytes selects the one-local prelude for some and the zero-local prelude for none. Which one applies is never the producer's choice: stringConcatPlanAccepted pins that state by CertDecode.carrierState modBytes modLen = some carrier, a strict three-state decode of the type section — some (some idx) when a carrier struct is present, some none when the section decodes and holds none, and none (admitting no declaration at all) when the section does not decode. A carriered module can therefore present only the one-local body and a carrierless one only the zero-local body, and the same pinned state also fixes stringConcatNLocals, the locals count the semantic frame carries, which step 4 and the code decode then check against the real locals vector. Reimplementors MUST NOT treat the two preludes as alternatives a certificate may select between.

Carrierless modules are admitted one step earlier as well, and the admission is scoped to one family. Obligations in the String.concat claim list pin their carrier field with AcceptedArtifact.decodedCarrierIndex, which matches on all three states of CertDecode.carrierState: a decoded carrier struct forces that exact index (the old decodeCarrier equality unchanged), a type section that decodes with no carrier struct forces the reserved index 0, and a type section that does not decode admits nothing. Every other non-expression-fragment family keeps decodedStrictCarrierIndex — the unchanged decodeCarrier … = some obligation.carrier — which no module without a decodable Int-carrier struct can satisfy, so no claim in those families exists in a carrierless module at all.

The scoping is load-bearing, not tidiness. The reserved index is a placeholder, not a claim that type 0 is a carrier, and it is harmless only for a face that provably never consults the CarrierSpec: String.concat's Dom/Cod are WVal, its domRepr is vs = [v] and its codRepr is verbatimRepr, all of which discard the spec argument. Citing no arith role is NOT sufficient for that — String.eq, verbatim dispatch, field projection and named-ADT construction also reach acceptance with the host-role table absent, and construct-v1's named face pins HEq o.Dom Int and HEq o.domRepr (intArgDomRepr env.carrier), an Int-representation face, with constructNamedFace fixing host = emptyHost so neither the role table nor the arithParams.carrier pin of section 4.3 constrains it. A reimplementation that applies the three-state binding uniformly would admit a constructor claim whose representation face is stated over CarrierSpec 0 in a module that provably has no carrier struct there. The two mechanisms are complementary: section 4.3's pin stops a role-citing family from wiring an Int runtime the type section does not corroborate, and this scoping stops a role-free but carrier-sensitive family from reaching the reserved index.

The producer states these equalities as example : ... := rfl lines per export in Plans.lean, and the acceptance predicates in AcceptedArtifactCore.lean / ExprFragmentAccepted.lean aggregate the same equalities into the accepted-artifact proof — the examples are redundant audit surface, so deleting one (or serializing plans somewhere else entirely, section 2.2) cannot weaken acceptance. A conforming verifier MUST NOT substitute an out-of-kernel (e.g. Rust-side) reimplementation of any of these four steps on its acceptance path.

One name-binding subtlety in step 4: a claim carries both a display name (exportName : String, equated with obligation.export_) and the byte-level lookup key (exportNameBytes : List Nat), and no in-kernel equality relates the string to its byte encoding. What closes the gap is whole-module accounting (section 5.3): the binding forces obligation.self to the function index found under exportNameBytes, and exportsAccounted requires the UTF-8 encoding of obligation.export_ to be an actual export of that same function index. With aliased exports a claim can therefore bind through one name while reporting the other — but both names provably export the same certified function.

7. Byte binding

Three mechanisms bind the certificate to one exact artifact:

Hash pinning. The verifier MUST read the caller-supplied .wasm, compute its SHA-256, and reject unless it equals wasm_sha256. The witness pins manifest.subject.artifactHash to the recomputed hash string, and Schema.Holds conjoins artifactHash = CertModule.wasmSha256, so the JSON envelope, the Lean manifest, the packaged Module.lean, and the actual bytes must all agree.

ArtifactBytes injection. The verifier MUST generate ArtifactBytes.lean itself from the bytes it read — the package has no opportunity to supply a different numeral. The encoding is a single little-endian natural: modBytes = Σ bytes[i] · 256^i (rendered as one hex numeral with the byte sequence reversed), plus the explicit modLen = <byte count>. The length is soundness-relevant because trailing 0x00 bytes are not represented in the numeral. Every in-kernel decode (CertDecode, WasmSlice) reads from this pair using shift/mask arithmetic; the witness pins Artifact.data.modBytes / Artifact.data.modLen to the checker-generated module's values, so the packaged claim data provably talks about the injected bytes.

Wall identity. format.wall_id names the exact audited Lean source set (plus toolchain) the proof must elaborate against, per section 1. The verifier materializes the embedded wall sources into the build directory itself; packaged files with wall-source names are ignored. Changing any audited wall source or the toolchain pin changes the identity, and a certificate naming an unknown identity MUST be rejected.

8. The checker witness, the axiom whitelist, and the fail-closed guard

After the package builds, the verifier authors CheckerWitness.lean — never accepted from the package — containing, in order: rfl pins equating Artifact.data.modBytes/modLen/manifest with the checker-generated ArtifactBytes values and AverCert.manifest; rfl pins of every kernel-pinned manifest field of section 4 (artifactHash to the recomputed hash, artifactRoot, obligation export names, subject.exports, StandardFace.reportEntries to the exact (name, class) pair list, policies, termination witnesses, contracts, declaredUncertified, capabilities, start, hostRoleTable — rendered as none or some {box, add, mul, sub, toIndex} mirroring the JSON — stringHostRoles, profile, abi); the theorem AverCertChecker.checked : AverCert.AcceptedArtifact.accepted AverCert.Artifact.data := AverCert.Artifact.certificate, which forces the packaged root to exist at exactly the accepted type; and finally the axiom guard.

The axiom guard is a checker-authored run_cmd that collects the axiom closure of AverCertChecker.checked via Lean.collectAxioms and throws unless every axiom is in the whitelist [propext, Classical.choice, Quot.sound]. Matching is exact: fully qualified, case-sensitive Lean.Name equality with subset semantics — no prefix or namespace matching. The guard is fail-closed by construction: it runs at elaboration of the witness, any thrown error fails the build, and a failed build is a rejected certificate. The package cannot carry a competing or defanged guard because run_cmd is one of the twenty substrings the staging scan of section 9 rejects. That scan is an enumerated blacklist, not a semantic ban on every elaboration-executing construct — commands outside the list pass (the producer itself emits #print axioms) — so the soundness story rests on this checker-authored guard plus kernel acceptance, with the scan as a hardening layer. Two placement facts matter: the witness is authored after any cache restore and is never cached, so the guard runs on every verify and check invocation; and the stage-10 fresh replay re-checks every term in the import closure but does not itself enforce any axiom policy, so the guard's location in the always-fresh witness is load-bearing, not redundant. A conforming verifier MUST enforce the same whitelist on the axiom closure of the accepted root and MUST treat any additional axiom — including sorryAx — as rejection.

9. The verification pipeline

A conforming verifier MUST execute the following stages in order and MUST reject (nonzero exit, no CERTIFIED output) on the first failure. Stage numbers reference the reference implementation in aver-cert/src/verifier.rs. (For the one place the reference explain mode deviates from the no-CERTIFIED-output-on-failure requirement, see the known gap in stage 11.)

1. Wasm validity gate. Read the artifact bytes and run a complete standard WebAssembly validator over them (wasmparser::Validator::validate_all in the reference). This is the one retained Rust semantic gate: the Lean wall decodes every trust-bearing section and instruction it consumes, but it is not a complete Wasm validation algorithm (stack/control typing included), so artifact acceptance is only stated over validator-accepted modules. Known gap: the reference constructs wasmparser::Validator::new() with that crate's default feature set (pinned at wasmparser 0.248); the exact set of enabled Wasm proposals is inherited from the dependency version rather than declared normatively, which cross-vendor agreement will eventually require.
2. Manifest parse and envelope checks. Compute SHA-256 of the bytes; parse cert-manifest.json strictly; require schema_version = 3, wasm_sha256 equal to the recomputed hash, format.version = 1, format.wall_id resolving to an embedded wall, and artifact_certificate_root = "AverCert.Artifact.certificate"; then parse the candidate fields of section 4 with the exact-object and policy/termination coupling rules and the printable-ASCII candidate gate.
3. Build-directory assembly. Create a fresh private build directory (mode 0700 on Unix, under a checker-selected temp root).
4. Staging of package data. For each regular file directly in the cert directory (non-files are skipped): ignore it unless its name ends in .lean; silently skip checker-owned names (ArtifactBytes.lean, lakefile.lean, CheckerWitness.lean, and every wall source name). Then walk subdirectories recursively, skipping every dot-directory (.lake, .git) outright at every depth — a shipped build cache can never join the staged tree — and rejecting nesting deeper than 16 directory levels (the package is the one tree whose recursion depth an untrusted party chooses). A nested .lean file found by the walk first passes the stage-5 name and shadow gates, and is then staged at its relative path exactly when the already-staged top-level Manifest.lean or Certificate.lean contains an import line for its dotted module name (Apps/Notepad/Store.lean requires import Apps.Notepad.Store); the import lines are collected from the exact bytes staged, never from a second read. The scan for those lines is LITERAL and normative: each line is trimmed, a leading import prefix is stripped, and the trimmed remainder is the admitted module name — Lean comments are NOT parsed, so a line beginning with import inside a block comment still admits a file, and a conforming reimplementation MUST match this scan exactly, or its build set diverges. The admission list is a one-level check with no transitive closure (the producer imports every model root from Manifest.lean, section 2.1), and because it is authored by the untrusted producer it is build-set minimization — it keeps decoy trees and sidecars out of the build — NOT a security boundary: what protects the verdict is that every staged file passes the stage-5/6 gates and that acceptance rests on the checker-authored witness and axiom guard of section 8. Nested files stage in sorted relative-path order, and staging any two paths (flat or nested) that are equal ASCII-case-insensitively is rejected outright — on a case-insensitive staging filesystem the two writes would silently merge into one nondeterministically-chosen file. A nested .lean file whose dotted name is not imported is ignored outright and never staged, scanned, or built.
5. Name sanitation and shadow rejection. A flat file name MUST match ^[A-Za-z][A-Za-z0-9_]*\.lean$; for a nested file the same rule applies to every /-separated path segment (the .lean suffix on the last), and the dotted module root is the .-join of the segments. The per-segment rule is simultaneously the traversal guard (no . inside a segment, no .., no empty or absolute components — every accepted segment is a plain Normal path component) and the lakefile-injection guard (roots are interpolated into the checker-authored lakefile unescaped, so only validated segments may become roots). Reject any root whose dotted name — or any dotted prefix of it — case-insensitively collides with a toolchain root (Init, Lake, Lean, Std), a wall source root, or ArtifactBytes/CheckerWitness/lakefile. Additionally reject any two staged paths (flat or nested) that are equal ASCII-case-insensitively — stage 4 states the rationale. Known gap: stage 4's .lean suffix test is case-sensitive, so a file with an uppercase extension (ArtifactBytes.LEAN) is silently ignored there rather than rejected here.
6. Elaboration-code scan. Reject any staged file whose text contains any of the twenty tokens #eval, run_cmd, run_elab, run_tac, initialize, builtin_initialize, macro, macro_rules, elab, elab_rules, syntax, notation, unsafe, implemented_by, extern, deriving, attribute, @[, «, open Lean. The check is a plain case-sensitive substring scan over the whole file after lossy UTF-8 decoding — comments included — and within its enumeration it is deliberately overbroad: package Lean files are data and definitions only. Its guarantee is exactly this list of twenty substrings and nothing broader; it does not establish that every elaboration-executing construct is banned (#print axioms, which the producer itself emits, passes). The sound backstop is the checker-authored axiom guard and kernel acceptance (section 8); this scan is hardening.
7. Checker-owned materialization. Write the embedded wall sources, the generated ArtifactBytes.lean (section 7), a checker-authored lakefile.lean whose roots are the sorted, deduplicated union of the staged package roots, the wall source roots, and ArtifactBytes, and the pinned lean-toolchain.
8. Hermetic Lean build. Run lake build through the pinned toolchain: the canonical Elan installation (ELAN_HOME or ~/.elan) is the single bootstrap trust anchor, invoked by absolute path as elan run --install <pinned-toolchain> lake ... with a cleared environment (no inherited LEAN_PATH/LEAN_SRC_PATH/ELAN_TOOLCHAIN/PATH/HOME), implicit Lake artifact caches disabled, and TMPDIR/TMP/TEMP redirected into a checker-owned directory. Every Lean toolchain subprocess — this build, the witness elaboration of stage 9, the kernel replay of stage 10, and the optional prelude-cache build — runs under a per-step wall-clock limit (15 minutes by default; AVER_CERT_PHASE_TIMEOUT_SECS replaces it, capped at one day), and on expiry the step's entire process tree is killed. For the mandatory steps a timeout is fail-closed — the certificate is declined — with one documented exception: a timeout of the opt-in prelude-cache build is downgraded to a loud warning and a cache miss, never an acceptance failure, because the mandatory proof build that follows re-does the same work under its own limit. Build caches are opt-in only and are trusted local state; a cache-assisted build that fails is retried once from clean before rejecting. The data cache (AVER_CERT_DATA_CACHE) is keyed on a SHA-256 over a cache-layout version, the schema version, the pinned artifact hash, the wall id, the toolchain version, and the /-normalized relative name and contents of every freshly staged build-directory file, walked recursively (nested model files included; dot-directories skipped; CheckerWitness.lean excluded) — a reimplementation keying only on schema/hash/wall/toolchain, or only on top-level files, could wrongly reuse stale .olean data after a package edit that leaves those pins untouched. AVER_CERT_PRELUDE_CACHE separately caches the artifact-independent wall prefix.
9. Witness elaboration. Author CheckerWitness.lean (section 8) and elaborate it (lake env lean -o ... CheckerWitness.lean). This runs on every invocation, outside any cache, so the manifest pins and the axiom guard can never be replayed from stale build products. Failure MUST be reported as the certificate not binding to this artifact.
10. Fresh whole-closure kernel replay (verify, explain, and inspect). Run lake env leanchecker --fresh CheckerWitness: the pinned toolchain's leanchecker re-checks the witness module and its entire import closure in a fresh declaration environment, so nothing is inherited from the elaboration environment of stage 9. The developer preflight check is the only mode that omits this stage; it trusts the freshly built or explicitly cached .olean closure and MUST report CHECKED, never CERTIFIED. check MUST NOT be used as a release or admission gate — note this is a requirement on consumers, not something the process status enforces: a successful check still exits zero.
11. Verdict mapping. Any failure above → nonzero exit with a mode-specific prefix: verify prints DECLINED with a reason, check prints CHECK FAILED, and explain/inspect print error:. Zero certified exports with everything passing → the admission-only verdict, a nonzero exit — a package that proves nothing about any export MUST NOT exit successfully, even though its whole-module accounting held — under a mode-specific banner: NO CERTIFIED EXPORTS (admission only, no behavioral claims) for verify, NO CHECKED EXPORTS (developer preflight only, no behavioral claims) for check, NO CERTIFIED EXPORTS for explain/inspect. Otherwise → CERTIFIED, exit zero, printing the artifact path, export count, level (L1 / L3 / mixed L1/L3 computed from the pinned policies), and one line per export containing only kernel-pinned facts: name, policy, and the class label mapped from the pinned reportEntries. The verdict IS the exit code. explain/inspect run the same strict check as verify and additionally print declared-only values under explicit labels. Known gap: after its strict check succeeds, the reference explain prints the positive report and only then performs a second read of cert-manifest.json for the informational source_level_only list; if that second read fails (concurrent deletion or mutation, I/O error), the process exits nonzero after positive output was already printed, and the declined list can come from a different manifest snapshot than the one verified. A reimplementation SHOULD reuse the manifest bytes it already verified.

10. Trust inventory

A CERTIFIED verdict is exactly as strong as the components below. They are listed individually rather than rounded down to "the Lean kernel", because several of them sit on the adversarial input path and are not themselves kernel-checked; a defect in any trusted item could admit a wrong certificate.

What a positive verdict does not trust:

• The Aver compiler and its certificate producer. The classifier, disassembler, rederiver, and Lean renderer in aver-cert's producer feature are diagnostics for emission; none of them is linked into or re-run on the verifier's acceptance path. A verifier reimplementation needs none of that code, and a wrong producer yields a declined certificate, not a wrong verdict.
• Manifest prose. Everything declared-only in section 4 — dom/cod strings, level, theorem, wasm, carrier_type_index, source_level_only, and every human-readable reason string — can lie without affecting the verdict, and MUST be presented as declarations, not findings. (The declaredUncertified reasons are equality-pinned as transported data, but their semantic truth is unvalidated — section 4.1.)
• Any Rust-side reconstruction of the claim. The reference verifier performs no parallel verdict computation: it does not disassemble the module, reconstruct obligations, or compare classifications. Rust owns transport and process orchestration; the facts come from the kernel. The JSON's certified list is a set of candidates with no authority until the checker witness pins it.
• Package-supplied build infrastructure. Wall sources, lakefile, toolchain pin, artifact bytes, and witness are checker-owned; packaged files with those names are ignored or rejected.
• Caches as evidence. Package-supplied caches and build products are ignored entirely, and opt-in local caches accelerate the build but cannot skip the witness elaboration or the fresh replay (their residual trust as local state is the last item below).
• Diagnostics. A diagnostic can explain a decline; it cannot upgrade one.

What a positive verdict does trust — the honest TCB:

• The Lean kernel and toolchain (pinned Lean 4.32 elaborator, kernel, Lake, and leanchecker), resolved through the local Elan installation as bootstrap trust anchor. leanchecker --fresh is a fresh-environment replay from the same distribution, not an independently implemented second kernel; the architecture MUST NOT be described as having two diverse kernels. The verifier pins the toolchain name, not the toolchain binaries' hashes: on first use Elan downloads and installs the pin, so the Elan installation and its acquisition channel are part of this trust anchor.
• The embedded wall sources — the statement schema, decoders, checkers, lowerers, faces, axes, and soundness/discharge theorems of sections 5–6 are audited Lean code; their identity is what wall_id pins. The schema of claims is part of the TCB: a certificate is only as meaningful as Obligation.holds/holdsTotal and the acceptance conjuncts, and auditing those definitions is exactly what the wall identity makes stable.
• The wall's Wasm model, as a model of real engines. The kernel proves the wall's instruction semantics, decoders, and canonical lowerings coherent with each other and binds them to the exact artifact bytes, but it cannot prove that the model is faithful to what real WebAssembly engines execute. That faithfulness is an assumption of the scheme, held empirically by differential testing rather than by proof: tests/cert_decode_spec.rs checks the in-kernel decoder term-for-term against an independent Python byte oracle (tools/certkit/decode_ref.py) and the Rust rederivation, plus byte-mutation and opcode-coverage suites, and the cross-backend execution differentials (tests/cross_backend_proptest.rs, tests/cross_backend_stress.rs, tests/wasm_gc_carrier_i64_differential.rs, tests/bigint_literals_differential.rs, tests/wasm_gc_perslot_int_unboxing_differential.rs) require exact agreement between the emitter output under a real engine and the VM reference semantics. Those execution suites currently exercise one production engine — the Wasmtime runtime embedded in the compiler's --wasm-gc run path; agreement with other engines is not yet pinned by a named suite.
• The Rust transport harness — file reading, hashing, JSON envelope checks, staging gates, hermetic process construction, the per-step subprocess timeouts of stage 8, and verdict mapping (verifier.rs, wall.rs, lean_process.rs, format.rs, main.rs). The harness performs no parallel verdict reconstruction, but a bug in any of these transport duties is a bug inside the TCB.
• wasmparser for full WebAssembly validity (stage 1 rationale): the input is attacker-chosen and the Lean wall does not subsume this check, so it sits on the adversarial path.
• SHA-256 collision resistance, for both the artifact hash and the wall identity — the two bindings that make a certificate non-transferable. An adversary who can produce SHA-256 collisions can transplant a certificate onto different bytes or a different wall.
• The named runtime contracts — the L1 theorems are conditional on the host helpers obeying the disclosed laws, and the L3 theorems additionally on the disclosed totality; proving the shipped runtime satisfies them is a per-toolchain-release obligation outside the certificate.
• Explicit source read declarations — user-ADT domain meaning, representation interpretation, and non-reconstructible models (section 5.1) are conditions of the theorem, not derived facts.
• Explicitly configured cache directories, if any, as trusted local state: their integrity manifests detect accidental corruption, not an active writer able to replace .olean outputs and Lake traces together.

11. Versioning and freeze policy

Section 1 defines the three acceptance identities and their exact-match rule; this section states how they evolve. All three live in aver-cert/src/format.rs (FORMAT_VERSION, CERT_SCHEMA_VERSION, CURRENT_WALL_ID); the aver-cert crate's own 0.1.x release version is a package-manager label, not an acceptance identity — none of the three checks reads it.

What changes bump which identity:

• Package layout changes — adding, removing, or restructuring package files or the envelope container — bump FORMAT_VERSION. The version check is exact-match, not a floor, so a bump orphans every previously issued package; a pure acceptance widening that leaves every previously verifiable package verifying identically does not bump. The worked example is nested model staging (section 9, stage 4): flat packages stage byte-for-byte as before under version 1, packages with nested model files never verified under any earlier checker, and an earlier checker declines them fail-closed at the Lean build (the dotted import cannot resolve) rather than mis-verifying them.
• Statement schema changes — any change to what a certificate can state or how it states it — bump CERT_SCHEMA_VERSION. The 1 → 2 bump is the worked example: schema 2 made the subject's hostRoleTable optional, with null pinned against the byte-derived helper-absence proof of section 4.3. The 2 → 3 bump added the required toIndex key to the object form of that table for the fused vector-read face; under exact-object matching the new key is not an additive extension, so it bumped the version.
• Wall source or toolchain changes change the computed wall identity, but the advertised identity does not update automatically: CURRENT_WALL_ID is a hand-maintained constant, and a release with changed wall sources requires a manual bump. The safety net is the recompute-and-assert of section 1 — the verifier recomputes the identity over its own embedded sources on first use and aborts on disagreement with the constant — so a source change without a bump is caught at runtime as a fail-closed wall-identity mismatch rather than shipping a wall under a stale name; still, "caught at runtime, fail-closed" is weaker than "automatic", and moving the recomputation to build time so a stale constant cannot ship at all is a known hardening candidate. A proof-only hardening of a wall predicate changes the wall identity without touching either version number. The coupling is one-way: a statement-schema change also changes the wall identity, because the schema types are themselves wall sources (Schema.lean, SchemaCore.lean), but most wall-identity changes are not schema bumps.

Certificate lifetime and re-certification. A certificate does not expire by time. It verifies exactly against a verifier that embeds the wall it names, and each aver-cert release currently embeds exactly one wall (the section 1 wall-registry box records the open grace-window question). The lifecycle at a wall change is: a new verifier release ships a changed wall under a new CURRENT_WALL_ID; that verifier rejects every previously issued package at the envelope gate as an unknown wall — fail-closed, before any Lean step runs; the holder re-certifies by re-running aver compile --certify with the compiler release paired to the new verifier. Because --certify binds the emitter's exact bytes, re-certification generally re-emits the module, and the new certificate is a statement about the new bytes; verifying the re-issued package still requires no trust in the compiler. An old verifier binary that is kept around continues to verify the packages of its era — its embedded wall never changes — but that is a preservation assumption on the relying party, not a guarantee of the scheme: archival verification of a historical artifact/package pair means preserving the matching verifier release, an Elan installation that can still resolve its pinned toolchain, and a platform that runs both.

OPEN DECISION — wall and schema freeze criterion. Neither FORMAT_VERSION = 1 nor CERT_SCHEMA_VERSION = 3 is declared frozen (section 1), and the wall currently changes at the tempo of ordinary software development: predicate hardenings change the wall identity, and each such change ends the forward-verifiable life of previously issued certificates. "Audit the wall once" only becomes real once the wall has the tempo of a standard, so a freeze needs an explicit criterion. The proposal on the table — a maintainer decision, deliberately not adopted by this document — is to declare a freeze candidate only after all three hold: (a) module framing and validation move into the kernel-checked wall, so wasmparser leaves the adversarial input path (section 10); (b) the wall build gains a mechanical pin-completeness check, so that every subject-visible fact must be pinned as an equality against the byte-derived decoder for the wall to build at all; and (c) N consecutive months pass with no soundness-motivated change to any wall source or to the statement schema, with N fixed when the criterion is adopted. Until a freeze is declared, relying parties should expect the wall identity to move between releases and plan for the re-certification path above.

12. Appendix: section-to-source traceability

Section	Authoritative sources (repository paths)
1 Versioning, wall identity	aver-cert/src/format.rs (FORMAT_VERSION, CERT_SCHEMA_VERSION, CURRENT_WALL_ID — the inline identity value, ARTIFACT_CERTIFICATE_ROOT), aver-cert/src/wall.rs (compute_id, current_id, resolve, SOURCES, LEAN_TOOLCHAIN — the include_str! embedding that preserves the trailing newline), aver-cert/assets/wall/current/lean-toolchain (ends in a newline byte)
2.1 Producer layout convention	aver-cert/src/engine/render_project.rs (write_project, sanitize_model_for_cert, render_artifact_certificate — the emitted #print axioms, render_artifact_soundness), aver-cert/src/engine/render_manifest.rs (render_final), src/main/commands.rs (certify entry, model emission reuse), tests/cert_certify_spec.rs
2.2 Acceptance file-set contract	aver-cert/src/verifier.rs (assemble_build — staging loop, is_checker_owned, lean_module_root, checker_witness — the witness import list), aver-cert/assets/wall/current/Schema.lean (Holds — the only wall reference to CertModule), aver-cert/assets/wall/current/AcceptedArtifactCore.lean (family predicates binding obligation.code, not named definitions)
3, 4 Manifest schema, pinned vs declared	aver-cert/src/verifier.rs (trusted_check, read_candidates — the exhaustive list of fields read on the acceptance path, parse_termination, exact_object_fields, gate_candidate, checker_witness — the profile/abi rfl pins with no fixed-identifier comparison, report_face, manifest_face, explain — the second manifest read and zero-export early return), aver-cert/src/engine/mod.rs (PROFILE_ID, RUNTIME_ABI — producer-only constants, CERT_LEVEL, contract strings), aver-cert/src/engine/render_manifest.rs (render_manifest, render_manifest_lean), aver-cert/assets/wall/current/ClaimAxes.lean (ContractUse.contracts — the canonical contract order, contractsMatch — exact list equality), aver-cert/assets/wall/current/AcceptedArtifactCore.lean (exportsAccounted, declaredUncertifiedNames — names-only byte accounting, decodedStringHostRoles), tests/snapshots/cert_certify_spec__add_one_certificate_package.snap (worked example)
4.3 Three-state host-role decode	aver-cert/assets/wall/current/CertDecode.lean (decodeRawExports, functionExports, decodeExports — function-export projection, AddSub.boxIdx, AddSub.toIndexIdx, AddSub.Roles, AddSub.carrierHelperAbsent — the exact pinned fact, carrierState — the carrier struct a declared table must name, StringHost.classify/StringHost.roleTable — defined-function order with duplicates retained), aver-cert/assets/wall/current/ArithTemplateDerisk.lean (ArithRole, ArithHostParams, checkArithHostParams — the LEB regime, s33, boxTemplateBody/toIndexTemplateBody/addTemplateBody/subTemplateBody/mulTemplateBody, arithHelperBody — the role-to-bytes dispatch), aver-cert/assets/wall/current/AcceptedArtifactCore.lean (bodyBytesAtFuncIndex, arithRoleCheck, arithTableCheck, decodedHostRoleTable, decodedStringHostRoles), aver-cert/assets/wall/current/SchemaCore.lean (Subject, Subject.hostRoles)
5 Obligations, policies, acceptance	aver-cert/assets/wall/current/SchemaCore.lean (Obligation, holds, holdsTotal, HoldsCore, Policy, TotalityRole, TerminationWitness, checkTerm, checkTermMutual, CAPABILITY_REGISTRY), aver-cert/assets/wall/current/Schema.lean (Holds), aver-cert/assets/wall/current/AcceptedArtifact.lean (accepted), aver-cert/assets/wall/current/AcceptedArtifactCore.lean (ArtifactData, claimsMatchManifest — plan-pair vs export-name-list equalities per family, claimObligationExports, exportsAccounted, coverage/accounting/closure defs), aver-cert/assets/wall/current/StandardFace.lean (checkedFaces, reportEntries, hostTableBound), aver-cert/assets/wall/current/ClaimAxes.lean (checked, canonicalTermination)
6 Plan grammar, byte-lowering contract	aver-cert/assets/wall/current/SchemaCore.lean (all raw-plan types and node grammars), aver-cert/assets/wall/current/PlanCheck.lean (checkers, encodeSymRawPlanToExprFragmentRawPlan and encodeSymBlockFuel — the generic bridge and its fail-closed node cases, hostRoleIdx?/structTyIdx? — byte-derived index provenance, stringEqPlanMatchesSymRawPlan, stringConcatPlanMatchesSymRawPlan, constructPlanMatchesSymRawPlan — the non-encoded family bridges, classifyRecursionPlanShape — self-call pinned to the current function, checkMutualPlanShape/recStepMutual — tail-call target pinned to the SCC member set, profile strings), aver-cert/assets/wall/current/PlanLower.lean, aver-cert/assets/wall/current/PlanBytes.lean (ULEB/SLEB, lower*CodeEntry, singleCarrierLocalBodyBytes/noLocalBodyBytes/carrierLocalsBodyBytes — the carrier-state-selected locals prelude), aver-cert/assets/wall/current/CertDecode.lean (carrierState — the strict three-state carrier decode), aver-cert/assets/wall/current/WasmSlice.lean (FuncBinding, exactFuncBindingForExport, type matchers, checkHostRoleFuncType/hostRoleFuncTypeMatches/hostTableFuncTypesMatch — the host-table declared-function-type pin, checkExprProjectionTypes/checkTagDispatchTypes — the face-layout arity pins, closure scanner), aver-cert/assets/wall/current/AcceptedArtifactCore.lean (family *PlanAccepted predicates — separate exportName/exportNameBytes fields, stringConcatNLocals, decodedCarrierIndex/decodedCarrierFreeClaims — the String.concat-only three-state binding, decodedStrictCarrierIndex/decodedObligationFacts — the strict binding every other non-expression-fragment family keeps; the expression-fragment family is bound by neither and carries symFragmentCarrierBound/symFragmentCarrierBindingRequired/fragPlanMentionsIntCarrier instead, see ExprFragmentAccepted.lean), aver-cert/src/engine/render_project.rs (render_expr_fragment_plans — the emitted rfl surface)
7 Byte binding	aver-cert/src/verifier.rs (hash checks, assemble_build), aver-cert/src/wall.rs (render_artifact_bytes), aver-cert/src/engine/render_project.rs (render_artifact_bytes_lean, byte-numeral comments), aver-cert/assets/wall/current/WasmSlice.lean (byte-cursor model)
8 Witness and axiom guard	aver-cert/src/verifier.rs (checker_witness — witness text, guard run_cmd, exact Lean.Name matching, AXIOM_WHITELIST, CHECKED_ROOT, CODE_EXEC_TOKENS, scan_for_code_exec), aver-cert/src/engine/render_project.rs (render_artifact_certificate — the producer-emitted #print axioms that the scan admits)
9 Pipeline	aver-cert/src/verifier.rs (verify, check, explain — all three replay modes, kernel_replay_args, trusted_check — the wasmparser validator gate, staging and scan functions, CODE_EXEC_TOKENS, FRESH_REPLAY_ARGS), aver-cert/src/lean_process.rs (hermetic subprocess boundary, per-step wall-clock limit — DEFAULT_PHASE_TIMEOUT, run_with_timeout), aver-cert/src/cache.rs (artifact_cache_key, staged_source_files — the full cache-key material), aver-cert/src/prelude_cache.rs (opt-in wall-prefix cache; the non-fatal-but-loud timeout downgrade), aver-cert/src/main.rs (Route, per-mode verdict/exit mapping and banners), aver-cert/Cargo.toml (wasmparser version pin), src/main/cli.rs (aver cert subcommands)
10 Trust inventory	aver-cert/src/verifier.rs (module header, validator comment), docs/certification.md, docs/certification-architecture.md, aver-cert/src/format.rs (WASM_GC_CAPABILITIES), aver-cert/src/lean_process.rs (trust anchor and environment tests), tests/cert_decode_spec.rs + tools/certkit/decode_ref.py and the cross-backend differential suites named in section 10 (model-faithfulness evidence)
11 Versioning, lifetime, freeze	aver-cert/src/format.rs (FORMAT_VERSION, CERT_SCHEMA_VERSION, CURRENT_WALL_ID — the hand-maintained constant), aver-cert/src/wall.rs (current_id — the recompute-and-assert safety net, resolve — single embedded wall), aver-cert/src/verifier.rs (the unknown-wall envelope rejection)