[TS PBT] Preserve runtime limitation reasons in property-search results #555

Part of the two-phase PBT -> USVM plan in #345, agreed on 2026-10-16.

Problem

The fixed-input PGOrbit investigation observed an ARRAY_INDEX_GROWTH event from TsInterpreterObserver, while the analysis result contained EXHAUSTED, no terminal states, no unsupported paths and unsupportedCall=false. The PBT search result therefore loses the reason that execution was incomplete.

The existing onRuntimeFeatureLimitation event already carries the statement, stable reason and detail. Calls consumers retain this signal; the PBT consumer should reuse it.

Required change

• Retain bounded, deduplicated runtime-limitation diagnostics in the existing PBT result/artifact path.
• Preserve the original source statement and reason, including array bounds and other supported model limitations.
• Distinguish exhausted supported search from paths excluded by a model limitation. Keep reached candidates, timeout, solver UNKNOWN and ordinary property outcomes independently visible.
• Use existing observer/result mechanisms. No generic telemetry system or new search session is required.

Acceptance

• A property whose only symbolic path exceeds the supported array capacity reports its actual stable runtime limitation reason rather than an unexplained no-finding result. Historical ARRAY_INDEX_GROWTH evidence remains preserved below.
• A property with both supported and excluded paths retains supported results and reports the limitation.
• The result survives normal DSL/campaign serialization, with the original program and oracle unchanged.

This issue reports the limitation; implementing sparse growth remains #388. Public end-to-end regressions and their current supported/excluded fixture boundary are recorded in the delivery status below.

Delivery status (2026-10-17)

The PBT observer/result delivery preserves bounded, deduplicated runtime limitation reasons in #560; #608 adds stopped/fresh unknown-call residual reasons, callee and source through the existing observer contract. Successfully applied models are not limitations. Ordinary and auxiliary public campaign round trips retain diagnostics. #608 passed 33 focused tests, strict Detekt and common-assembly checks; it remains an open PR.

The original sparse-growth event above is historical. #573 separately supplies bounded sparse growth under #388, so index 9 is no longer an excluded-path fixture in the current assembly. Index 1001 still truthfully reports usvm.runtime.array-length-capacity. This reporting does not add Float64Array, arbitrary computed initialization or private/helper closures.

The completed class pilot also preserves a different incompleteness boundary: some symbolic results have NO_VIOLATION_REACHED with no runtime limitation while original native verification leaves inputs unchecked; other runner processes are externally killed or fail artifact handling. These are not evidence of language unsupport or complete no-finding coverage. #354 and #357 retain their exact deadline/publication/native-check dispositions separately; no new speculative model limitation was invented from empty stdout.