allow empty in addition to None

aws · Oct 11, 2023 · 9a997a9 · 9a997a9
1 parent 6a229de
commit 9a997a9
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 10 deletions.
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DeleteItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DeleteItemTransform.dfy
@@ -25,7 +25,7 @@ module DeleteItemTransform {
       //= type=implication
       //# The DeleteItem request MUST NOT refer to any legacy parameters,
       //# specifically Expected and ConditionalOperator MUST NOT be set.
-      && input.sdkInput.Expected.None?
+      && NoMap(input.sdkInput.Expected)
       && input.sdkInput.ConditionalOperator.None?
 
       //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#validate-before-deleteitem
@@ -52,7 +52,7 @@ module DeleteItemTransform {
 
   {
     if input.sdkInput.TableName in config.tableEncryptionConfigs {
-      :- Need(input.sdkInput.Expected.None?, E("Legacy parameter 'Expected' not supported in UpdateItem with Encryption"));
+      :- Need(NoMap(input.sdkInput.Expected), E("Legacy parameter 'Expected' not supported in UpdateItem with Encryption"));
       :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption"));
 
       var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy
@@ -31,15 +31,15 @@ module ScanTransform {
     //# The Scan request MUST NOT refer to any legacy parameters,
     //# specifically AttributesToGet, ScanFilter and ConditionalOperator MUST NOT be set.
     ensures output.Success? && input.sdkInput.TableName in config.tableEncryptionConfigs ==>
-              && input.sdkInput.AttributesToGet.None?
-              && input.sdkInput.ScanFilter.None?
+              && NoList(input.sdkInput.AttributesToGet)
+              && NoMap(input.sdkInput.ScanFilter)
               && input.sdkInput.ConditionalOperator.None?
   {
     if input.sdkInput.TableName !in config.tableEncryptionConfigs {
       return Success(ScanInputTransformOutput(transformedInput := input.sdkInput));
     } else {
-      :- Need(input.sdkInput.AttributesToGet.None?, E("Legacy parameter 'AttributesToGet' not supported in UpdateItem with Encryption"));
-      :- Need(input.sdkInput.ScanFilter.None?, E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
+      :- Need(NoList(input.sdkInput.AttributesToGet), E("Legacy parameter 'AttributesToGet' not supported in UpdateItem with Encryption"));
+      :- Need(NoMap(input.sdkInput.ScanFilter), E("Legacy parameter 'ScanFilter' not supported in UpdateItem with Encryption"));
       :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption"));
       var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];
       var finalResult :- ScanInputForBeacons(tableConfig, input.sdkInput);

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/UpdateItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/UpdateItemTransform.dfy
@@ -23,8 +23,8 @@ module UpdateItemTransform {
       //= type=implication
       //# The UpdateItem request MUST NOT refer to any legacy parameters,
       //# specifically Expected, AttributeUpdates and ConditionalOperator MUST NOT be set.
-      && input.sdkInput.Expected.None?
-      && input.sdkInput.AttributeUpdates.None?
+      && NoMap(input.sdkInput.Expected)
+      && NoMap(input.sdkInput.AttributeUpdates)
       && input.sdkInput.ConditionalOperator.None?
       && var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];
 
@@ -50,8 +50,8 @@ module UpdateItemTransform {
       && output.value.transformedInput == input.sdkInput
   {
     if input.sdkInput.TableName in config.tableEncryptionConfigs {
-      :- Need(input.sdkInput.Expected.None?, E("Legacy parameter 'Expected' not supported in UpdateItem with Encryption"));
-      :- Need(input.sdkInput.AttributeUpdates.None?, E("Legacy parameter 'AttributeUpdates' not supported in UpdateItem with Encryption"));
+      :- Need(NoMap(input.sdkInput.Expected), E("Legacy parameter 'Expected' not supported in UpdateItem with Encryption"));
+      :- Need(NoMap(input.sdkInput.AttributeUpdates), E("Legacy parameter 'AttributeUpdates' not supported in UpdateItem with Encryption"));
       :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption"));
 
       var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName];