Skip to content

chore: Dafny test code changes for Python #1911

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 15 commits into
base: main
Choose a base branch
from
+19 −12
Open

chore: Dafny test code changes for Python #1911

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
5640109
sync
May 27, 2025
03411bc
m
May 27, 2025
7d96dc0
m
May 27, 2025
a0c39c8
m
May 27, 2025
d75b611
m
May 27, 2025
95201b6
Merge branch 'main' into python-dafny-changes
lucasmcdonald3 May 28, 2025
0f79ecc
sync
May 28, 2025
01edb60
Merge branch 'python-dafny-changes' of github.com:aws/aws-database-en…
May 28, 2025
1b4c1c4
sync
May 28, 2025
dadb2b8
m
May 30, 2025
f021e37
Merge branch 'main' into python-dafny-changes
rishav-karanjit May 30, 2025
8a3f69f
Merge branch 'main' into python-dafny-changes
lucasmcdonald3 Jun 3, 2025
1d2ddac
Merge branch 'main' into python-dafny-changes
lucasmcdonald3 Jun 5, 2025
31a7997
Merge branch 'main' into python-dafny-changes
lucasmcdonald3 Jun 6, 2025
e77acc2
Merge branch 'main' into python-dafny-changes
lucasmcdonald3 Jun 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 14 additions & 7 deletions DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoToStruct.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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]);
Expand All @@ -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]);
Expand Down Expand Up @@ -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(
Expand Down
10 changes: 5 additions & 5 deletions TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 := "\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
Expand Down
Loading