chore: Dafny test code changes for Python

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy

@@ -16,9 +16,8 @@ include "UpdateExpr.dfy"
 include "Util.dfy"
 include "Virtual.dfy"
 
-module
-  {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny" }
-  DynamoDbEncryption refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
+module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny" } DynamoDbEncryption
+  refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
 {
   import Operations = AwsCryptographyDbEncryptionSdkDynamoDbOperations
 

DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy

@@ -376,7 +376,8 @@ module DynamoToStructTest {
   //= type=test
   //# Entries in a String Set MUST be ordered in ascending [UTF-16 binary order](./string-ordering.md#utf-16-binary-order).
   method {:test} TestSortSSAttr() {
-    var stringSetValue := AttributeValue.SS(["&","｡","𐀂"]);
+    // "\ud800\udc02" <-> "𐀂"
+    var stringSetValue := AttributeValue.SS(["&","｡","\ud800\udc02"]);
     // Note that string values are UTF-8 encoded, but sorted by UTF-16 encoding.
     var encodedStringSetData := StructuredDataTerminal(value := [
                                                          0,0,0,3, // 3 entries in set
@@ -395,7 +396,8 @@ module DynamoToStructTest {
 
     var newStringSetValue := StructuredToAttr(encodedStringSetData);
     expect newStringSetValue.Success?;
-    expect newStringSetValue.value == AttributeValue.SS(["&","𐀂","｡"]);
+    // "\ud800\udc02" <-> "𐀂"
+    expect newStringSetValue.value == AttributeValue.SS(["&","\ud800\udc02","｡"]);
   }
 
   //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries
@@ -415,11 +417,13 @@ module DynamoToStructTest {
 
   method {:test} TestSetsInListAreSorted() {
     var nSetValue := AttributeValue.NS(["2","1","10"]);
-    var sSetValue := AttributeValue.SS(["&","｡","𐀂"]);
+    // "\ud800\udc02" <-> "𐀂"
+    var sSetValue := AttributeValue.SS(["&","｡","\ud800\udc02"]);
     var bSetValue := AttributeValue.BS([[1,0],[1],[2]]);
 
     var sortedNSetValue := AttributeValue.NS(["1","10","2"]);
-    var sortedSSetValue := AttributeValue.SS(["&","𐀂","｡"]);
+    // "\ud800\udc02" <-> "𐀂"
+    var sortedSSetValue := AttributeValue.SS(["&","\ud800\udc02","｡"]);
     var sortedBSetValue := AttributeValue.BS([[1],[1,0],[2]]);
 
     var listValue := AttributeValue.L([nSetValue, sSetValue, bSetValue]);
@@ -444,11 +448,13 @@ module DynamoToStructTest {
 
   method {:test} TestSetsInMapAreSorted() {
     var nSetValue := AttributeValue.NS(["2","1","10"]);
-    var sSetValue := AttributeValue.SS(["&","｡","𐀂"]);
+    // "\ud800\udc02" <-> "𐀂"
+    var sSetValue := AttributeValue.SS(["&","｡","\ud800\udc02"]);
     var bSetValue := AttributeValue.BS([[1,0],[1],[2]]);
 
     var sortedNSetValue := AttributeValue.NS(["1","10","2"]);
-    var sortedSSetValue := AttributeValue.SS(["&","𐀂","｡"]);
+    // "\ud800\udc02" <-> "𐀂"
+    var sortedSSetValue := AttributeValue.SS(["&","\ud800\udc02","｡"]);
     var sortedBSetValue := AttributeValue.BS([[1],[1,0],[2]]);
 
     var mapValue := AttributeValue.M(map["keyA" := sSetValue, "keyB" := nSetValue, "keyC" := bSetValue]);
@@ -490,7 +496,8 @@ module DynamoToStructTest {
   method {:test} TestSortMapKeys() {
     var nullValue := AttributeValue.NULL(true);
 
-    var mapValue := AttributeValue.M(map["&" := nullValue, "｡" := nullValue, "𐀂" := nullValue]);
+    // "\ud800\udc02" <-> "𐀂"
+    var mapValue := AttributeValue.M(map["&" := nullValue, "｡" := nullValue, "\ud800\udc02" := nullValue]);
 
     // Note that the string values are encoded as UTF-8, but are sorted according to UTF-16 encoding.
     var encodedMapData := StructuredDataTerminal(

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy

@@ -5,9 +5,8 @@ include "DdbMiddlewareConfig.dfy"
 include "AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations.dfy"
 include "../../DynamoDbEncryption/src/ConfigToInfo.dfy"
 
-module
-  {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transforms.internaldafny" }
-  DynamoDbEncryptionTransforms refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
+module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transforms.internaldafny" } DynamoDbEncryptionTransforms
+  refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
 {
   import opened DdbMiddlewareConfig
   import opened StandardLibrary

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy

@@ -4,9 +4,8 @@
 include "AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy"
 include "Util.dfy"
 
-module
-  {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny" }
-  DynamoDbItemEncryptor refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService
+module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny" } DynamoDbItemEncryptor
+  refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService
 {
   import opened DynamoDbItemEncryptorUtil
   import StructuredEncryption

DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy

@@ -3,9 +3,8 @@
 
 include "AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy"
 
-module
-  {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny" }
-  StructuredEncryption refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionService
+module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny" } StructuredEncryption
+  refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionService
 {
 
   import Operations = AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations

TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy

@@ -218,11 +218,11 @@ module {:options "-functionSyntax:4"} WriteManifest {
   const DoNothing : CryptoAction := 3
 
   const A : string := "A"
-  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
+  const B : string := "\ud000" // "Ud000" <-> "퀀"
+  const C : string := "\ufe4c" // "Ufe4c" <-> "﹌"
+  const D : string := "\u10001" // "U10001" <-> "𐀁" (surrogate pair: "\uD800\uDC01")
+  const E : string := "\u10002" // "U10002" <-> "𐀂" (same high surrogate as D: "\uD800\uDC02")
+  const F : string := "\u20002" // "U20002" <-> "𠀂"  (different high surrogate as D: "\D840\uDC02")
 
   lemma CheckLengths()
     ensures |A| == 1