leanVM

minimal hash-based zkVM, for post-quantum Ethereum

leanXMSS aggregation	1400/s
leanSPHINCS aggregation	470/s
leanDA commitment	2,8 MiB/s

2-to-1 recursion	150 ms
proving KECCAK	560K/s
cheap cycles	7M/s

security

leanVM is designed for security:

• 128-bit ROM (64-bit QROM) soundness
• no proximity gap conjecture
• end-to-end formal verification
• a traditional hash function (Keccak-256)

work in progress

• leanVM is not yet stable (Keccak-256 is a placeholder: SHA2 is another option).
• Formal statements are still under review
• The Lean statements only describe the spec. Proving the Rust implem is faithful to the spec is still WIP.

leanVM is not (yet) production ready.

benchmarks

machine: M4 Max MacBook Pro (12 performance cores, 4 efficiency cores, 48GB RAM, CPU only, i.e. no metal GPU)

leanXMSS aggregation

The leanXMSS parameters are specified in leanXMSS.pdf, with a security proof in Lean 4. This is not the definitive parameter set.

cargo leanvm aggregate --xmss 1400 --log-inv-rate 2 --repeat 3

aggregation, 1,400 leanXMSS signatures
  cycles (VM steps)           : 1,146,537 = 2^20.129
    details                   : XOR 2^18 (22.9%)  KECCAK 2^17.994 (22.8%)  MUL 2^17.856 (20.7%)  SET 2^17.37 (14.8%)  DEREF 2^17.281 (13.9%)  JUMP 2^15.811 (5.0%)  MEMORY 2^21.081  BYTECODE 2^18.902  TOTAL_COMMITTED 2^25.745
  proof size                  : 247.6 KiB
  proving time                : 0.949 s ± 4.6%      peak memory 5.487 GiB
  per signature               : 1,475.048 signatures/s
  verifying                   : 6.275 ms

leanSPHINCS aggregation

The leanSPHINCS parameters are specified in leanSPHINCS.pdf, with a security proof in Lean 4. This is not the definitive parameter set.

cargo leanvm aggregate --sphincs 500 --log-inv-rate 1 --repeat 3

aggregation, 500 leanSPHINCS signatures
  cycles (VM steps)           : 2,756,127 = 2^21.394
    details                   : XOR 2^19.755 (32.1%)  MUL 2^19.436 (25.7%)  SET 2^19.392 (25.0%)  KECCAK 2^17.976 (9.4%)  DEREF 2^17.175 (5.4%)  JUMP 2^16.058 (2.5%)  MEMORY 2^22.043  BYTECODE2^18.902  TOTAL_COMMITTED 2^26.629
  proof size                  : 347.9 KiB
  proving time                : 1.06 s ± 1.1%      peak memory 6.179 GiB
  per signature               : 471.496 signatures/s
  verifying                   : 6.966 ms

data availability

cargo leanvm aggregate --blobs 16 --log-inv-rate 1 --repeat 3

aggregation, 16 blobs
  cycles (VM steps)           : 3,019,625 = 2^21.526
    details                   : XOR 2^20.098 (37.2%)  MUL 2^19.811 (30.5%)  DEREF 2^19.201 (20.0%)  JUMP 2^18.052 (9.0%)  SET 2^16.056 (2.3%)  KECCAK 2^15.088 (1.2%)  MEMORY 2^21.799  BYTECODE2^18.902  TOTAL_COMMITTED 2^26.496
  proof size                  : 339.6 KiB
  proving time                : 0.699 s ± 2.3%      peak memory 5.6 GiB
  blob throughput             : 22.905 blobs/s, 2.863 MiB/s
  verifying                   : 6.858 ms

recursion

cargo leanvm recursion --n 2 --xmss-per-leaf 1400 --leaf-log-inv-rate 2 --log-inv-rate 1 --repeat 3

recursion 2→1, over leaves of 1,400 leanXMSS signatures, leaf rate = 1/4, recursion rate = 1/2  cycles (VM steps)           : 459,768 = 2^18.811
    details                   : MUL 2^17.264 (34.2%)  XOR 2^16.962 (27.8%)  DEREF 2^16.554 (20.9%)  SET 2^15.259 (8.5%)  JUMP 2^14.676 (5.7%)  KECCAK 2^13.682 (2.9%)  MEMORY 2^19.445  BYTECODE2^18.902  TOTAL_COMMITTED 2^23.845
  proof size                  : 321.3 KiB
  proving time                : 0.159 s ± 0.6%      peak memory 1.117 GiB
  verifying                   : 9.379 ms

Proving KECCAK

cargo leanvm hash --log-n 17 --repeat 3

Keccak GKR batch proving, 131,072 permutations, a state committed every 12 rounds
  witness                         :     11.1 ms ± 28.9%    4.8%
  commit                          :     18.5 ms ± 10.5%    8.0%
  output claim                    :      2.4 ms ± 17.5%    1.0%
  layers and openings             :    179.7 ms ± 1.1%   77.3%
  pcs opening                     :     20.7 ms ± 11.7%    8.9%
  ------------------------------------------
  prove TOTAL (witness included)  :    232.4 ms ± 1.1%
  verify                          :      3.2 ms
  throughput                      :        563,994 permutations/s ± 1.1%
  proof size                      :       267.1 KiB  (1562 scalars, 230.4 KiB of Merkle openings)

Fibonacci

cargo leanvm fibonacci --n 2000000 --log-inv-rate 1 --repeat 3

Fibonacci (in the exponent, i.e. modulo 2^64 - 1), N = 2,000,000
  cycles (VM steps)           : 2,040,016
    details                   : MUL 2^20.944 (98.9%)  SET 2^13.288 (0.5%)  DEREF 2^12.967 (0.4%)  JUMP 2^10.968 (0.1%)  XOR 2^10.966 (0.1%)  MEMORY 2^20.959  BYTECODE 2^10.017  TOTAL_COMMITTED2^25.261
  proof size                  : 308.1 KiB
  proving                     : 0.289 s ± 6.3%   7,064,777 cycles/s      peak memory 2.32 GiB
  verifying                   : 4.831 ms

SNARK machinery

• 192-bit binary field (degree-3 tower over the 64-bit field)
• WHIR PCS, aka Ligerito
• Hashcaster 2 proving Keccak via GKR and RMFE
• Binius/Binius64 ring switching, M3 arithmetisation, and more (see DP23 and DP24)

FV Credits:

• leanerVM by Nicolas Schleicher and others
• leanDA FV by Benedikt Wagner
• VCVio, ArkLib, CompPoly, (Verified zk(E)VM) Clean (zksecurity)