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.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static final record	WitnessEnumerator.Witness	A concrete counterexample: which value-class it came from, its EK9-source literal, and its value.

Method Summary

Modifier and Type	Method	Description
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.
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.
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.

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

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.