Repository navigation
[PBT] Infer bounded numeric relations from observations - #539
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.
Part of #397: evaluate numeric equality (
===) and order (<=) candidates from the existing property-observation artifacts. The caller explicitly selects two operands of the same assertion and call site; the result retains the exact observations, source hashes, and build status.Agreement requires at least two distinct admitted fast-check generation inputs and two distinct observed numeric pairs. Replay, shrinking, and solver observations may refute a candidate but cannot add independent support. Empty, incomplete, unsupported, and refuted evidence remain separate outcomes. Comparisons follow JavaScript binary64 behavior, including
NaN, infinities, and signed zero.This is a bounded first slice: one observation per selected point and invocation, no nested invocation matching, automatic operand discovery, affine relations, or symbolic-search integration. The result is an empirical candidate, not a proven invariant. It may repeat the original predicate or domain because this slice does not inspect their formulas. #397 remains open.
Validation: 16 focused inference tests and one real fast-check capture-to-inference test pass; strict PBT Detekt (main/test) and
git diff --checkpass. No experiment campaign was run.