Support for Float (was: Feature request: Adding support for scala Long's)

[saraswat]

For industrial projects it is useful to work with Byte, Long and other basic data types.

Seems like it should be easy to add in support?

If someone from the team can outline the process for Stainless blessing existing core classes (what needs to change, where), we could try to follow that and submit a pull request..I am poking around, but am sure we will be able to work faster with some guidance.

(FWIW, it appears Stainless knows about Long and operations on it, even though this is not mentioned in Pure Scala.)

[samarion]

I believe in this instance that it's rather the documentation which isn't up to date wrt the implementation. CodeExtraction seems to be correctly extracting the Byte, Long, etc. types. Do you have a snippet where extraction/verification is failing?

[saraswat]

(Thanks for the link to the relevant class. Much appreciate. Gives us a place to try to hook in. Is it possible to get the error message generated at the end of the file to display the offending source code pos?)

It does fail for Float. I have tried Byte and Long. Not yet tried Short.

Here is FloatTest -- tracebacks because of missing dependencies on Float$0.

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

import stainless.collection.List
// This does not work in stainless

case class CheckFloat(x: Float, a:Float) {
/*
  def i: Int = x.toInt

  // def bitops: List[Int] = List(x& a, x% a)

  def arith: List[Float] =
    List(x*a,
      x-a,
      x+a,
      // x / a,
      -x)

  def div: Float = {
    require(a != 0)
    x * a
  }

 def comp: List[Boolean] =
    List(x == a, x != a,  x < a, x <= a, x > a, x >= a)
 */
}

[saraswat]

Short works.

Where works means: no traceback, VCs are generated and checked. (May fail for divide by zero.)

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

import stainless.collection.List
// This does not work in stainless

case class CheckFloat(x: Short, a:Short) {

    def i: Int = x.toInt

    def bitops: List[Int] = List(x& a, x% a)

    def arith: List[Int] =
      List(x*a,
        x-a,
        x+a,
        // x / a,
        -x)

    def div: Int = {
      require(a != 0)
      x / a
    }

   def comp: List[Boolean] =
      List(x == a, x != a,  x < a, x <= a, x > a, x >= a)

}

[samarion]

There's unfortunately no support for floating-point arithmetic in Stainless. I don't think there's any technical reason to not have it, but rather it wasn't clear what (or how) you would want to provide as specifications for floating-point operations where error bounds and stability become more relevant.

In order to add support for Float, the main change would need to take place inside Inox. We would need to provide a FPType similarly to the BVType in Inox and add support for encoding floating-point operations in the various solver backends. Then, we would just need to extend Stainless code extraction to extract floating-point types similarly to how bitvector types (Long, Short, etc.) are extracted.

[saraswat]

Indeed, correctness for Float is an issue in its own right. However, when getting existing code to work in Stainless it is very valuable to even have a minimal level of support for classes such as Float-- no extra VCs are generated, just code with Float compiles in Stainless if it compiles in scalac (type-safety).

So I guess I see three levels of support:

• "Normal" Stainless support. Source code needs to be available. Stainless will check that methods terminate, check require, assert and ensuring clauses, check exhaustiveness of match statements, divide by zero and other runtime exceptions.
• "Pass through" (not a great phrase) support. Code may be available as byte code or source. Stainless only offers the guarantees of scalac. In particular, whether or not operations terminate is left up to the user to validate. Perhaps to ensure the user understands that they may introduce unsoundness in this way, have them mark the type in some way, e.g. @passthrough. (Exactly where to do this remains a question -- @extern does not work well because it is a point-of-use annotation, whereas we want a point-of-definition hook, or maybe point-of-import could work, or have them relabel using a type X = Y statement that is itself annotated. But such statements are not permitted at all places where import statements are... if possible I guess import statements should be annotated...)
• "Opaque" or "extern" support. Code may be available as byte code or source. Stainless considers these as opaque -- Stainless code cannot invoke any type-specific operations on an instance of this type.

Float should be in the "pass through" category. (It is possible to think of better static checks, but they are not yet developed; over time Float could move to "normal" support.)

[vkuncak]

@saraswat - this is something we have discussed endlessly but were not sure what to do beyond extern variants and adding things to our library. Why do you say @extern is point of use? It applies to declarations, no?

[saraswat]

(Re: @extern. I would like to be able to attach it to an import (#766) -- the place where a type is introduced into the system, rather than a place where it is used (as in a variable declaration or a method signature). Notice that Scala, like python, permits nested imports, this could actually be very useful. Most of my port right now consists of replacing import x.y.z with @exterrn type z = x.y.z. The problem with this is that I can't put type declarations everywhere I can put import statements, e.g. at the top-level of a file.

On this front, another improvement (#779) is to revisit parametrized types that use @extern types, i.e. you want two separate uses of the term Array[OrderT] to normalize to the same type Array[String] in the presence of an @extern type OrderT=String. I think currently what happens is something like Arrray[OrderT] becomes an Array[?] and of course two different Array[?] should not be treated the same. )

What do you think of the @passthrough above, which is roughly: you will only get the assurance that scalac gives you, we won't come in your way. (Right now, Stainless has only two modes, this could be a very valuable (in practice) third mode.) One could add more nuanced versions, e.g. letting the user declare that a procedure terminates. Of course it would be very valuable for Stainless to track the dependencies (cf truth/reason maintenance systems in problem solvers) on these assumptions and hence report out essentially conditional proofs: Assuming call x(y) terminates, these (assert, ensuring) predications hold.

From the purist's point of view, this is a step back. From the practitioner's point of view this is a huge step forward for it enables verification based tools to be used as a regular part of development practice.

[vkuncak]

Let's move this discussion to #766 and leave this for Float support, which we may decide to partly support directly at some point in the future (this is what we do for other types; it may require change to our internal evaluator/codegen, etc.)