ProveIR

Pre-compiled circuit template format: types, pipeline phases, and serialization.

Overview

ProveIR is the pre-compiled circuit template format that decouples compile-time circuit definition from runtime circuit instantiation. prove {…} blocks and Circom templates both produce ProveIR; both feed into the same instantiation → IR-SSA → backend pipeline.

Key crates:

• ir-forge — ProveIR data types, AST→ProveIR compiler, Lysis lift
• ir — orchestrates ProveIR, hosts CircomLibraryHandle trait, owns the module loader
• ir-core — leaf SSA types (Instruction<F>, SsaVar) shared by ir and ir-forge

Why pre-compile templates

• Avoids re-parsing/re-typechecking every prove invocation.
• Lets bytecode embed circuit definitions in the constant pool (TAG_BYTES).
• Allows Circom and .ach to share a single instantiation/optimization stack.
• Permits structural deduplication via the Lysis VM (in-progress).

Pipeline phases (A–H)

Phases A–B run at compile time; C–H run at runtime (VM mode) or directly in ach circuit mode (skipping serialize/deserialize).

Container types

ProveIR (file: ir-forge/src/types/prove_ir.rs:17-43):

pub struct ProveIR {
    pub name: Option<String>,
    pub public_inputs: Vec<ProveInputDecl>,
    pub witness_inputs: Vec<ProveInputDecl>,
    pub captures: Vec<CaptureDef>,
    pub body: Vec<CircuitNode>,
    pub capture_arrays: Vec<CaptureArrayDef>,
    pub component_bodies: HashMap<String, Vec<CircuitNode>>,
}

pub const PROVE_IR_MAGIC: &[u8; 4] = b"ACHP";
pub const PROVE_IR_FORMAT_VERSION: u8 = 6;

Serialization layout:

[MAGIC: 4 = "ACHP"][VERSION: 1][PRIME_ID: 1][BINCODE_PAYLOAD]

Version history (only v6 is currently accepted):

• v2 — added capture_arrays
• v3 — added message to CircuitNode::AssertEq
• v4 — added PrimeId byte (multi-prime)
• v5 — CircuitExpr::Const switched to FieldConst (32-byte canonical LE)
• v6 — added the component_bodies table for deferred component instances

CircuitExpr (expression tree)

File: ir-forge/src/types/expressions.rs:14-132.

Leaves:

Arithmetic:

Comparison:

Signed-range semantics — comparisons treat operands as signed values in (−p/2, p/2).

Boolean:

Crypto:

Integer ops:

Bitwise:

CircuitNode (statement-level)

File: ir-forge/src/types/nodes.rs:17-159.

pub enum CircuitNode {
    Let { name, value: CircuitExpr, span },
    LetArray { name, elements: Vec<CircuitExpr>, span },
    AssertEq { lhs, rhs, message: Option<String>, span },
    Assert { expr, message, span },
    For { var, range: ForRange, body: Vec<CircuitNode>, span },
    If { cond, then_body, else_body, span },
    Expr { expr, span },                                                   // builtin call w/ side effect
    Decompose { name, value, num_bits: u32, span },
    WitnessHint { name, hint: CircuitExpr, span },
    LetIndexed { array, index, value, span },                              // arr[i] = expr
    WitnessHintIndexed { array, index, hint, span },                       // arr[i] <-- expr
    WitnessCall { output_bindings, input_signals, program_bytes, span },   // Artik dispatch
    ComponentCall { body_key, comp_name, param_subs, span },                // deferred component instance
}

pub enum ForRange {
    Literal { start: u64, end: u64 },
    WithCapture { start: u64, end_capture: String },                       // bound is a template param
    WithExpr { start: u64, end_expr: Box<CircuitExpr> },                   // computed bound (e.g., n+1)
    Array(String),                                                          // iterate by name
}

Decompose is the bit-decomposition primitive: name is bound as a length-num_bits array of bool signals, with witness hints derived from value.

WitnessCall carries an embedded Artik bytecode blob — see Artik Witness VM. ComponentCall points into ProveIR::component_bodies; instantiation expands the shared body with the component name and parameter substitutions instead of serializing another inlined copy.

Captures

A prove {} block captures variables from the enclosing scope; Circom templates capture their parameters. Both use the same CaptureDef machinery:

pub struct CaptureDef {
    pub name: String,
    pub value: FieldConst,    // resolved at instantiation, not compile
}

pub struct CaptureArrayDef {
    pub name: String,
    pub elements: Vec<FieldConst>,
}

Captures stay symbolic in ProveIR (the Capture(name) leaf). They are bound by the Lysis-backed instantiation entry points such as ProveIR::instantiate_lysis(captures) and ProveIR::instantiate_lysis_with_outputs(captures, output_names).

Compiler entry point

File: ir-forge/src/ast_lower/api.rs.

ProveIrCompiler::compile_prove_block(
    block: &Block,
    outer_scope: &OuterScope,
    resolver_state: &ResolverState,
) -> Result<ProveIR, ProveIrError>

Submodules:

• ir-forge/src/ast_lower/exprs/ — CircuitExpr lowering (literals, ops, calls)
• ir-forge/src/ast_lower/calls/ — function/component dispatch (resolves through BuiltinRegistry + module loader)
• ir-forge/src/ast_lower/stmts/ — CircuitNode lowering (let, mut, for, if, assert)
• ir-forge/src/ast_lower/methods.rs — method desugaring (x.abs() → builtin-call)
• ir-forge/src/ast_lower/state.rs — compiler state (scope, witness auto-inference)

Instantiation

ProveIR::instantiate_extended(captures) first walks the ProveIR body into ExtendedInstruction<F>. The production entry points, instantiate_lysis and instantiate_lysis_with_outputs, then lower that extended form through Lysis into a flat IrProgram<F>. Loop handling, capture substitution, array index resolution, deferred component expansion, and Circom output projection all happen in this instantiation layer.

For Circom template libraries, circom/src/library/instantiate.rs handles component composition and parameter passing before producing the ProveIR nodes that use the same instantiation layer.

ExtendedInstruction (Lysis bridge)

File: ir-forge/src/extended.rs:63-112.

pub enum ExtendedInstruction<F: FieldBackend = Bn254Fr> {
    Plain(Instruction<F>),
    TemplateBody { id: TemplateId, frame_size: u8, n_params: u8, body: Vec<ExtendedInstruction<F>> },
    TemplateCall { template_id: TemplateId, captures: Vec<SsaVar>, outputs: Vec<SsaVar> },
    LoopUnroll { iter_var: SsaVar, start: i64, end: i64, body: Vec<ExtendedInstruction<F>> },
}

This wrapper layer enables the Lysis VM walker to lift loops and templates without inlining them in IR — a prerequisite for structural deduplication via the interner. Instantiation in this path is Bytecode-Oriented: ProveIR is lifted to a Lysis bytecode program whose execution emits the SSA IR. See Bytecode-Oriented Compilation for the architectural framing.

Source files

See Pipeline Overview for the full compile path. See IR & Optimization for what runs after instantiation. See Circom Frontend for how .circom files reach ProveIR.