Higher-order functions problem

[Nangos]

Hi All,

I recently met a problem when verifying with higher-order functions. It boils down to the following minimal example:

var f: int -> int;
assert seq(1, x => f(x))[0] == f(0);  // No problem
assert seq(1, f)[0] == f(0);  // Error: assertion might not hold

In the general case (especially when writing class methods), one would have to write x reads f.reads(x) requires f.requires(x) => f(x) in the place of f. This will be quite a boilerplate.

After some random attempts, I found an acceptable workaround:

// Seems like a mere identity function. What's going on here?
function magic<S, T>(f: S ~> T): (S ~> T) {
  x reads f.reads(x) requires f.requires(x) => f(x)
}

assert seq(1, magic(f))[0] == f(0);  // No problem now

I am still curious about what exactly is happening under the hood and whether there are more elegant ways to deal with this. Any suggestion is welcome.

[MikaelMayer]

Note that your code also works with the following simpler magic function:

function magic<S, T>(f: S -> T): (r: S -> T)
{
  x => f(x)
}

and now you can see why it's equivalent to the case when you explicitely use x => f(x) instead of f, because this is what this function is doing. If you were to replace the body of magic by just f, it would fail again. So you just moved the problem somewhere else.

Let's dive deep into the Boogie pool, which is the intermediate language in which Dafny compile. You can see such a file by running

dafny verify --bprint:filename.bpl filename.dfy

I did that, and under the hood, Dafny sends to Boogie the following axiom:

axiom (forall ty: Ty, heap: Heap, len: int, init: HandleType, i: int :: 
  { Seq#Index(Seq#Create(ty, heap, len, init), i) } 
  $IsGoodHeap(heap) && 0 <= i && i < len
     ==> Seq#Index(Seq#Create(ty, heap, len, init), i)
       == Apply1(TInt, ty, heap, init, $Box(i)));

I verified that this axiom could be instantiated correctly in the context of the assertion, and Boogie is able to prove that:

        assert $Unbox(Seq#Index(Seq#Create(TInt, $Heap, LitInt(1), f#0), LitInt(0))) ==
               $Unbox(Apply1(TInt, TSeq(TInt), $Heap, f#0, $Box(LitInt(0))));

However, assert seq(1, f)[0] == f(0); is translated to

        assert $Unbox(Seq#Index(Seq#Create(TInt, $Heap, LitInt(1), f#0), LitInt(0))): int
            == $Unbox(Apply1(TInt, TInt, $Heap, f#0, $Box(LitInt(0)))): int;

Note the subtle different, we can prove the assert when the second element is TSeq(TInt), but we want TInt
I'm not sure if one of them is incorrect. Need to investigate.

For the assertion that you can prove with x => f(x), it's because this lambda is wrapped in a Handle1 and Boogie has an axiom for that, the axiom you are looking for.

axiom (forall t0: Ty, 
    t1: Ty, 
    heap: Heap, 
    h: [Heap,Box]Box, 
    r: [Heap,Box]bool, 
    rd: [Heap,Box]Set Box, 
    bx0: Box, 
    bx: Box :: 
  { Reads1(t0, t1, heap, Handle1(h, r, rd), bx0)[bx] } 
  Reads1(t0, t1, heap, Handle1(h, r, rd), bx0)[bx] == rd[heap, bx0][bx]);

Thanks for pointing this verification incompleteness. I'll convert it to an issue.