[TS PBT] Replay and shrink USVM counterexamples through PBT backends
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 35/100
- Issue type
- Feature
- Clarity
- Mostly clear
- Activity status
- Active
- Tech stack
- kotlin, typescript
Research direction
Start with the candidate inputs from #352, JsConcreteValue, and the shared invocation contract from #384; trace them through the existing backend execution and reproduction path. Add focused tests using the existing adapters and codecs for replay classifications, explicit examples, and shrinking. Done means real TypeScript-runtime fixtures preserve values and aliases, minimized witnesses still violate the property, and unsupported or timed-out shrinking is reported without publishing unconfirmed counterexamples.
Written by the indexing model from the issue text.
Description
Part of #345. Depends on #352 and #384.
Goal
Confirm USVM candidate counterexamples in the original TypeScript runtime and reuse the concrete backend's shrinking.
Scope
- Consume the candidate inputs already extracted by #352 through JsConcreteValue. Do not add another symbolic-value decoder or Kotlin-to-Node process protocol.
- Reuse the existing backend execution/reproduction path and the shared invocation contract from #384.
- Check membership in the declared input domain, run the precondition, and then the original predicate.
- Classify each replay as confirmed violation, property holds, domain/precondition rejection, unrepresentable input, unsupported replay, or replay error. A thrown precondition is an error; a thrown predicate follows #384.
- Preserve undefined, null, NaN, infinities, negative zero and supported tuple/array structure without coercion.
- For fast-check, feed a confirmed witness through its existing explicit-example/reproduction support and verify that shrinking actually runs for supported domains. An example being executed is not proof it was minimized.
- Recheck a minimized result against the same domain, precondition and predicate. If shrinking is unsupported, fails, or exhausts its budget, retain the original confirmed witness and record the limitation.
- Store the original candidate, replay classification, minimized witness when available, actual backend version and existing reproduction data.
Definition of Done
- Confirmed, spurious, rejected, throwing, unrepresentable and shrinkable fixtures pass through the real TypeScript runtime.
- A minimized witness remains inside the declared domain and still violates the same property.
- Aliases and mutation isolation follow #384 during explicit examples, replay and shrinking.
- A backend without shrinking can still confirm and report a counterexample.
- Replay/shrinking share the run deadline and never turn timeout/tool failure into a property failure.
- No unconfirmed symbolic result is published as a final property counterexample.
- Implementation and focused tests reuse the existing adapter and codecs.
A new concrete EtsIR interpreter, general backend capability framework, or custom shrinker is not required.
- Dominant language
- Kotlin
- Stars
- 33
- Forks
- 27
- Avg merge
- 4d 3h
- Merged PRs (30d)
- 15
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from UnitTestBot/usvm
-
Difficulty 5/5 Over a week Newbie friendliness 45/100
UnitTestBot/usvm#388 ·
-
Difficulty 5/5 Over a week Newbie friendliness 25/100
UnitTestBot/usvm#384 ·
-
Difficulty 5/5 Over a week Newbie friendliness 35/100
UnitTestBot/usvm#382 ·
-
Difficulty 4/5 3-5 days Newbie friendliness 48/100
UnitTestBot/usvm#379 ·
-
Difficulty 5/5 Over a week Newbie friendliness 25/100
UnitTestBot/usvm#373 ·
All issues in UnitTestBot/usvm
Similar issues
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
bitcoindevkit/bdk-ffi#1125 ·
-
Issue: Bug
Difficulty 1/5 Under an hour Newbie friendliness 91/100
OpenAPITools/openapi-generator#24978 ·
-
helsemelding-json-schema json-schema-core
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
-
contributor: external needs review
Difficulty 2/5 1-3 hours Newbie friendliness 82/100