feat(format): quantized-dot-product-v1 5-gate PARTIAL discharge#1378
Closed
noahgift wants to merge 2 commits into
Closed
feat(format): quantized-dot-product-v1 5-gate PARTIAL discharge#1378noahgift wants to merge 2 commits into
noahgift wants to merge 2 commits into
Conversation
Binds FALSIFY-QDOT-001..005 from quantized-dot-product-v1 at PARTIAL_ALGORITHM_LEVEL via 5 verdict functions plus pinned ULP and divergence constants. - QDOT-001: SIMD vs scalar within 4 ULPs (|simd-scalar| <= 4*eps*|scalar|) - QDOT-002: cross-format kernel produces >100× divergence (strict) - QDOT-003: precomputed bsums == on-the-fly bsums (exact integer eq) - QDOT-004: trait-impl set == YAML registry set (no orphans, no ghosts) - QDOT-005: every format has at least the `scalar` dispatch entry ## Five Whys 1. Why does quantized-dot-product-v1 list 5 falsification IDs without algorithm-level discharge? PMAT lints flagged FALSIFY-QDOT-001..005 as unbound at PARTIAL_ALGORITHM_LEVEL. 2. Why does that block ship? Coverage % cannot move while peripheral GGML-format-isolation contracts have no algorithm-level verdict module. 3. Why 4 ULPs not 1? A Q4_K dot product accumulates over 32 elements with 6-bit quants and FP16 scales — IEEE summation drift over 32 adds is bounded by ~4 ULPs of the result. Tighter would Fail every correct SIMD kernel; looser would let actual sign-error bugs slip. 4. Why a HashSet for QDOT-004 vs sorted-vec equality? Format names are unordered identifiers; sorted comparison would impose a declaration-order constraint the YAML doesn't actually require. HashSet equality matches the contract intent: "every name in YAML has a code impl AND every code impl has a YAML name." 5. Why Fail-on-empty-registry for QDOT-004? Vacuous Pass would mask the regression class "registry was deleted entirely." A future `pv comply check` run on an empty registry must Fail loudly so the regression is caught at PR time. Adds 30 unit tests including a 0..7 ULP sweep on QDOT-001 and a ±1-element symmetry test for QDOT-004. Realistic-healthy walks the 3-format steady state (Q4_K, Q6_K, Q8_0); pre-fix walks 5 simultaneous regressions (sign-error in nibble extraction, 1% cross- format collision, off-by-one bsum, orphan trait-impl, missing dispatch entry). No runtime % shift; algorithm-level coverage advances by 5 gates.
noahgift
force-pushed
the
feat/qdot-001-005-partial-discharge
branch
from
838aca3 to
0bc7f62
Compare
Contributor
Author
auto-merge was automatically disabled
May 12, 2026 09:21
Pull request was closed
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
1 participant
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
quantized-dot-product-v1atPARTIAL_ALGORITHM_LEVELvia 5 verdict functions.Gates bound
|simd - scalar| ≤ 4 * f32::EPSILON * |scalar|.max(1.0)> 100 * |correct|.max(1.0)"scalar"dispatch keyPinned constants
AC_QDOT_ULP_TOLERANCE = 4AC_QDOT_CROSS_FORMAT_GARBAGE_FACTOR = 100.0AC_QDOT_DISPATCH_MIN_KEY = "scalar"Five Whys
See commit message — captures why 4 ULPs (not 1), why HashSet equality, and why Fail-on-empty-registry.
Test plan
cargo test -p aprender-core --lib qdot_001_005— 30 passed🤖 Generated with Claude Code