m

Author: lucasmcdonald3

TestVectors/Makefile

@@ -7,14 +7,17 @@ TRANSPILE_TESTS_IN_RUST=1
 include ../SharedMakefile.mk
 
 PROJECT_SERVICES := \
-	DDBEncryption
+	DDBEncryption \
+	WrappedDynamoDbItemEncryptor
 
 MAIN_SERVICE_FOR_RUST := DDBEncryption
 
 SMITHY_MODEL_ROOT := $(PROJECT_ROOT)/DynamoDbEncryption/dafny/DynamoDbEncryption/Model
 OUTPUT_LOCAL_SERVICE_DDBEncryption := --local-service-test
+OUTPUT_LOCAL_SERVICE_WrappedDynamoDbItemEncryptor := --local-service-test
 
 SERVICE_NAMESPACE_DDBEncryption=aws.cryptography.dbEncryptionSdk.dynamoDb
+SERVICE_NAMESPACE_WrappedDynamoDbItemEncryptor=aws.cryptography.dbEncryptionSdk.dynamoDb.itemEncryptor
 
 MAX_RESOURCE_COUNT=10000000
 # Order is important
@@ -81,6 +84,17 @@ SERVICE_DEPS_DDBEncryption := \
 	DynamoDbEncryption/dafny/DynamoDbEncryption \
 	submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders \
 
+SERVICE_DEPS_WrappedDynamoDbItemEncryptor := \
+	submodules/MaterialProviders/AwsCryptographyPrimitives \
+	submodules/MaterialProviders/ComAmazonawsKms \
+	submodules/MaterialProviders/ComAmazonawsDynamodb \
+	submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
+	submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
+	DynamoDbEncryption/dafny/StructuredEncryption \
+	DynamoDbEncryption/dafny/DynamoDbEncryption \
+	DynamoDbEncryption/dafny/DynamoDbItemEncryptor \
+	submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders \
+
 transpile_implementation_rust: _remove_wrapped_client_rust
 
 _remove_wrapped_client_rust:

TestVectors/dafny/DDBEncryption/src/CreateWrappedItemEncryptor.dfy

@@ -13,7 +13,7 @@ module {:extern} CreateWrappedItemEncryptor {
 
   // The `ensures` clause is copy-pasted from the DynamoDbItemEncryptor client method's `ensures` clause.
   method {:extern} CreateWrappedItemEncryptor(config: ENC.DynamoDbItemEncryptorConfig)
-    returns (output: Result<ENC.IDynamoDbItemEncryptorClient, AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error>)
+    returns (output: Result<ENC.IDynamoDbItemEncryptorClient, ENC.Error>)
     requires config.keyring.Some? ==>
       config.keyring.value.ValidState()
     requires config.cmm.Some? ==>
@@ -63,8 +63,4 @@ module {:extern} CreateWrappedItemEncryptor {
       ==>
         && var config := (output.value as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient).config;
         && config.plaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ?
-  {
-    var encryptor :- expect DynamoDbItemEncryptor.DynamoDbItemEncryptor(config);
-    return Success(encryptor);
-  }
 }

TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy

@@ -351,7 +351,6 @@ module {:options "-functionSyntax:4"} JsonConfig {
         plaintextOverride := plaintextOverride
       );
     var enc : ENC.IDynamoDbItemEncryptorClient :- expect CreateWrappedItemEncryptor.CreateWrappedItemEncryptor(encryptorConfig);
-    // var enc : ENC.IDynamoDbItemEncryptorClient :- expect DynamoDbItemEncryptor.DynamoDbItemEncryptor(encryptorConfig);
     assert enc is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient;
     var encr := enc as DynamoDbItemEncryptor.DynamoDbItemEncryptorClient;
     return Success(encr);

TestVectors/dafny/WrappedDynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypesWrapped.dfy

@@ -0,0 +1,20 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
+include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
+include "../src/Index.dfy"
+abstract module WrappedAbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService {
+  import opened Wrappers
+  import opened StandardLibrary.UInt
+  import opened UTF8
+  import opened Types = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
+  import WrappedService : AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService
+  function method WrappedDefaultDynamoDbItemEncryptorConfig(): DynamoDbItemEncryptorConfig
+  method {:extern} WrappedDynamoDbItemEncryptor(config: DynamoDbItemEncryptorConfig := WrappedDefaultDynamoDbItemEncryptorConfig())
+    returns (res: Result<IDynamoDbItemEncryptorClient, Error>)
+    ensures res.Success? ==>
+              && fresh(res.value)
+              && fresh(res.value.Modifies)
+              && fresh(res.value.History)
+              && res.value.ValidState()
+}

TestVectors/dafny/WrappedDynamoDbItemEncryptor/src/Index.dfy

@@ -0,0 +1,2 @@
+// Empty stub expected by Smithy-Dafny
+module WrappedItemEncryptor {}