Counterexamples As Assumptions (#5013)

### Problem

Right now Dafny reports counterexamples using special syntax that may be
difficult to understand. For example, consider the following Dafny
program that defines a standard `List` datatype with a function `View`
that maps the list to a sequence of integers:

```Dafny
datatype Node = Cons(next:Node, value:int) | Nil {
  function View():seq<int> 
    ensures Cons? ==> |View()| > 0 && View()[0] == value && View()[1..] == next.View()
  {
    if Nil? then [] else [value] + next.View()
  }
}
```

Suppose we were to (incorrectly) assert that the list cannot correspond
to the sequence of integers `[1, 2, 3]`, like so:

```Dafny
method m(list:Node) {
  assert list.View() != [1, 2, 3];
}
```

Currently, Dafny would return the following counterexample: 

```
At "method m(list:Node) {" (file.dfy:20):
    list:Problem.Node = Cons(next := @0, value := 1)
    @0:Problem.Node = Cons(next := @2, value := 2)
    @2:Problem.Node = Cons(next := @4, value := 3)
    @4:Problem.Node = Nil
```

This counterexample is confusing because it does not explain what the
meaning of `@0`, `@1`, etc. is. The notation is different from the Dafny
syntax, and it also does not capture some of the information that is
actually contained within the counterexample because there is no way to
express this information using this custom syntax. In particular, the
counterexample constrains the value returned by calling `View()` on the
`list` variable. This constrain might be redundant in this particular
example but in general, we would want to capture all the information
contained in the counterexample.

### Solution

This PR redesigns the counterexample generation functionality so that
counterexamples are represented internally and can be printed as Dafny
assumptions. For example, for the program above, the counterexample will
now look like this:

```Dafny
assume Node.Cons(Node.Cons(Node.Cons(Node.Nil, 3), 2), 1) == list 
    && Node.Cons(Node.Cons(Node.Cons(Node.Nil, 3), 2), 1).View.requires() 
    && [1, 2, 3] == Node.Cons(Node.Cons(Node.Cons(Node.Nil, 3), 2), 1).View() 
    && Node.Cons(Node.Cons(Node.Nil, 3), 2).View.requires() 
    && [2, 3] == Node.Cons(Node.Cons(Node.Nil, 3), 2).View() 
    && Node.Cons(Node.Nil, 3).View.requires() 
    && [3] == Node.Cons(Node.Nil, 3).View() 
    && Node.Nil.View.requires() 
    && [] == Node.Nil.View();
```

While admittedly more verbose because it explores the return values of
functions, this counterexample precisely constrains the argument that
leads to the assertion violation. In particular, if you were to insert
this assumption into the code and revert the assertion, Dafny would
verify that this counterexample is correct.

At a high level, this makes the following changes:
1) Represent counterexamples as Dafny statements that the user can
insert directly into their code to debug the failing assertion.
2) Make sure the counterexamples are wellformed, i.e. the constraints
are ordered in such a way that the resulting assumption verifies.
3) Support counterexample constraints over function return values (as an
example of something that can really only be done using native Dafny
syntax)
4) Automatically fix counterexamples that are internally inconsistent,
when such an inconsistency can be easily detected. For instance, a
counterexample will never describe negative indices of an array or
sequence, call a set empty if it contains elements, etc. All of these
are possible in the counterexample model returned by Boogie but we prune
such inconsistencies before reporting the counterexample, when possible.


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

---------

Co-authored-by: Aleksandr Fedchin <[email protected]>
Co-authored-by: Aaron Tomb <[email protected]>

Source/DafnyCore/CounterExampleGeneration/DafnyModelTypeUtils.cs

@@ -1,5 +1,6 @@
 // Copyright by the contributors to the Dafny Project
 // SPDX-License-Identifier: MIT
+#nullable enable
 
 using System;
 using System.Linq;
@@ -28,7 +29,9 @@ public static Type GetNonNullable(Type type) {
  }
 
  public static Type ReplaceTypeVariables(Type type, Type with) {
- return ReplaceType(type, t => t.Name.Contains('$'), _ => with);
+ var result = ReplaceType(type, t => t.Name.Contains('$'), _ => with);
+ FillInTypeArgs(result, with);
+ return result;
  }
 
  /// <summary>
@@ -61,6 +64,8 @@ public static Type GetInDafnyFormat(Type type) {
  // The code below converts every "__" to "_":
  newName = UnderscoreRemovalRegex.Replace(newName, "_");
  newName = ConvertTupleName(newName);
+ newName = string.Join(".", newName.Split(".")
+ .Where(part => part != "_module" && part != "_default" && part != "_System"));
  return new UserDefinedType(new Token(), newName,
  type.TypeArgs.ConvertAll(t => TransformType(t, GetInDafnyFormat)));
  }
@@ -82,15 +87,15 @@ private static Type TransformType(Type type, Func<UserDefinedType, Type> transfo
  switch (type) {
  case BasicType:
  return type;
- case MapType mapType:
+ case MapType mapType when mapType.HasTypeArg():
  return new MapType(mapType.Finite,
  TransformType(mapType.Domain, transform),
  TransformType(mapType.Range, transform));
- case SeqType seqType:
+ case SeqType seqType when seqType.HasTypeArg():
  return new SeqType(TransformType(seqType.Arg, transform));
- case SetType setType:
+ case SetType setType when setType.HasTypeArg():
  return new SetType(setType.Finite, TransformType(setType.Arg, transform));
- case MultiSetType multiSetType:
+ case MultiSetType multiSetType when multiSetType.HasTypeArg():
  return new MultiSetType(TransformType(multiSetType, transform));
  case UserDefinedType userDefinedType:
  return transform(userDefinedType);
@@ -101,5 +106,33 @@ private static Type TransformType(Type type, Func<UserDefinedType, Type> transfo
  }
  return type;
  }
+
+ /// <summary>
+ /// Whenever a collection type does not have an argument, fill it in with the provided arg type
+ /// </summary>
+ private static void FillInTypeArgs(Type type, Type arg) {
+ switch (type) {
+ case BasicType:
+ return;
+ case MapType mapType when !mapType.HasTypeArg():
+ mapType.SetTypeArgs(arg, arg);
+ return;
+ case SeqType seqType when !seqType.HasTypeArg():
+ seqType.SetTypeArg(arg);
+ return;
+ case SetType setType when !setType.HasTypeArg():
+ setType.SetTypeArg(arg);
+ return;
+ case MultiSetType multiSetType when !multiSetType.HasTypeArg():
+ multiSetType.SetTypeArg(arg);
+ return;
+ case UserDefinedType userDefinedType:
+ userDefinedType.TypeArgs.ForEach(typ => FillInTypeArgs(typ, arg));
+ return;
+ case InferredTypeProxy inferredTypeProxy:
+ FillInTypeArgs(inferredTypeProxy.T, arg);
+ return;
+ }
+ }
  }
 }