feat(ladder): a receipt names the binary that ran, never the checkout HEAD; the judge requires the release binary; GPU calls join gpu-q (#3771)

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,9 @@ 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.
+                                             # THE definition: scripts/lib/tensor_universe.py (producer, judge and #3742 share it)
     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 +163,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 = the binary's own git sha (#3771), apr_version = its `--version` verbatim, apr_sha, checkout_sha (not judged), 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/<version>/<host>.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 +218,16 @@ 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-010
+    type: invariant
+    property: "A receipt's identity is the binary that ran, and it is the release binary (prefix-equal git shas); a matching version string, or a checkout HEAD, is not the binary"
+    formal: "∀ host: sha(receipt) = gitsha(apr_version(receipt)) ∧ gitsha(apr_version(receipt)) ≡ gitsha(release_binary)"
+    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"
@@ -291,7 +307,7 @@ falsification_tests:
     if_fails: "absence scored as conformance: a host that listed nothing proved nothing and passed"
   - id: FALSIFY-MCL-015
     rule: "Every GPU apr call runs under the fleet lock, choom'd to 1000, with a bounded wait"
-    prediction: "check_model_ladder.sh --self-test: model_ladder.sh makes no \"$APR\" <subcommand> call outside apr_locked; a fake apr called through --lock-probe sees the lock held and oom_score_adj 1000; a lock held elsewhere declines with exit 2 naming the holder's pid; four producer mutants (raw call, no flock, no choom, no -w) are each killed. The real run is RED when the audit finds a raw call"
+    prediction: "check_model_ladder.sh --self-test: model_ladder.sh makes no \"$APR\" <subcommand> call outside apr_locked; a fake apr called through --lock-probe sees the lock held and oom_score_adj 1000; a lock held elsewhere declines with exit 2 naming the holder's pid; four producer mutants (raw call, no flock, no choom, no -w) are each killed; with the fleet's gpu-q present and bounding its wait (`gpu-q --caps` lists `wait`) the call is ordered at MODEL_LADDER_GPU_PRIO (1) with GPUQ_WAIT = the lock wait, a gpu-q without a bounded wait is never used, and mutants gpuq-unbounded and gpuq-no-caps are each killed. The real run is RED when the audit finds a raw call"
     test: "bash scripts/check_model_ladder.sh --self-test"
     if_fails: "a ladder run on gx10's unified memory OOM-kills the CI pool (15:56:08Z, 18 kills in 10 s) or hangs a release on a stuck lock"
 
@@ -301,6 +317,18 @@ 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"
+
+  - id: FALSIFY-MCL-018
+    rule: "The receipt names the binary that ran, and the judge requires it to be the release binary (#3771)"
+    prediction: "check_model_ladder.sh --self-test: a receipt measured by a different build of the same version, a receipt naming no binary (HEAD only), and a receipt whose sha is not its binary's are each RED; judge mutants binary-mismatch and no-binary-named and producer mutant identity-is-head are each killed; the producer's identity probe records the fake binary's own sha, not the checkout's HEAD"
+    test: "bash scripts/check_model_ladder.sh --self-test"
+    if_fails: "a receipt names a tree that was never measured (a run recorded bfd99757c while executing b89d126fc)"
+
 qa_gate:
   id: F-MCL-001
   name: Model Capability Ladder

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). ONE DEFINITION (asked by aprender-c3 for #3742, whose gate must use this universe, not a second one): the membership rule lives in scripts/lib/tensor_universe.py (histogram of >= 2-D tensor dtypes by count, upper-cased; dominant = every dtype at the max; member iff the dtype is among them, ties included; a file''s name never reaches it). The producer calls its `row` CLI on the header JSON it read through apr_header; the judge imports is_member (its former private copy of the rule is gone); scripts/lib/tensor_universe.sh (sourced, option-neutral) gives shell gates tu_dominant_dtypes <apr-bin> <file> and tu_is_member <apr-bin> <file> <DTYPE> (rc 0 member / 1 not / 2 unreadable), reading the header with CUDA_VISIBLE_DEVICES set empty. The definition''s own case table (7 cases incl. c3''s: a tie is a member, 1-D tensors do not vote, a Q5_0-dominant file is not a member whatever its name) runs from check_model_ladder.sh --self-test, and a mutant of the shared rule (ties excluded) is killed by red-tie-excluded. MEASURED through the shell wrapper on lambda''s real files: Q4_K_M gguf and q4k .apr -> [Q4_K] member; IQ4_XS -> [IQ4_XS] not; the f32 .apr -> [F32] not; a missing file -> rc 2.'

docs/roadmaps/entries/PMAT-3771.yaml

@@ -0,0 +1,17 @@
+- id: PMAT-3771
+  github_issue: 3771
+  item_type: task
+  title: Model-ladder receipts name the binary that ran (its --version sha), never the checkout HEAD; the judge requires the release binary
+  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 (#3771, quoted verbatim): "Found by aprender-fd (PMAT-3724), confirmed in code. `scripts/model_ladder.sh:60` records `sha` = `git rev-parse HEAD`. The binary''s own `--version` goes to a separate `apr_version` field (`:223`), which `check_model_ladder.sh` never reads; it gates on the version STRING alone (`:88`). So two binaries with the same version are indistinguishable. In unpinned mode the receipt''s sha names a tree that may never have been measured: fd''s run recorded bfd99757c while executing binary b89d126fc. This is dogfood §14 row 9 (#3768): a receipt names what it inferred, not what it measured. ## done_when - [ ] The receipt''s identity is the BINARY''s own `--version` output (version + git sha), recorded verbatim. The worktree HEAD, if recorded at all, sits in a separate field that nothing judges. - [ ] `check_model_ladder.sh` (and the release-readiness judge) requires the receipt''s binary sha == the pinned release binary''s sha. A version-string match alone is refused. - [ ] Mutants: a receipt whose binary sha differs from the pin but whose version string matches → RED; a receipt with a HEAD sha and no binary sha → RED. - [ ] Sweep every receipt producer in scripts/ and scripts/release/ for the same inference (HEAD or branch recorded as the identity of what ran), and list each with its fix. Owner: aprender-62 (row A). Refs #3712 #3768 #3724" WHAT THIS ROW DOES: scripts/model_ladder.sh records the receipt identity from the BINARY: `sha` = the git sha parsed from `"$APR" --version` (a binary whose --version names no sha is a decline: what ran cannot be identified), `apr_version` = that output verbatim, `apr_sha` = the full 40-hex of the BINARY''s commit resolved in the repo (null when unknown), `checkout_sha` = the worktree HEAD (recorded, never judged). scripts/check_model_ladder.sh requires, per host: an apr_version carrying a git sha (else ''receipt names no binary''), receipt sha == that sha, and that sha prefix-equal to the RELEASE binary''s sha; the release binary''s sha comes from the PINNED binary (scripts/apr_bin.sh, `"$APR" --version`) or, for case tables only, MODEL_LADDER_RELEASE_SHA -- the verdict line names which. A version-string match alone is refused. Cases: red-binary-sha-differs-same-version, red-receipt-head-only, red-receipt-sha-is-not-its-binary; judge mutants binary-mismatch and no-binary-named and producer mutant identity-is-head each killed; the producer''s --identity-probe with a fake `apr 9.9.9 (feedbee12)` records sha=feedbee12 (checkout differs). scripts/check_release_bump_pr_body.sh: fixture receipts name `apr 9.9.9 (0123abc)` and the prepare_bump run exports MODEL_LADDER_RELEASE_SHA=0123abc (the fixture tree has no apr to pin); the seed copies every scripts/lib/*.py the judge imports. SWEEP (done_when 4), every `git rev-parse ... HEAD` in scripts/ and scripts/release/ classified: DEFECT (fixed here): scripts/model_ladder.sh. PINNED BY CONSTRUCTION (HEAD == what ran): scripts/perf002_prefill_path_probe.sh:96 and scripts/perf041_batched_parity_probe.sh:58 (both source scripts/apr_bin.sh, whose freshness check refuses a binary whose --version lacks HEAD''s sha, APR_BIN override included); scripts/dogfood.sh:165 (RECEIPT_SHA names the tree the evidence describes; its binaries are pinned via apr_bin.sh and it has no unpinned escape). HEAD IS NOT A MEASUREMENT''S IDENTITY: scripts/release/models_t1.sh:49-50, scripts/release/autopilot.sh:65, scripts/release/publish_strict.sh:23, scripts/check_publish_preflight.sh:169 (HEAD compared to the release commit or tag); scripts/perf_gate.sh:1230/1234, scripts/perf_receipt_sign.sh:145 (a signing repo''s own HEAD); scripts/extract_ggml_traits.sh:106 (the source tree read, which is what is measured); scripts/pp066_state.sh:85 (printed state); batch_fold.sh, ci_resolve_dirty.sh, ci_test_tier.sh, predict_merge.sh, session_docs_commit.sh, check_row_pr_write_set.sh, install_pr_review_tools.sh (git plumbing); check_*.sh self-test fixtures and apr_bin.sh''s own freshness check. The apr-dogfood skill''s G13 compares the binary''s sha to HEAD and its DOGFOOD_ALLOW_UNPINNED mode only skips G13 for a binary with no embedded sha, writing no receipt that names HEAD. WHERE THE GATE RUNS: check_model_ladder.sh is declared only in Cargo.toml [package.metadata.dogfood] and listed in scripts/unwired_guards_baseline.txt; no PR workflow runs it. Stacked on #3763 (row A2) at the batch head. SECOND COMMIT (cop rule rev 6, 2026-09-21): model_ladder.sh''s apr_locked joins the fleet''s ORDERED gpu-q queue when gpu-q is present and bounds its wait (`gpu-q --caps` lists `wait`, gpu-q v3): `GPUQ_LOCK=$GPU_LOCK GPUQ_WAIT=$LOCK_WAIT gpu-q --prio ${MODEL_LADDER_GPU_PRIO:-1} -- "$APR" ...`; gpu-q exits 75 naming the holder when the bound expires, the same contract as the bounded flock, which remains the fallback and says it ''may have jumped the gpu-q queue''. The self-test drives both routes with fake gpu-qs (never the fleet queue: the existing probes set MODEL_LADDER_GPU_Q empty); producer mutants gpuq-unbounded (GPUQ_WAIT dropped) and gpuq-no-caps (the capability check dropped, so an unbounded gpu-q would be used) are each killed. The run header prints the GPU access route.'