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

Operation	Constraints	Notes
Add / Sub / Neg	0	LC arithmetic
Const / Input	0	Wire allocation
Mul	1	multiply_lcs
Div	2	inverse + multiply
Mux	2	boolean check + selection
AssertEq	1	enforce_equal
Assert	2	boolean check + enforce = 1
Not	1	boolean enforcement
And / Or	3	2 boolean checks + 1 multiply
IsEq / IsNeq	2	IsZero gadget
IsLt / IsLe	~760	2×252-bit range checks + 253-bit decomposition
PoseidonHash	361	360 round constraints + 1 capacity
RangeCheck(n)	n+1	n bit decomposition + sum check

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

Column	Kind	Purpose
s_arith	Fixed	Arithmetic gate selector
s_range	Fixed	Range check selector
constant	Fixed	Constant values
a, b, c, d	Advice	Computation wires
instance_0	Instance	Public inputs

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

Feature	R1CS	Plonkish
Constraint model	A×B=C	Gate polynomials
Addition cost	0 (LC)	0 (deferred)
Multiplication cost	1 constraint	1 row
Range check	n+1 constraints	1 lookup row
Binary export	.r1cs + .wtns (iden3)	Not yet
Proof system	Groth16 (arkworks)	KZG-PlonK (halo2)
CLI flag	--backend r1cs (default)	--backend plonkish

Source Files

Component	File
R1CS Backend	compiler/src/r1cs_backend.rs
Plonkish Backend	compiler/src/plonkish_backend.rs
Constraint System	constraints/src/r1cs.rs
Plonkish System	constraints/src/plonkish.rs
R1CS Errors	compiler/src/r1cs_error.rs