Repository navigation
feat: KZG on BN254 - #675
Merged
Merged
Conversation
Add a reusable compression pipeline for proofs of aggregated Ix root
certificates, preserving the original CheckEnv claim through:
aggregate root -> normalized Aiur root -> FRI -> KZG -> recursive KZG
Constrain the FRI transcript, Merkle openings, quotient algebra and batch
policy over Goldilocks, translate verification to the BLS12-381 scalar
field, then recursively verify KZG commitments and openings. Check the
final outer proof and both external pairing equations, including degree
bounds. Encode the final proof under a fixed verifier layout, retaining
the public pairing operands and certificate claim.
Derive the verifier locally from the compiled aggregate backend, SRS and
explicit bounds, without any certificate or proof witness. Normalize a
root by recursively wrapping it into one all-active Aiur trace shard.
Give each function and memory trace its own u8 log-height; retain native
byte-table heights and constrain memory closure endpoints. Reject layouts
that exceed bounds before allocating traces. The root may aggregate any
number of certificate shards whose verification fits those bounds.
Expose `ix compression layout`, `ix compression setup`, `ix compress` and
compressed-proof verification through `ix verify`. The prover supplies
only a proof address. Keep trusted settings and verifier keys outside the
proof store, bind backend/SRS/layout/partition limits into configuration
identity, and reject unknown configurations. Verification requires only
the local settings and verifier key, not the proving SRS. Import SRS data
with checked point/subgroup decoding and powers/degree-key validation;
known-trapdoor development setup is an explicit option. Use bounded,
versioned, canonical proof and verifier encodings.
Make FRI, intermediate KZG and final KZG partition limits independent.
Use lazy lowering, commit KZG partitions separately, reconstruct lookups
from committed columns, and release prior witnesses and fixed evaluations
as soon as possible. Store constant polynomials as a value and domain
length while retaining their full degree binding. Decode SRS powers in
parallel chunks and bound consistency-check MSM scratch. Pin multi-stark
to the backend-independent proving and exposed Plonkish interfaces these
stages require.
Keep one crate README with the CLI, bounds, library entry points and a
reproducible sub-3 KB recipe. Include the tested Init layout as an explicit
example, not a built-in policy. Keep measurements, SRS files, binaries and
proof artifacts out of the patch.
Reproduction from an existing full Init root (16 aggregated shards):
lake build ix
export RAYON_NUM_THREADS=32
export IX_COMPRESSION_HOME="$PWD/compression"
ix=.lake/build/bin/ix
root=ROOT_ADDRESS
"$ix" compression setup --dev-srs \
--root-layout crates/proof-compression/examples/init16-root-layout.json \
--fri-log-height 23 --log-height 25 --recursive-log-height 28
compressed=$("$ix" compress "$root")
"$ix" verify "$compressed"
"$ix" verify --aggregate --ixe Init.ixe --ixes Init-16.ixes "$compressed"
The final 2^28 partition admits one arithmetic trace plus a 2^17 lookup
table, avoiding the extra commitments/openings of a partitioned final
arithmetic circuit. The SRS covers 2^28 G1 powers and all degree keys.
The development SRS exercises the whole chain but is not production-secure;
production requires independently trusted parameters in the same format.
Other root layouts may need different bounds and can produce larger proofs.
Measured full Init run on 2026-10-15, Xeon 6975P-C, 32 Rayon threads,
512 GiB machine, CPU proving, using development parameters:
Native root: 5,738,532 bytes
Complete Ixon.Proof: 2,707 bytes
Compact KZG proof: 2,053 bytes
Pairing operands: 576 bytes (12 compressed G1 points)
Compression envelope: 40 bytes
Ixon wrapper and claim: 38 bytes
Local setup: 5,934.484 s; peak RSS 327.965 GiB
Compression: 12,254.842 s; peak RSS 359.891 GiB
Startup/SRS loading: 826.944 s
Root normalization: 50.529 s
Root -> FRI: 420.146 s
FRI -> KZG: 6,412.656 s
KZG -> recursive KZG: 4,544.567 s
Standalone verification: 1.499 s (CLI process)
Full environment audit: 1.679 s (CLI process)
The audit covers all 56,810 Init constants exactly once with zero
undischarged assumptions. Verification also passes without the SRS file.
Stage timings include preparation and verification, not only prover work.
Peak RSS values are process high-water marks. Setup is reusable.
Root: 608307acecf8cef1d9d188fb571343e45baeb3f907ff954c9feaaf01eecc5391
Proof: 8adee051c53cb06dce626d7625cf8ef55948a6340a7ae5b2fe0ff3844e3ab90a
Validation:
- Release Rust suites for ix-proof-compression and ix-ffi: 133 passed,
zero failed, one opt-in full-chain test ignored.
- Aiur normalization bounds and fixed-table behavior.
- Clippy with warnings denied, serial-feature build, rustfmt and diff checks.
- Lean CLI/test build and CLI integration tests.
- Saved full Init proof verified by the final CLI, including the environment
audit and verification using only local settings/key with no SRS.
- Generated fixtures cover native/constrained verifier agreement, malformed
inputs, statement binding, pairing/degree checks, and dense/streamed proof
equivalence. The expensive synthetic full-chain test remains opt-in;
the full production Init relation was exercised by the measured run.
Compress through a separate ix-compression-worker executable with authenticated Filecoin parameters, public-degree KZG and integrity-checked preprocessing caches. Verification uses exactly two application-bundled verifier profiles, Filecoin and development, with claim-bound fixtures; development parameters require --dev-srs on both compression and verification, which still check the proof, claim and pairings. Remove the local setup flow: `ix compression setup/layout`, the locally registered verifier directory, the rs_compression_layout extern and the setup-time root layout file. The bundled trust policy replaces them. Share circuit construction, lowering, statement schemas and prepared verification between the worker and the library stage APIs. Release frontend data before KZG proving, pass setup, cache and prefetch configuration explicitly to workers, and trace phases through IX_TEXRAY. The library keeps the general stage APIs, the normalized FixedRoot, multi-shard batch verification and witness-free verifier construction. Carry the improvements of the squashed FRI and recursive KZG compression into the restructured pipeline: - FixedRoot takes one log-height per system circuit and (width, circuit) memory pairs, matching the per-trace normalization in aiur. - stages::setup takes independent FRI, intermediate KZG and recursive KZG heights. - KZG keeps constant columns compact: interpolation, checkpoint loading and quotient slicing produce Column::Constant, which commits as a multiple of the first power and evaluates and opens without materializing coefficients. - SRS validation hashes through a streaming writer and bounds the MSM scratch by chunking adjacent-power pairs. - The FRI stage drops fixed evaluations, keys and witness-expansion data as soon as proving no longer needs them. Pin multi-stark to 2ed23ca (Plonkish proving improvements) for the witness and builder interfaces the stages use. CUDA proving lands separately.
Add the `cuda` feature of ix-proof-compression: KZG kernels compiled with nvcc into the worker run interpolation, commitments, coset evaluation, lookup and quotient construction, and opening divisions on NVIDIA GPUs, with device residency budgets, multi-device scheduling and optional SRS caching. CPU builds neither compile sppark nor link CUDA, and both paths produce the same proof bytes. Compact constant columns reach the device as their constant term, which the kernels zero-pad to the trace length. Link both the Lean executables and the compression worker against multi-stark's shared CUDA library instead of rewriting archives: Lake packages the library Cargo reports, executables load it from ../lib, and the CI CUDA job checks that its C++ runtime stays private and that the CLI and worker start without a GPU. CUDA compilation defaults to the detected GPU architectures; IX_KZG_CUDA_ARCHS and MULTI_STARK_CUDA_ARCHS keep explicit targets for headless builds. Document the GPU settings, NVMe and cache placement, capacity and retention, and cold/warm KZG benchmark boundaries, with the recorded Init KZG run on one RTX PRO 6000 Blackwell (471.87 s cold, 309.04 s warm, identical 2,181-byte packets). Pin multi-stark to sb/kzg-core at 416be66 (shared CUDA library and structured verification diagnostics). Only the multi-stark source entry changes in Cargo.lock.
Add an optional terminal PLONK stage that verifies the BLAKE3 KZG packet, including both pairing obligations, with two public claim-digest limbs. Recursive profiles move to version 6, whose final KZG transcript is BLAKE3; version 5 Keccak profiles still decode. Verification requires an independently authorized wrapper-key catalog. The `plonk` feature (on by default) exports the verifier relation of an authenticated profile: `wrap/outer/relation` validates the constraint graphs and fixed opening layouts and computes native differential vectors, and its `plonk` module emits the canonical scalar program and witness the gnark circuit consumes. Add the pinned gnark helper, parameter and artifact caches, native/FFI/CLI integration, the IxPlonkVerifier Solidity adapter under contracts/plonk, Lake/Nix packaging and Go CI coverage. A full Filecoin/BLAKE3 Init packet was wrapped and verified (recorded in tools/bls-plonk-wrapper/README.md): 21,184,618 constraints in a 2^25 domain, 127.17 s in plonk.Prove with keys prepared, 53.63 GiB peak prover RSS, 2.75 ms native verification and a 744-byte proof. The matching artifacts are archived in S3 with a pinned manifest digest.
Add an optional BN254 KZG pipeline beside the BLS12-381 default, selected by the `bn254` or `bls12-381` feature (IX_KZG_CURVE in Lake). BN254 keeps its own proof formats, setup identities, caches and verifier profiles, with native recursive field, curve, transcript, MSM and deferred-pairing constraints ported to it. The KZG backend, its SRS validation, compact constant columns and CUDA kernels are generic over the curve. Expose saved-root and saved-FRI pipeline commands with explicit development setup, claim binding and pinned-profile verification, plus a first-stage sizing preflight. Add authenticated Aztec Ignition import and admission for BN254, and curve-selectable terminal PLONK export, verification-key catalogs and CLI packaging. Split the profile relation into `wrap/outer/relation`, shared by the PLONK exporter. Classic GLV fits the real Init wrapper into a 2^24 domain with separate pairing checks. Add an optional native CUDA PLONK backend with pinned gnark/sppark patches, MSM/FFT dispatch, fused quotient computation and bounded Pippenger bucket accumulation for structured witnesses. contracts/plonk carries SP1's v6.1.0 BN254 PlonkVerifier with its circuit-key constants replaced and the IxPlonkVerifier claim adapter. Recorded measurements: real Init BN254 recursion has 61,151,005 rows padded to 2^26, against 118,389,942 rows at 2^27 for BLS12-381; three matched Init PLONK rounds took a 53.895 s median on CPU and 11.352 s with CUDA; the BN254 proof verifies on local Anvil through the claim adapter at 320,103 total transaction gas. docs/proof-benchmark-comparison.md compares warm Init proofs across the pipelines.
…FRI opening reduction The in-circuit FRI verifier recomputed, for every query and every opened column, the alpha power and the product with the shared opening denominator: three extension multiplications per column, two of which depend only on the claims. Fold the per-height alpha ladder and the alpha-weighted out-of-domain sums once before the query loop, so each query pays one extension-by-base product per opened column and one denominator product per (matrix, point). This ports the "hoist the query-invariant alpha work out of open_inputs" step of Plonky3 PR #2015 (commit a724a1aec0acab47384b34efc2a4d163e0351251) from the native verifier to the circuit. The reduced value, the alpha index of every column, the transcript and the proof bytes are unchanged; the circuit changes, so first-stage profiles and fixed preprocessing regenerate. Sized on the checked-in Init FRI key, the translated BN254 frontend goes from 1,125,583 to 554,220 gates and 312,920 to 141,070 lookups per query, 113.9M to 57.2M gates at 100 queries, and the first stage lowers to five 2^24 computation partitions instead of nine. Measured on one RTX PRO 6000 with development parameters, the warm first KZG stage went from 135.2 s to 92.2 s and peak RSS from 175.3 GiB to 114.4 GiB; the recursive stage natively verified the resulting proof and was unchanged at 76 s.
Record first-stage and recursive costs, direct-wrapper sizing, warm Ignition measurements, and gadget and lazy-nibble results in docs/compression-stage-collapse.md. Add the FRI sizing example and the FRI security-estimation script used for those figures. Require optimizations to preserve the current proven security bound.
Rename the recursive verifying key throughout, following SP1's usage
(`SP1VerifyingKey`, `vk`, `vk.bin`): the Rust type `VerifierProfile`
becomes `VerifyingKey`, `profiles/` becomes `verifying-keys/`, stage
outputs write `vk-id.bin` and `final-kzg/vk.bin`, the PLONK export is
`vk.json` with format `ix-{bn254,bls}-plonk-vk-v1`, and identifiers,
report keys, the worker's `plonk vk-blake3` subcommand, the Go helper
(`verifyingKey`, `VK`, `InnerVKSHA256`) and the Lean, Lake, Nix, CI and
Python references follow. The id derivation keeps its historical
`init-kzg-recursive-profile` label so every published verifying key id
is unchanged. Stage directories written before this change are not
readable by the new artifact names. The FRI proof-shape `ProofProfile`
and CPU-profiling names are unrelated and untouched.
Generalize the PLONK exporter and the gnark circuit from the two-circuit
recursive packet to any number of circuits: the opening layout, graph
inputs and scalar program take the circuit count from the system, claim
rows are exported as a schema of constants and public-scalar references,
intermediate lookup accumulators are carried per circuit, and the
deferred pairing is optional. `ix-compression-worker plonk export-first`
exports a saved first KZG stage directly. Keys without the new fields
keep the recursive defaults, so existing fixtures and keys are
unaffected. Compiling the export of the 15-circuit Init first proof
gives 130,850,185 constraints at domain 2^27.
Range-check the emulated Fq limbs, quotients and carries in 20-bit lookups against a 2^20-row table instead of 16-bit lookups against 2^16 rows. An Fq multiplication drops from 164 to 144 rows and an affine addition from 752 to 672, about 8% off every opening-MSM term; on the saved Init first proof the recursive frontend goes from 50,628,004 to 47,662,557 rows with the witness and external pairings passing. The merged table trace grows from 2^17 to 2^20 rows. Add two ignored counting tests that attribute rows to gadget components: the opening MSM's field operations, point operations, window tables, selects and whole-gadget scaling, and the first-stage verifier's Merkle level, row hashing, extension arithmetic, FRI round and transcript sampling. They run with `--ignored --nocapture` and print JSON.
BN254 halves the recursive stage's padded domain relative to BLS12-381 and is the target for further proving work, so select it by default. - Cargo: ix-proof-compression defaults to `bn254`, `plonk` and `parallel`; ix-ffi defaults to `bn254` and `plonk`. BLS12-381 builds with `--no-default-features --features bls12-381,...`; enabling both curves remains a compile error. - Lake: `IX_KZG_CURVE` defaults to `bn254`, and the PLONK helper's name and build tag follow the BLS12-381 selection instead of BN254. - Go helper: BN254 is the untagged build and `bls12381` selects BLS12-381, so `go test ./...` now covers BN254. - Nix: `.#plonk-wrapper` and `.#plonk-wrapper-cuda` are BN254, BLS12-381 is `.#plonk-wrapper-bls12-381`, and the Lake build uses the BN254 helper. - CI: the workspace jobs now exercise BN254; explicit steps cover the BLS12-381 crate (clippy and tests), the BLS12-381 Go helper, a BLS12-381 CUDA check and the BLS12-381 compression CLI, whose bundled verifying keys and packets are BLS12-381. - CLI: expose the compiled curve to Lean, report Ignition-setup proofs as such instead of as Filecoin, and make the compression CLI test check that a BN254 build rejects the bundled BLS12-381 packets. The BN254 verifying-key catalog stays empty: release verification on the default build needs a caller-supplied verifying key until an Ignition key is published.
Include the zero-anchor claim row when exporting recursive packets so all 22 public values and their anchor are represented in the wrapper circuit. Add a small-proof regression covering the complete schema and changed claims. Refresh the BN254 PlonkVerifier constants, proof fixture and provenance in contracts/plonk for the optimized Init recursive proof using admitted Ignition parameters, and record its GPU proving, independent CPU verification and local EVM results. As recorded, the GPU proof took 11.557 s in plonk.Prove and the ix adapter verification transaction used 320,091 gas.
Pin multi-stark to d8c950be (sb/kzg-core), which makes ByteValue nibbles optional: byte selects in the compact BLAKE3 lowering produce value-only bytes, and the paths that read nibbles materialize them on demand with the same constraints. Only the multi-stark source entry changes in Cargo.lock. Recorded results (docs/compression-stage-collapse.md): the first KZG stage drops from 77.07M to 60.59M used rows and from five to four 2^24 computation partitions, with 57.23M to 40.75M translated gates at 100 queries. On a warm GPU run the first stage went from 93.4 s to 80.6 s and its peak RSS from 114.4 GiB to 99.3 GiB.
…acing test - Raise the FRI blowup in fri_memory_reduction_preserves_the_dense_proof to 2, matching the neighbouring stage tests: the lowering now produces degree-4 constraints, which a blowup of 1 cannot support. - Run the partitioned-proving tracing test on a private rayon pool. While blocked inside the examined span, a thread could steal rayon jobs from concurrently running tests and count their spans as its own children. - Drop a redundant std::io qualification in the SRS cache constructor.
Replace truncating usize-to-u32 casts with checked conversions, borrow the lookup values as a one-element slice instead of cloning them, and gate the full-scale primitive benchmark on the `parallel` feature instead of asserting a constant.
Make BN254 unconditional for KZG and terminal PLONK. Remove Filecoin setup, BLS verifier catalogs, legacy contracts, fixtures, and curve build options. Rename the PLONK helper and update Lake, Nix, CI, and current documentation. Retain shared gnark/BLST support and fail-closed rejection of legacy formats. Validation: focused KZG and pipeline tests, BN254 tests without default features, CPU PLONK helper tests, all-target Clippy, Rust/Go formatting, Lean typechecks, seven Lake configurations, and Nix helper evaluation. GPU and full Init proving were not rerun. Rust checks used the separately updated multi-stark revision fd22b637 in the working tree.
Pin multi-stark to ea4cf6976462612ccd03255eacc1f8cc1cfe43fb after PR #93 merged into main. Its source tree is identical to the previously tested fd22b637 revision (tree 5fe11c46cbfed3d59a800f00e198023ec3ab6460). Update the manifest and matching lockfile source without changing any package versions. Locked workspace metadata and git diff --check pass; no rebuild is needed for the identical upstream source tree.
Build CPU and CUDA helpers from the same pinned upstream gnark module. Remove gnark patches, private module copies, vendor patching, fused quotient dispatch, and native version plumbing. Init benchmarks showed only a 1% median proving-time improvement from fusion. Keep classic GLV and separate pairing checks. Remove unused circuit variants, the legacy SP1 Lagrange importer, and capture/replay and sizing experiments. Consolidate profiling in the full Init test, require explicit verifier schema fields, and key Lagrange caches by setup, domain, and monomial receipt. Validation: CPU/CUDA builds and focused tests passed. The compiled Init constraint system is byte-identical, and a full CUDA Init proof passed independent CPU verification and altered-claim rejection. The Nix CUDA helper derivation evaluates successfully.
Wrap an aggregate root once more through ix_aggr and prove the wrap in a fixed, all-active, single-shard layout, so every root that fits the layout compresses under the same FRI verifier regardless of its shard count or trace heights. - aiur: per-circuit execution rows, layout sizing with headroom, and memory circuit order for normalized proving. - FixedRoot: canonical JSON layout, accessors and a backend-plus-layout identity. - FRI worker: verify through FixedRoot when the root directory carries fixed-root.json, taking memory ends as inputs instead of constants. - CLI: `ix compression layout` sizes one layout over several roots, `ix compression normalize` writes a normalized worker input, and `ix compress --fixed-root` normalizes before compressing. Init (3 shards) and Nat.add_comm (1 shard) roots normalized to one layout produce identical FRI verifier circuits (49,303,266 gates, 4 x 2^24 + 2^23 partitions), and both satisfy every constraint in FRI check-only mode.
Add CPU and ICICLE CUDA proving, explicit development setup and admitted key catalogs, and Solidity verification for the existing KZG relation. Wire terminal selection through Lean and Rust while preserving fixed-root normalization. Include proof fixtures and the matched Groth16/PLONK comparison. Focused Rust clippy, Go regression tests, and Solidity tests passed after the port; Lean/FFI rechecks remain deferred.
Call stock gnark through one C archive for PLONK and Groth16, with retained prover handles and Rust-owned artifact preparation and publication. Keep the Go runtime inside ix-compression-worker and select acceleration with the terminal backend features plus cuda. Remove the Go helper builders, package ICICLE with the worker, and trace native libraries, headers, and builder inputs in Lake.
Compression now runs in the ix process through `pipeline::compress(CompressInput, &CompressConfig)`: FRI, first KZG, recursive KZG and an optional PLONK or Groth16 terminal, keeping the on-disk stage directories. Each stage writes a `complete` marker last; rerunning `ix compress` with the same output directory reuses completed stages and refuses a directory whose root does not match. Pooled GPU memory is returned to the driver after normalization and after each stage (multi-stark `release_device_memory`). Removed: the ix-compression-worker executable and its subcommands, process spawning and capability checks, IX_COMPRESSION_WORKER, the worker Lake target, Nix packages and CI step. Release and key tooling (PLONK export and parameters, Groth16 compile/setup/import, pinned-key verification) remain library functions without a CLI. Builds without `plonk` or `groth16` reject those proofs with an error naming the switch. Native code: the KZG and PLONK CUDA kernels build into one libix_bn254_cuda.so against one sppark, with a private C++ runtime and only C exports, so it can share a process with Lean's runtime. Build scripts report runtime files (that library, and ICICLE with its backend plugins) in IX_RUNTIME_ARTIFACTS; Lake copies exactly those and links them through ld scripts. sppark_namespace.h, the standalone PLONK build, IX_PLONK_CUDA_LIBRARY and related variables are gone. Build switches mirror the Cargo features: IX_PLONK and IX_GROTH16 are off by default, so compression ends at the recursive KZG proof and the default build needs no Go; terminal features compile into ix only. IX_KZG_CURVE is removed. Groth16 CUDA links an installed ICICLE (/usr/local or IX_GROTH16_ICICLE_ROOT). CLI: `ix prove --ixe E --ixes M` proves and aggregates on every visible GPU by default (`--gpus`, `--shards-only`; `--lanes` is removed), and `--compress kzg|plonk|groth16` continues to a compressed proof, checking the setup before proving. One-shard manifests are wrapped into a root. `ix compress layout|normalize|fetch-params` replace `ix compression`. `fetch-params` downloads the pinned public Ignition files, which compression then finds without IX_KZG_IGNITION_* variables. Compression normalizes to the bundled release root layout unless `--fixed-root` overrides it. Fixed-preprocessing cache entries are keyed by format and stage verifying key, and PLONK circuit caches by format, circuit description, setup and gnark's go.sum, instead of the executable digest, so rebuilding ix keeps them. Validated on Nat.add_comm with admitted Ignition parameters: the compressed proof and recursive verifying key are byte-identical to the process-per-stage pipeline; peak host RSS 190 GB, peak GPU 95.8 GB. Pins multi-stark 1b5b65d (release_device_memory and a workaround for Plonky3's twiddle-cache deadlock) and sppark 9326ac0 (upstream-merged dev with the split-bucket MSM the PLONK kernels use).
Replace the worker command walkthroughs with `ix compress`, `ix prove --compress` and the `pipeline::compress` library flow: resume by rerunning with the same output directory, `ix compress fetch-params` and IX_PARAMS_DIR, the IX_PLONK/IX_GROTH16 switches, and the single libix_bn254_cuda.so. Key and release tooling is described as library functions. The `--out` help now states that a rerun resumes.
…a proof Bundle one key per proof system in verifying-keys/0.1/ with its layout, statement prefix and Ignition admission, pinned in pipeline/verifying_keys.rs. `ix verify` checks a proof's key identifier against the bundled key for its tag; the PLONK and Groth16 catalogs are removed, and the development Groth16 key requires --dev-srs. Add pipeline::derive_recursive_vk and plonk::derive_verifying_key, which derive the bundled keys from trusted inputs alone by sharing each stage's construction with the proving path; ignored tests reproduce both byte for byte. Remove the old non-matching pipeline::setup. Rename the first KZG stage's claim-dependent vk-id.bin to instance-id.bin.
- Reuse a checkpointed stage only when its proof verifies; drop the completion markers and --log-height. - Rename the terminal stage to final. - Key the PLONK circuit cache on the gnark source digest. - Share the CUDA build helper between aiur and proof-compression. - Move the analysis scripts to tools/compression and drop unused examples and fixtures.
Delegate final-contribution verification to gnark-ignition-verifier and load the standard gnark SRS (srs.bin), removing the custom transcript verification, cache receipts and admission metadata. The release keys and parameters are unchanged. The generator reads the Ix mirror of the final two contributions by default. Default the crate to parallel only, naming the gnark features in CI.
Stages read fixed preprocessing from the cache entry in place and publish moves it there; restoring used to copy ~69 GB into every compression output when the cache was on another filesystem. `ix compress setup` downloads srs.bin if missing, checks its pinned SHA-256, and derives and publishes the preprocessing of every bundled stage not already cached. It replaces `ix compress fetch-params`.
Fold pipeline/stages into the pipeline modules that use it (stage, lowering, claims, root, wrap/recursive) and fold single-function files into their callers. Rename the development SRS file cache and the GPU SRS residency module apart, and tools/plonk-wrapper to tools/gnark, which also proves Groth16 and converts the Ignition SRS. Drop the vendored SP1 Solidity verifier. The PLONK verifier is now gnark's own export of the bundled release key, written by tools/gnark/cmd/solidity; it is byte-identical to the verifier key preparation writes. Read nvcc, the CUDA architectures and the CUDA library directories from multi-stark's build metadata instead of rediscovering them in aiur and proof-compression; this removes crates/build_support. Merge the integration tests into one binary and remove benchmarks and cost reports posing as tests, tests that re-prove only to compare bytes with an older code path, tests made redundant by stronger ones, BLS12-381-era cases and unwired scripts. Test temporary directories share one RAII helper. Rename the aggregation "lanes" to multi-GPU (proveMultiGpu, --gpus, AIUR_PROOF_CACHE_DIR). CI: fix the compression CLI test for the current setup errors, expect the KZG backend in the CUDA link smoke test, fix clippy casts in the gnark SRS test, and stop installing Go in the bench workflows, whose builds no longer need it.
Lake now runs Cargo on every build and lets it decide what is stale, instead of keeping its own list of Rust inputs and toolchain variables. It snapshots the archive and the shared libraries the build scripts report, and targets relink only when the archive's contents change. The proof-compression build script lists every library an executable needs in IX_RUNTIME_ARTIFACTS, including multi-stark's, marked linked or runtime-loaded; with CUDA, each Rust archive links through an ld script naming the archive and its linked libraries, so no target names the CUDA runtime and the lakefile no longer knows library names or ICICLE paths. The C17 flag for Lean's older glibc stubs moves to .cargo/config.toml, so plain cargo builds match. Parse every IX_* build flag one way (1/true/yes). The compression CLI checks run as `lake test -- compression-cli` instead of a separate executable. Stop testing PLONK and Groth16 in CI for now: drop the Go test job, the plonk/groth16 features from the Rust checks, ICICLE and Go from the CUDA compile job, and the compression CLI test from the Ix CLI suite. The flake has no working GPU setup, so remove its CUDA package set, toolkit, dev shell, ICICLE package, Go toolchain, gnark check and the orphaned nextest-ignored package.
samuelburnham
force-pushed
the
kzg-bn254
branch
from
October 30, 2026 20:28
2f95609 to
5d9551a
Compare
Squash-merge of argumentcomputer/multi-stark#98; same tree as the previously pinned PR head c270c9d.
arthurpaulino
previously approved these changes
Nov 2, 2026
Drop the IX_CUDA=0 linkage step, the readelf/nm runtime-privacy check and the compression CLI GPU-less smoke test with its LD_PRELOAD shim, and the cmake, ninja-build and python3 packages left over from the ICICLE build and the worker capabilities check.
samuelburnham
marked this pull request as ready for review
November 2, 2026 20:15
samuelburnham
enabled auto-merge
November 2, 2026 20:57
arthurpaulino
approved these changes
Nov 2, 2026
samuelburnham
added a commit
that referenced
this pull request
Nov 4, 2026
Merges origin/main (426a242, "feat: KZG on BN254 (#675)") into the formal Aiur integration (PR 678 plus the formal port). PR 678 retired legacy Aiur, IxVM and MultiStark; main's KZG commit changed them in place. Main's legacy-side changes resolve to deletion; the compression crate, its CLI and the build plumbing are kept and moved onto the formal aggregation backend. Resolution: - Deleted: main's edits to legacy Aiur (`crates/aiur/src/synthesis*`), the legacy aggregate controller and multi-GPU driver (`crates/ffi/src/aiur/**`, including the legacy root normalizer `normalize.rs`), `crates/ffi/src/kernel.rs`, `Ix/Aggr/{Backend,FFI}`, `Benchmarks/Typecheck.lean` and `Tests/AggrActivation.lean`. The formal controller's lanes, scheduler and record pool keep PR 678's versions, as do `ix aggregate`, `ix shard` and the GPU proving docs. - Kept from main: `crates/proof-compression`, `tools/gnark`, `contracts`, the compression FFI and `ix compress`, Lake's runtime-artifact linking and feature selection (with the formal native kernels), the CFLAGS pin, the flake's compression fixtures and test sources, and main's removal of the separate CUDA dev shell. - multi-stark is pinned to d13dc8d (formal-aiur/kzg-merge in the fork): main's 3515632 and the integration's ed65a7c merged, plus a fix for the CUDA lookup graph reading spilled preprocessed traces from the host. aiur's build script takes its CUDA toolchain from multi-stark's build. Compression on the formal backend: - ix-proof-compression depends on the formal `aiur` crate only. RootKey wraps the formal VerifyingKey (which now exposes its system, parameters and policy-only preamble validation, and MEMSEG_CHANNEL) and checks roots and fixed layouts under formal Aiur's batch policy. Fixed-layout identities are domain-separated from the legacy backend's. The FRI stage's outer proof uses fixed recursion parameters (blowup 4, 100 queries, 20 query PoW bits). - Legacy root compression is removed: the release-layout lookup, the legacy root rows/layout/normalize FFI, and setup's preprocessing of the bundled version, which needed the legacy backend key. The bundled 0.1 keys stay as Ignition anchors and still verify proofs of that release. `ix compress setup --fixed-root LAYOUT` instead prepares the KZG stages for the formal artifact's key and that layout. - `ix compress derive-vk` derives the recursive key of the formal artifact and a layout; `ix verify` verifies compressed proofs under `--compression-vk` and its `--compression-vk-blake3` pin, with the statement derived from the formal artifact, or under the bundled keys, and accepts development final proofs with `--verifier-bundle`. - Compressing a root requires its normalization, which the next commit adds; until then `ix compress` refuses roots.
samuelburnham
added a commit
that referenced
this pull request
Nov 5, 2026
Merges origin/main (426a242, "feat: KZG on BN254 (#675)") into the formal Aiur integration (PR 678 plus the formal port). PR 678 retired legacy Aiur, IxVM and MultiStark; main's KZG commit changed them in place. Main's legacy-side changes resolve to deletion; the compression crate, its CLI and the build plumbing are kept and moved onto the formal aggregation backend. Resolution: - Deleted: main's edits to legacy Aiur (`crates/aiur/src/synthesis*`), the legacy aggregate controller and multi-GPU driver (`crates/ffi/src/aiur/**`, including the legacy root normalizer `normalize.rs`), `crates/ffi/src/kernel.rs`, `Ix/Aggr/{Backend,FFI}`, `Benchmarks/Typecheck.lean` and `Tests/AggrActivation.lean`. The formal controller's lanes, scheduler and record pool keep PR 678's versions, as do `ix aggregate`, `ix shard` and the GPU proving docs. - Kept from main: `crates/proof-compression`, `tools/gnark`, `contracts`, the compression FFI and `ix compress`, Lake's runtime-artifact linking and feature selection (with the formal native kernels), the CFLAGS pin, the flake's compression fixtures and test sources, and main's removal of the separate CUDA dev shell. - multi-stark is pinned to d13dc8d (formal-aiur/kzg-merge in the fork): main's 3515632 and the integration's ed65a7c merged, plus a fix for the CUDA lookup graph reading spilled preprocessed traces from the host. aiur's build script takes its CUDA toolchain from multi-stark's build. Compression on the formal backend: - ix-proof-compression depends on the formal `aiur` crate only. RootKey wraps the formal VerifyingKey (which now exposes its system, parameters and policy-only preamble validation, and MEMSEG_CHANNEL) and checks roots and fixed layouts under formal Aiur's batch policy. Fixed-layout identities are domain-separated from the legacy backend's. The FRI stage's outer proof uses fixed recursion parameters (blowup 4, 100 queries, 20 query PoW bits). - Legacy root compression is removed: the release-layout lookup, the legacy root rows/layout/normalize FFI, and setup's preprocessing of the bundled version, which needed the legacy backend key. The bundled 0.1 keys stay as Ignition anchors and still verify proofs of that release. `ix compress setup --fixed-root LAYOUT` instead prepares the KZG stages for the formal artifact's key and that layout. - `ix compress derive-vk` derives the recursive key of the formal artifact and a layout; `ix verify` verifies compressed proofs under `--compression-vk` and its `--compression-vk-blake3` pin, with the statement derived from the formal artifact, or under the bundled keys, and accepts development final proofs with `--verifier-bundle`. - Compressing a root requires its normalization, which the next commit adds; until then `ix compress` refuses roots.
johnchandlerburnham
added a commit
that referenced
this pull request
Nov 6, 2026
Brings in #675 (426a242) with the formal Aiur bridge from jcb/certified-compression (d9ac196): crates/proof-compression and the compression FFI and CLI run on aiur::trace::stark and MultiStark::ix_aggr shape 1, and multi-stark is pinned to main (3515632), which the compression Plonkish backend needs. The Lean certification of compression (Ix/Cert/Compression, its module audit guards and docs/certified-compression.md) stays on jcb/certified-compression. d9ac196 is not an ancestor, so merging this branch there keeps it.
johnchandlerburnham
added a commit
that referenced
this pull request
Nov 6, 2026
johnchandlerburnham
added a commit
that referenced
this pull request
Nov 6, 2026
#677's history after 05cc396 is squashed into fb8e986 (tree of 38f0340; #675's 426a242 kept as a parent so the compression bridge merges against #675's original files). - Legacy Aiur, IxVM, MultiStark and codegen files #677 changed stay deleted. Their semantics reach the formal programs by regeneration: tools/ixvm/adapt.py and recursion.py now read Ix at 38f0340 (self-assumption and duplicate-discharge checks, user axioms in claims, RoleSpecGen CSE). run_check_env's pointer-identity guard against an empty owned tree becomes a reviewed refutable Cons pattern. - The security fix's regressions move to the formal harnesses: Tests/FormalAiur.lean (Check/CheckEnv self-assumption, empty owned tree) and Tests/FormalAggregate.lean (duplicate and self-discharging joins, overlapping subjects). - ClaimContext.ofEnv keeps #678's bindingAssumed and gains #677's user axiom tree; ClaimHarness takes #677's assumeBinding/user-axiom scope. - #677's deletions win where #678 had only kept code alive: ix-bench (its two helpers move into the stark-verifier compare example), shardManifestFromPartition, dead ffi dependencies, retired suites and CI jobs. Tests/Main.lean starts from #677's registry minus the legacy suites #678 retired. - ProveCmd: --compress is refused with --assume-binding, as #677 refuses aggregation. - CI: drop ixon/sharing-profile, which no ixon version defines.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
After argumentcomputer/multi-stark#98