Ensure function methods are efficient at runtime

[robin-aws]

Fair warning, this is one of my classic thinking out loud issues that may not be immediately actionable. :)

I'm glad that the majority of the function definitions in this repository are function methods, so that it is possible for consumers to use them at runtime if they so desire. As per the discussion in https://github.com/dafny-lang/dafny/issues/1492 this is definitely part of the contract of the definition, and it doesn't make sense for the language to support consumers making this decision instead.

However, runtime efficiency is not currently an explicit goal of these libraries, and yet there should be some very low-hanging fruit in terms of easy, classic functional programming optimizations. For example, Seq.FoldRight is not tail-recursive, so it could very easily lead to a stack overflow in several target languages: https://github.com/dafny-lang/libraries/blob/162c2a95198f8abd206fcf03cb3c56c672c479b9/src/Collections/Sequences/Seq.dfy#L698-L702

Besides actually improving the implementations here, we need to actually define where the sweet spot should be in terms of runtime efficiency, and add some actual mechanisms in the CI to ensure the expectations are met. This will be tightly coupled to the Dafny compiler and runtime implementations themselves, to ensure the idioms we encourage at least eventually lead to good runtime performance.

For example, repeatedly concatenating small sequences (as most of the functions in Seq.dfy do recursively) should be considered an efficient pattern. That is currently only the case when compiling to C# and Java, since they have lazy evaluation of sequence concatenation, but this should be a property of any runtime and therefore not a reason to make the Dafny code more complex to work around it (such as by defining a List<T> = Nil | Cons(car: T, cdr: List<T>) datatype to use instead).

[seebees]

Yes, this is great. I think that this standard library should take on two "goals". First, provide simple useful composable tools that people can use. Second, provide clear patterns for Dafny developers to use in their libraries.

This second goal is how I see this particular issue playing out. Because having efficient implementations across runtimes is something every developer will care about!

[robin-aws]

For the record the second goal requires some nuance - we already determined that not everything the standard library do should be imitated without question, e.g. https://github.com/dafny-lang/libraries/issues/17

[parno]

In our projects, we explicitly separate out our trusted specification code from our verified implementation code and proofs. The goal is that a human should only need to look at the specification code to decide if they want to trust the system. For that to be a reasonable task (more reasonable than manually inspecting unverified code), we want our functional specifications to be as small, simple, and concise as possible. Adding complexity for the sake of performance would undermine those goals. Of course, if there are two equally concise ways of expressing something, and one performs better than the other, then it doesn't hurt to choose the performant option. But in general, I think that if you care about performance, it's better to have an implementation dedicated to it and prove that it's functionally correct.

[robin-aws]

That's a good point @parno, and I agree I wouldn't want to sacrifice clarity for performance. Would you consider my example of ensuring tail recursion too much of a sacrifice then?

We recently added a new feature called "function by method" for the (pending) 3.3 release of Dafny that I think is perfect for letting us have our cake and eat it too here. It allows you to declare a function that has an alternate method definition when compiled, which must be verified to be equivalent. For example:

function {:opaque} FoldRight<A,T>(f: (T, A) -> A, s: seq<T>, init: A): A {
  if |s| == 0 then init
  else f(s[0], FoldRight(f, s[1..], init))
} 
by method {
  var result := init;
  for i := 0 to |s| {
    result := f(s[|s| - i - 1], result);
  }
  return result;
}

Note I made no effort to actually get this to verify: I get an error that the implicit post-condition that the result must equal FoldRight(f, s, init) might not hold.

If it's reasonable for the standard library to depend on 3.3, we could start using this feature.

[seebees]

I want to provide a way to package up the trusted specification and the verified implementation together. (I think?) Along with some way to ensure performance across runtimes. Both as a model for other projects, but also as a way to keep ourselves honest and our customers happy :)

As people use Dafny and compose things with the standard library, or their own, performance concerns will come up. If customers want to have absolute metal results then they should roll their own.

There is a big difference between "mostly fast" and "all fast".

So I'm not suggesting that we change things so that they are faster per se, but that we make sure that functions methods called at runtime are reasonably performant :)

[parno]

@robin-aws If the tail-recursive version of the function was equally clear, then I don't think that would be problematic. If it made the function less readable, then I think that optimization would go better in verified method, e.g., implemented via "by method".