Introduce support for closures

[stefanomil]

This PR introduces support for closure verification in Gobra.

The new primitives are:

• Function literals, that can capture variables and can be assigned to another variable. They are treated as expressions with function type. Example:

     x@ := 0
     c := preserves acc(&x)
            ensures x == old(x) + n && m == x
            func f(n int) (m int) {
                  x += n;
                  return x
            }

• Function and method objects, operands with function types obtained from functions or methods. They can be assigned to variables and treated as closures. For example, assuming there exist function f1 and method SomeStruct.m1, one can write c := f1 or c := SomeStruct{...}.m1.

• Closure spec instances, entities that use existing functions or function literals, in combination with 0 or more parameters, to express properties of closures. For examples, assume that there exists function (or literal) func fsp(n int, m bool) (r int). The possible closure spec instances are fsp, fsp{2}, fsp{m: true}, fsp{2, true}, which have respective types func(int, bool)int, func(bool)int, func(int)int, func()int. Each parameter is associated with one argument of the base function.

• Implementation assertions, which assert that a closure implements a particular spec. Example: c implements fsp{m: true}. This means that it can be called assuming the preconditions of fsp, and ensuring the postconditions of fsp.

• Calls with spec, which allow to call a closure using some spec that we know it implements. Example: c(3) as fsp{m: true}. For the purposes of verification, this is equivalent to calling fsp(3, true), with the additional precondition that c implements fsp{m: true}.

• Closure spec implementation proofs, that allow to verify that a closure implements a certain spec. Example:

proof c implements fsp{m: true} {
     [fold, unfold]
     r = c(n) as f
     [fold, unfold]
}

The proof verifies if, assuming the preconditions of fsp and assigning value true to the argument m, it's possible to establish the preconditions of f and, after the call, the postconditions of fsp are established. After this statement, the assertion c implements fsp{m: true} holds.

Spec implementation proofs can also be used with function or method objects. In this case, the call in the proof can be a normal function/method invocation. For example, assuming f1 is a function, we can write (if the type of the function matches the type of the spec):

proof f1 implements fsp{3} {
   ...
   r = f1(m)
   ...
}

From now on f1 implements fsp{3} holds and it's possible to call f1(_) as fsp{3}. Similarly for methods.

[Felalolf]

I think your suggestion is ok. @jcp19 At some point, we should unify the nodes, e.g. something like:

sealed trait CallBase
case class FunctionBase(func: FunctionProxy) extends CallBase
case class MethodBase(recv: Expr, meth: MethodProxy) extends CallBase
case class ClosureBase(closure: Expr, spec: ClosureSpec) extends CallBase

sealed trait Call extends Node
case class CallStmt(targets: Vector[LocalVar], base: CallBase, args: Vector[Expr])(val info: Source.Parser.Info) extends Call with Stmt
case class CallExpr(base: CallBase, args: Vector[Expr])(val info: Source.Parser.Info) extends Call with Expr

case class Go(call: Call)(val info: Source.Parser.Info) extends Stmt

[Felalolf]

I looked at the encoding files. I have some comments, but overall looks quite positive. You definitely need more documentation. I still need to review the desugarer and the encoding parts (after you add documentation).

[jcp19]

Some minor comments

[Felalolf]

I have now looked at everything. I have a few more comments, but nothing should be particularly big. After my comments are addressed, I think we can merge it and then do later changes in new pull requests. Some parts in the ghost checker seem odd, but I have the impression that the fault lies with how we have handled interface implementation proofs so far.

[stefanomil]

@Felalolf I have now addressed all of the comments

[jcp19]

Looking at the tests, it looks like the warning that closures are an experimental feature is being printed on every test, even those that do not use the feature at all - this suggests that the closure encoding is always generated, regardless of whether it is used. Could we generate the closures' viper code only when we need them?

[stefanomil]

@jcp19 @Felalolf The Closure domain is now only generated only if it is used