Skip to content
Closed
15 changes: 14 additions & 1 deletion contracts/aprender/quantized-dot-product-v1.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -249,6 +249,19 @@ falsification_tests:
The dispatcher hid both AVX2 defects for as long as every x86 CI box had AVX-512 VNNI
(found 2026-09-10 when yoga, a Core Ultra 9 185H, joined the pool; reverting the fix gives
-3650.1 against scalar -25161.5)
- id: FALSIFY-QDOT-007
rule: Every CPU Q5_K reader decodes ggml's block_q5_K, judged against gguf-py (llama.cpp's
own reader) on a block llama.cpp quantized, never against another aprender reader
prediction: realizar dequantize_q5_k and aprender-quant dequantize_q5_k_to_f32 reproduce all
256 gguf-py values of a real Qwen3.5-0.8B-Q4_K_M super-block bit-exactly; fused_q5k_dot with
a one-hot activation returns each of them; quantize_q5_k round-trips through the fixed reader
test: cargo test -p aprender-serve --lib -- q5k_ggml; cargo test -p aprender-quant --lib -- q5k_ggml
if_fails: A reader packs a sub-block's 32 values into its own 16 qs bytes, or takes the fifth
bit from the wrong qh byte, and every Q5_K tensor decodes to other numbers. Found 2026-09-11
(PMAT-1101) on Qwen3.5-0.8B-Q4_K_M, whose attn_qkv and ssm_out are Q5_K; realizar disagreed
with gguf-py on 5,959,751 of 6,291,456 values of blk.0.attn_qkv and its layer-0 QKV sum was
+26.64 against llama.cpp's -17.06. The dequantizer and the fused dot shared the invented
layout, so every test that compared one with the other passed
qa_gate:
id: F-QDOT-001
name: Quantized Dot Product Contract
Expand All @@ -258,7 +271,7 @@ qa_gate:
- Format registry matches trait implementations
- Dispatch table covers all formats
- Cross-format isolation holds
pass_criteria: All 6 FALSIFY tests pass
pass_criteria: All 7 FALSIFY tests pass
falsification: Introduce a sign error in nibble extraction — gate must catch it
equations:
identity:
Expand Down
15 changes: 14 additions & 1 deletion contracts/quantized-dot-product-v1.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -249,6 +249,19 @@ falsification_tests:
The dispatcher hid both AVX2 defects for as long as every x86 CI box had AVX-512 VNNI
(found 2026-09-10 when yoga, a Core Ultra 9 185H, joined the pool; reverting the fix gives
-3650.1 against scalar -25161.5)
- id: FALSIFY-QDOT-007
rule: Every CPU Q5_K reader decodes ggml's block_q5_K, judged against gguf-py (llama.cpp's
own reader) on a block llama.cpp quantized, never against another aprender reader
prediction: realizar dequantize_q5_k and aprender-quant dequantize_q5_k_to_f32 reproduce all
256 gguf-py values of a real Qwen3.5-0.8B-Q4_K_M super-block bit-exactly; fused_q5k_dot with
a one-hot activation returns each of them; quantize_q5_k round-trips through the fixed reader
test: cargo test -p aprender-serve --lib -- q5k_ggml; cargo test -p aprender-quant --lib -- q5k_ggml
if_fails: A reader packs a sub-block's 32 values into its own 16 qs bytes, or takes the fifth
bit from the wrong qh byte, and every Q5_K tensor decodes to other numbers. Found 2026-09-11
(PMAT-1101) on Qwen3.5-0.8B-Q4_K_M, whose attn_qkv and ssm_out are Q5_K; realizar disagreed
with gguf-py on 5,959,751 of 6,291,456 values of blk.0.attn_qkv and its layer-0 QKV sum was
+26.64 against llama.cpp's -17.06. The dequantizer and the fused dot shared the invented
layout, so every test that compared one with the other passed
qa_gate:
id: F-QDOT-001
name: Quantized Dot Product Contract
Expand All @@ -258,7 +271,7 @@ qa_gate:
- Format registry matches trait implementations
- Dispatch table covers all formats
- Cross-format isolation holds
pass_criteria: All 6 FALSIFY tests pass
pass_criteria: All 7 FALSIFY tests pass
falsification: Introduce a sign error in nibble extraction — gate must catch it
equations:
identity:
Expand Down
9 changes: 3 additions & 6 deletions crates/aprender-quant/src/dequantize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -130,12 +130,9 @@ pub fn dequantize_q5_k_to_f32(data: &[u8], num_elements: usize) -> Vec<f32> {
let min_val = dmin * f32::from(mins[j]);
for k in 0..32 {
let idx = j * 32 + k;
let qs_idx = j * 16 + (k % 16);
let q_lo = if k < 16 {
qs[qs_idx] & 0x0F
} else {
(qs[qs_idx] >> 4) & 0x0F
};
// ggml block_q5_K: sub-blocks 2c and 2c + 1 share qs[32c..32c + 32], the even
// one in the low nibbles and the odd one in the high nibbles (PMAT-1101).
let q_lo = (qs[(j / 2) * 32 + k] >> (4 * (j % 2))) & 0x0F;
let q_hi = (qh[k] >> j) & 1;
let q = q_lo | (q_hi << 4);
result[out_start + idx] = scale * f32::from(q) - min_val;
Expand Down
14 changes: 8 additions & 6 deletions crates/aprender-quant/src/quantize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -252,14 +252,16 @@ fn pack_q5k_high_bits(q5_vals: &[u8; 256]) -> [u8; 32] {
qh
}

/// Pack `Q5_K` low nibbles: combine pairs of 4-bit values into 128 bytes.
/// Pack `Q5_K` low nibbles as ggml's `block_q5_K` does: sub-blocks `2c` and `2c + 1` share
/// `qs[32c..32c + 32]`, the even sub-block in the low nibbles and the odd one in the high
/// nibbles. Before PMAT-1101 each sub-block got its own 16 bytes, a layout no llama.cpp reader
/// decodes.
fn pack_q5k_low_nibbles(q5_vals: &[u8; 256]) -> [u8; 128] {
let mut qs = [0u8; 128];
for j in 0..8 {
for k in 0..16 {
let idx1 = j * 32 + k;
let idx2 = j * 32 + k + 16;
qs[j * 16 + k] = (q5_vals[idx1] & 0x0F) | ((q5_vals[idx2] & 0x0F) << 4);
for c in 0..4 {
for l in 0..32 {
let (even, odd) = (q5_vals[c * 64 + l], q5_vals[c * 64 + 32 + l]);
qs[c * 32 + l] = (even & 0x0F) | ((odd & 0x0F) << 4);
}
}
qs
Expand Down
Loading
Loading