machine-cat

Generic AIR (Algebraic Intermediate Representation) chip framework built on proof-cat, plonkish-cat, and comp-cat-rs.

Generalizes from plonkish-cat's wire-indexed constraints to execution trace tables where constraint polynomials must hold at every consecutive row pair. This is the standard STARK/AIR model, and Subset 2 from the SP1 decomposition.

Key concept

plonkish-cat constrains individual wires: Wire(3) - Wire(1) * Wire(2) = 0.

machine-cat constrains columns across rows: "for every row i, next_a - current_b = 0." This is how real proof systems (STARKs, SP1, Plonky3) work: constraints are transition rules that the execution trace must obey.

Architecture

Air::generate_trace(input) -> Trace<F>
             |
   bridge::air_prove(air, trace) -> AirProof<F>
             |
   bridge::air_verify(air, proof) -> Ok(true)

Modules

Module	Purpose
`column`	`Column`, `ColumnCount`, `ColumnRef` newtypes (row-relative addressing)
`air_expr`	`AirExpr<F>`: constraint expressions with `Current(col)` / `Next(col)` references
`trace`	`Trace<F>`: 2D execution trace (rows x columns)
`air`	`Air<F>` trait: defines columns, constraints, and trace generation
`fibonacci`	`FibonacciAir`: a concrete example proving Fibonacci computation
`bridge`	`air_prove` / `air_verify`: trace-to-sumcheck proof via proof-cat

Quick start

use plonkish_cat::F101;
use machine_cat::{Air, FibonacciAir, FibonacciInput, StepCount};
use machine_cat::bridge::{air_prove, air_verify};

fn main() -> Result<(), machine_cat::Error> {
    let air = FibonacciAir;
    let input = FibonacciInput::new(
        F101::new(1), F101::new(1), StepCount::new(7),
    );

    // Generate the execution trace: 8 rows of Fibonacci values.
    let trace = air.generate_trace(&input)?;

    // Prove the trace satisfies the Fibonacci transition constraints.
    let proof = air_prove(&air, &trace)?;

    // Verify (no trace needed, only the AIR definition and proof).
    assert!(air_verify(&air, &proof)?);
    Ok(())
}

How it works

The Air trait

An Air<F> defines:

Column count: how many field elements per row.
Transition constraints: AirExpr<F> expressions using Current(col) and Next(col) that must equal zero at every consecutive row pair.
Trace generation: given an input, produce the execution trace.

The Fibonacci example

The FibonacciAir has 2 columns (a, b) and 2 constraints:

next_a - current_b = 0 (next row's a = current row's b)
next_b - current_a - current_b = 0 (next row's b = sum of current a and b)

Given initial values (1, 1), the trace is:

Row	a	b
0	1	1
1	1	2
2	2	3
3	3	5
4	5	8
...	...	...

Proof protocol

Validate: check that the trace satisfies all constraints at every row pair.
Commit: flatten the trace into a Merkle tree.
Batch: squeeze random challenges from a Fiat-Shamir transcript and form a random linear combination of constraint evaluations.
Sumcheck: prove the combined evaluation polynomial sums to zero.
Open: open all trace column values with Merkle proofs.

The verifier replays the transcript, checks the sumcheck, verifies Merkle openings, and re-evaluates the constraints.

Categorical interpretation

Each AIR is a morphism in a category where objects are trace shapes (column counts). Parallel composition of independent AIRs is the tensor product (column concatenation). This structure is documented but not type-level enforced in v0.1; multi-chip machines with cross-chip lookup arguments are planned for v0.2.

Building

cargo build
cargo test
RUSTFLAGS="-D warnings" cargo clippy
cargo doc --no-deps --open

Dependencies

proof-cat: sumcheck proving infrastructure, Merkle commitment, Fiat-Shamir transcript
plonkish-cat: Field trait (transitive through proof-cat)
sha2: SHA-256 for transcript hashing (transitive through proof-cat)

Roadmap

v0.1 (current): single-AIR proving with Fibonacci example
v0.2: Machine type (collection of AIRs), cross-chip lookup arguments via spans from comp-cat-rs
v0.3: MonoidalCategory implementation for parallel AIR composition

License

MIT

machine-cat 0.3.0