docs(sycl): prove the integer_adm shift amount cannot go negative - #1284
Merged
Conversation
4 tasks
Document algebraic invariant proof showing clz > 17 (negative shift) is unreachable in core/src/feature/sycl/integer_adm_sycl.cpp (T-SYCL-ADM-NEGATIVE-SHIFT-REACHABILITY-2026-09-04). Because normalization is guarded by abs_oh >= 32768 (2^15), MSB index n >= 15, so leading zeros clz = 31 - n <= 16 and ks = 17 - clz >= 1. Matches unclamped CPU reference and CUDA twin. Move task row to Recently closed in docs/state.md as NOT-A-BUG.
lusoris
force-pushed
the
fix/sycl-adm-shift-reachability
branch
from
September 5, 2026 10:35
3d74569 to
8cf3be7
Compare
lusoris
marked this pull request as ready for review
September 5, 2026 10:35
Merged
17 tasks
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.
Summary
Settles the open question
T-SYCL-ADM-NEGATIVE-SHIFT-REACHABILITY-2026-09-04: atinteger_adm_sycl.cpplines ~705 and ~1032 the kernel computesclz = 31 - nfrom a hand-rolled leading-zero count and then shifts byks = 17 - clz. Ifclz > 17that shift would be negative — undefined behaviour. A tidy-cleanup agent had clamped it to>= 1; #1281 reverted that as an unjustified divergence from the CPU. This PR is the analysis that decides who was right.Verdict: NOT-A-BUG — the negative shift is algebraically unreachable. Both sites sit in the
elsearm of anabs_oh >= 32768guard, sotmp >= 2^15, the MSB indexn >= 15,clz = 31 - n <= 16, andks = 17 - clzlies in[1, 17]. The CPU reference has the identical contract:integer_adm.c:589callsget_best15_from32(abs_o, …)only whenabs_o >= 32768, giving__builtin_clz(temp) <= 16andk = 17 - clz >= 1with no clamp (integer_adm.c:556-563). CUDA's__clztwin relies on the same guard. The reverted clamp was therefore dead code — but it would also have masked the invariant had it ever been violated, which is worse than a crash.Both sites now carry an
INVARIANTcomment stating the guard and the derivation, so the next reader does not re-open this. No numeric change.Live check on the Arc
SYCL vs CPU on the Netflix
src01_hrc00/hrc01pair forinteger_adm: max abs delta 3.1e-05 (integer_adm_scale1), within the places=4 tolerance (5e-05) — unchanged by this PR, since nothing numeric moved; recorded here as the baseline the reverted clamp would have disturbed forclz > 16inputs, which do not exist.Type
docs— comments + state ledger; no code-path changeChecklist
make format && make lintis green locally.Bug-status hygiene (ADR-0165)
docs/state.md— the open row moves to Recently closed with the NOT-A-BUG verdict and the derivation.Netflix golden-data gate (ADR-0024)
assertAlmostEqual(...)score in the Netflix golden Python tests.Deep-dive deliverables (ADR-0108)
AGENTS.mdinvariant note — no rebase-sensitive invariants beyond whatdocs/rebase-notes.mdnow records (do not clampks; theabs_oh >= 32768guard is the invariant).docs/rebase-notes.md.Reproducer
🤖 Generated with Claude Code