UnitTestBot / UnitTestBot/usvm

[TS PBT] Evaluate runtime-derived PBT hints for symbolic search

Open
#355 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
Kotlin
Stars
33
Forks
27
Avg merge
4d 3h
Merged PRs (30d)
15

Description

Part of #345. Depends on #354, #356 and the shared contract #384.

Goal

Test whether a small amount of concrete runtime feedback improves symbolic property search enough to justify keeping it.

Scope

  • Start with at most one or two observation kinds motivated by the frozen development corpus, such as numeric ranges or array lengths. Do not implement every conceivable type/shape observation before measuring benefit.
  • Reuse existing per-property run artifacts and a small optional observation payload. A backend without observations is supported by skipping this experiment.
  • Define the selected hint precisely: its measured source, translation and whether it changes ordering or temporarily restricts the input domain. It never becomes a declared property precondition.
  • For temporarily restricted search, run a bounded hinted attempt, then restart from the full declared domain without hints if no confirmed violation is found.
  • Reserve a positive hint-free budget in advance and include observation, startup, hinted search, fallback and replay in the same total budget.
  • A fallback with the remaining budget does not guarantee the same discoveries as a full-budget hint-free run. Report this cost rather than claiming preservation of completeness.
  • Keep the hinted attempt and fallback separately attributable.
  • Compare with #354's sequential HYBRID on the same properties, backend, seeds and total budgets. Include one useful and one misleading observation fixture.

Definition of Done

  • The selected hint mechanism and budget split are frozen before the comparison.
  • A misleading hint fixture demonstrates that fallback removes the hint restrictions and can recover a counterexample; it is not a general discovery guarantee.
  • Results report replay-confirmed findings, time to confirmation, overhead and fallback frequency. State/solver counters are optional when already available.
  • Negative results and unsupported observations remain visible.
  • A short decision retains the tested subset, rejects it, or proposes one bounded follow-up.
  • No general invariant miner, object-shape framework, relation mining or dynamic engine-selection scheduler is introduced.

This experiment is optional for the baseline article. #357 may proceed without it, explicitly recording that runtime hints were not evaluated. It must not block baseline evaluation merely because an optional production feature has not been built.

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Read #354's sequential HYBRID comparison and dependencies #354, #356, and #384 first; this issue names no implementation files or tests. Identify the existing per-property run artifacts and observation payload entry points, then freeze one bounded hint and budget split. Done means comparing the same properties, backend, seeds, and budgets with useful and misleading fixtures, replay-confirmed results, fallback accounting, unsupported and negative outcomes, and a short decision.

Written by the indexing model from the issue text.

Assessment

Tech stack
kotlin
Domain
testing
Issue type
Feature
Difficulty
5/5
Estimated time
Over a week
Activity status
Active
Clarity
Mostly clear
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.