fix: SetToSequence should be a method, not a function (#1035)

* fix: SetToSequence should be a method, not a function

Author: ajewellamz

AwsCryptographicMaterialProviders/runtimes/rust/src/storm_tracker.rs

@@ -70,7 +70,7 @@ pub mod internal_StormTrackingCMC {
                             )});
                         }
                         EmptyWait {} => {
-                            if (crate::Time::_default::CurrentRelativeTimeMilli() <= max_in_flight) {
+                            if crate::Time::_default::CurrentRelativeTimeMilli() <= max_in_flight {
                                 std::thread::sleep(sleep_time);
                             } else {
                                 return std::rc::Rc::new(crate::_Wrappers_Compile::Result::Failure{error :

StandardLibrary/src/Sets.dfy

@@ -25,10 +25,12 @@ module {:extern "SortedSets"} SortedSets {
     ensures forall k <- s :: k in res
     ensures |res| == |s|
 
-  function method {:extern "SetToSequence"} ComputeSetToSequence<T(==, !new)>(
+  // This must be a method, not a function, because the results are not deterministic
+  // It might even return different results for the same input
+  method {:extern "SetToSequence"} ComputeSetToSequence<T(==, !new)>(
     s: set<T>
   )
-    : (res: seq<T>)
+    returns (res: seq<T>)
     ensures Seq.HasNoDuplicates(res)
     ensures forall k <- res :: k in s
     ensures forall k <- s :: k in res

TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/WriteJsonManifests.dfy

@@ -39,7 +39,7 @@ module {:options "-functionSyntax:4"} WriteJsonManifests {
   function EncryptionContextToJson(key: string, m: Types.EncryptionContext)
     : Result<seq<(string, JSON)>, string>
   {
-    var keys := SortedSets.ComputeSetToSequence(m.Keys);
+    var keys := SortedSets.ComputeSetToOrderedSequence2(m.Keys, (a, b) => a < b);
     var pairsBytes
       :- Seq.MapWithResult(
            k requires k in m.Keys =>