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
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
Scope and implementation boundary
Definition of Done