Python bindings for leanVM - a minimal zero-knowledge virtual machine.
leanVM is a minimal zkVM (zero-knowledge virtual machine) designed for post-quantum signature aggregation using XMSS (eXtended Merkle Signature Scheme). These Python bindings allow you to execute leanVM bytecode and work with field arithmetic from Python.
- Python 3.8 or higher
- Rust toolchain (for building from source)
- Access to the leanMultisig repository (for lean_compiler)
# Install maturin (Rust-Python build tool)
pip install maturin
# Navigate to the leanVM directory
cd /path/to/leanVM
# Build and install in development mode (fast, for testing)
maturin develop
# Or build an optimized wheel (slower build, faster runtime)
maturin build --release
pip install target/wheels/leanvm-*.whlimport leanvm
# 1. Field Arithmetic
# Create field elements (KoalaBear field)
a = leanvm.FieldElement(42)
b = leanvm.FieldElement(17)
# Perform arithmetic operations
c = a + b # Addition
d = a * b # Multiplication
e = a - b # Subtraction
f = a / b # Division (multiplicative inverse)
g = -a # Negation
h = a.pow(3) # Exponentiation
inv = a.inverse() # Multiplicative inverse
# Special elements
zero = leanvm.FieldElement.zero()
one = leanvm.FieldElement.one()
print(f"Result: {c}") # Prints: Result: 59
print(f"Is zero: {zero.is_zero()}") # Prints: True
# 2. Execute Bytecode
# Note: Bytecode must be compiled using lean_compiler
# from leanISA source code
# For example, after compiling with lean_compiler:
# bytecode = ... # Load your compiled bytecode here
# Execute the bytecode
result = leanvm.execute_bytecode(
bytecode,
public_input=[a, b], # Public inputs (list of FieldElements)
private_input=[], # Private inputs (list of FieldElements)
no_vec_runtime_memory=0, # Non-vectorized runtime memory size
profiling=True # Enable execution profiling
)
# Access execution results
print(result.summary) # Execution summary
print(result.num_instructions) # Number of instructions executed
print(result.public_memory_size) # Size of public memory
# Access final memory state
memory_value = result.memory.get(0) # Get value at address 0
memory_size = result.memory.size() # Get memory sizeSee the examples/ directory for more usage examples:
# Run the basic usage example
python examples/basic_usage.pyRun the test suite:
# Install pytest
pip install pytest
# Run tests
pytest tests/- KoalaBear field (31-bit prime field) operations
- Addition, subtraction, multiplication, division
- Exponentiation and multiplicative inverse
- Equality comparisons and hashing
- Execute leanVM bytecode with public/private inputs
- Access execution traces and memory states
- Support for profiling and debugging
- Precompiled Poseidon hash operations
The VM supports:
- Computation: ADD, MUL operations
- Deref: Double pointer dereference
- Jump: Conditional control flow
- Precompile: Specialized operations (Poseidon hashing, dot products)
The Python bindings wrap the following core components:
- FieldElement: KoalaBear field elements
- Bytecode: Compiled program representation
- Instruction: VM instruction types
- Memory: Sparse memory implementation
- ExecutionResult: Execution state and results
These bindings are designed to work with the leanMultisig toolchain:
- Write programs in leanISA (the VM's assembly language)
- Compile using
lean_compilerto generate bytecode - Execute the bytecode using these Python bindings
- Generate proofs using the WHIR proving system (future work)
# Build with debug symbols (faster compile, slower runtime)
maturin develop
# Build with optimizations
maturin develop --releaseleanVM/
├── src/ # Rust source code (PyO3 bindings)
│ ├── lib.rs # Main Python module
│ ├── field.rs # Field element wrapper
│ ├── bytecode.rs # Bytecode and instruction wrappers
│ └── execution.rs # Execution and memory wrappers
├── python/ # Python package
│ └── leanvm/ # Python module
│ └── __init__.py
├── examples/ # Usage examples
├── tests/ # Test suite
├── Cargo.toml # Rust dependencies
└── pyproject.toml # Python packaging config
class FieldElement:
def __init__(self, value: int) -> None: ...
@staticmethod
def from_u32(value: int) -> FieldElement: ...
@staticmethod
def zero() -> FieldElement: ...
@staticmethod
def one() -> FieldElement: ...
def to_u32(self) -> int: ...
def is_zero(self) -> bool: ...
def inverse(self) -> FieldElement: ...
def pow(self, exponent: int) -> FieldElement: ...
# Arithmetic operators
def __add__(self, other: FieldElement) -> FieldElement: ...
def __sub__(self, other: FieldElement) -> FieldElement: ...
def __mul__(self, other: FieldElement) -> FieldElement: ...
def __truediv__(self, other: FieldElement) -> FieldElement: ...
def __neg__(self) -> FieldElement: ...
def __eq__(self, other: FieldElement) -> bool: ...class Bytecode:
def __init__(self) -> None: ...
def len(self) -> int: ...
def is_empty(self) -> bool: ...
def program(self) -> str: ...
def starting_frame_memory(self) -> int: ...class ExecutionResult:
memory: Memory
summary: str
num_instructions: int
public_memory_size: int
no_vec_runtime_memory: intclass Memory:
def get(self, index: int) -> FieldElement: ...
def size(self) -> int: ...
def to_list(self) -> list[tuple[int, FieldElement]]: ...def execute_bytecode(
bytecode: Bytecode,
public_input: list[FieldElement] = None,
private_input: list[FieldElement] = None,
no_vec_runtime_memory: int = 0,
profiling: bool = False
) -> ExecutionResult: ...- The VM uses vectorized operations (VECTOR_LEN = 8) internally
- Field arithmetic is optimized using Montgomery form
- Memory is sparse and dynamically allocated
- Maximum memory size: 2^24 field elements
- Bytecode must be compiled using
lean_compiler(not included in these bindings) - No direct instruction building API (use compiler instead)
- Proof generation requires the
lean_provercrate (not exposed in Python bindings)
This project is part of the leanMultisig research project. For contributions or issues, please refer to the main repository.
MIT