-
Notifications
You must be signed in to change notification settings - Fork 8
Home
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 evenmathlib4
- 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:
- Build a Lean 4 → Lurk compiler
- Implement a content-addressing routine for Lean 4 sources that is capable of outputting anonymized data (Yatima IR)
- 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
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.