Skip to content

aiur: ground the FFT cost model in the prover's actual transforms - #539

Open
arthurpaulino wants to merge 1 commit into
mainfrom
ap/aiur-proving-cost
Open

aiur: ground the FFT cost model in the prover's actual transforms#539
arthurpaulino wants to merge 1 commit into
mainfrom
ap/aiur-proving-cost

Conversation

@arthurpaulino

Copy link
Copy Markdown
Member

The per-circuit FFT cost statistic (Ix/Aiur/Statistics.lean) was (stage1 + stage2 width) * h * log2(h) over function and memory circuits only. Compared against the pinned prover (multi-stark be1755e, Plonky3 e9d7561), that misses:

  • the quotient chunk columns: q*D committed base columns per circuit, q = next_pow2(max(d, 2) - 1) — constraint-degree changes were invisible to the statistic;
  • the commit transform structure: Radix2DitParallel::coset_lde_batch runs one size-h inverse DFT plus B size-h coset DFTs per column, not one size-B*h DFT;
  • the two quotient-rebasing transforms: the iDFT of the (q*h) x D flattened quotient and the size-h DFT of the q*D coefficient slices;
  • the Bytes1/Bytes2 gadget circuits, whose witness builders always emit full tables (256 / 65536 rows with zero multiplicities on unqueried rows), so they are active in every proof as a fixed cost.

The new per-circuit cost, with F(0) = 0, F(x) = x*log2(max(x, 2)), and the raw (unpadded) height h so one-row changes stay visible while structural powers of two (B, q) stay exact:

(B+1)*(m + s2 + q*D)*F(h) + D*F(q*h) + q*D*F(h)

summed over constrained functions, memories, Bytes1, and Bytes2.

Circuit shapes (main/stage-2 width, quotient degree, preprocessed dimensions) are read off the compiled Rust System through a new AiurSystem::circuit_shapes API and FFI — never re-derived in Lean, since max_constraint_degree requires the compiled constraint graph. ix check statistics use a one-shot build-extract-drop variant (that flow never builds a system otherwise, and pays the build only when stats are requested). The prove/verify/stats parameter triple is deduplicated into Aiur.defaultCommitmentParameters / defaultFriParameters.

The report now prints per-circuit costs in scientific notation (two-decimal mantissa); the total stays in full digits with the scientific form in parentheses.

A new aiur-cost primary suite covers the pure formula: exact values at power-of-two heights, one-row monotonicity across power-of-two boundaries (where the padded prover plateaus), per-input monotonicity in width, lookups, quotient degree, and blowup, and the scientific formatter (including the mantissa-carry edge). A Rust test pins circuit_shapes against System.circuits field-for-field, including canonical order and the fixed gadget table dimensions.

FFT pins regenerated from one lake test -- --ignored ixvm run (only the FFT pin assertions moved; all execution/parity tests passed). Small constants now sit on a ~174M fixed floor that is almost entirely the always-active Bytes2 commit: 5 * 32 * F(65536) ≈ 168M.

@arthurpaulino
arthurpaulino enabled auto-merge (squash) August 5, 2026 22:52
The per-circuit FFT cost statistic (`Ix/Aiur/Statistics.lean`) was
`(stage1 + stage2 width) * h * log2(h)` over function and memory
circuits only. Compared against the pinned prover (multi-stark
`be1755e`, Plonky3 `e9d7561`), that misses:

- the quotient chunk columns: `q*D` committed base columns per circuit,
  `q = next_pow2(max(d, 2) - 1)` — constraint-degree changes were
  invisible to the statistic;
- the commit transform structure: `Radix2DitParallel::coset_lde_batch`
  runs one size-h inverse DFT plus B size-h coset DFTs per column, not
  one size-`B*h` DFT;
- the two quotient-rebasing transforms: the iDFT of the `(q*h) x D`
  flattened quotient and the size-h DFT of the `q*D` coefficient
  slices;
- the `Bytes1`/`Bytes2` gadget circuits, whose witness builders always
  emit full tables (256 / 65536 rows with zero multiplicities on
  unqueried rows), so they are active in every proof as a fixed cost.

The new per-circuit cost, with `F(0) = 0`, `F(x) = x*log2(max(x, 2))`,
and the raw (unpadded) height `h` so one-row changes stay visible while
structural powers of two (`B`, `q`) stay exact:

    (B+1)*(m + s2 + q*D)*F(h) + D*F(q*h) + q*D*F(h)

summed over constrained functions, memories, `Bytes1`, and `Bytes2`.

Circuit shapes (main/stage-2 width, quotient degree, preprocessed
dimensions) are read off the compiled Rust `System` through a new
`AiurSystem::circuit_shapes` API and FFI — never re-derived in Lean,
since `max_constraint_degree` requires the compiled constraint graph.
`ix check` statistics use a one-shot build-extract-drop variant (that
flow never builds a system otherwise, and pays the build only when
stats are requested). The prove/verify/stats parameter triple is
deduplicated into `Aiur.defaultCommitmentParameters` /
`defaultFriParameters`.

The report now prints per-circuit costs in scientific notation
(two-decimal mantissa); the total stays in full digits with the
scientific form in parentheses.

A new `aiur-cost` primary suite covers the pure formula: exact values
at power-of-two heights, one-row monotonicity across power-of-two
boundaries (where the padded prover plateaus), per-input monotonicity
in width, lookups, quotient degree, and blowup, and the scientific
formatter (including the mantissa-carry edge). A Rust test pins
`circuit_shapes` against `System.circuits` field-for-field, including
canonical order and the fixed gadget table dimensions.

FFT pins regenerated from one `lake test -- --ignored ixvm` run (only
the FFT pin assertions moved; all execution/parity tests passed).
Small constants now sit on a ~174M fixed floor that is almost entirely
the always-active `Bytes2` commit: `5 * 32 * F(65536) ≈ 168M`.
@arthurpaulino

Copy link
Copy Markdown
Member Author

!bencher-thresholds-reset aiur-check-prove aiur-check-execute aiur-recursive

@github-actions github-actions Bot added bencher-thresholds-reset:aiur-check-execute bencher baseline reset queued on merge bencher-thresholds-reset:aiur-check-prove bencher baseline reset queued on merge bencher-thresholds-reset:aiur-recursive bencher baseline reset queued on merge labels Aug 6, 2026
@github-actions

github-actions Bot commented Aug 6, 2026

Copy link
Copy Markdown

♻️ Baseline reset queued for: aiur-check-execute aiur-check-prove aiur-recursive — will anchor to the merge commit when this PR merges.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bencher-thresholds-reset:aiur-check-execute bencher baseline reset queued on merge bencher-thresholds-reset:aiur-check-prove bencher baseline reset queued on merge bencher-thresholds-reset:aiur-recursive bencher baseline reset queued on merge

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant