feat(gpu): add bounded chip proving lanes

[hero78119]

Problem

GPU chip proving used an unbounded stream-pool worker count and lacked phase-level CUDA observability.

Design Rationale

Bounded lanes retain whole-task memory reservations and transcript order. Each lane owns one unique non-default CUDA stream, and completion events are awaited before stream or reservation release. CENO_CHIP_PROVING_MODE=lanes is the default, with four lanes; CENO_CHIP_PROVING_LANES accepts 1..=8.

Change Highlights

• Add the bounded, memory-aware lane scheduler and remove the stale unbounded path.
• Add GPU-only NVTX ranges, stable lane thread names, and stream IDs.
• Add an Nsight SQLite report helper and README.
• Fix the septic_curve test import.
• Move FullTracer replay AOT cold-start compilation into explicit setup; proving fails fast if the artifact was not prepared.

Benchmark / Performance Impact

Block 23817600, RTX 4090 24 GB, CPU witness generation.

Real baseline comparison:

Operation

Operation	Baseline (s)	4 lanes (s)	Improvement
app_prove.inner	50.2	44.3	11.8%
app.prove	100.320	47.701	52.5%

Layer

Layer	Baseline (s)	4 lanes (s)	Improvement
Recursion	6.048	5.904	2.4%
Total proof	106.435	53.671	49.6%

The baseline used Ceno 6f6bc870 and had an AOT cache miss (39.786s compile/load). The four-lane run used a cached AOT artifact, so the end-to-end improvement includes cache reuse and is not attributable only to scheduling.

Matched cached-AOT, memory-tracked lane comparison using frozen input 23b97818...686e:

Metric	3 lanes	4 lanes	8 lanes
app_prove.inner (s)	44.5	44.3	44.9
app.prove (s)	47.875	47.701	48.278
Recursion (s)	5.957	5.904	6.178
Total proof (s)	53.898	53.671	54.529
Minimum framebuffer free (MiB)	537.75	793.75	697.75

Four lanes produced the best measured time. All runs verified the root proof without OOM or reservation underestimation.

Benchmark command:

gh workflow run run-benchmark-v2.yml --repo scroll-tech/ceno-reth-benchmark --ref feat/opt_aot -f block_number=23817600 -f proof-uuid=idc-us-2-9 -f frozen_input_sha256=23b97818f3e2787dfe62956c999de15f5fa49af31215ee7ba61b2d598648686e -f cleanup=true -f ignore_failed=false -f run_gpu_benchmark=false -f run_gpu_mem_estimation=true -f chip_proving_mode=lanes-4 -f gpu_mem_tracking=1 -f gpu_enable_witgen=0 -f gpu_cache_level=1 -f gpu_large_task_booking_margin_mb=3048 -f max_cell_per_shard=4500000000 -f gpu_jagged_reshape_log_height=23

Environment: RTX 4090 24 GB; measured with Ceno cc2d431b; mode-only rename in c576f3af; benchmark workflow d48d72b9.

Raw data: baseline, 3 lanes, 4 lanes, 8 lanes.

Large-block scheduler regression check on block 25746900:

Metric	Legacy 64 workers	4 lanes	Change
app_prove.inner (s)	73.7	67.4	8.5% faster
Recursion (s)	8.979	8.943	0.4% faster
Root verification	Passed	Passed	—

Both runs initialized the 64-entry low-level stream pool; scheduler concurrency changed from 64 workers to four lanes. The legacy run had an AOT cache miss, while the four-lane run had an AOT cache hit, so outer application and total-proof times are omitted.

Testing

cargo fmt --all --check
cargo check -p ceno_zkvm --features gpu --lib
cargo test -p ceno_zkvm --features gpu --lib scheduler::tests

GPU check passed; four scheduler tests passed; remote block proof and root verification passed.

Risks and Rollout

The default changes to four bounded lanes. Sequential mode remains available for rollback. Measured framebuffer headroom is below 1 GiB, so larger defaults are not selected.

Follow-ups (optional)

Run cached trials without memory tracking and use NVTX telemetry to evaluate reservation phase splitting.

Copilot Reviewer Directive (keep this section)

When Copilot reviews this PR, apply .github/copilot-instructions.md strictly.