Dafny 4.11.0

[MikaelMayer]

New features

• Stabilize verifications by automatically computing triggers for the quantified proof obligations associated with :| constructs.
  Manually specified triggers and warning-suppressing attributes are also supported (and mentioned in warning messages, as for other quantifiers and comprehensions).
  Enhance witness guessing for the proof obligation associated for :| assignments.
  (feat: Compute triggers for such-that operations #6023)

• Four new Dafny standard libraries:

  • Std.Actions - utilities for abstract imperative actions, including enumerating and streaming values
  • Std.Frames - utilities related to working with dynamic framing, often related to reads and modifies clauses
  • Std.Ordinal - operations and properties of the ORDINAL type
  • Std.Termination - a datatype for representing Dafny decreases clauses and extensions
    (feat: Actions, Frames, Termination, and Ordinal standard libraries #6074)

• Support using --standard-libraries with --enforce-determinism. Removed Std.Collections.Seq.SetToSeq since it was slow and not compatible with this mode. (https://github.com/dafny-lang/daf
  ny/pull/6137)

• With --standard-libraries you can now read an UTF-8 text files from the disk using Std.FileIO.ReadUTF8FromFile(path: string): Result<string, string>.
  To write some content to the disk, use Std.FileIO.WriteUTF8ToFile(path: string, content: string): Outcome<string>.
  Standard library breaking change: All UnicodeEncodingForm versions of FromUTF8Checked, FromUTF16Checked and DecodeCodeUnitSequenceChecked now return a Result instead of an Option so that the error message is clearer. Migration is easy: Use .ToOption() if you really prefer an option. Affected refining modules: Utf8EncodingForm and Utf16EncodingForm
  (Feat: Std.FileIO.ReadFile and WriteFile #6198)

• The Dafny standard libraries now include a powerful parser combinators framework, available through Std.Parsers.StringBuilders.

  Key Features

  • Guaranteed Termination: All parsers, including those built with recursive combinators, are proven to terminate
  • Mutual Recursion Support: Build complex parsers that can reference each other (demonstrated in the Polynomial example)
  • Rich Error Reporting: Failed parsing attempts combine their error messages to provide meaningful feedback
  • Developer-Friendly Tools: Built-in debugging utilities for inspecting parser inputs and outputs
  • Memory-Efficient Recursion: Advanced implementations avoid stack overflow in recursive parsers
  • Elegant DSL: Compact, datatype-based combinators designed for readability and composition
  • Flexible Backtracking: Optional backtracking available through .??() (DSL) or ?(...) (standard syntax)
  • Comprehensive Toolkit: Rich set of combinators including lookahead, negation, folding, and binding operations
  • The library includes several practical examples, including JSON and SMT parsers, each implemented in about 50 lines of code.
    (Reinstate "Feat: Verified and easy-to-use parser combinators (#6143)" #6243)

• Dafny classes and traits can now redeclare methods defined by traits they inherit from. (Allow redeclaring trait methods #6280)

• Real literals now support scientific notation using lowercase e to denote the exponent (like 1.23e5 for 123000.0 or 5e-2 for 0.05). Real literals also support convenient trailing-dot
  shorthand (like 1. for 1.0) and leading-dot shorthand (like .5 for 0.5 or .5e2 for 50.0). Note that explicit + signs in exponents are not supported; use 5e2 instead of 5e+2. (ht
  tps://github.com/feat: Add comprehensive real literal support with scientific notation and dot shorthand #6286)

Bug fixes

• Fix soundness issue that could occur when using an opaque block and old or fresh in its ensures clause (Opaque blocks allow proving false #6060)

• Correctly display project files errors when using build command (Error does not mention faulty dfyconfig.toml file #6107)

• Fix crash that could occur when a forall statement was used inside a match case (fix: Fix crash when a simple forall statement was placed inside a match #6121)

• Fix a case where a forall statement would cause Dafny to crash (Unable to cast object of type 'Microsoft.Dafny.BinaryExpr' to type 'Microsoft.Dafny.QuantifierExpr' #6129)

• Fix @VerifyOnly and migrated the new code to use it (@VerifyOnly not working #6146)

• Java lambdas now accepting boxing/unboxing (Java equality between chars fails if one is unboxed. #6149)

• Fix crash in resolution of structural-inclusion greater-than operator (fix: Fix crash in resolution of structural-inclusion greater-than operator #6155)

• Generate alloc consequence axiom only for functions that read the heap (fixes unsoundness) (Soundness issue with constructors? #6164)

• Made the language server compliant with the LSP protocol so that it can be used with other editors, such as Helix (Non-compliant LSP message prevents wider editor support #6172)

• No more compilation issue when using bitvector shifts in Rust with the new resolver (Bitvector issue with --type-system-refresh #6196)

• Fix handling of opaque blocks in the Dafny IDE (Opaque blocks not working in VSCode extension #6203)

• JSON serialization now properly encodes unicode characters with 0 pre-pend instead of space-append.
  Also, string literals ending with escaped characters are now supported as well.
  (Standard Library serialization and deserialization error #6227)

• Fail more gracefully when reusing names (fix: Fail more gracefully when reusing names #6262)

• Escape user string literals in error messages (fix: Escape string literals in error messages #6273)

• Compilation of type conversion from a newtype-based on char to int (fix: C# compilation of newtype-char to int conversion #6296)

• Fix LSP bug that cause IDE exceptions during invalid parse states (Fix LSP bug that returned a invalid range for documentSymbol #6299)

• Fix two resolver crashes involving datatypes and traits (Fixes resolver crashes related to datatypes and traits #6321)

---

This discussion was created from the release Dafny 4.11.0.