fix(format): ModelConstraints dropped the gated-DeltaNet shape, so 18 of every 24 Qwen3.5 layers were counted as if their tensors did not exist - #3350
Open
noahgift wants to merge 4 commits into
Conversation
`pv proof-status` / `pv coverage` report `bindings=N/6` for qwen35-e2e-verification-v1 by counting entries in contracts/binding.yaml that map an EQUATION to an implementation function, over equations.len(). It was 0/6, so QE2E-BND-005 (`coverage(qwen35_contracts) = 1.0`) was false. Three falsification tests landed earlier and did not move it, because tests are not what it counts. Five equations now compute their formula from the architecture config as data (ModelSizeConfig + ModelConstraints, parsed from contracts/model-families/), in aprender::format::model_arithmetic beside model_family.rs which owns those types. No constant for any model is baked in; all integer arithmetic saturates so the functions stay total under property tests; no unwrap(). model_parameter_count P = V*d + L*(d_attn+d_ffn+d_norm) + d_final + V*d flops_per_token F = 2*P + the O(S*d*L) attention term memory_breakdown M = M_weights + M_kv + M_activations throughput_model tok/s = min(bw/bytes_per_token, compute/F) contract_composition compose(embedding, L x block, final_norm, unembed) 23 tests: a hand-computed worked example per equation plus six properties the contract states (P additive in layers, F linear in P, throughput monotone in bandwidth for QE2E-MON-004, Q4K<Q5K<Q6K<F16<F32 at whole super-blocks for QE2E-ORD-003, M_kv linear in S, composition chains and ends at [seq_len, V]). verification_ladder is deliberately NOT bound. It measures the contract corpus, not the model, and implementing it means deciding what makes an obligation "verified" — the decision #3347 reports as broken today (the --table L2 column ticks on `idx < falsification_tests.len()`). It would also be self-referential: its output is what QE2E-BND-005 asserts equals 1.0. Left unbound at 5/6 rather than marked `pending`, which count_binding_coverage excludes from the denominator and would have shown a clean 5/5. QE2E-BND-005 is therefore still FALSE and still a failing obligation. Nothing here asserts 1.0. Mutation results, measured not assumed. Each of the five bodies was mutated (dropped d_final; 2*P -> 3*P; KV factor 2 -> 1; min -> max; unembed emitting [S,d] not [S,V]) and the unit tests went RED every time, 1-3 failures each, green again on revert. The NAME-based checkers are a different story: renaming all five definitions left `pv proof-status --verify-bindings .` at 5/6 and `pv verify-bindings` at 58/60 — unchanged — because crates/aprender-contracts-staging/generated/*_scaffold.rs declares `fn` of all five names and the scan is a textual whole-tree sweep. That directory has no Cargo.toml and is in no workspace. With the scan root narrowed to crates/aprender-core the same rename drops the contract to 0/6, so the check works and its default root is what blunts it. Pmat-Ticket: PMAT-3347 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…annot reproduce QE2E-INV-001 could not be judged because nothing in the tree held a MEASURED Qwen3.5 tensor inventory to judge against. This adds one: the 320 tensors of ~/models/Qwen3.5-0.8B-Q4_K_M.gguf (sha256 bd258782...dc517), read straight from the GGUF header rather than from a model card. It already falsifies the current arithmetic. Dense/GQA accounting applied to that file gives 644,400,128 against a measured 752,393,024 — short by 107,992,896, 14.4% of the model, because 18 of the 24 layers are Gated DeltaNet and no term here counts their conv, gate, state or output projections. Two shapes in the file are also not what dense accounting predicts, and both are pinned: attn_q is [1024, 4096] = 2 * num_heads * head_dim (the q projection emits the attention output gate alongside the query; attn_output [2048, 1024] confirms num_heads * head_dim = 2048), and attn_q_norm/attn_k_norm are present at head_dim. The file is also TIED — it has no output.weight. Refs #3346 Pmat-Ticket: PMAT-3346 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… a hybrid model can be counted contracts/model-families/qwen3_5.yaml declares inner_size, state_size, conv_kernel, group_count and full_attention_interval under constraints:, and ModelConstraints carried none of them. A Gated DeltaNet layer's parameters live entirely in those dimensions, so every consumer of the descriptor counted Qwen3.5 as if three quarters of its layers did not exist. Carried through as ModelConstraints::deltanet: Option<DeltaNetShape> — the runtime YAML loader (parsing.rs) and the compiled-in registry (build_parsing.rs + build_codegen.rs) both populate it, and FALSIFY-MF-QWEN35-010 pins that the declared values survive the trip and that no other family acquires a shape it never declared. qwen3_5.yaml is the only descriptor with these keys, so every other family keeps byte-identical accounting. model_arithmetic gains gated_deltanet_layer_params (one term per GGUF tensor: attn_qkv, attn_gate, ssm_conv1d, ssm_alpha/beta, ssm_a, ssm_dt.bias, ssm_norm, ssm_out) and hybrid_layers (the interleaved schedule). attention_layer_params gained two terms the real file has and dense accounting did not model: the gated q projection (2*n_h*d_k) and the q/k norm vectors. Falsified against a real model, not against itself: fed the 0.8B configuration, the equation now reproduces the 320-tensor inventory of Qwen3.5-0.8B-Q4_K_M.gguf EXACTLY — 752,393,024, both layer kinds matching tensor for tensor. QE2E-INV-001 is still NOT asserted, and no range was widened to make it pass. The 9b descriptor now yields 8,344,907,136, up from 8,208,519,168 but still 0.655B below [9.0B, 9.2B]. The remaining gap looks like descriptor drift rather than missing arithmetic: 9b keeps inner_size 2048 — the value the 0.8B uses at hidden_dim 1024 — while quadrupling hidden_dim, and its group_count 8 fails 8 * 128 == 2048, a consistency the measured 0.8B satisfies at 16 * 128. Only a real Qwen3.5-9B file can settle it; none is on this box. Refs #3346, #3347 Pmat-Ticket: PMAT-3346 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…osed The note said the obligation was undischarged because ModelConstraints does not carry the DeltaNet shape keys. It does now, and the 0.8B count reproduces the real GGUF exactly. What actually blocks the obligation is descriptor drift at the 9b variant. Pmat-Ticket: PMAT-3346 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
noahgift
enabled auto-merge
September 16, 2026 07:48
|
§13.11 rung 1 — quorum shadow verdict Shadow mode: this records a verdict and merges nothing. A refusal |
github-merge-queue
Bot
removed this pull request from the merge queue due to a conflict with the base branch
Sep 16, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
#3346 asked which was wrong, the range or the descriptor. The answer is neither — it was the type that reads the descriptor. Stacked on #3348.
contracts/model-families/qwen3_5.yamldeclaresinner_size,state_size,conv_kernel,group_countandfull_attention_interval.ModelConstraintscarried none of them, so every consumer counted a hybrid model with dense/GQA accounting and silently missed the conv, the gates, the state norm and the mixer projections of 18 of every 24 layers.Ground truth first, and it now matches exactly
The measurement is against a real file, not against the formula's own assumptions:
~/models/Qwen3.5-0.8B-Q4_K_M.gguf(sha256bd258782…dc517), GGUF header parsed directly — 320 tensors, 752,393,024 parameters.Two shapes in that file contradict dense accounting and are now modelled, both read off the tensors rather than assumed:
attn_qis[1024, 4096]= 2·n_h·d_k — the q projection emits the output gate, andattn_output [2048,1024]proves only q is doubled.output.weight.The mutation: drop the
attn_gateterm andqwen35_0_8b_config_derived_count_equals_the_measured_gguf_inventorygoes RED, short by exactlyd·inner_size= 2,097,152.QE2E-INV-001 is still NOT asserted, and the range was not widened
P(9B) moves 8,208,519,168 → 8,344,907,136, still 0.655 B below [9.0B, 9.2B]. The residual is not arithmetic — the 9b descriptor contradicts itself: it keeps
inner_size: 2048(the value the 0.8B uses athidden_dim1024) while quadruplinghidden_dim, and itsgroup_count: 8failsgroup_count · state_size == inner_size(8·128 ≠ 2048), a consistency the measured 0.8B satisfies at 16·128.Only a real Qwen3.5-9B file settles that, and none is on this box, so the obligation stays unproved and the number is pinned by a test instead of asserted.
DeltaNetShape::heads_span_the_mixer()now catches the descriptor's self-inconsistency directly.Two disclosures
deltanet: None,fixture literals inapr-clitests/oracles. Zero logic change. The enum-payload alternative breaks the same crate, becauseapr-climatchesAttentionType::HybridGatedDeltaNetin two files.qk_normis left alone deliberately. The descriptor says the family has none, the real file hasattn_q_norm/attn_k_normon its attention layers, andtensor_expectation.rsasserts the opposite. Both are true of different layer kinds — the repo should settle whetherqk_normis per-family or per-layer-kind. It is worth 4,096 parameters at 9B, so it does not touch the verdict.The roadmap write
pmat work addproduced was reverted: #3297 moved entries to fragments, and a monolithic write is exactly the contention that PR removed.Gate:
aprender-core --lib model_arithmetic28 passed,aprender-contracts --lib1526 passed, clippy-D warningsclean, fmt clean.Refs #3346, #3347, #3091, #3114
no-close: #3346 stays open — which side of the 9b descriptor is wrong is undecided until a real Qwen3.5-9B GGUF is measured.
ont-delta: shape ModelConstraints gains inner_size, state_size, conv_kernel, group_count and full_attention_interval, and model_parameter_count gains the gated-DeltaNet layer term; no obligation is added or removed, and QE2E-INV-001 is not discharged.
🤖 Generated with Claude Code