[TS PBT] Infer property-relevant relational hypotheses from PBT observations #397

Implementation child of #355. Consumes #396 and the user-property context in #395. Coordinate development-corpus selection with #356; do not wait for final benchmark evaluation.

Goal

Derive a bounded, auditable set of behavioral hypotheses whose relevance to user assertions can be tested against coverage-only and observation-independent controls.

Bounded first delivery

For #405, freeze a small template set over supported numeric/scalar values and dense-array lengths, including equality/order, a bounded affine subset, pre/post and simple guarded relations. Use selected assertion-related observation points with a documented bounded dependency analysis and fallback. Required families below are exercised within this declared subset; they do not require full strings, arbitrary heaps, automatic invariant discovery or #400–#403.

Type/null facts are supported only where the core value model can represent them faithfully. Preserve explicit capability diagnostics for other values. #401 owns dedicated cross-execution pairing and #403 owns helper-summary context/refinement. A pilot hypothesis must add information beyond the original domain/precondition and must not merely restate the failure predicate.

Scope

• Use typed expressions over identified observed values, program points, pre/post states and supported guards. Preserve JavaScript binary64, NaN, signed zero, null/undefined, UTF-16 and collection semantics; do not reinterpret number relations as mathematical real arithmetic.
• Required implemented families: scalar/type/null facts; relations among inputs, intermediates and results (equality, order and a bounded set of affine templates); collection-length and pre/post relations; simple context/path-conditioned relations. Pairwise or cross-execution relations integrate with [TS PBT] Guide relational and metamorphic properties across multiple executions #401.
• Select observation points and candidate variables using a bounded dependency analysis tied to the original assertion, with explicit fallback when provenance/slicing is incomplete. Compare property-focused selection against unfocused selection.
• Do not learn every pair of locals indiscriminately. Bound template count, guard complexity, variable pairs and inference time; deterministically rank and deduplicate candidates.
• Filter facts copied from declared generator support/preconditions, duplicates of the queried original property, tautologies, unsupported arithmetic identities and single-value artifacts. A boolean that was filtered to true is not new behavioral knowledge.
• Store candidate ID, formula, context/program point, property relevance rationale, evidence input IDs, support, contradictions, derivation, representability and revision. Sample support/held-out agreement are not proofs.
• Maintain hypotheses across rounds, retaining counterexamples and invalidating only the context they refute. Track random, replay, shrink and solver-origin evidence separately to prevent feedback from manufacturing confidence.
• Use development-only traces for tuning. Export candidate sets for an observation-independent template control and randomized scheduling ablations in [TS PBT] Evaluate causal contributions of property-aware feedback and bounded extensions #357.

Definition of Done

• Several concrete runs yield a nontrivial relational hypothesis not implied by the domain or precondition, and a later concrete witness refutes it.
• Required families have useful and misleading fixtures, including already saturated code coverage, rare contexts and correlated replay evidence.
• Candidate selection, filtering and guard scope are reproducible and interpretable; unsupported formulas remain explicit.
• Per-phase limits and overhead are measured. A constructed fixture establishes functionality only; empirical value is evaluated in [TS PBT] Evaluate causal contributions of property-aware feedback and bounded extensions #357.