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: crates/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 const PROVE_IR_MAGIC: &[u8; 4] = b"ACHP";
pub const PROVE_IR_FORMAT_VERSION: u8 = 5;

Serialization layout:

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

Version history (only v5 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)

CircuitExpr (expression tree)

File: crates/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: crates/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
}

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.

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 at instantiation by ProveIR::instantiate(captures, ...).

Compiler entry point

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

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

Submodules:

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

Instantiation

ProveIR::instantiate(captures, public_values, witness_values) walks the ProveIR body and emits SSA IR. Loop unrolling, capture substitution, and array index resolution all happen here.

For Circom templates, instantiation is driven by the circom crate’s instantiate.rs which knows about component composition and parameter passing.

ExtendedInstruction (Lysis bridge)

File: crates/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.

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.