[TS PBT] Collect per-property TypeScript coverage from PBT runs #349

Coverage boundary for downstream integration

Coverage is optional for the baseline in #354. This issue records c8/V8 coverage, but its one-location branch records do not establish binary TypeScript if arms or EtsIR CFG edges. #350 preserves supported statement mapping; #382 owns exact c8/V8 branch reconstruction. Keep unsupported branch mapping explicit and do not infer an unexecuted edge from statement hits.

The existing coverage/diagnostic/provenance contract should be reused without adding another parser or process framework. The historical delivery below remains completed.

Goal

Collect source-level TypeScript coverage separately for every property executed by a compatible concrete PBT backend, starting with fast-check.

Why

The Kotlin-orchestrated hybrid pipeline needs to know which parts of the tested program were reached by concrete PBT before symbolic execution starts.

Coverage is a backend capability, not part of the common property model. The initial fast-check backend runs in Node and can use c8/Istanbul, while future backends should be able to provide the same coverage artifact or report that coverage is unsupported.

Scope

• Define a backend-neutral Kotlin contract for requesting and receiving per-property source coverage.
• Integrate c8/Istanbul with the internal Node runtime used by FastCheckBackend.
• Collect coverage separately for every property execution.
• Preserve coverage for successful and failing property runs.
• Map executed JavaScript coverage back to TypeScript through source maps.
• Record statement, function, and branch coverage.
• Define a per-property coverage artifact containing backend identity and provenance.
• Support configurable inclusion and exclusion of:
  • source-under-test files;
  • predicate and precondition files;
  • generated backend wrappers;
  • dependencies.
• Report missing or invalid source maps and unsupported backend coverage explicitly.
• Keep Node source coverage separate from future EtsIR replay coverage.

Source-to-EtsIR mapping and symbolic target construction are outside this issue.

Definition of Done

• Every covered property run produces its own coverage artifact.
• Coverage requests are initiated and collected by Kotlin orchestration.
• The fast-check backend maps coverage to original TypeScript files and source locations.
• Statement, function, and branch hits are represented.
• Coverage from different properties does not contaminate other results.
• Failed property runs retain the coverage collected before failure.
• Include and exclude rules are configurable and tested.
• Missing source maps and unsupported coverage capabilities produce actionable diagnostics.
• Golden fixtures verify TypeScript statement and branch coverage.
• The backend capability, coverage artifact format, and collection commands are documented.
• The implementation is delivered in a dedicated PR linked to this issue.