refactor(models,cli,docs): make the model corpus ask what it ships

[zhen8838]

Why

• Nine public roots declare a target and two topology levels, and nothing held them
  to it: every H200 consumer went through build_for(fixture), which overrides both
  fields the source declares. Deleting a level from any root broke no test.
• Every test ran against an editable install, and pip install -e never exercises the
  packaging manifest. The difference between "in the repository" and "shipped" was
  invisible: deepseek_v4_flash/hf_alias.py is in the tree, absent from the wheel, and
  the whole suite was green.
• The model coverage report was produced and consumed only by the tests that fed it.

What

• Removed the coverage reporter end to end: tests/models/report.py,
  coverage_artifact.py, test_coverage_artifact.py, the CI-only
  scripts/summarise_model_coverage.py, the pytest_configure plugin registration, and
  the two model-coverage CI steps.
• Moved test_tiled_mlp.py to tests/dsl/ — it authors and evaluates a DSL @module
  with no corpus, catalog, checkpoint or Hugging Face dependency.
• Added tests/integration/installed/analyzable/: seven smoke_*.py files, one per
  model directory, asking every corpus case through the installed tilefoundry
  commands against the directory tilefoundry models <name> --source names and the
  test copies whole. The machine is never injected — the copied model.py declares its
  own target and levels, and there is no argument to override them by.
• Deleted the six tests/models/test_*_coverage.py consumers those cases came from.
• Fixed a CLI source-loader bug the migration exposed: cli/source.py loaded an
  authored file without registering it in sys.modules, so any file pairing
  from __future__ import annotations with a @dataclass could not be loaded at all.
  The fix carries no test written for it: its dedicated regression test is deleted, and
  the shipped deepseek_v4_flash/model.py covers it instead by being such a file.
• Made ValueLifetime.binding identify one value, by suffixing repeated labels at the
  memory-report boundary.
• Moved the ten Hugging Face numerical comparisons into the same smoke_*.py files, so
  each parity run and each perturbation run is now a tilefoundry check against the
  shipped source with the oracle produced by the test and handed over through
  --expected. Nothing long-lived holds a frozen truth. The ten originals are deleted.
• Pulled the corpus back to answering on the machine each model declares. Deleted
  fixtures.ACCEPTANCE, which had no consumer; tests/core/test_analyze_at_a_size.py
  and the build-isolation assertions now ask build() instead of rebinding H200. Three
  tests whose only subject was the default fixture injection are replaced by one
  per-case test that asserts both halves at once: build() agrees with what the source
  declares, and build_for(apple_m2_pro()) aims the same case at a second machine
  sharing no Function with it. TargetFixture, CorpusError, CapabilityGate and
  build_for are kept — the alternate-target case and the KDA gate still use them.
• Deleted the verification-grading surface end to end: tests/models/verified.json and
  the L1/L2/L3 level, model evidence and oracle_level model with it, out of
  generate_model_catalog.py, the generated catalog.json, tilefoundry models,
  tilefoundry check's JSON field and text warning, docs/spec/cli.md and every test
  that asserted on them. Four models had shipped an L2 claim no test backed since
  4c938ac; nothing replaces it, and no new coverage label takes its place.

Contract

• docs/spec/analysis.md — ValueLifetime.binding is now stated to be unique within
  its function, with a constraint saying why an authored name is not.
• docs/spec/cli.md — breaking. Five MUSTs are removed. Four of them — the
  oracle-level warning, the listing's level and oracle split with its level meanings,
  the reporting of a level below the oracle's, and the promotion rule — give way to one
  constraint saying the catalog states what a model is, not how well verified it is.
  The fifth, "A validation level MUST NOT be generated", is deleted outright with no
  replacement: its rationale said the level comes from a committed record, and that
  record was verified.json. Nothing is stated in its place, deliberately — the
  models/counts behaviour stands on its own, and a future verification design owns
  any further contract. check's JSON no longer carries verification, and models
  no longer prints a level.
• catalog.json still ships and still backs tilefoundry models, now describing only
  each model's name, counts and modules.
• build_for is retained, now for its stated purpose only: asking one model about a
  second machine. It has one caller left in tests/.

Verification

• pytest tests/ -n 4 — 696 passed, test_results/final3-inprocess.xml.
• pytest tests/integration/installed -o python_files='smoke_*.py' -n 4 — 335 passed,
  test_results/final3-installed.xml, against a wheel and venv built fresh from this
  tree rather than a reused one, so the shipped spec and model sources under test are
  the ones this branch produces.
• Both runs are after rebasing onto upstream/main, which had moved four commits in
  total (8e97a45, 9d04b44, 403db1f, a8b5c77) and touched pyproject.toml,
  cli/data.py and tests/integration/installed/conftest.py — files this branch also
  depends on. Neither rebase took a conflict, and the eight model data-files entries,
  the CI workflow without its two removed coverage steps, and the installed-suite
  fixtures all survived intact.
• The in-process count moves 695 to 696 for two reasons that cancel out to +1: this
  branch deletes one test, and a8b5c77 added two cases to an existing parametrized
  list in tests/scripts/test_no_machine_paths_lint.py.
• AC-2-5 checked on that installation rather than on the checkout: catalog.json has
  models only, each entry name/counts/modules; tilefoundry models prints no
  level; no verified.json ships; and the shipped cli.md no longer contains the
  constraint that presumed a level existed.
• AC-2-2 is falsified against retained evidence. Corrupting one constant in the
  installed qwen3_1_7b/model.py — _EPS = config.rms_norm_eps to 1.0 — reddens
  that model's comparison: test_results/m2-ac22-broken.xml fails both
  parametrizations with check reporting allclose(atol=0.00195312 rtol=0) max_violation 0.371094 FAIL on all three outputs, ~190x the tolerance. Restoring the
  constant gives test_results/m2-ac22-restored.xml, 2 passed. No test changed between
  the two runs.
• The perturbation runs were vacuous and now are not, shown by probe. Every
  disagreed() run is held to breaking the same comparison its parity run passes,
  because a tighter bound is met by an unperturbed run too and the test then passes
  without perturbing anything. That is not hypothetical: it was the case here.
  test_results/m2-mla-vacuity-probe.xml shows test_mla_cache_pairing_is_load_bearing
  passing under an identity permutation, and m2-kimi-moe-probe.xml the same for
  the router-bias perturbation replaced by a no-op. With the bound corrected, the same
  two probes fail as they must — m2-mla-vacuity-probe-fixed.xml and (after the fix)
  m2-kimi-moe-probe.xml — while the real perturbations still pass,
  m2-mla-fixed.xml and m2-kimi-moe-fixed.xml. Measured cause: the MLA step's own
  parity bound is 0.00586 and the MoE block's is 0.0234, both above the fixed 1e-3 the
  migrated code was refusing at. qwen3_5's two perturbation runs were probed the same
  way and were never vacuous (m2-qwen35-vacuity-probe.xml fails under a no-op).
• The loader fix is falsifiable, and no longer through a test written for it. Its
  dedicated regression test is deleted; the coverage that replaces it is the shipped
  source itself, because deepseek_v4_flash/model.py is the model that pairs
  from __future__ import annotations with a @dataclass. Measured by reverting the
  fix inside the built installation: 8 of that model's analyzable cases fail,
  test_results/final-loader-probe.xml, and restoring the one line makes them pass
  again. So every command aimed at that source exercises the fix.
• The label de-duplication is falsifiable against retained evidence: the same three
  zero-size cases fail in test_results/m1-analyzable-fixed.xml and pass in
  test_results/m1-analyzable-dedup.xml, with no test edit between the two runs.

Risk / Follow-up

• The label de-duplication is a temporary workaround. Repeated
  ValueLifetime.binding labels are made unambiguous by numeric suffixes at the
  memory-report boundary only; the parser still attaches an assignment's name to every
  nested expression of its right-hand side, which is the actual cause. The later
  scoped value identity / source-anchor redesign is owned by
  docs/plans/todos/16-lifetime-report-value-identity.md. Measured scale of the
  underlying problem: 125 of 367 lifetime entries (34%) across the nine corpus entries
  sit under a colliding authored label.
• The coverage mechanism needs a redesign, and that redesign is required
  follow-up work. This PR removes the old reporter without replacing it. No interim
  design was recreated here deliberately. Until that redesign lands, the following
  guards are no longer enforced across the corpus. Two of them are gone outright; two
  survive only as a narrower check on a single model, named at the item that keeps it:
  • The max-context materialisation guard. Formerly
    test_max_context_coverage.py::test_the_largest_context_is_reasoned_about_and_not_allocated.
    It asserted, via tracemalloc, that analysing at a model's ceiling context does not
    allocate anything near it — i.e. that the analysis reasons about a tensor instead of
    building one. Only the observable half survives (the reported footprint must grow
    with the context). Nothing now catches an analysis that reports the right number by
    materialising what it was asked to reason about.
  • The four corpus-completeness guards, deleted with the six coverage files. Each
    ran over the whole corpus, so what is lost is the global guarantee: no test now
    holds every model to these properties. One model keeps a narrower local version —
    tests/models/deepseek_v4_flash/test_case.py is retained deliberately, and its
    test_the_case_selects_every_function_the_description_defines still asserts, for
    DeepSeek alone, CASE.untested("analyze", module) == () (:30),
    CASE.selected("schedule") == (module.entry_function().name,) (:31) and
    CASE.untested("schedule", module) == ("mla_kv_update",) (:32).
    1. test_the_corpus_selects_every_function_its_models_define — every function a
       model defines is selected by some analyze case. No global guarantee remains: a
       function added to any of the other six models can go unanalysed with nothing
       red. DeepSeek is covered by test_case.py:30.
    2. test_an_analysis_family_is_asked_of_the_target_not_written_down — the family
       list came from ANALYSES.selectors_for(target) rather than a literal. Gone
       outright, with no local equivalent anywhere: nothing now stops the four
       families drifting from what the target registers.
    3. test_the_functions_no_partition_can_take_are_untested_not_blocked — one
       schedule case per execution Module, each selector that Module's declared entry,
       leftovers counted exactly. No global guarantee remains; for DeepSeek the entry
       and leftover properties survive at test_case.py:31-32.
    4. test_every_model_with_an_open_dimension_is_asked_this_question — measured with
       dim_vars_reached: exactly the models reaching a DimVar must state a sized
       case. Gone outright, for every model including DeepSeek: test_case.py:35-51
       checks that the length DeepSeek states is one its model admits, which is a
       different property from having to state one at all.
• Three fixture/RoPE provenance guards are gone (M2 finding 1). Deleted with their
  test_decoder_layer.py files:
  qwen2_5_1_5b, gemma2_2b and minicpm3_4b's
  test_generation_inputs_match_the_drawn_position. Each asserted that the root's
  prepare_inputs_for_generation hands a decode step exactly what the drawn position
  implies: the token at step alone, rotary cos/sin bit-equal to
  reference._rope_at(step + 1), the table sized to that model's own published bound
  (max_position_embeddings for qwen2_5, sliding_window for gemma2), pos_ids == [step], the score scale's shape, and the caller's cache object handed straight back
  (checked by identity against a sentinel).
  Why check cannot exercise it: prepare_inputs_for_generation is neither a @func
  nor an orchestration method — it produces the activations a function is later given.
  It returns a heterogeneous tuple, one member of which is the caller's own object
  passed through, and check targets a function and compares declared tensor outputs
  positionally. There is no selector that names this method and no predicate that
  expresses "this is the object I passed in".
  What is now unguarded: a root may drift in how it draws a decode step — wrong
  position, mis-sized rotary table, a cache quietly rebuilt — and every retained
  comparison still passes, because each is handed activations drawn by the test rather
  than by the root. Not lost for qwen3_5_35b_a3b: step 2.6 retains
  tests/models/qwen3_5_35b_a3b/test_provenance.py::test_generation_inputs_match_the_drawn_position,
  which still asserts this for that root.
• Eight falsification guards were not askable of the shipped source and are gone
  (M2 finding 2). Each is named with what it falsified and why check cannot express
  it. check offers eight predicates — allclose, cosine, equal, max_abs,
  max_rel, nan_inf, rel_l2, ulp — every one of them a positional, whole-output
  comparison of one candidate against a reference the caller supplies.
  Three further guards were first misclassified as unaskable and are retained, not
  lost: kimi/test_moe.py's test_router_bias_is_load_bearing,
  test_routed_scaling_is_applied_after_normalisation and
  test_shared_expert_contributes. Their originals rebuilt the block at a reduced
  expert count, but that was a cost device, not a requirement: every parameter moe
  declares is non-const, so each perturbation is one --input tensor. They are now
  smoke_kimi_linear_48b_a3b.py::test_the_router_and_the_shared_expert_are_load_bearing,
  asked at the published 256 experts.
  1. kimi/test_moe.py::test_moe_matches_hf_at_reduced_expert_count — falsified that
     the reduced-expert fixture the four perturbation tests beside it ran against was
     itself a faithful MoE, so their results could not be artefacts of a shrunken
     model. check builds the model the shipped source declares; num_experts comes
     from the model's own config.json and no flag overrides it. With the
     reduced-count fixture gone this guard also has nothing left to validate.
  2. kimi/test_moe.py::test_router_gathers_unbiased_scores — falsified the one
     routing subtlety no published field states: the router selects on
     sigmoid(logits) + bias but takes the routing weights from the unbiased
     scores. It held the HIR router against a hand-computed correct variant and
     measured the wrong variant 1.08e-01 away, so it asserted both that the HIR
     matched and that the two variants are far enough apart for matching to mean
     something. check cannot: the test compares expert indices as a set and
     weights only after sort(-1), because the HIR's selection order is not HF's
     topk order, and none of the eight predicates is order-insensitive. Its second
     half also compares two hand-computed variants to each other, with no model call
     on either side.
  3. qwen3_5/test_moe.py::test_routing_selects_the_experts_hugging_face_selects —
     falsified the router's choice rather than its arithmetic: an index wrong by one
     is not slightly wrong, it runs a different expert. check cannot: the comparison
     is set(got) == set(want) plus weights gathered through argsort, deliberately
     order-insensitive because nothing downstream depends on the order the eight
     arrive in. No predicate expresses that.
  4. kimi/test_mla.py::test_identity_rotary_is_exactly_the_identity — falsified that
     cos = 1, sin = 0 really is the identity, which is how Kimi's NoPE form is
     expressed without a second kernel. check cannot: both sides are Hugging Face —
     apply_rotary_pos_emb against its own input — so there is no candidate to name.
     The claim now rests on the arithmetic of x * 1 + rotate_half(x) * 0, recorded
     as such at kimi/reference.py::identity_rope_caches and in model.py.
  5. kimi/test_mla.py::test_nope_and_rope_are_different_functions — falsified that
     the NoPE and RoPE parity tests were not both passing vacuously by ignoring the
     rotary: it required mla_step_oracle(nope=True) and mla_step_oracle(nope=False)
     to differ. check cannot: it compares two oracles to each other and never
     calls the model, so again there is no candidate.
  6. qwen3_5/test_full_attention.py::test_only_the_leading_rotary_dims_carry_a_position
     — falsified a kernel that rotated a whole head, or none of it: it ran
     partial_rope at two positions and required entries past rotary_dim to be
     bit-equal between them while entries before it differed. check cannot: this
     compares two candidate runs to each other, and on slices; check compares one
     candidate against a supplied reference, whole output at a time, and hands no run's
     output back for a second run to be compared with.
  7. qwen3_5/test_linear_attention.py::test_the_state_decays_rather_than_accumulating
     — falsified a fixture whose gating sat at one extreme, by requiring exp(g) from
     HF's own A_log through softplus to lie strictly inside (0, 1) and the drawn
     heads to span that interval. check cannot: it never calls the model. It is a
     property of the drawn weights, asserted about Hugging Face.
  8. qwen3_5/test_moe.py::test_the_shared_expert_is_part_of_the_block — falsified a
     fixture assembled from the published configuration alone: shared_expert and
     shared_expert_gate appear in no published field, so such a fixture would omit
     them and every routed number would still be right. It required
     routed + shared == want and, under pytest.raises, routed != want.
     Partially expressible, and recorded as such rather than as impossible. The
     falsifying half — the routed branch alone must not match the whole block — is a
     disagreed() against routed_experts, a function the source declares. Two things
     stopped it being re-expressed here. The composition half needs the outputs of two
     separate check runs added together, and check neither hands an output back nor
     compares a sum of two runs; that is the cross-process composition this migration
     has no mechanism for. And feeding routed_experts its routing weights and indices
     means taking them from HF's gate rather than from the HIR's router, whose selection
     order differs — so whether the guard survives that substitution is unestablished,
     and asserting it without establishing it is what this PR is trying to stop.
• The CLI loader fix has no dedicated regression test.
  test_an_authored_file_may_pair_deferred_annotations_with_a_dataclass is deleted. What
  remains is incidental rather than intentional coverage: it holds only while a shipped
  model happens to pair deferred annotations with a @dataclass, which today exactly
  one does (deepseek_v4_flash). If that file stopped using its @dataclass, the fix
  would become unguarded silently — nothing would fail to announce it. The failure it
  prevents is not subtle when it happens (every command against such a file errors), but
  it would return without a test naming it.
• Two pre-existing dead helpers, observed and left alone. Neither is a loss this PR
  causes; both were orphaned by 4c938ac on main, which deleted their only callers
  and left the helpers behind. Recorded here because they are the same
  scaffolding-outlives-its-test pattern this PR removes elsewhere, and because a reader
  auditing the deletions above will find them and wonder:
  tests/models/minicpm3_4b/reference.py's DecoderStepInputs.residual_scale, whose
  comment still reads "named for what a perturbation test asks" while that test is
  gone; and tests/models/qwen3_5_35b_a3b/reference.py's full_layer_oracle and
  linear_layer_oracle, uncalled since the same commit. Left untouched deliberately —
  they are outside this plan's scope.
• An H200 rebind is indistinguishable from the source declaration, so the per-case
  value assertion cannot detect one being reintroduced. Measured on qwen3_1_7b:
  build_for(h200_sxm()) and build() produce an equal target and identical
  topologies, cta 132 and thread 512, because the fixture reads the same hardware
  documents the model's own CudaTarget("nvidia.h200_sxm") resolves to. Only a foreign
  machine differs — apple_m2_pro does, which is what makes the new test's assertion
  falsifiable at all. So the guarantee that no case is silently aimed by a fixture rests
  on the structural check that no build_for caller outside the alternate-machine
  test exists, not on comparing values: a reintroduced build_for(h200_sxm()) would
  pass every value assertion in the suite. That equivalence is the defect this PR
  exists to remove, and it is recorded here because it bounds what the replacement
  test can promise.
• AC-1-3 holds for two of nine roots. --topology thread succeeds only on
  qwen3_1_7b and qwen2_5_1_5b, so only they can witness a deleted thread level.
  The other seven declare the level but reach ops with no registered type relation, so
  the command fails for an unrelated reason. Measured separately: removing thread from
  a root does not redden its existing cta schedule case, so the plan's assumption
  that the schedule family self-reddens is false.
• AC-1-4 has no live subject. No analyze, schedule or sized case in the corpus is
  gated BLOCKED (0 of 38/11/7), so the blocked-case contract — non-zero exit plus the
  registered gate.reason in stderr — is recorded rather than exercised. No inactive
  helper was added for it.