29. External Kernels🔗

Lean is both a proof assistant with powerful automation and an extensible, full-featured programming language. However, all theorems that can be proved in Lean are translated by the elaborator to a much smaller core type theory. The Lean kernel is a small, robust checker for this core theory.

As described in the chapter on validating Lean proofs, Lean is designed so that its core theory can also be checked by independently implemented kernels. This provides an extra layer of assurance.

Lean distributions include the following independently implemented kernels:

Nanoda (nanoda_bin): An implementation of the Lean kernel in Rust by Chris Bailey (source).
lean4lean: A port of the official kernel to Lean by Mario Carneiro (source). Significant parts of it are formally verified against a specification of Lean's type theory.
con-leche: An implementation of the Lean kernel in Lean by the Lean FRO (source). It includes a machine-checked proof that every environment it accepts has a model in set theory, so it never accepts a proof of False.
con-ron: A port of con-leche to Rust by the Lean FRO (source).

Kernels do not need to be able to call any particular external API or use any particular data structures. They are provided with a newline-delimited JSON file that contains all the terms and definitions to be checked.

29.1. Lean Export Format🔗

This section describes version 3.1.0 of the export format. The export is newline-delimited JSON: there is one object per line, and objects do not themselves contain newline characters. An exported .ndjson file will begin with an initial metadata object which includes version info for the exporter, Lean, and export format:

Initial metadata object

{
  "meta": {
    "exporter": {
      "name": string,
      "version": string
    },
    "lean": {
      "githash": string,
      "version": string
    },
    "format": {
      "version": string
    }
  }
}

The metadata object is followed by a sequence of primitives with integer tags (Name, Level, or Expr) and declarations (axiom, definition, theorem, opaque, quot, inductive including constructor and recursor), where related elements of an inductive or mutual inductive declaration (the inductive specifications, constructors, and recursors) are grouped together.

The export format contains information that is redundant and would likely be ignored or only validated by a full external checker (such as the types of recursors). These are included for the benefit of other tools that want all constants with their types (e.g. dependency analysis tools).

The construction of these elements is as described below. Line breaks are included for readability; note that the NDJSON format requires these JSON objects to be rendered without any line breaks.

29.1.1. Indices🔗

The export format uses explicit indices to refer to names, levels, and expressions. Each kind of object occupies its own table, and indices may be reused between tables. Within a table, each index is unique. The spec uses the following types to describe natural numbers that refer to entries in the table:

NameIdx: An index into the name table, bound by "in". Index 0 refers to the anonymous name and is predefined.
LevelIdx: An index into the level table, bound by "il". Index 0 refers to level 0 and is predefined.
ExprIdx: An index into the expression table, bound by "ie". There are no predefined values.
NameIdxDef: A NameIdx defined by this line
LevelIdxDef: A LevelIdx defined by this line
ExprIdxDef: A ExprIdx defined by this line

If an index is defined more than once, the kernel should reject the code. Every definition of an index must precede all uses; if an undefined index is encountered, the kernel should reject the code.

Other integer fields represent integer values. They may be de Bruijn indices ("bvar"), numeric name components ("i"), field indices ("idx"), definition heights ("regular"), constructor positions ("cidx"), or counts ("numParams", "numIndices", "numNested", "numFields", "numMotives", "numMinors", "nfields"). Natural number literals are encoded as JSON string literals instead of JSON numbers to reduce the risk of parsers truncating values at limits such as 2^{53}.

29.1.2. Names🔗

Names have two formats that correspond to the constructors of Lean.Name. Index 0 is predefined to refer to Lean.Name.anonymous.

Name.str

{
  "str": {
    "pre": NameIdx,
    "str": string
  },
  "in": NameIdxDef
}

Name.num

{
  "num": {
    "pre": NameIdx,
    "i": integer
  },
  "in": NameIdxDef
}

29.1.3. Levels🔗

Universe levels have four formats that correspond to the constructors of Lean.Level. Index 0 is predefined to refer to Lean.Level.zero and is not otherwise represented.

Level.succ

{
  "succ": LevelIdx,
  "il": LevelIdxDef
}

Level.max

{
  "max": [LevelIdx, LevelIdx],
  "il": LevelIdxDef
}

Level.imax

{
  "imax": [LevelIdx, LevelIdx],
  "il": LevelIdxDef
}

Level.param

{
  "param": NameIdx,
  "il": LevelIdxDef
}

29.1.4. Expressions🔗

Each constructor of Lean.Expr that may occur in elaborated code has a corresponding JSON representation. Free variables and metavariables do not appear in the export. There are no predefined expressions.

Expr.bvar

{
  "bvar": integer,
  "ie": ExprIdxDef
}

Expr.sort

{
  "sort": LevelIdx,
  "ie": ExprIdxDef
}

Expr.const

{
  "const": {
    "name": NameIdx,
    "us": Array<LevelIdx>
  },
  "ie": ExprIdxDef
}

Expr.app

{
  "app": {
    "fn": ExprIdx,
    "arg": ExprIdx
  },
  "ie": ExprIdxDef
}

Expr.lam

{
  "lam": {
    "name": NameIdx,
    "type": ExprIdx,
    "body": ExprIdx,
    "binderInfo": "default" | "implicit" | "strictImplicit" | "instImplicit"
  },
  "ie": ExprIdxDef
}

Expr.forallE

{
  "forallE": {
    "name": NameIdx,
    "type": ExprIdx,
    "body": ExprIdx,
    "binderInfo": "default" | "implicit" | "strictImplicit" | "instImplicit"
  },
  "ie": ExprIdxDef
}

Expr.letE

{
  "letE": {
    "name": NameIdx,
    "type": ExprIdx,
    "value": ExprIdx,
    "body": ExprIdx,
    "nondep": boolean
  },
  "ie": ExprIdxDef
}

Expr.proj

{
  "proj": {
    "typeName": NameIdx,
    "idx": integer,
    "struct": ExprIdx
  },
  "ie": ExprIdxDef
}

Expr.lit (Literal.natVal)

{
  "natVal": string,
  "ie": ExprIdxDef
}

Expr.lit (Literal.strVal)

{
  "strVal": string,
  "ie": ExprIdxDef
}

Expr.mdata

{
  "mdata": {
    "expr": ExprIdx,
    "data": object
  },
  "ie": ExprIdxDef
}

By default, metadata is stripped prior to export. The --export-mdata flag causes it to be included; when they are present, "data" is an object whose values are strings formatted by repr.

29.1.5. Declarations🔗

Each kind of declaration in the core type theory has a corresponding JSON representation. Sometimes, multiple kinds of Lean declarations elaborate to the same underlying representation; one example of this is structures and inductive types. In this case, there is only a single representation.

29.1.5.1. Axioms🔗

Axiom

{
  "axiom": {
    "name": NameIdx,
    "levelParams": Array<NameIdx>,
    "type": ExprIdx,
    "isUnsafe": boolean
  }
}

29.1.5.2. Definitions🔗

Definition

{
  "def": {
    "name": NameIdx,
    "levelParams": Array<NameIdx>,
    "type": ExprIdx,
    "value": ExprIdx,
    "hints": "opaque" | "abbrev" | {"regular": integer},
    "safety": "unsafe" | "safe" | "partial",
    "all": Array<NameIdx>
  }
}

29.1.5.3. Opaques🔗

Opaque

{
  "opaque": {
    "name": NameIdx,
    "levelParams": Array<NameIdx>,
    "type": ExprIdx,
    "value": ExprIdx,
    "isUnsafe": boolean,
    "all": Array<NameIdx>
  }
}

29.1.5.4. Theorems🔗

Theorem

{
  "thm": {
    "name": NameIdx,
    "levelParams": Array<NameIdx>,
    "type": ExprIdx,
    "value": ExprIdx,
    "all": Array<NameIdx>
  }
}

29.1.5.5. Quotients🔗

The official Lean kernel uses the fieldless constructor Lean.Declaration.quotDecl as the input to declare the quotient declarations. It then adds the four declarations that make up the quotient package to the environment. The export format includes the data of these generated declarations for convenience.

Quotient

{
  "quot": {
    "name": NameIdx,
    "levelParams": Array<NameIdx>,
    "type": ExprIdx,
    "kind": "type" | "ctor" | "lift" | "ind"
  }
}

29.1.5.6. Inductive Declaration:🔗

The official Lean kernel expects a Lean.Declaration.inductDecl, which contains a (mutual) group of inductive declarations with their constructors. From that the kernel derives the recursors and informational fields like isRec, isReflexive or cidx. The export format includes the data of these generated declarations for convenience. ι-reductions are specified by RecursorRule entries. Independent kernels may either trust the included derived recursor information or regenerate and check it for extra assurance.

Inductive Declaration

{
  "inductive": {
    "types": Array<InductiveVal>,
    "ctors": Array<ConstructorVal>,
    "recs": Array<RecursorVal>
  }
}

InductiveVal

{
  "name": NameIdx,
  "levelParams": Array<NameIdx>,
  "type": ExprIdx,
  "numParams": integer,
  "numIndices": integer,
  "all": Array<NameIdx>,
  "ctors": Array<NameIdx>,
  "numNested": integer,
  "isRec": boolean,
  "isUnsafe": boolean,
  "isReflexive": boolean
}

ConstructorVal

{
  "name": NameIdx,
  "levelParams": Array<NameIdx>,
  "type": ExprIdx,
  "induct": NameIdx,
  "cidx": integer,
  "numParams": integer,
  "numFields": integer,
  "isUnsafe": boolean
}

RecursorVal

{
  "name": NameIdx,
  "levelParams": Array<NameIdx>,
  "type": ExprIdx,
  "all": Array<NameIdx>,
  "numParams": integer,
  "numIndices": integer,
  "numMotives": integer,
  "numMinors": integer,
  "rules": Array<RecursorRule>,
  "k": boolean,
  "isUnsafe": boolean
}

RecursorRule

{
  "ctor": NameIdx,
  "nfields": integer,
  "rhs": ExprIdx
}