Dafny fails to verify very long line

[seebees]

Dafny version

4.9.0

Code to produce this issue

Command to run and resulting output

What happened?

This file has very long Base64 strings
https://github.com/aws/aws-encryption-sdk/blob/de9f7fec7e905c3781aade7219e4db18a4a00618/TestVectors/dafny/TestVectors/test/Fixtures.dfy

When trying to verify in the PR:
aws/aws-encryption-sdk#742

I get the following error: https://github.com/aws/aws-encryption-sdk/actions/runs/12802496582/job/35693699752?pr=742

   at System.String.GetNonRandomizedHashCode()
   at System.Collections.Generic.Dictionary`2[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].FindValue(System.__Canon)
   at System.Collections.Generic.Dictionary`2[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].TryGetValue(System.__Canon, System.__Canon ByRef)
   at System.Collections.Generic.CollectionExtensions.GetValueOrDefault[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]](System.Collections.Generic.IReadOnlyDictionary`2<System.__Canon,System.__Canon>, System.__Canon, System.__Canon)
   at Microsoft.Boogie.ResolutionContext.LookUpFunction(System.String)
   at Microsoft.Boogie.FunctionCall.Resolve(Microsoft.Boogie.ResolutionContext, Microsoft.Boogie.Expr)
   at Microsoft.Boogie.NAryExpr.Resolve(Microsoft.Boogie.ResolutionContext)
   at Microsoft.Boogie.NAryExpr.Resolve(Microsoft.Boogie.ResolutionContext)
   at Microsoft.Boogie.NAryExpr.Resolve(Microsoft.Boogie.ResolutionContext)
....
   at Microsoft.Boogie.NAryExpr.Resolve(Microsoft.Boogie.ResolutionContext)
   at Microsoft.Boogie.NAryExpr.Resolve(Microsoft.Boogie.ResolutionContext)
   at Microsoft.Boogie.NAryExpr.Resolve(Microsoft.Boogie.ResolutionContext)
   at Microsoft.Boogie.Axiom.Resolve(Microsoft.Boogie.ResolutionContext)
   at Microsoft.Boogie.Program.Resolve(Microsoft.Boogie.ResolutionContext)
   at Microsoft.Boogie.Program.Resolve(Microsoft.Boogie.CoreOptions, Microsoft.Boogie.IErrorSink)
   at Microsoft.Boogie.ExecutionEngine+<GetVerificationTasks>d__46.MoveNext()
   at System.Runtime.CompilerServices.AsyncMethodBuilderCore.Start[[Microsoft.Boogie.ExecutionEngine+<GetVerificationTasks>d__46, Boogie.ExecutionEngine, Version=3.3.3.0, Culture=neutral, PublicKeyToken=null]](<GetVerificationTasks>d__46 ByRef)
   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].Start[[Microsoft.Boogie.ExecutionEngine+<GetVerificationTasks>d__46, Boogie.ExecutionEngine, Version=3.3.3.0, Culture=neutral, PublicKeyToken=null]](<GetVerificationTasks>d__46 ByRef)
   at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Microsoft.Boogie.Program, System.Threading.CancellationToken)
   at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier+<GetVerificationTasksAsync>d__3.MoveNext()
   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1+AsyncStateMachineBox`1[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier+<GetVerificationTasksAsync>d__3, DafnyLanguageServer, Version=4.9.0.0, Culture=neutral, PublicKeyToken=null]].ExecutionContextCallback(System.Object)
   at System.Threading.ExecutionContext.RunFromThreadPoolDispatchLoop(System.Threading.Thread, System.Threading.ExecutionContext, System.Threading.ContextCallback, System.Object)
   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1+AsyncStateMachineBox`1[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier+<GetVerificationTasksAsync>d__3, DafnyLanguageServer, Version=4.9.0.0, Culture=neutral, PublicKeyToken=null]].MoveNext(System.Threading.Thread)
   at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1+AsyncStateMachineBox`1[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier+<GetVerificationTasksAsync>d__3, DafnyLanguageServer, Version=4.9.0.0, Culture=neutral, PublicKeyToken=null]].ExecuteFromThreadPool(System.Threading.Thread)
   at System.Threading.ThreadPoolWorkQueue.Dispatch()
   at System.Threading.PortableThreadPool+WorkerThread.WorkerThreadStart()
   at System.Threading.Thread.StartCallback()

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

Linux

[robin-aws]

This is a common problem with long sequence displays or string literals, since the encoding into Boogie uses a linked-list-like data type, and the processing generally uses recursive functions. This is unfortunately expensive to address at that level.

In this case the better alternative is usually storing the binary data in a file instead, and using the FileIO standard library to read the data (or since you're in the ESDK context, the older copy from dafny-lang/libraries)