[TS Calls] Evaluate fallback policies and models with concrete replay

[CaelmBleidd]

Part of #360.

Goal

Measure how stopping unknown calls, returning opaque values, and applying a small justified set of semantic models affect target discovery, concrete reproducibility and analysis cost.

Prerequisites

Depends on #383, #365, #366, #367 and #368.

Use the simplified #365/#366 implementation and the development corpus/inventory from #367/#368. Admit and validate the small experimental model set before freezing evaluation inputs. If a selected family still needs implementation, create a bounded family issue and make it a prerequisite.

Experiment

• Define three questions: how often unknown calls obstruct analysis; what opaque continuation changes; what validated models add to opaque continuation and stopping.
• Use one USVM/JacoDB revision and one native TypeScript frontend, solver configuration, search policy, input construction and target set for every profile.
• Evaluate the four combinations of an empty/frozen model set and STOP_PATH/FRESH_SYMBOLIC_RETURN. These are experiment configurations, not four engine APIs. Keep mandatory language semantics and correctness fixes identical in all profiles.
• Separate development projects used for model selection from held-out real projects. Freeze revisions, selected methods, target denominator, model IDs/content identity, seeds, phase/total budgets and environment before held-out runs.
• Reuse a concrete runner for the original TypeScript. A target counts as confirmed only when replay reaches that target; observing only a matching return value or exception is insufficient. Reuse existing replay components where suitable without requiring the PBT orchestration, hints or shrinking pipeline.
• Preserve solver-reached targets, extracted inputs, replay-confirmed targets, rejected/unrepresentable candidates, unknown-call decisions, timeouts and tool failures separately.
• Primary measures: unique replay-confirmed targets and their common denominator, confirmation rate, and total runtime. Also report solver-reached targets and unknown-call frequencies by project and distinct call site; solver counters are optional if already available.
• Use repeated seeded runs and a fixed or rotated execution order. Report variability and timeout censoring; equal seeds do not guarantee identical wall-clock-limited exploration.
• Preserve raw per-run results and provide a script producing the tables. Negative results and unsupported cases remain visible.

Definition of Done

• One command reproduces the experiment from the frozen manifest.
• Minimal fixtures demonstrate lost continuation, a spurious opaque witness and a replay-confirmed modeled witness.
• Development and held-out results distinguish the marginal effect of model selection and residual fallback.
• All reported confirmed coverage uses the same target denominator and real TypeScript replay.
• Conclusions answer the three questions even if modeling gives no gain.
• Model validation, corpus selection and threats to validity are documented.
• Deliver the experiment and report in a dedicated PR. Do not import historical result tables as current evidence.

PBT generation, runtime hints, hybrid scheduling, LLM/MCP and a general model-catalog framework are outside this issue. Stopped-frontier snapshots from #373 are optional and require a demonstrated measurement need.