Repository navigation
[TS PBT] Focus original property search using observed entry relations - #543
Open
CaelmBleidd wants to merge 1 commit into
Open
CaelmBleidd wants to merge 1 commit into
CaelmBleidd wants to merge 1 commit into
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
PBT numeric relations currently have no consumer in original-property symbolic search. Add adapter-owned
ENTRY_ARGUMENTobservations, captured from the ordered original inputs before the callback runs, and bind their numeric values through the existing EtsIR input slots.searchFocusedOnEntryRelationexplicitly adds the negation of a sampled equality/order relation to the same declared support, original precondition and original property-failure query. The existing unfocused API remains available. The result retains the applied binding and complete inference provenance, so a focused no-finding result cannot be presented as exhaustion of the original domain. Incompatible property/support/source identities, unsupported points, changed snapshots and ambiguous bindings cannot activate the focus.This first slice of #398 is restricted to root numeric entry arguments. It does not infer exact bindings for arbitrary user hooks, return/intermediate values, aliases or nested invocations. Executable-body build status remains
UNVERIFIED; exactness concerns the adapter-owned argument transport only. Each call still creates a search: shared sessions, scheduling the unfocused share and repeated feedback rounds remain with #481/#399/#355. #398 remains open.Stacked on #539 (
caelmbleidd/pbt-scalar-relations) at983f99f5c69f5197fa3c5a30af41d575c75596f9.Validation: 220 PBT Kotlin tests, 100 FastCheck Kotlin tests and 199 native adapter tests passed, along with strict Detekt on every changed Kotlin file and
git diff --check. With the same independent original predicateleft !== 1, two real native observation sets guide USVM to[1, 0]and[1, 2]; both violations are checked in native execution. Tests also cover NaN, original admission, an always-true original oracle, infeasible focused support and rejected bindings. No benchmark campaign was run.