Skip to content

README.md

Latest commit

 

History

History
267 lines (201 loc) · 6.97 KB

README.md

File metadata and controls

267 lines (201 loc) · 6.97 KB
Raw

leanVM Python Bindings

Python bindings for leanVM - a minimal zero-knowledge virtual machine.

Overview

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.

Installation

Prerequisites

  • Python 3.8 or higher
  • Rust toolchain (for building from source)
  • Access to the leanMultisig repository (for lean_compiler)

From source

# 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-*.whl

Quick Start

import 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 size

Examples

See the examples/ directory for more usage examples:

# Run the basic usage example
python examples/basic_usage.py

Testing

Run the test suite:

# Install pytest
pip install pytest

# Run tests
pytest tests/

Features

Field Arithmetic

  • KoalaBear field (31-bit prime field) operations
  • Addition, subtraction, multiplication, division
  • Exponentiation and multiplicative inverse
  • Equality comparisons and hashing

Bytecode Execution

  • Execute leanVM bytecode with public/private inputs
  • Access execution traces and memory states
  • Support for profiling and debugging
  • Precompiled Poseidon hash operations

VM Instructions

The VM supports:

  • Computation: ADD, MUL operations
  • Deref: Double pointer dereference
  • Jump: Conditional control flow
  • Precompile: Specialized operations (Poseidon hashing, dot products)

Architecture

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

Integration with leanMultisig

These bindings are designed to work with the leanMultisig toolchain:

  1. Write programs in leanISA (the VM's assembly language)
  2. Compile using lean_compiler to generate bytecode
  3. Execute the bytecode using these Python bindings
  4. Generate proofs using the WHIR proving system (future work)

Development

Building for development

# Build with debug symbols (faster compile, slower runtime)
maturin develop

# Build with optimizations
maturin develop --release

Project Structure

leanVM/
├── 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

API Reference

FieldElement

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: ...

Bytecode

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: ...

ExecutionResult

class ExecutionResult:
    memory: Memory
    summary: str
    num_instructions: int
    public_memory_size: int
    no_vec_runtime_memory: int

Memory

class Memory:
    def get(self, index: int) -> FieldElement: ...
    def size(self) -> int: ...
    def to_list(self) -> list[tuple[int, FieldElement]]: ...

Functions

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: ...

Performance Considerations

  • 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

Limitations

  • 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_prover crate (not exposed in Python bindings)

Contributing

This project is part of the leanMultisig research project. For contributions or issues, please refer to the main repository.

License

MIT