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:
ca: content-addresses Lean 4 code to Yatima IRprove: generates Lurk code for typechecking a content-addressed declarationtc: typechecks Yatima IRgen: generates Lurk code from Lean 4 codepin: edits the TypecheckM.lean file with the hashes for primitive operations and allowed axiomsgentc: compiles the Yatima typechecker to Lurkipfs put: sends Yatima IR to IPFSipfs get: retrieves Yatima IR from IPFSDon't hesitate to call yatima --help for more information.
Constraints:
ca subcommand must be triggered from within a Lean project that uses Lakeyatima binary.
To see the needed toolchain, call yatima --version and check the content before the pipe |olean files must be available