AIR Cryptographer Expertise
Expert-level knowledge for designing, implementing, and auditing Algebraic Intermediate Representations (AIRs) in zero-knowledge proof systems.
Core Mindset
Soundness-first thinking: Every constraint review starts with "how could a cheater slip through?" Think adversarially. Construct counterexample traces by hand. Exploit polynomial identity loopholes.
Algebraic precision: Constraints define solution spaces over finite fields. A missing constraint isn't just a bug—it's extra degrees of freedom for a malicious prover.
Finite Field Foundations
Essential intuitions:
- Characteristics and inverses: Every non-zero element has a multiplicative inverse. No zero divisors.
- Roots of unity: Multiplicative subgroups of order 2^k enable FFT-friendly evaluation domains.
- Extension fields: When you need more algebraic structure (e.g., M31 → QM31 for Stwo).
- Frobenius endomorphism: The map x → x^p is field-linear; crucial for extension field arithmetic.
Polynomial Mechanics
Interpolation: Given n points, unique polynomial of degree < n passes through them. Lagrange basis makes this explicit.
Vanishing polynomials: Z_H(x) = ∏(x - h) for h ∈ H vanishes exactly on domain H. This is the foundation of constraint enforcement.
Degree behavior:
- Multiplication: deg(f·g) = deg(f) + deg(g)
- Composition: deg(f∘g) = deg(f) · deg(g)
- Low-degree testing verifies a function is "close to" a low-degree polynomial
Evaluation domains: Multiplicative cosets for separation. Blowup factor determines security margin between trace degree and domain size.
Trace Design Principles
Column Classification
| Type | Definition | Example | | ------------------- | ---------------------------- | ---------------------------- | | Source of truth | Canonical witness data | PC, registers, memory values | | Derived | Computed from source columns | Flags, decompositions | | Auxiliary | Added to reduce degree | Intermediate products |
Critical rule: Every column must be constrained. An unconstrained column is a free variable for the prover.
Row Semantics
Define precisely what each row represents:
- CPU cycle / instruction
- Memory operation
- Padding (must be distinguishable!)
Row types require selectors. Selectors must be:
- Boolean:
s(s-1) = 0 - Mutually exclusive:
Σ s_i = 1(or coverage proof) - Actually constrained (not just documented)
Minimal vs Redundant Columns
Start minimal. Add auxiliary columns only when:
- Degree reduction is necessary
- Soundness requires explicit intermediate values
- Verification cost dominates
Constraint Categories
Transition Constraints (Local)
Express correct step relation between row i and row i+1:
next_pc = pc + instruction_size (when not branching)
next_register[k] = f(current_state, opcode)
Danger: Writing a relation instead of a function. Multiple valid next-states = unsound.
Boundary Constraints
Pin specific rows to specific values:
- Initial: Row 0 state matches expected start
- Final: Last row satisfies termination condition
- I/O: Public inputs/outputs bound at known positions
Danger: "Final row" must be uniquely defined. Variable-length traces need explicit halt handling.
Booleanity and Range Constraints
For boolean b: b(b-1) = 0
For k-bit value x with bits b0...b{k-1}:
x = Σ b_i · 2^i
b_i(b_i - 1) = 0 for all i
Danger: Forgetting booleanity constraints on decomposition bits.
Selector Discipline
Selectors gate which constraints apply to which rows.
Checklist:
- [ ] Each selector is boolean
- [ ] Exactly one selector active per row (or explicit coverage)
- [ ] No "ghost mode" where all selectors = 0
- [ ] Selector itself is constrained (not free)
Classic bug: All selectors zero makes all gated constraints vacuously true.
Global Consistency Arguments
Permutation / Multiset Equality
Prove two multisets are equal via grand product:
∏(α - a_i) = ∏(α - b_i)
Checklist:
- Initial product = 1 (boundary constraint)
- Final products equal (boundary constraint)
- Challenge α bound to transcript after commitments
- Duplicates handled correctly
Danger: Product hitting zero, missing boundary constraints, challenge reuse.
Lookup Arguments
Prove all values in column A appear in table T.
Checklist:
- Table is committed/fixed
- Compression is collision-resistant (sufficient randomness)
- Repeated lookups soundly counted
Danger: Weak compression allows out-of-table values.
Memory Consistency
Memory operations form a log: (address, timestamp, value, is_write)
Patterns:
- Sort by address, then by timestamp
- Consecutive same-address ops: read sees last write
- Permutation links memory log to CPU trace
Danger:
- Address aliasing across different trace sections
- Timestamp not proven monotonic
- Read-before-write not enforced
Quotient and Composition
Constraint polynomial C(x) should vanish on trace domain H.
Quotient: Q(x) = C(x) / Z_H(x)
If C doesn't vanish on H, Q has poles → not low-degree → FRI rejects.
Row-Set Control
Constraints apply to different row sets:
- All rows: divide by Z_H(x)
- All but last: divide by Z_H(x) / (x - ω^{n-1})
- First only: multiply by Lagrange selector for row 0
- Last only: multiply by Lagrange selector for row n-1
Danger: Constraint meant for "all rows" accidentally only enforced on subset due to incorrect vanishing factor.
Degree Accounting
Track degree of every constraint:
Base constraint degree: d
After selector multiplication: d + deg(selector)
After boundary polynomial: d + deg(boundary)
Composition polynomial degree must stay below domain size with sufficient margin (blowup factor).
Fiat-Shamir Hygiene
Transcript must bind:
- All commitments (trace, lookup tables, etc.)
- Public inputs
- Trace length / domain parameters
- Any prover messages
Challenge separation: Different arguments need independent challenges. Reusing challenges creates algebraic vulnerabilities.
Danger: Challenge derived before commitment → prover can adapt witness.
Adversarial Witness Exercises
Before declaring an AIR sound, try to break it:
- All selectors = 0: Do constraints still enforce anything?
- Corrupt one column: Can it drift without detection?
- Attack last row: Dump inconsistency into wrap-around?
- Duplicate/omit memory events: Does global check catch it?
- Force product to zero: Exploit grand product boundary?
- Exploit gating: Make "if flag then X" vacuous by leaving flag unconstrained?
If you find a counterexample trace, you found a bug.
Common Vulnerability Patterns
| Pattern | Symptom | Fix | | -------------------- | -------------------------- | ---------------------------------- | | Unconstrained column | Prover sets arbitrarily | Add constraint | | Missing booleanity | Non-binary "boolean" | Add b(b-1)=0 | | Selector leakage | Constraint bypassed | Enforce exclusivity | | Last row escape | Inconsistency hidden | Proper terminal constraints | | Product zero | Permutation argument fails | Boundary checks, domain separation | | Challenge reuse | Algebraic cancellation | Separate challenges per argument | | Weak compression | Lookup collision | Increase randomness |
Performance-Aware Design
Understand tradeoffs without being an engineer:
| Choice | Prover Cost | Verifier Cost | Soundness | | ----------------- | -------------------- | ------------- | ------------ | | More columns | Higher memory | Unchanged | Neutral | | Higher degree | More FRI rounds | More queries | Watch blowup | | More rows | Linear scaling | Log scaling | Neutral | | Auxiliary columns | Memory + constraints | Unchanged | Can improve |
Rules of thumb:
- Auxiliary columns to reduce degree often worth it
- Local constraints cheaper than global arguments
- Precomputation tables vs dynamic checks: depends on table size
Review Deliverables
When reviewing an AIR, produce:
- Column inventory: Name, meaning, range, where constrained
- Constraint map: Each semantic claim → which constraint enforces it
- Degree table: Every constraint's degree contribution
- Adversarial tests: Attempted counterexamples
- Risk ranking: Critical / High / Medium findings
- Proposed fixes: Concrete constraint additions/modifications
See references/review-checklist.md for the complete systematic review sheet.