diff --git a/Cargo.lock b/Cargo.lock index 358162b9af..5d45f73d89 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1217,6 +1217,7 @@ name = "aprender-quant" version = "0.68.2" dependencies = [ "half", + "serde_json", ] [[package]] diff --git a/README.md b/README.md index b3f7f2d721..182bfb024b 100644 --- a/README.md +++ b/README.md @@ -41,7 +41,7 @@ publishing — all backed by YAML provable contracts that fail CI on drift. | Metric | Count | Source of truth | |-------:|------:|---| | Workspace crates | **79** workspace crates | `cargo metadata --no-deps` (NOT `ls crates/` — 4 are `exclude`d, 1 has no Cargo.toml) | -| Provable contracts | **1799** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | +| Provable contracts | **1800** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | | CLI commands | **110** CLI commands | `apr --help` | | Book CLI chapters | **112** chapters | `ls book/src/cli/*.md` | | Book lib chapters | **71** chapters | `ls book/src/lib/*.md` (parity with `pub mod`) | @@ -262,7 +262,7 @@ falsification_tests: prediction: apr validate bad-model.apr exits non-zero ``` -The tree carries 1799 contracts across inference, training, quantization, attention, FFN, +The tree carries 1800 contracts across inference, training, quantization, attention, FFN, tokenization, model formats, CLI safety — and this README itself. ## Migration from old crates diff --git a/ci/explicit-test-commands.d/350-aprender-quant-ggml-traits-fixture.cmd b/ci/explicit-test-commands.d/350-aprender-quant-ggml-traits-fixture.cmd new file mode 100644 index 0000000000..c1fb36bcbb --- /dev/null +++ b/ci/explicit-test-commands.d/350-aprender-quant-ggml-traits-fixture.cmd @@ -0,0 +1 @@ +cargo test -p aprender-quant --test ggml_traits_fixture diff --git a/contracts/census.json b/contracts/census.json index 3009dd4060..d6286d1147 100644 --- a/contracts/census.json +++ b/contracts/census.json @@ -1,15 +1,15 @@ { "schema": "ont.paiml.dev/census/v1alpha1", "git_sha": null, - "n_files": 1799, - "n_parsed": 1799, + "n_files": 1800, + "n_parsed": 1800, "n_parse_errors": 0, "parse_errors": [], "quarantined_n": 0, "by_kind": { "beat-benchmark": 24, "corpus-assembly": 1, - "kernel": 362, + "kernel": 363, "model-family": 28, "model-family-variant": 1, "pattern": 86, @@ -25,11 +25,11 @@ "pv-contract": 1 }, "by_anchoring": { - "unanchored": 1796, + "unanchored": 1797, "class": 2, "instance": 1 }, - "id_set_sha256": "a547cd5527caeffade2d8260d25421f26506df1c1d8f00f5eb7b9cde12e8107e", + "id_set_sha256": "51cfc1e6cf27aa5cb6d9345e918a19863f13aa4728b4eba15bfa69bc6002bfb1", "declared_external": [ { "name": "provable-contracts", diff --git a/contracts/contracts.nt b/contracts/contracts.nt index 16022a5f13..7990b9e038 100644 --- a/contracts/contracts.nt +++ b/contracts/contracts.nt @@ -7742,6 +7742,12 @@ "contracts/model-families/gemma.yaml"^^ . "gemma"^^ . "model-family"^^ . + . + . + "contracts/ggml-type-v1.yaml"^^ . + "ggml-type-v1"^^ . + "ggml-type"^^ . + "1.0.0"^^ . . . "contracts/gguf-cpu-cache-v1.yaml"^^ . diff --git a/contracts/ggml-type-v1.yaml b/contracts/ggml-type-v1.yaml new file mode 100644 index 0000000000..6aab90e853 --- /dev/null +++ b/contracts/ggml-type-v1.yaml @@ -0,0 +1,202 @@ +metadata: + version: 1.0.0 + created: '2026-09-20' + author: PAIML Engineering + description: | + ONE ggml tensor-type enum for the workspace, and ONE table of what each + type weighs, both extracted from upstream ggml rather than written by hand. + + THE DEFECT THIS CLOSES (PMAT-3430, epic PP-QUANT-001 #3421). aprender named + ggml tensor types in three independent enums -- aprender-serve's + GgmlQuantType (16 ids), aprender-core's GgmlType (12), aprender-compute's + GgmlType (15) -- plus a private 13-row label table, against 35 live ids + upstream. Nothing compared any of them to upstream, so NVFP4 (40), Q1_0 (41) + and Q2_0 (42) appeared upstream with no signal in this tree at all, and the + byte-size tables disagreed with upstream AND with each other. + + THE ORACLE (operator ruling 2026-09-20, clauses 2' / 2a / 3). Upstream ggml + at scripts/llama_pin.toml `build_commit`, BY REFERENCE and never as a + literal sha, is the reference; in-tree values are the defendant. Every row + of trueno_quant::TRAITS is extracted by scripts/extract_ggml_traits.sh from + ggml's own compiled type_traits table into + crates/aprender-quant/fixtures/ggml_traits.json, which records the sha it + read. A pin bump therefore turns the fixture RED until it is regenerated in + the bump's own PR. + + WHY THE EXTRACTOR COMPILES A PROBE. ggml's table gives + `.type_size = sizeof(block_q4_1)` -- a C expression. Every in-tree table + that got these numbers wrong got them wrong by hand, so the extractor links + the pinned checkout's own libggml-base and calls ggml_type_size / + ggml_blck_size / ggml_type_name. + + THE COMMENTED-ROW TRAP. `enum ggml_type` has 8 commented-out rows and only + some say "removed" -- `// GGML_TYPE_Q4_0_4_8 = 32,` says nothing. A first + pass that classified by comment WORDING returned 44/41/3 instead of + 43/35/8. Membership is positional, and the classification must agree with + the compiled table or the extractor refuses to emit. + references: + - 'ggml/include/ggml.h enum ggml_type at the pinned comparator commit (GGML_TYPE_COUNT = 43)' + - 'ggml/src/ggml.c type_traits[GGML_TYPE_COUNT] -- .blck_size / .type_size / .type_name' + - 'scripts/llama_pin.toml build_commit -- the oracle, by reference' + - 'scripts/extract_ggml_traits.sh + scripts/extract_ggml_traits.awk -- the committed extraction command' + - 'crates/aprender-quant/fixtures/ggml_traits.json -- the checked-in fixture, recording its sha' + - 'crates/aprender-quant/src/ggml_type.rs -- GgmlType, QuantTraits, TRAITS[43]' + - 'GitHub #3430 (M1), #3431 (M2 reconciliation), #3421 (epic), #3563 (pin-derived artifacts, general case)' + +name: ggml-type +version: 1.0.0 +scope: aprender-quant (trueno_quant) ggml tensor-type enum and TRAITS table + +description: | + The workspace has exactly one ggml tensor-type id space, indexed by upstream + id, whose per-type block geometry equals upstream's at the pinned comparator + commit. A type's size is `type_size` bytes per `blck_size` elements; a removed + id is not constructible but keeps its slot; and the fixture that supplies + every number records the commit it was read from. + +equations: + block_geometry: + description: 'TRAITS[i].{blck_size,type_size} equals ggml at the pinned commit' + formula: | + For every live id i: + TRAITS[i].blck_size == ggml_blck_size(i) + TRAITS[i].type_size == ggml_type_size(i) + TRAITS[i].ggml_name == ggml_type_name(i) + For every removed id i: + TRAITS[i].blck_size == 0 AND TRAITS[i].type_size == 0 + domain: 'ggml tensor-type ids 0..=42 at build_commit d1d3c3396 (35 live, 8 removed)' + codomain: 'elements per block (u32) and bytes per block (u32)' + invariants: + - 'TRAITS has exactly 43 rows, dense, indexed by id' + - 'live + removed == 43; live == 35 and removed == 8 at the current pin' + - 'every live row has blck_size > 0 and type_size > 0' + - 'name and ggml_name differ in ASCII case only (Q4_K vs q4_K)' + lean_theorem: Theorems.Ggml_Block_Geometry + tensor_bytes: + description: 'bytes for n elements, rounding a partial block up' + formula: 'tensor_bytes(t, n) = ceil(n / blck_size(t)) * type_size(t)' + domain: 'a live type and a non-negative element count' + codomain: byte count (usize) + invariants: + - 'tensor_bytes(t, blck_size(t)) == type_size(t)' + - 'tensor_bytes(t, 0) == 0' + - 'checked_tensor_bytes refuses (None) when n is not a multiple of blck_size' + lean_theorem: Theorems.Ggml_Tensor_Bytes + +proof_obligations: +- id: GGMLT-INV-001 + type: invariant + property: every TRAITS row equals the upstream fixture row for its id + formal: | + ∀ i ∈ 0..43: + TRAITS[i].name ≡ fixture.types[i].enum_name ∧ + TRAITS[i].ggml_name ≡ fixture.types[i].ggml_name ∧ + TRAITS[i].blck_size ≡ fixture.types[i].blck_size ∧ + TRAITS[i].type_size ≡ fixture.types[i].type_size ∧ + (TRAITS[i].family ≡ Removed) ↔ (fixture.types[i].status ≠ "live") +- id: GGMLT-INV-002 + type: invariant + property: the fixture was extracted at the pin of record + formal: | + fixture.pin_build_commit ≡ llama_pin.build_commit ∧ + prefix(fixture.resolved_sha, llama_pin.build_commit) +- id: GGMLT-INV-003 + type: invariant + property: a removed id is distinguishable from an id that never existed + formal: | + ∀ r ∈ REMOVED_IDS: + from_id(r) ≡ None ∧ try_from_id(r) ≡ Err(Removed{id: r, name: TRAITS[r].name}) + ∀ u ≥ 43: try_from_id(u) ≡ Err(Unknown{id: u}) +- id: GGMLT-EQ-004 + type: equivalence + property: the 16 strings and 15 sizes the replaced enums carried are unchanged + formal: | + ∀ (id, name) ∈ SERVE_16: + as_str(from_id(id)) ≡ name ∧ + from_str_lossy(name) ≡ from_str_lossy(lower(name)) ≡ Some(from_id(id)) + ∀ (id, blck, bytes) ∈ COMPUTE_15: + block_size(from_id(id)) ≡ blck ∧ block_bytes(from_id(id)) ≡ bytes +- id: GGMLT-INV-005 + type: invariant + property: aprender's family column agrees with upstream's is_quantized flag + formal: | + ∀ i ∈ 0..43: + (TRAITS[i].family ∉ {Float, Int, Removed}) ↔ fixture.types[i].is_quantized + +falsification_tests: +- id: FT-GGMLT-001 + rule: mutating any one TRAITS row turns the fixture test RED + prediction: | + Setting TRAITS[9].type_size to 40 (gguf-py's value for Q8_1, which the C + static_assert refutes) fails traits_table_equals_the_upstream_fixture_row_for_row + AND computes_fifteen_sizes_are_unchanged. Renaming TRAITS[30].name from + BF16 to Bf16 fails serves_sixteen_strings_still_mean_what_they_meant. + Giving a removed row a live family fails two more. + test: cargo test -p aprender-quant --test ggml_traits_fixture + if_fails: 'a TRAITS row no longer matches the upstream-extracted fixture.' + evidence: | + Measured 2026-09-20, all four mutations RED and the unmutated control GREEN + (8 tests): M1 TRAITS[9].type_size 36->40, M2 TRAITS[30].name BF16->Bf16, + M3 TRAITS[4].family Removed->Affine, M4 a fake id 43 added to the fixture. +- id: FT-GGMLT-002 + rule: a comparator pin bump turns the fixture RED until it is regenerated + prediction: | + Rewriting the fixture's pin_build_commit to the superseded comparator + 39173bcac fails falsify_ggml_001_traits_fixture_records_the_current_pin + with a message naming both shas and the regeneration command. + test: cargo test -p aprender-core --test monorepo_invariants falsify_ggml + if_fails: 'the fixture and scripts/llama_pin.toml name different commits.' + evidence: 'Measured 2026-09-20: RED on the mutation, GREEN on the control (3 tests).' +- id: FT-GGMLT-003 + rule: the extractor refuses a live/Removed classification that disagrees with ggml + prediction: | + On synthetic inputs, the emitter exits 7 when the header revives a row the + compiled table calls dead, when it buries a live one, when GGML_TYPE_COUNT + disagrees, and when a live id has type_size 0 -- and exits 0, classifying a + wording-free commented row as Removed, on the control. + test: bash scripts/extract_ggml_traits_selftest.sh + if_fails: 'the extractor would emit a fixture that is confidently wrong on the commented rows.' + evidence: | + 7 cases, 0 failures, measured 2026-09-20. Also run in CI from + falsify_ggml_003_extractor_case_table_passes, which refuses a vacuous + (zero-case) run. +- id: FT-GGMLT-004 + rule: the crate's six legacy K-quant constants may not drift from TRAITS + prediction: | + Q4_K_BLOCK_BYTES != TRAITS[12].type_size is a COMPILE error (a const + assertion in lib.rs), not a test failure. + test: cargo build -p aprender-quant + if_fails: 'a published constant and the upstream table disagree about the same number.' + evidence: cargo build -p aprender-quant + +- id: FT-GGMLT-005 + rule: the family column cannot claim a quantization upstream does not report + prediction: | + Giving a Float/Int id a quantized family, or a quantized id the Float + family, fails the_family_classification_agrees_with_upstreams_is_quantized_flag + with the id, the family and both flags in the message. + test: cargo test -p aprender-quant --test ggml_traits_fixture + if_fails: 'aprender''s family classification and ggml''s is_quantized disagree.' + evidence: | + Measured 2026-09-20 by mutation M3 (TRAITS[4].family Removed -> Affine), + which this test catches independently of the row-for-row comparison. + +kani_harnesses: +- id: KANI-GGMLT-001 + obligation: every id in range resolves consistently and no method panics + property: | + For all id: u32 with id < 43, from_id(id).is_some() == (TRAITS[id].blck_size > 0), + try_from_id(id) is Ok exactly when from_id is Some, and for every live type + tensor_bytes(blck_size) == type_size with no panic and no overflow. + bound: 43 + strategy: exhaustive + solver: cadical + harness: verify_ggml_type_id_space + +qa_gate: + id: F-GGMLT-001 + name: ggml-type-v1 Contract + description: The workspace's single ggml tensor-type table must equal upstream ggml at the pinned comparator commit, row for row, with a fixture that records the commit it was read from. + checks: + - validation + - falsification diff --git a/crates/aprender-core/tests/monorepo_invariants.rs b/crates/aprender-core/tests/monorepo_invariants.rs index cc19a49a6f..a5940230c8 100644 --- a/crates/aprender-core/tests/monorepo_invariants.rs +++ b/crates/aprender-core/tests/monorepo_invariants.rs @@ -874,3 +874,152 @@ fn falsify_install_001_no_dead_profile_package_specs() { ); } } + +// =========================================================================== +// FALSIFY-GGML-001/002 (PMAT-3430): the ggml traits fixture is pinned +// +// Operator ruling 2026-09-20, clause 2a: the TRAITS fixture records the sha it +// was extracted from, and a test asserts that sha still equals +// scripts/llama_pin.toml `build_commit`. A pin bump therefore turns this RED +// until the fixture is regenerated by the committed extraction command — the +// bump's cost is visible in the BUMP's PR, not discovered later. #3563 asks for +// the general form of this across every pin-derived artifact in the tree. +// +// WHY IT LIVES HERE AND NOT IN aprender-quant. trueno_quant is published; a +// packaged crate has no scripts/llama_pin.toml, so a test there could only +// skip — and a skip is how this kind of check becomes decoration. This file is +// already wired into CI (ci/explicit-test-commands.d/030-*), so it is not a +// dark target. +// =========================================================================== + +/// Read one quoted key out of scripts/llama_pin.toml, the same narrow parse +/// `llama_pin_get` does in shell. tomllib is 3.11+ and the runner is 3.10, which +/// is why the shell side hand-parses; this side does not get to differ. +fn llama_pin_value(key: &str) -> String { + let path = workspace_root().join("scripts/llama_pin.toml"); + let text = std::fs::read_to_string(&path) + .unwrap_or_else(|e| panic!("scripts/llama_pin.toml must be readable: {e}")); + for line in text.lines() { + let line = line.trim(); + if let Some(rest) = line.strip_prefix(key) { + let rest = rest.trim_start(); + if let Some(rest) = rest.strip_prefix('=') { + return rest.trim().trim_matches('"').to_string(); + } + } + } + panic!("scripts/llama_pin.toml declares no `{key}`"); +} + +fn ggml_fixture() -> serde_json::Value { + let path = workspace_root().join("crates/aprender-quant/fixtures/ggml_traits.json"); + let text = std::fs::read_to_string(&path) + .unwrap_or_else(|e| panic!("the ggml traits fixture must be readable: {e}")); + serde_json::from_str(&text).expect("the ggml traits fixture must be valid JSON") +} + +/// FALSIFY-GGML-001: the fixture was extracted at the pin of record. +#[test] +fn falsify_ggml_001_traits_fixture_records_the_current_pin() { + let pin = llama_pin_value("build_commit"); + let fixture = ggml_fixture(); + let recorded = fixture["pin_build_commit"] + .as_str() + .expect("the fixture must record pin_build_commit"); + + assert_eq!( + recorded, pin, + "crates/aprender-quant/fixtures/ggml_traits.json was extracted at {recorded}, but \ + scripts/llama_pin.toml build_commit is now {pin}. Regenerate it with \ + `bash scripts/extract_ggml_traits.sh` against a checkout at {pin} and commit the \ + result in the SAME PR as the bump — every TRAITS row is an upstream reading, and a \ + bump may change any of them." + ); + + // The full sha the extractor resolved must still be the pin's prefix: the + // pin is abbreviated, and an abbreviation that stopped matching would mean + // the fixture and the pin name different commits. + let resolved = fixture["resolved_sha"] + .as_str() + .expect("the fixture must record resolved_sha"); + assert!( + resolved.starts_with(&pin), + "the fixture's resolved_sha {resolved} does not start with the pin {pin}" + ); +} + +/// FALSIFY-GGML-002: the fixture still describes upstream's 43 slots, and the +/// live/removed split the ruling measured (35 + 8). +#[test] +fn falsify_ggml_002_traits_fixture_is_the_whole_id_space() { + let fixture = ggml_fixture(); + let types = fixture["types"] + .as_array() + .expect("fixture has no types array"); + let count = fixture["ggml_type_count"] + .as_u64() + .expect("no ggml_type_count"); + let live = fixture["live_count"].as_u64().expect("no live_count"); + let removed = fixture["removed_count"].as_u64().expect("no removed_count"); + + assert_eq!( + types.len() as u64, + count, + "the fixture lists {} of {count} ids", + types.len() + ); + assert_eq!( + live + removed, + count, + "live {live} + removed {removed} != {count}" + ); + + // Ids are dense and in order, because TRAITS is indexed by id. + for (i, row) in types.iter().enumerate() { + assert_eq!( + row["id"].as_u64(), + Some(i as u64), + "the fixture's rows are not in dense id order at position {i}" + ); + } +} + +/// FALSIFY-GGML-003: the extractor's own case table passes. +/// +/// `scripts/extract_ggml_traits_selftest.sh` proves the live/Removed +/// classification refuses the four ways it can be wrong, on synthetic inputs — +/// no llama.cpp checkout, no compiler. It is invoked from HERE rather than from +/// a new ci.yml step because this target is already wired +/// (ci/explicit-test-commands.d/030-*), and a case table nothing runs is the +/// thing it was written to prevent. +#[test] +fn falsify_ggml_003_extractor_case_table_passes() { + let root = workspace_root(); + let script = root.join("scripts/extract_ggml_traits_selftest.sh"); + assert!( + script.is_file(), + "scripts/extract_ggml_traits_selftest.sh is missing" + ); + + let out = Command::new("bash") + .arg(&script) + .current_dir(&root) + .output() + .expect("the extractor self-test must be runnable"); + + let stdout = String::from_utf8_lossy(&out.stdout); + let stderr = String::from_utf8_lossy(&out.stderr); + assert!( + out.status.success(), + "extract_ggml_traits_selftest.sh failed ({}):\n{stdout}\n{stderr}", + out.status + ); + // A case table that runs zero cases passes vacuously. Require that it says + // how many it ran, and that the count is not zero. + let ran = stdout + .lines() + .find_map(|l| l.strip_suffix(" case(s), 0 failure(s)")) + .and_then(|n| n.trim().parse::().ok()) + .unwrap_or_else(|| panic!("the self-test did not report a case count:\n{stdout}")); + assert!(ran >= 7, "the extractor case table ran only {ran} case(s)"); +} diff --git a/crates/aprender-quant/Cargo.toml b/crates/aprender-quant/Cargo.toml index 866b1bb642..4ee81d3b87 100644 --- a/crates/aprender-quant/Cargo.toml +++ b/crates/aprender-quant/Cargo.toml @@ -15,7 +15,14 @@ name = "trueno_quant" [dependencies] half = "2.4" +[dev-dependencies] +# PMAT-3430: tests/ggml_traits_fixture.rs reads the upstream-extracted fixture. +# DEV-only, so the published crate still ships with `half` as its one dependency. +serde_json = { workspace = true } + [lints.rust] +# PMAT-3430: ggml_type.rs carries a #[cfg(kani)] harness (KANI-GGMLT-001). +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } unsafe_op_in_unsafe_fn = "warn" missing_docs = "warn" rust_2018_idioms = "warn" diff --git a/crates/aprender-quant/fixtures/ggml_traits.json b/crates/aprender-quant/fixtures/ggml_traits.json new file mode 100644 index 0000000000..e0df480eb0 --- /dev/null +++ b/crates/aprender-quant/fixtures/ggml_traits.json @@ -0,0 +1,398 @@ +{ + "_comment": "GENERATED by scripts/extract_ggml_traits.sh from upstream ggml at the pinned comparator commit. Do not hand-edit: regenerate. trueno_quant asserts that pin_build_commit below still equals scripts/llama_pin.toml build_commit.", + "source": "llama.cpp ggml/include/ggml.h + libggml-base type_traits", + "pin_build_commit": "d1d3c3396", + "resolved_sha": "d1d3c3396aa13a5f239109a822666c4870490ad5", + "ggml_type_count": 43, + "live_count": 35, + "removed_count": 8, + "types": [ + { + "id": 0, + "enum_name": "F32", + "ggml_name": "f32", + "status": "live", + "blck_size": 1, + "type_size": 4, + "is_quantized": false + }, + { + "id": 1, + "enum_name": "F16", + "ggml_name": "f16", + "status": "live", + "blck_size": 1, + "type_size": 2, + "is_quantized": false + }, + { + "id": 2, + "enum_name": "Q4_0", + "ggml_name": "q4_0", + "status": "live", + "blck_size": 32, + "type_size": 18, + "is_quantized": true + }, + { + "id": 3, + "enum_name": "Q4_1", + "ggml_name": "q4_1", + "status": "live", + "blck_size": 32, + "type_size": 20, + "is_quantized": true + }, + { + "id": 4, + "enum_name": "Q4_2", + "ggml_name": "DEPRECATED", + "status": "removed", + "blck_size": 0, + "type_size": 0, + "is_quantized": false + }, + { + "id": 5, + "enum_name": "Q4_3", + "ggml_name": "DEPRECATED", + "status": "removed", + "blck_size": 0, + "type_size": 0, + "is_quantized": false + }, + { + "id": 6, + "enum_name": "Q5_0", + "ggml_name": "q5_0", + "status": "live", + "blck_size": 32, + "type_size": 22, + "is_quantized": true + }, + { + "id": 7, + "enum_name": "Q5_1", + "ggml_name": "q5_1", + "status": "live", + "blck_size": 32, + "type_size": 24, + "is_quantized": true + }, + { + "id": 8, + "enum_name": "Q8_0", + "ggml_name": "q8_0", + "status": "live", + "blck_size": 32, + "type_size": 34, + "is_quantized": true + }, + { + "id": 9, + "enum_name": "Q8_1", + "ggml_name": "q8_1", + "status": "live", + "blck_size": 32, + "type_size": 36, + "is_quantized": true + }, + { + "id": 10, + "enum_name": "Q2_K", + "ggml_name": "q2_K", + "status": "live", + "blck_size": 256, + "type_size": 84, + "is_quantized": true + }, + { + "id": 11, + "enum_name": "Q3_K", + "ggml_name": "q3_K", + "status": "live", + "blck_size": 256, + "type_size": 110, + "is_quantized": true + }, + { + "id": 12, + "enum_name": "Q4_K", + "ggml_name": "q4_K", + "status": "live", + "blck_size": 256, + "type_size": 144, + "is_quantized": true + }, + { + "id": 13, + "enum_name": "Q5_K", + "ggml_name": "q5_K", + "status": "live", + "blck_size": 256, + "type_size": 176, + "is_quantized": true + }, + { + "id": 14, + "enum_name": "Q6_K", + "ggml_name": "q6_K", + "status": "live", + "blck_size": 256, + "type_size": 210, + "is_quantized": true + }, + { + "id": 15, + "enum_name": "Q8_K", + "ggml_name": "q8_K", + "status": "live", + "blck_size": 256, + "type_size": 292, + "is_quantized": true + }, + { + "id": 16, + "enum_name": "IQ2_XXS", + "ggml_name": "iq2_xxs", + "status": "live", + "blck_size": 256, + "type_size": 66, + "is_quantized": true + }, + { + "id": 17, + "enum_name": "IQ2_XS", + "ggml_name": "iq2_xs", + "status": "live", + "blck_size": 256, + "type_size": 74, + "is_quantized": true + }, + { + "id": 18, + "enum_name": "IQ3_XXS", + "ggml_name": "iq3_xxs", + "status": "live", + "blck_size": 256, + "type_size": 98, + "is_quantized": true + }, + { + "id": 19, + "enum_name": "IQ1_S", + "ggml_name": "iq1_s", + "status": "live", + "blck_size": 256, + "type_size": 50, + "is_quantized": true + }, + { + "id": 20, + "enum_name": "IQ4_NL", + "ggml_name": "iq4_nl", + "status": "live", + "blck_size": 32, + "type_size": 18, + "is_quantized": true + }, + { + "id": 21, + "enum_name": "IQ3_S", + "ggml_name": "iq3_s", + "status": "live", + "blck_size": 256, + "type_size": 110, + "is_quantized": true + }, + { + "id": 22, + "enum_name": "IQ2_S", + "ggml_name": "iq2_s", + "status": "live", + "blck_size": 256, + "type_size": 82, + "is_quantized": true + }, + { + "id": 23, + "enum_name": "IQ4_XS", + "ggml_name": "iq4_xs", + "status": "live", + "blck_size": 256, + "type_size": 136, + "is_quantized": true + }, + { + "id": 24, + "enum_name": "I8", + "ggml_name": "i8", + "status": "live", + "blck_size": 1, + "type_size": 1, + "is_quantized": false + }, + { + "id": 25, + "enum_name": "I16", + "ggml_name": "i16", + "status": "live", + "blck_size": 1, + "type_size": 2, + "is_quantized": false + }, + { + "id": 26, + "enum_name": "I32", + "ggml_name": "i32", + "status": "live", + "blck_size": 1, + "type_size": 4, + "is_quantized": false + }, + { + "id": 27, + "enum_name": "I64", + "ggml_name": "i64", + "status": "live", + "blck_size": 1, + "type_size": 8, + "is_quantized": false + }, + { + "id": 28, + "enum_name": "F64", + "ggml_name": "f64", + "status": "live", + "blck_size": 1, + "type_size": 8, + "is_quantized": false + }, + { + "id": 29, + "enum_name": "IQ1_M", + "ggml_name": "iq1_m", + "status": "live", + "blck_size": 256, + "type_size": 56, + "is_quantized": true + }, + { + "id": 30, + "enum_name": "BF16", + "ggml_name": "bf16", + "status": "live", + "blck_size": 1, + "type_size": 2, + "is_quantized": false + }, + { + "id": 31, + "enum_name": "Q4_0_4_4", + "ggml_name": "TYPE_Q4_0_4_4 REMOVED, use Q4_0 with runtime repacking", + "status": "removed", + "blck_size": 0, + "type_size": 0, + "is_quantized": false + }, + { + "id": 32, + "enum_name": "Q4_0_4_8", + "ggml_name": "TYPE_Q4_0_4_8 REMOVED, use Q4_0 with runtime repacking", + "status": "removed", + "blck_size": 0, + "type_size": 0, + "is_quantized": false + }, + { + "id": 33, + "enum_name": "Q4_0_8_8", + "ggml_name": "TYPE_Q4_0_8_8 REMOVED, use Q4_0 with runtime repacking", + "status": "removed", + "blck_size": 0, + "type_size": 0, + "is_quantized": false + }, + { + "id": 34, + "enum_name": "TQ1_0", + "ggml_name": "tq1_0", + "status": "live", + "blck_size": 256, + "type_size": 54, + "is_quantized": true + }, + { + "id": 35, + "enum_name": "TQ2_0", + "ggml_name": "tq2_0", + "status": "live", + "blck_size": 256, + "type_size": 66, + "is_quantized": true + }, + { + "id": 36, + "enum_name": "IQ4_NL_4_4", + "ggml_name": "TYPE_IQ4_NL_4_4 REMOVED, use IQ4_NL with runtime repacking", + "status": "removed", + "blck_size": 0, + "type_size": 0, + "is_quantized": false + }, + { + "id": 37, + "enum_name": "IQ4_NL_4_8", + "ggml_name": "TYPE_IQ4_NL_4_8 REMOVED, use IQ4_NL with runtime repacking", + "status": "removed", + "blck_size": 0, + "type_size": 0, + "is_quantized": false + }, + { + "id": 38, + "enum_name": "IQ4_NL_8_8", + "ggml_name": "TYPE_IQ4_NL_8_8 REMOVED, use IQ4_NL with runtime repacking", + "status": "removed", + "blck_size": 0, + "type_size": 0, + "is_quantized": false + }, + { + "id": 39, + "enum_name": "MXFP4", + "ggml_name": "mxfp4", + "status": "live", + "blck_size": 32, + "type_size": 17, + "is_quantized": true + }, + { + "id": 40, + "enum_name": "NVFP4", + "ggml_name": "nvfp4", + "status": "live", + "blck_size": 64, + "type_size": 36, + "is_quantized": true + }, + { + "id": 41, + "enum_name": "Q1_0", + "ggml_name": "q1_0", + "status": "live", + "blck_size": 128, + "type_size": 18, + "is_quantized": true + }, + { + "id": 42, + "enum_name": "Q2_0", + "ggml_name": "q2_0", + "status": "live", + "blck_size": 64, + "type_size": 18, + "is_quantized": true + } + ] +} diff --git a/crates/aprender-quant/src/ggml_type.rs b/crates/aprender-quant/src/ggml_type.rs new file mode 100644 index 0000000000..05a593e0b4 --- /dev/null +++ b/crates/aprender-quant/src/ggml_type.rs @@ -0,0 +1,806 @@ +//! ONE ggml tensor-type enum, and ONE table of what each type weighs. +//! +//! # Why this module exists (PMAT-3430, PP-QUANT-001 M1) +//! +//! aprender named ggml tensor types in three independent enums — serve's +//! `GgmlQuantType` (16 ids), core's `GgmlType` (12), compute's `GgmlType` (15) +//! — plus a fourth private label table, against 35 live ids upstream. They +//! disagreed about which ids exist, about spelling, and about SIZES. Nothing +//! compared any of them to upstream, so `NVFP4` (40), `Q1_0` (41) and `Q2_0` +//! (42) appeared upstream with no signal here at all. +//! +//! # The oracle is upstream, by reference +//! +//! Operator ruling 2026-09-20, clauses 2' and 3: upstream ggml at +//! `scripts/llama_pin.toml` `build_commit` is the reference; in-tree values are +//! the defendant. Every number in [`TRAITS`] is extracted from ggml's own +//! compiled `type_traits` table by `scripts/extract_ggml_traits.sh` into +//! `fixtures/ggml_traits.json`, and `tests/ggml_traits_fixture.rs` fails if a +//! single row here stops matching that fixture. The fixture records the sha it +//! was read from; a repo-level invariant (`monorepo_invariants.rs`) fails if +//! that sha stops being the pin — so bumping the comparator turns this RED in +//! the bump's own PR rather than silently later (clause 2a, generalised by +//! #3563). +//! +//! # What this module is NOT +//! +//! It is not an admission policy. [`GgmlType::from_id`] knows all 35 live ids; +//! whether a given crate should ACCEPT a given id at a parse boundary is that +//! crate's decision, and M1 preserves each one exactly as it was (#3430 Q1-c). +//! It also carries no dequantiser: knowing that `IQ3_S` is 110 bytes per 256 +//! elements is not the same as being able to read one. + +use core::fmt; + +/// How a type stores its numbers. +/// +/// This is aprender's classification, not upstream's: ggml's table has no +/// family column, only an `is_quantized` flag. The link back to upstream that +/// CAN fail is exactly that flag — [`GgmlFamily::Float`] and [`GgmlFamily::Int`] +/// are the non-quantized families, every other live family is quantized, and +/// `tests/ggml_traits_fixture.rs` checks that against the fixture. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum GgmlFamily { + /// IEEE / bfloat floats stored one per "block": `F32`, `F16`, `F64`, `BF16`. + Float, + /// Plain integers, one per "block": `I8`, `I16`, `I32`, `I64`. + Int, + /// The legacy fixed-block quants — a scale (and for the `_1` forms a min) + /// plus packed weights: `Q4_0`, `Q4_1`, `Q5_0`, `Q5_1`, `Q8_0`, `Q8_1`, and + /// upstream's newer `Q1_0` (128/block) and `Q2_0` (64/block). + Affine, + /// K-quants: 256-element super-blocks with per-sub-block scales. + KQuant, + /// The importance-matrix / codebook quants (`IQ*`), 256-element super-blocks + /// except `IQ4_NL`, which is 32. + Codebook, + /// Ternary packings `TQ1_0` and `TQ2_0`. + Ternary, + /// Microscaling floats: `MXFP4` (E8M0 scale, 32/block) and `NVFP4` + /// (UE4M3 sub-block scales, 64/block). + MicroscaleFp, + /// An id upstream has removed. No [`GgmlType`] variant constructs one; the + /// slot exists so [`TRAITS`] can stay indexed by id. + Removed, +} + +/// What one ggml tensor type weighs, and what to call it. +/// +/// `blck_size` and `type_size` are ggml's own field names, and ggml's own +/// values: `type_size` bytes hold exactly `blck_size` elements. Both are 0 for +/// a removed id. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct QuantTraits { + /// The upstream ENUM name without its `GGML_TYPE_` prefix — `"Q4_K"`, + /// `"IQ2_XXS"`, `"BF16"`. This is the GGUF-facing spelling and what + /// [`GgmlType::as_str`] returns. + pub name: &'static str, + /// The name `ggml_type_name()` returns — `"q4_K"`, `"iq2_xxs"`, `"bf16"`. + /// Differs from [`Self::name`] in case only, which the fixture test asserts. + pub ggml_name: &'static str, + /// Elements per block. 1 for the unquantized types, 0 for a removed id. + pub blck_size: u32, + /// Bytes per block. 0 for a removed id. + pub type_size: u32, + /// aprender's family classification (see [`GgmlFamily`]). + pub family: GgmlFamily, +} + +/// Why an id is not a [`GgmlType`]. +/// +/// The distinction is the point: `4` is not an unknown id, it is `Q4_2`, which +/// upstream removed. A loader that says "unknown tensor type 4" sends its +/// reader looking for a type that was deleted in 2023. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum GgmlTypeError { + /// The id names a type upstream has removed. + Removed { + /// The removed id. + id: u32, + /// Its upstream name, e.g. `"Q4_0_4_8"`. + name: &'static str, + }, + /// The id is not in `0..GGML_TYPE_COUNT` at the pinned commit. + Unknown { + /// The id that was offered. + id: u32, + }, +} + +impl fmt::Display for GgmlTypeError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Removed { id, name } => { + write!(f, "ggml tensor type {id} ({name}) was removed upstream") + } + Self::Unknown { id } => write!(f, "unknown ggml tensor type {id}"), + } + } +} + +impl std::error::Error for GgmlTypeError {} + +/// The number of id slots upstream defines (`GGML_TYPE_COUNT`). +pub const GGML_TYPE_COUNT: u32 = 43; + +// GENERATED ROWS: the `GgmlType` variants and the `TRAITS` table below are +// emitted from fixtures/ggml_traits.json, which scripts/extract_ggml_traits.sh +// extracted from upstream ggml at the pinned comparator commit. Editing a row +// by hand turns tests/ggml_traits_fixture.rs RED. + +/// A ggml tensor type, by its upstream id. +/// +/// 35 variants: every LIVE id at the pinned commit, and only those. The 8 ids +/// upstream removed are not constructible — see [`GgmlType::try_from_id`], which +/// tells a removed id apart from one that never existed — but they keep their +/// slots in [`TRAITS`] so the table is indexed by id. +#[repr(u32)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)] +#[allow(non_camel_case_types)] // upstream ids: Q4_0, TQ1_0 — the tree's spelling +pub enum GgmlType { + /// `F32` — ggml `f32`: `blck_size` 1, `type_size` 4. + F32 = 0, + /// `F16` — ggml `f16`: `blck_size` 1, `type_size` 2. + F16 = 1, + /// `Q4_0` — ggml `q4_0`: `blck_size` 32, `type_size` 18. + Q4_0 = 2, + /// `Q4_1` — ggml `q4_1`: `blck_size` 32, `type_size` 20. + Q4_1 = 3, + /// `Q5_0` — ggml `q5_0`: `blck_size` 32, `type_size` 22. + Q5_0 = 6, + /// `Q5_1` — ggml `q5_1`: `blck_size` 32, `type_size` 24. + Q5_1 = 7, + /// `Q8_0` — ggml `q8_0`: `blck_size` 32, `type_size` 34. + Q8_0 = 8, + /// `Q8_1` — ggml `q8_1`: `blck_size` 32, `type_size` 36. + Q8_1 = 9, + /// `Q2_K` — ggml `q2_K`: `blck_size` 256, `type_size` 84. + Q2K = 10, + /// `Q3_K` — ggml `q3_K`: `blck_size` 256, `type_size` 110. + Q3K = 11, + /// `Q4_K` — ggml `q4_K`: `blck_size` 256, `type_size` 144. + Q4K = 12, + /// `Q5_K` — ggml `q5_K`: `blck_size` 256, `type_size` 176. + Q5K = 13, + /// `Q6_K` — ggml `q6_K`: `blck_size` 256, `type_size` 210. + Q6K = 14, + /// `Q8_K` — ggml `q8_K`: `blck_size` 256, `type_size` 292. + Q8K = 15, + /// `IQ2_XXS` — ggml `iq2_xxs`: `blck_size` 256, `type_size` 66. + IQ2XXS = 16, + /// `IQ2_XS` — ggml `iq2_xs`: `blck_size` 256, `type_size` 74. + IQ2XS = 17, + /// `IQ3_XXS` — ggml `iq3_xxs`: `blck_size` 256, `type_size` 98. + IQ3XXS = 18, + /// `IQ1_S` — ggml `iq1_s`: `blck_size` 256, `type_size` 50. + IQ1S = 19, + /// `IQ4_NL` — ggml `iq4_nl`: `blck_size` 32, `type_size` 18. + IQ4NL = 20, + /// `IQ3_S` — ggml `iq3_s`: `blck_size` 256, `type_size` 110. + IQ3S = 21, + /// `IQ2_S` — ggml `iq2_s`: `blck_size` 256, `type_size` 82. + IQ2S = 22, + /// `IQ4_XS` — ggml `iq4_xs`: `blck_size` 256, `type_size` 136. + IQ4XS = 23, + /// `I8` — ggml `i8`: `blck_size` 1, `type_size` 1. + I8 = 24, + /// `I16` — ggml `i16`: `blck_size` 1, `type_size` 2. + I16 = 25, + /// `I32` — ggml `i32`: `blck_size` 1, `type_size` 4. + I32 = 26, + /// `I64` — ggml `i64`: `blck_size` 1, `type_size` 8. + I64 = 27, + /// `F64` — ggml `f64`: `blck_size` 1, `type_size` 8. + F64 = 28, + /// `IQ1_M` — ggml `iq1_m`: `blck_size` 256, `type_size` 56. + IQ1M = 29, + /// `BF16` — ggml `bf16`: `blck_size` 1, `type_size` 2. + BF16 = 30, + /// `TQ1_0` — ggml `tq1_0`: `blck_size` 256, `type_size` 54. + TQ1_0 = 34, + /// `TQ2_0` — ggml `tq2_0`: `blck_size` 256, `type_size` 66. + TQ2_0 = 35, + /// `MXFP4` — ggml `mxfp4`: `blck_size` 32, `type_size` 17. + MXFP4 = 39, + /// `NVFP4` — ggml `nvfp4`: `blck_size` 64, `type_size` 36. + NVFP4 = 40, + /// `Q1_0` — ggml `q1_0`: `blck_size` 128, `type_size` 18. + Q1_0 = 41, + /// `Q2_0` — ggml `q2_0`: `blck_size` 64, `type_size` 18. + Q2_0 = 42, +} + +/// The ggml tensor-type table, INDEXED BY ID, all 43 slots including the 8 removed. +/// +/// Dense so that `TRAITS[t.as_id() as usize]` is the lookup and no id needs a +/// search. A removed slot carries `family: GgmlFamily::Removed` and upstream's +/// own zeroes, which is what ggml reports for it. +pub const TRAITS: [QuantTraits; 43] = [ + QuantTraits { + name: "F32", + ggml_name: "f32", + blck_size: 1, + type_size: 4, + family: GgmlFamily::Float, + }, // 0 + QuantTraits { + name: "F16", + ggml_name: "f16", + blck_size: 1, + type_size: 2, + family: GgmlFamily::Float, + }, // 1 + QuantTraits { + name: "Q4_0", + ggml_name: "q4_0", + blck_size: 32, + type_size: 18, + family: GgmlFamily::Affine, + }, // 2 + QuantTraits { + name: "Q4_1", + ggml_name: "q4_1", + blck_size: 32, + type_size: 20, + family: GgmlFamily::Affine, + }, // 3 + QuantTraits { + name: "Q4_2", + ggml_name: "DEPRECATED", + blck_size: 0, + type_size: 0, + family: GgmlFamily::Removed, + }, // 4 + QuantTraits { + name: "Q4_3", + ggml_name: "DEPRECATED", + blck_size: 0, + type_size: 0, + family: GgmlFamily::Removed, + }, // 5 + QuantTraits { + name: "Q5_0", + ggml_name: "q5_0", + blck_size: 32, + type_size: 22, + family: GgmlFamily::Affine, + }, // 6 + QuantTraits { + name: "Q5_1", + ggml_name: "q5_1", + blck_size: 32, + type_size: 24, + family: GgmlFamily::Affine, + }, // 7 + QuantTraits { + name: "Q8_0", + ggml_name: "q8_0", + blck_size: 32, + type_size: 34, + family: GgmlFamily::Affine, + }, // 8 + QuantTraits { + name: "Q8_1", + ggml_name: "q8_1", + blck_size: 32, + type_size: 36, + family: GgmlFamily::Affine, + }, // 9 + QuantTraits { + name: "Q2_K", + ggml_name: "q2_K", + blck_size: 256, + type_size: 84, + family: GgmlFamily::KQuant, + }, // 10 + QuantTraits { + name: "Q3_K", + ggml_name: "q3_K", + blck_size: 256, + type_size: 110, + family: GgmlFamily::KQuant, + }, // 11 + QuantTraits { + name: "Q4_K", + ggml_name: "q4_K", + blck_size: 256, + type_size: 144, + family: GgmlFamily::KQuant, + }, // 12 + QuantTraits { + name: "Q5_K", + ggml_name: "q5_K", + blck_size: 256, + type_size: 176, + family: GgmlFamily::KQuant, + }, // 13 + QuantTraits { + name: "Q6_K", + ggml_name: "q6_K", + blck_size: 256, + type_size: 210, + family: GgmlFamily::KQuant, + }, // 14 + QuantTraits { + name: "Q8_K", + ggml_name: "q8_K", + blck_size: 256, + type_size: 292, + family: GgmlFamily::KQuant, + }, // 15 + QuantTraits { + name: "IQ2_XXS", + ggml_name: "iq2_xxs", + blck_size: 256, + type_size: 66, + family: GgmlFamily::Codebook, + }, // 16 + QuantTraits { + name: "IQ2_XS", + ggml_name: "iq2_xs", + blck_size: 256, + type_size: 74, + family: GgmlFamily::Codebook, + }, // 17 + QuantTraits { + name: "IQ3_XXS", + ggml_name: "iq3_xxs", + blck_size: 256, + type_size: 98, + family: GgmlFamily::Codebook, + }, // 18 + QuantTraits { + name: "IQ1_S", + ggml_name: "iq1_s", + blck_size: 256, + type_size: 50, + family: GgmlFamily::Codebook, + }, // 19 + QuantTraits { + name: "IQ4_NL", + ggml_name: "iq4_nl", + blck_size: 32, + type_size: 18, + family: GgmlFamily::Codebook, + }, // 20 + QuantTraits { + name: "IQ3_S", + ggml_name: "iq3_s", + blck_size: 256, + type_size: 110, + family: GgmlFamily::Codebook, + }, // 21 + QuantTraits { + name: "IQ2_S", + ggml_name: "iq2_s", + blck_size: 256, + type_size: 82, + family: GgmlFamily::Codebook, + }, // 22 + QuantTraits { + name: "IQ4_XS", + ggml_name: "iq4_xs", + blck_size: 256, + type_size: 136, + family: GgmlFamily::Codebook, + }, // 23 + QuantTraits { + name: "I8", + ggml_name: "i8", + blck_size: 1, + type_size: 1, + family: GgmlFamily::Int, + }, // 24 + QuantTraits { + name: "I16", + ggml_name: "i16", + blck_size: 1, + type_size: 2, + family: GgmlFamily::Int, + }, // 25 + QuantTraits { + name: "I32", + ggml_name: "i32", + blck_size: 1, + type_size: 4, + family: GgmlFamily::Int, + }, // 26 + QuantTraits { + name: "I64", + ggml_name: "i64", + blck_size: 1, + type_size: 8, + family: GgmlFamily::Int, + }, // 27 + QuantTraits { + name: "F64", + ggml_name: "f64", + blck_size: 1, + type_size: 8, + family: GgmlFamily::Float, + }, // 28 + QuantTraits { + name: "IQ1_M", + ggml_name: "iq1_m", + blck_size: 256, + type_size: 56, + family: GgmlFamily::Codebook, + }, // 29 + QuantTraits { + name: "BF16", + ggml_name: "bf16", + blck_size: 1, + type_size: 2, + family: GgmlFamily::Float, + }, // 30 + QuantTraits { + name: "Q4_0_4_4", + ggml_name: "TYPE_Q4_0_4_4 REMOVED, use Q4_0 with runtime repacking", + blck_size: 0, + type_size: 0, + family: GgmlFamily::Removed, + }, // 31 + QuantTraits { + name: "Q4_0_4_8", + ggml_name: "TYPE_Q4_0_4_8 REMOVED, use Q4_0 with runtime repacking", + blck_size: 0, + type_size: 0, + family: GgmlFamily::Removed, + }, // 32 + QuantTraits { + name: "Q4_0_8_8", + ggml_name: "TYPE_Q4_0_8_8 REMOVED, use Q4_0 with runtime repacking", + blck_size: 0, + type_size: 0, + family: GgmlFamily::Removed, + }, // 33 + QuantTraits { + name: "TQ1_0", + ggml_name: "tq1_0", + blck_size: 256, + type_size: 54, + family: GgmlFamily::Ternary, + }, // 34 + QuantTraits { + name: "TQ2_0", + ggml_name: "tq2_0", + blck_size: 256, + type_size: 66, + family: GgmlFamily::Ternary, + }, // 35 + QuantTraits { + name: "IQ4_NL_4_4", + ggml_name: "TYPE_IQ4_NL_4_4 REMOVED, use IQ4_NL with runtime repacking", + blck_size: 0, + type_size: 0, + family: GgmlFamily::Removed, + }, // 36 + QuantTraits { + name: "IQ4_NL_4_8", + ggml_name: "TYPE_IQ4_NL_4_8 REMOVED, use IQ4_NL with runtime repacking", + blck_size: 0, + type_size: 0, + family: GgmlFamily::Removed, + }, // 37 + QuantTraits { + name: "IQ4_NL_8_8", + ggml_name: "TYPE_IQ4_NL_8_8 REMOVED, use IQ4_NL with runtime repacking", + blck_size: 0, + type_size: 0, + family: GgmlFamily::Removed, + }, // 38 + QuantTraits { + name: "MXFP4", + ggml_name: "mxfp4", + blck_size: 32, + type_size: 17, + family: GgmlFamily::MicroscaleFp, + }, // 39 + QuantTraits { + name: "NVFP4", + ggml_name: "nvfp4", + blck_size: 64, + type_size: 36, + family: GgmlFamily::MicroscaleFp, + }, // 40 + QuantTraits { + name: "Q1_0", + ggml_name: "q1_0", + blck_size: 128, + type_size: 18, + family: GgmlFamily::Affine, + }, // 41 + QuantTraits { + name: "Q2_0", + ggml_name: "q2_0", + blck_size: 64, + type_size: 18, + family: GgmlFamily::Affine, + }, // 42 +]; + +const fn from_id_inner(id: u32) -> Option { + match id { + 0 => Some(GgmlType::F32), + 1 => Some(GgmlType::F16), + 2 => Some(GgmlType::Q4_0), + 3 => Some(GgmlType::Q4_1), + 6 => Some(GgmlType::Q5_0), + 7 => Some(GgmlType::Q5_1), + 8 => Some(GgmlType::Q8_0), + 9 => Some(GgmlType::Q8_1), + 10 => Some(GgmlType::Q2K), + 11 => Some(GgmlType::Q3K), + 12 => Some(GgmlType::Q4K), + 13 => Some(GgmlType::Q5K), + 14 => Some(GgmlType::Q6K), + 15 => Some(GgmlType::Q8K), + 16 => Some(GgmlType::IQ2XXS), + 17 => Some(GgmlType::IQ2XS), + 18 => Some(GgmlType::IQ3XXS), + 19 => Some(GgmlType::IQ1S), + 20 => Some(GgmlType::IQ4NL), + 21 => Some(GgmlType::IQ3S), + 22 => Some(GgmlType::IQ2S), + 23 => Some(GgmlType::IQ4XS), + 24 => Some(GgmlType::I8), + 25 => Some(GgmlType::I16), + 26 => Some(GgmlType::I32), + 27 => Some(GgmlType::I64), + 28 => Some(GgmlType::F64), + 29 => Some(GgmlType::IQ1M), + 30 => Some(GgmlType::BF16), + 34 => Some(GgmlType::TQ1_0), + 35 => Some(GgmlType::TQ2_0), + 39 => Some(GgmlType::MXFP4), + 40 => Some(GgmlType::NVFP4), + 41 => Some(GgmlType::Q1_0), + 42 => Some(GgmlType::Q2_0), + _ => None, + } +} + +/// The 8 ids upstream has removed: constructible by no one, but distinguishable +/// from an id that never existed. `// GGML_TYPE_Q4_0_4_8 = 32,` in ggml.h says +/// nothing about being removed, so membership here is positional, never textual. +const REMOVED_IDS: [u32; 8] = [4, 5, 31, 32, 33, 36, 37, 38]; + +/// Every live variant, in id order — the iteration surface for tests and callers. +pub const ALL: [GgmlType; 35] = [ + GgmlType::F32, + GgmlType::F16, + GgmlType::Q4_0, + GgmlType::Q4_1, + GgmlType::Q5_0, + GgmlType::Q5_1, + GgmlType::Q8_0, + GgmlType::Q8_1, + GgmlType::Q2K, + GgmlType::Q3K, + GgmlType::Q4K, + GgmlType::Q5K, + GgmlType::Q6K, + GgmlType::Q8K, + GgmlType::IQ2XXS, + GgmlType::IQ2XS, + GgmlType::IQ3XXS, + GgmlType::IQ1S, + GgmlType::IQ4NL, + GgmlType::IQ3S, + GgmlType::IQ2S, + GgmlType::IQ4XS, + GgmlType::I8, + GgmlType::I16, + GgmlType::I32, + GgmlType::I64, + GgmlType::F64, + GgmlType::IQ1M, + GgmlType::BF16, + GgmlType::TQ1_0, + GgmlType::TQ2_0, + GgmlType::MXFP4, + GgmlType::NVFP4, + GgmlType::Q1_0, + GgmlType::Q2_0, +]; + +impl GgmlType { + /// The type with this id, or `None` if no live type has it. + /// + /// Returns `None` for both a removed id and an id that never existed; use + /// [`Self::try_from_id`] when the difference should reach the user. The + /// signature is `Option` because that is what serve's `GgmlQuantType::from_id` + /// returned, and M1 does not move its callers. + #[must_use] + pub const fn from_id(id: u32) -> Option { + from_id_inner(id) + } + + /// The type with this id, naming WHY it is not one when it is not. + /// + /// # Errors + /// + /// [`GgmlTypeError::Removed`] for the 8 ids upstream has deleted, + /// [`GgmlTypeError::Unknown`] for anything else outside the live set. + pub const fn try_from_id(id: u32) -> Result { + match from_id_inner(id) { + Some(t) => Ok(t), + None => { + if id < GGML_TYPE_COUNT { + // In range and not live => one of the 8 removed slots, whose + // TRAITS row still carries upstream's name for it. + Err(GgmlTypeError::Removed { + id, + name: TRAITS[id as usize].name, + }) + } else { + Err(GgmlTypeError::Unknown { id }) + } + } + } + } + + /// This type's upstream id. + #[must_use] + pub const fn as_id(self) -> u32 { + self as u32 + } + + /// This type's upstream id as a byte, for the APR tensor header. + /// + /// Total, with no truncation to hide: the largest id at the pin is 42. + #[must_use] + pub const fn as_byte(self) -> u8 { + self as u8 + } + + /// The GGUF-facing name: `"Q4_K"`, `"IQ2_XXS"`, `"BF16"`. + #[must_use] + pub const fn as_str(self) -> &'static str { + self.traits().name + } + + /// The name ggml itself prints: `"q4_K"`, `"iq2_xxs"`, `"bf16"`. + #[must_use] + pub const fn ggml_name(self) -> &'static str { + self.traits().ggml_name + } + + /// This type's row in [`TRAITS`]. + #[must_use] + pub const fn traits(self) -> &'static QuantTraits { + &TRAITS[self as usize] + } + + /// This type's family. + #[must_use] + pub const fn family(self) -> GgmlFamily { + self.traits().family + } + + /// Bytes per block — ggml's `type_size`. + #[must_use] + pub const fn block_bytes(&self) -> usize { + self.traits().type_size as usize + } + + /// Elements per block — ggml's `blck_size`. + #[must_use] + pub const fn block_size(&self) -> usize { + self.traits().blck_size as usize + } + + /// Bytes for `n_elements` weights, rounding a partial block UP. + /// + /// This is compute's arithmetic, unchanged, because its callers depend on + /// the rounding. It says nothing about whether a partial block is LEGAL — + /// [`Self::checked_tensor_bytes`] is the one that refuses. + #[must_use] + pub const fn tensor_bytes(&self, n_elements: usize) -> usize { + let bs = self.block_size(); + let n_blocks = n_elements.div_ceil(bs); + n_blocks * self.block_bytes() + } + + /// Bytes for `n_elements` weights, or `None` if that is not a whole number + /// of blocks or the product overflows. + /// + /// A quantized tensor whose element count is not a multiple of `blck_size` + /// is not a short tensor, it is a malformed one; rounding it up produces a + /// plausible byte count for a file that cannot be read. + #[must_use] + pub const fn checked_tensor_bytes(self, n_elements: usize) -> Option { + let bs = self.block_size(); + if bs == 0 || !n_elements.is_multiple_of(bs) { + return None; + } + match (n_elements / bs).checked_mul(self.block_bytes()) { + Some(bytes) => Some(bytes), + None => None, + } + } + + /// Parse a GGUF-facing name, accepting its exact spelling or its all-lowercase + /// form — `"Q4_K"` and `"q4_k"`, as serve's `from_str_lossy` accepted them. + /// + /// Note that ggml's own `"q4_K"` is neither, and is deliberately still not + /// accepted: M1 changes no parser's admitted set. + #[must_use] + pub fn from_str_lossy(s: &str) -> Option { + ALL.into_iter().find(|t| { + let name = t.as_str(); + s == name + || (s.eq_ignore_ascii_case(name) && s.chars().all(|c| !c.is_ascii_uppercase())) + }) + } +} + +impl fmt::Display for GgmlType { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.write_str(self.as_str()) + } +} + +// --------------------------------------------------------------------------- +// Const assertions: these fail the BUILD, not a test run. +// --------------------------------------------------------------------------- + +/// `TRAITS` is indexed by id, so every variant must find its own row there. +const _: () = { + let mut i = 0; + while i < ALL.len() { + let t = ALL[i]; + assert!( + TRAITS[t.as_id() as usize].blck_size > 0, + "a live type indexes a removed TRAITS row" + ); + i += 1; + } +}; + +/// Every removed id is a removed row, and there are exactly 8 of them. +const _: () = { + let mut i = 0; + while i < REMOVED_IDS.len() { + let id = REMOVED_IDS[i]; + assert!( + TRAITS[id as usize].type_size == 0, + "a removed id has a non-zero type_size" + ); + assert!(from_id_inner(id).is_none(), "a removed id is constructible"); + i += 1; + } + assert!( + REMOVED_IDS.len() + ALL.len() == TRAITS.len(), + "live + removed != 43" + ); +}; + +// --------------------------------------------------------------------------- +// Kani harness (KANI-GGMLT-001, contracts/ggml-type-v1.yaml) +// --------------------------------------------------------------------------- + +/// Exhaustive over the id space: resolution agrees with the table, and no +/// method panics or overflows on a live type. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(44)] +fn verify_ggml_type_id_space() { + let id: u32 = kani::any(); + kani::assume(id < GGML_TYPE_COUNT); + + let live = TRAITS[id as usize].blck_size > 0; + assert_eq!(GgmlType::from_id(id).is_some(), live); + assert_eq!(GgmlType::try_from_id(id).is_ok(), live); + + if let Some(t) = GgmlType::from_id(id) { + assert_eq!(t.as_id(), id); + assert!(t.block_size() > 0); + assert!(t.block_bytes() > 0); + assert_eq!(t.tensor_bytes(t.block_size()), t.block_bytes()); + assert_eq!( + t.checked_tensor_bytes(t.block_size()), + Some(t.block_bytes()) + ); + } +} diff --git a/crates/aprender-quant/src/lib.rs b/crates/aprender-quant/src/lib.rs index d136f8eb3c..dc578b46ff 100644 --- a/crates/aprender-quant/src/lib.rs +++ b/crates/aprender-quant/src/lib.rs @@ -58,6 +58,7 @@ #![warn(missing_docs)] mod dequantize; +pub mod ggml_type; mod quantize; mod transpose; @@ -75,6 +76,13 @@ pub use quantize::{ }; pub use transpose::{transpose_q4k_for_matmul, transpose_q5k_for_matmul, transpose_q6k_for_matmul}; +// PMAT-3430: the one ggml tensor-type enum and its upstream-extracted table. +// Re-exported at the crate root so a consumer writes `trueno_quant::GgmlType` +// and never has to know which module it lives in. +pub use ggml_type::{ + GgmlFamily, GgmlType, GgmlTypeError, QuantTraits, ALL, GGML_TYPE_COUNT, TRAITS, +}; + // ============================================================================ // Constants // ============================================================================ @@ -101,6 +109,18 @@ pub const Q6_K_BLOCK_SIZE: usize = 256; /// `Q6_K` super-block byte size pub const Q6_K_BLOCK_BYTES: usize = 210; +// THESE SIX CONSTANTS PREDATE `TRAITS` AND SAY THE SAME THING (PMAT-3430). +// They are kept — they are public API — but they may no longer drift from the +// upstream-extracted table: a mismatch is a COMPILE error, not a test failure. +const _: () = { + assert!(Q4_K_BLOCK_SIZE == TRAITS[GgmlType::Q4K.as_id() as usize].blck_size as usize); + assert!(Q4_K_BLOCK_BYTES == TRAITS[GgmlType::Q4K.as_id() as usize].type_size as usize); + assert!(Q5_K_BLOCK_SIZE == TRAITS[GgmlType::Q5K.as_id() as usize].blck_size as usize); + assert!(Q5_K_BLOCK_BYTES == TRAITS[GgmlType::Q5K.as_id() as usize].type_size as usize); + assert!(Q6_K_BLOCK_SIZE == TRAITS[GgmlType::Q6K.as_id() as usize].blck_size as usize); + assert!(Q6_K_BLOCK_BYTES == TRAITS[GgmlType::Q6K.as_id() as usize].type_size as usize); +}; + // ============================================================================ // f16 Conversion Helpers // ============================================================================ diff --git a/crates/aprender-quant/tests/ggml_traits_fixture.rs b/crates/aprender-quant/tests/ggml_traits_fixture.rs new file mode 100644 index 0000000000..f1c868912c --- /dev/null +++ b/crates/aprender-quant/tests/ggml_traits_fixture.rs @@ -0,0 +1,275 @@ +// A test asserts; `expect` here names the malformed fixture in the failure +// message, which is the diagnosis. The crate bans it in library code +// (Cargo.toml [lints.clippy]), and lib.rs already allows it under `cfg(test)` +// — an integration target is a separate crate, so it says so itself. +#![allow(clippy::expect_used, clippy::panic, clippy::unwrap_used)] + +//! `TRAITS` is upstream's table, or this test is RED. +//! +//! PMAT-3430, operator ruling 2026-09-20 clause 3: every live row's +//! `blck_size` / `type_size` equals the value extracted from ggml at the pinned +//! comparator commit, the extraction output is a checked-in fixture, and +//! mutating any one row turns this test RED. +//! +//! The fixture is `fixtures/ggml_traits.json`, written by +//! `scripts/extract_ggml_traits.sh` — which compiles a probe against the pinned +//! checkout's own libggml-base rather than parsing `sizeof(block_q4_1)` out of +//! a C initialiser by hand. Every in-tree table that had these numbers wrong +//! got them wrong by hand. +//! +//! WHAT THIS TEST DOES NOT CHECK: that the fixture's sha is still the pin. That +//! is a property of the repo, not of this crate (a packaged crate has no +//! `scripts/llama_pin.toml`), and it lives in +//! `crates/aprender-core/tests/monorepo_invariants.rs`. + +use serde_json::Value; +use trueno_quant::{GgmlFamily, GgmlType, GgmlTypeError, ALL, GGML_TYPE_COUNT, TRAITS}; + +const FIXTURE: &str = include_str!("../fixtures/ggml_traits.json"); + +fn fixture() -> Value { + serde_json::from_str(FIXTURE).expect("fixtures/ggml_traits.json is not valid JSON") +} + +fn rows(fx: &Value) -> Vec { + fx["types"] + .as_array() + .expect("fixture has no `types` array") + .clone() +} + +#[test] +fn traits_table_equals_the_upstream_fixture_row_for_row() { + let fx = fixture(); + let rows = rows(&fx); + assert_eq!( + rows.len(), + TRAITS.len(), + "the fixture has {} ids and TRAITS has {}", + rows.len(), + TRAITS.len() + ); + + for row in &rows { + let id = row["id"].as_u64().expect("row without an id") as usize; + let traits = &TRAITS[id]; + let live = row["status"] == "live"; + + assert_eq!( + traits.name, + row["enum_name"].as_str().expect("row without enum_name"), + "id {id}: name disagrees with upstream" + ); + assert_eq!( + traits.ggml_name, + row["ggml_name"].as_str().expect("row without ggml_name"), + "id {id}: ggml_name disagrees with upstream" + ); + assert_eq!( + u64::from(traits.blck_size), + row["blck_size"].as_u64().expect("row without blck_size"), + "id {id} ({}): blck_size disagrees with upstream", + traits.name + ); + assert_eq!( + u64::from(traits.type_size), + row["type_size"].as_u64().expect("row without type_size"), + "id {id} ({}): type_size disagrees with upstream", + traits.name + ); + assert_eq!( + traits.family == GgmlFamily::Removed, + !live, + "id {id} ({}): family Removed disagrees with the fixture's status", + traits.name + ); + } +} + +#[test] +fn the_family_classification_agrees_with_upstreams_is_quantized_flag() { + // The one link between aprender's family column and upstream that can fail: + // ggml has no families, but it does say which types are quantized. + for row in rows(&fixture()) { + let id = row["id"].as_u64().expect("row without an id") as usize; + let quantized = row["is_quantized"] + .as_bool() + .expect("row without is_quantized"); + let family = TRAITS[id].family; + let expected = !matches!( + family, + GgmlFamily::Float | GgmlFamily::Int | GgmlFamily::Removed + ); + assert_eq!( + expected, quantized, + "id {id} ({}): family {family:?} implies is_quantized {expected}, upstream says {quantized}", + TRAITS[id].name + ); + } +} + +#[test] +fn live_and_removed_counts_are_upstreams() { + let fx = fixture(); + assert_eq!( + fx["ggml_type_count"].as_u64(), + Some(u64::from(GGML_TYPE_COUNT)) + ); + assert_eq!(fx["live_count"].as_u64(), Some(ALL.len() as u64)); + assert_eq!( + fx["removed_count"].as_u64(), + Some((TRAITS.len() - ALL.len()) as u64) + ); +} + +#[test] +fn every_live_id_round_trips_and_no_removed_id_is_constructible() { + let fx = fixture(); + for row in rows(&fx) { + let id = row["id"].as_u64().expect("row without an id") as u32; + let name = row["enum_name"].as_str().expect("row without enum_name"); + if row["status"] == "live" { + let t = GgmlType::from_id(id) + .unwrap_or_else(|| panic!("live id {id} ({name}) is not constructible")); + assert_eq!(t.as_id(), id); + assert_eq!(u32::from(t.as_byte()), id); + assert_eq!(t.as_str(), name); + assert!(GgmlType::try_from_id(id).is_ok()); + } else { + assert!( + GgmlType::from_id(id).is_none(), + "removed id {id} ({name}) is constructible" + ); + assert_eq!( + GgmlType::try_from_id(id), + Err(GgmlTypeError::Removed { + id, + name: TRAITS[id as usize].name + }), + "removed id {id} must be reported as removed, not unknown" + ); + } + } + // Off the end of the table entirely. + assert_eq!( + GgmlType::try_from_id(GGML_TYPE_COUNT), + Err(GgmlTypeError::Unknown { + id: GGML_TYPE_COUNT + }) + ); + assert_eq!( + GgmlType::try_from_id(9999), + Err(GgmlTypeError::Unknown { id: 9999 }) + ); +} + +#[test] +fn the_two_names_differ_in_case_only() { + for t in ALL { + assert!( + t.as_str().eq_ignore_ascii_case(t.ggml_name()), + "{}: GGUF name and ggml name are not the same string modulo case ({} vs {})", + t.as_id(), + t.as_str(), + t.ggml_name() + ); + } +} + +#[test] +fn sizes_are_a_whole_number_of_bytes_per_block_and_tensor_bytes_agrees() { + for t in ALL { + assert!(t.block_size() > 0, "{t} has no block size"); + assert!(t.block_bytes() > 0, "{t} has no block bytes"); + // One full block, and a partial one. + assert_eq!(t.tensor_bytes(t.block_size()), t.block_bytes()); + assert_eq!( + t.checked_tensor_bytes(t.block_size()), + Some(t.block_bytes()) + ); + assert_eq!(t.tensor_bytes(0), 0); + if t.block_size() > 1 { + // tensor_bytes ROUNDS UP; checked_tensor_bytes REFUSES. That + // difference is the point of having both. + assert_eq!(t.tensor_bytes(1), t.block_bytes()); + assert_eq!(t.checked_tensor_bytes(1), None); + } + } +} + +/// The 16 ids and strings serve's `GgmlQuantType` carried before M1, asserted +/// here so the leaf cannot quietly change what they mean. Not the admitted set +/// of any parser — that stays each crate's own decision (#3430 Q1-c). +#[test] +fn serves_sixteen_strings_still_mean_what_they_meant() { + let serve: [(u32, &str); 16] = [ + (0, "F32"), + (1, "F16"), + (2, "Q4_0"), + (3, "Q4_1"), + (6, "Q5_0"), + (7, "Q5_1"), + (8, "Q8_0"), + (9, "Q8_1"), + (10, "Q2_K"), + (11, "Q3_K"), + (12, "Q4_K"), + (13, "Q5_K"), + (14, "Q6_K"), + (16, "IQ2_XXS"), + (17, "IQ2_XS"), + (30, "BF16"), + ]; + for (id, name) in serve { + let t = GgmlType::from_id(id).expect("serve's id must still be live"); + assert_eq!(t.as_str(), name, "id {id} renamed"); + assert_eq!( + format!("{t}"), + name, + "id {id} Displays differently from as_str" + ); + assert_eq!( + GgmlType::from_str_lossy(name), + Some(t), + "{name} no longer parses" + ); + assert_eq!( + GgmlType::from_str_lossy(&name.to_ascii_lowercase()), + Some(t), + "{name} no longer parses in lower case" + ); + } + // Mixed case was rejected before and is still rejected — including ggml's + // own spelling of the K-quants. + assert_eq!(GgmlType::from_str_lossy("q4_K"), None); + assert_eq!(GgmlType::from_str_lossy("Q4_k"), None); + assert_eq!(GgmlType::from_str_lossy("nonsense"), None); + assert_eq!(GgmlType::from_str_lossy(""), None); +} + +/// compute's `block_bytes` / `block_size` for its 15 ids, from before M1. +#[test] +fn computes_fifteen_sizes_are_unchanged() { + let compute: [(u32, usize, usize); 15] = [ + (0, 1, 4), + (1, 1, 2), + (2, 32, 18), + (3, 32, 20), + (6, 32, 22), + (7, 32, 24), + (8, 32, 34), + (9, 32, 36), + (10, 256, 84), + (11, 256, 110), + (12, 256, 144), + (13, 256, 176), + (14, 256, 210), + (15, 256, 292), + (30, 1, 2), + ]; + for (id, block_size, block_bytes) in compute { + let t = GgmlType::from_id(id).expect("compute's id must still be live"); + assert_eq!(t.block_size(), block_size, "{t} block_size changed"); + assert_eq!(t.block_bytes(), block_bytes, "{t} block_bytes changed"); + } +} diff --git a/docs/audits/impl-PMAT-3430-m1-leaf-receipt.md b/docs/audits/impl-PMAT-3430-m1-leaf-receipt.md new file mode 100644 index 0000000000..24bbff51d5 --- /dev/null +++ b/docs/audits/impl-PMAT-3430-m1-leaf-receipt.md @@ -0,0 +1,153 @@ +# PMAT-3430 M1 — receipt: the leaf (`GgmlType` + `TRAITS[43]`), oracle-extracted + +**Ticket:** #3430 (PP-QUANT-001 M1) · **Epic:** #3421 · **Plan:** #3452 (`docs/audits/impl-PMAT-3430-plan.md`, v4) +**Ruling executed:** operator, 2026-09-20 on #3430, clauses 1–6, with amendment 2'/2a/2b. +**Measured on:** `origin/main` @ `aff11bd0e`, 2026-09-20, this worktree. +**Verdict:** `PASS` for the leaf. Phases 3–4 (re-export + admission) and the consumer +table fixes are NOT in this PR — see §6. + +## 1. The oracle, resolved by reference + +Clause 2' makes the oracle `scripts/llama_pin.toml` `build_commit`, never a literal sha. + +| | value | how | +|---|---|---| +| pin of record | `d1d3c3396` | `llama_pin_get build_commit` — the repo's only reader of that file | +| checkout read | `/home/noah/src/llama.cpp-d1d3c3396` | `git -C … rev-parse HEAD` → `d1d3c3396aa13a5f239109a822666c4870490ad5`, clean tree | +| the ruling's `3173a5647` | **not used** | struck by amendment 2': it was the checkout the 43/35/8 count was first measured at, not a pin | + +`scripts/extract_ggml_traits.sh` refuses (exit 3) a checkout whose HEAD is not the pin, +and refuses (exit 4) a dirty one. Neither refusal is theoretical: both were exercised +while writing it — the first `-s` attempt pointed at `/home/noah/src/llama.cpp-master`. + +## 2. What was extracted, and why a probe rather than a parse + +ggml's `type_traits[]` gives `.type_size = sizeof(block_q4_1)`: a C expression, not a +number. **Every in-tree table that got these numbers wrong got them wrong by hand.** So +the extractor compiles a probe against the pinned checkout's own `libggml-base` and calls +`ggml_type_name` / `ggml_blck_size` / `ggml_type_size` / `ggml_is_quantized`. + +Result, independently reproducing the operator's 2b measurement: + +| | count | +|---|---| +| `GGML_TYPE_COUNT` | 43 | +| live | 35 | +| removed (commented out in the header) | 8 — ids 4, 5, 31, 32, 33, 36, 37, 38 | + +The header is still parsed, as a **cross-check that can fail**: a row is Removed because +its line is COMMENTED, never because the comment says "removed" (`// GGML_TYPE_Q4_0_4_8 = 32,` +says nothing), and the classification must then agree with the compiled table's +`blck_size == 0`. Disagreement is exit 7 and no fixture. + +## 3. The falsifier (clause 3): mutation, measured + +Four mutations of the leaf, one of the fixture, one of the pin. **All RED; every control GREEN.** + +| # | mutation | result | +|---|---|---| +| M1 | `TRAITS[9].type_size` 36 → 40 (gguf-py's Q8_1, refuted by the C `static_assert`) | RED — `traits_table_equals_the_upstream_fixture_row_for_row` *and* `computes_fifteen_sizes_are_unchanged` | +| M2 | `TRAITS[30].name` `BF16` → `Bf16` | RED — `serves_sixteen_strings_still_mean_what_they_meant` | +| M3 | `TRAITS[4].family` `Removed` → `Affine` | RED — the row-for-row test *and* the is_quantized cross-check, independently | +| M4 | fixture gains a fake id 43 | RED — three tests | +| M5 | fixture `pin_build_commit` → `39173bcac` (the superseded comparator) | RED — `falsify_ggml_001`, message naming both shas and the regeneration command | +| M6 | a row deleted from the fixture | RED — `falsify_ggml_002` ("the fixture lists 42 of 43 ids") | +| — | unmutated | GREEN: 8 + 3 tests | + +The extractor's own refusal is proved by a 7-case table on synthetic inputs +(`scripts/extract_ggml_traits_selftest.sh`), which needs no llama.cpp checkout and no +compiler, and is run in CI from `falsify_ggml_003` — which **refuses a zero-case run**, +because a case table that runs nothing passes vacuously. + +## 4. Clause 2a: a pin bump turns this RED in the bump's own PR + +The fixture records `pin_build_commit` and `resolved_sha`. +`crates/aprender-core/tests/monorepo_invariants.rs::falsify_ggml_001` asserts the first +still equals `llama_pin.toml build_commit`. It lives there and not in `aprender-quant` +because trueno_quant is **published**, and a packaged crate has no `scripts/llama_pin.toml` +— a test there could only skip, and a skip is how this becomes decoration. That target is +already in `ci/explicit-test-commands.d/030-*`, so it is not a dark target. The new +`aprender-quant` target is wired by `350-aprender-quant-ggml-traits-fixture.cmd`; +`check_explicit_test_commands.sh` passes (49 fragments). + +## 5. Findings — measured, and NOT fixed here + +These are clause 4's input (#3431's reconciliation table). Every value below is +`type_size / blck_size` at the pin. + +| # | site | in-tree | upstream | verdict | +|---|---|---|---|---| +| F1 | `aprender-compute` `GgmlType::block_bytes` / `block_size`, 15 ids | **all 15 correct** | — | no defect. The plan's premise that compute's `Q8_1 = 36` disagreed with upstream was wrong: 36 IS upstream (C `static_assert`); 40 is gguf-py's pre-f16 number, and it appears in no in-tree code | +| F2 | `aprender-core` `GgufTensor::byte_size`, `format/gguf/types.rs:365` | `Q4_0 \| Q4_1 => …*18` | Q4_1 is **20** | REGRESSION-shaped, but **latent**: `export_tensors_to_gguf` sizes tensors with `tensor.data.len()`, and `byte_size()` has **no non-test caller in the workspace**. So no GGUF was ever written wrong by it. Clause 5's "refusal on load" has no load path to attach to here | +| F3 | `aprender-core` `format/gguf/shape.rs:216-240` | all correct, incl. `Q4_1 = 20` | — | so core contains two tables of this fact that **disagree with each other** | +| F4 | `aprender-core` `ggml_dtype_element_size`, `format/safetensors.rs` | **10 of 31 rows wrong** | — | NEVER-WORKED. From index 16 the table follows the ORDER OF ITS OWN COMMENT (`… I8, I16, BF16, I32, I64, F64, IQ1_M`) instead of ggml id order (24 I8, 25 I16, 26 I32, 27 I64, 28 F64, 29 IQ1_M, 30 BF16), and the IQ rows carry values belonging to no type. Wrong: 16, 17, 18, 19, 21, 22, 23, 26, 27, 29, 30 | +| F5 | same table | ids 34, 35, 39–42 absent (`unwrap_or(4.0)`) | TQ1_0, TQ2_0, MXFP4, NVFP4, Q1_0, Q2_0 | the four "recent" types the ruling predicted would be NEVER-WORKED | +| F6 | `aprender-quant`'s own `Q4_K_BLOCK_BYTES` &c. | correct | — | **fixed structurally here**: six `const` assertions now make a drift a COMPILE error | + +**F4 is the one with a user-visible consequence.** `list_tensors_gguf` uses that table for +the #2569 truncation check. BF16 (id 30) read **0.375 B/elem instead of 2.0** — a 5.3× +under-estimate, so a truncated BF16 GGUF passed the extent check (fail-open) and +`apr tensors` printed a size 5.3× too small. The IQ rows err the other way and would +reject an intact file as truncated. PMAT-869 corrected four K-quant rows in this same +table in 2026-06 and stopped there: the audit-lags-main pattern, again. + +**Not fixed in this PR on purpose.** The fix is a lookup into `TRAITS`, which is what this +PR creates; doing both at once would make the leaf's "changes no behaviour" claim +unverifiable. The patch is written and measured (11 rows, every value an exact dyadic +fraction) and lands next, before Phases 3–4. + +## 6. Deviations from plan v4, each with its reason + +| plan said | this PR | why | +|---|---|---| +| Phase 0b (`Q4_1` 18→20) lands FIRST, before the leaf | leaf lands first; the table fixes follow, **derived from `TRAITS`** | the plan's ordering pre-dates the fixture existing. Fixing a table by hand-typing a second set of numbers is the defect, not the remedy. The leaf changes no behaviour, so nothing rides a refactor either way | +| `TRAITS[i].name` is the value `as_str()` returns | `name` (GGUF spelling, `"Q4_K"`, == `as_str()`) **and** `ggml_name` (`"q4_K"`, what `ggml_type_name` returns) | ggml's `type_name` is not serve's string. Carrying one and deriving the other would have meant a case transform in `const fn`; carrying both makes each a fixture-checked reading, and the test asserts they differ in case only | +| falsifier: `TRAITS` == gguf-py `GGML_QUANT_SIZES` with a named exception list | superseded by clause 3 | gguf-py is no longer consulted at all. The C table is the oracle, so Q8_1 is simply 36 and there is no exception list to rot | +| clause 5: wrong-sized types ship with a refusal on load | **no refusal shipped** | measured: the only wrong in-tree size (F2) sits in a function with no production caller, so there is no load to refuse. Stated rather than silently skipped: if #3431's reconciliation finds a wrong size on a real load path, that type gets clause 5's treatment there | + +## 6a. What adding ONE contract file actually costs, measured + +Not planned for, and worth recording because the plan did not see it and nor did I. +`contracts/ggml-type-v1.yaml` is one new file. It staled **three** tracked derivatives +and tripped a **fourth** guard, and they surfaced **one per CI round**, because each was +masked by the one before it — a failing job ends the run (#3587). + +| round | red | derivative | remedy | +|---|---|---|---| +| 1 | guard-cargo | `contracts/census.json` (1799 vs 1800) | `make contracts` (`pv census contracts`) | +| 1 | shard (1/3) | `contracts/contracts.nt` — `the_tracked_repo_graph_is_fresh`, R-18 | `pv extract contracts` | +| 2 | guard-cargo | README's generated `CONTRACT_COUNT` block — **invisible in round 1**, masked by the census red | `make readme-sync` | +| 3 | guard-tree | §11.1 ont-delta: touching README.md at all reclassifies the PR as a *sweep* | an `ont-delta:` line in the PR body | + +The fourth is the one to notice: it is not a derivative of the contract, it is a +consequence of the **remedy** for the third. `make readme-sync` is mandatory (guard-cargo +refuses without it) and README.md is a §11.1 prose sink, so fixing guard-cargo is what +made guard-tree fail. Neither guard can see the other, and nothing in either message says +so. + +Two further findings that cost a round each, both mine and both the same shape — reasoning +about an environment instead of measuring it: + +- **`git rev-parse --show-toplevel` fails in the container** ("dubious ownership in + repository at `/workspace`": the tree is uid 1000, the container is root). A script + locating its own siblings never needed git. Now derived from `$0`; generalised as #3586, + where 7 of 22 such call sites are unguarded and 15 more carry `|| pwd`, which does not + fail — it silently reads the wrong tree. +- **`python3` is absent from the container.** The extractor's classifier was python and + its case table drove it with python3, so the one artifact proving the classifier can + fail could not execute where the code executes. Ported to awk; the port is proved + faithful by regenerating the fixture **byte-identically**, and proved portable by + running the case table under `env -i PATH=` with no python3 on PATH. + I had inferred python's presence from `python3 scripts/lib/roadmap_merge.py --selftest` + in ci.yml — a step in a different job, on the host runner. + +## 7. Not in this PR + +Phases 3–4: the three enums become re-exports, each crate gets its admission function +(compute 15 ids, serve 16, core none), `Bf16`→`BF16`, `QTYPE_LABELS` removed, +`GgufTensor::byte_size` delegates. Until then `scripts/check_one_ggml_type_enum.sh` would +be RED, so it is not shipped yet either — a guard that cannot go green gets disabled +(#2512's lesson), and the honest sequence is guard-with-the-fix. + +The 558 bare-integer qtype lines, the 53 raw-integer fields, and the Table E merges remain +#3431 / T1 / #3423 as the plan says. diff --git a/docs/audits/quorum-PMAT-3430.json b/docs/audits/quorum-PMAT-3430.json new file mode 100644 index 0000000000..6babcfcec6 --- /dev/null +++ b/docs/audits/quorum-PMAT-3430.json @@ -0,0 +1,171 @@ +{ + "ticket": "PMAT-3430", + "base": "main", + "base_resolved": "origin/main", + "base_note": "local main differs from origin/main by 118 commit(s); judged against origin/main", + "head": "9bbcaa42b7ada310dcdbb5900b9e42fe6e86acd6", + "diff_sha256": "351e341eb58c9acff059a06e525b9f83fd54cc87bd02d92e9f8c62e94858b84b", + "width": 3, + "executor": "agy", + "prompt_mode": "inline", + "prompt_bytes": 96474, + "author": { + "model": "claude-opus-5", + "family": "claude", + "source": "flag" + }, + "agreed": true, + "lanes": [ + { + "lane": 1, + "status": "SUCCESS", + "verdict": "PASS", + "summary": "The diff correctly implements PMAT-3430 by adding the `GgmlType` enum and the 43-row `TRAITS` table in `aprender-quant` (which sits below `aprender-core` and `aprender-compute`). \n\n1. **Ticket Match**: It introduces precisely 35 live variants and 8 removed variants as documented, extracted directly from the upstream `llama.cpp` using the newly added C probe (`scripts/extract_ggml_traits.sh`).\n2. **Strict Verification**: The implementation is backed by robust compilation-time assertions (in `aprender-quant/src/lib.rs` and `ggml_type.rs`), integration tests ensuring that the `TRAITS` table identically matches the checked-in fixture, and Kani property-based tests verifying absence of panics across the entire ID space.\n3. **Receipt Validation**: The claims in the receipt (`docs/audits/impl-PMAT-3430-m1-leaf-receipt.md`) exactly align with the diff. All test mutations predicted in the receipt are enforced by tests like `falsify_ggml_001` and `traits_table_equals_the_upstream_fixture_row_for_row`.\n4. **No Unrequested Changes**: There is no behavioral drift or weakening of gates. Legacy values are kept but strictly bound to the `TRAITS` oracle at compile time.\n\nNo findings refute the implementation.", + "findings": [], + "raw_bytes": 3807, + "err_bytes": 100, + "envelope_status": "SUCCESS", + "verdict_source": "structured_output", + "grounding_check": "parity", + "model": "gemini-3.1-pro-high", + "model_measured": "gemini-3.1-pro-high", + "model_source": "measured", + "family": "gemini" + }, + { + "lane": 2, + "status": "SUCCESS", + "verdict": "PASS", + "summary": "Lane 2 verdict: PASS. PMAT-3430 (PP-QUANT-001 M1) introduces the leaf `#[repr(u32)] GgmlType` enum with 35 live variants (and 8 removed ids distinguishable via `try_from_id`), dense `TRAITS[43]` table in `crates/aprender-quant/src/ggml_type.rs` below core/compute, upstream-extracted fixture `fixtures/ggml_traits.json`, extraction tooling and self-test suite, monorepo pin invariants, contract `contracts/ggml-type-v1.yaml`, and CI wiring. All 8 fixture tests, 19 quant crate unit tests, 3 monorepo falsification invariant tests, the 7-case extractor self-test, and `check_explicit_test_commands.sh` pass cleanly with zero warnings under clippy and shellcheck. No gates were weakened, all receipt claims are grounded in the diff, and no unrequested behavior changes were introduced.", + "findings": [], + "raw_bytes": 2848, + "err_bytes": 0, + "envelope_status": "SUCCESS", + "verdict_source": "structured_output", + "grounding_check": "parity", + "model": "gemini-3.8-flash-high", + "model_measured": "gemini-3.8-flash-high", + "model_source": "measured", + "family": "gemini" + }, + { + "lane": 3, + "status": "SUCCESS", + "verdict": "PASS", + "summary": "Lane 3 of 3 review PASS for PMAT-3430 (PP-QUANT-001 M1).\n\nThe diff was rigorously checked against ticket PMAT-3430 and all requirements:\n1. Implements `#[repr(u32)] GgmlType` with 35 live variants corresponding to upstream ggml IDs 0..=42 in `crates/aprender-quant/src/ggml_type.rs`.\n2. Implements `TRAITS[43]` dense table covering all 43 slots (35 live and 8 removed), located in `crates/aprender-quant` (`trueno_quant`), strictly below `aprender-compute`, `aprender-core`, and `aprender-serve` in the dependency hierarchy.\n3. Oracle-derived fixture: verified against `scripts/llama_pin.toml` (`build_commit = \"d1d3c3396\"`), extracted from upstream checkout `/home/noah/src/llama.cpp-d1d3c3396` via `scripts/extract_ggml_traits.sh` and compiled probe. Re-running the extractor independently reproduced `crates/aprender-quant/fixtures/ggml_traits.json` byte-for-byte.\n4. Contract & Formal Verification: `contracts/ggml-type-v1.yaml` validated clean with `pv validate` (0 errors, 0 warnings). The Kani harness `verify_ggml_type_id_space` verified successfully via `cargo kani` (100/100 checks passed, 0 failures).\n5. All test suites pass: `cargo test -p aprender-quant` (28/28 passed), `cargo test -p aprender-core --test monorepo_invariants falsify_ggml` (3/3 passed), `scripts/extract_ggml_traits_selftest.sh` (7/7 cases passed), `scripts/check_explicit_test_commands.sh` (49 fragments ok).\n6. Linting & syntax: `cargo clippy -p aprender-quant --tests` (0 warnings), `bash -n` and `shellcheck -S error` (0 errors), `ruff check` (clean).\n7. Receipt verification: all claims in `docs/audits/impl-PMAT-3430-m1-leaf-receipt.md` are grounded by the diff and measurements. No gates were weakened, no tests assert opposite of ticket, and no out-of-scope modifications were introduced.", + "findings": [ + { + "claim": "GgmlType is defined as #[repr(u32)] with exactly 35 live variants matching active ggml tensor type IDs 0..=42 in the pinned comparator commit.", + "file": "crates/aprender-quant/src/ggml_type.rs", + "fix": "Verified enum definition with #[repr(u32)] and 35 live variants matching upstream ggml IDs 0..=42.", + "grounding": "cited", + "line": 140 + }, + { + "claim": "TRAITS is a dense 43-row table indexed by ggml ID (35 live + 8 Removed) with exact block size, byte size, and family classifications.", + "file": "crates/aprender-quant/src/ggml_type.rs", + "fix": "Verified pub const TRAITS: [QuantTraits; 43] dense array with 0 blck_size/type_size on all 8 removed entries.", + "grounding": "cited", + "line": 198 + }, + { + "claim": "Compile-time const assertions prevent drift between legacy K-quant constants and TRAITS.", + "file": "crates/aprender-quant/src/lib.rs", + "fix": "Verified const assertions for Q4_K, Q5_K, and Q6_K block size and byte constants against TRAITS table.", + "grounding": "cited", + "line": 115 + }, + { + "claim": "Integration test suite in ggml_traits_fixture.rs executes 8 tests verifying row-for-row equivalence with upstream fixture, family flags, and backwards compatibility.", + "file": "crates/aprender-quant/tests/ggml_traits_fixture.rs", + "fix": "Ran `cargo test -p aprender-quant --test ggml_traits_fixture` (8 passed, 0 failed).", + "grounding": "measured", + "line": 42 + }, + { + "claim": "Monorepo invariants falsify_ggml_001, falsify_ggml_002, and falsify_ggml_003 pass and enforce pin synchronization and extractor self-testing.", + "file": "crates/aprender-core/tests/monorepo_invariants.rs", + "fix": "Ran `cargo test -p aprender-core --test monorepo_invariants falsify_ggml` (3 passed, 0 failed).", + "grounding": "measured", + "line": 920 + } + ], + "raw_bytes": 8345, + "err_bytes": 0, + "envelope_status": "SUCCESS", + "verdict_source": "structured_output", + "grounding_check": "parity", + "model": "gemini-3.7-flash-high", + "model_measured": "gemini-3.7-flash-high", + "model_source": "measured", + "family": "gemini" + } + ], + "dissent": [], + "dedup": [ + { + "file": "crates/aprender-core/tests/monorepo_invariants.rs", + "line": 920, + "lanes_agreeing": [ + 3 + ], + "claims": [ + "Monorepo invariants falsify_ggml_001, falsify_ggml_002, and falsify_ggml_003 pass and enforce pin synchronization and extractor self-testing." + ] + }, + { + "file": "crates/aprender-quant/src/ggml_type.rs", + "line": 140, + "lanes_agreeing": [ + 3 + ], + "claims": [ + "GgmlType is defined as #[repr(u32)] with exactly 35 live variants matching active ggml tensor type IDs 0..=42 in the pinned comparator commit." + ] + }, + { + "file": "crates/aprender-quant/src/ggml_type.rs", + "line": 198, + "lanes_agreeing": [ + 3 + ], + "claims": [ + "TRAITS is a dense 43-row table indexed by ggml ID (35 live + 8 Removed) with exact block size, byte size, and family classifications." + ] + }, + { + "file": "crates/aprender-quant/src/lib.rs", + "line": 115, + "lanes_agreeing": [ + 3 + ], + "claims": [ + "Compile-time const assertions prevent drift between legacy K-quant constants and TRAITS." + ] + }, + { + "file": "crates/aprender-quant/tests/ggml_traits_fixture.rs", + "line": 42, + "lanes_agreeing": [ + 3 + ], + "claims": [ + "Integration test suite in ggml_traits_fixture.rs executes 8 tests verifying row-for-row equivalence with upstream fixture, family flags, and backwards compatibility." + ] + } + ], + "uncovered": [], + "coverage_source": "lanes", + "partial": false, + "partial_reasons": [], + "auto_merge": { + "checked": true, + "was_armed": false, + "disarmed": false, + "note": "auto-merge not armed" + }, + "lint": { + "ok": true, + "output": "receipt complete: kind=artifact lanes=3 author=claude-opus-5/claude" + } +} diff --git a/scripts/extract_ggml_traits.awk b/scripts/extract_ggml_traits.awk new file mode 100644 index 0000000000..5961389e34 --- /dev/null +++ b/scripts/extract_ggml_traits.awk @@ -0,0 +1,119 @@ +# extract_ggml_traits.awk — classify every ggml tensor-type id and emit the fixture. +# +# Called by scripts/extract_ggml_traits.sh. This half does the two jobs the shell +# should not do inline: it classifies each id live/Removed from `enum ggml_type` +# BY WHETHER ITS LINE IS COMMENTED (never by the comment's wording — +# `// GGML_TYPE_Q4_0_4_8 = 32,` says nothing), and it refuses to emit unless that +# classification agrees with the compiled table. +# +# WHY awk AND NOT python3. This was python3, and `workspace-test-shard (3/3)` +# failed with `python3: command not found` — the containerized job has no python. +# The self-test that proves this classifier can fail has to run WHERE CI RUNS, so +# the classifier may not depend on an interpreter that is absent there. awk is in +# the container, and in every base image this fleet uses. Measured, not assumed: +# the previous version of this file was python and its self-test was green on the +# dev box and exit 127 in CI. +# +# Inputs (as -v): pin, resolved, probe (TSV path), header (ggml.h path) +# Output: the fixture JSON on stdout. +# Exit: 0 ok · 2 malformed input · 7 the header and the compiled table disagree. + +function fail(msg) { print "extract: " msg > "/dev/stderr"; problems = problems + 1 } + +BEGIN { + if (pin == "" || resolved == "" || probe == "" || header == "") { + print "extract: pin, resolved, probe and header are all required" > "/dev/stderr" + exit 2 + } + + # ---- the header: id -> name, and whether its line is COMMENTED ------- + inside = 0; header_count = -1; n_header = 0 + while ((getline line < header) > 0) { + if (!inside) { if (line ~ /^[ \t]*enum ggml_type[ \t]*\{/) inside = 1; continue } + if (line ~ /^[ \t]*\};/) break + # A row is: optional `//`, then GGML_TYPE_ = , + if (line !~ /^[ \t]*(\/\/[ \t]*)?GGML_TYPE_[A-Z0-9_]+[ \t]*=[ \t]*[0-9]+[ \t]*,/) continue + commented = (line ~ /^[ \t]*\/\//) ? 1 : 0 + name = line; sub(/^[ \t]*(\/\/[ \t]*)?GGML_TYPE_/, "", name); sub(/[ \t]*=.*$/, "", name) + id = line; sub(/^[^=]*=[ \t]*/, "", id); sub(/[^0-9].*$/, "", id) + if (name == "COUNT") { header_count = id + 0; continue } + hname[id + 0] = name + hlive[id + 0] = (commented ? 0 : 1) + n_header = n_header + 1 + } + close(header) + if (header_count < 0) { print "extract: no GGML_TYPE_COUNT in enum ggml_type" > "/dev/stderr"; exit 2 } + + # ---- the compiled table, as the probe printed it --------------------- + if ((getline first < probe) <= 0) { print "extract: probe produced nothing" > "/dev/stderr"; exit 2 } + probe_count = first + 0 + n_probe = 0 + while ((getline line < probe) > 0) { + n = split(line, f, "\t") + if (n < 5) continue + id = f[1] + 0 + pname[id] = f[2]; pblck[id] = f[3] + 0; psize[id] = f[4] + 0; pquant[id] = (f[5] + 0 == 1) + seen[id] = 1 + n_probe = n_probe + 1 + } + close(probe) + + # ---- the cross-check that can FAIL ----------------------------------- + problems = 0 + if (header_count != probe_count) + fail("GGML_TYPE_COUNT: header " header_count " vs compiled " probe_count) + if (n_probe != probe_count) + fail("probe emitted " n_probe " rows for COUNT " probe_count) + for (i = 0; i < probe_count; i++) { + if (!(i in hname)) { fail("id " i " is in the compiled table but not in the header enum"); continue } + if (!(i in seen)) { fail("id " i " (" hname[i] ") is in the header but not in the compiled table"); continue } + compiled_live = (pblck[i] > 0) ? 1 : 0 + if (hlive[i] != compiled_live) + fail("id " i " (" hname[i] "): header says " (hlive[i] ? "live" : "Removed") \ + ", compiled table says " (compiled_live ? "live" : "Removed") \ + " (blck_size=" pblck[i] ", type_name=\"" pname[i] "\")") + if (hlive[i] && psize[i] <= 0) + fail("id " i " (" hname[i] ") is live but type_size is " psize[i]) + } + if (problems > 0) { + print "extract: the header and the compiled table disagree (" problems " problem(s))" > "/dev/stderr" + exit 7 + } + + # ---- emit ------------------------------------------------------------ + live = 0 + for (i = 0; i < probe_count; i++) if (hlive[i]) live = live + 1 + + print "{" + print " \"_comment\": \"GENERATED by scripts/extract_ggml_traits.sh from upstream ggml at the pinned comparator commit. Do not hand-edit: regenerate. trueno_quant asserts that pin_build_commit below still equals scripts/llama_pin.toml build_commit.\"," + print " \"source\": \"llama.cpp ggml/include/ggml.h + libggml-base type_traits\"," + print " \"pin_build_commit\": \"" pin "\"," + print " \"resolved_sha\": \"" resolved "\"," + print " \"ggml_type_count\": " probe_count "," + print " \"live_count\": " live "," + print " \"removed_count\": " (probe_count - live) "," + print " \"types\": [" + for (i = 0; i < probe_count; i++) { + print " {" + print " \"id\": " i "," + print " \"enum_name\": \"" hname[i] "\"," + print " \"ggml_name\": \"" json_escape(pname[i]) "\"," + print " \"status\": \"" (hlive[i] ? "live" : "removed") "\"," + print " \"blck_size\": " pblck[i] "," + print " \"type_size\": " psize[i] "," + print " \"is_quantized\": " (pquant[i] ? "true" : "false") + print " }" (i == probe_count - 1 ? "" : ",") + } + print " ]" + print "}" + exit 0 +} + +# ggml's removed rows carry a type_name with commas and spaces but no quotes or +# backslashes; escape anyway rather than rely on that staying true upstream. +function json_escape(s, out) { + out = s + gsub(/\\/, "\\\\", out) + gsub(/"/, "\\\"", out) + return out +} diff --git a/scripts/extract_ggml_traits.sh b/scripts/extract_ggml_traits.sh new file mode 100755 index 0000000000..27189abebc --- /dev/null +++ b/scripts/extract_ggml_traits.sh @@ -0,0 +1,180 @@ +#!/usr/bin/env bash +# extract_ggml_traits.sh — EXTRACT the ggml tensor-type table from upstream at +# the pinned comparator sha, and emit it as a checked-in fixture. +# +# WHY THIS EXISTS (PMAT-3430, operator ruling 2026-09-20 clauses 2'/2a/3). +# aprender carried three enums naming ggml tensor types, plus at least three +# separate byte-size tables for the same fact, and they disagreed — with each +# other and with upstream. The ruling settles the argument by naming an ORACLE: +# upstream ggml at `scripts/llama_pin.toml` `build_commit`, BY REFERENCE, never +# a literal sha. In-tree values are the defendant, never the reference. +# +# THE OUTPUT IS A FIXTURE, NOT A BUILD STEP. CI never runs this: it reads the +# committed JSON. The fixture RECORDS THE SHA IT WAS READ FROM, and +# `trueno_quant`'s tests assert that sha still equals the pin. A pin bump +# therefore turns the fixture RED until it is regenerated here, so the bump's +# cost is visible in the bump PR rather than discovered later (clause 2a; the +# general case is #3563). +# +# WHY IT COMPILES A PROBE INSTEAD OF PARSING THE TABLE. ggml's `type_traits[]` +# gives `.type_size = sizeof(block_q4_1)` — a C expression, not a number. Every +# in-tree table that got these numbers wrong got them wrong BY HAND. The only +# non-hand answer is to ask ggml itself, so the probe links against the pinned +# checkout's own libggml-base and calls `ggml_blck_size` / `ggml_type_size` / +# `ggml_type_name`. +# +# THE HEADER IS STILL PARSED, as a cross-check that can fail. `enum ggml_type` +# has EIGHT commented-out rows (4, 5, 31-33, 36-38) and only some of them say +# "removed" — `// GGML_TYPE_Q4_0_4_8 = 32,` says nothing at all. A first pass +# during the ruling classified rows by comment WORDING and returned 44/41/3 +# instead of 43/35/8. Here a row is Removed because its line is COMMENTED, and +# the classification is then required to agree with the compiled table's +# blck_size == 0. If they disagree the script refuses rather than emitting. +# +# Exit codes (each names one failure, so a caller can tell them apart): +# 0 ok · 2 pin/declaration unreadable · 3 checkout missing or wrong sha +# 4 checkout dirty · 5 libggml-base not built · 6 probe build/run failed +# 7 header parse vs compiled table disagree +set -euo pipefail + +usage() { + cat <<'USAGE' +usage: scripts/extract_ggml_traits.sh [-o OUT] [-s LLAMA_SRC] + + -o OUT write the fixture here (default: crates/aprender-quant/fixtures/ggml_traits.json) + -s LLAMA_SRC the llama.cpp checkout to read (default: $LLAMA_SRC, else + $HOME/src/llama.cpp-) + +The checkout must be AT the pinned build_commit, clean, and already built +(cmake -B build), because the probe links its libggml-base. +USAGE +} + +# The repo root is this script's parent, not `git rev-parse --show-toplevel`: +# git refuses a tree whose owner differs from the caller ("dubious ownership"), +# which is exactly the CI container's situation, and locating our own sibling +# files never needed to ask git anything. +repo_root=$(cd -- "$(dirname -- "$0")/.." && pwd) +[ -f "$repo_root/scripts/llama_pin.toml" ] || { + echo "extract_ggml_traits: no scripts/llama_pin.toml under '$repo_root'" >&2 + exit 2 +} + +out="$repo_root/crates/aprender-quant/fixtures/ggml_traits.json" +src="${LLAMA_SRC:-}" +opt="" +while getopts ":o:s:h" opt; do + case "$opt" in + o) out="$OPTARG" ;; + s) src="$OPTARG" ;; + h) usage; exit 0 ;; + *) usage >&2; exit 2 ;; + esac +done + +# ---------------------------------------------------------------- the oracle +# BY REFERENCE. The sha is never typed into this script (clause 2'). +# ONE producer for the declaration: `llama_pin_get` is the repo's only reader +# of scripts/llama_pin.toml, and a second hand-rolled sed here would be a +# second producer that can drift from it. +# +# ITS STATUS IS DELIBERATELY NOT PROPAGATED. Sourcing llama_bin.sh also runs +# `llama_bin_resolve` and returns THAT — whether a llama-bench BINARY is built +# on this host. Reading a C header needs no binary, so that status is not this +# script's business. What would be fatal is the reader not existing, which the +# next line checks. +# shellcheck source=scripts/llama_bin.sh +. "$repo_root/scripts/llama_bin.sh" || true +if ! command -v llama_pin_get >/dev/null 2>&1; then + echo "extract_ggml_traits: scripts/llama_bin.sh did not define llama_pin_get" >&2 + exit 2 +fi +pin=$(llama_pin_get build_commit "$repo_root/scripts/llama_pin.toml") || pin="" +if [ -z "$pin" ] || [ "$pin" = "UNPINNED" ]; then + echo "extract_ggml_traits: scripts/llama_pin.toml declares no usable build_commit (got '${pin}')" >&2 + exit 2 +fi + +[ -n "$src" ] || src="$HOME/src/llama.cpp-$pin" +# `[ -d "$src/.git" ]` would have been wrong: the pinned checkout here is a +# git WORKTREE, whose .git is a file. Ask git, not the filesystem. +if ! git -C "$src" rev-parse --git-dir >/dev/null 2>&1; then + echo "extract_ggml_traits: no llama.cpp checkout at '$src' (pin $pin). Pass -s, or set LLAMA_SRC." >&2 + exit 3 +fi + +resolved=$(git -C "$src" rev-parse HEAD) +case "$resolved" in + "$pin"*) : ;; + *) echo "extract_ggml_traits: '$src' is at $resolved, the pin is $pin — refusing to extract from a different oracle" >&2 + exit 3 ;; +esac + +dirty=$(git -C "$src" status --porcelain) +if [ -n "$dirty" ]; then + echo "extract_ggml_traits: '$src' has uncommitted changes — the oracle must be exactly the pinned commit" >&2 + exit 4 +fi + +lib_dir="$src/build/bin" +if [ ! -f "$lib_dir/libggml-base.so" ]; then + echo "extract_ggml_traits: $lib_dir/libggml-base.so is absent — build the pinned checkout first:" >&2 + echo " cmake -B build -S '$src' && cmake --build '$src/build' -j" >&2 + exit 5 +fi + +# ------------------------------------------------------------------ the probe +work=$(mktemp -d) +# "${work:?}" and not "$work": an empty variable here would make this `rm -rf /` +# (bashrs SEC011). mktemp cannot return empty under `set -e`, but the guard costs +# nothing and the failure mode is unrecoverable. +trap 'rm -rf "${work:?}"' EXIT + +cat > "$work/probe.c" <<'PROBE' +#include +#include "ggml.h" +int main(void) { + printf("%d\n", (int) GGML_TYPE_COUNT); + for (int t = 0; t < GGML_TYPE_COUNT; t++) { + printf("%d\t%s\t%lld\t%zu\t%d\n", t, + ggml_type_name((enum ggml_type) t), + (long long) ggml_blck_size((enum ggml_type) t), + ggml_type_size((enum ggml_type) t), + ggml_is_quantized((enum ggml_type) t) ? 1 : 0); + } + return 0; +} +PROBE + +cc_bin="${CC:-cc}" +command -v "$cc_bin" >/dev/null 2>&1 || cc_bin=gcc +if ! "$cc_bin" -O0 -I "$src/ggml/include" -o "$work/probe" "$work/probe.c" \ + -L "$lib_dir" -lggml-base -Wl,-rpath,"$lib_dir" > "$work/cc.log" 2>&1; then + echo "extract_ggml_traits: probe did not build:" >&2 + cat "$work/cc.log" >&2 + exit 6 +fi +if ! "$work/probe" > "$work/probe.tsv" 2> "$work/probe.err"; then + echo "extract_ggml_traits: probe did not run:" >&2 + cat "$work/probe.err" >&2 + exit 6 +fi + +# ------------------------------------------- header parse + cross-check + emit +# awk, NOT python3. This was python and `workspace-test-shard (3/3)` failed with +# `python3: command not found`: the containerized CI job has no python. The +# self-test that proves this classifier can FAIL has to run where CI runs, so the +# classifier may not depend on an interpreter that is absent there. +# +# The emitter writes to a temp file and is moved into place only on success, so a +# refusal (exit 7) never leaves a half-written fixture that the next reader +# mistakes for a real extraction. +if awk -v pin="$pin" -v resolved="$resolved" \ + -v probe="$work/probe.tsv" -v header="$src/ggml/include/ggml.h" \ + -f "$repo_root/scripts/extract_ggml_traits.awk" > "$work/fixture.json"; then + mv "$work/fixture.json" "$out" +else + exit 7 +fi + +echo "extract_ggml_traits: wrote $out from $src @ $resolved (pin $pin)" diff --git a/scripts/extract_ggml_traits_selftest.sh b/scripts/extract_ggml_traits_selftest.sh new file mode 100755 index 0000000000..4e76897974 --- /dev/null +++ b/scripts/extract_ggml_traits_selftest.sh @@ -0,0 +1,125 @@ +#!/usr/bin/env bash +# extract_ggml_traits_selftest.sh — the CASE TABLE for the ggml extractor. +# +# scripts/extract_ggml_traits.awk classifies each ggml id live-or-Removed and +# refuses to emit a fixture when that classification disagrees with the +# compiled table. This proves that refusal FIRES, and that it fires for the +# right reasons, on synthetic inputs — no llama.cpp checkout, no compiler, so +# it runs anywhere CI runs. +# +# IT EXISTS BECAUSE THE OBVIOUS EXTRACTOR IS WRONG. A one-line grep written +# during the ruling returned 44 types / 41 live / 3 removed instead of +# 43 / 35 / 8: it counted GGML_TYPE_COUNT as a type, and it called a commented +# row "live" whenever the comment did not contain the word "removed" — +# `// GGML_TYPE_Q4_0_4_8 = 32,` contains no such word. Case 5 below is that +# exact line, and it must be classified Removed. +# +# Guard regexes ship a case table (CLAUDE.md, verification discipline 7): the +# pattern was wrong five times in this repo and review caught none of them. +set -euo pipefail + +# THE ROOT COMES FROM THIS SCRIPT'S OWN PATH, NOT FROM git. `git rev-parse +# --show-toplevel` fails inside the CI container with "detected dubious +# ownership in repository at '/workspace'" — the bind-mounted tree is owned by +# uid 1000 and the container runs as root — and this self-test needs no git at +# all. Measured: it turned workspace-test-shard (3/3) red on the first run of +# this very file. +here=$(cd -- "$(dirname -- "$0")" && pwd) +emitter="$here/extract_ggml_traits.awk" +work=$(mktemp -d) +trap 'rm -rf "${work:?}"' EXIT + +fails=0 +ran=0 + +# A minimal but REAL-SHAPED header: two live ids, one commented row whose +# comment explains itself, one that says nothing, and the COUNT sentinel. +write_header() { + cat > "$1" <<'HDR' + enum ggml_type { + GGML_TYPE_F32 = 0, + GGML_TYPE_Q4_0 = 1, + // GGML_TYPE_Q4_2 = 2, support has been removed + // GGML_TYPE_Q4_0_4_8 = 3, + GGML_TYPE_COUNT = 4, + }; +HDR +} + +# The compiled table as the probe prints it: COUNT, then one row per id. +write_probe() { + cat > "$1" <<'PROBE' +4 +0 f32 1 4 0 +1 q4_0 32 18 1 +2 DEPRECATED 0 0 0 +3 TYPE_Q4_0_4_8 REMOVED, use Q4_0 with runtime repacking 0 0 0 +PROBE +} + +check() { + # check
+ ran=$((ran + 1)) + name=$1; want=$2; header=$3; probe=$4 + set +e + awk -v pin=deadbeef -v resolved=deadbeefcafe -v probe="$probe" -v header="$header" \ + -f "$emitter" > "$work/out.json" 2> "$work/log" + got=$? + set -e + if [ "$got" -eq "$want" ]; then + printf ' PASS %-58s exit %s\n' "$name" "$got" + else + printf ' FAIL %-58s exit %s, wanted %s\n' "$name" "$got" "$want" + sed 's/^/ /' "$work/log" + fails=$((fails + 1)) + fi +} + +printf 'extract_ggml_traits self-test\n' + +# --- MUST PASS ------------------------------------------------------------- +write_header "$work/ok.h" +write_probe "$work/ok.tsv" +check "control: header and compiled table agree" 0 "$work/ok.h" "$work/ok.tsv" + +# Case 5, the trap: `// GGML_TYPE_Q4_0_4_8 = 3,` carries no explanation at all +# and must STILL be Removed. The control above already contains it, so assert +# the emitted classification rather than just the exit code. +# Read the counts with sed rather than a JSON library: the fixture is emitted by +# this same awk program, so a shape change breaks BOTH sides at once and the +# Rust consumer (serde_json, tests/ggml_traits_fixture.rs) is the real parser. +removed=$(sed -n 's/^[[:space:]]*"removed_count":[[:space:]]*\([0-9]*\),.*$/\1/p' "$work/out.json") +live=$(sed -n 's/^[[:space:]]*"live_count":[[:space:]]*\([0-9]*\),.*$/\1/p' "$work/out.json") +ran=$((ran + 1)) +if [ "$removed" = "2" ] && [ "$live" = "2" ]; then + printf ' PASS %-58s live %s removed %s\n' "a commented row with no 'removed' wording is Removed" "$live" "$removed" +else + printf ' FAIL %-58s live %s removed %s (wanted 2 and 2)\n' "a commented row with no 'removed' wording is Removed" "$live" "$removed" + fails=$((fails + 1)) +fi + +# GGML_TYPE_COUNT is the sentinel, never a type. +ran=$((ran + 1)) +names=$(sed -n 's/^[[:space:]]*"enum_name":[[:space:]]*"\([^"]*\)",.*$/\1/p' "$work/out.json" | tr '\n' ',' | sed 's/,$//') +case "$names" in + *COUNT*) printf ' FAIL %-58s %s\n' "GGML_TYPE_COUNT is not emitted as a type" "$names"; fails=$((fails + 1)) ;; + *) printf ' PASS %-58s %s\n' "GGML_TYPE_COUNT is not emitted as a type" "$names" ;; +esac + +# --- MUST FAIL (exit 7) ---------------------------------------------------- +sed 's|// GGML_TYPE_Q4_0_4_8 = 3,|GGML_TYPE_Q4_0_4_8 = 3,|' "$work/ok.h" > "$work/uncommented.h" +check "header revives a row the compiled table calls dead" 7 "$work/uncommented.h" "$work/ok.tsv" + +sed 's| GGML_TYPE_Q4_0 = 1,| // GGML_TYPE_Q4_0 = 1,|' "$work/ok.h" > "$work/buried.h" +check "header buries a row the compiled table calls live" 7 "$work/buried.h" "$work/ok.tsv" + +sed 's|GGML_TYPE_COUNT = 4,|GGML_TYPE_COUNT = 5,|' "$work/ok.h" > "$work/count.h" +check "GGML_TYPE_COUNT disagrees with the compiled table" 7 "$work/count.h" "$work/ok.tsv" + +# A live row whose compiled type_size is zero: the table was read from the +# wrong place, or the type is a stub. +sed 's|^1\tq4_0\t32\t18\t1$|1\tq4_0\t32\t0\t1|' "$work/ok.tsv" > "$work/zero.tsv" +check "a live id with type_size 0" 7 "$work/ok.h" "$work/zero.tsv" + +printf '\n%s case(s), %s failure(s)\n' "$ran" "$fails" +[ "$fails" -eq 0 ] || exit 1