Repository navigation
[TS PBT] Capture bounded property-scoped observations in original TypeScript #396
Description
Resolution (2026-10-14)
Audited against usvm main at 19866c959d.
The bounded observation pilot is implemented independently of campaign integration. It records invocation inputs, registered operand points, phases/admission/results, bounded snapshots and explicit unsupported/truncated outcomes; selected source bytes are checked before import. Implementation: usvm #411, usvm #413.
Validation: RealSuiteRegistrationTest passed on current main. DESIGN.md documents explicit observePoint hooks, source verification, limits and unverified transitive/transpiled build scope. This closes bounded capture, not #355/#405 or full automatic instrumentation.
Continuation clarified on 2026-10-14
The accepted bounded observation delivery remains closed. Reuse its input/invocation IDs, phases/admission, explicit points, bounded snapshots and selected-source verification.
The new cooperation requirements do not reopen this capture issue:
- [TS PBT] Integrate exact c8/EtsIR edge feedback into target selection #382 and the early integration slice of [TS PBT] Integrate the core iterative property-observation feedback loop #355 supply supported native edge evidence correlated with admitted original-property execution.
- [TS PBT] Preserve a shared incremental search session across feedback rounds #481 consumes cumulative confirmed evidence deltas; [TS PBT] Project observed relations and assertion goals into exact EtsIR bindings #398 owns exact observation/value/time/context binding and any bounded metadata extension required by that binding.
- Aggregate-only coverage or unknown context cannot be promoted by those consumers to an exact tested edge/context. The current selected-file verification and unverified transitive/transpiled build scope remain distinct capabilities.
- Broader automatic instrumentation or richer nested-call contexts land as explicitly scoped follow-ups in their owning integration/extension issues, not as retroactive blockers of this completed pilot.
Original report and acceptance context, retained for traceability
Implementation child of #355. Builds on #395, #348/#349/#384. Design and basic probes can start before #354, #356 or #382 complete.
Goal
Capture actual program values and their property context from concrete PBT runs, beyond aggregate coverage and a final boolean.
Pilot scope
The first delivery supports #405: numeric/scalar and dense bounded-array values, arguments/returns and selected explicit intermediate points, bounded snapshots and original assertion provenance. Restrict automatic instrumentation to the selected supported syntax/points and record annotation cost; whole-program automatic instrumentation is not a pilot prerequisite. Unsupported values and side effects are diagnosed instead of sampled unsafely. Dedicated cross-execution pairing, command-state contexts and helper-summary inference are accepted in #401/#402/#403, respectively.
Scope
- Extend the existing per-property artifact with run/input identity, provenance, property/assertion ID, generator identity, source/build hash, precondition admission, result/exception, phase (generation, explicit example, symbolic replay, shrinking), and available coverage.
- Observe selected function arguments and returns, pre/post values, assertion operands, and selected intermediate values at stable program points. Begin with function boundaries and explicit observation points; add supported automatic instrumentation using the existing TypeScript toolchain. Report manual annotation cost.
- Pair pre/post snapshots by invocation and distinguish repeated call sites, nested calls and property context. Reuse tagged values and supported alias representation. Arbitrary graphs/getters/proxies are not silently JSON-coerced.
- Instrumentation must evaluate expressions once and preserve this-binding, evaluation order, short-circuiting, throws, supported mutation isolation and async classification. Do not invoke getters or user serialization merely to record a value; mark unsupported observations.
- Bound points, collection elements, trace size and retained examples with deterministic policies. Record truncated/dropped observations and capture overhead; absence is not zero or a null value.
- Retain admitted/rejected/failing provenance without accidentally learning a program invariant only because a precondition or the tested assertion filtered the data.
- Mark correlated shrink/replay samples and solver-generated samples. They may refine hypotheses but cannot inflate the count of independent random evidence.
- Export common artifacts suitable for [TS PBT] Infer property-relevant relational hypotheses from PBT observations #397 and [TS PBT] Project observed relations and assertion goals into exact EtsIR bindings #398; no new process framework.
Definition of Done
- Real fast-check runs capture at least one input-to-result and one intermediate relation relevant to an original user property.
- Instrumented/uninstrumented executions have matching supported outcomes on fixtures covering mutation, special values, exceptions and short-circuiting.
- Isolation across properties, phases and invocations is tested. Stable provenance permits source-to-EtsIR binding and rejects stale builds.
- Bounded retention, unsupported values, instrumentation failure and missing coverage produce explicit outcomes.
- Capture works with no branch mapping and no completed campaign orchestrator; full-run overhead is available to [TS PBT] Evaluate causal contributions of property-aware feedback and bounded extensions #357.
Activity