Add missing (!new) type characteristics (#182)

A bug in Dafny meant these were erroneously unchecked before. Now
they're required (as they always should have been).

Some of the changes are in the `libraries` repository, so this commit
updates that submodule, as well.

Co-authored-by: Aaron Tomb <[email protected]>

StandardLibrary/src/Sets.dfy

@@ -8,11 +8,11 @@ module {:extern "SortedSets"} SortedSets {
   import opened StandardLibrary
   import Seq
 
-  method {:extern "SetToOrderedSequence"} ComputeSetToOrderedSequence<T(==)>(s: set<seq<T>>, less: (T, T) -> bool) returns (res: seq<seq<T>>)
+  method {:extern "SetToOrderedSequence"} ComputeSetToOrderedSequence<T(==, !new)>(s: set<seq<T>>, less: (T, T) -> bool) returns (res: seq<seq<T>>)
     requires Trichotomous(less) && Transitive(less)
     ensures res == SetToOrderedSequence(s, less)
 
-  function method {:extern "SetToOrderedSequence2"} ComputeSetToOrderedSequence2<T(==)>(
+  function method {:extern "SetToOrderedSequence2"} ComputeSetToOrderedSequence2<T(==, !new)>(
     s: set<seq<T>>,
     less: (T, T) -> bool
   )
@@ -25,7 +25,7 @@ module {:extern "SortedSets"} SortedSets {
     ensures forall k <- s :: k in res
     ensures |res| == |s|
 
-  function method {:extern "SetToSequence"} ComputeSetToSequence<T(==)>(
+  function method {:extern "SetToSequence"} ComputeSetToSequence<T(==, !new)>(
     s: set<T>
   )
     : (res: seq<T>)

StandardLibrary/src/Sorting.dfy

@@ -122,7 +122,7 @@ module Sorting {
    * Sorting routines
    */
 
-  method {:vcs_split_on_every_assert} SelectionSort<Data>(a: array<Data>, below: (Data, Data) -> bool)
+  method {:vcs_split_on_every_assert} SelectionSort<Data(!new)>(a: array<Data>, below: (Data, Data) -> bool)
     requires StandardLibrary.Transitive(below)
     requires Connected(below)
     modifies a

StandardLibrary/src/StandardLibrary.dfy

@@ -244,7 +244,7 @@ module StandardLibrary {
     assert LexicographicLessOrEqualAux(a, a, less, |a|);
   }
 
-  lemma LexIsAntisymmetric<T>(a: seq<T>, b: seq<T>, less: (T, T) -> bool)
+  lemma LexIsAntisymmetric<T(!new)>(a: seq<T>, b: seq<T>, less: (T, T) -> bool)
     requires Trich: Trichotomous(less)
     requires LexicographicLessOrEqual(a, b, less)
     requires LexicographicLessOrEqual(b, a, less)
@@ -287,7 +287,7 @@ module StandardLibrary {
     }
   }
 
-  lemma LexIsTransitive<T>(a: seq<T>, b: seq<T>, c: seq<T>, less: (T, T) -> bool)
+  lemma LexIsTransitive<T(!new)>(a: seq<T>, b: seq<T>, c: seq<T>, less: (T, T) -> bool)
     requires Transitive(less)
     requires LexicographicLessOrEqual(a, b, less)
     requires LexicographicLessOrEqual(b, c, less)
@@ -299,7 +299,7 @@ module StandardLibrary {
     assert LexicographicLessOrEqualAux(a, c, less, k);
   }
 
-  lemma LexIsTotal<T>(a: seq<T>, b: seq<T>, less: (T, T) -> bool)
+  lemma LexIsTotal<T(!new)>(a: seq<T>, b: seq<T>, less: (T, T) -> bool)
     requires Trich: Trichotomous(less)
     ensures LexicographicLessOrEqual(a, b, less) || LexicographicLessOrEqual(b, a, less)
   {
@@ -375,23 +375,23 @@ module StandardLibrary {
     forall z :: z in s ==> LexicographicLessOrEqual(a, z, less)
   }
 
-  lemma ThereIsAMinimum<T>(s: set<seq<T>>, less: (T, T) -> bool)
+  lemma ThereIsAMinimum<T(!new)>(s: set<seq<T>>, less: (T, T) -> bool)
     requires s != {}
     requires Trichotomous(less) && Transitive(less)
     ensures exists a :: IsMinimum(a, s, less)
   {
     var a := FindMinimum(s, less);
   }
 
-  lemma MinimumIsUnique<T>(a: seq<T>, b: seq<T>, s: set<seq<T>>, less: (T, T) -> bool)
+  lemma MinimumIsUnique<T(!new)>(a: seq<T>, b: seq<T>, s: set<seq<T>>, less: (T, T) -> bool)
     requires IsMinimum(a, s, less) && IsMinimum(b, s, less)
     requires Trichotomous(less)
     ensures a == b
   {
     LexIsAntisymmetric(a, b, less);
   }
 
-  lemma FindMinimum<T>(s: set<seq<T>>, less: (T, T) -> bool) returns (a: seq<T>)
+  lemma FindMinimum<T(!new)>(s: set<seq<T>>, less: (T, T) -> bool) returns (a: seq<T>)
     requires s != {}
     requires Trichotomous(less) && Transitive(less)
     ensures IsMinimum(a, s, less)