Backends

R1CS and Plonkish constraint compilation backends.

Achronyme compiles the same SSA IR into two constraint-system backends in the zkc crate: R1CS (for Groth16) and Plonkish (for KZG-PlonK). The bytecode compiler (akronc) is a separate VM-mode compiler and is not where constraint backend emission lives.

R1CS Backend

File: zkc/src/r1cs_backend.rs

The R1CS backend compiles IR instructions into rank-1 constraint system constraints of the form A × B = C, where A, B, C are linear combinations of wire values.

Core Data Structures

R1CSCompiler {
    cs: ConstraintSystem,          // A×B=C constraints
    bindings: HashMap<String, Variable>,  // declared var → wire
    lc_map: LcMap,                 // SSA var → linear combination
    witness_ops: SegmentedVec<WitnessOp>,   // trace for witness generation
    proven_boolean: HashSet<SsaVar>,  // skip boolean enforcement
}

Wire Layout

Index:  0       1..n_pub    n_pub+1..
        ONE     public      witness + intermediate

Wire 0 is always the constant 1. Public inputs are allocated before witnesses for snarkjs compatibility.

Compilation Strategy

The backend maps each SsaVar to a LinearCombination (sparse Vec<(Variable, FieldElement)>).

Free operations (LC arithmetic only, no constraints):

• Add(a, b) → lc_a + lc_b
• Sub(a, b) → lc_a - lc_b
• Neg(a) → -lc_a
• Const(v) → v * Variable::ONE

Constraint-emitting operations:

• Mul(a, b) → allocate wire, enforce a × b = result (1 constraint)
• Div(a, b) → compute inverse, enforce b × inv = 1, then a × inv = result (2 constraints)
• Mux(c, t, f) → enforce c boolean, enforce c × (t-f) = result - f (2 constraints)
• AssertEq(a, b) → enforce a = b (1 constraint)

Constraint Costs

Boolean Optimization

If a variable is in the proven_boolean set (from the bool_prop pass), the backend skips its boolean enforcement constraint. This saves 1 constraint per known-boolean variable used in Mux, And, Or, or Not.

R1CS Substitution Soundness

After IR-level optimization, an R1CS-level pass performs linear elimination and substitution to shrink the constraint count (this is what brings ECDSAVerify(64,4) to ~1.49M constraints, below circom’s own count). The greedy eliminator could previously leave a surviving constraint that still referenced a wire the pass had already eliminated — a forgeable-witness hazard, because the eliminated wire was no longer pinned by any constraint.

This is now closed via per-cluster cycle resolution: substitutions are resolved cluster-by-cluster (Tarjan SCC + RREF, including self-loops) on the un-composed substitution map, then the driver flattens the closure so no eliminated wire survives as a dangling reference. Generated witnesses are bit-identical to the pre-fix path and the optimized constraint count still holds below circom — the fix is purely a soundness repair, not a count regression.

Plonkish Backend

File: zkc/src/plonkish_backend/

The Plonkish backend compiles IR into a table of gate rows with columns, copy constraints, and lookup tables.

Standard Columns

Standard Arithmetic Gate

s_arith · (a · b + c − d) = 0

Each multiplication emits one row. Addition is encoded as a·1 + c = d.

Lazy Evaluation

The Plonkish backend uses PlonkVal for lazy evaluation:

PlonkVal::Cell(CellRef)          // materialized in a cell
PlonkVal::Constant(FieldElement)  // not yet placed
PlonkVal::DeferredAdd(a, b)      // deferred until needed
PlonkVal::DeferredSub(a, b)      // deferred until needed
PlonkVal::DeferredNeg(a)         // deferred until needed

Add, Sub, and Neg operations build deferred expressions. Only when a value is needed for multiplication or a builtin does materialize_val() emit an actual row.

This means a chain of additions like a + b + c + d emits fewer rows than in a naive approach — only the final materialization emits rows.

Range Checks via Lookups

Unlike R1CS (which uses n+1 bit decomposition constraints), Plonkish range checks use a lookup table: 1 row per supported check. The range table is pre-populated with values [0, 2^bits), so very large bit widths are rejected rather than materializing an impractically large table.

Comparison Operations

• IsLt(a, b) → 252-bit range checks on both operands + 253-bit decomposition of b − a + 2^252 − 1
• IsLe(a, b) → 1 − IsLt(b, a) (swap and negate)
• IsZero(a) → sets d to constant 0 (not an ArithRow) for sound enforcement

Witness Generation

PlonkishWitnessGenerator replays PlonkWitnessOp entries to fill the assignment table:

PlonkWitnessOp::AssignInput { cell, name }
PlonkWitnessOp::CopyValue { from, to }
PlonkWitnessOp::SetConstant { cell, value }
PlonkWitnessOp::ArithRow { row }       // compute d = a*b + c
PlonkWitnessOp::InverseRow { row }     // compute inverse
PlonkWitnessOp::IsZeroRow { row }      // compute IsZero helper cells
PlonkWitnessOp::BitExtract { ... }     // extract bit from value
PlonkWitnessOp::IntDivMod { ... }      // integer quotient + remainder

Backend Comparison

Source Files