Deep Dive

Architecture Overview

ZKSync Airbender's architecture is built around several key components that work together to provide efficient and secure ZK proving of RISC-V execution.

• RISC-V 32I+M Architecture: Airbender implements a complete RISC-V 32-bit integer instruction set with multiplication extensions, providing a familiar and well-specified execution environment for developers.
• Modular Circuit Design: The system employs configurable "machine variants" that can selectively enable or disable features based on use case requirements. This flexibility allows for optimized circuits tailored to specific execution contexts, from general-purpose kernel execution to highly specialized recursive proving scenarios.
• Advanced Cryptographic Primitives: The proof system integrates optimized implementations of Blake2s, Blake3, and 256-bit big integer operations as precompiled circuits, enabling efficient cryptographic operations within the proven execution environment.
• Scalable Proof Generation: Airbender can handle up to 2³⁰ CPU cycles in a single proving run, with intelligent batching that processes approximately 2²² cycles per chunk.
• Hybrid CPU/GPU Implementation: The system provides both CPU and GPU implementations of the prover, with preliminary witness generation performed on CPU before transitioning to GPU-accelerated circuit-specific proving for optimal performance.

Circuit Design Philosophy

• Mersenne31 Field Arithmetic: All arithmetic operations are performed over Mersenne31 field elements (2³¹ - 1), chosen for its efficiency in both software and hardware implementations. When additional security is required, the system switches to extension fields, particularly for lookup finalization operations.
• Register and Memory Model: The system implements an approach where all 32-bit RISC-V registers are stored in RAM rather than as dedicated circuit elements. This design choice relegates register access to the RAM argument system while maintaining only minimal shared state (such as the Program Counter) across execution cycles.
• Degree-2 Constraint Optimization: All AIR (Algebraic Intermediate Representation) constraints are limited to degree-2 polynomials, which streamlines STARK/FRI optimizations and simplifies circuit performance analysis by focusing on witness trace column counts.

Execution Model

• Fetch-Decode-Execute Loop: Airbender follows the traditional CPU execution model with a standardized fetch-decode-execute loop that operates in machine privilege mode. This loop is identically enforced at each cycle and row of the witness trace, providing predictable and verifiable execution semantics.
• ROM-Based Instruction Storage: Program bytecode is stored in a read-only memory (ROM) region that is accessed through preprocessed lookup tables. This ROM virtually inhabits a reserved portion of the RAM address space, simplifying the memory model while maintaining clear separation between code and data.
• Custom Instruction Extensions: The system supports custom instructions through the CSRRW opcode, which is converted to delegation argument calls for accessing precompiled circuits and non-deterministic storage. This extension mechanism allows for efficient implementation of complex operations while maintaining the core RISC-V compatibility.
• Batch Processing: The system processes execution in batches of approximately 4 million cycles (2²²), with individual chunks proven separately and connected through global RAM and delegation arguments.

Configuration Variants

Airbender supports multiple machine configurations to optimize for different use cases:

• Full Kernel Mode: Complete RISC-V 32I+M support for running ZKsync OS kernel code, with standard compiler assumptions about memory alignment and instruction usage.
• Application Mode: Removes signed multiplication and division operations to reduce circuit complexity for applications that don't require these operations.
• Recursion Mode: Highly optimized configuration for recursive proof verification, supporting custom field arithmetic operations while eliminating unnecessary instruction support.

Limitations

Airbender makes several standard assumptions about the code that needs to be proven:

• Static Bytecode Model: The current implementation assumes bytecode is placed in ROM and does not support runtime-loaded or dynamically generated code. This design choice simplifies the proving model but limits certain programming patterns.
• Initialization Constraints: The system does not support non-trivially initialized static variables, requiring manual initialization patterns for programs that need persistent state.
• Trap Handling: Rather than implementing complex trap handling within the CPU state, the system converts traps to unprovable constraints, causing the prover to fail when bugs are encountered. This approach ensures correctness but requires careful program design.
• Memory Alignment: The system disallows inefficient unaligned memory accesses to maintain proving efficiency, relying on compiler guarantees for proper memory layout.