update

aws · Nov 13, 2024 · d5cd793 · d5cd793
1 parent c0e0d45
commit d5cd793
Showing 1 changed file with 0 additions and 6 deletions.
diff --git a/TestVectors/dafny/TestVectors/src/WriteVectors.dfy b/TestVectors/dafny/TestVectors/src/WriteVectors.dfy
@@ -65,7 +65,6 @@ module {:options "-functionSyntax:4"} WriteVectors {
     var allTests :- getVersionTests(version);
 
     var tests := SortedSets.ComputeSetToSequence(allTests);
-    :- Need(TestVectorListHasNoDuplicates(tests), "Error: Duplicate in test vectors");
 
     DescriptionLessThanIsTotal();
     var sortedTests := MergeSortBy(tests, DescriptionLessThan);
@@ -162,11 +161,6 @@ module {:options "-functionSyntax:4"} WriteVectors {
     case _ => Failure("Only version 4 of generate manifest is supported\n")
   }
 
-  predicate TestVectorListHasNoDuplicates(xs: seq<EsdkTestVectors.EsdkEncryptTestVector>)
-  {
-    forall i, j :: 0 <= i < j < |xs| ==> xs[i].description != xs[j].description
-  }
-
   predicate DescriptionLessThan(x: EsdkTestVectors.EsdkEncryptTestVector, y: EsdkTestVectors.EsdkEncryptTestVector) {
     Below(x.description, y.description)
   }