Merge remote-tracking branch 'origin/master' into CounterexamplesAsPr…

…edicates

.github/workflows/doc-tests.yml

@@ -10,6 +10,8 @@ on:
  workflow_dispatch:
  pull_request:
  branches: [ master, main-* ]
+ merge_group:
+ branches: [ master, main-* ]
 
 concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}

.github/workflows/jekyll.yml

@@ -37,7 +37,7 @@ jobs:
  working-directory: 'docs'
  - name: Setup Pages
  id: pages
- uses: actions/configure-pages@v4
+ uses: actions/configure-pages@v5
  - name: Build with Jekyll
  # Outputs to the './_site' directory by default
  run: (cd docs; bundle exec jekyll build --baseurl "${{ steps.pages.outputs.base_path }}" --destination ../_site)

.github/workflows/msbuild.yml

@@ -4,6 +4,8 @@ on:
  workflow_dispatch:
  pull_request:
  branches: [ master, main-* ]
+ merge_group:
+ branches: [ master, main-* ]
 
 concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}

.github/workflows/refman.yml

@@ -4,6 +4,8 @@ on:
  workflow_dispatch:
  pull_request:
  branches: [ master, main-* ]
+ merge_group:
+ branches: [ master, main-* ]
 
 concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}

.github/workflows/runtime-tests.yml

@@ -4,6 +4,8 @@ on:
  workflow_dispatch:
  pull_request:
  branches: [ master, main-* ]
+ merge_group:
+ branches: [ master, main-* ]
 
 concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}

.github/workflows/standard-libraries.yml

@@ -4,6 +4,8 @@ on:
  workflow_dispatch:
  pull_request:
  branches: [ master, main-* ]
+ merge_group:
+ branches: [ master, main-* ]
 
 concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}

.gitignore

@@ -79,3 +79,5 @@ Source/IntegrationTests/TestFiles/LitTests/LitTest/server/*.bvd
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/assumptions-lib
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/log.smt2
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/model
+Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/*.html
+Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/*.html

CONTRIBUTING.md

@@ -74,7 +74,7 @@ After doing these steps once, for other PRs, one only needs to re-run deep check
 - If some required tests fail, investigate and push more commits, but know that each CI run takes a lot of time, so try to fix the problem with as few commits as possible (ideally 1)
  It is also possible you find some tests that fail randomly, in that case, re-run them and report to the team. Avoid using the re-run all failed jobs here, because it will re-run _all_ jobs, so select them individually instead.
 - Have someone approve the PR and merge it (or auto-merge).
-- Once the PR with the fix to the CI is merged to master, go to https://github.com/dafny-lang/dafny/actions/workflows/deep-tests.yml
+- Once the PR with the fix to the CI is merged to master, go to https://github.com/dafny-lang/dafny/actions/workflows/nightly-build.yml
 - Select "Run workflow..."
 - Select master
 - Wait for this new run to succeed.
@@ -101,3 +101,9 @@ For example, `Formatting.dfy`
 ### What is the release process?
 
 You can find a description of the release process in [docs/dev/RELEASE.md](https://github.com/dafny-lang/dafny/blob/master/docs/dev/RELEASE.md).
+
+### Backwards compatibility
+
+Dafny is still changing and backwards incompatible changes may be made. Any backwards compatibility breaking change must be easy to adapt to, such as by adding a command line option. In the future, we plan to add a `dafny migrate` command which should support migrating any Dafny codebase from the previous to the current CLI version. 
+
+As rule, Dafny features must be marked as deprecated, including migration instructions, at least one release before they are removed.

README.md

@@ -1,3 +1,5 @@
+# Dafny
+
 [![Build and Test](https://github.com/dafny-lang/dafny/workflows/Build%20and%20Test/badge.svg)](https://github.com/dafny-lang/dafny/actions?query=workflow%3A%22Build+and+Test%22) [![Gitter](https://badges.gitter.im/dafny-lang/community.svg)](https://gitter.im/dafny-lang/community?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge)
 
 Dafny is a **verification-ready programming language**. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can **compile your code to C#, Go, Python, Java, or JavaScript** (more to come!), so it can integrate with your existing workflow.
@@ -23,33 +25,33 @@ Documentation about the dafny language and tools is located
 [here](https://dafny-lang.github.io/dafny).
 A reference manual is available both [online](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef) and as [pdf](https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/out/DafnyRef.pdf). (A LaTeX version can be produced if needed.)
 
-# Community
+## Community
 
 You can ask questions about Dafny on [Stack Overflow](https://stackoverflow.com/questions/tagged/dafny) or participate in general discussion on Dafny's [![Gitter](https://badges.gitter.im/dafny-lang/community.svg)](https://gitter.im/dafny-lang/community?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge).
 
-# Try Dafny
+## Try Dafny
 
 The easiest way to try out Dafny is to [install Dafny on your own machine in Visual Studio Code](https://github.com/dafny-lang/dafny/wiki/INSTALL#visual-studio-code)
 and follow along with the [Dafny tutorial](https://dafny-lang.github.io/dafny/OnlineTutorial/guide).
 You can also [download and install](https://github.com/dafny-lang/dafny/wiki/INSTALL#install-the-binaries) the Dafny CLI if you prefer to work from the command line.
 
-# Read more
+## Read more
 
 Here are some ways to get started with Dafny:
 
 * 4-part course on the _Basics of specification and verification of code_:
- - Lecture 0: [Pre- and postconditions](https://youtu.be/oLS_y842fMc) (19:08)
- - Lecture 1: [Invariants](https://youtu.be/J0FGb6PyO_k) (20:56)
- - Lecture 2: [Binary search](https://youtu.be/-_tx3lk7yn4) (21:14)
- - Lecture 3: [Dutch National Flag algorithm](https://youtu.be/dQC5m-GZYbk) (20:33)
+ * Lecture 0: [Pre- and postconditions](https://youtu.be/oLS_y842fMc) (19:08)
+ * Lecture 1: [Invariants](https://youtu.be/J0FGb6PyO_k) (20:56)
+ * Lecture 2: [Binary search](https://youtu.be/-_tx3lk7yn4) (21:14)
+ * Lecture 3: [Dutch National Flag algorithm](https://youtu.be/dQC5m-GZYbk) (20:33)
 * New overview article: [Accessible Software Verification with Dafny](https://www.computer.org/csdl/mags/so/2017/06/mso2017060094-abs.html), IEEE Software, Nov/Dec 2017
 * [Online tutorial](https://dafny-lang.github.io/dafny/OnlineTutorial/guide), focusing mostly on simple imperative programs
 * [3-page tutorial notes](https://leino.science/papers/krml233.pdf) with examples (ICSE 2013)
 * Dafny [Quick Reference](https://dafny-lang.github.io/dafny/QuickReference)
 * Language reference for the [Dafny type system](https://leino.science/papers/krml243.html), which also describes available expressions for each type
 * [Cheatsheet](https://docs.google.com/document/d/1kz5_yqzhrEyXII96eCF1YoHZhnb_6dzv-K3u79bMMis/edit?pref=2&pli=1): basic Dafny syntax on two pages
 * Dafny Reference Manual [[html](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef)] [[pdf](https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/out/DafnyRef.pdf)]
-* [Dafny libraries](https://github.com/dafny-lang/libraries), a standard library of useful Dafny functions and lemmas
+* [Dafny libraries](Source/DafnyStandardLibraries/README.md), a standard library of useful Dafny functions and lemmas
 * [Dafny Power User](https://leino.science/dafny-power-user)
 * Videos at [Verification Corner](https://www.youtube.com/channel/UCP2eLEql4tROYmIYm5mA27A)
 * [Blog](https://dafny.org/blog)
@@ -63,17 +65,17 @@ The language itself draws pieces of influence from:
 * ML (like the module system, and its functions and inductive datatypes), and
 * Coq and VeriFast (like the ability to include co-inductive datatypes and being able to write inductive and co-inductive proofs).
 
-# External contributions
+## External contributions
 
 * [Haskell-to-Dafny translator](https://www.doc.ic.ac.uk/~dcw/h2d.cgi), by Duncan White
 * [Vim-loves-Dafny mode](https://github.com/mlr-msft/vim-loves-dafny) for vim, by Michael Lowell Roberts
 * [Boogie-Friends Emacs mode](https://github.com/boogie-org/boogie-friends)
 
-# Contributors
+## Contributors
 
 Information and instructions for potential contributors are provided [here](CONTRIBUTING.md).
 
-# License
+## License
 
 Dafny itself is licensed under the MIT license. (See `LICENSE.txt` in the root
 directory for details.) The subdirectory `Source/Dafny/Coco` contains third

RELEASE_NOTES.md

@@ -2,6 +2,117 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.5.0
+
+## New features
+
+- Add the option `--include-test-runner` to `dafny translate`, to enable getting the same result as `dafny test` when doing manual compilation. (https://github.com/dafny-lang/dafny/pull/3818)
+
+- - Fix: verification in the IDE no longer fails for iterators
+ - Fix: the IDE now provides feedback when verification fails to run, for example due to a bad solver path
+ - Fix: let the IDE correctly use the solver-path option when it's specified in a project file
+ - Feat: improve the order of verification diagnostics emitted by the Dafny CLI, so that they now always follow the line order of the program.
+ (https://github.com/dafny-lang/dafny/pull/4798)
+
+- - Add an option `--filter-position` to the `dafny verify` command. The option filters what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5` will only verify things that range over line 5 in the file `source1.dfy`. In combination with ``--isolate-assertions`, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: `dafny verify MyFile.dfy --filter-position=:23`
+ - Add an option `--filter-symbol` to the `dafny verify` command, that only verifies symbols whose fully qualified name contains the given argument. For example, `dafny verify dfyconfig.toml --filter-symbol=MyModule` will verify everything inside `MyModule`.
+ - The option `--boogie-filter` has been removed in favor of --filter-symbol
+ (https://github.com/dafny-lang/dafny/pull/4816)
+
+- Add a `json` format to those supported by `--log-format` and `/verificationLogger`, for producing thorough, machine readable logs of verification results. (https://github.com/dafny-lang/dafny/pull/4951)
+
+- - Flip the behavior of `--warn-deprecation` and change the name to `--allow-deprecation`, so the default is now false, which is standard for boolean options.
+ - When using `--allow-deprecation`, deprecated code is shown using tooltips in the IDE, and on the CLI when using `--show-tooltips`.
+ - Replace the option `--warn-as-error` with the option `--allow-warnings`. The new option, when false, the default value, causes Dafny to stop generating executable output and return a failure exit code, when warnings occur in the program. Contrary to the previous `--warn-as-error` option, warnings are always reported as warnings.
+ - During development, users must use `dafny run --allow-warnings` if they want to run their Dafny code when it contains warnings.
+ - If users have builds that were passing with warnings, they have to add `--allow-warnings` to allow them to still pass. 
+ - If users upgrade to a new Dafny version, and are not using `--allow-warnings`, and do not want to migrate off of deprecated features, they will have to use `--allow-deprecation`.
+ - When using the legacy CLI, the option /warningsAsErrors now has the behavior of --allow-warnings=false
+ - A doo file that was created using `--allow-warnings` causes a warning if used by a consumer that does not use it.
+ (https://github.com/dafny-lang/dafny/pull/4971)
+
+- The new `{:contradiction}` attribute can be placed on an `assert` statement to indicate that it forms part of an intentional proof by contradiction and therefore shouldn't be warned about when `--warn-contradictory-assumptions` is turned on. (https://github.com/dafny-lang/dafny/pull/5001)
+
+- Function and method parameters and return types, and datatype constructor arguments, can now have attributes. By default, there are no attributes that Dafny recognizes in these positions, but custom back-ends can use this feature to get extra information from the source files. (https://github.com/dafny-lang/dafny/pull/5032)
+
+- Under the CLI option `--general-newtypes`, the base type of a `newtype` declaration can now be (`int` or `real`, as before, or) `bool`, `char`, or a bitvector type.
+
+ `as` and `is` expressions now support more types than before. In addition, run-time type tests are supported for `is` expressions, provided type parameters are injective (as was already required) and provided the constraints of any subset type or newtype is compilable. Note, although both `as` and `is` allow many more useful cases than before, using `--general-newtypes` will also forbid some unusual cases that were previously allowed. Any such case that is now forbidden can still be done by doing the `as`/`is` via `int`.
+ (https://github.com/dafny-lang/dafny/pull/5061)
+
+- Allow newtype declarations to be based on set/iset/multiset/seq. (https://github.com/dafny-lang/dafny/pull/5133)
+
+## Bug fixes
+
+- Fixed crash caused by cycle in type declaration (https://github.com/dafny-lang/dafny/pull/4471)
+
+- Fix resolution of unary minus in new resolver (https://github.com/dafny-lang/dafny/pull/4737)
+
+- The command line and the language server now use the same counterexample-related Z3 options. (https://github.com/dafny-lang/dafny/pull/4792)
+
+- Dafny no longer crashes when required parameters occur after optional ones. (https://github.com/dafny-lang/dafny/pull/4809)
+
+- Use defensive coding to prevent a crash in the IDE that could occur in the context of code actions. (https://github.com/dafny-lang/dafny/pull/4818)
+
+- Fix null-pointer problem in new resolver (https://github.com/dafny-lang/dafny/pull/4875)
+
+- Fixed a crash that could occur when a case body of a match that was inside a loop, had a continue or break statement. (https://github.com/dafny-lang/dafny/pull/4894)
+
+- Compile run-time constraint checks for newtypes in comprehensions (https://github.com/dafny-lang/dafny/pull/4919)
+
+- Fix null dereference in constant-folding invalid string-indexing expressions (https://github.com/dafny-lang/dafny/pull/4921)
+
+- Check for correct usage of type characteristics in specifications and other places where they were missing.
+
+ This fix will cause build breaks for programs with missing type characteristics (like `(!new)` and `(0)`). Any such error message is accompanied with a hint about what type characterics need to be added where.
+ (https://github.com/dafny-lang/dafny/pull/4928)
+
+- Initialize additional fields in the AST (https://github.com/dafny-lang/dafny/pull/4930)
+
+- Fix crash when a function/method with a specification is overridden in an abstract type. (https://github.com/dafny-lang/dafny/pull/4954)
+
+- Fix crash for lookup of non-existing member in new resolver (https://github.com/dafny-lang/dafny/pull/4955)
+
+- Fix: check that subset-type variable's type is determined (resolver refresh).
+ Fix crash in verifier when there was a previous error in determining subset-type/newtype base type.
+ Fix crash in verifier when a subset type has no explicit `witness` clause and has a non-reference trait as its base type.
+ (https://github.com/dafny-lang/dafny/pull/4956)
+
+- The `{:rlimit N}` attribute, which multiplied `N` by 1000 before sending it to Z3, is deprecated in favor of the `{:resource_limit N}` attribute, which can accept string arguments with exponential notation for brevity. The `--resource-limit` and `/rlimit` flags also now omit the multiplication, and the former allows exponential notation. (https://github.com/dafny-lang/dafny/pull/4975)
+
+- Allow a datatype to depend on traits without being told "datatype has no instances" (https://github.com/dafny-lang/dafny/pull/4997)
+
+- Don't consider `:= *` to be a definite assignment for non-ghost variables of a `(00)` type (https://github.com/dafny-lang/dafny/pull/5024)
+
+- Detect the same ghost usage in initializing assignments as in other expressions. The effect of this fix is to allow more iset/imap comprehensions to be compiled.
+
+ Also, report errors if the LHS of `:=` in compiled `map`/`imap` comprehensions contains ghosts.
+ (https://github.com/dafny-lang/dafny/pull/5041)
+
+- Escape names of nested modules in C# and Java (https://github.com/dafny-lang/dafny/pull/5049)
+
+- A parent trait that is a reference type can now be named via `import opened`.
+
+ Implicit conversions between a datatype and its parent traits no longer crashes the verifier.
+
+ (Dis)equality expressions of a (co)datatype and its parent traits no longer crashes the verifier.
+ (https://github.com/dafny-lang/dafny/pull/5058)
+
+- Fixed support for newtypes as sequence comprehension lengths in Java (https://github.com/dafny-lang/dafny/pull/5065)
+
+- Don't emit an error message for a `function-by-method` with unused type parameters. (https://github.com/dafny-lang/dafny/pull/5068)
+
+- The syntax of a predicate definition must always include parentheses. (https://github.com/dafny-lang/dafny/pull/5069)
+
+- Termination override check for certain non-reference trait implementations (https://github.com/dafny-lang/dafny/pull/5087)
+
+- Malformed Python code for some functions involving lambdas (https://github.com/dafny-lang/dafny/pull/5093)
+
+- Let verifier understand opaque function overrides, supporting both when the overridden function is opaque and non-opaque. Revealing such a function for one overriding type has the effect of revealing it for all overriding types.
+
+ Also, forbid the case where a function is opaque in a parent trait and the function override is not opaque. (Previously, this had caused a crash.)
+ (https://github.com/dafny-lang/dafny/pull/5111)
+
 # 4.4.0
 
 ## New features

Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs

@@ -3,7 +3,7 @@
 
 namespace Microsoft.Dafny;
 
-public class LambdaExpr : ComprehensionExpr, ICloneable<LambdaExpr> {
+public class LambdaExpr : ComprehensionExpr, ICloneable<LambdaExpr>, IFrameScope {
  public override string WhatKind => Reads.Expressions.Count != 0 ? "lambda" : Range != null ? "partial lambda" : "total lambda";
 
  public Expression Body => Term;
@@ -84,4 +84,6 @@ public override bool SetIndent(int indentBefore, TokenNewIndentCollector formatt
 
  return true;
  }
+
+ public string Designator => "lambda";
 }

Source/DafnyCore/AST/Grammar/ParseErrors.cs

@@ -137,7 +137,8 @@ public enum ErrorId {
  p_deprecated_statement_refinement,
  p_internal_exception,
  p_file_has_no_code,
- p_general_traits_beta,
+ p_general_traits_datatype,
+ p_general_traits_full,
  }
 
  static ParseErrors() {
@@ -153,9 +154,16 @@ static ParseErrors() {
 Only modules may be declared abstract.
 ".TrimStart(), Remove(true));
 
- Add(ErrorId.p_general_traits_beta,
+ Add(ErrorId.p_general_traits_datatype,
  @"
-Use of traits as non-reference types is a beta feature. To engage, use /generalTraits:datatype.
+A newtype extending a trait is not generally supported. The option --general-traits=full causes
+Dafny to allow them in the input, but is not recommended.
+".TrimStart(), Remove(true));
+
+ Add(ErrorId.p_general_traits_full,
+ @"
+Use of traits as non-reference types is supported, but is not yet the default. Until it becomes the
+default, use --general--traits=datatype to enable it.
 ".TrimStart(), Remove(true));
 
  Add(ErrorId.p_no_ghost_for_by_method,

Source/DafnyCore/AST/IHasUsages.cs

@@ -28,6 +28,10 @@ public interface ICanVerify : ISymbol {
  string FullDafnyName { get; }
 }
 
+public interface IFrameScope {
+ string Designator { get; } // "lambda expression", "method", "function"...
+}
+
 public static class AstExtensions {
 
  public static string GetMemberQualification(MemberDecl memberDecl) {

Source/DafnyCore/AST/Members/ConstantField.cs

@@ -65,4 +65,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
  AutoRevealFunctionDependencies.GenerateMessage(addedReveals.ToList()));
  }
  }
+ public string Designator => WhatKind;
 }