$ show powdr-labs/powdr
This repository implements a compiler-based optimization framework for zero-knowledge virtual machines (zkVMs), specifically targeting OpenVM and SP1. Its core innovation is Automatic Precompile Synthesis (APC), which analyzes execution traces of RISC-V guest programs and synthesizes optimized constraint systems (symbolic machines) that drastically reduce proof cost—achieving up to 9x column reduction and 88x constraint reduction on complex operations. The system combines profile-guided optimization (PGO), a sophisticated constraint solver with range reasoning and rule-based rewriting, and an optional Lean4 verified optimizer via FFI. The architecture is a multi-crate Rust workspace with a CLI (`powdr_openvm_riscv`) orchestrating a staged pipeline: generate APCs from execution profiles, select the best candidates using PGO metrics, setup the prover with the selected APCs, execute the program, and generate proofs. It supports CPU and GPU (CUDA) backends, and includes extensive benchmarking infrastructure with nightly regression analysis and a web-based APC effectiveness viewer. Bus interaction handling is abstracted via a `BusMap` and adapter pattern, making the optimization logic VM-agnostic. While primarily an application, the repository has strong research character: it includes domain-specific formal methods (Lean4, Datalog rules), empirical constraint detection, and a large corpus of snapshot tests documenting optimizer outputs. It is actively maintained with CI pipelines, but depends on several tightly coupled forks (OpenVM, SP1) and pinned nightly Rust toolchains, posing moderate technical drift risk.
The LLM identified 5 files worth highlighting for reuse:
Implements RangeConstraint as a combination of wrapping intervals and bitmasks for over-approximating finite-field value ranges. Provides algebraic operations (sum, product, square, conjunction, disjunction) and is used throughout the constraint solver and optimizer. Reusable for any field-based constraint system needing value range reasoning.
Defines a BusMap that maps bus IDs to typed bus variants (Memory, Byte, BitwiseLookup, VariableRangeChecker, TupleRangeChecker), and provides a default OpenVM bus map. The bus interaction handlers are implemented via a trait pattern, making the constraint solver and optimizer independent of the specific VM. This component can be extracted and adapted for other zkVMs.
Core data types (SymbolicMachine, SymbolicBusInteraction, SymbolicConstraint) for representing optimized instruction semantics. Supports rendering with bus maps, children visitors, and conversion to constraint systems. The representation is generic over field types and reusable for any instruction set optimization pipeline.
Implements a Datalog-style rule engine (using the `crepe!` macro) for pattern-matching on algebraic constraints. Contains 100+ rules for detecting boolean variables, one-hot encodings, single-occurrence combinations, and equal-zero checks. The driver orchestrates batch replacement with conflict resolution and degree-bound-aware inlining. This is a reusable pattern for automated theorem proving in constraint systems.
Implements StagedPipeline, a generic pattern for orchestrating generate → select → setup → execute → prove stages with caching. Each stage is a separate step that can be resumed from cache. This pattern is reusable for any multi-stage build/verify workflow, not just zkVM proving.