Home

Welcome to the yatima-lang wiki!

The end goal of this repository is to:

• Content-address every Lean 4 environment, declaration, expression and universe level via using the IPLD data format, with a name-irrelevant representation similar to the Unison language
• Independently evaluate and typecheck Lean 4 programs with a kernel implemented in Lean 4
• Compile Lean programs to the Lurk zk-SNARK language, so that we can generate zero-knowledge proof, which can be verified in constant-time and space, that a Lean program f, with input x, evaluates to y
• Compile the Yatima typechecker itself to Lurk, so we can generate zero-knowledge proofs that our Lean typechecker, with inputs env : Yatima.Environment and const : Yatima.Constant, returns successfully without error. For example, we can produce a cryptographic witness that some definition def foo : M := N correctly typechecks, which can be validated without re-running the typechecker.

This will enable us to produce a succinct and efficiently verifiable correctness certificate for e.g. Lean's mathematical library (and for each of its declarations) once it's ported to Lean 4, which currently takes over 4 hours to be typechecked by the Lean 3 kernel (as of May '22).

Execution plan

1. Since we want to build on top of Lean 4 source files, we can take advantage from the fact that its API becomes available for any Lean 4 code that does import Lean. Thus, we are creating an application in Lean 4 to make use of its Lean.Elab.runFrontend function, which can parse the source files and instantiate a Lean.Environment for us. Then with a Lean.Environment at hand, we can translate its declarations to our own content-addressed types and populate a Yatima.Store, our intermediate representation of Lean 4 objects

2. The objects in Yatima.Store are glued together via CID references, but we can convert them to raw types that use direct references that simplify and speed up the next steps

3. We're going to build a typechecker, that calls the converter mentioned in the previous item and then operates on the resulting (simplified) types

4. We're going to build a transpiler, which also calls the converter and then is able to output Lurk code

Finally, and this is where the pieces of the puzzle come together, we are going to compile our own typechecker and then transpile it to Lurk. That is, we're going to have a powerful typechecker written in Lurk that's capable of generating cryptographic certificates that the original Lean 4 code typechecks.

The four steps above are implemented in the following modules, respectively:

1. Yatima.Compiler
2. Yatima.Converter
3. Yatima.Typechecker
4. Yatima.Transpiler

Learning resources

• Created by the team

  • Inductive types in Lean 4
  • Universe levels in Lean 4
  • IPLD and CID
  • Zero knowledge proofs and zk-SNARKs
  • An example of content addressing Universes

• Official documentation

  • Lean 4
  • IPLD
  • Lurk

• Literature, books, repositories, videos, pages etc

  • Curry–Howard correspondence
  • A presentation about Lurk
  • Type-Directed Partial Evaluation
  • Checking Dependent Types with Normalization by Evaluation: A Tutorial
  • pi-forall