metadata:
  version: "1.0.0"
  created: "2026-03-21"
  author: "PAIML Engineering"
  description: "GGUF quantization and dequantization contracts for model weights"
  references:
    - "Frantar et al. (2023) GPTQ: Accurate Post-Training Quantization for GPT"
    - "Dettmers et al. (2023) QLoRA: Efficient Finetuning of Quantized LLMs"

equations:
  q4_0_dequant:
    formula: "value = scale * (quant_nibble - 8), block_size = 32"
    domain: "scale ∈ ℝ, quant_nibble ∈ [0, 15]"
    invariants:
      - "Block size is always 32 values"
      - "Each byte encodes 2 values (low nibble, high nibble)"
  q8_0_dequant:
    formula: "value = scale * quant_int8, block_size = 32"
    domain: "scale ∈ ℝ, quant_int8 ∈ [-128, 127]"
    invariants:
      - "Scale factor is per-block (1 f32 per 32 values)"
      - "Dequantized values are finite (no NaN/Inf)"
  q4_k_dequant:
    formula: "value = d * block_scale * quant - dmin * block_min, super_block_size = 256"
    domain: "d, dmin ∈ f16, block_scale ∈ [0, 63], quant ∈ [0, 15]"
    invariants:
      - "Super-block has 8 blocks of 32 values each"
      - "6-bit packed scales: blocks 0-3 simple, blocks 4-7 packed layout"
  quantize_roundtrip:
    formula: "|dequantize(quantize(x)) - x| ≤ max_error(format)"
    domain: "x ∈ ℝ^n"
    invariants:
      - "Q8_0 max relative error < 1% for typical weight distributions"
      - "Q4_K achieves 4.5 bits per weight with < 5% perplexity degradation"
  simd_scalar_equivalence:
    formula: "dequant_simd(data) = dequant_scalar(data) within floating-point tolerance"
    domain: "data: valid quantized block bytes"
    invariants:
      - "SIMD and scalar produce identical results up to float rounding"
      - "SIMD path selected based on runtime CPU feature detection"

proof_obligations:
  - type: invariant
    property: "SIMD-scalar equivalence for all formats"
    formal: "|dequant_simd(x) - dequant_scalar(x)| < eps for all valid x"
    tolerance: 1.0e-4
    applies_to: all
  - type: bound
    property: "Dequantized values are finite"
    formal: "∀ v ∈ dequant(data): v.is_finite()"
    applies_to: all
  - type: invariant
    property: "Block size consistency"
    formal: "input.len() mod block_byte_size = 0 for valid input"
    applies_to: all
  - type: bound
    property: "Quantize output bounded"
    formal: "quantize_q8(x) ∈ [-128, 127] for all x"
    applies_to: all

falsification_tests:
  - id: FALSIFY-QUANT-001
    rule: "Q4_K SIMD-scalar equivalence"
    prediction: "dequantize_q4_k_simd(data) ≈ dequantize_q4_k_parallel(data)"
    test: "Generate random Q4_K blocks, compare SIMD vs scalar output"
    if_fails: "SIMD shuffle or scale extraction diverges from scalar path"
  - id: FALSIFY-QUANT-002
    rule: "Q8_0 roundtrip fidelity"
    prediction: "dequant(quant(x)) within 1% of x for normal distribution"
    test: "Quantize random f32 vector to Q8_0, dequantize, check max error"
    if_fails: "Scale computation or rounding in quantize_to_q8_blocks is wrong"
  - id: FALSIFY-QUANT-003
    rule: "Invalid block size rejected"
    prediction: "dequantize_q4_0 with non-multiple-of-block-size returns Err"
    test: "Pass truncated data (e.g., 17 bytes for Q4_0 block)"
    if_fails: "Missing block size validation in dequantization"
  - id: FALSIFY-QUANT-004
    rule: "Zero scale produces zero output"
    prediction: "Q8_0 block with scale=0.0 dequantizes to all zeros"
    test: "Create Q8_0 block with scale=0.0, verify output is all 0.0"
    if_fails: "Scale multiplication path has additive offset bug"
  - id: FALSIFY-QUANT-005
    rule: "Fused quantize-matmul equivalence"
    prediction: "fused_rmsnorm_q4_0_matmul ≈ separate rmsnorm + dequant + matmul"
    test: "Compare fused vs decomposed pipeline on random input"
    if_fails: "Fused kernel skips or reorders normalization step"

kani_harnesses:
  - id: quant-kani-001
    obligation: "Dequantized values are finite"
    bound: 4
    strategy: stub_float
  - id: quant-kani-002
    obligation: "Quantize output bounded"
    bound: 8
    strategy: bounded_int
