ROADMAP.md

AppleZKProver Roadmap

This project is an Apple-silicon-first backend for hash-heavy transparent proving. The near-term target is not a broad cryptography catalog; it is a GPU-resident prover substrate where hash commitments, field lanes, codeword/PCS work, and sumcheck rounds can be composed without avoidable CPU synchronization.

Current State

• CPU oracle: full SHA3-256, Keccak-256, and SHA3 Merkle roots.
• GPU hash: rate-bounded SHA3-256 and Keccak-256 for 0...136 byte messages.
• GPU specialization: exact 32-byte, 64-byte, 128-byte, and full-rate 136-byte SHA3/Keccak kernels.
• GPU Keccak-F: permutation-only batch plans are implemented with a scalar baseline kernel, opt-in Apple7+ simdgroup kernel, CPU differential tests, and standalone JSON benchmark reports.
• GPU Merkle: raw leaves are uploaded once, parents stay GPU-resident, small upper-tree reductions are fused in threadgroup memory, and only final public material is copied back. Lower-subtree treelet kernels now cover the fixed-rate SHA3 leaf contract (0...136 bytes), use race-free ping-pong threadgroup scratch, and can be selected by the planner after correctness-gated races. Raw-leaf opening extraction now copies back only the requested sibling path plus the root, emits lower-path nodes during treelet root construction when configured, and has independent CPU verification.
• GPU M31/CM31/QM31: canonical CPU oracle operations and reusable Metal vector plans now cover M31 add, subtract, negate, multiply, square, inverse, and dot product; CM31 add, subtract, negate, multiply, and square over M31[X]/(X^2 + 1); and QM31 add, subtract, negate, multiply, square, and inverse over CM31[U]/(U^2 - 2 - i). QM31 radix-2 FRI fold command plans now include both a single-layer resident fold and a chained multi-round resident fold that encodes all requested rounds into one command buffer. The chain supports explicit challenges, a transcript-derived mode that absorbs 32-byte per-round commitment roots, and a Merkle-bound transcript mode that commits each current resident QM31 layer before deriving the next challenge. A linear QM31 FRI proof format now serializes transcript-sampled query decommitments, has an independent CPU verifier, and has a dedicated zkmetal-bench --qm31-fri-proof timing mode for proof construction, deterministic serialization, strict deserialization, and verification. Inputs are canonicality-checked at the public array boundary, zero is rejected for inversion and public inverse-domain fold inputs, and GPU results have CPU-verified execution.
• Circle PCS and application artifact: the implemented Circle FFT-basis slice now has a production-facing conservative128 parameter profile, a strict CPU verifier contract over committed-polynomial semantics, a conservative soundness note, a checked-in canonical proof corpus with tamper/rejection vectors, a code-level PCS scope manifest, verifier-checked nonzero grinding support for lower-level V1 artifacts, a resident monomial coefficient witness-column to Circle FFT-basis producer, a resident private column-major M31 witness to row-major AIR trace synthesis plan, and a fused final-FFT-stage first-layer leaf-hash commitment schedule. ApplicationProofV1 now binds witness, AIR, and GKR digests to verified M31 sum-check chunk and Circle PCS proofs in one final statement-bound artifact, while M31MultilinearSumcheckProofV1 and AIRConstraintMultilinearSumcheckProofV1 add a public full multilinear AIR-reduction sumcheck sidecar. AIRProofV1 adds a strict public revealed-trace AIR proof scaffold with transcript-composed constraint evaluations and CPU public trace quotient-divisibility validation. AIRProofQuotientPCSArtifactV1 adds a public PCS-backed quotient low-degree layer for packed quotient coefficient chunks, while explicitly leaving privacy, zero-knowledge, and succinct AIR/GKR theorem proof integration open. ApplicationProofClaimScopeV1 and ApplicationProofVerificationReportV1 make the accepted implemented slice distinct from the unsupported witness/AIR/GKR theorem in the proof bytes alone. ApplicationTheoremVerifierV1 adds a public sidecar theorem path that checks named-layout witness-to-AIR trace production, AIR semantics, AIR-to-sum-check reduction, and CPU GKR claim semantics when sidecars are provided. AIRTraceToCirclePCSWitnessV1 packs public AIR trace rows into QM31 CirclePCSFRIPolynomialClaimV1 chunks for arbitrary AIR column layouts, AIRTraceToCircleFFTBasisWitnessV1 derives matching Circle FFT-basis chunks for those public layouts, AIRTraceCirclePCSProofBundleV1 proves every generated chunk with the strict Circle PCS contract and now has strict bundle encoding/digest support, AIRTracePCSOpeningConstraintVerifierV1 checks AIR constraints directly on PCS-opened trace rows with complete-coverage reporting, AIRTracePCSOpeningQueryPlannerV1 derives public AIR query rows from initial trace PCS commitments, AIRTraceQuotientPCSQueryAlignmentVerifierV1 checks matching public quotient PCS openings at those query storage indices, AIRSharedDomainQuotientIdentityPCSProofBundleV1 checks N(z) = Z(z) * Q(z) over shared row-domain trace, shifted-trace, and quotient PCS openings, ApplicationPublicTheoremTracePCSArtifactV1 binds that trace bundle to the public theorem artifact, ApplicationPublicTheoremArtifactV1 packages the public sidecars with the statement and proof into one self-contained public theorem artifact with stable digest corpus coverage, and ApplicationPublicTheoremIntegratedArtifactV1 combines the public theorem, AIR sumcheck, quotient identity, and GKR reports into one public verifier surface with strict encoding, domain-separated digests, and integrated corpus coverage. This does not complete AIR semantic verification over private resident traces, a succinct AIR/GKR proof, zero-knowledge masking for the M31 chunk, or external parameter review.
• Runtime: Apple GPU family detection, nonuniform dispatch, reusable hash/Merkle execution plans with explicit buffer clearing, CPU-verified accelerator APIs, KernelSpec-keyed pipeline cache, optional Metal binary archive persistence, ring-buffered shared upload staging, private residency arenas, and SQLite plan history.
• Bench: warmups, repeated measurements, CPU verification, text output, and JSON output.
• Baselines: first optimized Apple M4 / Apple9 suite baseline is checked in under BenchmarkBaselines/.

Phase 0: Measurement Discipline

Every performance claim must be backed by a benchmark artifact generated by zkmetal-bench --json. Benchmark reports must include:

• exact device name and registry ID,
• Apple GPU family capability flags,
• leaf count, leaf length, warmup count, iteration count,
• standalone hash function,
• pipeline archive mode and path,
• wall-time samples,
• GPU-time samples when Metal reports them,
• root and CPU verification status.

Exit gate:

• swift test passes.
• swift test -c release -Xswiftc -Osize passes while the current Swift release -O throwing-codegen issue remains reproducible on the benchmark host.
• zkmetal-bench --json works for leaf lengths 0, 32, 64, 135, and 136.
• benchmark JSON is stable enough to check into BenchmarkBaselines/ for each measured machine. The first Apple M4 / Apple9 baseline is checked in.
• benchmark JSON records device threadgroup memory, selected Merkle subtree leaf count, and selected upper-fusion node limit.

Phase 1: Runtime Substrate

The runtime must make expensive host work explicit and controllable.

• Keep all pipeline creation outside timed benchmark regions.
• Use binary archives when configured, but keep library default side-effect-free.
• Add a GPU scratch arena for long-lived private buffers beyond the current hash/Merkle plans. The first ResidencyArena is implemented for Merkle and transcript state.
• Add a ring-buffered upload path for shared staging buffers. The first SharedUploadRing is implemented and used by reusable Merkle and M31 sum-check plans.
• Extend command-plan objects from hash and Merkle construction into future PCS passes.
• Add kernel autotuning records keyed by device registry ID, OS build, shader hash, protocol hash, workload shape, and threadgroup geometry. SQLite plan history is implemented for Merkle races.
• Promote the lower Merkle subtree path from explicit benchmark mode to automatic selection only after correctness-gated records show a net win for a given device and tree shape.

Exit gate:

• timed benchmark regions do not compile pipelines,
• timed benchmark regions do not allocate avoidable scratch buffers,
• Merkle commit can reuse caller-visible execution plans and private scratch buffers with explicit clearing.

Phase 2: Hash And Merkle Leadership

This is the first performance battlefield.

• Keep one-thread-per-Keccak-state kernels as correctness baselines.
• Implement Apple7+ simdgroup-cooperative Keccak-F1600. The first path is implemented, CPU-differential-tested, wired into selectable fixed-width SHA3/Keccak batch kernels, and benchmarked with explicit independent-state packing per threadgroup; current Apple M4 / Apple9 measurements are slower than scalar, so it remains opt-in and planner-ineligible.
• Specialize SHA3 paths for 32-byte, 64-byte, 128-byte, and full-rate 136-byte absorbs. The 32-byte, 64-byte, 128-byte, and full-rate 136-byte SHA3/Keccak paths are implemented.
• Keep Keccak-256 domain handling separate from SHA3-256 and add Keccak-domain Merkle only as a distinct commitment API.
• Add Keccak-F permutation-only batch kernels for Plonky3-style benchmark relevance. Scalar and opt-in simdgroup batch plans are implemented with CPU verification and a dedicated zkmetal-bench --keccakf-permutation JSON report.
• Extend fused threadgroup-local Merkle subtree kernels beyond 32-byte leaves where measurements justify it. The fixed-rate extension covers 0...136 byte SHA3 leaves with CPU/GPU differential tests. After the race-free ping-pong scratch fix, Apple M4 / Apple9 automatic smoke measurements promote only the near-rate 135- and 136-byte shapes; other shapes require explicit fixed mode or planner tuning records.
• Extend fused multi-level parent reduction into more tree shapes where measurements justify it.
• Add proof-node extraction kernels so Merkle openings can remain mostly GPU-resident. Raw-leaf SHA3 openings now have CPU opening construction, CPU proof verification, scalar-level GPU extraction, combined treelet root/lower-sibling extraction, and JSON benchmark coverage.

Exit gate:

• benchmarked Merkle throughput improves over the one-thread baseline on M3/M4-class Apple9 GPUs,
• CPU/GPU roots match for randomized and deterministic leaves,
• no intermediate Merkle levels are read back by default; only final roots and requested opening nodes are host-visible.

Phase 3: Prime Field Lanes

Field arithmetic should start with transparent proving ecosystems, not pairing-heavy systems.

Priority order:

1. M31 for Circle-STARK/Stwo-style work.
2. BabyBear and KoalaBear for Plonky3-compatible work.
3. Goldilocks for existing STARK workloads.
4. Binary tower fields for Binius/GKR-style work.
5. BN254/BLS12-381 only after the transparent path is mature.

Required kernels:

• vector add, subtract, negate. The first canonical M31 reusable vector plan is implemented with CPU oracle tests,
• vector multiply and square. The first canonical M31 reusable vector plan is implemented with CPU oracle tests,
• extension-field multiply. The first CM31 CPU oracle and reusable Metal vector arithmetic plan are implemented for M31[X]/(X^2 + 1). The first QM31 secure-field CPU oracle and reusable Metal vector plan are implemented for CM31[U]/(U^2 - 2 - i), including multiply, square, inverse, uploaded-buffer execution, CPU/GPU differential tests, and JSON benchmark reporting,
• batch inverse. A CPU Montgomery batch-inversion oracle and first GPU M31 vector inverse path are implemented with zero rejection, CPU/GPU differential tests, and JSON benchmark reporting,
• dot products and reductions. The first reusable M31 dot-product plan is implemented with CPU oracle tests, uploaded-buffer execution, explicit clearing, and a benchmark report that records elements/sec plus input bandwidth,
• layout transforms for FRI/codeword stages. QM31 radix-2 FRI folding now has a CPU oracle, Metal kernel, single-layer resident executeResident path, chained multi-round resident command plan, transcript-derived chain challenge mode, Merkle-bound layer-root challenge mode, linear query/decommitment proof serialization, independent verifier tests, and JSON benchmark reporting. Canonical Circle domain points, Circle FFT twiddles, and Circle FRI inverse-domain layers now have GPU-resident materialization with CPU/GPU parity gates. The Circle PCS/FRI slice has a fixed conservative verifier profile, while full proof-system parameter review remains open.

Exit gate:

• every field operation has CPU reference tests,
• randomized differential tests cover edge values,
• benchmark reports include elements/sec and effective bandwidth.

Phase 4: Codeword And PCS Engine

The project should then move from hashing trees to generating the data that those trees commit to.

• Implement tiled matrix/codeword kernels.
• Implement FRI fold kernels over the selected field. QM31 radix-2 folding is implemented for caller-supplied inverse-domain points with resident buffer output, including a multi-round command scheduler that keeps intermediate layers in private GPU scratch, a transcript-derived challenge path that consumes 32-byte per-round commitment roots without CPU challenge round-trips, and a Merkle-bound path that commits the actual current resident QM31 layer buffers before deriving the next challenge. Linear query sampling, Merkle decommitment extraction, verifier-facing proof serialization, an independent CPU verifier, and a proof/verifier benchmark mode are implemented for this radix-2 layout. Circle-domain proof V1 now has GPU-resident domain/twiddle materialization, a resident Circle FFT codeword plan for P(x) + yQ(x), a resident monomial coefficient witness-column to Circle FFT-basis producer, resident private M31 witness-column to AIR trace synthesis, a single explicit Circle FFT-basis coefficient-to-proof command-plan surface with final-FFT-stage first-layer leaf hashing, a strict production-facing PCS verifier contract, a scope manifest, verifier-checked lower-level grinding nonce support, and a reproducible proof corpus. ApplicationProofV1 composes verified M31 sum-check chunk and Circle PCS proofs under one public statement digest, AIRProofV1 verifies public revealed-trace AIR constraint composition and CPU public quotient divisibility, AIRProofQuotientPCSArtifactV1 proves packed quotient chunks with Circle PCS, ApplicationTheoremVerifierV1 verifies AIR/GKR semantics for public sidecars, AIRTraceToCirclePCSWitnessV1 bridges public AIR trace layouts into structured PCS claims, AIRTraceToCircleFFTBasisWitnessV1 derives matching Circle FFT-basis chunks for those public layouts, AIRTraceCirclePCSProofBundleV1 proves and strictly encodes those public trace chunks, AIRTracePCSOpeningConstraintVerifierV1 checks AIR constraints directly on PCS-opened trace rows with complete-coverage reporting, AIRTracePCSOpeningQueryPlannerV1 derives public AIR query rows from initial trace PCS commitments, AIRTraceQuotientPCSQueryAlignmentVerifierV1 aligns public trace and quotient PCS openings at the sampled storage indices, AIRSharedDomainQuotientIdentityPCSProofBundleV1 checks the row-domain quotient identity at shared PCS openings, ApplicationPublicTheoremTracePCSArtifactV1 binds the trace PCS bundle to the public theorem artifact, ApplicationPublicTheoremArtifactV1 encodes a self-contained public theorem artifact with stable corpus coverage, and ApplicationPublicTheoremIntegratedArtifactV1 now encodes the public AIR sumcheck plus shared-domain quotient-identity surface with corpus-pinned digests. Remaining work is AIR semantic verification over private resident traces, succinct AIR/GKR proof integration, zero-knowledge masking for the M31 chunk, a reviewed production profile that assigns grinding credit, and external cryptographic review.
• Implement layout transforms: linear, bit-reversed, tiled, Morton-order where useful.
• Avoid random global writes in encoder paths unless benchmarks prove the tradeoff.
• Compose codeword generation and Merkle commitment in one command plan.

Exit gate:

• codeword generation can feed Merkle commitment without CPU readback,
• a benchmark reports codeword throughput plus Merkle/proof throughput for the same command-plan surface while disallowing full-codeword and intermediate-FRI-layer readback.

Phase 5: Sumcheck And GKR

Sumcheck is where Apple7 SIMD reductions and Apple9 64-bit atomics become important.

• The first M31 chunk now keeps round coefficients, framed transcript challenge generation, and fold/halve on GPU with multi-block transcript absorb. A CPU verifier-facing M31SumcheckProofV1 checks the narrow chunk transcript and is embedded in ApplicationProofV1; M31SumcheckVerificationReportV1 classifies that legacy chunk as a revealed evaluation-vector folding trace.
• M31MultilinearSumcheckProofV1 now implements the public full multilinear evaluation-table protocol with transcript-derived challenges and (1-r) * f(0) + r * f(1) folding, and AIRConstraintMultilinearSumcheckProofV1 binds that proof to the canonical AIR reduction vector with a zero-sum claim. This is public and revealed-vector, not zero-knowledge.
• Implement batched resident multilinear evaluation for the public protocol shape.
• Add simdgroup reduction variants.
• Add Apple9 atomic accumulation variants where the memory layout justifies them.
• Add binary-field lanes for bitwise-hash proof systems.

Exit gate:

• one complete narrow sumcheck proof over a specified field backend runs end-to-end with stable vectors,
• transcript challenges are generated from framed coefficient data,
• verifier checks the proof using independent CPU code,
• the narrow proof is bound into the final application artifact without claiming AIR or GKR semantics.

Phase 6: Full Prover Integration

The flagship should be a transparent, hash-heavy prover that proves real cryptographic statements efficiently on Apple silicon.

Initial statement classes:

• Merkle inclusion over SHA3/Keccak leaves,
• batched hash preimage commitments,
• FRI-backed low-degree claims over M31,
• binary-field proof sketches for SHA3/Keccak circuits.

Exit gate:

• one documented end-to-end proof has stable vectors,
• verifier code is small, deterministic, and independent from GPU execution,
• AIR semantic verification and GKR verification are implemented or explicitly excluded by the statement class,
• public theorem artifacts are replaced or complemented by succinct/ZK proof artifacts for private-witness claims,
• benchmark output captures full proof latency.

Engineering Rules

• No performance claim without JSON benchmark output.
• No new cryptographic API without a CPU oracle.
• No GPU kernel without deterministic tests.
• No secret-bearing buffer reuse without an explicit clearing policy.
• No protocol shortcut without domain separation and transcript tests.
• No lattice parameter claim without a pinned independent lattice-estimator reproduction artifact.
• No roadmap item is complete until it has correctness tests and measurement.