[TS PBT][P0] Align and simplify property execution semantics before integration

Start by locating the existing concrete invocation, symbolic projection/search paths, and the shared property API referenced in the issue. Review the work from #351 and #352 before adding the listed cross-backend fixtures, then compare classifications for preconditions, predicates, special values, aliases, and mutation isolation. Done means the shared contract and focused regressions are integrated without duplicating the invocation or property framework.

Part of #345. Priority: P0 / Urgent.

Goal

Make fast-check execution, USVM search and replay implement one explicit property contract before extending #351–#354.

Why

The current concrete adapter passes a thrown precondition to fast-check, while symbolic precondition projection discards unsuccessful completions. The concrete adapter also clones arguments separately for the precondition and predicate. One shared manifest alone does not guarantee equivalent execution.

Shared execution contract

• Inputs follow the existing Kotlin domains and JsConcreteValue encoding. Preserve argument order, special primitive values, and aliases within each supported input graph.
• A supported precondition is a pure boolean function of its inputs. true admits the input; false discards it. An escaping exception or a non-boolean result is a property-definition/execution error, never a discard or a counterexample.
• Purity is an author obligation for the supported subset. Do not build a general purity analyzer, heap snapshot framework, or arbitrary side-effect rollback. Fixtures using global state or mutating preconditions are outside this subset.
• A predicate returns boolean: false is a candidate violation; true holds for that invocation. Any escaping predicate exception, including an assertion exception, is a candidate violation. Expected exceptions must be caught and checked inside the predicate. A non-boolean result is a property-definition error.
• Predicate-local mutation is allowed. Isolate supported input values between samples, explicit examples, replay and shrinking while preserving aliases within one invocation. No persistent external/module state is supported by the initial symbolic contract.
• Async predicates/preconditions remain concrete-only where already supported; symbolic execution reports unsupported rather than silently changing their meaning.
• Timeout, unsupported execution, solver uncertainty and tool errors are not property violations or proof that the property holds.

Scope and implementation boundary

• Document this contract once beside the common property API; link it from execution, projection, search and replay.
• Reuse the existing backend invocation and value codec. Fix concrete/symbolic differences at their actual execution points; do not introduce a second property framework or duplicate process clients.
• Audit the minimal process/coverage helpers touched by these fixes for duplicate validation and hand-written replacements for standard APIs. Keep necessary timeout/cleanup and lossless transport guarantees; unrelated cleanup stays in its owning issue.
• Before adding replay/shrinking orchestration, add small cross-backend fixtures for true/false/throwing/non-boolean preconditions, false/throwing predicates, special numbers, aliases, and mutation isolation. Test observable behavior rather than internal helper structure.
• Define exact/approximate/unsupported projection relative to the declared input domain; document the direction and limitation of every retained approximation.

Definition of Done

• Shared fixtures produce consistent classifications in the existing concrete invocation and symbolic projection/search paths where each supports the property. Replay uses the same existing concrete invocation; completion of #353 orchestration is not a prerequisite for this gate.
• Existing fast-check generation, reproduction and shrinking still use the same invocation contract.
• Existing work for #351/#352 is adjusted and reused; it is not reimplemented in parallel.
• The contract and focused regressions are integrated before #351–#354 are marked complete.
• No claim of general purity checking, arbitrary mutable-object support, or proof from a bounded unsuccessful search is introduced.