Missing export-provides causes crash

[RustanLeino]

Dafny version

4.11

Code to produce this issue

module Library {
  export
    reveals Base
    // The following line is required. Not including the line ought to give some
    // kind of resolution error. But instead, Dafny generates malformed Boogie and
    // crashes.
    //
    // provides Base.Get

  trait {:termination false} Base extends object {
    function Get(): int
  }
}

module Client {
  import Library
    
  class MyClass extends Library.Base {
    constructor () { }
    function Get(): int { 5 }
  }
}

Command to run and resulting output

% dafny verify test.dfy

Encountered internal compilation exception: Boogie program had 4 resolution errors:
Microsoft.Dafny.SourceOrigin: use of undeclared function: Library.Base.Get
Microsoft.Dafny.SourceOrigin: use of undeclared function: Library.Base.Get#canCall
Microsoft.Dafny.SourceOrigin: use of undeclared function: Library.Base.Get#canCall
Microsoft.Dafny.SourceOrigin: use of undeclared function: Library.Base.Get
test.dfy(15,4): Error: Internal error occurred during verification: Boogie program had 4 resolution errors:
 Microsoft.Dafny.SourceOrigin: use of undeclared function: Library.Base.Get
 Microsoft.Dafny.SourceOrigin: use of undeclared function: Library.Base.Get#canCall
 Microsoft.Dafny.SourceOrigin: use of undeclared function: Library.Base.Get#canCall
 Microsoft.Dafny.SourceOrigin: use of undeclared function: Library.Base.Get
    at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
    at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken) in $DAFNY/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs:line 65
    at Microsoft.Dafny.Compilation.<>c__DisplayClass60_1.<<VerifyUnverifiedSymbol>b__1>d.MoveNext() in $DAFNY/Source/DafnyCore/Pipeline/Compilation.cs:line 371
 --- End of stack trace from previous location ---
    at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed) in $DAFNY/Source/DafnyCore/Pipeline/Compilation.cs:line 370
    at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed) in $DAFNY/Source/DafnyCore/Pipeline/Compilation.cs:line 370
    at DafnyDriver.Commands.CliCompilation.VerifyAllLazily(Nullable`1 randomSeed)+MoveNext() in $DAFNY/Source/DafnyDriver/CliCompilation.cs:line 274
   |
15 |     constructor () { }
   |     ^^^^^^^^^^^^^^^^^^

Unhandled exception. System.ArgumentException: Boogie program had 4 resolution errors:
Microsoft.Dafny.SourceOrigin: use of undeclared function: Library.Base.Get
Microsoft.Dafny.SourceOrigin: use of undeclared function: Library.Base.Get#canCall
Microsoft.Dafny.SourceOrigin: use of undeclared function: Library.Base.Get#canCall
Microsoft.Dafny.SourceOrigin: use of undeclared function: Library.Base.Get
   at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken) in $DAFNY/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs:line 65
   at Microsoft.Dafny.Compilation.<>c__DisplayClass60_1.<<VerifyUnverifiedSymbol>b__1>d.MoveNext() in $DAFNY/Source/DafnyCore/Pipeline/Compilation.cs:line 371
--- End of stack trace from previous location ---
   at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed) in $DAFNY/Source/DafnyCore/Pipeline/Compilation.cs:line 370
   at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed) in $DAFNY/Source/DafnyCore/Pipeline/Compilation.cs:line 370
   at DafnyDriver.Commands.CliCompilation.VerifyAllLazily(Nullable`1 randomSeed)+MoveNext() in $DAFNY/Source/DafnyDriver/CliCompilation.cs:line 274
   at DafnyDriver.Commands.CliCompilation.VerifyAllLazily(Nullable`1 randomSeed)+System.Threading.Tasks.Sources.IValueTaskSource<System.Boolean>.GetResult()
   at System.Linq.AsyncEnumerable.ToObservableObservable`1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext() in /_/Ix.NET/Source/System.Linq.Async/System/Linq/Operators/ToObservable.cs:line 50
--- End of stack trace from previous location ---
   at System.Reactive.PlatformServices.ExceptionServicesImpl.Rethrow(Exception exception) in /_/Rx.NET/Source/src/System.Reactive/Internal/ExceptionServicesImpl.cs:line 16
   at System.Reactive.ExceptionHelpers.Throw(Exception exception) in /_/Rx.NET/Source/src/System.Reactive/Internal/ExceptionServices.cs:line 14
   at System.Reactive.Stubs.<>c.<.cctor>b__2_1(Exception ex) in /_/Rx.NET/Source/src/System.Reactive/Internal/Stubs.cs:line 16
   at System.Reactive.AnonymousObserver`1.OnErrorCore(Exception error) in /_/Rx.NET/Source/src/System.Reactive/AnonymousObserver.cs:line 73
   at System.Reactive.ObserverBase`1.OnError(Exception error) in /_/Rx.NET/Source/src/System.Reactive/ObserverBase.cs:line 59
   at System.Reactive.Subjects.Subject`1.OnError(Exception error) in /_/Rx.NET/Source/src/System.Reactive/Subjects/Subject.cs:line 103
   at System.Linq.AsyncEnumerable.ToObservableObservable`1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext() in /_/Ix.NET/Source/System.Linq.Async/System/Linq/Operators/ToObservable.cs:line 60
--- End of stack trace from previous location ---
   at System.Linq.AsyncEnumerable.ToObservableObservable`1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext() in /_/Ix.NET/Source/System.Linq.Async/System/Linq/Operators/ToObservable.cs:line 74
--- End of stack trace from previous location ---
   at System.Threading.Tasks.Task.<>c.<ThrowAsync>b__128_1(Object state)
   at System.Threading.ThreadPoolWorkQueue.Dispatch()
   at System.Threading.PortableThreadPool.WorkerThread.WorkerThreadStart()
   at System.Threading.Thread.StartCallback()

What happened?

Both Library.Base and Client.MyClass are declaring a function Get(). If module Library had exported this member, then it would be clear that Client.MyClass is intending to override that member. However, since Library is not exporting that member, module Client doesn't actually know if it needs to export such a member or not, or whether or not its declared Get member is a new member or is overriding something in the trait parent.

In other situations where a client is trying to access a non-exported item in an imported module, Dafny (peeks into the imported module and notices that there is actually such a member, but it isn't exported, and then) gives a friendly error message to that effect. The same ought to happen for the program above. That is, when Dafny performs the check that MyClass is implementing all things left un-implemented in the trait parent, then Dafny also ought to check if the parent member is visible to the client. If it is not, Dafny could produce an error message like

class 'MyClass' implements trait function 'Base.Get', but this function
is not exported by module `Library`; to fix this problem, export the
function from module `Library`

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

Mac