[TS PBT] Evaluate causal contributions of property-aware feedback and bounded extensions #357

Part of #345. Final runs depend on #405, #354/#355/#356/#382 and the required bounded #400, #401, #402 and #403 implementations. #403 owns its extension integration separately from the core #355. Protocol/statistical design starts before these implementations finish.

Development pilot versus final evaluation

Provide the pilot protocol to #405 before full implementation: original oracles/support, equal total budgets, seed/repetition plan, analysis unit, cost accounting and controls below. The pilot is executed and completed in #405 on #356's development manifest; it does not wait for #400–#403 or for this issue to close.

The pilot compares the six core configurations plus observation-independent templates, property-focused versus unfocused inference, no-return-loop and output-novelty selection on eligible common subsets. Use planned contrasts rather than a Cartesian product; retain native fast-check as an adaptation-overhead baseline where applicable. Freeze settings before the comparison, report uncertainty descriptively, and preserve negative results. An observed relation causing a fault witness establishes the mechanism; it does not by itself establish superiority over direct original-property search.

Use pilot evidence to diagnose feasibility, costs and plausible research claims, and to set the final protocol on development data. Freeze the final plan before inspecting held-out results. This issue closes only after final held-out core and extension evaluation; early core evaluation is tracked independently in #405.

Research questions

• Does feedback add confirmed faults or reduce time to confirmation beyond direct PBT, direct USVM and a sequential portfolio?
• What do observed relations add beyond exact coverage, output novelty and the same unconditioned relation templates?
• Does focusing observations/relations on the user's assertion help beyond collecting unrelated program facts?
• Does returning/refining inputs across rounds help beyond one PBT-to-USVM handoff?
• What do dependent generator choices, metamorphic relations, bounded stateful commands and context-specific helper summaries add, and where do they regress?

Core configurations

Use identical original properties, admissible input support and total budgets:

1. PBT_ONLY.
2. SYMBOLIC_ONLY with concrete confirmation.
3. SEQUENTIAL without feedback.
4. COVERAGE_FEEDBACK.
5. RELATION_FEEDBACK.
6. COMBINED_FEEDBACK with repeated return to PBT.

Also retain a native fast-check run of each eligible reused suite with the same oracle, generator support and budget, to expose adaptation/bridge overhead. Select any practical same-language coverage-guided comparator during the literature/pilot phase, freeze its configuration before held-out evaluation and document a concrete incompatibility if no fair comparator can be run. Cross-language tools are related work, not automatically comparable benchmark scores.

Use controlled additional ablations, not an uncontrolled Cartesian explosion:

• Same template vocabulary and target budget without selection by observed evidence; control for added symbolic goals.
• Property-focused versus unfocused inference, and fixed/randomized target ordering.
• No return-to-PBT/one-round mode versus repeated rounds.
• Output-behavior novelty selection, reflecting the Go/gopter thesis boundary.
• Each bounded extension enabled/disabled on the same original oracle and eligible subset. A more expressive oracle is not by itself evidence of a better search algorithm.
• Context-specific helper relations versus entry-only relations; any speculative summary substitution is a separately labeled experiment.
• Direct projection/rejection-based generation versus choice-space generation, with differences in bounded support reported.

Protocol and budget

• Freeze project/family split, case/mutant selection, versions, observation templates/points, limits, scheduler, phase/round allocations, seeds, repetitions, machine settings and analysis before held-out runs.
• Tune only on development cases. Use a pilot to set repetitions and report uncertainty; repeat independently seeded campaigns, rotate/interleave execution order and document timeout-limited nondeterminism.
• Include instrumentation, inference, mapping, startup/frontend/adapter work, search, original-runtime replay and reduction in the total budget. State treatment of shared setup, cold/warm runs and memory limits consistently.
• Report timeouts as censored outcomes, not dropped samples. Define aggregation and paired comparisons at project/case level so multiple seeds/mutants do not masquerade as independent projects.
• Report confidence intervals/effect sizes and a predefined treatment of multiple comparisons where applicable; do not rely solely on a best seed, mean coverage or p-value.
• Correctness fixes are applied uniformly to all affected configurations; regenerate affected comparisons. No final-result tuning or favorable benchmark replacement.

Outcomes

Primary: distinct original-oracle-confirmed faulty implementations (real defects and mutants separately), time to first confirmation, marginal faults, and regressions under the same budget. Count each fault once regardless of multiple witnesses/properties.

Secondary: supported denominator, manual adaptation effort, observations/truncation, candidate relation support/contradictions, mapping precision/capability, target attempts/yield, source coverage, output novelty, solver/state work, returned-seed usefulness, fallback, replay acceptance, minimized size, per-phase time and memory. Unsupported metrics are unavailable, not zero.

A hypothesis refutation is not an original-property failure. A false human specification is analyzed separately from an implementation defect. EtsIR reached targets are not concrete source coverage. Statement-only mappings cannot be labeled exact branch guidance.

Definition of Done

• One command runs the frozen plan and another regenerates all summary tables from preserved raw data.
• Held-out results quantify each central mechanism beyond the corresponding controls, including no-gain and harmful-feedback cases.
• Required bounded extensions have actual end-to-end runs on their eligible strata, with full-corpus capability limits alongside supported-only comparisons.
• Artifacts preserve configuration, observations, hypotheses, target decisions, candidates, concrete replay, phase costs, failures and analysis provenance.
• Conclusions state what the data support. Implementation completion does not require a positive result; stronger claims do.
• Hand off validated tables and claim/evidence links to [TS PBT][Research] Establish novelty and deliver the reproducible property-feedback paper #404.