From 56401097d8ebf2fd1e07b887a8c8d8a33e237fc8 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 27 May 2025 13:53:25 -0700 Subject: [PATCH 1/8] sync --- .../dafny/DynamoDbEncryption/src/Index.dfy | 5 ++-- .../test/DynamoToStruct.dfy | 18 ++++++------- .../src/Index.dfy | 5 ++-- .../dafny/DynamoDbItemEncryptor/src/Index.dfy | 5 ++-- .../dafny/StructuredEncryption/src/Index.dfy | 5 ++-- .../dafny/DDBEncryption/src/WriteManifest.dfy | 27 ++++++++++--------- 6 files changed, 31 insertions(+), 34 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy index 8faa05326..13624c005 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy +++ b/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 diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy index 223678b96..14aa730a3 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy @@ -376,14 +376,14 @@ 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(["&","｡","𐀂"]); + 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 0,0,0,1, // 1st entry is 1 byte 0x26, // "&" in UTF-8 encoding 0,0,0,4, // 2nd entry is 4 bytes - 0xF0,0x90,0x80,0x82, // "𐀂" in UTF-8 encoding + 0xF0,0x90,0x80,0x82, // "\ud800\udc02" in UTF-8 encoding 0,0,0,3, // 3rd entry is 3 bytes 0xEF,0xBD,0xA1 // "｡" in UTF-8 encoding ], @@ -395,7 +395,7 @@ module DynamoToStructTest { var newStringSetValue := StructuredToAttr(encodedStringSetData); expect newStringSetValue.Success?; - expect newStringSetValue.value == AttributeValue.SS(["&","𐀂","｡"]); + expect newStringSetValue.value == AttributeValue.SS(["&","\ud800\udc02","｡"]); } //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries @@ -415,11 +415,11 @@ module DynamoToStructTest { method {:test} TestSetsInListAreSorted() { var nSetValue := AttributeValue.NS(["2","1","10"]); - var sSetValue := AttributeValue.SS(["&","｡","𐀂"]); + 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(["&","𐀂","｡"]); + var sortedSSetValue := AttributeValue.SS(["&","\ud800\udc02","｡"]); var sortedBSetValue := AttributeValue.BS([[1],[1,0],[2]]); var listValue := AttributeValue.L([nSetValue, sSetValue, bSetValue]); @@ -444,11 +444,11 @@ module DynamoToStructTest { method {:test} TestSetsInMapAreSorted() { var nSetValue := AttributeValue.NS(["2","1","10"]); - var sSetValue := AttributeValue.SS(["&","｡","𐀂"]); + 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(["&","𐀂","｡"]); + 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 +490,7 @@ module DynamoToStructTest { method {:test} TestSortMapKeys() { var nullValue := AttributeValue.NULL(true); - var mapValue := AttributeValue.M(map["&" := nullValue, "｡" := nullValue, "𐀂" := nullValue]); + 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( @@ -500,7 +500,7 @@ module DynamoToStructTest { 0x26, // "&" UTF-8 encoded 0,0, 0,0,0,0, // null value 0,1, 0,0,0,4, // 2nd key is a string 4 bytes long - 0xF0, 0x90, 0x80, 0x82, // "𐀂" UTF-8 encoded + 0xF0, 0x90, 0x80, 0x82, // "\ud800\udc02" UTF-8 encoded 0,0, 0,0,0,0, // null value 0,1, 0,0,0,3, // 3rd key is a string 3 bytes long 0xEF, 0xBD, 0xA1, // "｡" diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy index 83e19fb0a..b82f33140 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy +++ b/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 diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy index 1ee469bab..4c207afad 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy +++ b/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 diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy index 19533014a..5b6d2271b 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy +++ b/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 diff --git a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy index 1e668a2de..0339bad1d 100644 --- a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy +++ b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy @@ -218,20 +218,21 @@ 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 := "\u100001" // U10001 + const E : string := "\u100002" // U10002 - same high surrogate as D + const F : string := "\u200002" // U20002 - different high surrogate as D - lemma CheckLengths() - ensures |A| == 1 - ensures |B| == 1 - ensures |C| == 1 - ensures |D| == 2 - ensures |E| == 2 - ensures |F| == 2 - {} + // 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 + // {} // Let's make attribute names with complex characters. // It shouldn't matter, but let's make sure From 03411bc0080bd59e275d52fa58f75585f807775b Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 27 May 2025 14:09:08 -0700 Subject: [PATCH 2/8] m --- .../test/DynamoToStruct.dfy | 7 +++++ .../dafny/DDBEncryption/src/WriteManifest.dfy | 26 +++++++++---------- 2 files changed, 20 insertions(+), 13 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy index 14aa730a3..aaaffbaeb 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy @@ -376,6 +376,7 @@ 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() { + // "\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 := [ @@ -395,6 +396,7 @@ module DynamoToStructTest { var newStringSetValue := StructuredToAttr(encodedStringSetData); expect newStringSetValue.Success?; + // "\ud800\udc02" <-> "𐀂" expect newStringSetValue.value == AttributeValue.SS(["&","\ud800\udc02","｡"]); } @@ -415,10 +417,12 @@ module DynamoToStructTest { method {:test} TestSetsInListAreSorted() { var nSetValue := AttributeValue.NS(["2","1","10"]); + // "\ud800\udc02" <-> "𐀂" var sSetValue := AttributeValue.SS(["&","｡","\ud800\udc02"]); var bSetValue := AttributeValue.BS([[1,0],[1],[2]]); var sortedNSetValue := AttributeValue.NS(["1","10","2"]); + // "\ud800\udc02" <-> "𐀂" var sortedSSetValue := AttributeValue.SS(["&","\ud800\udc02","｡"]); var sortedBSetValue := AttributeValue.BS([[1],[1,0],[2]]); @@ -444,10 +448,12 @@ module DynamoToStructTest { method {:test} TestSetsInMapAreSorted() { var nSetValue := AttributeValue.NS(["2","1","10"]); + // "\ud800\udc02" <-> "𐀂" var sSetValue := AttributeValue.SS(["&","｡","\ud800\udc02"]); var bSetValue := AttributeValue.BS([[1,0],[1],[2]]); var sortedNSetValue := AttributeValue.NS(["1","10","2"]); + // "\ud800\udc02" <-> "𐀂" var sortedSSetValue := AttributeValue.SS(["&","\ud800\udc02","｡"]); var sortedBSetValue := AttributeValue.BS([[1],[1,0],[2]]); @@ -490,6 +496,7 @@ module DynamoToStructTest { method {:test} TestSortMapKeys() { var nullValue := AttributeValue.NULL(true); + // "\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. diff --git a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy index 0339bad1d..dbb95f86d 100644 --- a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy +++ b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy @@ -218,21 +218,21 @@ 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" // "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" // 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 From 7d96dc0398ff034d2e6b65f355f78ea14aaf1703 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 27 May 2025 14:09:56 -0700 Subject: [PATCH 3/8] m --- TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy | 1 - 1 file changed, 1 deletion(-) diff --git a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy index dbb95f86d..7c1afb4b9 100644 --- a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy +++ b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy @@ -224,7 +224,6 @@ module {:options "-functionSyntax:4"} WriteManifest { const E : string := "\u10002" // "U10002" <-> "𐀂" (same high surrogate as D: "\uD800\uDC02") const F : string := "\u20002" // "U20002" <-> "𠀂" (different high surrogate as D: "\D840\uDC02" - // Dafny doesn't handle unicode surrogates correctly. lemma CheckLengths() ensures |A| == 1 ensures |B| == 1 From a0c39c8afa3af7dd62ca87123bc884c7b924b718 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 27 May 2025 14:10:29 -0700 Subject: [PATCH 4/8] m --- TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy index 7c1afb4b9..2f6e3a112 100644 --- a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy +++ b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy @@ -222,7 +222,7 @@ module {:options "-functionSyntax:4"} WriteManifest { 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" + const F : string := "\u20002" // "U20002" <-> "𠀂" (different high surrogate as D: "\D840\uDC02") lemma CheckLengths() ensures |A| == 1 From d75b611f04867cc56cb4aec5d95dfd2b5fd83428 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 27 May 2025 14:12:07 -0700 Subject: [PATCH 5/8] m --- .../dafny/DynamoDbEncryption/test/DynamoToStruct.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy index aaaffbaeb..ec8ce9dcc 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy @@ -384,7 +384,7 @@ module DynamoToStructTest { 0,0,0,1, // 1st entry is 1 byte 0x26, // "&" in UTF-8 encoding 0,0,0,4, // 2nd entry is 4 bytes - 0xF0,0x90,0x80,0x82, // "\ud800\udc02" in UTF-8 encoding + 0xF0,0x90,0x80,0x82, // "𐀂" in UTF-8 encoding 0,0,0,3, // 3rd entry is 3 bytes 0xEF,0xBD,0xA1 // "｡" in UTF-8 encoding ], @@ -507,7 +507,7 @@ module DynamoToStructTest { 0x26, // "&" UTF-8 encoded 0,0, 0,0,0,0, // null value 0,1, 0,0,0,4, // 2nd key is a string 4 bytes long - 0xF0, 0x90, 0x80, 0x82, // "\ud800\udc02" UTF-8 encoded + 0xF0, 0x90, 0x80, 0x82, // "𐀂" UTF-8 encoded 0,0, 0,0,0,0, // null value 0,1, 0,0,0,3, // 3rd key is a string 3 bytes long 0xEF, 0xBD, 0xA1, // "｡" From 0f79ecc463f3e0d397f78f0bc3cbc9c3e20ce3a0 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Wed, 28 May 2025 14:07:38 -0700 Subject: [PATCH 6/8] sync --- .../test/DynamoToStruct.dfy | 11 ++------ .../dafny/DDBEncryption/src/WriteManifest.dfy | 27 ++++++++++--------- 2 files changed, 16 insertions(+), 22 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy index ec8ce9dcc..14aa730a3 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy @@ -376,7 +376,6 @@ 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() { - // "\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 := [ @@ -384,7 +383,7 @@ module DynamoToStructTest { 0,0,0,1, // 1st entry is 1 byte 0x26, // "&" in UTF-8 encoding 0,0,0,4, // 2nd entry is 4 bytes - 0xF0,0x90,0x80,0x82, // "𐀂" in UTF-8 encoding + 0xF0,0x90,0x80,0x82, // "\ud800\udc02" in UTF-8 encoding 0,0,0,3, // 3rd entry is 3 bytes 0xEF,0xBD,0xA1 // "｡" in UTF-8 encoding ], @@ -396,7 +395,6 @@ module DynamoToStructTest { var newStringSetValue := StructuredToAttr(encodedStringSetData); expect newStringSetValue.Success?; - // "\ud800\udc02" <-> "𐀂" expect newStringSetValue.value == AttributeValue.SS(["&","\ud800\udc02","｡"]); } @@ -417,12 +415,10 @@ module DynamoToStructTest { method {:test} TestSetsInListAreSorted() { var nSetValue := AttributeValue.NS(["2","1","10"]); - // "\ud800\udc02" <-> "𐀂" var sSetValue := AttributeValue.SS(["&","｡","\ud800\udc02"]); var bSetValue := AttributeValue.BS([[1,0],[1],[2]]); var sortedNSetValue := AttributeValue.NS(["1","10","2"]); - // "\ud800\udc02" <-> "𐀂" var sortedSSetValue := AttributeValue.SS(["&","\ud800\udc02","｡"]); var sortedBSetValue := AttributeValue.BS([[1],[1,0],[2]]); @@ -448,12 +444,10 @@ module DynamoToStructTest { method {:test} TestSetsInMapAreSorted() { var nSetValue := AttributeValue.NS(["2","1","10"]); - // "\ud800\udc02" <-> "𐀂" var sSetValue := AttributeValue.SS(["&","｡","\ud800\udc02"]); var bSetValue := AttributeValue.BS([[1,0],[1],[2]]); var sortedNSetValue := AttributeValue.NS(["1","10","2"]); - // "\ud800\udc02" <-> "𐀂" var sortedSSetValue := AttributeValue.SS(["&","\ud800\udc02","｡"]); var sortedBSetValue := AttributeValue.BS([[1],[1,0],[2]]); @@ -496,7 +490,6 @@ module DynamoToStructTest { method {:test} TestSortMapKeys() { var nullValue := AttributeValue.NULL(true); - // "\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. @@ -507,7 +500,7 @@ module DynamoToStructTest { 0x26, // "&" UTF-8 encoded 0,0, 0,0,0,0, // null value 0,1, 0,0,0,4, // 2nd key is a string 4 bytes long - 0xF0, 0x90, 0x80, 0x82, // "𐀂" UTF-8 encoded + 0xF0, 0x90, 0x80, 0x82, // "\ud800\udc02" UTF-8 encoded 0,0, 0,0,0,0, // null value 0,1, 0,0,0,3, // 3rd key is a string 3 bytes long 0xEF, 0xBD, 0xA1, // "｡" diff --git a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy index 2f6e3a112..0339bad1d 100644 --- a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy +++ b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy @@ -218,20 +218,21 @@ 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 := "\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") + 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 - lemma CheckLengths() - ensures |A| == 1 - ensures |B| == 1 - ensures |C| == 1 - ensures |D| == 2 - ensures |E| == 2 - ensures |F| == 2 - {} + // 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 + // {} // Let's make attribute names with complex characters. // It shouldn't matter, but let's make sure From 1b4c1c46421df29df2099c1f59bbb6a5ee9e1474 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Wed, 28 May 2025 14:09:52 -0700 Subject: [PATCH 7/8] sync --- .../test/DynamoToStruct.dfy | 11 ++++++-- .../dafny/DDBEncryption/src/WriteManifest.dfy | 27 +++++++++---------- 2 files changed, 22 insertions(+), 16 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy index 14aa730a3..ec8ce9dcc 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy @@ -376,6 +376,7 @@ 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() { + // "\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 := [ @@ -383,7 +384,7 @@ module DynamoToStructTest { 0,0,0,1, // 1st entry is 1 byte 0x26, // "&" in UTF-8 encoding 0,0,0,4, // 2nd entry is 4 bytes - 0xF0,0x90,0x80,0x82, // "\ud800\udc02" in UTF-8 encoding + 0xF0,0x90,0x80,0x82, // "𐀂" in UTF-8 encoding 0,0,0,3, // 3rd entry is 3 bytes 0xEF,0xBD,0xA1 // "｡" in UTF-8 encoding ], @@ -395,6 +396,7 @@ module DynamoToStructTest { var newStringSetValue := StructuredToAttr(encodedStringSetData); expect newStringSetValue.Success?; + // "\ud800\udc02" <-> "𐀂" expect newStringSetValue.value == AttributeValue.SS(["&","\ud800\udc02","｡"]); } @@ -415,10 +417,12 @@ module DynamoToStructTest { method {:test} TestSetsInListAreSorted() { var nSetValue := AttributeValue.NS(["2","1","10"]); + // "\ud800\udc02" <-> "𐀂" var sSetValue := AttributeValue.SS(["&","｡","\ud800\udc02"]); var bSetValue := AttributeValue.BS([[1,0],[1],[2]]); var sortedNSetValue := AttributeValue.NS(["1","10","2"]); + // "\ud800\udc02" <-> "𐀂" var sortedSSetValue := AttributeValue.SS(["&","\ud800\udc02","｡"]); var sortedBSetValue := AttributeValue.BS([[1],[1,0],[2]]); @@ -444,10 +448,12 @@ module DynamoToStructTest { method {:test} TestSetsInMapAreSorted() { var nSetValue := AttributeValue.NS(["2","1","10"]); + // "\ud800\udc02" <-> "𐀂" var sSetValue := AttributeValue.SS(["&","｡","\ud800\udc02"]); var bSetValue := AttributeValue.BS([[1,0],[1],[2]]); var sortedNSetValue := AttributeValue.NS(["1","10","2"]); + // "\ud800\udc02" <-> "𐀂" var sortedSSetValue := AttributeValue.SS(["&","\ud800\udc02","｡"]); var sortedBSetValue := AttributeValue.BS([[1],[1,0],[2]]); @@ -490,6 +496,7 @@ module DynamoToStructTest { method {:test} TestSortMapKeys() { var nullValue := AttributeValue.NULL(true); + // "\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. @@ -500,7 +507,7 @@ module DynamoToStructTest { 0x26, // "&" UTF-8 encoded 0,0, 0,0,0,0, // null value 0,1, 0,0,0,4, // 2nd key is a string 4 bytes long - 0xF0, 0x90, 0x80, 0x82, // "\ud800\udc02" UTF-8 encoded + 0xF0, 0x90, 0x80, 0x82, // "𐀂" UTF-8 encoded 0,0, 0,0,0,0, // null value 0,1, 0,0,0,3, // 3rd key is a string 3 bytes long 0xEF, 0xBD, 0xA1, // "｡" diff --git a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy index 0339bad1d..2f6e3a112 100644 --- a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy +++ b/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" // "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") - // 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 From dadb2b89065ede2b7b1bca8f3e883fdcf18f08c1 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Fri, 30 May 2025 09:45:24 -0700 Subject: [PATCH 8/8] m --- TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy index 2f6e3a112..a6635393c 100644 --- a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy +++ b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy @@ -220,9 +220,9 @@ module {:options "-functionSyntax:4"} WriteManifest { const A : string := "A" 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") + const D : string := "\uD800\uDC01" // "U10001" <-> "𐀁" (surrogate pair: "\uD800\uDC01") + const E : string := "\uD800\uDC02" // "U10002" <-> "𐀂" (same high surrogate as D: "\uD800\uDC02") + const F : string := "\uD840\uDC02" // "U20002" <-> "𠀂" (different high surrogate as D: "\D840\uDC02") lemma CheckLengths() ensures |A| == 1