m

ajewellamz · ajewellamz · commit 4b0c56da7cc7 · 2025-04-29T15:37:50.000-07:00
diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -665,13 +665,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         results[i] := FullSearch(client, queries[i]);
       }
 
-      var configs := tableEncryptionConfigs.Keys;
-      while configs != {}
-        decreases |configs|
-        invariant forall k <- configs :: k in tableEncryptionConfigs
+      var configs := SortedSets.ComputeSetToOrderedSequence2(tableEncryptionConfigs.Keys, CharLess);
+      for i := 0 to |configs|
       {
-        var config :| config in configs;
-        configs := configs - { config };
+        var config := configs[i];
         BasicQueryTestConfig(tableEncryptionConfigs[config], results, globalRecords);
       }
     }

Original file line number	Diff line number	Diff line change
`@@ -665,13 +665,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {`
`665`	`665`	`results[i] := FullSearch(client, queries[i]);`
`666`	`666`	`}`
`667`	`667`
`668`		`- var configs := tableEncryptionConfigs.Keys;`
`669`		`- while configs != {}`
`670`		`- decreases \|configs\|`
`671`		`- invariant forall k <- configs :: k in tableEncryptionConfigs`
	`668`	`+ var configs := SortedSets.ComputeSetToOrderedSequence2(tableEncryptionConfigs.Keys, CharLess);`
	`669`	`+ for i := 0 to \|configs\|`
`672`	`670`	`{`
`673`		`- var config :\| config in configs;`
`674`		`- configs := configs - { config };`
	`671`	`+ var config := configs[i];`
`675`	`672`	`BasicQueryTestConfig(tableEncryptionConfigs[config], results, globalRecords);`
`676`	`673`	`}`
`677`	`674`	`}`