Skip to content

[TS PBT] Guide original property search with admitted edge coverage - #524

Open
CaelmBleidd wants to merge 15 commits into
mainfrom
caelmbleidd/pbt-edge-guidance-399
Open

CaelmBleidd wants to merge 15 commits into
mainfrom
caelmbleidd/pbt-edge-guidance-399

Conversation

@CaelmBleidd

@CaelmBleidd CaelmBleidd commented Oct 15, 2026 •

Copy link
Copy Markdown
Member

BOTH previously ran FastCheck and USVM sequentially without using concrete coverage to choose symbolic work. It now passes exact coverage from admitted predicate invocations into the original-property analysis: changing only the concrete evidence changes which pending path USVM selects. Covered edges leave the coverage goals while remaining traversable; original-property search continues after coverage saturates.

The guided half uses the ordinary CLOSEST_TO_UNCOVERED_RANDOM NURS factory from #526 with the configured machine RNG seed. One aggregate nearest-goal calculation supplies each state's weight. Coverage changes and exhausted replay attempts never refresh the queue: existing weights remain stale until normal add/update. The adapter reads its live edge goals directly, without per-target calculators, target snapshots or selector-specific coverage notifications. Every second turn still uses BfsPathSelector for the original property; failed or exhausted attempts remain concretely uncovered.

The PBT consumer retains exact TypeScript edge distances, admitted source/runtime identity, native replay confirmation and bounded retry attempts. Native coverage excludes preconditions, rejected inputs, import initialization and shrinking trials. Exact single-input replay confirms new edges before they update the running search. Failed or incompatible replay and unknown edges remain explicit in the trace. The shared monotonic deadline includes final witness validation; already-running frontend preparation, solver queries and shutdown may exceed it, and elapsed time records that work.

This is the first coverage-guided slice of #399, with the supported c8/EtsIR integration from #382. It does not complete either issue's broader acceptance, infer relations, change PBT generation or retain a session between runner calls (#481/#355). The admitted collector covers the main Node isolate and only exactly mapped supported if arms. Scientific benchmark campaigns remain paused.

Stack: based on #526 at 9b311ae3c81e4826c3f9f38dca0f5ef5efd474fe; own head 024804408f2873130b810c24c25911a72aeedca8. The exact child range was restacked, with range-diff showing only parent-context changes. The final child commit replaces the superseded standalone coverage selector with lazy NURS.

Current implementation validation on JDK 11:

  • 17 focused UsvmPropertySearcherTest tests passed.
  • At the final restacked head, 23 real-backend Kotlin tests passed: 5 PbtEdgeGuidanceTest, 7 UsvmEdgeFeedbackContractTest and 11 KotlinPropertyDslTest; no failures or skips.
  • These cover varied PBT evidence, covered prefixes, newly discovered nested goals, if without else, saturated coverage with an original-property violation, stale/absent/unsupported evidence, failed replay, cancellation, bounded retry exhaustion, every-second-turn original search and deadline behavior. No assertions were weakened.
  • TS/PBT module Detekt and final FastCheck Detekt passed. git diff --check passed.

Earlier full-suite results are not current-head full-suite validation. GitHub CI is separate from these local checks. The local pre-commit hook's nonexistent checkLicense task was bypassed per commit without changing hook configuration.

Refs #399, #382.

Reuse closest-to-uncovered and weighted selectors with revisioned goals supplied by callers. Refresh pending priorities after coverage changes while retaining queued states and existing reporting semantics.
Restore existing statistics and selector APIs. Keep goal updates and lazy priority refresh inside CoverageGuidedPathSelector, and remove the unsolicited README.
@CaelmBleidd
CaelmBleidd force-pushed the caelmbleidd/pbt-edge-guidance-399 branch from a0e6bcc to be0b569 Compare October 16, 2026 07:52
@CaelmBleidd
CaelmBleidd changed the base branch from main to caelmbleidd/external-coverage-core October 16, 2026 07:52
@CaelmBleidd
CaelmBleidd force-pushed the caelmbleidd/pbt-edge-guidance-399 branch from be0b569 to 852fa26 Compare October 16, 2026 16:32
Use Java 11-compatible stream collection and restore the public npm artifact URL. Select the innermost V8 function before requiring block coverage, and retain separate regressions for supported nonterminal branches and unsupported logical conditions.
Stop before mapping or constructing a symbolic search after preparation exhausts the shared deadline. Keep functional DSL checks on the public default budget, add stage diagnostics, and verify deadline expiration remains inconclusive.
Delegate directed state priorities and external coverage updates to CoverageGuidedPathSelector. Keep TS edge distances, per-step alternation with BFS, native confirmation, and bounded replay attempts in the PBT consumer.
@CaelmBleidd
CaelmBleidd force-pushed the caelmbleidd/pbt-edge-guidance-399 branch from 852fa26 to 0248044 Compare October 16, 2026 16:36
@CaelmBleidd
CaelmBleidd force-pushed the caelmbleidd/external-coverage-core branch from 9b311ae to 42cc2c9 Compare October 16, 2026 16:41
Base automatically changed from caelmbleidd/external-coverage-core to main October 16, 2026 16:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant