Cost-Reuse: Fix latent classification bugs and code cleanup

[unp1]

Related Issue

Follow-up to #3873 (cost-reuse follow-up fixes), itself a follow-up to #3837. No separate issue.

Intended Change

The cost-reuse locality classifier (CostReuse) decides which taclet costs may be reused
unchanged as the proof grows. For a @StableCost composite feature the annotation means
"transparent": the walk recurses into the feature's children and it stays reusable only if
they are all local too. However, CostReuse.follow descended only into Feature and
TermGenerator children — ProjectionToTerm and TermFeature were silently skipped.

As a result a feature such as ApplyTFFeature, whose cost is
termFeature.compute(proj.toTerm(...)), was classified stable unconditionally, even
though ProjectionToTerm.toTerm(app, pos, goal, mState) receives the goal and can therefore
read volatile proof state. Nine @StableCost features share this shape (ApplyTFFeature,
LetFeature, InstantiatedSVFeature, and the polynomial/monomial family).

This is currently harmless — no ProjectionToTerm in the tree reads volatile goal state
(all only fetch the stable Services; the genuine goal-readers InstantiationCost and
IntroducedSymbolBy are Features, correctly left unmarked → volatile) — but it is a latent
gap: a future goal-reading projection dropped into one of these composites would be silently
mis-classified, letting the strategy reuse a stale cost. As always for costs, that can never
make a proof unsound; it can only perturb (or stall) the heuristic search.

This PR closes the gap:

• CostReuse now treats ProjectionToTerm as a first-class classified node — follow routes
  it and the walk recurses into it exactly like a child feature, so composite projections
  (Subterm, TermConstruction, CoeffGcd, AbstractDividePolynomials, ReduceMonomials)
  are validated too. An unannotated projection is treated as volatile — the safe default.

• The twelve concrete ProjectionToTerm implementations are annotated by what their toTerm
  actually reads:

  • ten @StableCost — the two SV/trigger-instantiation projections, the pinned-\assumes
    projection, the term buffer, and the transparent subterm / term-construction / monomial /
    polynomial projections: each derives its term only from the rule application / match / find
    subterm and the stable Services.
  • two @WeakStableCost — FocusFormulaProjection returns the whole find formula, and
    FocusProjection with stepsUpwards > 0 (e.g. FocusProjection.create(1)) walks up from
    the find subterm. Both read above the subterm, so their cost is reusable only while the
    find formula is unchanged.

  (Annotations are not inherited, so the two concrete subclasses of the abstract divide-projection
  — DividePolynomialsProjection, MonomialColumnOp — are annotated directly; allFields still
  walks their inherited sub-projection fields.)

• TermFeature is deliberately left untraversed and documented as stable by interface: its
  compute(term, mState, services) has no goal, so it cannot read volatile state.

Classification changes only for taclets scored through the two focus projections: they move
from StableCost to WeakStableCost, i.e. their cost is now recomputed when the find formula
changes instead of being reused unconditionally. Because the baseline VERIFY run is clean (those
costs did not in fact vary), the recomputed value equals the previously-reused one, so proof
search — and node counts — are expected to be identical to main; the only effect is a little
extra cost recomputation for those taclets. This must be confirmed by the validation runs below
(it is no longer neutral purely by construction). Everything else keeps its classification.

A possible later refinement: split FocusProjection so the common create(0) (find subterm,
genuinely stable) keeps StableCost and only the upward variant is weak-stable. Left out here to
keep the change minimal and conservative.

Second change: a common CostClassifiable interface (commit d29b748b66)

With the classifier now recursing into projections, its dispatch was still an
o instanceof Feature || o instanceof TermGenerator || o instanceof ProjectionToTerm chain plus
inline annotation reading, with term generators handled specially (annotation only, no recursion).
This commit unifies that:

• A new interface CostClassifiable (in ncore.calculus.costbased) is extended by Feature,
  TermGenerator and ProjectionToTerm — exactly the three components that receive the goal and
  can therefore be volatile. TermFeature stays out (its compute has no goal → stable by
  construction). It carries the reuse-locality as an annotation-driven default locality()
  returning a new CostLocality enum (STABLE / WEAK_STABLE / VOLATILE).
• CostReuse becomes uniform: follow routes any CostClassifiable, and walk recurses into
  every child the same way (kind() collapses to localityOf() over a CostLocality cache). The
  only remaining instanceof is the NonDuplicateApp veto — which is an application guard,
  not a locality, so its being special is honest. The isLocal helper and the term-generator
  branch are gone.
• Bonus soundness: because term generators are now recursed like every other component, a
  ProjectionToTerm held by a generator (SubtermGenerator, MultiplesModEquationsGenerator,
  RootsGenerator) is validated instead of silently skipped — a small gap the first commit left.
  This is an additional behavioural surface the validation runs below must cover.

Plan

• Generalise the walk to classify ProjectionToTerm (recurse into composite projections)
• Annotate the twelve concrete projections by locality (10 @StableCost, 2 @WeakStableCost)
• Unify Feature / TermGenerator / ProjectionToTerm under CostClassifiable; make the
  CostReuse walk uniform (removes the instanceof chain; recurses generators' projections)
• key.core compiles
• -Dkey.strategy.costReuse.verify = 0 mismatches over the RAP corpus (the same gate Follow-up fixes for cost-reuse: remove unsound static caches #3873 used)
• Full (non-VERIFY) RAP run: all proofs close with identical node counts vs main
• spotlessApply pass over the touched files

Type of pull request

• Refactoring (behaviour should not change or only minimally change)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I have tested the feature as follows: the change is exercised by the existing cost-reuse
  verification harness (-Dkey.strategy.costReuse.verify), which recomputes every reused cost
  and warns on any mismatch; this PR must show 0 mismatches over the RAP corpus before merge
  (pending — see Plan). No new unit test is added: the classifier's contract is checked
  corpus-wide by that harness rather than by isolated cases.
• I have checked that runtime performance has not deteriorated: the classification verdict is
  unchanged for every existing feature, so cost reuse is neither gained nor lost on the current
  rule base.

Additional information and contact(s)

Created with AI tooling support.

Spotted during a review of the @StableCost annotations: ApplyTFFeature is marked stable at
the class level although its cost depends on the ProjectionToTerm it wraps. The audit that
followed showed the same pattern in nine composites and confirmed it is dormant today, which is
why this is a robustness/refactoring change rather than a bug fix.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.