Problem with preprocessing?

[jad-hamza]

import leon.lang._
import leon.proof._

object Preprocessing {

  def theorem(b: Boolean): Unit = {
    require (b)

    check(b)
    true

  } ensuring ( _ => true )

}

The check(b) fails. Is there an issue with preprocessing?

Removing ": Unit", "true" (at the end), or the ensuring clause make the verification go through.

[mantognini]

I had a very brief look at it with --debug=trees and it appears that your code is understood as:

object Preprocessing$0 {
  def theorem$0(b$0 : Boolean): Unit =  {
    require(b$0)
    check$0(b$0)
    true
  } ensuring {
    (x$1$0 : Boolean) => true
  }
  () // <- Mind this part
}

and then the xlang desugaring phase will, mistakenly, keep only the check-part. I believe the issue is linked to ExprOps.preconditionOf and ExprOps.postconditionOf not handling blocks as the FunDef pre/postcondition are both None before xlang desugaring phase.

The question is, should those functions be fixed or should such program be explicitly rejected? (It could be argued that having return type of Boolean for a theorem is more intuitive.) Maybe @regb knows?

[regb]

Indeed the issue is that require/ensuring can be attached to any expression, and due to the Unit type and the final boolean expression, the parsed expression is a sequence of two operations:

  def theorem(b: Boolean): Unit =  {
    val tmp = {
      require(b)
      check(b)
      true
    } ensuring {
      (_ : Boolean) => true
    }
    ()
  }

And then for some reason, xlang extract the check function call without the require. That could be fixed, but then there are other issues in the solver itself, which does not seem to support require at arbitrary position in the tree.

In an ideal world we should be able to solve the solver, I don't see any issue with supporting require at any level of a function @colder @samarion @manoskouk ? But for now it's probably better to be careful and not write such functions.

[manoskouk]

This seems like a typo to me (the return type should be Boolean), but on the subject itself: Right now, require and ensuring are handled as pre- and postconditions of entire functions respectively. I think this is what they are meant to mean in Scala as well. If you need to state an assumption within the body of the function, one would use assume (resp. assert). Assert is already available, whereas assume is not. Introducing assume is of course possible but would be slightly complicated because we would need to check the assumption in all call sites. There are certainly a few benchmarks that could use it but it is not high in our priority list.