function transparency vs isolate-assertions vs split_here

[hmijail]

Dafny version

4.7

Code to produce this issue

const C1 : int := 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000
const C2: int := C1 - 1

type T1 = i:nat | i <= 1
type T2 = n:nat | n < 256
type T3 = i:int | 0 <= i <= C2

type T4 = seq<T3> 
type T5 = seq<T1> 
type T6 = seq<T2> 

datatype D = D(
        F1: T4,
        F2: T4,
        F3: T4,
        F4: T5,
        F5: T5,
        F6: T5,
        F7: T5,
        F8: T4,
        F9: T5,
        F10: T4,
        F11: T6)
    {
        predicate wellFormed()
        {
            (0 < |F1| == |F2| == |F3| 
             == |F4| == |F5| 
             == |F6| == |F7| == |F8| == |F9|
             == |F10| == |F11| 
             )
        }
    }

opaque predicate P(t: D)
requires t.wellFormed()
{
    && (forall i:nat | 7<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> (128 * t.F6[i-7] as nat) + (64 * t.F6[i-6] as nat) + (32 * t.F6[i-5] as nat) + (16 * t.F6[i-4] as nat) + (8 * t.F6[i-3] as nat) + (4 * t.F6[i-2] as nat) + (2 * t.F6[i-1] as nat) + t.F6[i] as nat == t.F11[i] as nat)
    // $$ assert {:split_here} true;
    && (forall i:nat | 15<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F10[i] as nat == (128 * t.F6[i-15] as nat) + (64 * t.F6[i-14] as nat) + (32 * t.F6[i-13] as nat) + (16 * t.F6[i-12] as nat) + (8 * t.F6[i-11] as nat) + (4 * t.F6[i-10] as nat) + (2 * t.F6[i-9] as nat) + t.F6[i-8] as nat)
    // $$ assert {:split_here} true;
    && (forall i:nat | 3<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F8[i] as nat == (8 * t.F6[i-3] as nat) + (4 * t.F6[i-2] as nat) + (2 * t.F6[i-1] as nat) + t.F6[i] as nat)
    && (forall i:nat | 4<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F7[i] == t.F6[i-4])
    && (forall i:nat | 15<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F9[i] == t.F6[i-15])
}

opaque predicate empty(t: D) 
{
	&& (1 == |t.F1|
		== |t.F2|
		== |t.F3|
		== |t.F4|
		== |t.F5|
		== |t.F6|
		== |t.F7|
		== |t.F8|
		== |t.F9|
		== |t.F10|
		== |t.F11|)
	&& (0 == t.F1[0] as nat
		== t.F2[0] as nat
		== t.F3[0] as nat
		== t.F4[0] as nat
		== t.F5[0] as nat
		== t.F6[0] as nat
		== t.F7[0] as nat
		== t.F8[0] as nat
		== t.F9[0] as nat
		== t.F10[0] as nat
		== t.F11[0] as nat)
}






lemma expensive(t: D) 
	requires empty(t) && t.wellFormed()
{
	reveal empty();
   	reveal P();
	assert P(t);
}

lemma cheap(t: D)
	requires empty(t) && t.wellFormed()
{
	reveal empty();
   	
	assert P1(t);
}


 predicate P1(t: D)
requires t.wellFormed()
{
    && P2(t)
	&& P3(t)
	&& P4(t)
}


 predicate P2(t: D)
requires t.wellFormed()
{
    (forall i:nat | 7<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> (128 * t.F6[i-7] as nat) + (64 * t.F6[i-6] as nat) + (32 * t.F6[i-5] as nat) + (16 * t.F6[i-4] as nat) + (8 * t.F6[i-3] as nat) + (4 * t.F6[i-2] as nat) + (2 * t.F6[i-1] as nat) + t.F6[i] as nat == t.F11[i] as nat)

}

 predicate P3(t: D)
requires t.wellFormed()
{ 
    (forall i:nat | 15<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F10[i] as nat == (128 * t.F6[i-15] as nat) + (64 * t.F6[i-14] as nat) + (32 * t.F6[i-13] as nat) + (16 * t.F6[i-12] as nat) + (8 * t.F6[i-11] as nat) + (4 * t.F6[i-10] as nat) + (2 * t.F6[i-9] as nat) + t.F6[i-8] as nat)
}

 predicate P4(t: D)
requires t.wellFormed()
{ 
    && (forall i:nat | 3<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F8[i] as nat == (8 * t.F6[i-3] as nat) + (4 * t.F6[i-2] as nat) + (2 * t.F6[i-1] as nat) + t.F6[i] as nat)
    && (forall i:nat | 4<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F7[i] == t.F6[i-4])
    && (forall i:nat | 15<=i<|t.F1| :: (t.F3[i] == 15 && t.F4[i] as nat + t.F5[i] as nat == 1) ==> t.F9[i] == t.F6[i-15])
}

Command to run and resulting output

dafny verify example.dfy --resource-limit 10000000

What happened?

Consider the function expensive(). Its verification times out with over 50M Resource Units. To try to tackle it, I tried using --isolate-assertions. Some of the resulting Assertion Batches still timed out over 50M.

Separately I tried manually breaking down expensive() into smaller functions, and then invoking them all inside of cheap(). Turns out that cheap() verifies with <200K RU - over 2 orders of magnitude better. But I don't understand what could cause such a big difference.

I understand that there is a degree of randomness here because of both how the Assertion Batches are constructed, and of what the solver might "discover" while working without isolated assertions. But apart from that, I wonder if I'm missing something more fundamental, hence these questions:

1. Given that these functions are transparent, shouldn't cheap() end up being equivalent to expensive()?
2. Given that --isolate-assertions breaks expensive() down to ABs, shouldn't the verification of those ABs be cheaper, rather similarly to what cheap() achieves?
3. --isolate-assertions is explained to work by asserting assertions one by one while assuming the previous ones. Now, imagine the case of a function that contains 10 Assertion Batches. The active assertion in AB 5 is false, but the solver times out before realizing. AB 6 will then effectively start with assume false, right? Therefore, will AB 6 (and subsequent ones) be "poisoned" by this?
4. P() shows a couple of commented-out && assert {:split_here} true that partition the function just like the smaller functions did for P1(). Indeed, this improves verification of P(). If the only reason to extract those smaller functions is to ease verification, is it then equivalent to use split_here?

What type of operating system are you experiencing the problem on?

Mac

[hmijail]

Question 3 is probably the most pressing, since that would affect the usefulness of --isolate-assertions and the strategies to use it.

[keyboardDrummer]

1. Given that these functions are transparent, shouldn't cheap() end up being equivalent to expensive()?

Your examples are bit large. Any chance you could simplify them to make it easier to answer your questions?

2. Given that --isolate-assertions breaks expensive() down to ABs, shouldn't the verification of those ABs be cheaper

Yes but only in general. There may still be one AB that is (almost) as expensive as the whole. I'm working on a PR that will hopefully make --isolate-assertions more effective though.

3. Question 3 is probably the most pressing, since that would affect the usefulness of --isolate-assertions and the strategies to use it.

Does the following example answer your question?

function Foo() {
  assert false; // Always fails
  assert false; // This assertion never fails because the previous one establishes false, 
  // regardless of whether you're using `--isolate-assertions` or not
}

4. P() shows a couple of commented-out && assert {:split_here} true that partition the function just like the smaller functions did for P1(). Indeed, this improves verification of P(). If the only reason to extract those smaller functions is to ease verification, is it then equivalent to use split_here?

Note that if you're already using --isolate-assertions, then adding splits shouldn't have any positive effect. Also, splits will only affect the verification where they are placed, so adding splits to functions will only makes verifying the wellformedness of that function easier, but won't affect callers of that function.

---

One more thing to note is that we're adding hide statements as an easier to use, and more performant version of {:opaque}: #5562

But it's still work on progress.

[hmijail]

Your examples are bit large. Any chance you could simplify them to make it easier to answer your questions?

What I posted here was already heavily minimized. I realize it's still off-puttingly big, but the behavior I described is very finicky and it seemed to disappear with further minimization.
I will try to minimize further, but does it help if I try to minimize the explanation, or turn it into pseudocode?

• there's an expensive function that contains 5 lines.
• there's a much cheaper function that contains those same 5 lines, only across smaller functions. Given that functions are transparent, why would cheap() cost less than expensive()?
• --isolate-assertions should be doing to expensive() something similar to what cheap() did. Yet the result is still very expensive. Any idea why?
  In pseudocode:

lemma expensive(t: D) 
{
	reveal empty();
   	reveal P();
	assert P(t);
}

opaque predicate P(t: D){
(5 lines)
}

lemma cheap(t: D)
{
	reveal empty();
	assert P1(t);
}

 predicate P1(t: D)
requires t.wellFormed()
{
    && P2(t)
	&& P3(t)
	&& P4(t)
}

Note that if you're already using --isolate-assertions, then adding splits shouldn't have any positive effect.

I understand that case; but if not using --isoloate-assertions, if the only reason to extract smaller functions is to ease verification, is it then equivalent to use split_here?

[keyboardDrummer]

there's a much cheaper function that contains those same 5 lines, only across smaller functions. Given that functions are transparent, why would cheap() cost less than expensive()?

I see, I don't understand the difference either. Sorry! It could be debugged by dropping to the Boogie level, but I'm afraid I don't have time for that now. One

--isolate-assertions should be doing to expensive() something similar to what cheap() did.

Note really. --isolate-assertions generates a separate VC for each assertion in a proof, but in both your lemma's there's only a single assertion, so I don't even see how --isolate-assertions would have an effect.