ADT invariant does not appear in the path for verification conditions

[jad-hamza]

I was expecting the post-condition of theorem to go through due to the false invariant of False, but it is reported as invalid.

object False {
  case class False() {
    require(false)

    def theorem() = {
      assert(false)
    }
  }
}

[romac]

As another data point, the following example goes through without issues:

object Pos {
  case class Pos(n: BigInt) {
    require(n > 0)

    def inner = {
      assert(n > 0)
    }

    def value = n
  }

  def outer = {
    assert(Pos(2).value > 0)
  }
}

[romac]

Also to be noted that:

object False {
  case class False() {
    require(false)

    def theorem() = {
      assert(false)  // invalid
    }

    def isTrue = false
  }

  def outer = {
    assert(False().isTrue) // invalid (add invariant + body assertion)
  }
}

[romac]

Looking at the TIP output for False.theorem, we see this:

(assert (not false))

(check-sat)

; check-assumptions required here, but not part of tip standard

while for Pos.inner, we get:

(declare-datatypes () ((Pos!3 (Pos!4 (n!7 Int)))))

(declare-const thiss!7 Pos!3)

(datatype-invariant thiss!6 Pos!3 (> (let ((e!11 thiss!6)) (n!7 e!11)) 0))

(assert (not (> (n!7 thiss!7) 0)))

(check-sat)

; check-assumptions required here, but not part of tip standard

[romac]

On the other hand, with get the following by adding a field to False and referencing it from within inner:

object False2 {
  case class False2(n: BigInt) {
    require(false)

    def inner = {
      assert(n > 0 || n <= 0) // valid
      assert(false) // valid
    }

    def isTrue = false
  }

  def outer = {
    assert(False2(42).isTrue) // invalid (both body assertion and adt invariant)
  }
}

The weird thing is that the VC corresponding to assert(false) is ¬(thiss.n > 0 || thiss.n <= 0), and the corresponding TIP output is thus:

(declare-datatypes () ((False2!7 (False2!8 (n!9 Int)))))

(declare-const thiss!3 False2!7)

(datatype-invariant thiss!0 False2!7 false)

(assert (not (not (or (> (n!9 thiss!3) 0) (<= (n!9 thiss!3) 0)))))

(check-sat)

; check-assumptions required here, but not part of tip standard

[samarion]

This issue is caused by the thiss variable corresponding to the instance of the ADT with a require is not used in the VC and is therefore simplified in Inox. I have already added support in Inox for introducing a context in which the VC has to be verified, however we still need to change the verification checker to a type checker as described in the foundations paper.