feat(ladder): model gate judges cells (verb × thinking × context rung) from the measured inventory (#3712 row B1)

contracts/model-capability-ladder-v1.yaml

@@ -62,6 +62,23 @@ ladder:
     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
     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,
+  # thinking, context rung). The RUNGS are not declared here: ids and token counts live in ONE file,
+  # evidence/release/context-rungs.json (apr-release-context-rungs/v1, #3715), which pv reads too;
+  # consumer-max is the max over its consumers[].max_prompt_tokens. Thinking modes are derived per model
+  # from its chat template (#3723). A cell fits a host iff weights + kv_bytes_per_token * tokens + workspace
+  # <= the host's TOTAL GPU memory (operator "a", #3710): a fitting cell must pass, a non-fitting one must be
+  # an honest pre-load refusal, and every owed cell must pass on >= 1 required host. Long rungs are owed by
+  # the families below plus ONE representative per other arch, named here by file (cop 2026-09-21).
+  cells:
+    verbs: [run, chat, serve, code]
+    long_rungs_for:
+      families: [qwen35]                      # every consumer's family: the full rung set, through declared
+      representatives:                        # one file per other arch the fleet holds
+        qwen2: qwen2.5-coder-7b-instruct-q4_k_m.gguf      # lambda + gx10
+        qwen3: Qwen3-8B-Q4_K_M.gguf                       # lambda + gx10
+        qwen3moe: Qwen3-Coder-30B-A3B-Instruct-Q4_K_M.gguf  # gx10 (128 GB unified); fits no 24 GB card long
   rungs:
     - id: qwen2-1.5b-q4km
       family: qwen2.5
@@ -190,6 +207,11 @@ proof_obligations:
     property: "No Q4_K rung is optional, and every one claims CUDA"
     formal: "∀ rung ∈ ladder.rungs: q4k(rung) ⟹ rung.required = true ∧ cuda ∈ rung.backends"
     applies_to: gate_verdict
+  - id: MCL-INV-008
+    type: invariant
+    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-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"
@@ -273,6 +295,12 @@ falsification_tests:
     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"
 
+  - id: FALSIFY-MCL-016
+    rule: "Cells: verbs x thinking x context rung, derived and proved"
+    prediction: "check_model_ladder.sh --self-test: green-cells passes (20 owed on lambda, 12 pass, 8 honest refusals); a missing cell, a duplicate row, a fallback, a thinking block that never closed, a prompt under its rung, an empty answer, a co-tenant refusal, an OOM instead of a refusal, a rung that passes nowhere, thinking_modes that disagree with the template, a missing context_length (#3733), no cells, a consumer without a number, a missing context-rungs file, a dropped cells block or verb, a rung id or consumer dropped from context-rungs.json vs origin/main, an arch with no held representative, and a pass where the declared arithmetic says the cell cannot fit (the arithmetic decides what is owed, so it must be right) are each RED naming it; 11 module mutants are each killed by their case"
+    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"
+
 qa_gate:
   id: F-MCL-001
   name: Model Capability Ladder

docs/roadmaps/entries/PMAT-3712.yaml

@@ -1,7 +1,7 @@
 - id: PMAT-3712
   github_issue: 3712
   item_type: task
-  title: Model gate universe = each host's measured Q4_K inventory; no Q4_K rung optional; skip/fallback/rc!=0 RED
+  title: Model gate universe = each host's measured Q4_K inventory; the gate refuses an optional Q4_K rung (the contract's last one flips in the 0.69.1 fold, per the done_when 1 amendment); skip/fallback/rc!=0 RED; cells = verb x thinking x context rung
   status: in_progress
   priority: critical
   assigned_to: null
@@ -14,4 +14,4 @@
   estimated_effort: null
   labels:
   - kind:code
-  notes: 'ACCEPTANCE (hand-entered from gh#3712; this row = done_when 1 + 2, the GATE side; cop assignment 2026-09-21: worker B). Issue done_when 1, verbatim: "Universe = measured inventory, not a list. The release gate derives the model set from what''s ON each required host (every `*Q4_K*` GGUF/APR under the declared models dir on lambda AND gx10), unioned with the ladder. A model present on a host but missing from the gate''s run is a FAIL naming it. The ladder has no `required: false` for any Q4_K rung; a guard refuses the key on a Q4_K rung (case row + mutant)." Issue done_when 2, verbatim: "Every (model, host) cell is GREEN on CUDA: capability_match passed (not skipped), golden_output passed (not skipped; #3711), `apr run --gpu` rc 0 with no fallback line. One red cell = NO-GO. There is no known, optional or pre-existing exemption, and no threshold like >= N%." WHAT THIS ROW DOES: (a) contracts/model-capability-ladder-v1.yaml gains `ladder.inventory` {dirs, patterns (case-insensitive *q4_k*/*q4k* .gguf/.apr), backends [cuda]}; (b) scripts/model_ladder.sh measures ladder UNION the host''s inventory (every match, depth 1), judges each inventory model on cuda with the SAME measure() as a rung, and writes receipt schema apr-model-ladder-receipt/v2 carrying `inventory` [{file, sha256, bytes}], `file` per row, and `apr_sha` (full 40-hex, for #3715); (c) scripts/check_model_ladder.sh FAILs: `required` not true on a Q4_K rung; a Q4_K rung that does not claim cuda; a ladder with no inventory; a receipt that is not v2 or has no inventory; an EMPTY inventory; an inventory file with no present row (MISSING from the run, named); an inventory-only model not green on cuda (skip, fallback, rc != 0 are RED); (d) case table grows 18 -> 26 (every case red for exactly its own reason, one FAIL line each except the two-host cases), plus 3 self-mutants each killed by its case (q4k-required-false, q4k-without-cuda, inventory-missing); --case with no such case is now RED, and the root is derived from the script path, not git rev-parse (#3581). WHAT IT DOES NOT DO (cop ruling 2026-09-21): qwen3-8b-q4km stays `required: false` in the contract, and the gate refuses that key at T-2, so the release cannot ship on it. Flipping it here would turn pv lint red on EVERY PR: the armed ladder-green shape reads the committed 0.68.2 lambda receipt (golden_output: Empty output), measured rc 0 -> 1 with only that flip. The flip folds into the 0.69.1 batch with the qwen3-8b fix and a committed green lambda receipt. So done_when 1''s `no required: false` clause is NOT met by this row: Refs, not Closes. Done_when 2''s cells turn green only through the model fixes under EPIC #3710; done_when 3 and 4 are aprender-f0''s (#3708). cells[] per verb x context (the widened bar, #3715 proposal) ships with the cop''s widened-bar delta, not here. WHERE THE GATE RUNS (so its rc=1 on the real contract is the release NO-GO, not a PR red): check_model_ladder.sh is declared ONLY in Cargo.toml [package.metadata.dogfood] gates (line 612, the T-2 pre-publish dogfood) and is listed in scripts/unwired_guards_baseline.txt (line 12): no PR workflow runs it, and guard_tree skips it (unwired-baseline). pv lint is a different tool that never runs this script; it reads the contract and PASSES with qwen3-8b at required: false. Measured on this head: guard_tree --no-cargo 0 failed, pv lint contracts/ PASS, cargo test -p aprender-contracts --lib 0 failed. THE GPU LOCK (cop ruling 2026-09-21, after a gx10 global OOM at 15:56:08Z killed CI containers): every apr call in model_ladder.sh goes through apr_locked = flock -E 75 -w ${MODEL_LADDER_LOCK_WAIT:-1800} /tmp/apr-gpu.lock choom -n 1000 --; a lock still held after the wait is an ENV decline (exit 2) naming the holder pid from /proc/locks, never a hang and never a model verdict. T-1 wraps the script in choom only (a second flock outside would deadlock). check_model_ladder.sh audits it statically in the REAL run (a raw "$APR" <subcommand> call is RED) and behaviourally in --self-test (fake apr via --lock-probe: lock held + oom 1000; a held lock declines naming the pid), with four producer mutants each killed: raw-apr-call, no-lock, no-choom, unbounded. FALSIFY-MCL-015.'
+  notes: 'ISSUE AMENDMENT (#3712 comment by the issue author, quoted verbatim): "done_when 1 amended (issue author, cop aprender-04, 2026-09-21 16:56Z): the guard that refuses `required: false` on a Q4_K rung (case row + mutant) is met by #3721. The contract''s own `qwen3-8b-q4km` rung flips to `required: true` in the 0.69.1 fold, together with aprender-fd''s qwen3-8b fix and a committed green lambda receipt. Flipping it earlier would turn `pv lint contracts/` red on every PR, because the armed ladder-green shape reads the committed 0.68.2 lambda receipt, in which qwen3-8b is red. This changes only the order of the work, not the bar: 0.69.1 does not tag until qwen3-8b is `required: true` and green on both lambda and gx10." ISSUE AMENDMENT 2 (#3712 comment 5764495191 by the issue author, quoted verbatim; lanes judge the cells scope against it): "done_when 5 added (issue author, cop aprender-04, 2026-09-21 17:12Z). Operator, verbatim, 2026-09-21: "lets ensure this release has 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, etc," - [ ] The cells matrix. A cell is (Q4_K model, required host, verb ∈ {run, chat, serve, code}, thinking mode derived from the model''s chat template, context rung). Rungs come from `evidence/release/context-rungs.json` up to the model''s declared `context_length`, which is read from the GGUF. The long rungs are owed by qwen35 (always the full set through the declared length) plus one representative per other arch, named in the ladder contract and echoed in the receipt (issue author''s ruling). - [ ] What each cell must do. Where the cell fits the host''s total GPU memory by the declared arithmetic, it must pass on CUDA. Where it doesn''t fit, it must be an honest pre-load refusal naming the arithmetic, never a CPU fallback (operator "a", #3710). - [ ] Coverage. Every rung must pass on at least one required host. The operator''s sentence is the requirement. The cell definition above is the issue author''s reading of it, so a lane judging scope judges against this comment. This is not unrequested scope." ACCEPTANCE (hand-entered from gh#3712; this row = done_when 1 + 2, the GATE side; cop assignment 2026-09-21: worker B). Issue done_when 1, verbatim: "Universe = measured inventory, not a list. The release gate derives the model set from what''s ON each required host (every `*Q4_K*` GGUF/APR under the declared models dir on lambda AND gx10), unioned with the ladder. A model present on a host but missing from the gate''s run is a FAIL naming it. The ladder has no `required: false` for any Q4_K rung; a guard refuses the key on a Q4_K rung (case row + mutant)." Issue done_when 2, verbatim: "Every (model, host) cell is GREEN on CUDA: capability_match passed (not skipped), golden_output passed (not skipped; #3711), `apr run --gpu` rc 0 with no fallback line. One red cell = NO-GO. There is no known, optional or pre-existing exemption, and no threshold like >= N%." WHAT THIS ROW DOES: (a) contracts/model-capability-ladder-v1.yaml gains `ladder.inventory` {dirs, patterns (case-insensitive *q4_k*/*q4k* .gguf/.apr), backends [cuda]}; (b) scripts/model_ladder.sh measures ladder UNION the host''s inventory (every match, depth 1), judges each inventory model on cuda with the SAME measure() as a rung, and writes receipt schema apr-model-ladder-receipt/v2 carrying `inventory` [{file, sha256, bytes}], `file` per row, and `apr_sha` (full 40-hex, for #3715); (c) scripts/check_model_ladder.sh FAILs: `required` not true on a Q4_K rung; a Q4_K rung that does not claim cuda; a ladder with no inventory; a receipt that is not v2 or has no inventory; an EMPTY inventory; an inventory file with no present row (MISSING from the run, named); an inventory-only model not green on cuda (skip, fallback, rc != 0 are RED); (d) case table grows 18 -> 26 (every case red for exactly its own reason, one FAIL line each except the two-host cases), plus 3 self-mutants each killed by its case (q4k-required-false, q4k-without-cuda, inventory-missing); --case with no such case is now RED, and the root is derived from the script path, not git rev-parse (#3581). WHAT IT DOES NOT DO (cop ruling 2026-09-21): qwen3-8b-q4km stays `required: false` in the contract, and the gate refuses that key at T-2, so the release cannot ship on it. Flipping it here would turn pv lint red on EVERY PR: the armed ladder-green shape reads the committed 0.68.2 lambda receipt (golden_output: Empty output), measured rc 0 -> 1 with only that flip. The flip folds into the 0.69.1 batch with the qwen3-8b fix and a committed green lambda receipt. So done_when 1''s `no required: false` clause is NOT met by this row: Refs, not Closes. Done_when 2''s cells turn green only through the model fixes under EPIC #3710; done_when 3 and 4 are aprender-f0''s (#3708). cells[] per verb x context (the widened bar, #3715 proposal) ships with the cop''s widened-bar delta, not here. WHERE THE GATE RUNS (so its rc=1 on the real contract is the release NO-GO, not a PR red): check_model_ladder.sh is declared ONLY in Cargo.toml [package.metadata.dogfood] gates (line 612, the T-2 pre-publish dogfood) and is listed in scripts/unwired_guards_baseline.txt (line 12): no PR workflow runs it, and guard_tree skips it (unwired-baseline). pv lint is a different tool that never runs this script; it reads the contract and PASSES with qwen3-8b at required: false. Measured on this head: guard_tree --no-cargo 0 failed, pv lint contracts/ PASS, cargo test -p aprender-contracts --lib 0 failed. THE GPU LOCK (cop ruling 2026-09-21, after a gx10 global OOM at 15:56:08Z killed CI containers): every apr call in model_ladder.sh goes through apr_locked = flock -E 75 -w ${MODEL_LADDER_LOCK_WAIT:-1800} /tmp/apr-gpu.lock choom -n 1000 --; a lock still held after the wait is an ENV decline (exit 2) naming the holder pid from /proc/locks, never a hang and never a model verdict. T-1 wraps the script in choom only (a second flock outside would deadlock). check_model_ladder.sh audits it statically in the REAL run (a raw "$APR" <subcommand> call is RED) and behaviourally in --self-test (fake apr via --lock-probe: lock held + oom 1000; a held lock declines naming the pid), with four producer mutants each killed: raw-apr-call, no-lock, no-choom, unbounded. FALSIFY-MCL-015. ROW B1 (the judge side of cells; stacked on row A; operator bar raise 2026-09-21: "lets ensure this release has 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, etc,"). A cell is (model, host, verb, thinking, context rung). contracts/model-capability-ladder-v1.yaml gains `ladder.cells` {verbs [run, chat, serve, code], long_rungs_for {families [qwen35], representatives: one file per other arch}}. The RUNGS are deliberately NOT in the contract: they live in evidence/release/context-rungs.json (apr-release-context-rungs/v1, landing in #3715), one declaration shared with pv; consumer-max = max over consumers[].max_prompt_tokens. The judge (scripts/lib/model_ladder_cells.py, called from check_model_ladder.sh) derives the owed set from the MEASURED inventory: short rungs for every model up to its context_length, long rungs for qwen35 and each arch''s representative; thinking modes from the template evidence (enable_thinking -> both; always-open <think> -> on; else off, #3723), never the producer''s claim; fit := weights + kv_bytes_per_token * tokens + workspace <= gpu_mem_total_bytes (operator ''a'', #3710; an unmeasured term keeps the cell owed in full). A fitting cell must pass (cuda, no fallback, rc 0, prompt_tokens >= rung, answer_chars > 0, think_closed when on); a non-fitting cell must be `refused` with required_bytes > the host TOTAL (a co-tenant refusal is RED); every owed cell must pass on >= 1 required host; every arch in any inventory has a representative some required host holds. A missing context-rungs file, a consumer without a number, a missing context_length (#3733) and a receipt with no cells are each a named FAIL, never an empty owed set. Anti-shrink floors vs origin/main: the cells block (block, verbs, long-rung families and representatives) AND the rung file evidence/release/context-rungs.json (its rung ids and consumers; git show origin/main, absent there = bootstrap), because the rungs live in that file, not in the cells block. A `pass` on a cell the declared arithmetic says cannot fit is RED (MCL-INV-008: not fits => refused): the arithmetic decides what is owed, so a pass beyond it proves the arithmetic wrong (#3596). The module itself keeps only REQUIRED hosts'' receipts. Case table 26 -> 47; 10 module mutants each killed by its case. The PRODUCER side (row B2: measuring the cells) is not in this row: it needs #3723 (thinking toggle), #3733 (inspect keys) and #3596 (capacity::plan, the pre-load refusal). Until it lands, the real T-2 run is RED on ''receipt carries no cells'', which is the operator''s bar, not a PR red: check_model_ladder.sh runs only in the release dogfood (Cargo.toml [package.metadata.dogfood]) and is listed in scripts/unwired_guards_baseline.txt. MEASURED (answers a round-3 lane claim that qwen35-family GGUFs report general.architecture = qwen2): on lambda, Qwen3.5-0.8B-Q4_K_M.gguf and Qwen3.5-4B-Q4_K_M.gguf report general.architecture = qwen35 (apr inspect --json, and a direct GGUF v3 header read whose keys are qwen35.block_count, qwen35.context_length 262144, qwen35.full_attention_interval 4, ...), so `families: [qwen35]` matches them by arch. The fixture''s q.gguf is arch qwen35 and owes 16 cells in green-cells, every long rung included; a mutant deleting the families check (family-long) is killed by red-cells-missing-cell. 11 cells mutants.'