Feat: 10 more implicit assertions made explicit

[MikaelMayer]

In the series of #3888 and #3890,
here is the first batch of implicit assertions made explicit by the proof obligation descriptions.

1. Unicity for let such that expressions
   

2. Existence for let such that expressions
   

3. Seq index out of range
   
   That also works for seq update expressions, like a(2)[i + 3 := 1]

4. Seq lower bound out of range
   Note the difference with the above: the upper comparison is "<=" and not "<"
   

5. Seq upper bound out of range
   

6. Array index out of range
   
   It works also for array2<int> and will output Length0 and Length1 as needed

7. Element not in domain
   

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[RustanLeino]

I love these!!

[codyroux]

YES!

[robin-aws]

I love how easy it is to add each new case.

Can you add some way of testing that GetAssertedExpr is consistent with the actual Boogie translation before the next batch?

[robin-aws]

Since you've added more cases, you should generalize this a bit! Perhaps say that several common assertion types are supported with more on the way, and mention what happens if one isn't supported (?)

[robin-aws]

More about the previous change, but can you add a comment to GetAssertedExpr in the supertype about whether the result needs to be resolved or not?

[MikaelMayer]

I love how easy it is to add each new case.
Can you add some way of testing that GetAssertedExpr is consistent with the actual Boogie translation before the next batch?

What I will do before the next batch is the following:

• I will change the way we add assertions so that we can add more assertions at the same time, and we can give it an expression translator
• I will add a flag for the ProofObligationDescription to tell whether the GetAssertedExpr should be a Dafny equivalent or an expression in Dafny that implies the asserted expression. I might do this step lazily if necessary.
• If an option is set (e.g. options.TestCodeActions) and we are adding an assert "BoogieExpr" whose proof obligation description has a non-null expression E from GetAssertedExpr(), then we will translate it using the expression translator, and add one more assertion that verifies that expressionTranslator(E) <==> BoogieExpr (or ==> if it should just imply it)

Sound like a good plan?

Note that I already encountered cases where <==> is true but boogie cannot prove it, so we might have false negatives even with testing.
For example:

predicate P(x: int)
 
function Test(x: int, z: int): int
  requires P(z) && x <= z
{
  var b, c :| x <= b && P(c); // Cannot prove unicity
  b
}

The inserted Dafny expression is

assert forall b: int, c: int, b': int, c': int | x <= b && P(c) && x <= b' && P(c') :: b == b' && c == c';

However, Boogie cannot use it to prove unicity as it cannot find a trigger that covers all quantified variables, so it ends up trying to prove a similar forall statement. (if you were to duplicate this assert forall, the second one could not be proved either)

[robin-aws]

That sounds great and pretty much what I imagined as well. If we do need something like options.TestCodeActions we should make it internal-only though.

I think we should stick to only equivalent expressions (<==>) rather than allow stronger ones (==>) - I expect users will occasionally be confused if a stronger version is not actually true and they can't make it verify. If your intention is to have simpler expressions so the extra assertion can be proven in the testing strategy you suggest, I'd prefer a way to allow-list expressions that don't prove in the testing harness instead.

[robin-aws]

Out of scope for this PR, but I think we should mention this feature in the readme for https://github.com/dafny-lang/ide-vscode too! And in the details of the extension (if that isn't automatically the same content)

[robin-aws]

❤️

[MikaelMayer]

That sounds great and pretty much what I imagined as well. If we do need something like options.TestCodeActions we should make it internal-only though.

I think we should stick to only equivalent expressions (<==>) rather than allow stronger ones (==>) - I expect users will occasionally be confused if a stronger version is not actually true and they can't make it verify. If your intention is to have simpler expressions so the extra assertion can be proven in the testing strategy you suggest, I'd prefer a way to allow-list expressions that don't prove in the testing harness instead.

Problem.

Here is the result of my first experience. For the code and when trying to prove only the equivalence between the two

predicate P(x: int, c: int)
 
function Test(x: int, z: int): int
  requires P(x, z) && x <= z
{
  var b, c :| x <= b && P(b, c); // Here
  b
}

the Dafny-generated assertion is

forall b: int, c: int, b': int, c': int | x <= b && P(b, c) && x <= b' && P(b', c') :: b == b' && c == c'

Here is the code Boogie generates

havoc b#7;
        havoc c#7;
        if (true)
        {
            if (x#0 <= b#7)
            {
                ##x#3 := b#7;
                // assume allocatedness for argument to function
                assume $IsAlloc(##x#3, TInt, $Heap);
                ##c#3 := c#7;
                // assume allocatedness for argument to function
                assume $IsAlloc(##c#3, TInt, $Heap);
                assume _module.__default.P#canCall(b#7, c#7);
            }
        }

        assert ((
              $Is(x#0, TInt)
               && $Is(LitInt(0), TInt)
               && 
              x#0 <= x#0
               && _module.__default.P(x#0, LitInt(0)))
             || 
            (
              $Is(LitInt(0), TInt)
               && $Is(LitInt(0), TInt)
               && 
              x#0 <= LitInt(0)
               && _module.__default.P(LitInt(0), LitInt(0)))
             || 
            (exists b#3: int :: 
              $Is(LitInt(0), TInt) && x#0 <= b#3 && _module.__default.P(b#3, LitInt(0)))
             || 
            (exists c#3: int :: 
              $Is(x#0, TInt) && x#0 <= x#0 && _module.__default.P(x#0, c#3))
             || 
            (exists c#3: int :: 
              $Is(LitInt(0), TInt) && x#0 <= LitInt(0) && _module.__default.P(LitInt(0), c#3))
             || (exists b#3: int, c#3: int :: x#0 <= b#3 && _module.__default.P(b#3, c#3)))
           == (exists b#3: int, c#3: int :: x#0 <= b#3 && _module.__default.P(b#3, c#3));
        assume (
            $Is(x#0, TInt)
             && $Is(LitInt(0), TInt)
             && 
            x#0 <= x#0
             && _module.__default.P(x#0, LitInt(0)))
           || 
          (
            $Is(LitInt(0), TInt)
             && $Is(LitInt(0), TInt)
             && 
            x#0 <= LitInt(0)
             && _module.__default.P(LitInt(0), LitInt(0)))
           || 
          (exists b#3: int :: 
            $Is(LitInt(0), TInt) && x#0 <= b#3 && _module.__default.P(b#3, LitInt(0)))
           || 
          (exists c#3: int :: 
            $Is(x#0, TInt) && x#0 <= x#0 && _module.__default.P(x#0, c#3))
           || 
          (exists c#3: int :: 
            $Is(LitInt(0), TInt) && x#0 <= LitInt(0) && _module.__default.P(LitInt(0), c#3))
           || (exists b#3: int, c#3: int :: x#0 <= b#3 && _module.__default.P(b#3, c#3));
        assume true;
        assume x#0 <= b#7 && _module.__default.P(b#7, c#7);
        havoc b#8;
        havoc c#8;
        assume true;
        assume x#0 <= b#8 ==> _module.__default.P#canCall(b#8, c#8);
        assume x#0 <= b#8 && _module.__default.P(b#8, c#8);
        assume true;
        assert (b#7
           == b#8)
           || !(forall b#3: int, c#3: int, b'#0: int, c'#0: int :: 
            x#0 <= b#3
                 && _module.__default.P(b#3, c#3)
                 && 
                x#0 <= b'#0
                 && _module.__default.P(b'#0, c'#0)
               ==> b#3 == b'#0 && c#3 == c'#0);

TL;DR Boogie is not proving a forall statement. It's already creating variables, assuming the range, and try to prove that the variables are equal.
Hence, because we can't access these Boogie variables, Boogie cannot obviously prove the equivalence there.
Note that if I replace the middle "==" on the last assertion by a left implicitation "<==", then Boogie can prove it.

Thus, at this point, I think I have to enable implication and not equivalence.

Boogie can prove the implication from right to left without problem.