Fix least lemma IDE verification bug and add test (#4607)

### Changes
Allow least lemmas to be verified in the IDE

### Testing
Added XUnit test

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs

@@ -21,6 +21,17 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization {
  public class DiagnosticsTest : ClientBasedLanguageServerTest {
  private readonly string testFilesDirectory = Path.Combine(Directory.GetCurrentDirectory(), "Synchronization/TestFiles");
 
+ [Fact]
+ public async Task LeastLemmaIsVerified() {
+ var source = @"
+least lemma Foo()
+ ensures false
+{}";
+ var document = await CreateOpenAndWaitForResolve(source);
+ var diagnostics = await GetLastDiagnostics(document);
+ Assert.NotEmpty(diagnostics);
+ }
+
  [Fact(Skip = "Not implemented. Requires separating diagnostics from different sources")]
  public async Task FixedParseErrorUpdatesBeforeResolution() {
  var source = @"

Source/DafnyLanguageServer/Workspace/CompilationManager.cs

@@ -160,10 +160,6 @@ public async Task<bool> VerifySymbol(FilePosition verifiableLocation, bool onlyP
  cancellationSource.Token.ThrowIfCancellationRequested();
 
  var compilation = await ResolvedCompilation;
- var verifiable = compilation.Program.FindNode<ICanVerify>(verifiableLocation.Uri, verifiableLocation.Position.ToDafnyPosition());
- if (verifiable == null) {
- return false;
- }
 
  if (compilation.ResolutionDiagnostics.Values.SelectMany(x => x).Any(d =>
  d.Level == ErrorLevel.Error &&
@@ -172,6 +168,21 @@ public async Task<bool> VerifySymbol(FilePosition verifiableLocation, bool onlyP
  throw new TaskCanceledException();
  }
 
+ var verifiable = compilation.Program.FindNode(verifiableLocation.Uri, verifiableLocation.Position.ToDafnyPosition(),
+ node => {
+ if (node is not ICanVerify) {
+ return false;
+ }
+ // Sometimes traversing the AST can return different versions of a single source AST node,
+ // for example in the case of a LeastLemma, which is later also represented as a PrefixLemma.
+ // This check ensures that we consistently use the same version of an AST node. 
+ return compilation.Verifiables!.Contains(node);
+ }) as ICanVerify;
+
+ if (verifiable == null) {
+ return false;
+ }
+
  var containingModule = verifiable.ContainingModule;
  if (!containingModule.ShouldVerify(compilation.Program.Compilation)) {
  return false;

docs/dev/news/4607.fix

@@ -0,0 +1 @@
+Fix a bug that prevented certain types of lemma to be verified in the IDE