docs(gpu): correct the d=1 composition-parts comments and stale group counts - #948
Open
MauroToscano wants to merge 2 commits into
Open
docs(gpu): correct the d=1 composition-parts comments and stale group counts#948MauroToscano wants to merge 2 commits into
MauroToscano wants to merge 2 commits into
Conversation
Adding cuda_d1_path as Group 3 of gpu_test.sh renumbered the groups after it, but five references still describe the old five-group layout: - scripts/gpu_test.sh: "the prover suite (Groups 4 & 5) proves asm AND rust guests" is now Groups 5 & 6 - and it is the only thing explaining why the script builds rust guests up front, so a Group 5 failure sends the reader to test-cuda-fallback, which needs no rust guests. - Makefile: a hang in Group 1 now costs Groups 2-6, not 2-5. - gpu-tests.yml: the group enumeration and "5 test groups" both predate the new group; that comment is the merge-gate contract for anyone who does not open the shell script. - cuda_path_integration.rs: the R2 composition-LDE comment enumerates two num_parts arms; there are now three, and the new one increments neither counter in the assertion below it (the assertion is still correct - no d=1 table here crosses the default threshold - so this is comment-only). Also move the coverage note off the end of check_composition. It described suite-wide coverage from inside a helper shared by two tests, and its claim that the end-to-end d=1 counterpart "is not asserted ... exercised by real-program proves (ethrex) and the GPU bench instead" was invalidated by this branch's own second commit, which adds prover/tests/cuda_d1_path.rs. Restate it accurately on the decode-shaped test it actually describes.
…ssion gate Four claims in the new d=1 prose do not match the code. 1. "all of which already read the part count from `handle.m`", and the same in decompose_comp_h_dev's doc. Only the R2 commit and the R4 openings read handle.m. R3's z^P exponent and R4 DEEP's gamma count read lde_composition_poly_evaluations.len() - the host part Vec's length - and DEEP merely validates the handle against it, declining on a mismatch. FRI never receives the handle at all. Benign today, because the d=1 arm always drains one host part, but the sentence is the stated reason for not touching R3/R4 and it credits the handle with the host Vec's authority. Replace it with the invariant that actually has to hold - handle.m == lde_composition_poly_evaluations.len(), which materialize_composition_parts_host also requires - and note the same on the d=2 arm's doc. 2. "it is the only end-to-end check that the device m=1 gather / DEEP / FRI layout is correct". The canary compares a device composition-row gather against the host part evals; DEEP and FRI consume separate downstream buffers and are not covered by it. cuda_d1_path.rs already describes the same canary correctly, as guarding "the composition-row gather". Narrow the claim to the in-prove gather check and point at proof verification for DEEP/FRI. 3. "zeroing a preprocessed table's host trace fails its commitment check". Preprocessed tables do go device-only: commit_main_trace takes device_only, the caller applies no preprocessed exclusion, and the preprocessed branch passes !device_only as want_host precisely to support it. The precomputed-root check runs against the device-built tree, so the host drain cannot reach it, and host_trace_empty is not set until Round1 construction - after every R1 commit. Nothing is zeroed either; the Vec is left empty. Restore the accurate reason (any other part count has no device R2 path and needs the host evaluator) and give d=1's real one: it always drains its single part to feed the canary, so it gains nothing from dropping the host trace. 4. "the degree gate below" in decompose_comp_h_dev. There is no gate below it in that function; the gate is device_only_for, far above. Also drop the duplicated half of device_only_for's rationale, which restated the d=2 sentence eight lines later and was where claim 3 lived, and correct the "nothing to unwind" note on the d=1 download ordering: both values drop by RAII in either order, so the ordering is about keeping the blocking D2H off the tail of the de-interleave launch, not about unwinding. Two small cleanups while in here: - Hoist the admission gate the d=1 and d=2 producers had duplicated verbatim (two TypeId guards plus the threshold/power-of-two test) into dev_comp_parts_gate, so a future condition - a VRAM check, a tower widening - cannot land on only one arm and silently diverge them. - Rename try_deinterleave_comp_h_dev to try_comp_h_to_slabs_dev, matching the kernel (comp_h_to_slabs_ext3), the math-cuda entry point (comp_h_to_slabs) and the counter (GPU_COMP_H_SLABS_CALLS); it was the one link in that chain that a grep from either end would miss. Drop the single-use `decomposed` temporary at the call site, which read as a borrow workaround where none is needed.
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.
Targets
decode-deep-fri-gpu(#946), notmain— every item is either prose #946 adds, or a reference that only became wrong after its group renumber. No behaviour change.Companion to #947, which fixes the
test-cuda-d1threshold/fixture. Independent — either can merge first.Four comment claims that don't match the code
1. "all of which already read the part count from
handle.m" (and the same indecompose_comp_h_dev's doc). Only the R2 commit and the R4 openings readhandle.m. R3'sz^Pexponent and R4 DEEP's gamma count readlde_composition_poly_evaluations.len()— the host part Vec's length — and DEEP merely validates the handle against it, declining on a mismatch. FRI never receives the handle at all.Benign today, since the d=1 arm always drains one host part. But this sentence is the stated reason for not touching R3/R4, and it credits the handle with the host Vec's authority — while the adjacent block floats returning empty parts. Replaced with the invariant that actually has to hold:
handle.m == lde_composition_poly_evaluations.len(), whichmaterialize_composition_parts_hostalso requires.2. "the only end-to-end check that the device m=1 gather / DEEP / FRI layout is correct." The canary compares a device composition-row gather against the host part evals; DEEP and FRI consume separate downstream buffers and aren't covered.
cuda_d1_path.rsin the same branch already describes the same canary correctly, as guarding "the composition-row gather". Narrowed to the in-prove gather check, pointing at proof verification for DEEP/FRI.3. "zeroing a preprocessed table's host trace fails its commitment check." Preprocessed tables do go device-only:
commit_main_tracetakesdevice_only, the caller applies no preprocessed exclusion, and the preprocessed branch passes!device_onlyaswant_hostprecisely to support it. The precomputed-root check runs against the device-built tree, so the host drain can't reach it, andhost_trace_emptyisn't set untilRound1construction — after every R1 commit. Nothing is zeroed either; the Vec is left empty.This one replaced a base comment that was accurate, so it restores the real reason (any other part count has no device R2 path and needs the host evaluator) and states d=1's: it always drains its single part to feed the canary, so it gains nothing from dropping the host trace.
4. "the degree gate below" in
decompose_comp_h_dev— there is no gate below it in that function; the gate isdevice_only_for, far above.Also drops the duplicated half of
device_only_for's rationale (it restated the d=2 sentence eight lines later, and was where claim 3 lived) and corrects the "nothing to unwind" note on the d=1 download ordering — both values drop by RAII in either order, so the ordering is about keeping the blocking D2H off the tail of the de-interleave launch.Five stale group references
Adding
cuda_d1_pathas Group 3 renumbered everything after it:scripts/gpu_test.shMakefilegpu-tests.ymlcuda_path_integration.rsnum_partsarmsThe
gpu_test.shline is the only thing explaining why the script builds rust guests up front, so a Group 5 failure sent the reader totest-cuda-fallback, which needs none. Thegpu-tests.ymlcomment is the merge-gate contract for anyone who doesn't open the shell script. Thecuda_path_integration.rsassertion is still correct (no d=1 table there crosses the default threshold) — comment only.Also moves the coverage note off the end of
check_composition: it described suite-wide coverage from inside a helper shared by two tests, and its claim that the end-to-end d=1 counterpart "is not asserted … exercised by real-program proves (ethrex) and the GPU bench instead" was invalidated by this branch's own second commit addingcuda_d1_path.rs.Two cleanups
TypeIdguards plus the threshold/power-of-two test). Hoisted intodev_comp_parts_gateso a future condition — a VRAM check, a tower widening — can't land on only one arm and silently diverge them.try_deinterleave_comp_h_dev→try_comp_h_to_slabs_dev, matching the kernel (comp_h_to_slabs_ext3), the math-cuda entry point (comp_h_to_slabs) and the counter (GPU_COMP_H_SLABS_CALLS) — it was the one link in that chain a grep from either end would miss. Also drops the single-usedecomposedtemporary, which read as a borrow workaround where none is needed.Both are in the second commit, so they can be dropped independently of the doc fixes.
Verification
cargo clippy -p stark -p math-cuda --features stark/cuda --all-targetsand-p lambda-vm-prover --features cuda --test cuda_path_integration: clean, same pre-existing warning count as the base branch.cargo fmt --all --checkclean. Comment-only apart from the two cleanups, which are behaviour-preserving; no GPU here, so nothing was executed.