m

Author: lucasmcdonald3

TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy

@@ -218,21 +218,20 @@ module {:options "-functionSyntax:4"} WriteManifest {
   const DoNothing : CryptoAction := 3
 
   const A : string := "A"
-  const B : string := "\ud000" // Ud000"
-  const C : string := "\ufe4c" // Ufe4c"
-  const D : string := "\u100001" // U10001
-  const E : string := "\u100002" // U10002 - same high surrogate as D
-  const F : string := "\u200002" // U20002 - different high surrogate as D
+  const B : string := "퀀" // Ud000"
+  const C : string := "﹌" // Ufe4c"
+  const D : string := "𐀁" // U10001
+  const E : string := "𐀂" // U10002 - same high surrogate as D
+  const F : string := "𠀂" // U20002 - different high surrogate as D
 
-  // Dafny doesn't handle unicode surrogates correctly.
-  // lemma CheckLengths()
-  //   ensures |A| == 1
-  //   ensures |B| == 1
-  //   ensures |C| == 1
-  //   ensures |D| == 2
-  //   ensures |E| == 2
-  //   ensures |F| == 2
-  // {}
+  lemma CheckLengths()
+    ensures |A| == 1
+    ensures |B| == 1
+    ensures |C| == 1
+    ensures |D| == 2
+    ensures |E| == 2
+    ensures |F| == 2
+  {}
 
   // Let's make attribute names with complex characters.
   // It shouldn't matter, but let's make sure