QE2E-INV-001 asserts 9.0–9.2 B, but the repo's own 9B descriptor sums to 8.209 B
Found while writing the missing QE2E bodies for #3091/#3114. Nothing was widened or hardcoded to make a test pass — the equation is proved, the range instantiation is not.
contracts/qwen35-e2e-verification-v1.yaml:
QE2E-INV-001 invariant "Parameter count matches architecture"
formal: P(Qwen3.5-9B) ∈ [9.0B, 9.2B]
Evaluating that contract's own model_parameter_count formula on the repo's own constants — contracts/model-families/qwen3_5.yaml, size_variants.9b: V=248320, d=4096, L=32, n_h=16, d_k=256, intermediate=12288, untied lm_head — gives
8,208,535,552 = 8.209 B (outside [9.0B, 9.2B] by ~0.8 B)
The same descriptor's tensor_template declares no Gated DeltaNet tensors, so the missing ~0.8 B has no shape in the tree to come from. Two possibilities, and the repo cannot currently tell them apart:
- the range is wrong (copied from a model card rather than derived), or
- the descriptor is incomplete — it is missing the DeltaNet projections (
ssm_*, conv, the gates), which is exactly the ~0.8 B shape.
(2) is the more likely, and it would mean every consumer of size_variants.9b under-counts Qwen3.5-9B.
What is proved meanwhile
The new test qe2e_inv_001_parameter_sum_matches_tensor_inventory proves the equation: the config-derived sum equals the measured tensor inventory, over both layer types and two schedules. Dropping ffn_down from the config side turns it red. The ∈ [9.0B, 9.2B] instantiation is deliberately not asserted, because asserting it today would require widening the range until it passed.
Ask
Decide which side is wrong, with a measurement: sum the tensor shapes of a real Qwen3.5-9B GGUF and compare against both the descriptor and the range. Then fix the one that disagrees, and let QE2E-INV-001 assert the range.
Refs #3091, #3114
QE2E-INV-001asserts 9.0–9.2 B, but the repo's own 9B descriptor sums to 8.209 BFound while writing the missing QE2E bodies for #3091/#3114. Nothing was widened or hardcoded to make a test pass — the equation is proved, the range instantiation is not.
contracts/qwen35-e2e-verification-v1.yaml:Evaluating that contract's own
model_parameter_countformula on the repo's own constants —contracts/model-families/qwen3_5.yaml,size_variants.9b: V=248320, d=4096, L=32, n_h=16, d_k=256, intermediate=12288, untied lm_head — givesThe same descriptor's
tensor_templatedeclares no Gated DeltaNet tensors, so the missing ~0.8 B has no shape in the tree to come from. Two possibilities, and the repo cannot currently tell them apart:ssm_*, conv, the gates), which is exactly the ~0.8 B shape.(2) is the more likely, and it would mean every consumer of
size_variants.9bunder-counts Qwen3.5-9B.What is proved meanwhile
The new test
qe2e_inv_001_parameter_sum_matches_tensor_inventoryproves the equation: the config-derived sum equals the measured tensor inventory, over both layer types and two schedules. Droppingffn_downfrom the config side turns it red. The∈ [9.0B, 9.2B]instantiation is deliberately not asserted, because asserting it today would require widening the range until it passed.Ask
Decide which side is wrong, with a measurement: sum the tensor shapes of a real Qwen3.5-9B GGUF and compare against both the descriptor and the range. Then fix the one that disagrees, and let QE2E-INV-001 assert the range.
Refs #3091, #3114