Module reference 

The reference translator: a deliberately small, unoptimized reading of a Lean export’s declaration TYPES into kernel terms, sharing no code with the production reader’s conversion, sharing or caching machinery. It is the independent oracle a result’s statement is compared against (competition rule R8): a faulty production translation and a faulty emitter cannot agree with it by construction.

What it reads, and what it refuses

One pass over the NDJSON records builds three tables — names, levels, expressions — keeping each record as the JSON it arrived as. The requested declaration’s type is then translated by a plain post-order walk: sort, bvar, const, app, lam, forallE, letE, mdata (transparent), natVal and strVal. Nothing is shared, cached, reduced or checked here; the kernel decides what the resulting term means.

A strVal string literal is read as the constructor application the export’s own Lean release defines it to be, from the header’s meta.lean.version and nothing else: Lean 4.14.0, whose String is the structure String.mk (data : List Char), reads "ab" as String.mk [Char.ofNat 97, Char.ofNat 98]; Lean 4.29.1, 4.30.0 and 4.33.0, whose String is UTF-8 bytes, read it as String.ofList [Char.ofNat 97, Char.ofNat 98]. Under any other release a literal has no reference reading and is declined. Nothing about the export’s String is looked up or checked here; the kernel decides whether the reading is well-typed.

proj is refused as unsupported: the production reader lowers it through typed machinery (a projection needs its structure’s constructor telescope), and reproducing that machinery would make this oracle neither small nor independent. A statement that needs one is reported as having no reference translation, which is an explicit gap and never a pass.

The identity contract

Names are the export’s hierarchical names written component by component — /s:"T06_002"/s:"x" for a string component, /n:3 for a numeric one — and universe parameters are spelled the same way. The kernel’s primitive identities are the one place a Lean name is not its own spelling: Nat, Nat.zero and Nat.succ are the kernel’s Nat, Zero and Succ (every other Nat.x lives under Nat/), and Lean’s four quotient primitives are the kernel’s certified kernel.quot.* declarations. That table is the translation’s contract with the kernel, written out here in full rather than imported, so a change to it on either side is a visible disagreement.

Structs

Reference

An export read once, for reading many declarations from it.

ReferenceDeclaration

One declaration as the reference translator reads it.

Enums

ReferenceKind

What a Lean declaration record is, as far as the statement binding needs to know.

Constants

REFERENCE_NODE_BUDGET

The largest term (in tree nodes) the reference translation will build. Exports share subexpressions as a DAG; a tree unfolding is bounded so a hostile export cannot make the oracle allocate without limit.

Functions

kernel_name_of_components

The kernel spelling of a Lean name given as its hierarchical components.

reference_declaration

The whole reference reading of one declaration: kernel name, kind, universe parameters and type.

reference_type

The type of declaration as the reference translator reads it from export.