[TS PBT] Search for property violations with USVM

Start with dependencies #351 and #384, then trace the existing target and machine execution APIs and the JsConcreteValue extraction path. Review the focused examples and relevant tests for holding, false, throwing, precondition, and multi-call relational predicates. Done means scoped candidate artifacts and tests distinguish termination and capability outcomes without confirming candidates.

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 #351 inputs and a supported pure precondition following #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. #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 #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.