leanerVM

leanerVM is a Lean 4 implementation and formalization of leanVM, leanEthereum's minimal hash-based SNARK virtual machine for post-quantum signature aggregation. Current leanVM uses binary fields and BLAKE2s; the historical KoalaBear/Poseidon implementation remains available on its koalabear branch.

The primary application target is leanVM's recursive XMSS and SPHINCS aggregation guest. At the pinned revision, XMSS claims are grouped by epoch with one message per group, while each SPHINCS claim carries its own message. The final result must be bound to that exact guest and imply the intended claim about every published key, message, epoch, and signature.

The executable Lean semantics serves three complementary purposes: it anchors proofs from VM execution through the proof system, provides an implementation worth optimizing in its own right, and supplies an independent reference for validating the existing Rust implementation. That validation begins with differential testing against pinned Rust revisions and may grow into formal verification of the relevant Rust code.

Project status

The repository baseline is in place: module boundaries, the test library, validation policy, CI with a kernel axiom audit, and dependency tracking. The first formalization effort, the leanISA roadmap (docs/roadmap/leanisa-blueprint.md, issue #4), has landed its Layers 0 to 7: the fields and the generator, BLAKE2s compression and the cell encoding, instructions, the memory image and the public input, the step function and valid executions, the bytecode encoding, the bus channels, the six opcode tables as Clean components, each sound and complete for the relation its row refines, and the three boundary blocks; Layer 8 supplies the constraint statement SatisfiedBy and one hand-built witness. The reference step and run are noncomputable; fixed-image executable checkers are proved equivalent to them for exact and fuel-bounded runs. Finite traces and a pinned Rust comparison lane provide the first ISA validation boundary. The bus theorems, constraint soundness (constraintSoundness, with the computable trace of traceOf_valid, for bytecode whose sentinel slot is not a JUMP) and constraint completeness (constraintCompleteness, for well-formed bytecode and an execution that fits the caps, through a padded trace) are proved, with the equivalence on inputs satisfiable_iff_valid; no proof-system claim has landed. See the checker guide.

Recursive CTE is an open research problem: the intended knowledge-soundness arguments for the concrete inner SNARKs live in the random-oracle model, while the known outer recursion-topology argument requires an extraction interface that is not presently justified by such inner results. The architecture keeps the desired final theorem as a target schema and does not claim that this bridge has been solved.

Assurance goals

• Give leanVM a pure executable semantics for its six-opcode instruction set, binary-field machine state, write-once memory, and halting behavior.
• Prove that valid arithmetized traces correspond to executions of those semantics, including the converse obligations needed by the intended correctness statement.
• Compose those results through witness generation, guest correctness, the base proof system, and recursion into versioned end-to-end soundness and completeness theorems.
• Assemble leanVM-specific protocols from reusable, reviewed components in ArkLib, VCVio, CompPoly, and Clean.
• Validate versioned Rust leanVM behavior with shared vectors and differential execution tests; pursue a proved Rust correspondence when an appropriate verification boundary is available.
• Bind constants, encodings, layouts, and challenge schedules to exact source revisions.
• State deployment gaps and cryptographic assumptions explicitly, with inhabited examples and negative controls for load-bearing definitions.
• Establish reproducible performance baselines and improve execution through Lean's native C code-generation path, specified Rust or CUDA FFI kernels, and a future domain-specific compiler.

Compilation is only one part of acceptance. Public theorem statements, assumptions, trust closure, non-vacuity, and correspondence with the referenced implementation are reviewed as part of the deliverable.

Execution and performance

The pure Lean implementation is the semantic reference, not merely a testing oracle for Rust. The project will measure and improve the executable produced by Lean's native C backend, while retaining the same observable VM behavior. Where profiling justifies specialized kernels, fast Rust or CUDA implementations may be connected through narrow FFI boundaries and checked against the Lean reference on shared workloads.

A future domain-specific compiler can provide a more specialized execution path. Its source language, target behavior, and preservation theorem must be explicit: generated code becomes part of the trusted result only to the extent justified by those proofs and the documented compiler/runtime assumptions.

Getting started

Install elan, then clone the repository and run:

./scripts/validate.sh

The repository is pinned by lean-toolchain to Lean v4.34.1. The complete validation command checks source policy, imports, architectural dependencies, documentation, the timing helper, the Lean build, and executable tests.

Useful focused commands are:

lake build
lake test
lake env lean -E warning tests/Main.lean
./scripts/audit-lean.sh
./scripts/check-imports.sh
./scripts/check-layers.sh

See CONTRIBUTING.md for code style, theorem review, testing, attribution, and pull-request requirements.

Architecture

Parameters ──→ Semantics ──→ Arithmetization ──→ Protocol
                         └──→ Applications ────────┘

An arrow points from a foundational layer to a layer that may depend on it. scripts/check-layers.sh enforces the forbidden reverse edges, and the proof system's wall: no protocol module imports the arithmetization except the few that meet it (docs/architecture.md).

Layer	Responsibility
LeanerVM/Semantics/	ISA, state, memory, bytecode, transition relation, and executable interpreter
LeanerVM/Parameters/	Versioned constants, encodings, layouts, and authoritative source bindings
LeanerVM/Arithmetization/	Tables, buses, witness generation, constraints, and semantic refinement
LeanerVM/Applications/	Guest specifications, exact programs, compiler boundaries, and application correctness
LeanerVM/Protocol/	leanVM-specific composition of polynomial, oracle, commitment, and proof-system components

The detailed ownership and dependency rules are in docs/architecture.md.

Repository map

Path	Contents
LeanerVM/	Production Lean library
LeanerVM.lean	Aggregate import surface
tests/	Executable examples and proof-regression tests
bench/	Benchmark contracts and reproducible workloads
docs/	Architecture, dependencies, development, and CI documentation
scripts/	Validation, repository checks, drift reporting, and timing tools
.github/workflows/	Build, policy, review, benchmark, and maintenance automation

Dependencies

Lean and library versions are tracked centrally rather than through floating branches. docs/dependencies.md defines the update and review policy, while upstreams.json provides the machine-readable release baseline. The audited target, its relationship to the original leanVM implementation, and the current formalization gaps are recorded in docs/leanvm-target.md.

Reusable results should live in their natural upstream library:

• ArkLib for generic proof systems and oracle reductions;
• VCVio for oracle computations and cryptographic security definitions;
• CompPoly for computable polynomial and field infrastructure; and
• Clean for circuit, AIR, table, and witness-generation infrastructure.

leanerVM owns the machine semantics, executable implementation, concrete parameters, leanVM arithmetization instances, application specifications, protocol assembly, implementation-validation boundary, and optimized execution paths specific to leanVM.

Testing and automation

lake test builds the LeanerVMTests.lean test library, whose #guards and examples are checked at compile time; tests/Main.lean imports it and is elaborated with warnings as errors by scripts/validate.sh. Tests for semantics should cover successful executions, boundaries, and malformed inputs. Constraint work should include witness mutations that demonstrate rejection, and implementation-validation work should include differential vectors tied to authoritative Rust source revisions. Differential agreement is regression evidence; it is not presented as a proof about the Rust source.

CI keeps build/tests, repository policy, import layering, and documentation integrity as independent required checks. It also provides automated PR summaries, member-triggered review, upstream release tracking, and informational build timing. Project releases follow reviewed milestones rather than Lean toolchain updates. The benchmark job records clean-build, warm-build, and test-path wall/user/system time with JSONL records and logs. See docs/ci.md and bench/README.md.

License

leanerVM is licensed under the Apache License 2.0. See LICENSE.