Yatima is a Lean 4 compiler backend targeting the the Lurk language for recursive zkSNARKs, enabling zero-knowledge proofs of Lean 4 execution. Additionally, Yatima has its own Lean 4 implementation of a kernel for the Lean 4 core language, which can be compiled to Lurk to allow zero-knowledge proofs of Lean 4 typechecking. By verifying a zero knowledge proof that a Lean 4 declaration has passed the typechecker, one can verify that the declaration is type-safe without re-running the typechecker.
Yatima also implements nameless content-addressing for Lean 4, allowing each expression, declaration and environment to receive unique hash identifiers, independent of computationally-irrelevant naming (such as the names of definitions and local variables).
Run lake run setup, which will build the yatima binary and ask you where to place it.
You can choose a directory that's already in your path, for example.
Running the setup script will also compile the Yatima typechecker and store it in the FS, under the $HOME/.yatima directory.
The subcommands planned to be available for the yatima CLI are:
- Main commands
ca: content-addresses Lean 4 code to Yatima IRprove: generates Lurk code for typechecking a content-addressed declaration
- Auxiliary commands
tc: typechecks Yatima IRgen: generates Lurk code from Lean 4 codepin: edits theTypecheckM.leanfile with the hashes for primitive operations and allowed axiomsgentc: compiles the Yatima typechecker to Lurk
- Network
ipfs put: sends Yatima IR to IPFSipfs get: retrieves Yatima IR from IPFS
Don't hesitate to call yatima --help for more information.
Constraints:
- The
casubcommand must be triggered from within a Lean project that uses Lake - The Lean 4 code to be content-addressed must use the same toolchain as the one used to compile the
yatimabinary. To see the needed toolchain, callyatima --versionand check the content before the pipe| - To compile a Lean 4 file that imports others, the imported
oleanfiles must be available