q2krail

The q2_K reference quantizer is the only K-quant packer that stores its packed scale and min nibbles with a bare int -> uint8_t cast and no MIN/MAX clamp. Every sibling (q4_K, q5_K, q6_K) clamps. This audits whether the omission is a latent corruption or safe by construction, and finds it safe: across an adversarial corpus the pre-store integers never leave [0,15], so the missing guard is a no-op. The reason is exact, and the audit shows the harness would have caught a wrap if one existed.

The setup

quantize_row_q2_K_ref (ggml/src/ggml-quants.c, build 9760, commit 6ee0f65793) packs a per-sub-block scale and min into the two nibbles of scales[j] with no clamp:

if (max_scale > 0) { float iscale = 15.f/max_scale;
    for (j) { int l = nearest_int(iscale*scales[j]); y[i].scales[j]  =  l; } }        // 864-865
if (max_min   > 0) { float iscale = 15.f/max_min;
    for (j) { int l = nearest_int(iscale*mins[j]);   y[i].scales[j] |= (l << 4); } }  // 875-876

The siblings all guard the analogous store: q4_K MIN(63, ...), q5_K, q6_K MIN(127, ...). q2_K is the lone outlier. If a pre-store integer l could fall below 0 or above 15, the bare cast would wrap: a negative l sign-extends (-1 << 4 truncates to 0xF0, corrupting the min nibble to 15), and an l of 16 overflows the nibble. Either silently corrupts the quantized scale or min, and this is the default Q2_K path.

The result: safe by construction

The pre-store integer is l = nearest_int(iscale * v) with iscale = 15/max(v). Two facts bound it:

• v <= max(v) by definition of the max, so iscale * v <= 15, and it can round up to 16 only if v/max(v) > 1.033, which cannot happen. So no overflow.
• v is never negative: make_qkx2_quants forces min <= 0 (lines 760 and 797-798) and returns *the_min = -min >= 0, so every mins[j] >= 0. The scale is non-negative too: the main-branch refinement slope (sum_w*sum_xl - sum_x*sum_l)/D is a non-negative weighted covariance of L and x (they are similarly ordered, since L is a non-decreasing function of x), and the this_min>0 branch's alternative slope sum_xl/sum_l2 can only be negative when it fits worse and is therefore not selected. So no negative wrap.

Together, every pre-store integer lies in [0,15] and the omitted MIN/MAX guard is a no-op.

The scale non-negativity is the load-bearing sub-claim, so scalehunt.cpp stress-tests it directly: it hammers make_qkx2_quants with 20 million adversarial sub-blocks (all-negative, heavy-tailed, anti-correlated with a few positives among negatives to drive the slope down, growing-magnitude, large-negative) and finds no negative scale or min. Combined with the argument above, the deducted-min formulation keeps both values non-negative.

The audit confirms this on the real kernel over a factored adversarial corpus (all-equal, all-negative, single spike, a mixed-sign block placing an all-negative sub-block beside positive ones, extreme scale ratios, and 4000 random blocks including heavy-tailed spikes):

blocks 4008
out-of-range pre-store integers 0        (observed range [0, 15])
scales never negative: true              mins never negative: true
rail law on real bytes: max scale nibble = 15 on all 4007 non-degenerate blocks;
                        max min   nibble = 15 on all 4003 blocks with a min

The rail law is read off the REAL output bytes: because iscale = 15/max, the argmax sub-block's nibble must be exactly 15. It holds on every block, which confirms the argmax scale/min is not itself wrapped and that iscale is applied as expected. It is corroboration, not the whole guarantee: a non-argmax sub-block wrapping up to 15 would leave max == 15 intact, so the rail law alone does not exclude a non-argmax wrap. The guarantee against any sub-block wrapping is the scales[j] >= 0 and mins[j] >= 0 result above (proven, and stress-tested over 20M sub-blocks), not the rail law.

Why the certificate is trustworthy (not vacuous)

• Real subject. The harness links the real exported quantize_row_q2_K_ref from libggml-base and reads its output bytes. No model, no vocab, no decode. Build 9760, commit 6ee0f65793.
• Non-vacuity control. A mutant that injects a negative scale on one sub-block (with max_scale > 0) is flagged out-of-range by the detector on every one of the 4007 rail blocks. So out_of_range = 0 is a real observation, not a detector that can never fire: if the kernel ever produced a negative pre-store integer, the harness would catch it.
• Sensitivity control. A mutant that clamps the pre-store integer to 14 alters the real bytes on every rail block (the argmax nibble drops from 15 to 14), proving the byte comparison is sensitive to a one-step nibble change.
• Structural, not fp-fragile. The certificate rests on the bound (v <= max(v), v >= 0) and the rail law on the real bytes. A verbatim clean-room port of the packer reproduces the real scale bytes on most blocks (3801/4008 at -O2, and 4008/4008 at -O0/-O3), and on every block and every compilation its pre-store integers stay in [0,15]; the remaining mismatches are fp-contraction tie-breaks in the least-squares refinement that select a different but equally in-range candidate. So the result does not depend on byte-identity.

Reachability

This is the DEFAULT Q2_K path. quantize_q2_K dispatches to quantize_row_q2_K_ref when quant_weights == NULL, i.e. llama-quantize model.gguf out.gguf Q2_K with no importance matrix. The imatrix path uses make_qp_quants, which clamps separately, and is out of scope.

Run

./run.sh

Needs the Homebrew llama.cpp/ggml at /opt/homebrew. Fully CPU, deterministic; no model, no decode; a few thousand blocks run in well under a second.

Files

• q2krail.cpp: links the real quantizer; the adversarial corpus, the rail law on real bytes, the clean-room port with pre-store and sign instrumentation, and the sensitivity and non-vacuity controls.
• repro.cpp: minimal standalone reproduction on one mixed-sign block, plus the wrap arithmetic the certificate rules out.
• scalehunt.cpp: the 20-million-sub-block hunt for a negative scale/min (the load-bearing sub-claim).
• PREREG.md: the pre-registration.
• results/main.json: machine-checked output; results/summary.txt: the one-line summary; results/scalehunt.txt: the negative-scale hunt result.

Scope

Fully CPU, deterministic; no model, no decode, no GPU. The audited quantity is the packed scale/min nibbles of the real q2_K reference kernel. The result is a certificate that the lone un-guarded K-quant packer is nonetheless rail-exact and overflow-free by construction. The imatrix Q2_K path, other K-quants, and the dequantized weight error are out of scope.

License

MIT.