feat: Add bounded polymorphism

[RustanLeino]

Description

This PR adds bounded polymorphism to the Dafny language. This feature allows any formal type parameter to be declared with a suffix of any number of

extends Type

clauses, where Type is any trait or subset type thereof. At call sites, the actual type arguments are checked to be subtypes of the listed type bounds. Where the formal type parameters are in scope, an expression whose type is the type parameter can be converted to a supertype of any of the type bounds by an explicit type conversion (as). In some cases, the type conversion is inferred automatically and can then be omitted from the program text.

The feature requires --type-system-refresh for full functionality.

Closes #5211

Example

For test.dfy being the program

trait Printable {
  method Print()
}

method SelectPrintReturn<T extends Printable>(operateOnLeft: bool, left: T, right: T) returns (r: T)
{
  r := if operateOnLeft then left else right;
  (r as Printable).Print();
}

datatype Dt extends Printable = Dt(u: int) {
  method Print() {
    print u, "\n";
  }
}

method Main() {
  var d0 := Dt(500);
  var d1 := Dt(702);
  var e0 := SelectPrintReturn(true, d0, d1); // 500
  var e1 := SelectPrintReturn(false, d0, d1); // 702
  print (d0, d1) == (d0, d1), "\n"; // true
}

we get:

> dafny run test.dfy --type-system-refresh --general-traits=datatype

Dafny program verifier finished with 3 verified, 0 errors
500
702
true

Bonus

The PR also

• suppresses near-identical error messages (in particular, it reports only one error for conditions that split into several checks, like the type equality A==B which turns into both A :> B and B >: A)

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

[ssomayyajula]

Reporting some issues on behalf of @erniecohen:

1. If X extends T and one has x: X, then one frequently has to assert that x is T. In fact, I myself can't get this to check:

trait T {}

function F<X extends T>(x: X): T {
  assert x is T; x // x is not assignable to T
}

Is there a missing constraint during type inference?

2. The following doesn't check.

trait T { 
    static const z := 0
}
trait U<X extends T> {
    static const z := X.z // unresolved identifier: X
}

3. Ill-typed Boogie generation:

module Util {
function min(x:nat, y:nat):nat { if x < y then x else y }
function max(x:nat, y:nat):nat { if x < y then y else x }
}

trait Op<T> { function op(t:T):T }
trait BOp<S,T> { function op(s:S,t:T):T }

trait Dom<T(!new)> {
    predicate has(t:T)
    ghost predicate andPost(d:Dom<T>,r:Dom<T>) { forall t:T | has(t) && d.has(t) :: r.has(t) }
    function and(d:Dom<T>):(r:Dom<T>) ensures andPost(d,r)
    ghost predicate orPost(d:Dom<T>,r:Dom<T>) { forall t:T | has(t) || d.has(t) :: r.has(t) }
    function or(d:Dom<T>):(r:Dom<T>) ensures andPost(d,r)
    ghost static predicate topPost() { forall t:T :: top().has(t) }
    static function top():Dom<T> ensures topPost()
}

newtype Reg = nat {
    const v := this 
    const n := this as nat
    function inc():Reg { v + 1 }
    function plus(r:Reg):Reg { v + r.v }
}

datatype Ivl extends Dom<Reg> = Ivl(min:Reg,max:Reg) {
    predicate has(t:Reg) { min <= t < max }
    function and(d:Dom<Reg>):(r:Dom<Reg>) ensures andPost(d,r) && r is Ivl {
        if (d is Ivl) then var d := d as Ivl; 
            var r := Ivl(Util.max(min.n,d.min.n) as Reg, Util.min(max.n,d.max.n) as Reg); r
        else this
    }
    function or(d:Dom<Reg>):(r:Dom<Reg>) ensures orPost(d,r) {
        if (d is Ivl) then var d := d as Ivl;
            var r := Ivl(Util.min(min.n,d.min.n) as Reg, Util.max(max.n,d.max.n) as Reg); r
        else top() // triggers internal error on verification
    }
}

returns

Encountered internal compilation exception: Boogie program had 2 type errors:
Microsoft.Dafny.BoogieRangeToken: branches of if-then-else have incompatible types DatatypeType and Box
Microsoft.Dafny.BoogieRangeToken: branches of if-then-else have incompatible types DatatypeType and Box
/root/Test-bounded-poly.dfy(7,23): Error: Internal error occurred during verification: Boogie program had 2 type errors:
 Microsoft.Dafny.BoogieRangeToken: branches of if-then-else have incompatible types DatatypeType and Box
 Microsoft.Dafny.BoogieRangeToken: branches of if-then-else have incompatible types DatatypeType and Box
    at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program)
    at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken) in /com.docker.devenvironments.code/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs:line 65
    at Microsoft.Dafny.Compilation.<>c__DisplayClass54_1.<<VerifyUnverifiedSymbol>b__1>d.MoveNext() in /com.docker.devenvironments.code/Source/DafnyCore/Pipeline/Compilation.cs:line 325
 --- 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 /com.docker.devenvironments.code/Source/DafnyCore/Pipeline/Compilation.cs:line 324
    at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed) in /com.docker.devenvironments.code/Source/DafnyCore/Pipeline/Compilation.cs:line 324
  |
7 | trait Op<T> { function op(t:T):T }
  |                        ^^

Unhandled exception. System.ArgumentException: Boogie program had 2 type errors:
Microsoft.Dafny.BoogieRangeToken: branches of if-then-else have incompatible types DatatypeType and Box
Microsoft.Dafny.BoogieRangeToken: branches of if-then-else have incompatible types DatatypeType and Box
   at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program)
   at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken) in /com.docker.devenvironments.code/Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs:line 65
   at Microsoft.Dafny.Compilation.<>c__DisplayClass54_1.<<VerifyUnverifiedSymbol>b__1>d.MoveNext() in /com.docker.devenvironments.code/Source/DafnyCore/Pipeline/Compilation.cs:line 325
--- 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 /com.docker.devenvironments.code/Source/DafnyCore/Pipeline/Compilation.cs:line 324
   at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed) in /com.docker.devenvironments.code/Source/DafnyCore/Pipeline/Compilation.cs:line 324
   at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed) in /com.docker.devenvironments.code/Source/DafnyCore/Pipeline/Compilation.cs:line 324
   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 124
   at System.Linq.AsyncEnumerable.ToObservableObservable`1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext()
--- 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.QueueUserWorkItemCallbackDefaultContext.Execute()
   at System.Threading.ThreadPoolWorkQueue.Dispatch()
   at System.Threading.PortableThreadPool.WorkerThread.WorkerThreadStart()
   at System.Threading.Thread.StartCallback()

[RustanLeino]

Thanks for the feedback and the example code.

Regarding point 1:

The only way I'm able to reproduce getting an "not assignable" type-checking error is if I use the old type system. To use is with more types (and, in particular, with a type parameter), you must use the new type system (--type-system-refresh). I think this explains the behavior of point 1.

However, even with --type-system-refresh, the code in point 1 revealed some crashes and malformed generated code in the verifier and compilers (some with --general-traits=legacy and some with --general-traits=datatype. I have now fixed those bugs in the new commits.

[RustanLeino]

Regarding point 2:

X.z is not support when X is a type parameter. To reference the static member of the trait T that X extends, write T.z.

[RustanLeino]

Regarding point 3: Thanks. Evidently, this was a problem with if-then-else expressions involving non-reference trait types already in Dafny 4.6.0. I reported the problem in Issue #5570 and fixed it.

[ssomayyajula]

Thanks! Lastly, @ecohen is reporting that the following code...

module Foo.Bar {

trait {:termination false}Dom<T> {
    predicate  has(t:T)
    ghost predicate isMe(r:Dom<T>) 
    function and(d:Dom<T>):(r:Dom<T>) requires isMe(d) ensures isMe(r) 
}
}
module Foo {
import opened Bar
datatype Prod<T, L extends Dom<T>, R extends Dom<T>> extends Dom<T> = Prod(l:L,r:R) {
    
    predicate has(t:T)  { (l as Dom<T>).has(t) && (r as Dom<T>).has(t) } 
    ghost predicate isMe(d:Dom<T>) { 
        && d is Prod<T,L,R> 
        && var d1 := d as Prod<T,L,R>; 
           ((l as Dom<T>).isMe(d1.l) && (r as Dom<T>).isMe(d1.r)) 
    }
    function and(d:Dom<T>):(r:Dom<T>) requires isMe(d) ensures isMe(r) {
        var d1 := d as Prod<T,L,R>;
        var p := Prod((l as Dom<T>).and(d1.l),(r as Dom<T>).and(d1.r));
        assert isMe(p) by {
          assert (l as Dom<T>).isMe(d1.l);
          assert (r as Dom<T>).isMe(d1.r);
        }
        p
    }
}
}

...produces

/root/Test-bounded-poly.dfy(22,15): Error: assertion might not hold
   |
22 |         assert isMe(p) by {
   |                ^^^^^^^

/root/Test-bounded-poly.dfy(22,20): Related location: this proposition could not be proved
   |
22 |         assert isMe(p) by {
   |                     ^

Looks like the wrong token was assigned for the related location?

[ssomayyajula]

So to review:

1. Type parameters are aware of their bounds
2. Parent types to declared types are aware of their bounds (this and above = intro rules)
3. Pre-type inference accounts for type bounds at call sites because that's when type parameters are instantiated (the elim rule)
4. The verifier now emits type bound axioms and boxing is modified to account for bounds
5. There are misc. changes in each backend to account for coercions if necessary

This all looks good to me, esp. since bounded polymorphism is (or should be, at least) a conservative extension to Dafny's type theory.

[RustanLeino]

I added Ernie's new bug report into Issue #5586 and fixed it in PR #5587.