Lean 4 in RISC Zero Guest

This example shows how to compile Lean 4 to RISC Zero, using the C code generated by Lean with a custom runtime and a Lean Init library precompiled to RISC Zero. To run your own Lean 4 program in the RISC Zero zkVM just replace the guest/ directory with your Lean 4 sources. The supported version of Lean is 4.22.0.

Running

1. Make sure you have the following environment variables set.

• LEAN_RISC0_PATH: path to the Lean RISC0 runtime, typically $HOME/.lean-risc0.
• RISC0_TOOLCHAIN_PATH: path to RISC0 toolchain, typically $HOME/.risc0/toolchains/v2024.1.5-cpp-x86_64-unknown-linux-gnu/riscv32im-linux-x86_64.

2. Install Lean RISC0 runtime.
3. Install Lean RISC0 Init standard library.
4. just build
5. target/release/host N

Main example

The main branch contains an example of a sum function in Lean operating on Nat. The example implements a general interface to Lean 4, passing data via a byte array which is then parsed to Nat on the Lean side. The result is returned in a byte array which is then parsed on the Rust side. The example properly initializes the runtime.

Sum example

The sum-example branch contains a lightweight example of a sum function in Lean operating on 32-bit unsigned integers. This example doesn't perform runtime initialization.

Running your own Lean 4 program in the RISC Zero zkVM

Replace the guest/ directory with your Lean 4 project. The supported version of Lean is 4.22.0. Your project needs to:

• contain a Guest.lean file in its root directory which imports all project modules,
• define a risc0_main function exported to C under this name which serves as the entry point:

@[export risc0_main]
def risc0_main (input : ByteArray) : ByteArray := ...

You may also want to modify methods/guest/src/main.rs and host/src/main.rs to change the input type.

Performance

The lightweight example from the branch sum-example takes similar time to run (execution + proving time) as an analogous function written in C running in RISC0 zkVM, which is a few seconds. This is not surprising because the C code generated by Lean when using UInt32 is similar to how one would write a recursive sum function in C by hand, and no Lean-specific initialization is performed.

The full example in main takes much more time due to the initialization of Init library modules. The initialization of the runtime itself is relatively quick (a few seconds). The initialization of Init modules takes about 13 minutes on my laptop. The bulk of this seems to be proving time. My machine has 16 cores, but I'm not using the GPU.

The reason for the slowness of module initialization seems to be that the RISC0 zkVM is very slow in general, in comparison to native execution. The initialization of modules needs to traverse all modules recursively (there are almost 400 of them in Init) and execute module-specific initialization for each. It just takes time to prove this execution.

Implementation details

Implementing compilation of Lean 4 to RISC Zero required:

• a custom version of the Lean runtime avoiding certain features (IO, exceptions, signals, threading),
• compiling the Lean Init library to RISC0,
• linking the libc and libstdc++ libraries provided by the RISC0 toolchain,
• providing shims for some C functions.

The linker for the guest needs the --allow-multiple-definition flag, which is fragile and things may fail on a different system.

Related projects

György Kurucz ported Lean to cross-compile to the ESP32-C3 RISC-V microcontroller:

• blog post,
• repository.