Compatibility with Dafny 4.3, 4.4, and newer

.github/workflows/tests.yml

@@ -13,7 +13,7 @@ jobs:
   verification:
     strategy:
       matrix:
-        version: [ 3.13.1, 4.0.0, 4.1.0, 4.2.0 ]
+        version: [ 3.13.1, 4.0.0, 4.1.0, 4.2.0, 4.3.0, 4.4.0 ]
 
     uses: ./.github/workflows/reusable-tests.yml
     with:

src/Collections/Sequences/MergeSort.dfy

@@ -12,7 +12,7 @@ module {:options "-functionSyntax:4"} Seq.MergeSort {
   import opened Relations
 
   //Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using `MergeSortedWith`
-  function MergeSortBy<T>(a: seq<T>, lessThanOrEq: (T, T) -> bool): (result :seq<T>)
+  function MergeSortBy<T(!new)>(a: seq<T>, lessThanOrEq: (T, T) -> bool): (result :seq<T>)
     requires TotalOrdering(lessThanOrEq)
     ensures multiset(a) == multiset(result)
     ensures SortedBy(result, lessThanOrEq)
@@ -31,7 +31,7 @@ module {:options "-functionSyntax:4"} Seq.MergeSort {
       MergeSortedWith(leftSorted, rightSorted, lessThanOrEq)
   }
 
-  function {:tailrecursion} MergeSortedWith<T>(left: seq<T>, right: seq<T>, lessThanOrEq: (T, T) -> bool) : (result :seq<T>)
+  function {:tailrecursion} MergeSortedWith<T(!new)>(left: seq<T>, right: seq<T>, lessThanOrEq: (T, T) -> bool) : (result :seq<T>)
     requires SortedBy(left, lessThanOrEq)
     requires SortedBy(right, lessThanOrEq)
     requires TotalOrdering(lessThanOrEq)

src/Collections/Sequences/Seq.dfy

@@ -752,11 +752,11 @@ module {:options "-functionSyntax:4"} Seq {
   }
 
   /* inv(b, xs) ==> inv(FoldLeft(f, b, xs), []). */
-  lemma LemmaInvFoldLeft<A,B>(inv: (B, seq<A>) -> bool,
-                              stp: (B, A, B) -> bool,
-                              f: (B, A) -> B,
-                              b: B,
-                              xs: seq<A>)
+  lemma LemmaInvFoldLeft<A(!new),B(!new)>(inv: (B, seq<A>) -> bool,
+                                          stp: (B, A, B) -> bool,
+                                          f: (B, A) -> B,
+                                          b: B,
+                                          xs: seq<A>)
     requires InvFoldLeft(inv, stp)
     requires forall b, a :: stp(b, a, f(b, a))
     requires inv(b, xs)
@@ -810,11 +810,11 @@ module {:options "-functionSyntax:4"} Seq {
   }
 
   /* inv([], b) ==> inv(xs, FoldRight(f, xs, b)) */
-  lemma LemmaInvFoldRight<A,B>(inv: (seq<A>, B) -> bool,
-                               stp: (A, B, B) -> bool,
-                               f: (A, B) -> B,
-                               b: B,
-                               xs: seq<A>)
+  lemma LemmaInvFoldRight<A(!new),B(!new)>(inv: (seq<A>, B) -> bool,
+                                           stp: (A, B, B) -> bool,
+                                           f: (A, B) -> B,
+                                           b: B,
+                                           xs: seq<A>)
     requires InvFoldRight(inv, stp)
     requires forall a, b :: stp(a, b, f(a, b))
     requires inv([], b)
@@ -876,7 +876,7 @@ module {:options "-functionSyntax:4"} Seq {
   }
 
   /* Proves that any two sequences that are sorted by a total order and that have the same elements are equal. */
-  lemma SortedUnique<T>(xs: seq<T>, ys: seq<T>, R: (T, T) -> bool)
+  lemma SortedUnique<T(!new)>(xs: seq<T>, ys: seq<T>, R: (T, T) -> bool)
     requires SortedBy(xs, R)
     requires SortedBy(ys, R)
     requires TotalOrdering(R)
@@ -896,7 +896,7 @@ module {:options "-functionSyntax:4"} Seq {
   }
 
   /* Converts a set to a sequence that is ordered w.r.t. a given total order. */
-  function SetToSortedSeq<T>(s: set<T>, R: (T, T) -> bool): (xs: seq<T>)
+  function SetToSortedSeq<T(!new)>(s: set<T>, R: (T, T) -> bool): (xs: seq<T>)
     requires TotalOrdering(R)
     ensures multiset(s) == multiset(xs)
     ensures SortedBy(xs, R)

src/Relations.dfy

@@ -92,7 +92,7 @@ module {:options "-functionSyntax:4"} Relations {
     max in s && forall x | x in s && R(max, x) :: R(x, max)
   }
 
-  lemma LemmaNewFirstElementStillSortedBy<T>(x: T, s: seq<T>, lessThan: (T, T) -> bool)
+  lemma LemmaNewFirstElementStillSortedBy<T(!new)>(x: T, s: seq<T>, lessThan: (T, T) -> bool)
     requires SortedBy(s, lessThan)
     requires |s| == 0 || lessThan(x, s[0])
     requires TotalOrdering(lessThan)