Report counterexamples for traits and simplify them for functions and traits

[vkuncak]

In the code below, Stainless reports counterexample value of f in twice but does not report the analogous value of trait valued t apply method in tracetr:

import stainless._
import stainless.lang._

object Transform {
  def twice(f: Int => Int): Int = {
    f(f(0))
  }.ensuring(_ == 0)

  trait Transformer {
    def apply(e: Int): Int
  }
  def twicetr(t: Transformer): Int = {
    t(t(0))
  }.ensuring(_ == 0)
}

Clearly such examples are very useful. Instead, it reports a counterexample where t is equal to TransformerExt(0), whatever that is.

As an orthgonal note: for trace it reports

[Warning ] Found counter-example:
[Warning ]   f: (Int) => Int -> (x$129: Int) => if (x$129 == 1) {
[Warning ]     1
[Warning ]   } else if (x$129 == 0) {
[Warning ]     1
[Warning ]   } else if (true) {
[Warning ]     1
[Warning ]   } else {
[Warning ]     1
[Warning ]   }

where it would be nice to simplify the final if (true) test and possibly also to eliminate branches that are equal to the default branch. This should give constant function (x$129: Int) => 1 in this case.

[vkuncak]

@samarion wrote: Yes, the interpretation does exist in the model, it's just not extracted correctly for printing It's stored in the chooses field: https://github.com/epfl-lara/inox/blob/dc719cc9602df4b47fe20150a133910bc2b34dd6/src/main/scala/inox/Model.scala#L31

[saraswat]

Absolutely, given all the machinery available, it would be awesome for the user for the machinery to be applied to generate succinct results.

In the context of Stainless, generation of counter-examples (that are potentially recursive programs) is very natural (though of course, immensely difficult). For this, it may be useful to think through source language support in Stainless for refutations, much in the same way that assert and ensuring support verification.

For example, one could build on Sketch's ? expression (e.g. val x:T = _ and related syntax). The could be the trigger for Stainless to synthesize a term t of type T (that would be legal at this point in the code -- hence can use only accessible symbols).

// Program I
def fact_invert(y: Int):Int = {
 require(y > 0)
   _
} ensuring(_ >= 0 && fact(_) <= y && fact(_+1) > y)

This is just a reformulation of the following "verification" program (whose counter-example is the witness):

 // Program II
def fact_invert(y: Int):Int = {
 require(y > 0)
 fails(forall(x:Int => fact(x) > y || fact(x+1) <= y)
} 

As and when there gets to be support for dependent types (as we had worked out in X10 ~15 years ago), Program I could be written as:

// Program III
def fact_invert(y: Int{_ >0}):Int{_ >= 0 && fact(_) <= y && fact(_+1) > y} = _

This is of course intimately tied to Scala implicit (though AFAIK the synthesis algorithm there is restricted).

The above is illustrative -- the real value, of course, would be synthesis of programs over ADTs. This kind of "synthesis from logical specifications" could, again, be very useful practically many settings where business professionals have to deal with detailed logical specifications (e.g. how buy and sell orders are to be matched against each other). (Of course this kind of "logic" programming had been envisioned by people like Cordell Green in the 60s ... but now we might be able to do this for real for some concrete application domains ...)

All of this is natural and obvious -- apologies if this has already been worked out by various groups ... need to read up where people are on synthesis now.

[vkuncak]

@saraswat : Yes, higher-order counterexample finding is synthesis. We worked on this for a number of years, but we can already return many non-recursive examples without doing much extra work. I would say that synthesis of recursive functions is too slow to be invoked automatically. When we did this, we did check back to Cordel Green's work when reading on related work for our work on synthesis. Here are some papers from our group:

• CACM research highlight paper Software Synthesis Procedures
• Refutation-Based Synthesis in SMT
• Synthesis Modulo Recursive Functions A talk around 50 minutes that gives overview is here. https://youtu.be/EA4TY47ihzg You can still install Leon system to try it, but web interface (leon.epfl.ch or leondev.epfl.ch) may not necessarily work, especially over firewall.

[romac]

@saraswat Re: dependent types: while Inox has some support for dependent types, it's not exposed in Stainless. We do however support refinement types in the Dotty frontend with the following syntax:

def fact_invert(y: { Int => y > 0 }): { r: { Int r >= 0 && fact(r) <= y && fact(r + 1) > y } = _

[vkuncak]

Yes, but Re: dotty, #713