[TS PBT] Search for property violations with USVM

[CaelmBleidd]

Delivery boundary in the full #345 roadmap

Preserve the original-predicate violation search in PR #387 as this issue's scope. #398 adds assertion/intermediate/hypothesis targets, #399 selects them, and #355 integrates feedback. #401 and #402 own richer relational/sequence support; this issue does not acquire all their acceptance gates. Searching an original user property remains a mandatory baseline in every feedback comparison.

Part of #345. Depends on #351 and #384.

Goal

Use USVM to search for inputs violating the original TypeScript predicate under the shared declared domain and precondition.

Scope

• Execute the mapped predicate with [TS PBT] Project property domains and preconditions into USVM #351 inputs and a supported pure precondition following [TS PBT][P0] Align and simplify property execution semantics before integration #384.
• A false predicate result or any escaping predicate exception, including an assertion failure, is a candidate violation. Expected exceptions are caught inside the predicate. A non-boolean result is a property-definition error.
• Support a relational predicate making multiple ordinary calls within one invocation. This does not require a general stateful-testing framework or persistent state between samples.
• Use the existing target and machine execution APIs.
• Extract supported candidate inputs once using JsConcreteValue, preserving ordered inputs and the supported alias/value semantics. [TS PBT] Confirm, classify and shrink symbolic property and hypothesis witnesses #353 consumes this representation rather than implementing a second extraction layer.
• Keep reached-target information independent from extraction failure and run termination. A reached state with unrepresentable inputs remains visible but is not a confirmed counterexample.
• Distinguish no violation found within this search, timeout, unsupported execution, property-definition error, engine failure and input-resolution failure.
• Async or otherwise unsupported predicates remain concrete-only where a backend can run them.

Definition of Done

• Focused examples cover a holding predicate, false predicate, throwing predicate, precondition rejection/error and a multi-call relational property.
• Candidate artifacts retain property ID, inputs when available, reached target, termination status and capability limitations.
• No unsupported/opaque execution or timeout is reported as a proved property.
• Every candidate remains unconfirmed until [TS PBT] Confirm, classify and shrink symbolic property and hypothesis witnesses #353 replays it in the original runtime.
• No duplicate capability model, exception framework, value codec or generic target framework is introduced.
• Deliver the existing scoped implementation with relevant tests.

Concrete replay, shrinking and search hints are outside this issue.