From f01b19d87da926679c792963b5e3cc1e419ba77d Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 27 Aug 2024 15:47:25 -0700 Subject: [PATCH 1/2] fix: remove usage of `:|` --- .../src/BatchGetItemTransform.dfy | 13 ++++++----- .../src/BatchWriteItemTransform.dfy | 22 ++++++++++++++----- .../src/Index.dfy | 16 +++++++++----- 3 files changed, 34 insertions(+), 17 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchGetItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchGetItemTransform.dfy index 26c0172ba..25dad2033 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchGetItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchGetItemTransform.dfy @@ -11,6 +11,7 @@ module BatchGetItemTransform { import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes import EncTypes = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes import Seq + import SortedSets method Input(config: Config, input: BatchGetItemInputTransformInput) returns (output: Result) @@ -34,14 +35,15 @@ module BatchGetItemTransform { return Success(BatchGetItemOutputTransformOutput(transformedOutput := input.sdkOutput)); } var tableNames := input.sdkOutput.Responses.value.Keys; + var tableNamesSeq := SortedSets.ComputeSetToSequence(tableNames); + ghost var tableNamesSet' := tableNames; + var i := 0; var result := map[]; - while tableNames != {} - decreases |tableNames| - invariant tableNames <= input.sdkOutput.Responses.value.Keys + while i < |tableNamesSeq| + invariant tableNamesSet' <= input.sdkOutput.Responses.value.Keys // true but expensive -- invariant result.Keys + tableNames == input.sdkOutput.Responses.value.Keys { - var tableName :| tableName in tableNames; - tableNames := tableNames - { tableName }; + var tableName := tableNamesSeq[i]; var responses := input.sdkOutput.Responses.value[tableName]; if tableName in config.tableEncryptionConfigs { var tableConfig := config.tableEncryptionConfigs[tableName]; @@ -74,6 +76,7 @@ module BatchGetItemTransform { } else { result := result + map[tableName := responses]; } + i := i + 1; } return Success(BatchGetItemOutputTransformOutput(transformedOutput := input.sdkOutput.(Responses := Some(result)))); } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy index 482a222c1..217e93cbc 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy @@ -11,9 +11,10 @@ module BatchWriteItemTransform { import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes import EncTypes = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes import Seq + import SortedSets import Util = DynamoDbEncryptionUtil - method Input(config: Config, input: BatchWriteItemInputTransformInput) + method {:vcs_split_on_every_assert} Input(config: Config, input: BatchWriteItemInputTransformInput) returns (output: Result) requires ValidConfig?(config) ensures ValidConfig?(config) @@ -21,12 +22,16 @@ module BatchWriteItemTransform { { var tableNames := input.sdkInput.RequestItems.Keys; var result : map := map[]; - while tableNames != {} - decreases |tableNames| - invariant tableNames <= input.sdkInput.RequestItems.Keys + var tableNamesSeq := SortedSets.ComputeSetToSequence(tableNames); + ghost var tableNamesSet' := tableNames; + var i := 0; + while i < |tableNamesSeq| + invariant Seq.HasNoDuplicates(tableNamesSeq) + invariant forall j | i <= j < |tableNamesSeq| :: tableNamesSeq[j] in tableNamesSet' + invariant |tableNamesSet'| == |tableNamesSeq| - i + invariant tableNamesSet' <= input.sdkInput.RequestItems.Keys { - var tableName :| tableName in tableNames; - tableNames := tableNames - { tableName }; + var tableName := tableNamesSeq[i]; var writeRequests : DDB.WriteRequests := input.sdkInput.RequestItems[tableName]; //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-batchwriteitem @@ -64,6 +69,11 @@ module BatchWriteItemTransform { } writeRequests := encryptedItems; } + tableNamesSet' := tableNamesSet' - {tableName}; + i := i + 1; + assert forall j | i <= j < |tableNamesSeq| :: tableNamesSeq[j] in tableNamesSet' by { + reveal Seq.HasNoDuplicates(); + } result := result[tableName := writeRequests]; } :- Need(|result| == |input.sdkInput.RequestItems|, E("Internal Error")); // Dafny gets too confused diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy index bf08e3e59..ac9ba1876 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy @@ -16,6 +16,7 @@ module import DynamoDbItemEncryptor import SearchConfigToInfo import Seq + import SortedSets import ET = AwsCryptographyDbEncryptionSdkDynamoDbTypes import SET = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes import DDB = ComAmazonawsDynamodbTypes @@ -119,6 +120,9 @@ module //# [DynamoDb Item Encryptor](./ddb-table-encryption-config.md) //# per configured table, using these table encryption configs. var m' := config.tableEncryptionConfigs; + var mKeys := m'.Keys; + var tableNamesSeq := SortedSets.ComputeSetToSequence(mKeys); + ghost var mKeysSet := mKeys; ghost var inputConfigsModifies: set := set tableConfig <- config.tableEncryptionConfigs.Values, @@ -130,8 +134,9 @@ module :: o; var allLogicalTableNames := {}; - - while m'.Keys != {} + var i := 0; + + while i < |tableNamesSeq| invariant m'.Keys <= config.tableEncryptionConfigs.Keys invariant forall k <- m' :: m'[k] == config.tableEncryptionConfigs[k] invariant forall internalConfig <- internalConfigs.Values :: internalConfig.logicalTableName in allLogicalTableNames @@ -140,10 +145,10 @@ module invariant AllTableConfigsValid?(internalConfigs) invariant ValidConfig?(Config(internalConfigs)) - decreases m'.Keys modifies inputConfigsModifies { - var tableName: string :| tableName in m'; + var tableName: string := tableNamesSeq[i]; + var inputConfig := config.tableEncryptionConfigs[tableName]; :- Need(inputConfig.logicalTableName !in allLogicalTableNames, E("Duplicate logical table maped to multipule physical tables: " + inputConfig.logicalTableName)); @@ -223,8 +228,7 @@ module assert ConfigsMatch(tableName, internalConfig, inputConfig); } - // Pop 'tableName' off the map, so that we may continue iterating - m' := map k' | k' in m' && k' != tableName :: m'[k']; + i := i + 1; } assert SearchValidState(DdbMiddlewareConfig.Config(tableEncryptionConfigs := internalConfigs)); From a3b7bb6bd514a5de88e64583372742d03e111a19 Mon Sep 17 00:00:00 2001 From: Jose Corella Date: Tue, 27 Aug 2024 15:53:31 -0700 Subject: [PATCH 2/2] format --- .../src/BatchWriteItemTransform.dfy | 8 ++++---- .../dafny/DynamoDbEncryptionTransforms/src/Index.dfy | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy index 217e93cbc..5073b5c4e 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy @@ -27,8 +27,8 @@ module BatchWriteItemTransform { var i := 0; while i < |tableNamesSeq| invariant Seq.HasNoDuplicates(tableNamesSeq) - invariant forall j | i <= j < |tableNamesSeq| :: tableNamesSeq[j] in tableNamesSet' - invariant |tableNamesSet'| == |tableNamesSeq| - i + invariant forall j | i <= j < |tableNamesSeq| :: tableNamesSeq[j] in tableNamesSet' + invariant |tableNamesSet'| == |tableNamesSeq| - i invariant tableNamesSet' <= input.sdkInput.RequestItems.Keys { var tableName := tableNamesSeq[i]; @@ -72,8 +72,8 @@ module BatchWriteItemTransform { tableNamesSet' := tableNamesSet' - {tableName}; i := i + 1; assert forall j | i <= j < |tableNamesSeq| :: tableNamesSeq[j] in tableNamesSet' by { - reveal Seq.HasNoDuplicates(); - } + reveal Seq.HasNoDuplicates(); + } result := result[tableName := writeRequests]; } :- Need(|result| == |input.sdkInput.RequestItems|, E("Internal Error")); // Dafny gets too confused diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy index ac9ba1876..f44f59b6c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy @@ -135,7 +135,7 @@ module var allLogicalTableNames := {}; var i := 0; - + while i < |tableNamesSeq| invariant m'.Keys <= config.tableEncryptionConfigs.Keys invariant forall k <- m' :: m'[k] == config.tableEncryptionConfigs[k]