chore: add more tests to ComputeSetToOrderedSequence (#111)

StandardLibrary/test/TestComputeSetToOrderedSequenceCharLess.dfy

@@ -0,0 +1,105 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "../src/StandardLibrary.dfy"
+include "../src/Sets.dfy"
+  // Just to make sure we don't conflict with dafny-lang/libraries' Sets.dfy
+include "../../libraries/src/Collections/Sets/Sets.dfy"
+
+
+// This function is commonly used for sorting
+// But there are also subtle order effects
+// that are important for cryptographic libraries.
+// These order functions and externs MUST
+// be interoperable across runtimes
+// to be used for canonical ordering
+
+module TestComputeSetToOrderedSequenceCharLess {
+  import opened StandardLibrary
+  import opened UInt = StandardLibrary.UInt
+  import opened SortedSets
+
+  predicate method CharLess(x : char, y : char)
+  {
+    x < y
+  }
+
+  predicate method CharGreater(x : char, y : char) {
+    y < x
+  }
+
+  method {:test} TestSetToOrderedSequenceEmpty() {
+    var output := ComputeSetToOrderedSequence({}, CharLess);
+    var output2 := ComputeSetToOrderedSequence2({}, CharLess);
+    var expected := [];
+    expect output == expected;
+    expect output2 == expected;
+  }
+
+  method {:test} TestSetToOrderedSequenceOneItem() {
+    var a := {"a"};
+    var output := ComputeSetToOrderedSequence(a, CharLess);
+    var output2 := ComputeSetToOrderedSequence2(a, CharLess);
+    var expected := ["a"];
+    expect output == expected;
+    expect output2 == expected;
+  }
+
+  method {:test} TestSetToOrderedSequenceSimple() {
+    var a := {"ac", "ab"};
+    var output := ComputeSetToOrderedSequence(a, CharLess);
+    var output2 := ComputeSetToOrderedSequence2(a, CharLess);
+    var expected := ["ab", "ac"];
+    expect output == expected;
+    expect output2 == expected;
+  }
+
+  method {:test} TestSetToOrderedSequencePrefix() {
+    var a := {"abc", "ab"};
+    var output := ComputeSetToOrderedSequence(a, CharLess);
+    var output2 := ComputeSetToOrderedSequence2(a, CharLess);
+    var expected := ["ab", "abc"];
+    expect output == expected;
+    expect output2 == expected;
+  }
+
+  method {:test} TestSetToOrderedSequenceComplex() {
+    var a := {"abc", "bbc", "ab"};
+    var output := ComputeSetToOrderedSequence(a, CharLess);
+    var output2 := ComputeSetToOrderedSequence2(a, CharLess);
+    var expected := ["ab", "abc", "bbc"];
+    expect output == expected;
+    expect output2 == expected;
+  }
+
+  method {:test} TestSetToOrderedSequenceComplexReverse() {
+    var a := {"abc", "bbc", "ab"};
+    var output := ComputeSetToOrderedSequence(a, CharGreater);
+    var output2 := ComputeSetToOrderedSequence2(a, CharGreater);
+    var expected := ["bbc", "ab", "abc"];
+    expect output == expected;
+    expect output2 == expected;
+  }
+
+  method {:test} TestSetSequence() {
+    var a :=  {"abc", "bbc", "ab"};
+    var output := ComputeSetToSequence(a);
+    expect multiset(output) == multiset(a);
+  }
+
+  method {:test} TestSetToOrderedComplexUnicode() {
+    var a := {"𐐷", "&", "Љ", "ᝀ", "🂡", "｡", "𐀂"};
+    var output := ComputeSetToOrderedSequence(a, CharLess);
+    var output2 := ComputeSetToOrderedSequence2(a, CharLess);
+    var expected := ["&", "Љ", "ᝀ", "𐀂", "𐐷", "🂡", "｡"];
+    // This is the pure logographic order
+    // however this function is used in the DB-ESDK
+    // to canonicalized sets and needs to remain the same.
+    // This order is kept here so that it is clear that this order is incorrect in this case
+    // var expected := ["&", "Љ", "ᝀ", "｡", "𐀂", "𐐷", "🂡"];
+    expect output == expected;
+    expect output2 == expected;
+  }
+
+
+}

StandardLibrary/test/Sets.dfy → StandardLibrary/test/TestComputeSetToOrderedSequenceUInt8Less.dfy

@@ -6,7 +6,14 @@ include "../src/Sets.dfy"
   // Just to make sure we don't conflict with dafny-lang/libraries' Sets.dfy
 include "../../libraries/src/Collections/Sets/Sets.dfy"
 
-module TestSeqReaderReadElements {
+// This function is commonly used for sorting
+// But there are also subtle order effects
+// that are important for cryptographic libraries.
+// These order functions and externs MUST
+// be interoperable across runtimes
+// to be used for canonical ordering
+
+module TestComputeSetToOrderedSequenceUInt8Less {
   import opened StandardLibrary
   import opened UInt = StandardLibrary.UInt
   import opened SortedSets
@@ -17,43 +24,55 @@ module TestSeqReaderReadElements {
 
   method {:test} TestSetToOrderedSequenceEmpty() {
     var output := ComputeSetToOrderedSequence({}, UInt8Less);
+    var output2 := ComputeSetToOrderedSequence2({}, UInt8Less);
     var expected := [];
     expect output == expected;
+    expect output2 == expected;
   }
 
   method {:test} TestSetToOrderedSequenceOneItem() {
     var a := {[0]};
     var output := ComputeSetToOrderedSequence(a, UInt8Less);
+    var output2 := ComputeSetToOrderedSequence2(a, UInt8Less);
     var expected := [[0]];
     expect output == expected;
+    expect output2 == expected;
   }
 
   method {:test} TestSetToOrderedSequenceSimple() {
     var a := {[0, 2], [0, 1]};
     var output := ComputeSetToOrderedSequence(a, UInt8Less);
+    var output2 := ComputeSetToOrderedSequence2(a, UInt8Less);
     var expected := [[0, 1], [0, 2]];
     expect output == expected;
+    expect output2 == expected;
   }
 
   method {:test} TestSetToOrderedSequencePrefix() {
     var a := {[0, 1, 2], [0, 1]};
     var output := ComputeSetToOrderedSequence(a, UInt8Less);
+    var output2 := ComputeSetToOrderedSequence2(a, UInt8Less);
     var expected := [[0, 1], [0, 1, 2]];
     expect output == expected;
+    expect output2 == expected;
   }
 
   method {:test} TestSetToOrderedSequenceComplex() {
     var a := {[0, 1, 2], [1, 1, 2], [0, 1]};
     var output := ComputeSetToOrderedSequence(a, UInt8Less);
+    var output2 := ComputeSetToOrderedSequence2(a, UInt8Less);
     var expected := [[0, 1], [0, 1, 2], [1, 1, 2]];
     expect output == expected;
+    expect output2 == expected;
   }
 
   method {:test} TestSetToOrderedSequenceComplexReverse() {
     var a := {[0, 1, 2], [1, 1, 2], [0, 1]};
     var output := ComputeSetToOrderedSequence(a, UInt8Greater);
+    var output2 := ComputeSetToOrderedSequence2(a, UInt8Greater);
     var expected := [[1, 1, 2], [0, 1], [0, 1, 2]];
     expect output == expected;
+    expect output2 == expected;
   }
 
   method {:test} TestSetSequence() {
@@ -65,8 +84,10 @@ module TestSeqReaderReadElements {
   method {:test} TestSetToOrderedSequenceManyItems() {
     var a := set x:uint16 | 0 <= x < 0xFFFF :: UInt16ToSeq(x);
     var output := ComputeSetToOrderedSequence(a, UInt8Less);
+    var output2 := ComputeSetToOrderedSequence2(a, UInt8Less);
     var expected : seq<seq<uint8>> := seq(0xFFFF, i requires 0 <= i < 0xFFFF => UInt16ToSeq(i as uint16));
     expect output == expected;
+    expect output2 == expected;
   }
 
 }