fix: for test vectors, use SetToSequenceSorted (#1034)

aws · Nov 21, 2024 · 21ad206 · 21ad206
1 parent 5a7ddbf
commit 21ad206
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 8 deletions.
diff --git a/...fny/TestVectorsAwsCryptographicMaterialProviders/src/VectorsComposition/AllDefaultCmm.dfy b/...fny/TestVectorsAwsCryptographicMaterialProviders/src/VectorsComposition/AllDefaultCmm.dfy
@@ -92,7 +92,7 @@ module {:options "-functionSyntax:4"} AllDefaultCmm {
           encryptDescription := RawAesKeyring,
           decryptDescription := RawAesKeyring,
           encryptionContext := encryptionContext,
-          requiredEncryptionContextKeys := Some(SortedSets.ComputeSetToSequence(requiredEncryptionContextKeys)),
+          requiredEncryptionContextKeys := Some(SortedSets.ComputeSetToOrderedSequence2(requiredEncryptionContextKeys, (a, b) => a < b)),
           reproducedEncryptionContext := Some(reproducedEncryptionContext)
         )
 
@@ -127,7 +127,7 @@ module {:options "-functionSyntax:4"} AllDefaultCmm {
           encryptDescription := RawAesKeyring,
           decryptDescription := RawAesKeyring,
           encryptionContext := encryptionContext,
-          requiredEncryptionContextKeys := Some(SortedSets.ComputeSetToSequence(requiredEncryptionContextKeys)),
+          requiredEncryptionContextKeys := Some(SortedSets.ComputeSetToOrderedSequence2(requiredEncryptionContextKeys, (a, b) => a < b)),
           reproducedEncryptionContext := Some(reproducedEncryptionContext)
         )
 

diff --git a/...CryptographicMaterialProviders/src/VectorsComposition/AllRequiredEncryptionContextCmm.dfy b/...CryptographicMaterialProviders/src/VectorsComposition/AllRequiredEncryptionContextCmm.dfy
@@ -56,17 +56,17 @@ module {:options "-functionSyntax:4"} AllRequiredEncryptionContextCmm {
           encryptDescription := KeyVectorsTypes.RequiredEncryptionContext(
             KeyVectorsTypes.RequiredEncryptionContextCMM(
               underlying := AllDefaultCmm.RawAesKeyring,
-              requiredEncryptionContextKeys := SortedSets.ComputeSetToSequence(requiredEncryptionContextKeys)
+              requiredEncryptionContextKeys := SortedSets.ComputeSetToOrderedSequence2(requiredEncryptionContextKeys, (a, b) => a < b)
             )
           ),
           decryptDescription := KeyVectorsTypes.RequiredEncryptionContext(
             KeyVectorsTypes.RequiredEncryptionContextCMM(
               underlying := AllDefaultCmm.RawAesKeyring,
-              requiredEncryptionContextKeys := SortedSets.ComputeSetToSequence(requiredEncryptionContextKeys)
+              requiredEncryptionContextKeys := SortedSets.ComputeSetToOrderedSequence2(requiredEncryptionContextKeys, (a, b) => a < b)
             )
           ),
           encryptionContext := encryptionContext,
-          requiredEncryptionContextKeys := Some(SortedSets.ComputeSetToSequence(requiredEncryptionContextKeys)),
+          requiredEncryptionContextKeys := Some(SortedSets.ComputeSetToOrderedSequence2(requiredEncryptionContextKeys, (a, b) => a < b)),
           reproducedEncryptionContext := Some(reproducedEncryptionContext)
         )
 
@@ -102,17 +102,17 @@ module {:options "-functionSyntax:4"} AllRequiredEncryptionContextCmm {
           encryptDescription := KeyVectorsTypes.RequiredEncryptionContext(
             KeyVectorsTypes.RequiredEncryptionContextCMM(
               underlying := AllDefaultCmm.RawAesKeyring,
-              requiredEncryptionContextKeys := SortedSets.ComputeSetToSequence(requiredEncryptionContextKeys)
+              requiredEncryptionContextKeys := SortedSets.ComputeSetToOrderedSequence2(requiredEncryptionContextKeys, (a, b) => a < b)
             )
           ),
           decryptDescription := KeyVectorsTypes.RequiredEncryptionContext(
             KeyVectorsTypes.RequiredEncryptionContextCMM(
               underlying := AllDefaultCmm.RawAesKeyring,
-              requiredEncryptionContextKeys := SortedSets.ComputeSetToSequence(requiredEncryptionContextKeys)
+              requiredEncryptionContextKeys := SortedSets.ComputeSetToOrderedSequence2(requiredEncryptionContextKeys, (a, b) => a < b)
             )
           ),
           encryptionContext := encryptionContext,
-          requiredEncryptionContextKeys := Some(SortedSets.ComputeSetToSequence(requiredEncryptionContextKeys)),
+          requiredEncryptionContextKeys := Some(SortedSets.ComputeSetToOrderedSequence2(requiredEncryptionContextKeys, (a, b) => a < b)),
           reproducedEncryptionContext := Some(reproducedEncryptionContext)
         )
   // These are only required encryption context vectors with static aes keyrings