Class WitnessEnumerator

java.lang.Object
org.ek9lang.compiler.symbolic.WitnessEnumerator
public final class WitnessEnumerator extends Object
The bounded-model witness materialiser for the Symbolic/Contract scanner (M3): given an obligation expressed as a predicate over a candidate input, enumerate the representative value-classes of a type and return the first input that violates it — a concrete counterexample.

This is the ∃-polarity payoff: the census (M1) says an obligation is undischarged; this turns "undischarged" into a specific witnessing input a developer can paste into a test. It rests on the small-model premise (proven by spike S3, cost interactive) — if a contract can be violated at all it can almost always be violated by one of a type's few representative edge values, so enumerating the value-class vocabulary rather than a full domain is both sound-enough and fast.

Two sources of representatives:

  • Built-in leaf types — the real InputVarietyModel literal pool via BuiltinTypeClassModels.classIdsFor(String) (Example 1: count != 0 → ZERO="0").
  • User constrained types over [lo,hi] — the MIN/NEAR_MIN/NEAR_MAX/MAX edges of the constraint window (Example 3: base + 20 <= 100 over [0,100] → NEAR_MAX=99, since 99 + 20 > 100).

Proven by spike S3b (see EK9_SYMBOLIC_SCANNER_SPIKE_REFERENCE.md §5.3). Net-new for production, tracked: seed InputVarietyModel.literalFor(String, String) for the other ~16 built-ins (mechanical); read the [lo,hi] window from a user constrained type's constraint AST instead of being handed it.

  • Method Details

    • firstViolatingBuiltin

      public static Optional<WitnessEnumerator.Witness> firstViolatingBuiltin(String typeName, LongPredicate obligation)
      Built-in leaf: enumerate the real InputVarietyModel pool and return the first value for which obligation does NOT hold (i.e. the first violator).
      Parameters:
      typeName - the built-in simple type name (e.g. "Integer")
      obligation - the safe condition that should hold for every input; the witness is where it fails
      Returns:
      the first violating witness, or empty if every representative satisfies the obligation

    • firstViolatingConstrained

      public static Optional<WitnessEnumerator.Witness> firstViolatingConstrained(long lo, long hi, LongPredicate obligation)
      User constrained type over [lo,hi]: enumerate the constraint-window edges and return the first violator.
      Parameters:
      lo - the inclusive lower bound of the constraint window
      hi - the inclusive upper bound of the constraint window
      obligation - the safe condition that should hold; the witness is where it fails
      Returns:
      the first violating edge witness, or empty if every edge satisfies the obligation

    • constraintEdges

      public static List<WitnessEnumerator.Witness> constraintEdges(long lo, long hi)
      The MIN/NEAR_MIN/NEAR_MAX/MAX edge witnesses of a [lo,hi] window, de-duplicated by value and clamped to the window.

      🔑 The clamp is load-bearing, not tidying. On a narrow window the neighbours fall OUTSIDE it — constrain as == 5 folds to [5,5], whose lo + 1 and hi - 1 are 6 and 4, neither of which the type can hold. Unclamped, the verifier could report x=6 as a counterexample for a value the type makes unrepresentable (a fabricated counterexample — precisely the "prove configurations impossible" soundness question), and the fuzz generator would emit an argument the constraint rejects. The same clamp absorbs the Long-extreme wrap: a window at [Long.MAX_VALUE, Long.MAX_VALUE] has a lo + 1 that overflows negative, and it is simply dropped for being out of window.

      Parameters:
      lo - the inclusive lower bound
      hi - the inclusive upper bound
      Returns:
      the in-window edge witnesses, most significant first; empty when lo > hi

    • constraintEdgesWithNominal

      public static List<WitnessEnumerator.Witness> constraintEdgesWithNominal(long lo, long hi)
      The window's edges PLUS a nominal interior value — the boundary-value-analysis set for a range: both bounds, just inside each bound, and one ordinary value that is not near either end.

      🔑 Generation policy, not verification. The plain constraintEdges(long, long) set is what a bounded-model VERIFIER wants (a violation of a monotone obligation shows up at an extreme, and the engine asks CriticalValues directly for anything interior it cares about). A generated TEST suite wants the nominal case too: driving Rating over [1000,2000] at 1000/1001/ 1999/2000 alone exercises only the boundary handling and never the ordinary path through the code. Hence a separate entry point rather than widening the edge set both consumers share.

      The midpoint is (lo & hi) + ((lo ^ hi) >> 1), the branch-free floor of the average, and it is used because the obvious spellings both break at the extremes: (lo + hi) / 2 overflows on a window in the upper half of the range, and lo + (hi - lo) / 2 overflows in hi - lo on a window spanning most of it — measured, that one silently collapsed the full Long window's midpoint back onto lo. The nominal is dropped when it merely repeats a corner (a window narrower than five values is already fully covered by its edges).

      Parameters:
      lo - the inclusive lower bound
      hi - the inclusive upper bound
      Returns:
      the edge witnesses followed by the nominal one, when it adds anything