Pipeline Overview

The compilation pipeline from source to proofs.

Achronyme compiles source code through four distinct paths: VM mode for general execution, Circuit mode for constraint generation via ach circuit, Prove mode for inline proof generation via prove {} blocks, and Circom mode for compiling .circom files through the same backend pipeline.

Pipeline Diagram

Stage 1: Parsing

Entry point: achronyme_parser::parse_program(source)

Hand-written recursive descent parser with Pratt expression parsing. Produces an owned AST with Program, Stmt, Expr, and Block nodes. Handles public/witness declarations, type annotations, prove {} blocks, method calls, and static namespace access (Type::MEMBER).

Operator precedence (high to low):

1. ^ (power)
2. *, /, % (multiplicative)
3. +, - (additive)
4. ==, !=, <, <=, >, >= (comparison)
5. && (logical AND)
6. || (logical OR)

Stage 2a: Bytecode Compilation (VM Mode)

Entry point: akronc::Compiler::compile()

For ach run, the AST is compiled to bytecode for the register-based VM (37 opcodes). A 3-pass bytecode optimizer runs after compilation:

• Peephole — fuses common instruction sequences
• Constant folding — evaluates arithmetic on known constants
• Dead store elimination — removes writes to registers never read

prove {} blocks are handled specially: the block body is compiled to ProveIR at compile time (not at runtime), serialized as bytes in the constant pool (TAG_BYTES), and deserialized + instantiated when the VM reaches the prove expression.

Stage 2b: IR Lowering (Circuit Mode)

Entry point: IrLowering::lower_circuit(source, pub_vars, wit_vars)

For ach circuit, the AST is lowered directly to SSA IR. Key behaviors:

• let bindings are aliases — no instruction emitted
• if/else compiles to Mux(cond, then_val, else_val) — both branches evaluated
• for loops are statically unrolled (max 10,000 iterations)
• Function calls are inlined at each call site; recursion detected via call stack guard
• Arrays support compile-time indexing: a[i] where i must be constant

Stage 2c: ProveIR Pipeline (Prove Mode)

Entry point: ProveIrCompiler::compile_prove_block()

prove {} blocks go through an 8-phase pipeline:

This design means prove blocks are pre-compiled at compile time — no re-parsing at runtime. The ProveIR format carries type information, source spans, and function references through serialization.

Stage 2d: Circom Frontend

Crate: circom — Entry point: circom::parser::parse_circom(source)

Compiles .circom files through the same ProveIR → IR → Backend pipeline. The Circom frontend adds structural safety: <-- (unconstrained signal assignment) without a corresponding === constraint produces a hard compile-time error (E100), catching under-constrained signals that are the #1 source of ZK vulnerabilities.

The lowered ProveIR feeds into the same instantiation → optimization → backend pipeline as prove {} blocks and ach circuit. Circom templates can also be imported and called from .ach files in both circuit and VM modes — see the Circom Interop chapter for the user-facing syntax and semantics.

Stage 3: Optimization

Entry point: ir::passes::optimize(&mut program)

Five passes run sequentially on the IR:

Constant Folding (const_fold)

Forward pass that evaluates operations on known constants. Folds arithmetic (Const(3) + Const(5) → Const(8)), simplifies identities (x * 0 → 0, x - x → 0, x / x → 1), and folds boolean logic.

Bound Inference (bound_inference)

Rewrites unbounded IsLt/IsLe comparisons to bounded variants when operands have proven bitwidth bounds from RangeCheck. Unbounded comparisons cost ~761 constraints; bounded cost ~(n+3) where n is the bitwidth.

Common Sub-expression Elimination (cse)

Single-pass O(n) that identifies duplicate pure computations and remaps to the first occurrence. Covers arithmetic, Poseidon, Mux, boolean ops, comparisons. Particularly effective on unrolled loops.

Dead Code Elimination (dce)

Iterative fixpoint pass that removes instructions whose results are never used. Side-effecting instructions (AssertEq, Assert, Input, RangeCheck) are never eliminated.

Boolean Propagation (bool_prop)

Computes the set of proven-boolean SSA variables. Seeds from comparisons, RangeCheck(x, 1), Assert operands, and Bool annotations. Propagates through Not, And, Or, Mux. The R1CS backend uses this to skip redundant boolean enforcement.

Taint Analysis (taint)

Warns about under-constrained or unused witness inputs. Tracks dataflow from witnesses to assertions — a witness that doesn’t influence any constraint is flagged.

Stage 4: Backend Compilation

R1CS Backend (default)

Entry point: R1CSCompiler::compile_ir(program)

Maps each SsaVar to a LinearCombination. Add/Sub/Neg are free (LC arithmetic). Mul/Div/Mux/Poseidon emit R1CS constraints (A × B = C).

Wire layout: [ONE, pub₁..pubₙ, wit₁..witₘ, intermediates...]

Plonkish Backend

Entry point: PlonkishCompiler::compile_ir(program)

Lazy evaluation with PlonkVal — defers add/sub/neg until multiplication forces materialization. Standard gate: s_arith · (a·b + c − d) = 0. Range checks use a lookup table (1 row vs n+1 constraints in R1CS).

Stage 5: Proof Generation

Crate: proving

Native in-process proof generation — no external tools required.

Also generates Solidity verifier contracts for on-chain verification of Groth16 proofs.

The .r1cs and .wtns binary exports remain snarkjs-compatible for users who prefer external tooling.

Multi-Prime Support

The pipeline is generic over the prime field via FieldElement<F: FieldBackend>. Three backends are implemented:

Field selection is resolved once at the session boundary; monomorphization eliminates all runtime overhead.

Source Files