From c08b9a89e28b60a0fb779be816d9ba6f5b1b1a71 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 21 Sep 2026 20:30:37 +0200 Subject: [PATCH 1/4] feat(ladder): the Q4_K universe is read from each file's tensor header, never its name; the judge recomputes membership quantization". Row A's inventory was a *q4_k*/*q4k* filename glob. #3763 (row A2). - contract: inventory.patterns -> candidates [*.gguf, *.apr] (by extension) + member_dtype Q4_K; MCL-INV-009, FALSIFY-MCL-017. - model_ladder.sh: every candidate is read with `apr tensors --json` through apr_header (no GPU visible, no fleet lock); a member iff Q4_K is a most-frequent dtype of its >= 2-D tensors (ties are members; by count, since a Q4_K_M file is Q6_K by bytes); the receipt carries every candidate's histogram or its read error. - check_model_ladder.sh: refuses `patterns`; requires the candidates; names an unreadable one; recomputes membership and FAILs a Q4_K file left out of the inventory or a non-Q4_K file let in. - case table 47 -> 55; judge mutants filename-glob, header-excluded, header-included, tie-not-member and producer mutant header-sees-gpu are each killed. Measured dry run on lambda: f16, IQ4_XS and an f32 .apr are not members; the Q4_K_M GGUF, the q4k .apr and the Q4_K_M file renamed unlabelled-model.gguf are. Refs #3763 #3712 Co-Authored-By: Claude Opus 5 (1M context) --- contracts/model-capability-ladder-v1.yaml | 26 ++- docs/roadmaps/entries/PMAT-3763.yaml | 17 ++ docs/roadmaps/roadmap.yaml | 17 ++ scripts/check_model_ladder.sh | 44 +++- .../decline-no-required-host/ladder.yaml | 8 +- .../green-cells/ladder.yaml | 8 +- .../green-cells/receipts/gx10.json | 37 ++++ .../green-cells/receipts/lambda.json | 37 ++++ .../green-grown-ladder/ladder.yaml | 8 +- .../green-grown-ladder/receipts/gx10.json | 52 +++++ .../green-grown-ladder/receipts/lambda.json | 52 +++++ .../green-inventory-beyond-ladder/ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 52 +++++ .../green-rung-listed-one-host/ladder.yaml | 8 +- .../receipts/gx10.json | 52 +++++ .../receipts/lambda.json | 37 ++++ .../green-tie-is-a-member/expected_rc | 1 + .../green-tie-is-a-member/ladder.yaml | 36 ++++ .../green-tie-is-a-member/must_match | 1 + .../green-tie-is-a-member/receipts/gx10.json | 167 +++++++++++++++ .../receipts/lambda.json | 121 +++++++++++ .../green-tie-is-a-member/version | 1 + .../expected_rc | 1 + .../ladder.yaml | 36 ++++ .../must_match | 1 + .../receipts/gx10.json | 121 +++++++++++ .../receipts/lambda.json | 191 ++++++++++++++++++ .../green-unlabelled-q4k-is-a-member/version | 1 + .../lib/model_ladder_cases/green/ladder.yaml | 8 +- .../green/receipts/gx10.json | 37 ++++ .../green/receipts/lambda.json | 37 ++++ .../red-absent-required/ladder.yaml | 8 +- .../red-absent-required/receipts/gx10.json | 22 ++ .../red-absent-required/receipts/lambda.json | 37 ++++ .../red-candidate-unreadable/expected_rc | 1 + .../red-candidate-unreadable/ladder.yaml | 36 ++++ .../red-candidate-unreadable/must_match | 1 + .../receipts/gx10.json | 121 +++++++++++ .../receipts/lambda.json | 127 ++++++++++++ .../red-candidate-unreadable/version | 1 + .../red-capability/ladder.yaml | 8 +- .../red-capability/receipts/gx10.json | 37 ++++ .../red-capability/receipts/lambda.json | 37 ++++ .../ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-cells-block-dropped/ladder.yaml | 8 +- .../red-cells-block-dropped/ladder_main.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-cells-cotenant-refusal/ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-cells-duplicate-row/ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-cells-missing-cell/ladder.yaml | 8 +- .../red-cells-missing-cell/receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-cells-no-answer/ladder.yaml | 8 +- .../red-cells-no-answer/receipts/gx10.json | 37 ++++ .../red-cells-no-answer/receipts/lambda.json | 37 ++++ .../red-cells-no-cells/ladder.yaml | 8 +- .../red-cells-no-cells/receipts/gx10.json | 37 ++++ .../red-cells-no-cells/receipts/lambda.json | 39 +++- .../red-cells-no-context-length/ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-cells-oom-not-refusal/ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-cells-pass-fell-back/ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-cells-prompt-under-rung/ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-cells-rungs-file-missing/ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-cells-verb-dropped/ladder.yaml | 8 +- .../red-cells-verb-dropped/ladder_main.yaml | 8 +- .../red-cells-verb-dropped/receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-dropped-backend/ladder.yaml | 8 +- .../red-dropped-backend/receipts/gx10.json | 37 ++++ .../red-dropped-backend/receipts/lambda.json | 37 ++++ .../red-dropped-host-on-rung/ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-dropped-rung/ladder.yaml | 8 +- .../red-dropped-rung/receipts/gx10.json | 22 ++ .../red-dropped-rung/receipts/lambda.json | 22 ++ .../red-fallback/ladder.yaml | 8 +- .../red-fallback/receipts/gx10.json | 37 ++++ .../red-fallback/receipts/lambda.json | 37 ++++ .../model_ladder_cases/red-golden/ladder.yaml | 8 +- .../red-golden/receipts/gx10.json | 37 ++++ .../red-golden/receipts/lambda.json | 37 ++++ .../expected_rc | 1 + .../ladder.yaml | 39 ++++ .../red-inventory-by-filename-glob/must_match | 1 + .../receipts/gx10.json | 121 +++++++++++ .../receipts/lambda.json | 121 +++++++++++ .../red-inventory-by-filename-glob/version | 1 + .../red-inventory-empty/ladder.yaml | 8 +- .../red-inventory-empty/receipts/gx10.json | 8 +- .../red-inventory-empty/receipts/lambda.json | 37 ++++ .../red-inventory-model-fell-back/ladder.yaml | 8 +- .../receipts/gx10.json | 52 +++++ .../receipts/lambda.json | 37 ++++ .../ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 52 +++++ .../red-inventory-model-missing/ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 52 +++++ .../red-ladder-without-inventory/must_match | 2 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-listed-host-absent/ladder.yaml | 8 +- .../red-listed-host-absent/receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-missing-host/ladder.yaml | 8 +- .../red-missing-host/receipts/lambda.json | 37 ++++ .../red-non-q4k-in-inventory/expected_rc | 1 + .../red-non-q4k-in-inventory/ladder.yaml | 36 ++++ .../red-non-q4k-in-inventory/must_match | 1 + .../receipts/gx10.json | 165 +++++++++++++++ .../receipts/lambda.json | 121 +++++++++++ .../red-non-q4k-in-inventory/version | 1 + .../red-q4k-header-excluded/expected_rc | 1 + .../red-q4k-header-excluded/ladder.yaml | 36 ++++ .../red-q4k-header-excluded/must_match | 1 + .../receipts/gx10.json | 121 +++++++++++ .../receipts/lambda.json | 136 +++++++++++++ .../red-q4k-header-excluded/version | 1 + .../red-q4k-required-false/ladder.yaml | 8 +- .../red-q4k-required-false/receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-q4k-rung-cpu-only/ladder.yaml | 8 +- .../red-q4k-rung-cpu-only/receipts/gx10.json | 52 +++++ .../receipts/lambda.json | 52 +++++ .../red-receipt-v1-no-inventory/ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../expected_rc | 1 + .../ladder.yaml | 36 ++++ .../red-receipt-without-candidates/must_match | 1 + .../receipts/gx10.json | 121 +++++++++++ .../receipts/lambda.json | 89 ++++++++ .../red-receipt-without-candidates/version | 1 + .../red-skipped-is-not-passed/ladder.yaml | 8 +- .../receipts/gx10.json | 37 ++++ .../receipts/lambda.json | 37 ++++ .../red-stale-version/ladder.yaml | 8 +- .../red-stale-version/receipts/gx10.json | 37 ++++ .../red-stale-version/receipts/lambda.json | 37 ++++ .../red-tie-excluded/expected_rc | 1 + .../red-tie-excluded/ladder.yaml | 36 ++++ .../red-tie-excluded/must_match | 1 + .../red-tie-excluded/receipts/gx10.json | 134 ++++++++++++ .../red-tie-excluded/receipts/lambda.json | 121 +++++++++++ .../red-tie-excluded/version | 1 + .../red-vacuous-empty/ladder.yaml | 8 +- .../red-vacuous-empty/receipts/gx10.json | 8 +- .../red-vacuous-empty/receipts/lambda.json | 8 +- scripts/model_ladder.sh | 104 +++++++--- 192 files changed, 6109 insertions(+), 233 deletions(-) create mode 100644 docs/roadmaps/entries/PMAT-3763.yaml create mode 100644 scripts/lib/model_ladder_cases/green-tie-is-a-member/expected_rc create mode 100644 scripts/lib/model_ladder_cases/green-tie-is-a-member/ladder.yaml create mode 100644 scripts/lib/model_ladder_cases/green-tie-is-a-member/must_match create mode 100644 scripts/lib/model_ladder_cases/green-tie-is-a-member/receipts/gx10.json create mode 100644 scripts/lib/model_ladder_cases/green-tie-is-a-member/receipts/lambda.json create mode 100644 scripts/lib/model_ladder_cases/green-tie-is-a-member/version create mode 100644 scripts/lib/model_ladder_cases/green-unlabelled-q4k-is-a-member/expected_rc create mode 100644 scripts/lib/model_ladder_cases/green-unlabelled-q4k-is-a-member/ladder.yaml create mode 100644 scripts/lib/model_ladder_cases/green-unlabelled-q4k-is-a-member/must_match create mode 100644 scripts/lib/model_ladder_cases/green-unlabelled-q4k-is-a-member/receipts/gx10.json create mode 100644 scripts/lib/model_ladder_cases/green-unlabelled-q4k-is-a-member/receipts/lambda.json create mode 100644 scripts/lib/model_ladder_cases/green-unlabelled-q4k-is-a-member/version create mode 100644 scripts/lib/model_ladder_cases/red-candidate-unreadable/expected_rc create mode 100644 scripts/lib/model_ladder_cases/red-candidate-unreadable/ladder.yaml create mode 100644 scripts/lib/model_ladder_cases/red-candidate-unreadable/must_match create mode 100644 scripts/lib/model_ladder_cases/red-candidate-unreadable/receipts/gx10.json create mode 100644 scripts/lib/model_ladder_cases/red-candidate-unreadable/receipts/lambda.json create mode 100644 scripts/lib/model_ladder_cases/red-candidate-unreadable/version create mode 100644 scripts/lib/model_ladder_cases/red-inventory-by-filename-glob/expected_rc create mode 100644 scripts/lib/model_ladder_cases/red-inventory-by-filename-glob/ladder.yaml create mode 100644 scripts/lib/model_ladder_cases/red-inventory-by-filename-glob/must_match create mode 100644 scripts/lib/model_ladder_cases/red-inventory-by-filename-glob/receipts/gx10.json create mode 100644 scripts/lib/model_ladder_cases/red-inventory-by-filename-glob/receipts/lambda.json create mode 100644 scripts/lib/model_ladder_cases/red-inventory-by-filename-glob/version create mode 100644 scripts/lib/model_ladder_cases/red-non-q4k-in-inventory/expected_rc create mode 100644 scripts/lib/model_ladder_cases/red-non-q4k-in-inventory/ladder.yaml create mode 100644 scripts/lib/model_ladder_cases/red-non-q4k-in-inventory/must_match create mode 100644 scripts/lib/model_ladder_cases/red-non-q4k-in-inventory/receipts/gx10.json create mode 100644 scripts/lib/model_ladder_cases/red-non-q4k-in-inventory/receipts/lambda.json create mode 100644 scripts/lib/model_ladder_cases/red-non-q4k-in-inventory/version create mode 100644 scripts/lib/model_ladder_cases/red-q4k-header-excluded/expected_rc create mode 100644 scripts/lib/model_ladder_cases/red-q4k-header-excluded/ladder.yaml create mode 100644 scripts/lib/model_ladder_cases/red-q4k-header-excluded/must_match create mode 100644 scripts/lib/model_ladder_cases/red-q4k-header-excluded/receipts/gx10.json create mode 100644 scripts/lib/model_ladder_cases/red-q4k-header-excluded/receipts/lambda.json create mode 100644 scripts/lib/model_ladder_cases/red-q4k-header-excluded/version create mode 100644 scripts/lib/model_ladder_cases/red-receipt-without-candidates/expected_rc create mode 100644 scripts/lib/model_ladder_cases/red-receipt-without-candidates/ladder.yaml create mode 100644 scripts/lib/model_ladder_cases/red-receipt-without-candidates/must_match create mode 100644 scripts/lib/model_ladder_cases/red-receipt-without-candidates/receipts/gx10.json create mode 100644 scripts/lib/model_ladder_cases/red-receipt-without-candidates/receipts/lambda.json create mode 100644 scripts/lib/model_ladder_cases/red-receipt-without-candidates/version create mode 100644 scripts/lib/model_ladder_cases/red-tie-excluded/expected_rc create mode 100644 scripts/lib/model_ladder_cases/red-tie-excluded/ladder.yaml create mode 100644 scripts/lib/model_ladder_cases/red-tie-excluded/must_match create mode 100644 scripts/lib/model_ladder_cases/red-tie-excluded/receipts/gx10.json create mode 100644 scripts/lib/model_ladder_cases/red-tie-excluded/receipts/lambda.json create mode 100644 scripts/lib/model_ladder_cases/red-tie-excluded/version diff --git a/contracts/model-capability-ladder-v1.yaml b/contracts/model-capability-ladder-v1.yaml index 8c6859e96e..7cc738a647 100644 --- a/contracts/model-capability-ladder-v1.yaml +++ b/contracts/model-capability-ladder-v1.yaml @@ -49,9 +49,13 @@ entity: # publishing with "most working" is a "p0 tire fire"): # * NO Q4_K rung is optional. `required: false` on a Q4_K rung is refused by the # gate, and so is a Q4_K rung whose `backends` does not claim cuda. -# * The universe is what each host HOLDS, not this list. `inventory` names where -# and what to look for; scripts/model_ladder.sh measures every match on the host -# (on `inventory.backends`) and writes the list into the receipt (schema v2). +# * The universe is what each host HOLDS, not this list, and a file's quantization is +# read from its HEADER, never its name (issue author, #3712 done_when 1 clarified: +# "filename is not evidence of quantization"; #3763). scripts/model_ladder.sh reads +# every `inventory.candidates` file with `apr tensors --json`, keeps those whose +# dominant >= 2-D tensor dtype is `member_dtype` (by count: a Q4_K_M file's big Q6_K +# embedding outweighs its Q4_K matrices in bytes), measures them on +# `inventory.backends`, and writes EVERY candidate's histogram into the receipt. # An inventory model missing from the run, or not green on CUDA, is a FAIL # naming it. A rung is still how a model gets a pinned sha256 and a host list. ladder: @@ -60,7 +64,8 @@ ladder: - { id: gx10, isa: aarch64, gpu: "GB10", cc: sm_121, required: true } inventory: dirs: ["~/models", "~/.apr/models", "~/.cache/apr/models"] # depth 1, the fleet's model dirs - patterns: ["*q4_k*.gguf", "*q4k*.gguf", "*q4_k*.apr", "*q4k*.apr"] # case-insensitive + candidates: ["*.gguf", "*.apr"] # EVERY model file, by extension; its name is not evidence (#3763) + member_dtype: Q4_K # a member iff Q4_K is a most-frequent >= 2-D tensor dtype (`apr tensors --json`); ties are members backends: [cuda] # #3712 row B (operator 2026-09-21: "MORE than enough tokens for our needs (overdo it), and our verbs are # dogfooded, i.e chat with and without thinking, ditto run, ditto code"). A cell is (model, host, verb, @@ -157,7 +162,7 @@ equations: - "binary pinned via scripts/apr_bin.sh (built from HEAD) or DOGFOOD_ALLOW_UNPINNED=1 for the published-crate mode" - "every apr call runs through apr_locked: the fleet GPU lock (flock, bounded wait; a held lock is an ENV decline naming its holder) and choom -n 1000, so a measurement and never a CI job is the OOM victim (#3712; gx10 global OOM 2026-09-21 15:56:08Z killed CI containers)" host_receipt: - formula: "receipt(host) = {schema: apr-model-ladder-receipt/v2, host, version, sha, apr_sha, gpu, cc, inventory: [{file, sha256, bytes}], rungs: [{id, file, present, capability_match, golden_output, backends: {b: {ran, fallback, rc}}}]}" + formula: "receipt(host) = {schema: apr-model-ladder-receipt/v2, host, version, sha, apr_sha, gpu, cc, inventory: [{file, sha256, bytes}], candidates: [{file, bytes, dtype_counts, dominant, member} | {file, error}], rungs: [{id, file, present, capability_match, golden_output, backends: {b: {ran, fallback, rc}}}]}" domain: "evidence/dogfood/models//.json, written only by scripts/model_ladder.sh" invariants: - "receipt.version equals the cargo root version of the tree it was measured on" @@ -212,6 +217,11 @@ proof_obligations: property: "Every owed (model, verb, thinking, rung) cell is proved: pass where it fits, an honest refusal where it does not, and a pass on at least one required host" formal: "∀ host, m ∈ inventory(host), v ∈ cells.verbs, t ∈ modes(template(m)), r ∈ rungs(m): |rows(host, m, v, t, r)| = 1 ∧ (fits(m, r, total(host)) ⟹ pass(row) ∧ backend = cuda ∧ ¬fallback ∧ prompt_tokens ≥ tokens(r) ∧ answer_chars > 0 ∧ (t = on ⟹ think_closed)) ∧ (¬fits ⟹ refused(row) ∧ required_bytes(row) > total(host)) ∧ ∃ host': pass(host', m, v, t, r)" applies_to: gate_verdict + - id: MCL-INV-009 + type: invariant + property: "Q4_K membership is read from each file's header and recomputed by the judge — a name is not evidence" + formal: "∀ host, ∀ c ∈ receipt(host).candidates: readable(c) ∧ (member(c) ⟺ counts₂D(c)[member_dtype] = max counts₂D(c)) ∧ inventory(host) = { c.file | member(c) } ∧ patterns ∉ ladder.inventory" + applies_to: host_receipt - id: MCL-INV-007 type: invariant property: "The universe is the host's measured inventory — every Q4_K model it holds is in the run and green on CUDA" @@ -301,6 +311,12 @@ falsification_tests: test: "bash scripts/check_model_ladder.sh --self-test" if_fails: "a release dogfoods one verb at one short prompt with thinking off and calls the model family working" + - id: FALSIFY-MCL-017 + rule: "The Q4_K universe is the files whose header says Q4_K, whatever their name" + prediction: "check_model_ladder.sh --self-test: a ladder naming a filename glob, an unreadable candidate, a Q4_K-header file left out of the inventory, a non-Q4_K file let in, a Q4_K tie left out, and a receipt with no candidates are each RED naming it; an unlabelled Q4_K file and a tie are members (green); 4 judge mutants and the no-GPU header-read producer mutant are each killed" + test: "bash scripts/check_model_ladder.sh --self-test" + if_fails: "a `q4k` name holding fp16 is measured as Q4_K, or a Q4_K file with no quant in its name is never measured" + qa_gate: id: F-MCL-001 name: Model Capability Ladder diff --git a/docs/roadmaps/entries/PMAT-3763.yaml b/docs/roadmaps/entries/PMAT-3763.yaml new file mode 100644 index 0000000000..431ff9a3a3 --- /dev/null +++ b/docs/roadmaps/entries/PMAT-3763.yaml @@ -0,0 +1,17 @@ +- id: PMAT-3763 + github_issue: 3763 + item_type: task + title: '#3712 row A2: the Q4_K universe is read from each file''s tensor header (apr tensors --json), never a filename glob; the judge recomputes membership' + status: in_progress + priority: critical + assigned_to: null + created: '2026-09-21T00:00:00Z' + updated: '2026-09-21T00:00:00Z' + spec: null + acceptance_criteria: [] + phases: [] + subtasks: [] + estimated_effort: null + labels: + - kind:code + notes: 'ISSUE TEXT (#3712 done_when 1 clarification by the issue author, quoted verbatim): "done_when 1 clarified (issue author, cop aprender-04, 2026-09-21 18:15Z), after aprender-c3 asked whether `…-q4k.apr` (no underscore) counts as Q4_K. Under the operator''s rule ("tests are dervived from surface and SHACL enforced … it is hand coded not derived", #3745), filename is not evidence of quantization. A file is in the Q4_K universe iff its header says so: the dominant weight-tensor dtype read by apr''s own header reader (GGUF `file_type` / per-tensor ggml types; APR tensor dtypes) is Q4_K, with Q4_K_M/Q4_K_S included. A `*Q4_K*` filename glob is refused as the universe definition. Every candidate model file on the host (`*.gguf`, `*.apr`) is read, and the receipt lists each file with its measured dominant dtype, so a mislabelled file is visible both ways: a `q4k` name holding fp16 is excluded, and an unlabelled file holding Q4_K is included." COP RULING (2026-09-21, A2 design approved): candidates = every *.gguf/*.apr under the model dirs, by extension; membership = Q4_K is a most-frequent >= 2-D tensor dtype, ties included (the strict side); the receipt carries every candidate''s histogram, the JUDGE recomputes membership from it, an unreadable candidate is a named FAIL; the header read runs through a no-GPU wrapper, not the fleet lock; apr inspect''s wrong `quantization` field is filed separately (#3762) and not fixed here. WHAT THIS ROW DOES: contracts/model-capability-ladder-v1.yaml `inventory.patterns` (the *q4_k*/*q4k* filename glob) is replaced by `candidates: [*.gguf, *.apr]` and `member_dtype: Q4_K`; MCL-INV-009, FALSIFY-MCL-017. scripts/model_ladder.sh reads every candidate with `apr tensors --json` through apr_header (CUDA_VISIBLE_DEVICES set empty, no lock), counts the dtypes of its >= 2-D tensors, and writes EVERY candidate (histogram, dominant, member | error) into the receipt; the inventory it measures is the members. scripts/check_model_ladder.sh refuses a ladder that still names `patterns`, requires the candidates list, names an unreadable candidate, recomputes membership from each histogram, and FAILs a Q4_K-header file missing from the inventory (left out by its name) and a non-Q4_K file in it (let in by its name). BY COUNT, NOT BYTES, measured: Qwen3.5-0.8B-Q4_K_M.gguf is Q6_K by bytes (its 248k-vocab embedding/output) but Q4_K by count of >= 2-D tensors (Q4_K 98, Q5_K 36, Q8_0 36, F32 18, Q6_K 17). MEASURED dry run on lambda, real files: Qwen2.5-0.5B-f16.gguf not a member [F16]; Qwen3.5-0.8B-IQ4_XS.gguf not a member [IQ4_XS]; Qwen3.5-0.8B-Q4_K_M.gguf MEMBER; qwen2.5-coder-1.5b-instruct-q4k.apr MEMBER; qwen2.5-coder-1.5b-instruct-st.apr not a member [F32]; the Q4_K_M file symlinked as unlabelled-model.gguf MEMBER. Case table 47 -> 55; 4 judge mutants (filename-glob, header-excluded, header-included, tie-not-member) and the producer mutant header-sees-gpu are each killed. WHERE THE GATE RUNS: check_model_ladder.sh is declared only in Cargo.toml [package.metadata.dogfood] (the T-2 pre-publish dogfood) and listed in scripts/unwired_guards_baseline.txt; no PR workflow runs it, so its real-run RED (no receipts yet for the cut) is the release bar, not a PR red. Stacked on #3738 (row B1), which is stacked on #3721 (row A).' diff --git a/docs/roadmaps/roadmap.yaml b/docs/roadmaps/roadmap.yaml index 6897fc231a..d006925c3a 100644 --- a/docs/roadmaps/roadmap.yaml +++ b/docs/roadmaps/roadmap.yaml @@ -20537,6 +20537,23 @@ roadmap: labels: - kind:code notes: 'SCOPE: scripts/llama_bin.sh (one line: the commit-token extraction), evidence/parity/pin-bump-d1d3c3396/RESOLVE-{intel,mini}.txt, and this fragment. STACKED on #3563(A) (branch PMAT-3563-llama-pin-resolves-both-hosts @ 8fe36c080, receipt committed), whose canonical-location resolver it uses; fold #3563(A) first. HOST PROVISIONING (the cop''s fleet row; the operator: "you are traffic cop and have ssh, you fix anything you need"; done before the 0.69.1 train starts, not inside it): intel: `cmake --build ~/src/llama.cpp-d1d3c3396/build --target llama-bench llama-server llama-tokenize llama-cli -j 8` under nice 19 / ionice idle (incremental; the existing cache already matched build_flags_intel, GGML_NATIVE=ON, GGML_CUDA=OFF), BUILD_EXIT=0. mini: `git clone https://github.com/ggml-org/llama.cpp ~/src/llama.cpp-d1d3c3396 && git checkout d1d3c3396aa13a5f239109a822666c4870490ad5 && cmake -B build -DGGML_METAL=ON` (build_flags_mini verbatim), then the same four targets, BUILD_EXIT=0. DEFECT FOUND BY THE PROOF (fixed here): on mini, #3563(A)''s resolver refused the correct build as wrong_build. Its commit extraction `sed -nE ''s/…/p;t;s/…/p''` is one expression, and BSD sed (macOS /usr/bin/sed) reads everything after `t` as a LABEL, so it failed with "undefined label" and extracted nothing. Measured pre-fix on mini, rc 1: `sed: 2: "s/.*commit ([0-9a-f]{7, ...": undefined label '';s/.*\(([0-9a-f]{7,40})\).*/\1/p''` then `FAIL llama.cpp named but NOT the declared build (wrong_build)`. FIX: the same three commands as separate -e arguments. PROBE: 4 inputs (commit d1d3c3396, paren abcdef1, a 6-digit commit, no commit) give byte-identical output under GNU sed 4.8 (lambda) and BSD sed (mini): d1d3c3396 / abcdef1 / empty / empty. MEASURED AFTER: `bash scripts/check_llama_pin.sh` rc 0, 43 ok rows, both mutants still killed; live `env -u LLAMA_BENCH_PATH LLAMA_PIN_HOST= bash scripts/llama_bin.sh` rc 0 on intel (`version: 0.4.1-dev (build 2744, commit d1d3c3396)`) and on mini (`version: 0.4.1-dev (build 10987, commit d1d3c3396)`), in the committed RESOLVE files. REMAINDER: the llama.cpp builds live in user-space trees under ~/src on each host; declaring them in forjar (so a re-provisioned host rebuilds them) is not in this PR.' +- id: PMAT-3763 + github_issue: 3763 + item_type: task + title: '#3712 row A2: the Q4_K universe is read from each file''s tensor header (apr tensors --json), never a filename glob; the judge recomputes membership' + status: in_progress + priority: critical + assigned_to: null + created: '2026-09-21T00:00:00Z' + updated: '2026-09-21T00:00:00Z' + spec: null + acceptance_criteria: [] + phases: [] + subtasks: [] + estimated_effort: null + labels: + - kind:code + notes: 'ISSUE TEXT (#3712 done_when 1 clarification by the issue author, quoted verbatim): "done_when 1 clarified (issue author, cop aprender-04, 2026-09-21 18:15Z), after aprender-c3 asked whether `…-q4k.apr` (no underscore) counts as Q4_K. Under the operator''s rule ("tests are dervived from surface and SHACL enforced … it is hand coded not derived", #3745), filename is not evidence of quantization. A file is in the Q4_K universe iff its header says so: the dominant weight-tensor dtype read by apr''s own header reader (GGUF `file_type` / per-tensor ggml types; APR tensor dtypes) is Q4_K, with Q4_K_M/Q4_K_S included. A `*Q4_K*` filename glob is refused as the universe definition. Every candidate model file on the host (`*.gguf`, `*.apr`) is read, and the receipt lists each file with its measured dominant dtype, so a mislabelled file is visible both ways: a `q4k` name holding fp16 is excluded, and an unlabelled file holding Q4_K is included." COP RULING (2026-09-21, A2 design approved): candidates = every *.gguf/*.apr under the model dirs, by extension; membership = Q4_K is a most-frequent >= 2-D tensor dtype, ties included (the strict side); the receipt carries every candidate''s histogram, the JUDGE recomputes membership from it, an unreadable candidate is a named FAIL; the header read runs through a no-GPU wrapper, not the fleet lock; apr inspect''s wrong `quantization` field is filed separately (#3762) and not fixed here. WHAT THIS ROW DOES: contracts/model-capability-ladder-v1.yaml `inventory.patterns` (the *q4_k*/*q4k* filename glob) is replaced by `candidates: [*.gguf, *.apr]` and `member_dtype: Q4_K`; MCL-INV-009, FALSIFY-MCL-017. scripts/model_ladder.sh reads every candidate with `apr tensors --json` through apr_header (CUDA_VISIBLE_DEVICES set empty, no lock), counts the dtypes of its >= 2-D tensors, and writes EVERY candidate (histogram, dominant, member | error) into the receipt; the inventory it measures is the members. scripts/check_model_ladder.sh refuses a ladder that still names `patterns`, requires the candidates list, names an unreadable candidate, recomputes membership from each histogram, and FAILs a Q4_K-header file missing from the inventory (left out by its name) and a non-Q4_K file in it (let in by its name). BY COUNT, NOT BYTES, measured: Qwen3.5-0.8B-Q4_K_M.gguf is Q6_K by bytes (its 248k-vocab embedding/output) but Q4_K by count of >= 2-D tensors (Q4_K 98, Q5_K 36, Q8_0 36, F32 18, Q6_K 17). MEASURED dry run on lambda, real files: Qwen2.5-0.5B-f16.gguf not a member [F16]; Qwen3.5-0.8B-IQ4_XS.gguf not a member [IQ4_XS]; Qwen3.5-0.8B-Q4_K_M.gguf MEMBER; qwen2.5-coder-1.5b-instruct-q4k.apr MEMBER; qwen2.5-coder-1.5b-instruct-st.apr not a member [F32]; the Q4_K_M file symlinked as unlabelled-model.gguf MEMBER. Case table 47 -> 55; 4 judge mutants (filename-glob, header-excluded, header-included, tie-not-member) and the producer mutant header-sees-gpu are each killed. WHERE THE GATE RUNS: check_model_ladder.sh is declared only in Cargo.toml [package.metadata.dogfood] (the T-2 pre-publish dogfood) and listed in scripts/unwired_guards_baseline.txt; no PR workflow runs it, so its real-run RED (no receipts yet for the cut) is the release bar, not a PR red. Stacked on #3738 (row B1), which is stacked on #3721 (row A).' - id: PMAT-3770 github_issue: 3770 item_type: task diff --git a/scripts/check_model_ladder.sh b/scripts/check_model_ladder.sh index b42e950d81..3fbe023dd6 100755 --- a/scripts/check_model_ladder.sh +++ b/scripts/check_model_ladder.sh @@ -91,9 +91,14 @@ for r in rungs: print(f"FAIL rung {r['id']} is a Q4_K rung with required: {r.get('required')!r} — no Q4_K model is optional; every one must be green on CUDA (#3712)"); rc = 1 if is_q4k(r) and "cuda" not in (r.get("backends") or []): print(f"FAIL rung {r['id']} is a Q4_K rung that does not claim cuda — every Q4_K model must be green on CUDA (#3712)"); rc = 1 -inv_backends = list((L.get("inventory") or {}).get("backends") or []) -if not (L.get("inventory") or {}).get("patterns") or "cuda" not in inv_backends: - print("FAIL the ladder declares no inventory (patterns + backends incl. cuda) — the universe cannot be the host's measured Q4_K models (#3712)"); rc = 1 +inv_spec = L.get("inventory") or {} +inv_backends = list(inv_spec.get("backends") or []) +want_dtype = str(inv_spec.get("member_dtype") or "").upper() +# #3763: a file's name is not evidence of its quantization. The universe is read from the header. +if inv_spec.get("patterns"): + print("FAIL the ladder names a filename glob (inventory.patterns) — a file's name is not evidence of its quantization; its header is (#3763)"); rc = 1 +if not inv_spec.get("candidates") or not want_dtype or "cuda" not in inv_backends: + print("FAIL the ladder declares no header-read inventory (candidates + member_dtype + backends incl. cuda) — the universe cannot be the host's measured Q4_K models (#3712, #3763)"); rc = 1 # anti-shrink vs origin/main if main_p and os.path.exists(main_p): try: @@ -146,6 +151,27 @@ for h in hosts: print(f"FAIL {h['id']:7} receipt carries no measured inventory (schema {R.get('schema')!r}) — the universe is what the host HOLDS, not a list (#3712)"); rc = 1; continue if not inv: print(f"FAIL {h['id']:7} measured inventory is EMPTY — a host holding no Q4_K model proved nothing (#3712)"); rc = 1; continue + # #3763: recompute every candidate's membership from its header histogram. The inventory must be + # EXACTLY the members: a Q4_K file left out, or a non-Q4_K file let in, went by its name. + cands = R.get("candidates") + if not want_dtype: + pass # the ladder names no member_dtype: already a FAIL above, and there is nothing to recompute against + elif not isinstance(cands, list) or not cands: + print(f"FAIL {h['id']:7} receipt lists no header-read candidates — membership cannot be recomputed, so its inventory is only a claim (#3763)"); rc = 1; continue + members = set() + for c in (cands if want_dtype else []): + cf = c.get("file") + if c.get("error") or not c.get("dtype_counts"): + print(f"FAIL {h['id']:7} candidate {cf} is UNREADABLE ({c.get('error', 'no dtype histogram')}) — a file whose header was not read cannot be excluded (#3763)"); rc = 1; continue + counts = {str(k).upper(): int(v) for k, v in c["dtype_counts"].items()} + top = max(counts.values()) + if top > 0 and counts.get(want_dtype, 0) == top: # a tie at the top is a member: the strict side + members.add(cf) + inv_files = {x.get("file") for x in inv} if want_dtype else set() + for f in sorted(members - inv_files): + print(f"FAIL {h['id']:7} {f} is {want_dtype} by its header but is NOT in the inventory — left out by its name? (#3763)"); rc = 1 + for f in sorted(inv_files - members): + print(f"FAIL {h['id']:7} {f} is in the inventory but its header is not {want_dtype}-dominant — let in by its name? (#3763)"); rc = 1 good[h["id"]] = R by = {r.get("id"): r for r in R.get("rungs", [])} by_file = {x.get("file"): x for x in R.get("rungs", []) if x.get("file")} @@ -226,7 +252,8 @@ lock_probe() { local prod=$1 w=$2 out rc hp bad=0 mkdir -p "$w"; : > "$w/lock" printf '#!/usr/bin/env bash\nif flock -n "$FAKE_LOCK" true; then l=UNLOCKED; else l=LOCKED; fi\necho "fake-apr $1 lock=$l oom=$(cat /proc/self/oom_score_adj)"\n' > "$w/apr" - chmod +x "$w/apr" + printf '#!/usr/bin/env bash\necho "cvd=[${CUDA_VISIBLE_DEVICES-unset}]"\n' > "$w/cvd" + chmod +x "$w/apr" "$w/cvd" out=$(FAKE_LOCK="$w/lock" MODEL_LADDER_ROOT="$PWD" MODEL_LADDER_GPU_LOCK="$w/lock" DOGFOOD_ALLOW_UNPINNED=1 APR="$w/apr" timeout 60 bash "$prod" --lock-probe qa probe 2>&1); rc=$? if [ "$rc" = 0 ] && grep -q 'lock=LOCKED oom=1000' <<< "$out"; then echo "ok lock: an apr call runs holding the lock, at oom_score_adj 1000" else echo "FAIL lock: the probe call did not run holding the lock at oom 1000 (rc=$rc): $out"; bad=1; fi @@ -237,6 +264,10 @@ lock_probe() { kill "$hp" 2> /dev/null; wait "$hp" 2> /dev/null if [ "$rc" = 2 ] && grep -q 'was not free after 1s' <<< "$out" && grep -q "holder: pid $hp" <<< "$out"; then echo "ok lock: a held lock declines (exit 2) in the bounded wait, naming the holder's pid" else echo "FAIL lock: a held lock did not decline in the bounded wait naming its holder (rc=$rc): $out"; bad=1; fi + # the header read (not GPU work, not locked) must run with no GPU visible + out=$(MODEL_LADDER_ROOT="$PWD" DOGFOOD_ALLOW_UNPINNED=1 APR="$w/cvd" timeout 60 bash "$prod" --header-probe tensors probe 2>&1); rc=$? + if [ "$rc" = 0 ] && grep -qx 'cvd=\[\]' <<< "$out"; then echo "ok header read: runs with CUDA_VISIBLE_DEVICES set and empty (no GPU visible)" + else echo "FAIL header read: the apr_header call saw a GPU (rc=$rc): $out"; bad=1; fi return "$bad" } @@ -274,6 +305,10 @@ if [ "$SELF_TEST" = 1 ]; then mutant q4k-required-false red-q4k-required-false 's/if is_q4k(r) and r.get("required") is not True:/if False:/' mutant q4k-without-cuda red-q4k-rung-cpu-only 's/if is_q4k(r) and "cuda" not in (r.get("backends") or \[\]):/if False:/' mutant inventory-missing red-inventory-model-missing 's/if x is None or not x.get("present"): # held by the host, absent from the run/if False:/' + mutant filename-glob red-inventory-by-filename-glob 's/^if inv_spec.get("patterns"):/if False:/' + mutant header-excluded red-q4k-header-excluded 's/ for f in sorted(members - inv_files):/ for f in []:/' + mutant header-included red-non-q4k-in-inventory 's/ for f in sorted(inv_files - members):/ for f in []:/' + mutant tie-not-member red-tie-excluded 's/if top > 0 and counts.get(want_dtype, 0) == top:/if top > 0 and counts.get(want_dtype, 0) == top and list(counts.values()).count(top) == 1:/' # The lock: the real producer passes both halves; each producer mutant must fail at least one. prod=scripts/model_ladder.sh if lock_audit "$prod" > "$mdir/audit.out"; then echo "ok lock: $prod makes no GPU apr call outside apr_locked" @@ -290,6 +325,7 @@ if [ "$SELF_TEST" = 1 ]; then pmutant no-lock 's/^apr_locked() { flock -E "\$LOCK_BUSY" -w "\$LOCK_WAIT" "\$GPU_LOCK" choom/apr_locked() { choom/' pmutant no-choom 's/ choom -n 1000 -- "\$APR" "\$@"/ "$APR" "$@"/' pmutant unbounded 's/ -w "\$LOCK_WAIT"//' + pmutant header-sees-gpu 's/^apr_header() { CUDA_VISIBLE_DEVICES= "\$APR"/apr_header() { "$APR"/' # The cells module (scripts/lib/model_ladder_cells.py): each rule deleted in a copy, imported through # MODEL_LADDER_CELLS_LIB, and the case that names the rule must go RED under the copy. cmutant() { # cmutant