From 6eced81fa3f882b6dace98181c483357b3d51b91 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 27 Jul 2026 10:30:47 +0000 Subject: [PATCH 1/2] fix(justdummies): name the excluding constraint in conflict messages MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Eager conflict detection promises a message that names both sides of an impossible Arrange (ADR-0035). That held for bound-vs-bound conflicts but broke whenever an exclusion (NonZero/Except/DifferentFrom) was the real cause: the four interval engines tracked bounds with provenance (_minConstraint, _maxConstraint, _stepConstraint, _allowedConstraint) but kept exclusions as a bare list of values, so DescribeExhaustion had no label to name and fell back to a bound — producing messages that were self-referential ("Zero() already pins the value to 0") or provably false ("GreaterThanOrEqualTo(5) already pins the value to 5", which allows 5..MaxValue). Give exclusions the same provenance bounds already carry: each engine now stores exclusions as (constraint label, ordinals) pairs and derives its flat draw-time set from them. DescribeExhaustion attributes the emptiness to the exclusion constraints that actually bit — those forbidding a value the interval, lattice and allow-list would otherwise permit — naming the n-ary participants without over-attributing a pin to a single bound. The feasibility and sampling engines are unchanged; only the diagnostic layer gains the information it was missing. Two correctness details fall out of an exhaustive audit of the message against every legal combination: * The allow-list claim is qualified. An allowed value can be dropped by a bound or the lattice rather than by an exclusion, so "forbids every value OneOf(...) allows" would overstate the exclusion's reach. When the allow-list was narrowed by another constraint the message says "every value OneOf(...) allows that the other constraints leave", which stays true; the bare form is used only when no allowed value was dropped. * The message no longer echoes the applied constraint. When the applied constraint is itself the sole cause, the clause refers back to it as "it" ("Cannot apply Except(1) because it forbids ...") instead of repeating the constraint on both sides of "because". The fix spans all four engines that share the exhaustion path: ordinal (integers, TimeSpan, DateTime, DateOnly, TimeOnly), wide (Int128/UInt128), decimal, and continuous (double/float/Half). Bound-vs-bound messages are untouched, the public API baseline is unchanged, and the build stays at 0 warnings. Refs: #312 --- .../ConflictMessageProvenanceTests.cs | 150 ++++++++++++++++++ JustDummies/ContinuousIntervalSpec.cs | 94 +++++++++-- JustDummies/DecimalIntervalSpec.cs | 102 +++++++++--- JustDummies/OrdinalIntervalSpec.cs | 107 ++++++++++--- JustDummies/WideIntervalSpec.cs | 107 ++++++++++--- 5 files changed, 482 insertions(+), 78 deletions(-) create mode 100644 JustDummies.UnitTests/ConflictMessageProvenanceTests.cs diff --git a/JustDummies.UnitTests/ConflictMessageProvenanceTests.cs b/JustDummies.UnitTests/ConflictMessageProvenanceTests.cs new file mode 100644 index 00000000..828aad9f --- /dev/null +++ b/JustDummies.UnitTests/ConflictMessageProvenanceTests.cs @@ -0,0 +1,150 @@ +#region Usings declarations + +using JetBrains.Annotations; + +using NFluent; + +#endregion + +namespace JustDummies.UnitTests; + +/// +/// A conflict message must name the constraint that actually caused the conflict. When an exclusion +/// (NonZero/Except/DifferentFrom) empties the domain, the interval engines used to name a +/// bound instead — or the constraint being applied — producing messages that were self-referential +/// ("Cannot apply Zero() because Zero() already pins the value to 0") or factually false +/// ("GreaterThanOrEqualTo(5) already pins the value to 5", which allows 5..MaxValue). Issue #312. +/// +/// +/// Message content is the example suite's job (ADR-0040): these pin the contract "name the excluding +/// constraint", not the exact prose. Each asserts that the offending exclusion appears in the message — the +/// information that was missing — which is red against the old engines and green once exclusions carry +/// provenance. The four interval engines (ordinal, wide, decimal, continuous) share one exhaustion path, so a +/// case per engine guards them all. +/// +[TestSubject(typeof(ConflictingAnyConstraintException))] +public sealed class ConflictMessageProvenanceTests { + + #region Statics members declarations + + private static string ConflictMessage(Action build) { + try { + build(); + } catch (ConflictingAnyConstraintException exception) { + return exception.Message; + } + + return ""; + } + + #endregion + + // ----- OrdinalIntervalSpec: integers (and, by sharing the engine, TimeSpan/DateTime/DateOnly/TimeOnly) ----- + + [Fact(DisplayName = "A pin emptied by NonZero names NonZero, not the pin itself.")] + public void PinEmptiedByNonZeroNamesTheExclusion() { + string message = ConflictMessage(() => Any.Byte().NonZero().Zero()); + + Check.WithCustomMessage($"The exclusion was not named. Message: {message}").That(message).Contains("NonZero()"); + } + + [Fact(DisplayName = "A single-value bound emptied by NonZero names NonZero.")] + public void BoundEmptiedByNonZeroNamesTheExclusion() { + string message = ConflictMessage(() => Any.Byte().NonZero().LessThan(1)); + + Check.WithCustomMessage($"The exclusion was not named. Message: {message}").That(message).Contains("NonZero()"); + } + + [Fact(DisplayName = "A range pinned by two bounds and emptied by Except names Except, not a bound.")] + public void PinEmptiedByExceptNamesTheExclusionNotABound() { + string message = ConflictMessage(() => Any.Int32().Except(5).GreaterThanOrEqualTo(5).LessThanOrEqualTo(5)); + + Check.WithCustomMessage($"The exclusion was not named. Message: {message}").That(message).Contains("Except(5)"); + } + + [Fact(DisplayName = "A pin emptied by DifferentFrom names DifferentFrom.")] + public void PinEmptiedByDifferentFromNamesTheExclusion() { + string message = ConflictMessage(() => Any.Int32().DifferentFrom(-1).Negative().GreaterThan(-2)); + + Check.WithCustomMessage($"The exclusion was not named. Message: {message}").That(message).Contains("DifferentFrom(-1)"); + } + + [Fact(DisplayName = "A lattice emptied by Except names Except and the lattice, not the lattice alone.")] + public void LatticeEmptiedByExceptNamesBothTheExclusionAndTheLattice() { + string message = ConflictMessage(() => Any.Int32().MultipleOf(5).Except(0).Between(-4, 4)); + + Check.WithCustomMessage($"The exclusion was not named. Message: {message}").That(message).Contains("Except(0)"); + Check.WithCustomMessage($"The lattice was not named. Message: {message}").That(message).Contains("MultipleOf(5)"); + } + + [Fact(DisplayName = "An allow-list emptied by Except names Except, not just the allow-list.")] + public void AllowListEmptiedByExceptNamesTheExclusion() { + string message = ConflictMessage(() => Any.Int32().Except(1, 2).OneOf(1, 2)); + + Check.WithCustomMessage($"The exclusion was not named. Message: {message}").That(message).Contains("Except(1, 2)"); + } + + // ----- DecimalIntervalSpec ----- + + [Fact(DisplayName = "A decimal pin emptied by DifferentFrom names DifferentFrom.")] + public void DecimalPinEmptiedByDifferentFromNamesTheExclusion() { + string message = ConflictMessage(() => Any.Decimal().DifferentFrom(1m).Between(1m, 1m)); + + Check.WithCustomMessage($"The exclusion was not named. Message: {message}").That(message).Contains("DifferentFrom(1)"); + } + + // ----- ContinuousIntervalSpec: double (and, by sharing the engine, Single/Half) ----- + + [Fact(DisplayName = "A double pin emptied by DifferentFrom names DifferentFrom.")] + public void DoublePinEmptiedByDifferentFromNamesTheExclusion() { + string message = ConflictMessage(() => Any.Double().DifferentFrom(1d).Between(1d, 1d)); + + Check.WithCustomMessage($"The exclusion was not named. Message: {message}").That(message).Contains("DifferentFrom(1)"); + } + +#if NET8_0_OR_GREATER + // ----- WideIntervalSpec: Int128/UInt128 (net8.0 leg only) ----- + + [Fact(DisplayName = "An Int128 pin emptied by NonZero names NonZero.")] + public void Int128PinEmptiedByNonZeroNamesTheExclusion() { + string message = ConflictMessage(() => Any.Int128().NonZero().Between(System.Int128.Zero, System.Int128.Zero)); + + Check.WithCustomMessage($"The exclusion was not named. Message: {message}").That(message).Contains("NonZero()"); + } +#endif + + // ----- Correctness of the claim, not only the naming (surfaced by the exhaustive audit). ----- + + [Fact(DisplayName = "An allow-list narrowed by a bound before an exclusion empties it does not claim the exclusion forbids every allowed value.")] + public void AllowListNarrowedByABoundIsNotOverclaimed() { + // OneOf(1, 3) offers two values, but Between(0, 1) already drops 3; Except(1) then removes the only one + // that survived. Saying Except(1) forbids *every* value OneOf allows would be false — it never forbids 3 — + // so the claim must be qualified to the values the other constraints leave. + string message = ConflictMessage(() => Any.Int32().Except(1).Between(0, 1).OneOf(1, 3)); + + Check.WithCustomMessage($"The exclusion was not named. Message: {message}").That(message).Contains("Except(1)"); + Check.WithCustomMessage($"The message overclaims that Except(1) forbids every value OneOf allows. Message: {message}") + .That(message).Contains("that the other constraints leave"); + } + + [Fact(DisplayName = "When the applied exclusion is itself the sole cause, the message reads 'it forbids', not the constraint twice.")] + public void AnExclusionAppliedLastIsNotRepeatedOnBothSides() { + // Zero() pins the byte to 0; NonZero(), applied last, is itself the forbidder. Repeating "NonZero()" on + // both sides of "because" reads as circular, so the clause refers back to the applied constraint as "it". + string message = ConflictMessage(() => Any.Byte().Zero().NonZero()); + + Check.WithCustomMessage($"The applied constraint should be referred to as 'it'. Message: {message}").That(message).Contains("it forbids"); + Check.WithCustomMessage($"The applied constraint is echoed after 'because'. Message: {message}").That(message).Not.Contains("because NonZero()"); + } + + // ----- Regression guard: bound-vs-bound messages must stay correct and unchanged. ----- + + [Fact(DisplayName = "A bound-vs-bound conflict still names the opposing bound (unchanged).")] + public void BoundVersusBoundStillNamesBothSides() { + string message = ConflictMessage(() => Any.Int32().Between(1, 10).GreaterThan(50)); + + Check.That(message).Contains("Between(1, 10)"); + Check.That(message).Contains("GreaterThan(50)"); + } + +} diff --git a/JustDummies/ContinuousIntervalSpec.cs b/JustDummies/ContinuousIntervalSpec.cs index c71c4a09..13a51048 100644 --- a/JustDummies/ContinuousIntervalSpec.cs +++ b/JustDummies/ContinuousIntervalSpec.cs @@ -57,6 +57,7 @@ internal static double NextDown(double value) { private readonly string? _allowedConstraint; private readonly List? _effectiveAllowed; private readonly IReadOnlyList _excluded; + private readonly IReadOnlyList<(string Constraint, double[] Ordinals)> _exclusions; private readonly Func _nextUp; private readonly double _max; private readonly string? _maxConstraint; @@ -72,7 +73,7 @@ private ContinuousIntervalSpec(string typeName, Func render, Fu double min, string? minConstraint, double max, string? maxConstraint, IReadOnlyList? allowed, string? allowedConstraint, - IReadOnlyList excluded) { + IReadOnlyList<(string Constraint, double[] Ordinals)> exclusions) { _typeName = typeName; _render = render; _quantize = quantize; @@ -83,8 +84,10 @@ private ContinuousIntervalSpec(string typeName, Func render, Fu _maxConstraint = maxConstraint; _allowed = allowed; _allowedConstraint = allowedConstraint; - _excluded = excluded; - // Materialized once here — "constrain once, draw many": Generate never refilters the allow-list. + _exclusions = exclusions; + // The flat value set drives every draw-time decision; the provenance in _exclusions is consulted only + // when a conflict message must name the excluding constraint. Materialized once — "constrain once, draw many". + _excluded = exclusions.SelectMany(pair => pair.Ordinals).ToList(); _effectiveAllowed = allowed?.Where(value => value >= min && value <= max && !IsExcluded(value)).ToList(); } @@ -99,7 +102,7 @@ internal ContinuousIntervalSpec WithMinimum(double minimum, string applying) { throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {_maxConstraint} already requires values less than or equal to {_render(_max)}."); } - return Validated(new ContinuousIntervalSpec(_typeName, _render, _quantize, _nextUp, minimum, applying, _max, _maxConstraint, _allowed, _allowedConstraint, _excluded), applying); + return Validated(new ContinuousIntervalSpec(_typeName, _render, _quantize, _nextUp, minimum, applying, _max, _maxConstraint, _allowed, _allowedConstraint, _exclusions), applying); } /// Tightens the upper bound; a looser bound than the current one is a no-op. @@ -113,7 +116,7 @@ internal ContinuousIntervalSpec WithMaximum(double maximum, string applying) { throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {_minConstraint} already requires values greater than or equal to {_render(_min)}."); } - return Validated(new ContinuousIntervalSpec(_typeName, _render, _quantize, _nextUp, _min, _minConstraint, maximum, applying, _allowed, _allowedConstraint, _excluded), applying); + return Validated(new ContinuousIntervalSpec(_typeName, _render, _quantize, _nextUp, _min, _minConstraint, maximum, applying, _allowed, _allowedConstraint, _exclusions), applying); } /// Tightens the lower bound to strictly above — via the type's next representable value. @@ -132,15 +135,16 @@ internal ContinuousIntervalSpec WithAllowed(double[] values, string applying) { double[] distinct = values.Distinct().ToArray(); - return Validated(new ContinuousIntervalSpec(_typeName, _render, _quantize, _nextUp, _min, _minConstraint, _max, _maxConstraint, distinct, applying, _excluded), applying); + return Validated(new ContinuousIntervalSpec(_typeName, _render, _quantize, _nextUp, _min, _minConstraint, _max, _maxConstraint, distinct, applying, _exclusions), applying); } /// Adds values the generator must never produce. internal ContinuousIntervalSpec WithExcluded(double[] values, string applying) { - List excluded = new(_excluded); - excluded.AddRange(values); + // The applied constraint tags its own values, so a later exhaustion message can name the exclusion + // that actually emptied the domain rather than a bound that merely happens to border it. + List<(string Constraint, double[] Ordinals)> exclusions = new(_exclusions) { (applying, values) }; - return Validated(new ContinuousIntervalSpec(_typeName, _render, _quantize, _nextUp, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, excluded), applying); + return Validated(new ContinuousIntervalSpec(_typeName, _render, _quantize, _nextUp, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, exclusions), applying); } /// @@ -240,7 +244,7 @@ private bool IsExcluded(double value) { private ContinuousIntervalSpec Validated(ContinuousIntervalSpec candidate, string applying) { if (candidate.IsSatisfiable()) { return candidate; } - throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {candidate.DescribeExhaustion()}."); + throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {candidate.DescribeExhaustion(applying)}."); } private bool IsSatisfiable() { @@ -250,18 +254,74 @@ private bool IsSatisfiable() { return !IsExcluded(_min); } - private string DescribeExhaustion() { + private string DescribeExhaustion(string applying) { + IReadOnlyList culprits = ExcludingConstraintsInEffect(); + if (_allowed is not null) { - if (_excluded.Count > 0) { - return $"no value {_allowedConstraint} allows remains available"; - } + if (culprits.Count == 0) { return $"none of the values {_allowedConstraint} allows satisfies the constraints already defined"; } + + // Only the allow-list values the bounds still permit can be forbidden by an exclusion; if some allowed + // value was already dropped by a bound, the exclusions do not forbid "every" allowed value, so the claim + // is qualified rather than overstated. + string allowed = _allowed.All(WouldAllowIgnoringExclusions) + ? $"every value {_allowedConstraint} allows" + : $"every value {_allowedConstraint} allows that the other constraints leave"; + + return $"{Forbids(culprits, applying)} {allowed}"; + } + + if (culprits.Count == 0) { + string pinning = _minConstraint ?? _maxConstraint ?? "the declared bounds"; - return $"none of the values {_allowedConstraint} allows satisfies the constraints already defined"; + return $"{pinning} already pins the value to {_render(_min)}, which the exclusions forbid"; + } + + return $"{Forbids(culprits, applying)} {_render(_min)}, {PinningClause()}"; + } + + /// + /// The distinct exclusion constraints that actually caused the exhaustion — those forbidding at least one + /// value the interval and allow-list would otherwise permit. An exclusion whose values fall outside the + /// surviving domain never bit, so naming it would mislead; first-declared order is preserved. + /// + private IReadOnlyList ExcludingConstraintsInEffect() { + List names = new(); + foreach ((string constraint, double[] values) in _exclusions) { + if (names.Contains(constraint)) { continue; } + if (values.Any(WouldAllowIgnoringExclusions)) { names.Add(constraint); } } - string pinning = _minConstraint ?? _maxConstraint ?? "the declared bounds"; + return names; + } + + /// Whether would be in the domain if no exclusion were applied. + private bool WouldAllowIgnoringExclusions(double value) { + if (_allowed is not null && !_allowed.Contains(value)) { return false; } + + return value >= _min && value <= _max; + } + + /// + /// The subject of the exhaustion clause. A single culprit that is the constraint being applied becomes "it", + /// so the message reads "Cannot apply DifferentFrom(1) because it forbids …" rather than repeating the + /// constraint on both sides of "because". + /// + private static string Forbids(IReadOnlyList names, string applying) { + if (names.Count == 1) { return names[0] == applying ? "it forbids" : $"{names[0]} forbids"; } + + return $"{string.Join(", ", names)} forbid"; + } + + /// Names the bounds that pinned the domain to its single value, for the "forbids X, the only value ... leaves" form. + private string PinningClause() { + List bounds = new(); + if (_minConstraint is not null) { bounds.Add(_minConstraint); } + if (_maxConstraint is not null && _maxConstraint != _minConstraint) { bounds.Add(_maxConstraint); } + + if (bounds.Count == 0) { return "the only value the declared bounds leave"; } + if (bounds.Count == 1) { return $"the only value {bounds[0]} leaves"; } - return $"{pinning} already pins the value to {_render(_min)}, which the exclusions forbid"; + return $"the only value {string.Join(" and ", bounds)} leave"; } } diff --git a/JustDummies/DecimalIntervalSpec.cs b/JustDummies/DecimalIntervalSpec.cs index c3494e21..a528e095 100644 --- a/JustDummies/DecimalIntervalSpec.cs +++ b/JustDummies/DecimalIntervalSpec.cs @@ -40,6 +40,7 @@ private static decimal Pow10(int power) { private readonly decimal _ceiledMin; private readonly List? _effectiveAllowed; private readonly IReadOnlyList _excluded; + private readonly IReadOnlyList<(string Constraint, decimal[] Ordinals)> _exclusions; private readonly int _excludedOnLattice; private readonly decimal _flooredMax; private readonly bool _latticeHasPoint; @@ -59,7 +60,7 @@ private DecimalIntervalSpec(string typeName, Func render, decimal min, string? minConstraint, decimal max, string? maxConstraint, IReadOnlyList? allowed, string? allowedConstraint, - IReadOnlyList excluded, + IReadOnlyList<(string Constraint, decimal[] Ordinals)> exclusions, int scale, string? scaleConstraint) { _typeName = typeName; _render = render; @@ -69,16 +70,19 @@ private DecimalIntervalSpec(string typeName, Func render, _maxConstraint = maxConstraint; _allowed = allowed; _allowedConstraint = allowedConstraint; - _excluded = excluded; + _exclusions = exclusions; _scale = scale; _scaleConstraint = scaleConstraint; + // The flat value set drives every draw-time decision; the provenance in _exclusions is consulted only + // when a conflict message must name the excluding constraint. Materialized once — "constrain once, draw many". + _excluded = exclusions.SelectMany(pair => pair.Ordinals).ToList(); // Lattice-derived state, materialized once — "constrain once, draw many". if (scale >= 0) { _step = 1m / Pow10(scale); _ceiledMin = CeilToGrid(min, scale, _step); _flooredMax = FloorToGrid(max, scale, _step); _latticeHasPoint = _ceiledMin <= _flooredMax; - _excludedOnLattice = excluded.Count(value => value >= min && value <= max && IsOnGrid(value, scale)); + _excludedOnLattice = _excluded.Count(value => value >= min && value <= max && IsOnGrid(value, scale)); } else { _step = 0m; _ceiledMin = min; @@ -100,7 +104,7 @@ internal DecimalIntervalSpec WithMinimum(decimal minimum, string applying) { throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {_maxConstraint} already requires values less than or equal to {_render(_max)}."); } - return Validated(new DecimalIntervalSpec(_typeName, _render, minimum, applying, _max, _maxConstraint, _allowed, _allowedConstraint, _excluded, _scale, _scaleConstraint), applying); + return Validated(new DecimalIntervalSpec(_typeName, _render, minimum, applying, _max, _maxConstraint, _allowed, _allowedConstraint, _exclusions, _scale, _scaleConstraint), applying); } /// Tightens the upper bound; a looser bound than the current one is a no-op. @@ -113,7 +117,7 @@ internal DecimalIntervalSpec WithMaximum(decimal maximum, string applying) { throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {_minConstraint} already requires values greater than or equal to {_render(_min)}."); } - return Validated(new DecimalIntervalSpec(_typeName, _render, _min, _minConstraint, maximum, applying, _allowed, _allowedConstraint, _excluded, _scale, _scaleConstraint), applying); + return Validated(new DecimalIntervalSpec(_typeName, _render, _min, _minConstraint, maximum, applying, _allowed, _allowedConstraint, _exclusions, _scale, _scaleConstraint), applying); } /// Tightens the lower bound to strictly above — the inclusive bound plus a point exclusion. @@ -132,15 +136,16 @@ internal DecimalIntervalSpec WithAllowed(decimal[] values, string applying) { decimal[] distinct = values.Distinct().ToArray(); - return Validated(new DecimalIntervalSpec(_typeName, _render, _min, _minConstraint, _max, _maxConstraint, distinct, applying, _excluded, _scale, _scaleConstraint), applying); + return Validated(new DecimalIntervalSpec(_typeName, _render, _min, _minConstraint, _max, _maxConstraint, distinct, applying, _exclusions, _scale, _scaleConstraint), applying); } /// Adds values the generator must never produce. internal DecimalIntervalSpec WithExcluded(decimal[] values, string applying) { - List excluded = new(_excluded); - excluded.AddRange(values); + // The applied constraint tags its own values, so a later exhaustion message can name the exclusion + // that actually emptied the domain rather than a bound that merely happens to border it. + List<(string Constraint, decimal[] Ordinals)> exclusions = new(_exclusions) { (applying, values) }; - return Validated(new DecimalIntervalSpec(_typeName, _render, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, excluded, _scale, _scaleConstraint), applying); + return Validated(new DecimalIntervalSpec(_typeName, _render, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, exclusions, _scale, _scaleConstraint), applying); } /// @@ -155,7 +160,7 @@ internal DecimalIntervalSpec WithScale(int scale, string applying) { throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {_scaleConstraint} is already defined."); } - return Validated(new DecimalIntervalSpec(_typeName, _render, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, _excluded, scale, applying), applying); + return Validated(new DecimalIntervalSpec(_typeName, _render, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, _exclusions, scale, applying), applying); } /// @@ -324,7 +329,7 @@ private bool IsExcluded(decimal value) { private DecimalIntervalSpec Validated(DecimalIntervalSpec candidate, string applying) { if (candidate.IsSatisfiable()) { return candidate; } - throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {candidate.DescribeExhaustion()}."); + throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {candidate.DescribeExhaustion(applying)}."); } private bool IsSatisfiable() { @@ -341,22 +346,81 @@ private bool IsSatisfiable() { return !IsExcluded(_min); } - private string DescribeExhaustion() { + private string DescribeExhaustion(string applying) { + IReadOnlyList culprits = ExcludingConstraintsInEffect(); + if (_allowed is not null) { - if (_excluded.Count > 0) { - return $"no value {_allowedConstraint} allows remains available"; - } + if (culprits.Count == 0) { return $"none of the values {_allowedConstraint} allows satisfies the constraints already defined"; } - return $"none of the values {_allowedConstraint} allows satisfies the constraints already defined"; + // Only the allow-list values the bounds and scale lattice still permit can be forbidden by an exclusion; + // if some allowed value was already dropped by a bound or the grid, the exclusions do not forbid "every" + // allowed value, so the claim is qualified rather than overstated. + string allowed = _allowed.All(WouldAllowIgnoringExclusions) + ? $"every value {_allowedConstraint} allows" + : $"every value {_allowedConstraint} allows that the other constraints leave"; + + return $"{Forbids(culprits, applying)} {allowed}"; } if (_scale >= 0) { - return $"no {_typeName} value {_scaleConstraint} allows remains between {_render(_min)} and {_render(_max)}"; + if (!_latticeHasPoint || culprits.Count == 0) { return $"no {_typeName} value {_scaleConstraint} allows remains between {_render(_min)} and {_render(_max)}"; } + + return $"{Forbids(culprits, applying)} every {_scaleConstraint} value between {_render(_min)} and {_render(_max)}"; + } + + if (culprits.Count == 0) { + string pinning = _minConstraint ?? _maxConstraint ?? "the declared bounds"; + + return $"{pinning} already pins the value to {_render(_min)}, which the exclusions forbid"; + } + + return $"{Forbids(culprits, applying)} {_render(_min)}, {PinningClause()}"; + } + + /// + /// The distinct exclusion constraints that actually caused the exhaustion — those forbidding at least one + /// value the interval, scale lattice and allow-list would otherwise permit. An exclusion whose values fall + /// outside the surviving domain never bit, so naming it would mislead; first-declared order is preserved. + /// + private IReadOnlyList ExcludingConstraintsInEffect() { + List names = new(); + foreach ((string constraint, decimal[] values) in _exclusions) { + if (names.Contains(constraint)) { continue; } + if (values.Any(WouldAllowIgnoringExclusions)) { names.Add(constraint); } } - string pinning = _minConstraint ?? _maxConstraint ?? "the declared bounds"; + return names; + } + + /// Whether would be in the domain if no exclusion were applied. + private bool WouldAllowIgnoringExclusions(decimal value) { + if (_allowed is not null && !_allowed.Contains(value)) { return false; } + if (_scale >= 0 && !IsOnGrid(value, _scale)) { return false; } + + return value >= _min && value <= _max; + } + + /// + /// The subject of the exhaustion clause. A single culprit that is the constraint being applied becomes "it", + /// so the message reads "Cannot apply DifferentFrom(1) because it forbids …" rather than repeating the + /// constraint on both sides of "because". + /// + private static string Forbids(IReadOnlyList names, string applying) { + if (names.Count == 1) { return names[0] == applying ? "it forbids" : $"{names[0]} forbids"; } + + return $"{string.Join(", ", names)} forbid"; + } + + /// Names the bounds that pinned the domain to its single value, for the "forbids X, the only value ... leaves" form. + private string PinningClause() { + List bounds = new(); + if (_minConstraint is not null) { bounds.Add(_minConstraint); } + if (_maxConstraint is not null && _maxConstraint != _minConstraint) { bounds.Add(_maxConstraint); } + + if (bounds.Count == 0) { return "the only value the declared bounds leave"; } + if (bounds.Count == 1) { return $"the only value {bounds[0]} leaves"; } - return $"{pinning} already pins the value to {_render(_min)}, which the exclusions forbid"; + return $"the only value {string.Join(" and ", bounds)} leave"; } } diff --git a/JustDummies/OrdinalIntervalSpec.cs b/JustDummies/OrdinalIntervalSpec.cs index a1ac575f..4a6e1dfa 100644 --- a/JustDummies/OrdinalIntervalSpec.cs +++ b/JustDummies/OrdinalIntervalSpec.cs @@ -91,7 +91,7 @@ private static bool TryFirstLatticePoint(ulong min, ulong max, ulong anchor, ulo private readonly ulong _domainMax; private readonly ulong _domainMin; private readonly List? _effectiveAllowed; - private readonly IReadOnlyList _excluded; + private readonly IReadOnlyList<(string Constraint, ulong[] Ordinals)> _exclusions; private readonly List _excludedInRange; private readonly List _excludedOnLattice; private readonly ulong _latticeFirst; @@ -111,7 +111,7 @@ private OrdinalIntervalSpec(string typeName, Func render, ulong d ulong min, string? minConstraint, ulong max, string? maxConstraint, IReadOnlyList? allowed, string? allowedConstraint, - IReadOnlyList excluded, + IReadOnlyList<(string Constraint, ulong[] Ordinals)> exclusions, ulong step, ulong anchor, string? stepConstraint) { _typeName = typeName; _render = render; @@ -123,11 +123,14 @@ private OrdinalIntervalSpec(string typeName, Func render, ulong d _maxConstraint = maxConstraint; _allowed = allowed; _allowedConstraint = allowedConstraint; - _excluded = excluded; + _exclusions = exclusions; _step = step; _anchor = anchor; _stepConstraint = stepConstraint; - // Materialized once here — "constrain once, draw many": GenerateOrdinal never refilters or resorts. + // The flat ordinal set drives every hot-path decision; the provenance in _exclusions is consulted only + // when a conflict message must name the excluding constraint. Materialized once here — "constrain once, + // draw many": GenerateOrdinal never refilters or resorts. + ulong[] excluded = exclusions.SelectMany(pair => pair.Ordinals).ToArray(); _excludedInRange = excluded.Where(value => value >= min && value <= max).Distinct().ToList(); _excludedInRange.Sort(); // Lattice-derived state, kept alongside so the hot path is a straight index-and-stride. @@ -156,7 +159,7 @@ internal OrdinalIntervalSpec WithMinimum(ulong minimum, string applying) { throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {_maxConstraint} already requires values less than or equal to {_render(_max)}."); } - return Validated(new OrdinalIntervalSpec(_typeName, _render, _domainMin, _domainMax, minimum, applying, _max, _maxConstraint, _allowed, _allowedConstraint, _excluded, _step, _anchor, _stepConstraint), applying); + return Validated(new OrdinalIntervalSpec(_typeName, _render, _domainMin, _domainMax, minimum, applying, _max, _maxConstraint, _allowed, _allowedConstraint, _exclusions, _step, _anchor, _stepConstraint), applying); } /// Tightens the lower bound to strictly above — the exclusive form of . @@ -176,7 +179,7 @@ internal OrdinalIntervalSpec WithMaximum(ulong maximum, string applying) { throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {_minConstraint} already requires values greater than or equal to {_render(_min)}."); } - return Validated(new OrdinalIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, maximum, applying, _allowed, _allowedConstraint, _excluded, _step, _anchor, _stepConstraint), applying); + return Validated(new OrdinalIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, maximum, applying, _allowed, _allowedConstraint, _exclusions, _step, _anchor, _stepConstraint), applying); } /// Tightens the upper bound to strictly below — the exclusive form of . @@ -192,15 +195,16 @@ internal OrdinalIntervalSpec WithAllowed(ulong[] ordinals, string applying) { ulong[] distinct = ordinals.Distinct().ToArray(); - return Validated(new OrdinalIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, _max, _maxConstraint, distinct, applying, _excluded, _step, _anchor, _stepConstraint), applying); + return Validated(new OrdinalIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, _max, _maxConstraint, distinct, applying, _exclusions, _step, _anchor, _stepConstraint), applying); } /// Adds values the generator must never produce. internal OrdinalIntervalSpec WithExcluded(ulong[] ordinals, string applying) { - List excluded = new(_excluded); - excluded.AddRange(ordinals); + // The applied constraint tags its own ordinals, so a later exhaustion message can name the exclusion + // that actually emptied the domain rather than a bound that merely happens to border it. + List<(string Constraint, ulong[] Ordinals)> exclusions = new(_exclusions) { (applying, ordinals) }; - return Validated(new OrdinalIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, excluded, _step, _anchor, _stepConstraint), applying); + return Validated(new OrdinalIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, exclusions, _step, _anchor, _stepConstraint), applying); } /// @@ -217,7 +221,7 @@ internal OrdinalIntervalSpec WithStep(ulong step, ulong anchor, string applying) throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {_stepConstraint} is already defined."); } - return Validated(new OrdinalIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, _excluded, step, anchor, applying), applying); + return Validated(new OrdinalIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, _exclusions, step, anchor, applying), applying); } /// @@ -305,7 +309,7 @@ private bool IsFullWidth() { private OrdinalIntervalSpec Validated(OrdinalIntervalSpec candidate, string applying) { if (candidate.IsSatisfiable()) { return candidate; } - throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {candidate.DescribeExhaustion()}."); + throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {candidate.DescribeExhaustion(applying)}."); } private bool IsSatisfiable() { @@ -320,26 +324,87 @@ private bool IsSatisfiable() { return _max - _min + 1 - (ulong)_excludedInRange.Count > 0; } - private string DescribeExhaustion() { + private string DescribeExhaustion(string applying) { + IReadOnlyList culprits = ExcludingConstraintsInEffect(); + if (_allowed is not null) { - if (_excluded.Count > 0) { - return $"no value {_allowedConstraint} allows remains available"; - } + if (culprits.Count == 0) { return $"none of the values {_allowedConstraint} allows satisfies the constraints already defined"; } - return $"none of the values {_allowedConstraint} allows satisfies the constraints already defined"; + // Only the allow-list values the bounds and lattice still permit can be forbidden by an exclusion; if + // some allowed value was already dropped by a bound or the lattice, the exclusions do not forbid + // "every" allowed value, so the claim is qualified rather than overstated. + string allowed = _allowed.All(WouldAllowIgnoringExclusions) + ? $"every value {_allowedConstraint} allows" + : $"every value {_allowedConstraint} allows that the other constraints leave"; + + return $"{Forbids(culprits, applying)} {allowed}"; } if (_step > 1UL) { - return $"no {_typeName} value {_stepConstraint} allows remains between {_render(_min)} and {_render(_max)}"; + if (!_latticeHasPoint || culprits.Count == 0) { return $"no {_typeName} value {_stepConstraint} allows remains between {_render(_min)} and {_render(_max)}"; } + + return $"{Forbids(culprits, applying)} every {_stepConstraint} value between {_render(_min)} and {_render(_max)}"; } if (_min == _max) { - string pinning = _minConstraint ?? _maxConstraint ?? "the declared bounds"; + if (culprits.Count == 0) { + string pinning = _minConstraint ?? _maxConstraint ?? "the declared bounds"; - return $"{pinning} already pins the value to {_render(_min)}"; + return $"{pinning} already pins the value to {_render(_min)}"; + } + + return $"{Forbids(culprits, applying)} {_render(_min)}, {PinningClause()}"; + } + + if (culprits.Count == 0) { return $"no value remains between {_render(_min)} and {_render(_max)} once the excluded values are removed"; } + + return $"{Forbids(culprits, applying)} every value between {_render(_min)} and {_render(_max)}"; + } + + /// + /// The distinct exclusion constraints that actually caused the exhaustion — those forbidding at least one + /// value the interval, lattice and allow-list would otherwise permit. An exclusion whose values fall outside + /// the surviving domain never bit, so naming it would mislead; first-declared order is preserved. + /// + private IReadOnlyList ExcludingConstraintsInEffect() { + List names = new(); + foreach ((string constraint, ulong[] ordinals) in _exclusions) { + if (names.Contains(constraint)) { continue; } + if (ordinals.Any(WouldAllowIgnoringExclusions)) { names.Add(constraint); } } - return $"no value remains between {_render(_min)} and {_render(_max)} once the excluded values are removed"; + return names; + } + + /// Whether would be in the domain if no exclusion were applied. + private bool WouldAllowIgnoringExclusions(ulong ordinal) { + if (_allowed is not null && !_allowed.Contains(ordinal)) { return false; } + if (_step > 1UL && !IsOnLattice(ordinal, _anchor, _step)) { return false; } + + return ordinal >= _min && ordinal <= _max; + } + + /// + /// The subject of the exhaustion clause. A single culprit that is the constraint being applied becomes "it", + /// so the message reads "Cannot apply Except(1) because it forbids …" rather than repeating the constraint on + /// both sides of "because". + /// + private static string Forbids(IReadOnlyList names, string applying) { + if (names.Count == 1) { return names[0] == applying ? "it forbids" : $"{names[0]} forbids"; } + + return $"{string.Join(", ", names)} forbid"; + } + + /// Names the bounds that pinned the domain to its single value, for the "forbids X, the only value ... leaves" form. + private string PinningClause() { + List bounds = new(); + if (_minConstraint is not null) { bounds.Add(_minConstraint); } + if (_maxConstraint is not null && _maxConstraint != _minConstraint) { bounds.Add(_maxConstraint); } + + if (bounds.Count == 0) { return "the only value the declared bounds leave"; } + if (bounds.Count == 1) { return $"the only value {bounds[0]} leaves"; } + + return $"the only value {string.Join(" and ", bounds)} leave"; } } diff --git a/JustDummies/WideIntervalSpec.cs b/JustDummies/WideIntervalSpec.cs index e3bed2f2..7de29fdc 100644 --- a/JustDummies/WideIntervalSpec.cs +++ b/JustDummies/WideIntervalSpec.cs @@ -58,7 +58,7 @@ private static bool TryFirstLatticePoint(UInt128 min, UInt128 max, UInt128 ancho private readonly List _excludedInRange; private readonly List _excludedOnLattice; private readonly UInt128 _domainMin; - private readonly IReadOnlyList _excluded; + private readonly IReadOnlyList<(string Constraint, UInt128[] Ordinals)> _exclusions; private readonly UInt128 _latticeFirst; private readonly bool _latticeHasPoint; private readonly UInt128 _max; @@ -76,7 +76,7 @@ private WideIntervalSpec(string typeName, Func render, UInt128 UInt128 min, string? minConstraint, UInt128 max, string? maxConstraint, IReadOnlyList? allowed, string? allowedConstraint, - IReadOnlyList excluded, + IReadOnlyList<(string Constraint, UInt128[] Ordinals)> exclusions, UInt128 step, UInt128 anchor, string? stepConstraint) { _typeName = typeName; _render = render; @@ -88,11 +88,14 @@ private WideIntervalSpec(string typeName, Func render, UInt128 _maxConstraint = maxConstraint; _allowed = allowed; _allowedConstraint = allowedConstraint; - _excluded = excluded; + _exclusions = exclusions; _step = step; _anchor = anchor; _stepConstraint = stepConstraint; - // Materialized once here — "constrain once, draw many": GenerateOrdinal never refilters or resorts. + // The flat ordinal set drives every hot-path decision; the provenance in _exclusions is consulted only + // when a conflict message must name the excluding constraint. Materialized once here — "constrain once, + // draw many": GenerateOrdinal never refilters or resorts. + UInt128[] excluded = exclusions.SelectMany(pair => pair.Ordinals).ToArray(); _excludedInRange = excluded.Where(value => value >= min && value <= max).Distinct().ToList(); _excludedInRange.Sort(); if (step > UInt128.One) { @@ -120,7 +123,7 @@ internal WideIntervalSpec WithMinimum(UInt128 minimum, string applying) { throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {_maxConstraint} already requires values less than or equal to {_render(_max)}."); } - return Validated(new WideIntervalSpec(_typeName, _render, _domainMin, _domainMax, minimum, applying, _max, _maxConstraint, _allowed, _allowedConstraint, _excluded, _step, _anchor, _stepConstraint), applying); + return Validated(new WideIntervalSpec(_typeName, _render, _domainMin, _domainMax, minimum, applying, _max, _maxConstraint, _allowed, _allowedConstraint, _exclusions, _step, _anchor, _stepConstraint), applying); } /// Tightens the lower bound to strictly above — the exclusive form of . @@ -140,7 +143,7 @@ internal WideIntervalSpec WithMaximum(UInt128 maximum, string applying) { throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {_minConstraint} already requires values greater than or equal to {_render(_min)}."); } - return Validated(new WideIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, maximum, applying, _allowed, _allowedConstraint, _excluded, _step, _anchor, _stepConstraint), applying); + return Validated(new WideIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, maximum, applying, _allowed, _allowedConstraint, _exclusions, _step, _anchor, _stepConstraint), applying); } /// Tightens the upper bound to strictly below — the exclusive form of . @@ -156,15 +159,16 @@ internal WideIntervalSpec WithAllowed(UInt128[] ordinals, string applying) { UInt128[] distinct = ordinals.Distinct().ToArray(); - return Validated(new WideIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, _max, _maxConstraint, distinct, applying, _excluded, _step, _anchor, _stepConstraint), applying); + return Validated(new WideIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, _max, _maxConstraint, distinct, applying, _exclusions, _step, _anchor, _stepConstraint), applying); } /// Adds values the generator must never produce. internal WideIntervalSpec WithExcluded(UInt128[] ordinals, string applying) { - List excluded = new(_excluded); - excluded.AddRange(ordinals); + // The applied constraint tags its own ordinals, so a later exhaustion message can name the exclusion + // that actually emptied the domain rather than a bound that merely happens to border it. + List<(string Constraint, UInt128[] Ordinals)> exclusions = new(_exclusions) { (applying, ordinals) }; - return Validated(new WideIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, excluded, _step, _anchor, _stepConstraint), applying); + return Validated(new WideIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, exclusions, _step, _anchor, _stepConstraint), applying); } /// @@ -181,7 +185,7 @@ internal WideIntervalSpec WithStep(UInt128 step, UInt128 anchor, string applying throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {_stepConstraint} is already defined."); } - return Validated(new WideIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, _excluded, step, anchor, applying), applying); + return Validated(new WideIntervalSpec(_typeName, _render, _domainMin, _domainMax, _min, _minConstraint, _max, _maxConstraint, _allowed, _allowedConstraint, _exclusions, step, anchor, applying), applying); } /// @@ -265,7 +269,7 @@ private bool IsFullWidth() { private WideIntervalSpec Validated(WideIntervalSpec candidate, string applying) { if (candidate.IsSatisfiable()) { return candidate; } - throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {candidate.DescribeExhaustion()}."); + throw new ConflictingAnyConstraintException($"Cannot apply {applying} because {candidate.DescribeExhaustion(applying)}."); } private bool IsSatisfiable() { @@ -280,26 +284,87 @@ private bool IsSatisfiable() { return _max - _min + 1 - (UInt128)_excludedInRange.Count > 0; } - private string DescribeExhaustion() { + private string DescribeExhaustion(string applying) { + IReadOnlyList culprits = ExcludingConstraintsInEffect(); + if (_allowed is not null) { - if (_excluded.Count > 0) { - return $"no value {_allowedConstraint} allows remains available"; - } + if (culprits.Count == 0) { return $"none of the values {_allowedConstraint} allows satisfies the constraints already defined"; } - return $"none of the values {_allowedConstraint} allows satisfies the constraints already defined"; + // Only the allow-list values the bounds and lattice still permit can be forbidden by an exclusion; if + // some allowed value was already dropped by a bound or the lattice, the exclusions do not forbid + // "every" allowed value, so the claim is qualified rather than overstated. + string allowed = _allowed.All(WouldAllowIgnoringExclusions) + ? $"every value {_allowedConstraint} allows" + : $"every value {_allowedConstraint} allows that the other constraints leave"; + + return $"{Forbids(culprits, applying)} {allowed}"; } if (_step > UInt128.One) { - return $"no {_typeName} value {_stepConstraint} allows remains between {_render(_min)} and {_render(_max)}"; + if (!_latticeHasPoint || culprits.Count == 0) { return $"no {_typeName} value {_stepConstraint} allows remains between {_render(_min)} and {_render(_max)}"; } + + return $"{Forbids(culprits, applying)} every {_stepConstraint} value between {_render(_min)} and {_render(_max)}"; } if (_min == _max) { - string pinning = _minConstraint ?? _maxConstraint ?? "the declared bounds"; + if (culprits.Count == 0) { + string pinning = _minConstraint ?? _maxConstraint ?? "the declared bounds"; - return $"{pinning} already pins the value to {_render(_min)}"; + return $"{pinning} already pins the value to {_render(_min)}"; + } + + return $"{Forbids(culprits, applying)} {_render(_min)}, {PinningClause()}"; + } + + if (culprits.Count == 0) { return $"no value remains between {_render(_min)} and {_render(_max)} once the excluded values are removed"; } + + return $"{Forbids(culprits, applying)} every value between {_render(_min)} and {_render(_max)}"; + } + + /// + /// The distinct exclusion constraints that actually caused the exhaustion — those forbidding at least one + /// value the interval, lattice and allow-list would otherwise permit. An exclusion whose values fall outside + /// the surviving domain never bit, so naming it would mislead; first-declared order is preserved. + /// + private IReadOnlyList ExcludingConstraintsInEffect() { + List names = new(); + foreach ((string constraint, UInt128[] ordinals) in _exclusions) { + if (names.Contains(constraint)) { continue; } + if (ordinals.Any(WouldAllowIgnoringExclusions)) { names.Add(constraint); } } - return $"no value remains between {_render(_min)} and {_render(_max)} once the excluded values are removed"; + return names; + } + + /// Whether would be in the domain if no exclusion were applied. + private bool WouldAllowIgnoringExclusions(UInt128 ordinal) { + if (_allowed is not null && !_allowed.Contains(ordinal)) { return false; } + if (_step > UInt128.One && !IsOnLattice(ordinal, _anchor, _step)) { return false; } + + return ordinal >= _min && ordinal <= _max; + } + + /// + /// The subject of the exhaustion clause. A single culprit that is the constraint being applied becomes "it", + /// so the message reads "Cannot apply Except(1) because it forbids …" rather than repeating the constraint on + /// both sides of "because". + /// + private static string Forbids(IReadOnlyList names, string applying) { + if (names.Count == 1) { return names[0] == applying ? "it forbids" : $"{names[0]} forbids"; } + + return $"{string.Join(", ", names)} forbid"; + } + + /// Names the bounds that pinned the domain to its single value, for the "forbids X, the only value ... leaves" form. + private string PinningClause() { + List bounds = new(); + if (_minConstraint is not null) { bounds.Add(_minConstraint); } + if (_maxConstraint is not null && _maxConstraint != _minConstraint) { bounds.Add(_maxConstraint); } + + if (bounds.Count == 0) { return "the only value the declared bounds leave"; } + if (bounds.Count == 1) { return $"the only value {bounds[0]} leaves"; } + + return $"the only value {string.Join(" and ", bounds)} leave"; } } From d9b60eb6a2c0bb8062988660a88ac545e60befad Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 27 Jul 2026 11:31:15 +0000 Subject: [PATCH 2/2] test(justdummies): guard conflict-message truthfulness with a property MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The example suite pins the specific exclusion-conflict messages; this adds the class-level guarantee behind them. For every legal combination of Between / MultipleOf / OneOf / Except on each interval engine, the property catches the ConflictingAnyConstraintException and checks its message against a feasibility oracle recomputed independently over a small integer universe: every universal claim ("forbids every ...", "every value between ...") must be backed by that ground truth, a bare allow-list claim must not be used when a bound or the lattice already narrowed the allow-list, and the message must not echo the applied constraint on both sides of "because". This is the one property that reads message text rather than only the exception type. The rule "assert types, not text" (ADR-0040) targets unstable wording; what is asserted here is truthfulness, not phrasing — an invariant with a real input space and no type-level proxy — so it is a property by that same document's core question. It is coupled only to the stable claim fragments, and it fails on the pre-fix engines (the audit that motivated it counted tens of thousands of false messages), which is the falsifiability the suite requires. The oracle and generators are shared; ordinal, decimal and continuous run in the netstandard-safe file, and the 128-bit sibling runs in ModernTypeInvariantProperties, which the net472 floor leg excludes. Refs: #312 --- .../ConflictMessageTruthfulnessProperties.cs | 208 ++++++++++++++++++ .../ModernTypeInvariantProperties.cs | 18 ++ 2 files changed, 226 insertions(+) create mode 100644 JustDummies.PropertyTests/ConflictMessageTruthfulnessProperties.cs diff --git a/JustDummies.PropertyTests/ConflictMessageTruthfulnessProperties.cs b/JustDummies.PropertyTests/ConflictMessageTruthfulnessProperties.cs new file mode 100644 index 00000000..a21b8658 --- /dev/null +++ b/JustDummies.PropertyTests/ConflictMessageTruthfulnessProperties.cs @@ -0,0 +1,208 @@ +#region Usings declarations + +using FsCheck; +using FsCheck.Fluent; + +using JetBrains.Annotations; + +#endregion + +namespace JustDummies.PropertyTests; + +/// +/// The one property in this suite that reads a conflict message rather than only its exception type. The +/// rule "assert exception types, never message text" (ADR-0040) exists because message wording is unstable; +/// the invariant proven here is not the wording but its truthfulness — for every legal combination of +/// constraints that empties the domain, the emitted message must make only claims that are literally true, must +/// name no falsehood, and must not echo the applied constraint on both sides of "because". That correctness has a +/// genuine input space (every bound / lattice / allow-list / exclusion combination) and no type-level proxy, so it +/// is a property, and the audit that first found the defect (issue #312: an allow-list narrowed by a bound was +/// reported as forbidden "entirely" by the exclusion) becomes a standing guard rather than a one-off check. +/// +/// +/// +/// The oracle recomputes feasibility independently over a small integer universe and rejects any message whose +/// universal claim ("forbids every …", "every value between …") is not backed by that ground truth, any bare +/// allow-list claim used when the allow-list was in fact narrowed by another constraint, and any "Cannot apply +/// X because X forbids …" echo. It is deliberately coupled to the stable claim fragments, not the full prose: +/// a reworded message that stops making a checkable claim would pass, but a message that makes a false +/// claim cannot. This property fails on the pre-fix engines (the audit counted tens of thousands of false +/// messages), which is the falsifiability the suite requires. +/// +/// +/// The engines share one exhaustion path, so a builder per family — ordinal (), decimal, +/// continuous () — proves them all; the 128-bit sibling is checked in +/// ModernTypeInvariantProperties, which the net472 floor leg excludes. +/// +/// +[TestSubject(typeof(ConflictingAnyConstraintException))] +public sealed class ConflictMessageTruthfulnessProperties { + + #region Statics members declarations + + /// Small, exact-in-every-numeric-type values; some (10) fall outside the generated Between window on purpose, to drive the narrowed-allow-list case. + internal static readonly int[] Universe = [0, 1, 2, 3, 5, 10]; + + /// Builds an engine's chain in the order Between?, MultipleOf?, OneOf?, Except?; returns the conflict message, or null when the chain is satisfiable. + internal delegate string? EngineBuilder(bool hasBetween, int lo, int hi, int step, int[] allow, int[] excl); + + /// Runs the truthfulness property against one engine, quantifying over the constraint combinations it supports. + internal static void CheckEngine(EngineBuilder build, bool supportsLattice) { + Gen<(bool HasBetween, int Lo, int Hi, int Step, int[] Allow, int[] Excl)> combos = + from hasBetween in Gen.Elements(true, false) + from a in Gen.Choose(0, 4) + from b in Gen.Choose(0, 4) + from step in Gen.Choose(1, supportsLattice ? 3 : 1) + from allowMask in Gen.Choose(0, (1 << Universe.Length) - 1) + from exclMask in Gen.Choose(0, (1 << Universe.Length) - 1) + select (hasBetween, Math.Min(a, b), Math.Max(a, b), step, Subset(allowMask), Subset(exclMask)); + + Prop.ForAll(combos.ToArbitrary(), + combo => { + string? message = build(combo.HasBetween, combo.Lo, combo.Hi, combo.Step, combo.Allow, combo.Excl); + if (message is null) { return true; } + + (int step, int[] allow, int[] excl) = InEffect(combo.HasBetween, combo.Lo, combo.Hi, combo.Step, combo.Allow, combo.Excl); + + return MessageIsTruthful(message, combo.HasBetween, combo.Lo, combo.Hi, step, allow, excl); + }) + .QuickCheckThrowOnFailure(); + } + + private static int[] Subset(int mask) { + List chosen = []; + for (int i = 0; i < Universe.Length; i++) { + if ((mask & (1 << i)) != 0) { chosen.Add(Universe[i]); } + } + + return chosen.ToArray(); + } + + /// The constraints actually in force at the throw: the prefix of the fixed build order up to the first one that empties the domain. + private static (int Step, int[] Allow, int[] Excl) InEffect(bool hasBetween, int lo, int hi, int step, int[] allow, int[] excl) { + int curStep = 1; + int[] curAllow = []; + int[] curExcl = []; + + if (Feasible(hasBetween, lo, hi, curStep, curAllow, curExcl).Count == 0) { return (curStep, curAllow, curExcl); } + if (step > 1) { curStep = step; if (Feasible(hasBetween, lo, hi, curStep, curAllow, curExcl).Count == 0) { return (curStep, curAllow, curExcl); } } + if (allow.Length > 0) { curAllow = allow; if (Feasible(hasBetween, lo, hi, curStep, curAllow, curExcl).Count == 0) { return (curStep, curAllow, curExcl); } } + if (excl.Length > 0) { curExcl = excl; } + + return (curStep, curAllow, curExcl); + } + + private static List Feasible(bool hasBetween, int lo, int hi, int step, int[] allow, int[] excl) { + int rangeLo = hasBetween ? lo : -50; + int rangeHi = hasBetween ? hi : 50; + + List feasible = []; + for (int value = rangeLo; value <= rangeHi; value++) { + if (allow.Length > 0 && !allow.Contains(value)) { continue; } + if (excl.Contains(value)) { continue; } + if (step > 1 && value % step != 0) { continue; } + feasible.Add(value); + } + + return feasible; + } + + /// The oracle: true when every checkable claim the message makes is backed by independently computed ground truth. + private static bool MessageIsTruthful(string message, bool hasBetween, int lo, int hi, int step, int[] allow, int[] excl) { + // A conflict was thrown, so the in-effect domain must genuinely be empty. + if (Feasible(hasBetween, lo, hi, step, allow, excl).Count != 0) { return false; } + + // Allow-list claims. The bare form asserts every allowed value is forbidden; the qualified form asserts only + // the values the bounds and lattice still permit are forbidden. + if (message.Contains("every value") && message.Contains("allows") && allow.Length > 0) { + int rangeLo = hasBetween ? lo : -50; + int rangeHi = hasBetween ? hi : 50; + int[] reachable = allow.Where(a => a >= rangeLo && a <= rangeHi && (step <= 1 || a % step == 0)).ToArray(); + + bool qualified = message.Contains("that the other constraints leave"); + bool claimTrue = qualified ? reachable.All(a => excl.Contains(a)) : allow.All(a => excl.Contains(a)); + if (!claimTrue) { return false; } + + // The bare form must not be used when a bound or the lattice already dropped an allowed value. + if (!qualified && reachable.Length != allow.Length) { return false; } + } + + // A range claim must hold for every value in the window. + if (hasBetween && message.Contains($"every value between {lo} and {hi}")) { + if (!Enumerable.Range(lo, hi - lo + 1).All(value => excl.Contains(value))) { return false; } + } + + // A lattice claim must hold for every on-lattice value in the window. + if (hasBetween && step > 1 && message.Contains($"every MultipleOf({step}) value between {lo} and {hi}")) { + if (!Enumerable.Range(lo, hi - lo + 1).Where(value => value % step == 0).All(value => excl.Contains(value))) { return false; } + } + + // Comprehensibility: no malformed fragment, and no "Cannot apply X because X forbids …" echo. + if (message.Contains(" ") || message.Contains(" ,") || message.Contains("forbids ,") || message.Contains("forbid ,")) { return false; } + int because = message.IndexOf(" because ", StringComparison.Ordinal); + if (because >= 0 && message.StartsWith("Cannot apply ", StringComparison.Ordinal)) { + int prefix = "Cannot apply ".Length; + string applied = message.Substring(prefix, because - prefix); + string clause = message.Substring(because + " because ".Length); + if (clause.StartsWith(applied + " forbids", StringComparison.Ordinal) || clause.StartsWith(applied + " forbid", StringComparison.Ordinal)) { return false; } + } + + return true; + } + + #endregion + + [Fact(DisplayName = "Ordinal: every exclusion-caused conflict message makes only true claims, over the whole combination space.")] + public void OrdinalConflictMessagesAreTruthful() { + CheckEngine(BuildInt32, supportsLattice: true); + } + + [Fact(DisplayName = "Decimal: every exclusion-caused conflict message makes only true claims, over the whole combination space.")] + public void DecimalConflictMessagesAreTruthful() { + CheckEngine(BuildDecimal, supportsLattice: false); + } + + [Fact(DisplayName = "Continuous: every exclusion-caused conflict message makes only true claims, over the whole combination space.")] + public void ContinuousConflictMessagesAreTruthful() { + CheckEngine(BuildDouble, supportsLattice: false); + } + + #region Engine builders + + private static string? BuildInt32(bool hasBetween, int lo, int hi, int step, int[] allow, int[] excl) { + try { + AnyInt32 spec = Any.Int32(); + if (hasBetween) { spec = spec.Between(lo, hi); } + if (step > 1) { spec = spec.MultipleOf(step); } + if (allow.Length > 0) { spec = spec.OneOf(allow); } + if (excl.Length > 0) { spec = spec.Except(excl); } + + return null; + } catch (ConflictingAnyConstraintException exception) { return exception.Message; } + } + + private static string? BuildDecimal(bool hasBetween, int lo, int hi, int step, int[] allow, int[] excl) { + try { + AnyDecimal spec = Any.Decimal(); + if (hasBetween) { spec = spec.Between(lo, hi); } + if (allow.Length > 0) { spec = spec.OneOf(allow.Select(value => (decimal)value).ToArray()); } + if (excl.Length > 0) { spec = spec.Except(excl.Select(value => (decimal)value).ToArray()); } + + return null; + } catch (ConflictingAnyConstraintException exception) { return exception.Message; } + } + + private static string? BuildDouble(bool hasBetween, int lo, int hi, int step, int[] allow, int[] excl) { + try { + AnyDouble spec = Any.Double(); + if (hasBetween) { spec = spec.Between(lo, hi); } + if (allow.Length > 0) { spec = spec.OneOf(allow.Select(value => (double)value).ToArray()); } + if (excl.Length > 0) { spec = spec.Except(excl.Select(value => (double)value).ToArray()); } + + return null; + } catch (ConflictingAnyConstraintException exception) { return exception.Message; } + } + + #endregion + +} diff --git a/JustDummies.PropertyTests/ModernTypeInvariantProperties.cs b/JustDummies.PropertyTests/ModernTypeInvariantProperties.cs index 1a24c20d..cde6a82c 100644 --- a/JustDummies.PropertyTests/ModernTypeInvariantProperties.cs +++ b/JustDummies.PropertyTests/ModernTypeInvariantProperties.cs @@ -176,6 +176,24 @@ public void Int128LessThanIsStrictAndConflictsAtTheFloor() { .QuickCheckThrowOnFailure(); } + [Fact(DisplayName = "Int128: every exclusion-caused conflict message makes only true claims, over the whole combination space.")] + public void Int128ConflictMessagesAreTruthful() { + // The 128-bit sibling of the ordinal engine; the shared oracle lives in ConflictMessageTruthfulnessProperties. + ConflictMessageTruthfulnessProperties.CheckEngine(BuildInt128, supportsLattice: true); + } + + private static string? BuildInt128(bool hasBetween, int lo, int hi, int step, int[] allow, int[] excl) { + try { + AnyInt128 spec = Any.Int128(); + if (hasBetween) { spec = spec.Between(lo, hi); } + if (step > 1) { spec = spec.MultipleOf(step); } + if (allow.Length > 0) { spec = spec.OneOf(allow.Select(value => (Int128)value).ToArray()); } + if (excl.Length > 0) { spec = spec.Except(excl.Select(value => (Int128)value).ToArray()); } + + return null; + } catch (ConflictingAnyConstraintException exception) { return exception.Message; } + } + [Fact(DisplayName = "Int128: Positive and Negative meet a bound on their own side of zero, and conflict with one on the other.")] public void Int128SignConstraintsMeetABoundOrConflict() { Prop.ForAll(Int128Values().ToArbitrary(),