[TS PBT] Focus original property search using observed entry relations

usvm-ts-fast-check/fast-check-adapter/src/execute-property.ts

@@ -761,7 +761,7 @@ function validateObservationRequest(value: unknown, manifest: PropertyManifestWi
     const point = requireRecord(value, adapterDiagnostic.protocolRequestInvalid, 'Point must be an object', path);
     if (typeof point.id !== 'string' || typeof point.assertionId !== 'string'
       || typeof point.operandId !== 'string'
-      || !['argument', 'return', 'intermediate', 'pre', 'post'].includes(point.kind as string)) {
+      || !['entry-argument', 'argument', 'return', 'intermediate', 'pre', 'post'].includes(point.kind as string)) {
       throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid point identity', path);
     }
 
@@ -773,7 +773,7 @@ function validateObservationRequest(value: unknown, manifest: PropertyManifestWi
       callSite: validateSourcePoint(point.callSite, `${path}.callSite`),
       kind: point.kind as ObservationPointRequest['kind'],
     };
-    if (point.kind === 'argument') {
+    if (point.kind === 'argument' || point.kind === 'entry-argument') {
       if (!Number.isInteger(point.inputIndex) || (point.inputIndex as number) < 0
         || (point.inputIndex as number) >= manifest.inputs.length) {
         throw protocolError(adapterDiagnostic.protocolRequestInvalid, 'Invalid argument index', `${path}.inputIndex`);

usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts

@@ -12,7 +12,7 @@ export interface ObservationPointRequest {
   operandId: string;
   source: SourcePoint;
   callSite: SourcePoint;
-  kind: 'argument' | 'return' | 'intermediate' | 'pre' | 'post';
+  kind: 'entry-argument' | 'argument' | 'return' | 'intermediate' | 'pre' | 'post';
   inputIndex?: number;
 }
 
@@ -153,6 +153,12 @@ export class ObservationRecorder {
       return invocation();
     }
 
+    for (const point of this.request.points) {
+      if (point.kind === 'entry-argument') {
+        this.capturePoint(record, point, values[point.inputIndex!]);
+      }
+    }
+
     return contexts.run({ recorder: this, invocation: record }, invocation);
   }
 
@@ -166,7 +172,19 @@ export class ObservationRecorder {
 
   point(record: InvocationRecord, pointId: string, value: unknown): void {
     const point = this.pointsById.get(pointId);
-    if (point === undefined || record.points.length >= this.request.maxPointsPerInvocation) {
+    // Entry snapshots belong to the adapter; user callbacks cannot replace or repeat them.
+    if (point?.kind === 'entry-argument') return;
+    if (point === undefined) {
+      this.artifact.droppedPoints = incrementCounter(this.artifact.droppedPoints);
+
+      return;
+    }
+
+    this.capturePoint(record, point, value);
+  }
+
+  private capturePoint(record: InvocationRecord, point: ObservationPointRequest, value: unknown): void {
+    if (record.points.length >= this.request.maxPointsPerInvocation) {
       this.artifact.droppedPoints = incrementCounter(this.artifact.droppedPoints);
 
       return;

usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts

@@ -175,6 +175,34 @@ test('bounded explicit observation preserves special values and refuses proxies,
   assert.equal(recorder.result.invocations.length, 1);
 });
 
+test('entry arguments are adapter snapshots before user code and cannot be replaced through the hook', () => {
+  const source = { module: 'property.ts', line: 1, column: 1 };
+  const recorder = new ObservationRecorder('property', {
+    points: ['left', 'right'].map((id, inputIndex) => ({
+      id, assertionId: 'original', operandId: id, source, callSite: source,
+      kind: 'entry-argument', inputIndex,
+    })),
+    sources: [{ module: 'property.ts', sha256: 'a'.repeat(64) }],
+    maxInvocations: 1, maxPointsPerInvocation: 2, maxArrayElements: 2, maxBytes: 65_536,
+  });
+  installObservationHook();
+  const hook = (globalThis as Record<symbol, unknown>)[Symbol.for('org.usvm.ts.pbt.observe')] as
+    (pointId: string, value: unknown) => unknown;
+  const inputs = [Number.NaN, -0];
+
+  recorder.run(inputs, 'generation', () => {
+    inputs[0] = 7;
+    hook('left', 42);
+    hook('right', Number.POSITIVE_INFINITY);
+  });
+
+  const invocation = recorder.result.invocations[0]!;
+  assert.deepEqual(invocation.points.map((event) => event.value.value), [encodeJsValue(Number.NaN), encodeJsValue(-0)]);
+  assert.deepEqual(invocation.points.map((event) => event.occurrence), [0, 0]);
+  assert.equal(recorder.result.buildStatus, 'unverified');
+  assert.equal(recorder.result.droppedPoints, 0);
+});
+
 test('observation limits report dropped invocations and points without changing returned values', () => {
   const request: ObservationRequest = {
     points: [{

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckBackend.kt

@@ -10,6 +10,7 @@ import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.PropertyDefinition
 import org.usvm.ts.pbt.model.accepts
 import org.usvm.ts.pbt.model.contains
+import org.usvm.ts.pbt.observation.ObservationPointKind
 import org.usvm.ts.pbt.observation.PropertyObservationRequest
 import org.usvm.ts.pbt.validation.requireValid
 import org.usvm.ts.pbt.validation.validatePropertyDefinition
@@ -86,7 +87,9 @@ class FastCheckBackend(
             }
         }
         val allInputIndexesValid = request.points.all { point ->
-            if (point.kind == org.usvm.ts.pbt.observation.ObservationPointKind.ARGUMENT) {
+            val isArgument = point.kind == ObservationPointKind.ARGUMENT ||
+                point.kind == ObservationPointKind.ENTRY_ARGUMENT
+            if (isArgument) {
                 point.inputIndex in property.inputs.indices
             } else {
                 point.inputIndex == null