[TS PBT][Checkpoint] Validate the bounded core feedback loop and assess its research value #405

Part of #345. This is the first independently completable research checkpoint. #355 owns core integration; its dependency chain includes #353/#354, #382 and #395–#399. #356 supplies a development manifest, #357 supplies the pilot protocol and #404 supplies nearest-work/claim analysis as early artifacts; none of those three issues needs to close first. #400–#403 are subsequent extensions, not prerequisites.

Objective

Establish whether a bounded, property-aware PBT → observations → symbolic challenge → original-runtime replay → PBT cycle works, and measure whether its empirical promise justifies the next research steps. Separate implementation feasibility from comparative benefit. Full #345 delivery remains broader than this checkpoint.

Fixed core scope

• Reuse original human-written predicates/assertions, declared preconditions and generator support. Start with supported bounded numeric/scalar inputs, tuples and dense bounded arrays; include a directly representable dependent input relationship without requiring generator-choice search.
• Observe selected arguments/returns and explicit intermediate points with stable property, source, invocation and pre/post identity. Use a small documented vocabulary of equality/order, bounded affine, length, pre/post and simple guarded relations tied to the user's assertion.
• Preserve actual JavaScript semantics and classify unsupported bindings/values explicitly. No arbitrary heap/generator execution, command-model framework, dedicated cross-execution inference or helper-summary refinement is required.
• Use deterministic scheduling of original-property, exact mapped branch-coverage and hypothesis targets under one total deadline. Existing ordinary multi-call predicates remain usable wherever supported.
• Replay every candidate in original TypeScript, shrink eligible witnesses while preserving the target, and return useful inputs to a bounded generator-consistent neighborhood policy for a subsequent PBT round.

Functional acceptance

• Real PBT runs produce a nontrivial property-relevant relation not implied by input support/preconditions and not merely a restatement of the original property; that relation changes an actual USVM target.
• A replay-confirmed hypothesis-refutation witness changes subsequent generated inputs and relation evidence. Re-executing an unchanged example list alone is insufficient.
• A curated fault fixture produces an original-property failure via an observation-derived challenge after coverage saturates. Keep it separate from a useful passing hypothesis refutation; do not use a false specification as an implementation defect or hard-code the fault target into inference.
• Independently changed real-runtime branch evidence changes a coverage target through [TS PBT] Map c8/V8 branch coverage to EtsIR CFG edges #382/[TS PBT] Schedule assertion, coverage and hypothesis targets under one budget #399. Statement-only mapping does not satisfy this gate.
• Source/context/time mismatches, misleading hypotheses, unsupported cases, timeouts and budget exhaustion have explicit outcomes. Preserve original-property search and concrete validation budget.
• At least one eligible external witness is reduced and still reproduces its original target. Unsupported shrinking elsewhere remains visible.
• One reproducible command and pinned artifacts expose input lineage, observations, inferred formulas, exact bindings, target choices, replay, returned inputs and all phase costs.

The curated fault demonstrates functionality and causal use of an observation. It does not establish an advantage over direct symbolic search of the same property.

Development comparison

• Freeze a versioned manifest and comparison settings before measuring outcomes. Include at least two independent property families, an imported real fast-check suite, saturated-coverage cases, a misleading/no-benefit case and correct implementations. Report project concentration and adaptation cost. All these cases remain development data.
• Run PBT_ONLY, SYMBOLIC_ONLY for the same original property, SEQUENTIAL, COVERAGE_FEEDBACK, RELATION_FEEDBACK and COMBINED_FEEDBACK with identical declared support and total budgets on explicit common supported subsets.
• Include planned contrasts for observation-independent templates with the same vocabulary/target budget, property-focused versus unfocused inference, no-return-loop, and output-novelty selection. Run native fast-check on eligible suites to expose adaptation overhead. Do not require a Cartesian product of controls.
• Count original-oracle-confirmed implementation faults and time to confirmation; report hypothesis-only refutations and false specifications separately. Separate real defects, validated mutants and curated functional cases.
• Include observation/inference/mapping, startup, search, replay, feedback and shrinking costs. Use predeclared independent seeds/repetitions, report uncertainty and timeouts, preserve regressions/no-gain cases and retain the supported denominator. Never claim benefit from coverage or one selected seed alone.
• Keep final held-out projects/families out of pilot tuning. Version later pilot revisions and retain prior results instead of selecting a favorable comparison retrospectively.

Assessment and completion

Record pinned code/configuration/manifest revisions, reproduction commands, functional evidence, comparison tables, nearest-work implications and the main limiting costs/capabilities. Choose and justify a next action: proceed with the planned extensions; refine a specific core mechanism in a separately recorded development iteration; or reassess the research claim/scope in an explicit roadmap decision.

This checkpoint closes when the bounded functional gates, planned development comparisons and assessment are complete. A negative or inconclusive comparison is a valid completed result; no positive effect size, statistically significant win or general superiority claim is required. Unimplemented core behavior or missing required measurements is not a completed pilot and stays open with explicit blockers.

Closure does not close #345, #356, #357 or #404, waive #400–#403, or authorize submission/publication. The full roadmap retains those required deliverables. Final empirical claims come from the frozen held-out evaluation, not this development pilot.