| name | circuit-optimization |
| description | Optimizing arithmetic circuits / constraint systems (R1CS, PLONKish, AIR) for zero-knowledge proofs — minimizing multiplication constraints, rows, witnesses, and gate degree. Use when reducing constraint/witness counts, designing or golfing R1CS/PLONK/AIR gadgets (boolean ops, adders, range checks, hashes like SHA-256/Keccak/Poseidon), doing foreign-field/non-native or CRT/RNS arithmetic, choosing lookups vs arithmetic, or using SMT (cvc5) and SageMath (Gröbner basis) to synthesize, verify, and certify constraint encodings. |
Circuit optimization
Reduce the cost of an arithmetic circuit / constraint system without breaking soundness.
A toolbox and a method, not a fixed playbook: references/techniques.md primes known
moves but is deliberately incomplete — the largest wins come from composing tricks or
from structure specific to your circuit.
Know what is free
Every optimization moves work into what the proof system charges nothing for and
minimizes what it charges for.
| System | Pays for | Free / cheap |
|---|
| R1CS (Groth16, Marlin, Spartan) | multiplication rows (A·z)(B·z)=(C·z) | linear combinations feeding a row, inlined wire definitions (a standalone asserted equality still costs a row) |
| PLONKish (halo2, plonky2/3, Kimchi) | rows × columns; FFT blowup ∝ max gate degree | additions within a gate, selectors on unused rows |
| AIR / STARK | trace width × length; constraint degree | — |
State the scarce metric (mult-constraints? rows? witnesses? degree?) and get a baseline
before optimizing.
Workflow
- Measure the scarce resource; find the dominating hotspot.
- Prime with
references/techniques.md, then look for structure the catalogue misses —
usually the bigger win.
- Synthesize a candidate. Small boolean gadgets: search exactly with
scripts/synthesize.sage (fix the multiplier R, solve a linear system over QQ).
- Verify soundness before trusting it:
scripts/verify.smt2 (cvc5 QF_FF) proves the
constraint forces the output over a real F_p; scripts/impossible.smt2 proves a
shape impossible when the search is empty.
- Certify for a proof assistant if needed:
scripts/cofactors.sage extracts the
cofactors proving the output is uniquely determined.
- Re-measure; track the bounds each trick relies on (field size, carry width,
characteristic).
Tools
Two tools on PATH, no Python glue: Sage for algebra (search + certificates), cvc5
for SMT (QF_FF, run directly on .smt2).
sage scripts/synthesize.sage
sage scripts/cofactors.sage
cvc5 scripts/verify.smt2
cvc5 scripts/impossible.smt2
cvc5 QF_FF proves a statement about the specific prime in the file (exact, no side
condition); Sage over QQ yields small prime-independent constants and a single "holds
for all char > bound" result (the form Lean proofs consume). Use both. See
references/smt.md, references/sage.md.
Files
references/techniques.md — the catalogue (free linear combos, multi-operand add,
carry-save, single-constraint boolean gadgets, CRT/RNS, lookups, range-check/spread,
custom gates, non-deterministic advice, solver methods, primitive notes).references/smt.md — cvc5 / SMT-LIB: verify, prove impossibility, model the field.references/sage.md — SageMath: Gröbner ideal-membership proofs, cofactor lifts,
CRT/RNS bounds, computing hard-coded constants.scripts/ — synthesize.sage, cofactors.sage, verify.smt2, impossible.smt2.
Self-checking, cross-checked against the verified SHA-256 gadgets in ~/src/clean.
Lean / Clean
Circuits proven in Lean (e.g. Clean, ~/src/clean): unless explicitly asked, never change the spec to make a proof pass, and never leave sorry — leave the proof unfinished and say what is missing.
