This repository contains an MLIR dialect for zkLean. zkLean is a domain specific language (DSL) for specifying zero-knowledge statements in the Lean theorem prover. This dialect is intended to interface with LLZK (WIP).

• A C++ compiler
• LLVM / MLIR,
• Ninja

While standing in zklean-mlir/, run

bash build_deps.sh
bash build_test.sh

The first command will build MLIR, assuming the LLVM project source is placed in zklean-mlir/externals/. The second command will build zklean-opt and run tests. These commands have succeeded on x86 machines running Debian and NixOS. Please inspect build_deps.sh, build_test.sh, and CMakeLists.txt and modify to point to your llvm-project/ directory (or as needed).

Work in progress

• MLIR standalone example
• MLIR-tutorial