Enforce purity for class invariants

[mario-bucev]

Also adds some explanation when purity is expected, specifying which impure functions were called. Closes #1474

[vkuncak]

Can we also have a first few lines in docs on purity annotation of parameters? Here is a patch for reference to the thesis.

patch.txt

[mario-bucev]

Yes, good idea!

[mario-bucev]

I've added some examples for @pure parameters in the section discussing @extern functions and methods of non-sealed traits.

[vkuncak]

This test fails?

import stainless._
import stainless.lang._
import stainless.annotation._

object i1306b {
  def root(a: BigInt): BigInt = {
    require(a >= 0)
    var i: BigInt = 0
    def nextSquare = ((i + 1) * (i + 1))
    def accessI(x: BigInt, y: BigInt) = i + x + y
    def modifyI(x: BigInt, y: BigInt) = { i += x + y }
    (while (nextSquare <= a) {
      decreases(a - nextSquare)
      val z = accessI(a, nextSquare)
      assert(z == i + a + (i + 1) * (i + 1))
      val w = accessI(a, i)
      assert(w == i + a + i)
      i = i + 1
    }) invariant { i >= 0 && ((i * i) <= a) }
    i
  } ensuring { root => (root * root) <= a && a < ((root + 1) * (root + 1)) }
}

[mario-bucev]

This one is flaky, funnily enough I've just opened a PR to disable it (https://github.com/epfl-lara/stainless/pull/1478). The CI was unexpectedly slower for some of the PRs, there might be other processes running on the server.