Incompleteness with the closure encoding

[jcp19]

In Scion, I have a program of the following form:

func (d *DataPlane) Run() {
    read /*@@@*/ :=
		// spec hidden
		func /*@ rc @*/ (ingressID uint16, rd BatchConn) {
                    // ...
                }
    cl := 
        // @ requires acc(&read, _) && read implements rc
        func /*@ closure1 @*/ (c BatchConn) {
                // @ assert read implements rc
		read(0, c) //@ as rc // (*)
	}
   go cl(d.internal) // @ as rc
}

Unfortunately, the call to read in (*) fails with the following perplexing error

Error at: </Users/joao/code/VerifiedSCION/router/dataplane.go:1046:5> Precondition of call read(0, c) as rc might not hold. 
read might not implement rc.

Note that this precondition is asserted immediately before the call. Looking at the generated Viper code reveals the failing precondition (marked in blue):

The problem is that, at the source program level, there is no way to write a term that encodes to closureGet$rc_Run_80c2a36d_F0(d_V0_RN3), except for the allocation of a closure.

[jcp19]

This could be addressed in tandem with #713

[jcp19]

Minimal example:

package closure_err

func f() {
	i@ := 0
	x@ :=
		preserves acc(&i) 
		func x1() {
			i += 1
		}
	g :=
		requires acc(&x, _)
		requires x implements x1
		preserves acc(&i)  
		func g1() {
			x() as x1
		}
}

[Felalolf]

From my perspective, this is a design problem and not a problem of the encoding. Function literal names are not full specifications because the captured variables are missing. As a consequence, you cannot call a closure with the function literal contract outside of the immediate context. To call the closure inside of another closure, you have to give the called closure a proper specification:

ghost
preserves acc(i)
decreases _
func xSpec(ghost i *int)

func f() {
	i@ := 0
	x@ :=
		preserves acc(&i)
		decreases _
		func x1() {
			i += 1
		}

   ghost pi := &i // for some reason, typechecker complains about &i in the next line

	proof x implements xSpec{pi} {
	    x() as x1
	}

	g :=
		requires acc(&x, _)
		requires x implements xSpec{&i}
		preserves acc(&i)
		func g1() {
			x() as xSpec{&i}
		}

    assert g != nil
}

Admittedly, doing it as shown above is more verbose than referring to the x1 directly.

I see two points:

1. Currently, x implements x1 should be rejected to avoid misunderstandings. Its current encoding is not incorrect, but also not useful.
2. As an improvement, we could make function literal names a full specification within the scope of the captured variables (by statically inferring the captured variables). That means that x implements x1 is ok within the scope of the literal definition. x implements x1 could then be encoded to the getClosure expression or an implements expression with an additional argument. In both cases, the captured variables are inferred statically.

[Felalolf]

I though about is bit more. I am not completely sure whether the following approach works, but I wanted to document it for now:

Currently, captured variables are encoded via uninterpreted getters. If captured variables are only encoded in implements expressions and calls for function literals, then instead of using uninterpreted getters, we might be able to just use the captured variable dircectly. The reasoning is that implements expressions and call for function literals can only happen in the scope of the function literal, which should be the same scope of the captured variables.

This requires (1) a careful naming scheme in the desugared representation such that captured variable parameters always have the same name for the same captured variable and (2) that x implements x1 is encoded to something with the captured variable as a parameter.

One challenge of the encoding is that how captured variables are replaced in different within a closure and outside a closure. Inside a closure, the captured variable is some paramter. Outside a closure, the captured variable is a reference to some parameter. At the Viper level, both are encoded to the same, namely just the variable. One solution might be to always use an exclusive variable with the pointer type, even outside of closures. Unless I am missing something, an exclusive variable with a pointer type should be translated correctly outside of the closure because the encoding does not check whether a variable with the same type was actually defined (which does not hold because the actual variable has the element type of the pointer type).