Home

Welcome to the Yatima Wiki!

Yatima is meant to ultimately produce Lurk proofs of typechecking for Lean 4 constants (definitions, theorems etc) by running a Lean 4 typechecker written in Lurk. Developing such a typechecker, however, is a tricky task and this Wiki aims to clarify how we are doing it.

Before we go over the details, let's enumerate some properties we want the Yatima stack to have:

• The typechecker implementation should be type-safe
• The typechecker should be efficiently testable over arbitrarily vast input that's already out there, such as Lean 4's Init lib or even mathlib4
• The proofs of typechecking should be name-irrelevant, so the names of variables, definitions, theorems, types, universes etc. shouldn't affect the resulting Lurk proofs
• Processed Lean 4 code should generate data that's efficiently shared via IPFS or other content-addressing network
• Previous computational efforts should be cached for future use

The general strategy to achieve these goals is:

1. Build a Lean 4 → Lurk compiler
2. Implement a content-addressing routine for Lean 4 sources that is capable of outputting anonymized data (Yatima IR)
3. Build a typechecker in Lean 4 that consumes Yatima IR

Then we're able to compile the typechecker from Lean 4 to Lurk. Feeding the typechecker in Lurk with the right data, however, is not trivial. So we will see how that's done later. But we can already cross-out the first goal since the typechecker is originally written in Lean 4, so type-safety is guaranteed (if we trust the compiler).

Each item mentioned in the strategy above corresponds to a module in the yatima repository, respectively

1. Yatima.CodeGen
2. Yatima.ContAddr
3. Yatima.Typechecker

Such modules are then tied together by the Yatima CLI, whose commands are mentioned in the README.

TODO: explain how the remaining goals are fulfilled.