forAll with ||, and exists with &&, can be inconsistent

Summary

Revised original post on 9/19/18 and 9/20/18 based on additional research and (slightly) deeper understanding of the implementation logic.

Issue: Prop.&&(Prop): Prop and Prop.||(Prop): Prop can be logically inconsistent with their component Props.

• Props are fundamentally stateless. In particular the result of each test is independent of prior results. This applies to existential, universal, and binary combinations && and ||.

• An exists prop that has been proved with one test may appear undecided with the next. Continuing to reevaluate a proved prop effectively erases the information that it has been proved. This allows subsequent evaluations to cause an inconsistent result.

• A forAll prop that has been falsified with one test may appear true with the next.
  Continuing to reevaluate a falsified prop effectively erases the information that it has been falsified. This allows subsequent evaluations to cause an inconsistent result.

• Test.check(Parameters,Prop) accumulates the results of multiple evaluations of its top-level Prop. If the top-level Prop is a combination, it reevaluates its own components each time it is evaluated, but with no memory of prior results of its components.

• In the case of a && combination with exists components, the && result is Proved if and only if both exists components evaluate to Proved for the same top-level test iteration. Otherwise && returns Undecided. This can result in exhausting the Prop, even if both components evaluated to Proved, although at different test iterations.

• In the case of a || combination with forAll components, the || is False if and only if both forAll components evaluate to False for the same top-level test iteration. Otherwise || returns True. This can result in the top-level Prop succeeding even though both components were falsified, although at different test iterations.

This results in incorrect results for && and ||. Detailed examples below.

Correcting this issue seems to require remembering more history of component Props (for && and ||, or more generally, an arbitrary tree of Props) and ceasing reevaluation of any component Prop that has been unequivocally proved or disproved. That is, exists props that are Proved due to a true evaluation, and forAll props that have falsified due to a false evaluation should not be further reevaluated.

The inconsistency can be demonstrated unambiguously (100% guaranteed) in a small specialized failing case with just two properties and a fixed-order generator. See Example 1 below.

The inconsistency can be demonstrated in a slightly more realistic scenario as well, involving a
larger number of properties, based on random generators. With the random generators, the
inconsistency is highly probable, but not 100% guaranteed. See Example 2 below.

Note on Current Implementation

The current implementations of && and || are correct in specific cases:

• Conjunction of universal properties (&& of forAll) gives the expected outcomes. This seems
  likely to be the most common case in practice.

• Disjunction of existential properties (|| of exists) gives the expected outcomes.

In the former case (&& of forAll), the semantics of success require that all evaluations of all component prop by true

Likewise for || of exists, the semantics of success require the entire predicate matrix to have
at least one true in some components at some iteration. For the combination prop to be false, all results for all iterations must be false.

Workarounds

For conjuction of existential properties a workaround is to create and test separate properties and
avoid the conjunction.

For disjunction of universal properties a workaround is to combine the predicates into a single
predicate wrapped in a single property. Of course, this requires a common generator.

Detailed Example 1

This example demonstrates the inconsistency 100% repeatably because it relies on fixed-order
non-random generators and props based on them which are carefully orchestrated to align (or misalign)
the predicate streams to demonstrate the inconsistency.

Example 2

Example 1 Code

  // Factory for fixed order (true, false, ...) generators. 
  def makeTF(): Gen[Boolean] = {
    val c = List(true, false)
    var it = c.iterator
    Gen.const(-99).map { _ => if (!it.hasNext) it = c.iterator; it.next }
  }

  // Prop factory: asserts that some generated value == `b`. (Expected to succeed.)
  def makeExists(b: Boolean): Prop = exists(makeTF())(_ == b)

  // Prop factory: asserts that all generated values == `b`. (Expected to fail.)
  def makeForAll(b: Boolean): Prop = forAll(makeTF())(_ == b)

  // Each makeExists property succeeds individually.
  List(true, false).foreach { i =>
    val ep = makeExists(i)
    property(s"ep($i) succeeds individually") = ep
  }

  // Conjunction of successful existential properties fails.
  val epT = makeExists(true)
  val epF = makeExists(false)
  val conjunction = epT && epF
  property(s"ep(true) && ep(false) fails") = conjunction

  // Each makeForAll property fail individually.
  List(true, false).foreach { i =>
    val ap = makeForAll(i)
    property(s"ap($i) fails individually") = ap
  }

  // Disjunction of failing universal properties succeeds.
  // (Edited original post to correct typo. 16 Sep 2018.)
  val apT = makeForAll(true)
  val apF = makeForAll(false)
  val disjunction = apT || apF
  property(s"ap(true) || ap(false) succeeds") = disjunction

Notes on the code

• The makeTF factory method produces fixed order generators, that always generate the stream (true, false, true, false, ...).
• The makeExists and makeForAll factory product properties based on makeTF generators.
• Each property based on fixed order generators require fresh Prop and fresh Gen instances.
• The constructed Props are assigned to val before being set assigned to a property: See [https://github.com/rickynils/scalacheck/issues/424 Issue 424]

Example 1 Output

Here is the output (lightly edited) from checking the above properties.

+ ep(true) succeeds individually: OK, proved property.
+ .ep(false) succeeds individually: OK, proved property.
! ep(true) && ep(false) fails: Gave up after only 0 passed tests. 501 tests were discarded.

! ap(true) fails individually: Falsified after 1 passed tests.
! ap(false) fails individually: Falsified after 0 passed tests.
+ ap(true) || ap(false) succeeds: OK, proved property.

Detailed Example 2

This example demonstrates the inconsistency with very high probability but not 100%.

It is a bit more realisitic than the contrived Example 1.

The combined all prop uses 10 props that separately check the the choose(0,9) does in fact, eventually,
choose each integer in the range (0 to 9).

However for the all conjunction to succeed it requires that some specific iteration of the 10
generators for the 10 properties generates the precise sequence of values (0, 1, 2, 3, 4, 5, 6, 7, 8, 9). This is extremely unlikely. It's probability is (.1)^10 = 1 in 10 billion.

Example 2 Code

  def makeChooseProp(n: Int) = exists(Gen.choose(0,9))(_ == n)

  (0 to 9).foreach { i =>
    val p = makeChooseProp(i)
    property(s"makeChooseProp($i) succeeds") = p
  }

  val props = (0 to 9).map(makeChooseProp)
  property("(0 to 9).map(makeChooseProp) generally fails") = all(props:_*)

Example 2 Output

+ makeChooseProp(0) succeeds: OK, proved property.
+ makeChooseProp(1) succeeds: OK, proved property.
+ makeChooseProp(2) succeeds: OK, proved property.
+ makeChooseProp(3) succeeds: OK, proved property.
+ makeChooseProp(4) succeeds: OK, proved property.
+ makeChooseProp(5) succeeds: OK, proved property.
+ makeChooseProp(6) succeeds: OK, proved property.
+ makeChooseProp(7) succeeds: OK, proved property.
+ makeChooseProp(8) succeeds: OK, proved property.
+ makeChooseProp(9) succeeds: OK, proved property.
! (0 to 9).map(makeChooseProp) generally fails: Gave up after only 0 passed tests. 501 tests were discarded.

Start with Test.check and the Prop composition paths for &&, ||, exists, and forAll, then run the fixed-order Example 1 from the issue. Done means the combined properties retain proved or falsified component results across evaluations and no longer produce the inconsistent outcomes shown in the example.