Home

Welcome to the Yatima wiki!

Yatima is meant to ultimately produce Lurk proofs of typechecking for Lean 4 declarations (definitions, theorems etc) by running a Lean 4 typechecker written in Lurk. Developing such 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 mathlib
• 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
• Previous computational efforts should be cached for future use

The general strategy to achieve those goals is:

1. Build a Lean 4 → Lurk transpiler
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 can transpile the typechecker to Lurk. Feeding the typechecker in Lurk with the right data, however, becomes tricky. 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 transpiler). Now let's go deeper and explore the remaining goals.

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

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.