feat: add virtual fields

DynamoDbEncryptionMiddlewareInternal/src/DDBSupport.dfy

@@ -18,6 +18,7 @@ module DynamoDBMiddlewareSupport {
   import opened StandardLibrary.UInt
   import opened BS = DynamoDBSupport
   import opened DdbMiddlewareConfig
+  import AwsCryptographyDynamoDbItemEncryptorOperations
 
   // IsWritable examines an AttributeMap and fails if it is unsuitable for writing.
   // Generally this means that no attribute names starts with "aws_dbe_"
@@ -62,6 +63,7 @@ module DynamoDBMiddlewareSupport {
   // returning a replacement AttributeMap.
   function method {:opaque} AddBeacons(config : ValidTableConfig, item : DDB.AttributeMap)
     : Result<DDB.AttributeMap, Error>
+    requires AwsCryptographyDynamoDbItemEncryptorOperations.ValidInternalConfig?(config.itemEncryptor.config)
   {
     BS.AddBeacons(config.itemEncryptor.config, item)
       .MapFailure(e => E(e))

DynamoDbEncryptionMiddlewareInternal/src/TransactWriteItemsTransform.dfy

@@ -28,13 +28,12 @@ module TransactWriteItemsTransform {
     ensures output.Success? ==> |output.value.transformedInput.TransactItems| == |input.sdkInput.TransactItems|
 
     //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-transactwriteitems
-    //= type=implication
     //# To protect against a possible fifth field being added to the TransactWriteItem structure in the future,
     //# the client MUST fail if none of the `Update`, `ConditionCheck`, `Delete` and `Put` fields are set.
     ensures output.Success? ==>
       forall item <- input.sdkInput.TransactItems :: IsValid(item)
   {
-    :- Need(forall item <- input.sdkInput.TransactItems :: IsValid(item), E("Each item in TransactWriteItems must specify at least one operation"));
+    :- Need(forall item <- input.sdkInput.TransactItems :: IsValid(item), E("Each item in TransactWriteItems must specify at least one supported operation"));
     var result : seq<DDB.TransactWriteItem> := [];
     for x := 0 to |input.sdkInput.TransactItems|
       invariant |result| == x
@@ -110,7 +109,8 @@ module TransactWriteItemsTransform {
         //# the result [Encrypted DynamoDB Item](./encrypt-item.md#encrypted-dynamodb-item)
         //# calculated above.
         var put := Some(item.Put.value.(Item := encrypted.encryptedItem));
-        result := result + [item.(Put := put)];
+        var newItem := item.(Put := put);
+        result := result + [newItem];
       } else {
         //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-transactwriteitems
         //# Any actions other than `Put, MUST be unchanged.

DynamoDbEncryptionMiddlewareInternal/test/TransactWriteItemsTransform.dfy

@@ -61,7 +61,7 @@ module TransactWriteItemsTransformTest {
         sdkInput := input
       )
     );
-    ExpectFailure(transformed, "Each item in TransactWriteItems must specify at least one operation");
+    ExpectFailure(transformed, "Each item in TransactWriteItems must specify at least one supported operation");
   }
 
   method {:test} TestTransactWriteItemsOutputTransform() {

DynamoDbItemEncryptor/src/AwsCryptographyDynamoDbItemEncryptorOperations.dfy

@@ -3,6 +3,7 @@
 include "../Model/AwsCryptographyDynamoDbItemEncryptorTypes.dfy"
 include "../../private-aws-encryption-sdk-dafny-staging/AwsCryptographicMaterialProviders/src/CMMs/ExpectedEncryptionContextCMM.dfy"
 include "DynamoToStruct.dfy"
+include "../../StructuredEncryption/src/SearchInfo.dfy"
 
 module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptographyDynamoDbItemEncryptorOperations {
   import opened StructuredEncryptionUtil
@@ -18,6 +19,7 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog
   import SE =  StructuredEncryptionUtil
   import MaterialProviders
   import ExpectedEncryptionContextCMM
+  import opened SearchableEncryptionInfo
 
   datatype Config = Config(
     nameonly cmpClient : MaterialProviders.MaterialProvidersClient,
@@ -29,7 +31,8 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog
     nameonly allowedUnauthenticatedAttributes: Option<ComAmazonawsDynamodbTypes.AttributeNameList>,
     nameonly allowedUnauthenticatedAttributePrefix: Option<string>,
     nameonly algorithmSuiteId: Option<CMP.DBEAlgorithmSuiteId>,
-    nameonly structuredEncryption: StructuredEncryption.StructuredEncryptionClient
+    nameonly structuredEncryption: StructuredEncryption.StructuredEncryptionClient,
+    nameonly beacons : Option<SearchInfo>
     // TODO legacy encryptor
     // TODO legacy schema
   )
@@ -266,6 +269,7 @@ module AwsCryptographyDynamoDbItemEncryptorOperations refines AbstractAwsCryptog
     && (forall attribute <- config.attributeActions.Keys ::
           !(SE.ReservedPrefix <= attribute))
 
+    && (config.beacons.Some? ==> config.beacons.value.ValidState())
   }
 
   function ModifiesInternalConfig(config: InternalConfig) : set<object>