[TS PBT] Collect per-property TypeScript coverage

usvm-ts-pbt/DESIGN.md

@@ -7,6 +7,7 @@ API and CLI examples, see [README.md](README.md).
 
 - Kotlin owns property definitions, validation, registries, orchestration, and public results.
 - Node is a thin adapter around fast-check and direct TypeScript loading.
+- Per-property source coverage is an optional backend capability collected by Kotlin through an isolated c8 run.
 - The JSON exchange is one request and one response from the same packaged distribution; it has no persistence or
   compatibility negotiation.
 - Failures are typed without exposing runtime-dependent Node stack traces.
@@ -38,6 +39,7 @@ flowchart LR
 
     FastCheck[fast-check]
     Tsx[tsx]
+    C8[c8 and Istanbul JSON]
     UserTS[User TypeScript source]
 
     CLI --> Registry
@@ -47,6 +49,8 @@ flowchart LR
     Backend --> Model
     Backend --> Process
     Process --> ExecutionCLI
+    Process --> C8
+    C8 --> ExecutionCLI
     Projection --> ProjectionCLI
     ExecutionCLI --> Execute
     Execute --> Domains
@@ -67,7 +71,7 @@ flowchart LR
 | Kotlin model and validation | Define one backend-neutral property and reject invalid structure before execution. |
 | Registry and CLI | Select Kotlin-defined properties and turn user options into a run configuration. |
 | `FastCheckBackend` | Validate examples, resolve source roots, and create the adapter request. |
-| `FastCheckProcessClient` | Supervise Node with coroutines, bounded I/O, hard deadlines, and response validation. |
+| `FastCheckProcessClient` | Supervise Node with coroutines and optionally decode one isolated c8 report. |
 | `execution-cli.ts` | Read one JSON request, protect protocol stdout from user logging, and write one response. |
 | `execute-property.ts` | Build the fast-check property, run it, and translate `RunDetails` into the common result. |
 | `project-domain.ts` | Translate domain descriptors into real `fc.Arbitrary` instances. |
@@ -93,17 +97,22 @@ flowchart LR
     Verify --> Result[PropertyRunResult or PbtBackendException]
 ```
 
-The execution request contains `manifest`, `sourceRoots`, optional `seed` and `replayPath`, `numRuns`,
-`timeoutMillis`, and tagged `examples`. A response is either:
+The private execution request contains `manifest`, `sourceRoots`, optional `seed` and `replayPath`, `numRuns`,
+`timeoutMillis`, and tagged `examples`. `coverageRequest` is Kotlin-only transport metadata and is not serialized
+to Node or added to `PropertyManifest`. A Node response is either:
 
 ```text
 { status: "ok", result: PropertyRunResult }
 { status: "error", diagnostics: [{ kind, code, message, path }] }
 ```
 
-There is intentionally no request ID, operation name, schema version, protocol version, backend ID, or backend
-version. The exchange is private, one-shot, and produced and consumed by the same build. Adding compatibility
-metadata would create branches that no supported workflow uses.
+There is intentionally no request ID, operation name, backend ID, or backend version. The exchange is private,
+one-shot, and produced and consumed by the same build. Adding compatibility metadata would create branches that
+no supported workflow uses.
+
+Coverage uses the same private protocol. When requested, Kotlin starts the execution CLI under c8, then reads a
+separate Istanbul report after a valid response. Backend identity belongs to `coverageCapability` and
+`PropertyCoverageArtifact`, not the ordinary property result or private wire response.
 
 Kotlin validates trusted model objects and examples early so callers get local errors. Node validates the decoded
 JSON again because the process boundary must not trust malformed input. Diagnostic codes have one owner per
@@ -139,6 +148,9 @@ sequenceDiagram
     FC-->>Node: RunDetails
     Node-->>Client: one JSON response
     Client->>Client: validate exit, size, shape, category, and property ID
+    opt coverage requested
+        Client->>Client: decode isolated c8 Istanbul report
+    end
     Client-->>Backend: PropertyRunResult
     Backend-->>Caller: PropertyRunResult
 ```
@@ -167,6 +179,40 @@ Falsification and a timeout cleanly reported by fast-check are completed propert
 entry-point failures, process failures, malformed responses, and the JVM hard timeout are infrastructure
 exceptions.
 
+Coverage collection failures use the separate `COVERAGE` infrastructure category. Stable diagnostics distinguish
+an unsupported backend or Node runtime, unavailable runtime version, missing collector, missing or malformed
+report, and missing or invalid source map. They are never converted into an empty artifact.
+
+## Coverage collection and filtering
+
+For each coverage-enabled property the process client creates unique `raw` and `report` directories and runs:
+
+```text
+node <adapter>/node_modules/c8/bin/c8.js
+  --config=<run>/c8-config.json
+  --reporter=json
+  --reports-dir=<run>/report
+  --temp-directory=<run>/raw
+  --exclude-after-remap
+  --allowExternal
+  --exclude=__usvm_no_default_excludes__
+  node <adapter>/dist/src/execution-cli.js
+```
+
+Kotlin first probes the configured Node executable and rejects versions older than 18.18 before creating the c8
+workspace. The verified version is reused as artifact provenance. The c8 process inherits the caller's current
+directory so user predicates observe the same environment with and without coverage, while an explicit empty
+configuration prevents project-local c8 settings from altering collection. c8 then performs V8-to-Istanbul
+conversion and source-map remapping. Kotlin rejects reports larger than 64 MiB before
+reading them, validates statement, function, and branch maps and counters, classifies remapped files into
+source-under-test, property entry points, generated wrappers, or dependencies, then applies include and exclude
+globs. Excludes take precedence. Files and diagnostics are sorted deterministically before constructing the
+artifact.
+
+A successful or falsified property exits the bridge normally, allowing c8 to flush the report. Process crashes,
+invalid protocol responses, and hard kills do not produce a completed property result. The workspace is removed
+in all cases, and a new workspace is used for every property.
+
 The execution client starts stdout, stderr, and stdin work concurrently on the coroutine I/O dispatcher. Requests
 and stdout are limited to 4 MiB; stderr is limited to 64 KiB. These are transport safety bounds, not property-policy
 limits. The hard deadline is the property timeout plus two seconds for transport, followed by a 250 ms graceful
@@ -175,8 +221,8 @@ shutdown before force-kill. The only run-control maximum is `2^31 - 1` milliseco
 
 ## Runtime packaging
 
-Gradle installs pinned adapter dependencies, compiles only the private adapter, and packages `dist/src` plus its
-runtime dependencies in the application distribution. User TypeScript stays as source. During repository tests,
+Gradle installs pinned adapter dependencies, including c8 10.1.3, compiles only the private adapter, and packages
+`dist/src` plus its runtime dependencies in the application distribution. User TypeScript stays as source. During repository tests,
 Gradle passes the adapter directory through a JVM system property; an installed distribution resolves it next to
 the application libraries. Node.js 18.18 or newer is required, and runtime archives carry an OS/architecture
 classifier because `tsx` depends on a native esbuild package.
@@ -190,11 +236,14 @@ classifier because `tsx` depends on a native esbuild package.
   fast-check: startup failure, non-zero exit, malformed output, explicit diagnostic categories, and hard timeout.
 - Backend integration tests execute real uncompiled TypeScript through the packaged adapter, including replay,
   shrinking, explicit examples, preconditions, async predicates, and timeouts.
+- Coverage golden tests assert literal TypeScript statement and branch outcomes for successful and falsified runs,
+  cross-property isolation, scope and glob filtering, and source-map/report diagnostics.
 
 ## Non-goals
 
 - Persisting requests or results, or supporting old wire formats.
 - Discovering properties by scanning TypeScript source roots.
 - Compiling user TypeScript as part of the PBT workflow.
 - Reimplementing generation, replay, skip accounting, or shrinking in Kotlin.
-- Recording coverage or other per-run artifacts in this change.
+- Mapping Node source locations to EtsIR or constructing symbolic targets from coverage.
+- Combining Node source coverage with future EtsIR replay coverage.

usvm-ts-pbt/README.md

@@ -73,7 +73,7 @@ val result = backend.run(
 
 The defaults are 100 successful runs and a 60-second timeout. Configuration also supports replay paths and
 positional explicit examples. `PropertyRunResult` contains the property ID, status, actual seed, replay path,
-counterexample, run/skip/shrink counts, failure details, and elapsed time.
+counterexample, run/skip/shrink counts, failure details, elapsed time, and optional per-property coverage.
 
 Predicate falsification and a timeout reported by fast-check are normal `FAILURE` results. Invalid input,
 entry-point, process, and transport failures throw `PbtBackendException`.
@@ -82,6 +82,61 @@ Synchronous entry points must return a boolean directly. Asynchronous entry poin
 resolves to a boolean. A false precondition is passed to fast-check as a skipped input. Generation, replay, explicit
 examples, checking, and shrinking retain fast-check semantics.
 
+## Per-property TypeScript coverage
+
+Coverage is a backend capability, not part of `PropertyDefinition` or `PropertyManifest`.
+`PropertyBasedTestingBackend.coverageCapability` exposes the backend identity, backend version, and collector
+before execution. `FastCheckBackend` reports c8 10.1.3. An unsupported backend reports
+`coverage.unsupported` explicitly.
+
+Kotlin requests coverage for one run through `PropertyRunConfiguration`:
+
+```kotlin
+val result = backend.run(
+    property = property,
+    configuration = PropertyRunConfiguration(
+        seed = 42,
+        coverageRequest = PropertyCoverageRequest(
+            scopes = setOf(CoverageScope.SOURCE_UNDER_TEST),
+            includePatterns = listOf("packages/core/**/*.ts"),
+            excludePatterns = listOf("**/*.generated.ts"),
+        ),
+    ),
+)
+```
+
+The default scope is `SOURCE_UNDER_TEST`. Available scopes are:
+
+| Scope | Files retained after source-map remapping |
+| --- | --- |
+| `SOURCE_UNDER_TEST` | Files below a source root except exact predicate and precondition modules |
+| `PROPERTY_ENTRY_POINTS` | Exact predicate and optional precondition modules |
+| `GENERATED_BACKEND_WRAPPERS` | Files in the private adapter runtime outside `node_modules` |
+| `DEPENDENCIES` | Executed files below `node_modules` |
+
+Include and exclude globs operate on original remapped paths, use `/` separators, and support `*`, `?`, and `**`.
+An empty include list retains every file in a selected scope; exclude rules always win.
+
+For every requested property Kotlin creates a unique c8 workspace, runs the private adapter as
+`node c8.js ... node execution-cli.js`, decodes `coverage-final.json`, and removes the workspace. This isolation
+prevents coverage from one property contaminating another. The adapter inherits the caller's current directory,
+while an explicit empty c8 configuration prevents project-local c8 settings from altering collection. A falsified
+property remains a completed Node run, so its artifact preserves coverage collected before falsification.
+
+Before starting c8, Kotlin probes the configured Node executable once. Versions older than 18.18 are rejected with
+`coverage.runtime.unsupported`; an unavailable or unparseable version uses `coverage.runtime.version-unavailable`.
+The verified version is recorded in the artifact provenance without a second probe.
+
+The artifact has kind `NODE_SOURCE` and contains backend/property identity, c8 and Node provenance, canonical
+source roots, the original request, and deterministic per-file statement, function, and branch hits. Lines are
+one-based and columns are zero-based, following Istanbul. Node source coverage remains separate from future EtsIR
+replay coverage.
+
+Missing or malformed reports use `coverage.report.missing` and `coverage.report.invalid`. Reports larger than
+64 MiB are rejected as invalid before they are read. JavaScript below a TypeScript source root that c8 could not
+remap produces `coverage.source-map.missing` or `coverage.source-map.invalid`; a missing packaged c8 runtime
+produces `coverage.collector.not-found`.
+
 ## Registries and CLI
 
 The CLI loads Kotlin property registries through `ServiceLoader`:
@@ -107,20 +162,27 @@ java -cp '/opt/usvm-ts-pbt/lib/*:/workspace/example-properties.jar' \
   --registry example \
   --property array.reverse-twice \
   --seed 42 \
-  --num-runs 1000
+  --num-runs 1000 \
+  --coverage \
+  --coverage-scope source-under-test \
+  --coverage-exclude '**/*.generated.ts'
 ```
 
 Use `--help` for the complete option list. `--source-root` and `--registry` are repeatable. Without `--registry`,
 all providers run in registry-ID order; without `--property`, all selected properties run in registry order.
 Replay paths and explicit examples require exactly one selected property.
 
+`--coverage` enables collection. `--coverage-scope`, `--coverage-include`, and `--coverage-exclude` are repeatable;
+scope and path options require `--coverage`. Without an explicit scope, source-under-test coverage is collected.
+
 The CLI writes a JSON array of results to stdout. Exit code `0` means every property succeeded, `1` means at least
 one property failed, and `2` means a CLI, registry, validation, backend, or transport error. Exit-code-2 diagnostics
 are written as one JSON object to stderr.
 
 ## Verification
 
 Requires JDK 11, Node.js 18.18 or newer, npm, and the repository Gradle wrapper.
+The private distribution pins c8 10.1.3 because it supports the module's Node 18 floor.
 
 ```shell
 npm ci --prefix usvm-ts-pbt/fast-check-adapter --ignore-scripts

usvm-ts-pbt/build.gradle.kts

@@ -1,3 +1,5 @@
+import groovy.json.JsonSlurper
+
 plugins {
     id("usvm.kotlin-conventions")
     kotlin("plugin.serialization") version Versions.kotlin
@@ -14,7 +16,12 @@ dependencies {
 }
 
 val fastCheckAdapterDir = layout.projectDirectory.dir("fast-check-adapter")
+val fastCheckAdapterPackageJson = fastCheckAdapterDir.file("package.json")
+val fastCheckAdapterPackageLock = fastCheckAdapterDir.file("package-lock.json")
 val fastCheckRuntimeProperty = "org.usvm.ts.pbt.fastcheck.runtime"
+val generatedFastCheckRuntimeMetadataDirectory = layout.buildDirectory.dir(
+    "generated/resources/fastCheckRuntimeMetadata",
+)
 val hostOperatingSystem = System.getProperty("os.name").lowercase()
 val hostPlatform = when {
     hostOperatingSystem.contains("mac") -> "darwin"
@@ -31,12 +38,52 @@ val hostArchitecture = when (val architecture = System.getProperty("os.arch").lo
 val fastCheckRuntimeClassifier = "$hostPlatform-$hostArchitecture"
 val npmExecutable = if (hostPlatform == "win32") "npm.cmd" else "npm"
 
+val generateFastCheckRuntimeMetadata = tasks.register("generateFastCheckRuntimeMetadata") {
+    inputs.file(fastCheckAdapterPackageLock)
+    outputs.dir(generatedFastCheckRuntimeMetadataDirectory)
+
+    doLast {
+        val packageLock = JsonSlurper().parse(fastCheckAdapterPackageLock.asFile) as? Map<*, *>
+            ?: error("Invalid fast-check adapter package lock")
+        val packages = packageLock["packages"] as? Map<*, *>
+            ?: error("Missing packages in fast-check adapter package lock")
+        fun dependencyVersion(dependency: String): String {
+            val metadata = packages["node_modules/$dependency"] as? Map<*, *>
+                ?: error("Missing locked fast-check adapter dependency: $dependency")
+
+            return (metadata["version"] as? String)
+                ?.takeIf(String::isNotBlank)
+                ?: error("Missing locked fast-check adapter dependency version: $dependency")
+        }
+
+        val metadataFile = generatedFastCheckRuntimeMetadataDirectory.get()
+            .file("org/usvm/ts/pbt/fastcheck/runtime-dependencies.properties")
+            .asFile
+        metadataFile.parentFile.mkdirs()
+        metadataFile.writeText(
+            """
+            fast-check.version=${dependencyVersion("fast-check")}
+            c8.version=${dependencyVersion("c8")}
+            """.trimIndent() + "\n",
+            Charsets.UTF_8,
+        )
+    }
+}
+
+sourceSets.main {
+    resources.srcDir(generatedFastCheckRuntimeMetadataDirectory)
+}
+
+tasks.processResources {
+    dependsOn(generateFastCheckRuntimeMetadata)
+}
+
 val installFastCheckAdapter = tasks.register<Exec>("installFastCheckAdapter") {
     workingDir(fastCheckAdapterDir)
     commandLine(npmExecutable, "ci", "--ignore-scripts")
     inputs.files(
-        fastCheckAdapterDir.file("package.json"),
-        fastCheckAdapterDir.file("package-lock.json"),
+        fastCheckAdapterPackageJson,
+        fastCheckAdapterPackageLock,
     )
     inputs.property("runtimeClassifier", fastCheckRuntimeClassifier)
     outputs.dir(fastCheckAdapterDir.dir("node_modules"))