samplesMeetTheEvidenceFloor

The four laws below were handed enough evidence to have tested anything: at least DISTINCT_SAMPLE_FLOOR pairwise-distinct samples.

This is not a test of the type; it is a test of the evidence — the same job us.tractat.kuilt.conformance.lattice.LatticeLawSuite.generatorIsNotVacuous does for the generated half of this pair, which is the half that had it. Every law here quantifies over samples, so a binding returning listOf(x) — or listOf(x, x, x) — clears pieceIsIdempotent, pieceIsCommutative, pieceIsAssociative and pieceIsLeastUpperBound having compared one value with itself, on any type whatsoever, and the suite reports four green laws over a lattice it never entered. That was true of this suite from the day it was written: the floor was in samples' KDoc and nothing read it (#2312). Hand-picked lists are exactly the ones a tidy-up shrinks, and a shrunk list has no other tripwire.

The measured counts print on every run, green or red, because a floor whose value nobody sees is a floor nobody notices drifting toward.

Distinct by ==, and why that is the reading rather than distinct-by-bytes — see checkSampleEvidenceFloor, which also argues why the count is not samples().toSet().size.

What this cannot detect, and where each one is covered instead:

  • Three distinct but totally ordered samples. A chain clears this floor, and a chain is a thinner search than three mutually concurrent states — concurrency is where a join has to decide something. It is not floored here because it cannot be: a genuinely totally-ordered lattice has no concurrent pair to offer (IntMax is one, and its binding is a chain by nature), so a concurrency floor needs a per-binding declaration to waive it. The sibling has exactly that — us.tractat.kuilt.conformance.lattice.VacuityFloors.concurrentPairs, waived by us.tractat.kuilt.conformance.lattice.VacuityFloors.totalOrder — and measures it as a rate over a generated pool, which a hand-picked list of four is not.

  • Samples that are distinct but dull — three values that never exercise a branch of the type's piece. Nothing here reads the type's decision tree; retirementReAssertion is the one shape this suite insists on by name, and the sibling's op alphabet is where breadth is measured.

  • A type whose equals is broken outright — one returning false for a value against itself reads every entry as distinct and clears this floor. pieceIsIdempotent reds on such a type first, so the pair is sound; this guard alone is not.

  • A samples that returns a different list on each call. The floor measures the call it made; another law's call could still be thin. No binding does this and nothing stops one.