Malformed Boogie in match inside forall

[RustanLeino]

trafficstars

Dafny version

4.10

Code to produce this issue

datatype Instr = Branch(m: nat)

predicate WellTyped(ii: seq<Instr>, typing: seq<nat>) {
  forall pc :: 0 <= pc < |ii| ==>
    match ii[pc]
    case Branch(n) =>
      typing[pc + n] == typing[pc]
}

Command to run and resulting output

dafny verify test.dfy

What happened?

Dafny crashes:

% dafny verify test.dfy
Encountered internal compilation exception: Boogie program had 7 resolution errors:
Microsoft.Dafny.SourceOrigin: undeclared identifier: n#0
Microsoft.Dafny.SourceOrigin: undeclared identifier: n#0
Microsoft.Dafny.SourceOrigin: undeclared identifier: n#0
Microsoft.Dafny.SourceOrigin: undeclared identifier: n#0
Microsoft.Dafny.SourceOrigin: undeclared identifier: n#0
Microsoft.Dafny.SourceOrigin: undeclared identifier: n#0
Microsoft.Dafny.SourceOrigin: undeclared identifier: n#0

Looking at the Boogie generated, I get the following impression. Trigger generation introduces a new variable _t#0#2 with the meaning _t#0#2 == pc#3 + n#0. Clearly, n#0 stems from the bound variable in the pattern Branch(n). Such patterns are rewritten during the desugaring of match expressions. But something loses the connection between this use of n#0 and the fact that n#0 is supposed to equal ii[pc].m.

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

Mac

[keyboardDrummer]

The loop detection code produces the following incorrect Dafny code:

predicate WellTyped(ii: seq<Instr>, typing: seq<nat>)
  decreases ii, typing
{
  forall pc: int, _t#0: int {:trigger typing[pc], typing[_t#0]} {:trigger typing[_t#0], ii[pc]} | _t#0 == pc + n :: 
    0 <= pc &&
    pc < |ii| ==>
      match ii[pc] case Branch(n: int) => typing[_t#0] == typing[pc]
}

note that n is used before it is defined.

typing[pc + n] is detected as causing a matching loop, and that's why pc + n is extracted into a new quantified variable.

explanation:

    // rewrite quantifier to avoid matching loops
    // before:
    //    assert forall i :: 0 <= i < a.Length-1 ==> a[i] <= a[i+1];
    // after:
    //    assert forall i,j :: j == i+1 ==> 0 <= i < a.Length-1 ==> a[i] <= a[j];

I don't know this logic well enough to decide how to proceed. The creation of a new quantified variable seems quite aggressive to me.

In Dafny 3.10, in this case it would not do the above refactoring, and would produce:

predicate WellTyped(ii: seq<Instr>, typing: seq<nat>)
  decreases ii, typing
{
  forall pc: int {:trigger ii[pc]} :: 
    0 <= pc &&
    pc < |ii| ==>
      match ii[pc] { case Branch(_mcc#0: nat) => var n: nat := _mcc#0; typing[pc + n] == typing[pc] }
}

because for some reason I do not understand, it would look for the subexpression pc + _mcc#0 instead of pc + n, and thus not find it.

One thing we could do is check whether all parts of the lifted expression, pc + n in the above case, are free in the quantifier body, and if not, do not do the lifting.