Prepare for making new resolver the default #5653

RustanLeino · 2024-07-30T01:27:21Z

This PR prepares for making the new resolver the default (i.e., making --type-system-refresh --general-traits=datatype --general-newtypes the default), but it does not actually change the default.

It fixes many bugs in the new resolver and makes other improvements (tighter inference, better error messages, etc.)
It changes the test suite to run the new resolver, except in a few dozen test cases that explicitly invoke the legacy resolver. (Among those exceptions, many will be moved to use the new resolver in due time, but for now it seems better to get these bug fixes in rather than delaying this PR.) By default, tests that use %testDafnyForEachResolver and %testDafnyForEachCompiler use both the old and new resolver.
It changes the building of the Dafny runtime, Dafny standard library, AutoExtern, and documentation to use the new resolver.

This PR does not change the default resolver. So, users of the old resolver are mostly unaffected, and users of the new resolver obtain the PR's bug fixes.

Commnents for reviewers

The behavior of the resolver requires changes in some Dafny code, which affects the test suite:
- In the new type system, a trait is not a reference type unless it's declared with extends object.
- The new resolver infers all bound variables to be of base types (like int), never of a subset type (like nat).
- In some places, specific type parameters have to be given explicitly (usually because the type needs to be a subset type--maybe these can be improved in the future).
- The old type system would automatically downcast (from a trait to a class). The new resolver requires an explicit cast for this (as does C# and Java, for example).
Sometimes, the tests show a different number of things verified. That's because the new or old type system takes care of all the proof obligations.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

comp/Class.dfy

The 1 more verified comes from the type of {}. It’s really inferred to be set<object?_\bot>, but this is later turned into just set<object?>.

Found via traits/TraitResolution1.dfy

keyboardDrummer · 2025-03-10T09:37:20Z

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

  }

+  public static IEnumerable<MemberDecl> AllMembers(IEnumerable<TopLevelDecl> declarations) {
+    foreach (var decl in declarations.OfType<TopLevelDeclWithMembers>()) {


better to use declarations.OfType<TopLevelDeclWithMembers>().SelectMany(d => d.Members)

keyboardDrummer · 2025-03-10T09:44:16Z

Source/DafnyCore/Options/CommonOptionBag.cs

  public static readonly Option<bool> TypeSystemRefresh = new("--type-system-refresh", () => false,
    @"
-false - The type-inference engine and supported types are those of Dafny 4.0.
+false (default) - The type-inference engine and supported types are those of Dafny 4.0.


The generated documentation already indicates the default value, so no need to specify it explicitly. Example:

keyboardDrummer · 2025-03-10T09:53:37Z

Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs

      Constraints.AddConfirmation(tok, () => CheckComparableTypes(a, b, allowBaseTypeCast), errorMessage);
    }

+    private void AddComparableTypesDefault(PreType a, PreType b) {


Would be good to have an example of what Dafny code this is could help with

keyboardDrummer · 2025-03-10T09:59:39Z

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs

          }
        case LiteralExpr:
          CheckResultToBeInType(expr.Origin, expr, expr.Type, locals, builder, etran);
+          if (expr is StringLiteralExpr stringLiteralExpr) {


What's this about?

keyboardDrummer · 2025-03-10T10:01:34Z

Source/DafnyStandardLibraries/src/Std/JSON/Deserializer.dfy


  function Object(js: Grammar.jobject): DeserializationResult<seq<(string, Values.JSON)>> {
-    Seq.MapWithResult(d requires d in js.data => KeyValue(d.t), js.data)
+    var f := d requires d in js.data => KeyValue(d.t);


Why is this needed?

keyboardDrummer · 2025-03-10T10:05:13Z

The new resolver infers all bound variables to be of base types (like int), never of a subset type (like nat).

From a user's perspective, this is a regression of the type system, right? I see quite a few changes were made in the standard library to accommodate for this change.

keyboardDrummer · 2025-03-10T10:05:57Z

Source/DafnyStandardLibraries/src/Std/JSON/ZeroCopy/Deserializer.dfy

-            assert sep.StrictlySplitFrom?(elem.cs, c => Spec.Structural(c, SpecView)) by {
-              assert sep.BytesSplitFrom?(elem.cs, c => Spec.Structural(c, SpecView)) by {
-                assert sep.SplitFrom?(elem.cs, c => Spec.Structural(c, SpecView));
+            assert sep.StrictlySplitFrom?(elem.cs, (c: Structural<jcomma>) => Spec.Structural(c, SpecView)) by {


These types of changes are not exactly pretty. What's the trade-off here?

keyboardDrummer

I committed a few small changes. Approving, although the change to no longer infer subset types for bound variables makes user code less readable. What would it take to enable that?

Ideally we would enable that before moving the stdlib to the new resolver, so it would not need many of the changes it got now.

# Conflicts: # Source/DafnyCore/AST/TypeDeclarations/Declaration.cs

RustanLeino · 2025-03-18T17:56:02Z

Thanks for the review, changes, and comments. I will merge this into master and will write down work items as an Issue.

the change to no longer infer subset types for bound variables makes user code less readable. What would it take to enable that?

This change was in the new resolver before. That is, this PR does not change this behavior. The old resolver could infer bound variables as subset types, but that can potentially create surprises. For example, given

predicate P(n: nat, s: string)
predicate Q(s: string)

consider inferring the type of x in

forall x, s :: if 0 <= x then P(x, s) else Q(s)

If the type of x is inferred as nat (which may be tempting, given that P's first parameter has type nat), then the else branch is dead code. The new resolver handles bound variables consistently by never inferring subset types.

RustanLeino and others added 14 commits May 28, 2024 13:16

Change default settings

51e033a

Explicitly declare trait to be a reference type

5204eeb

Make the new type system the default

3bdaa87

Merge branch 'master' into refresh-by-default

48a8cf4

Explicitly declare trait as reference type

3101604

Changed from full to datatype

a134465

Add “extends object” where it was assumed to be so before

d75f39f

Fix error location for desugared elephant assert

46484e6

Merge branch 'refresh-by-default' into typeSystemRefreshDefault

74a49df

Merge branch 'master' into refresh-by-default

af730de

Use explicit legacy switches in testDafnyForEach…

5acc14b

Fix missing box adjustment in verifier

611ac55

fix: Use just one pre-type proxy for element type in array allocation

4979a6e

Merge branch 'master' into refresh-by-default

d701a33

RustanLeino changed the title ~~Refresh resolver by default~~ Use refresh resolver by default Jul 30, 2024

RustanLeino added 15 commits August 17, 2024 17:05

Fix pre-type of StaticReceiverExpr

7a5d171

comp/Class.dfy

Update tests to support new defaults

a4bf314

Involve compatible-type constraints in decision process

18addcf

Update test

47d4abc

The 1 more verified comes from the type of {}. It’s really inferred to be set<object?_\bot>, but this is later turned into just set<object?>.

Extract method SansPrintablePreType

43a6a37

Fix type inference of seq/map/multiset update expressions

a6820e1

Merge branch 'master' into refresh-by-default

99fbb08

Fix asserted-expression output for frames

5026519

Fix creation of yield-identifier expression

dab7870

Update expect files

8028152

Fix pre-type resolution of export-provided members/types

86e2312

Found via traits/TraitResolution1.dfy

Improve formatting

bb2d519

Adjust tests and expected test output

d2624ee

Fix parameter order

456afc5

Adjust tests and expected test output

954dd42

RustanLeino added 7 commits March 7, 2025 15:47

Fix typo in option

9f2dc9a

Split %translate/%trargs the same way as in lit.site.cfg

17badf9

Remove redundant option

7ed588a

Improve RUN command

c60c7be

Add new-resolver arguments in a missing place

9dc943d

Fix audit tests and macros

aa5d612

Fix typo in new definition

1ddc176

RustanLeino marked this pull request as ready for review March 9, 2025 20:37

RustanLeino changed the title ~~Use refresh resolver by default~~ Prepare for making new resolver the default Mar 9, 2025

RustanLeino requested a review from keyboardDrummer March 9, 2025 20:41

keyboardDrummer reviewed Mar 10, 2025

View reviewed changes

keyboardDrummer added 2 commits March 10, 2025 11:13

Code review

c354a9e

Merge branch 'master' into refresh-by-default

54652be

keyboardDrummer previously approved these changes Mar 10, 2025

View reviewed changes

RustanLeino added 2 commits March 14, 2025 15:12

Merge branch 'master' into refresh-by-default

780d883

Merge branch 'master' into refresh-by-default

c1831c3

# Conflicts: # Source/DafnyCore/AST/TypeDeclarations/Declaration.cs

RustanLeino dismissed keyboardDrummer’s stale review via c1831c3 March 18, 2025 17:43

RustanLeino enabled auto-merge (squash) March 18, 2025 17:44

Allow variation of error message in test output

3a679b4

keyboardDrummer approved these changes Mar 19, 2025

View reviewed changes

RustanLeino merged commit 60e9ae5 into dafny-lang:master Mar 19, 2025
22 checks passed

RustanLeino deleted the refresh-by-default branch March 19, 2025 19:26

MikaelMayer mentioned this pull request Apr 16, 2025

Bitvector issue with --type-system-refresh #6196

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Prepare for making new resolver the default #5653

Prepare for making new resolver the default #5653

Uh oh!

RustanLeino commented Jul 30, 2024 •

edited

Loading

Uh oh!

keyboardDrummer Mar 10, 2025

Uh oh!

keyboardDrummer Mar 10, 2025

Uh oh!

keyboardDrummer Mar 10, 2025 •

edited

Loading

Uh oh!

keyboardDrummer Mar 10, 2025

Uh oh!

keyboardDrummer Mar 10, 2025

Uh oh!

keyboardDrummer commented Mar 10, 2025 •

edited

Loading

Uh oh!

keyboardDrummer Mar 10, 2025 •

edited

Loading

Uh oh!

keyboardDrummer left a comment •

edited

Loading

Uh oh!

RustanLeino commented Mar 18, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Prepare for making new resolver the default #5653

Prepare for making new resolver the default #5653

Uh oh!

Conversation

RustanLeino commented Jul 30, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Commnents for reviewers

Uh oh!

keyboardDrummer Mar 10, 2025

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Mar 10, 2025

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Mar 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Mar 10, 2025

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Mar 10, 2025

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer commented Mar 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

keyboardDrummer Mar 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

RustanLeino commented Mar 18, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

RustanLeino commented Jul 30, 2024 •

edited

Loading

keyboardDrummer Mar 10, 2025 •

edited

Loading

keyboardDrummer commented Mar 10, 2025 •

edited

Loading

keyboardDrummer Mar 10, 2025 •

edited

Loading

keyboardDrummer left a comment •

edited

Loading