Skip to content

Home

Jump to bottom
Arthur Paulino edited this page May 23, 2022 · 32 revisions

Welcome to the yatima-lang wiki!

The end goal of this repository is to:

  • Independently evaluate and typecheck Lean 4 programs with a kernel implemented both in Rust and Lean 4
  • 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
  • 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 Lean.Environment for us.

  2. With a Lean.Environment at hand, we can translate its declarations to our own content-addressed "Yatima" types and populate a Yatima.Env

  3. The Yatima.Env can be printed to a .ya file, which then can be read by a typechecker. Up to this point, everything is done in Lean 4

  4. We can parse .ya files and typecheck them with our own kernels. We aim to build a kernel in Lean 4 and another one in Rust

  5. Typechecking can be implemented as Lurk programs, expected to be fast/cheap with the use of recursive zk-SNARKs

  6. If typechecking succeeds, we can upload the content-addressed environment to IPFS and generate a cryptographic certificate that the original Lean 4 code can be trusted

Content-addressing

We want our Lean 4 certificates to be "name-irrelevant". That is, the following should be mapped as the very same definition:

  • def foo : Nat := 0
  • def bar : Nat := 0
  • def boo := 0

Having name-irrelevant certificates can reduce the need for duplicate computations if the Lean 4 code doesn't change in semantics.

Learning resources

Clone this wiki locally