Skip to content

fix: remove usage of :| #1320

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

Merged
merged 2 commits into from
Aug 28, 2024
Merged

fix: remove usage of :| #1320

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f01b19d
fix: remove usage of `:|`
josecorella Aug 27, 2024
a3b7bb6
format
josecorella Aug 27, 2024
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
13 changes: 8 additions & 5 deletions DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchGetItemTransform.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<BatchGetItemInputTransformOutput, Error>)
Expand All @@ -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];
Expand Down Expand Up @@ -74,6 +76,7 @@ module BatchGetItemTransform {
} else {
result := result + map[tableName := responses];
}
i := i + 1;
}
return Success(BatchGetItemOutputTransformOutput(transformedOutput := input.sdkOutput.(Responses := Some(result))));
}
Expand Down
22 changes: 16 additions & 6 deletions DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,22 +11,27 @@ 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<BatchWriteItemInputTransformOutput, Error>)
requires ValidConfig?(config)
ensures ValidConfig?(config)
modifies ModifiesConfig(config)
{
var tableNames := input.sdkInput.RequestItems.Keys;
var result : map<DDB.TableName, DDB.WriteRequests> := 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
Expand Down Expand Up @@ -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
Expand Down
14 changes: 9 additions & 5 deletions DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ module
import DynamoDbItemEncryptor
import SearchConfigToInfo
import Seq
import SortedSets
import ET = AwsCryptographyDbEncryptionSdkDynamoDbTypes
import SET = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
import DDB = ComAmazonawsDynamodbTypes
Expand Down Expand Up @@ -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<object> := set
tableConfig <- config.tableEncryptionConfigs.Values,
Expand All @@ -130,8 +134,9 @@ module
:: o;

var allLogicalTableNames := {};
var i := 0;

while m'.Keys != {}
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
Expand All @@ -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));

Expand Down Expand Up @@ -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));

Expand Down
Loading