Reflection

[romac]

@romac's meta approach seems very convenient to use and indeed promising. In any case, we need some meta.api that reflects (a subset of) Stainless trees. This can be initially just a syntax tree you can import and then add later functionality for it. Let's think about the layered API for reflecting syntax, starting with expressions that can be mapped to boolean circuits (so also including Int and Long operations). This is something that Dragana can then use and even interface it with Chisel.

Let us keep the above goal in mind as non-controversial while we ponder things more broadly.

What I infer about @romac's particular solution is that it acts a bit like Dotty's reflection phases in a compiler. This is a more controlled, yet a little more limited, than exposing Stainless/Inox as an API in Scala programs that you can execute, which is what I am after. Maybe a modification of 'choose' can recover such functionality when you run Stainless code, as in Kaplan:

http://lara.epfl.ch/~kuncak/papers/KoeksalETAL12ConstraintsControl.pdf

It is easy to understand what ScalaZ3 does. Now, Kaplan added Inox-like capabilities for solving on top of ScalaZ3, as well as the ability to lift static function definitions to trees, which I think romac's prototype also does and maybe more flexibly. Yet Kaplan performed a compilation: you got a compiled Scala code that could invoke constraint solver and make decisions based on outcomes of solving constraints, including using counterexamples returned as value. This allows you to really use constraints as in Constraint Logic Programming (CLP(X)), and also allows you to write reasonably performing custom theorem provers.

So, I wonder: could we enrich 'choose' to do these things:

• be also able to accept reflected tree as input, not just 'boolean' expression
• can be implemented as pre-transformation on trees that can be compiled (with dependency on Inox), so we do not need an interpreter to execute them and the things outside choose run at normal Scala speed
• possibly be available with find variant (gives back models) and findAll options (which returns a stream of models)
• allow choosing solver options (not elegant, but likely useful)

Thus, such compiled 'choose' properly lifts Stainless into the computation domain. This is likely some work to do as far as I understand, but it does not seem too confusing regarding how we want it to work, especially given Kaplan, ScalaZ3, and even Welder as reference points. To emphasize again, the code that manipulates various trees in this model executes at normal Scala speed. It is not really different than a user hacking Stainless to make it do what you want, except that it should be easier for users to start doing it as they don't need to wonder where to start and what to change.

We can say that the current way of invoking Stainless is equivalent to automatically creating a verification script that verifies each method, but then we will allow user to write their own verification scripts as methods stored in same files. So, in addition to

--functions=foo

we could give option

--meta-functions=bar

that invokes 'bar' as a meta-level script that explicitly starts other verification tasks.

Once we think about verification in this way, we can also introduce hints that escape back into the meta level, indicating which tactics one should use to do verification. For example, you could say

def hardBitvectorThing(x: Long, y: Long, z: Long): Unit = {
} ensuring (_ => x*(y+z) = (z+y)*x) by bitVectorMaster

def bitVectorMaster(x: meta.Expr): meta.Theorem = {
 find(meta.Not(x),solver="cvc4",ops=List("tryHard")) match {
   case Counterexample(s) => false
   case UNSAT(theorem) => theorem
   case Unknown => bitVectorMaster(simplify(x))
 }
}

here "by" is used like "because" but its argument is the name of a function that goes from meta.Expr to a meta theorem. When you generate VC, you invoke this function on it. Initially, theorems are just private-constructor wrappers around expressions, returned only by Inox. Then you can compose them just like in Welder.

Eventually I would also like to have meta functions like bitVectorMasterbe accepted by Stainless, so that we can prove things about them. We could write specifications on trees saying findAll(!expr)==Stream.empty which would be a way of saying that 'expr' represents a theorem expressed in a computable sub-language. We could also prove that certain tree transformations preserve equivalence and then use them as rewrites. But this is something we can explore afterwards.

So, this is sort of what I am wondering about. Your proposal that performs staged computation as a stainless phase is lighter-weight from user's view and can probably co-exist with the more flexible 'choose'-based approach, but the experience shows time and again that wonderful things can happen when you give users power tools like this scripted verification. It may also be the preferred approach when using meta facilities for constructing System FR types; I need to think more on that.

— @vkuncak

Related to #683.

[romac]

For reference, the meta approach attributed to me above is a very simple way of reflecting/quoting expressions, and splicing them back into the program, which looks like:

  @meta
  def mul(n: Int, expr: Expr[Int]): Expr[Int] = {
    require(n >= 0)
    if (n == 0) Expr.IntLiteral(0)
    else if (n == 1) expr
    else Expr.Plus(expr, mul(n - 1, expr))
  }

  def testMul = {
    val five = splice(mul(5, quote(1)))
    assert(5 == five)
  }

and yields the following program after the reflection phase:

  def testMul = {
    val five = 1 + 1 + 1 + 1 + 1
    assert(5 == five)
  }

[samarion]

Isn't the difference between the two proposals just a question of somehow exposing the solver within the meta-language API (and maybe compiling meta functions)? I expect that exposing the solver should be straightforward. As for compiling meta functions, if we rely on codegen, this should be relatively easy. We can probably also use the Scala compiler somehow but that might be more involved, especially if we want to allow meta functions to call back out into the solver.

[romac]

Isn't the difference between the two proposals just a question of somehow exposing the solver within the meta-language API (and maybe compiling meta functions)?

It is, I just figured I would open this issue as a kind of meta-issue for discussion/tracking progress, but we could indeed merge them.

I expect that exposing the solver should be straightforward. As for compiling meta functions, if we rely on codegen, this should be relatively easy. We can probably also use the Scala compiler somehow but that might be more involved, especially if we want to allow meta functions to call back out into the solver.

Agreed, on both points.