Backends

R1CS and Plonkish constraint compilation backends.

Achronyme compiles the same SSA IR into two constraint system backends: R1CS (for Groth16) and Plonkish (for KZG-PlonK). Both live in the compiler crate.

R1CS Backend

File: compiler/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
    vars: HashMap<SsaVar, LinearCombination>,  // SSA var → LC
    witness_ops: Vec<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.

Plonkish Backend

File: compiler/src/plonkish_backend.rs

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 check regardless of bit width. The range table is pre-populated with values [0, 2^bits).

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 { column, row, name }
PlonkWitnessOp::CopyValue { dst_col, dst_row, src_col, src_row }
PlonkWitnessOp::SetConstant { column, row, value }
PlonkWitnessOp::ArithRow { row }       // compute d = a*b + c
PlonkWitnessOp::InverseRow { row }     // compute inverse
PlonkWitnessOp::BitExtract { ... }     // extract bit from value

Backend Comparison

Source Files