v0.10

Full rewrite with binary fields and blake2s

leanVM documentation

Auto-built on every push to main.

leanVM.pdf contains the leanVM specification.
XMSS.pdf contains the XMSS specification.
SPHINCS.pdf contains the SPHINCS specification.

v0.9

Changelog (by Opus 5)

v0.9 (2026-07-30)

Changes between v0.8 (2026-05-29) and v0.9 that affect users of the crates or of the
zkDSL.

Repository renamed from leanMultisig to leanVM (github.com/leanEthereum/leanVM). Old
remotes still resolve through GitHub's redirect; git dependencies should be repointed. The
root Rust package keeps the name lean-multisig (lean_multisig:: in code).

---

0. At a glance

Area	Change	Severity
XMSS	Keys and signatures from v0.8 no longer verify	Regenerate
Proofs	All v0.8 proofs and serialized aggregates are rejected	Regenerate
zkDSL	Poseidon precompiles renamed, two names kept with different meaning	Silent hazard
zkDSL	range / parallel_range can no longer mutate outer-scope variables	Compile error
zkDSL	Several previously-accepted programs are now rejected	Compile error
Rust	mt-* package names dropped, top-level utils crate removed	Compile error
Rust	XMSS and aggregation APIs reworked (names, argument order, message type)	Compile error
Rust	#[global_allocator] removed, setup_prover() now owns the arena	Compile error
Rust	Verifier is single-threaded, new parallel crate	Behavior
Limits	Extension-op and Poseidon tables now allow 2^22 rows (was 2^21)	Relaxed

---

1. What must be regenerated

1.1 XMSS keys and signatures

Two independent changes: WotsPublicKey::hash moved from a Merkle-Damgard chain of
compressions to an overwrite sponge (poseidon16_permute, output read from the second half
of the state), and the public API now signs a raw 32-byte message hashed off-circuit into
the 8 field elements the WOTS encoding consumes.

Both change the Merkle leaves, hence the root, hence the public key. Every key pair and
every signature produced by v0.8 is invalid under v0.9, with no migration path other than
fresh key generation. Persisted secret keys are rejected with an explicit error rather than
mis-decoded: XmssSecretKey gained a versioned serde format.

1.2 Proofs and serialized aggregates

v0.8 proofs are rejected by the v0.9 verifier and vice versa. Independent causes:

• slice hashing switched to the overwrite sponge, changing every Fiat-Shamir transcript,
  Merkle root, bytecode hash and public-input hash;
• Merkle pruning became optimal (about 5% smaller proofs);
• the WHIR initial sumcheck was restructured (fused combine, delayed extension-field
  representation);
• the Poseidon table gained a second output-length flag, changing its column layout;
• merkle_verify now takes a leaf permutation and a node compression separately.

Serialized aggregates are additionally incompatible because LZ4 framing was removed (see
3.4).

The bundled Python verifier (crates/lean_prover/python-verifier/verifier.py) was updated
in lockstep and now ships 5 test vectors instead of 1.

---

2. zkDSL

The grammar is unchanged. Everything below is semantic or library-level. Full reference:
crates/lean_compiler/zkDSL.md.

2.1 Poseidon precompiles renamed (read this first)

The suffix now counts how many of the 16 permutation cells are kept, instead of being
relative to a digest.

v0.8	v0.9	Cells written
poseidon16_compress(L, R, O)	poseidon16_compress_half(L, R, O)	O[0..8]
poseidon16_compress_half(L, R, O)	poseidon16_compress_quarter(L, R, O)	O[0..4]
poseidon16_compress_hardcoded_left(L, R, O, off)	poseidon16_compress_half_hardcoded_left(L, R, O, off)	O[0..8]
poseidon16_compress_half_hardcoded_left(L, R, O, off)	poseidon16_compress_quarter_hardcoded_left(L, R, O, off)	O[0..4]
poseidon16_permute(L, R, O)	unchanged	O[0..16]
(new)	poseidon16_permute_half(L, R, O)	O[0..8]
(new)	poseidon16_permute_half_hardcoded_left(L, R, O, off)	O[0..8]

compress_* applies the feed-forward addition (Poseidon(x) + x), permute_* is the raw
permutation. _hardcoded_left reads the first 4 cells of the left input from the
compile-time address off, the last 4 still from m[L..L+4].

poseidon16_compress_half and poseidon16_compress_half_hardcoded_left exist in both
versions and now write 8 cells instead of 4, so an unmigrated program still compiles. Under
write-once memory the 4 extra constrained cells usually surface as a conflicting-write
failure at run time, but may instead silently consume memory you intended to use.

Migration. Rename _half before the bare names, or the two steps collide:

# 1. the *_half names first (4 cells -> *_quarter)
grep -rl 'poseidon16_compress_half' --include='*.py' . | xargs sed -i '' \
  -e 's/poseidon16_compress_half_hardcoded_left/poseidon16_compress_quarter_hardcoded_left/g' \
  -e 's/poseidon16_compress_half(/poseidon16_compress_quarter(/g'

# 2. then the bare names (8 cells -> *_half)
grep -rl 'poseidon16_compress' --include='*.py' . | xargs sed -i '' \
  -e 's/poseidon16_compress_hardcoded_left/poseidon16_compress_half_hardcoded_left/g' \
  -e 's/poseidon16_compress(/poseidon16_compress_half(/g'

Not idempotent: run once. Use sed -i without the '' on GNU/Linux. Then grep for
poseidon16_compress(; the name no longer exists, so any leftover is a compile error.

Rust-side constants in lean_vm:

v0.8	v0.9
POSEIDON16_NAME	POSEIDON16_COMPRESS_HALF_NAME
POSEIDON16_HALF_NAME	POSEIDON16_QUARTER_NAME
POSEIDON16_HARDCODED_LEFT_NAME	same name, value now "poseidon16_compress_half_hardcoded_left"
POSEIDON16_HALF_HARDCODED_LEFT_NAME	POSEIDON16_QUARTER_HARDCODED_LEFT_NAME
POSEIDON_COL_FLAG_SHORT / POSEIDON_FLAG_SHORT_SHIFT	POSEIDON_COL_FLAG_OUT4 + POSEIDON_COL_FLAG_OUT8 / POSEIDON_FLAG_OUT8_SHIFT

ALL_POSEIDON16_NAMES grew from 5 to 7 entries; Poseidon table column indices after
POSEIDON_COL_FLAG_* all shifted by one.

2.2 range and parallel_range no longer carry mutables

A range loop is lowered to a recursive function, which breaks the compiler's SSA renaming.
The compiler used to hide this by silently inserting buffer arrays. That implicit rewrite is
gone: reassigning a variable declared outside the loop is a compile error, at any nesting
depth in the body (inside an if, inside a nested loop). Same rule for parallel_range.
unroll is unaffected and still supports loop-carried mutables.

total: Mut = 0
for i in range(0, n):
    total = total + a[i]    # v0.8: accepted. v0.9: compile error, loop-carried mutable
assert total == expected

Migration. Carry state through an explicit write-once buffer, one slot per iteration
plus one:

def sum(arr, n):
    total_buf = Array(n + 1)
    total_buf[0] = 0
    for i in range(0, n):
        total: Mut = total_buf[i]      # loop-LOCAL mutable: allowed
        total += arr[i]
        total_buf[i + 1] = total
    result = total_buf[n]              # value after the loop
    return result

For a small compile-time bound, switching range to unroll avoids the buffer entirely.

Mutables declared inside the body need no buffer:

y = 9
for i in range(0, n):
    x: Mut = f(i)
    x += 4
    x *= y
    assert x < 455

Fixtures: error_99 (range), error_100 (parallel_range), error_101 (mutation inside
a nested if), error_102 (nested range).

parallel_range's documented constraint is now stated as: each iteration writes only to its
own call frame and to addresses disjoint from every other iteration, with identical memory
footprint and identical hint consumption per iteration.

2.3 match_range

• No longer shadows a target defined in an outer scope.
• Bindings are immutable like any other binding. Declare the target : Mut only if you
  assign it more than once in the same scope; once per unroll iteration stays
  immutable, since each iteration is a fresh scope.
• An empty range is rejected (it produced a match with no cases): error_96.

a: Mut
a, b = match_range(n, range(0, 4), lambda i: two_values(i))
a += 1                                                    # second assignment => a must be : Mut

for k in unroll(0, n):
    c = match_range(k, range(0, 4), lambda i: one_value(i))  # immutable: fresh binding per iteration

2.4 Programs that no longer compile

Previously accepted, or panicked inside the compiler; all now produce a clean error.

Rejected	Fixture	Note
Const-array index out of bounds (A[10] for A = [1, 2, 3])	error_93
Writing into a const array (A[0] = 1)	error_94	Rejected even when the written value matches
Const array as a call-assignment target (A[0] = foo())	error_95
match_range over an empty range	error_96
Nested call to an undefined function (1 + undefined_fn(3))	error_97
unroll with an enormous bound	error_98	Would have expanded unboundedly
Loop-carried mutables in range / parallel_range	error_99 to error_102	See 2.2
Undefined array base (a = ARR[0] with no ARR)	error_103	Used to panic in codegen
Multidimensional read on a non-const array (arr[0][1])	error_104	Used to panic
Multidimensional assignment target (arr[0][1] = 5)	error_105	Used to silently compile as arr[0] = 5
Multidimensional compound-assignment target (arr[0][1] += 1)	error_106

2.5 Semantics now documented (no behavior change)

• unroll(start, end) with start >= end expands to zero iterations. range /
  parallel_range count up until the counter equals end, so start > end wraps ...

v0.8

recursion program: more efficient logup

Latest spec PDF

Auto-built from misc/minimal_zkVM.tex on every push to main.