Lean Kernel Arena / logos-kernel

logos-kernel — the kernel core of LOGOS, a Lean 4 checker in Rust.

• Expressions live in a maximally shared, hash-consed DAG with de Bruijn indices: structural equality is one integer compare, and every cache is keyed on node identity. The export's own sharing is preserved exactly; nothing is expanded into a tree.
• Declarations are checked by evaluation into closures: β extends an environment, a binder is crossed by binding a fresh variable, and δ/ι wait in neutral values until conversion or inference asks for a weak head. Types are values too, and closures keep only the variables their body mentions.
• Conversion is Lean's algorithm: lazy δ by definitional height, proof irrelevance, η, structure η, unit-like types, K, quotients, Nat/String literals, with a complete decision procedure for universe level ≤/≡.
• Inductive families, nested ones included, are elaborated by the kernel itself; an export's recursors, rules and flags are admitted only if identical to what the kernel derives.
• The Nat literal fast paths (add … gcd, bitwise, shifts) and String literals are enabled only after the environment's definitions are validated in the manner of lean4lean, against reference terms elaborated by Lean itself.
• Rejections explain themselves on stderr: which declaration, which rule, which terms.