test: Use Dafny TestVector Runner as opposed to Native Runner

.gitmodules

@@ -11,3 +11,6 @@
 [submodule "AwsEncryptionSDK/runtimes/net/TestVectorsV3/TestVectors/resources/aws-encryption-sdk-test-vectors"]
 	path = AwsEncryptionSDK/runtimes/net/TestVectorsV3/TestVectors/resources/aws-encryption-sdk-test-vectors
 	url = https://github.com/awslabs/aws-encryption-sdk-test-vectors.git
+[submodule "TestVectors/aws-encryption-sdk-test-vectors"]
+	path = TestVectors/aws-encryption-sdk-test-vectors
+	url = https://github.com/awslabs/aws-encryption-sdk-test-vectors.git

TestVectors/.gitignore

@@ -0,0 +1,6 @@
+TestResults
+ImplementationFromDafny.cs
+TestsFromDafny.cs
+**/bin
+**/obj
+/runtimes/java/dafny

TestVectors/Makefile

@@ -0,0 +1,60 @@
+# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+CORES=2
+
+include ../SharedMakefileV2.mk
+
+DIR_STRUCTURE_V2=V2
+
+PROJECT_SERVICES := \
+	ESDK \
+
+SMITHY_MODEL_ROOT := $(PROJECT_ROOT)/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model
+OUTPUT_LOCAL_SERVICE_ESDK := --local-service-test
+
+SERVICE_NAMESPACE_ESDK=aws.cryptography.encryptionSdk
+
+MAX_RESOURCE_COUNT=10000000
+# Order is important
+# In java they MUST be built
+# in the order they depend on each other
+PROJECT_DEPENDENCIES := \
+	mpl/AwsCryptographyPrimitives \
+	mpl/ComAmazonawsKms \
+	mpl/ComAmazonawsDynamodb \
+	mpl/AwsCryptographicMaterialProviders \
+	mpl/TestVectorsAwsCryptographicMaterialProviders \
+	AwsEncryptionSDK \
+
+# Since we are packaging projects differently, we cannot make assumptions
+# about where the files are located. 
+# This is here to get unblocked but should be removed once we have migrated packages
+# to the new packaging format.
+PROJECT_INDEX := \
+	mpl/AwsCryptographyPrimitives/src/Index.dfy \
+	mpl/ComAmazonawsKms/src/Index.dfy \
+	mpl/ComAmazonawsDynamodb/src/Index.dfy \
+	mpl/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy \
+	mpl/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy \
+	mpl/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy \
+	mpl/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy \
+	AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy \
+
+STD_LIBRARY=mpl/StandardLibrary
+SMITHY_DEPS=mpl/model
+
+
+# Dependencies for each local service
+SERVICE_DEPS_ESDK := \
+	mpl/AwsCryptographyPrimitives \
+	mpl/ComAmazonawsKms \
+	mpl/ComAmazonawsDynamodb \
+	mpl/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
+	mpl/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore \
+	AwsEncryptionSDK/dafny/AwsEncryptionSdk \
+	mpl/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders \
+
+
+format_net:
+	pushd runtimes/net && dotnet format && popd

TestVectors/README.md

@@ -0,0 +1,31 @@
+# AWS Encryption SDK Test Vectors
+
+This project contains code encrypts and decrypts a suite unstructured data.
+This validates the Encryption SDK's cross compatability between major versions
+of the Encryption SDK and runtimes.
+
+## Getting Started
+
+### Development Requirements
+
+* Dafny 4.2.0: https://github.com/dafny-lang/dafny
+
+  The code that executes the test vectors is written in Dafny. 
+  You must install the Dafny runtime to compile the Dafny tests into Java.
+* A .NET 6.0 TargetFramework or newer development environment
+
+### Building and Running
+
+1. Start in the root `./TestVectors` directory
+2. Run `make transpile_net`
+3. Run `make test_net_mac_intel` if running on a MacOS environment or
+`make test_net` if running on a Windows or Linux environment.
+
+## Security
+
+See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more information.
+
+## License
+
+This project is licensed under the Apache-2.0 License.
+

TestVectors/dafny/ESDK/Model/AwsCryptographyEncryptionSdkTypesWrapped.dfy

@@ -0,0 +1,24 @@
+// 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 "../../../../mpl/StandardLibrary/src/Index.dfy"
+  // BEGIN MANUAL EDIT
+include "../../../../AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy"
+include "../../../../mpl/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/Index.dfy"
+  // END MANUAL EDIT
+include "../src/Index.dfy"
+abstract module WrappedAbstractAwsCryptographyEncryptionSdkService {
+  import opened Wrappers
+  import opened StandardLibrary.UInt
+  import opened UTF8
+  import opened Types = AwsCryptographyEncryptionSdkTypes
+  import WrappedService : AbstractAwsCryptographyEncryptionSdkService
+  function method WrappedDefaultAwsEncryptionSdkConfig(): AwsEncryptionSdkConfig
+  method {:extern} WrappedESDK(config: AwsEncryptionSdkConfig := WrappedDefaultAwsEncryptionSdkConfig())
+    returns (res: Result<IAwsEncryptionSdkClient, Error>)
+    ensures res.Success? ==>
+              && fresh(res.value)
+              && fresh(res.value.Modifies)
+              && fresh(res.value.History)
+              && res.value.ValidState()
+}

TestVectors/dafny/ESDK/src/EsdkManifestOptions.dfy

@@ -0,0 +1,27 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "LibraryIndex.dfy"
+
+module {:options "-functionSyntax:4"} EsdkManifestOptions {
+  import opened Wrappers
+
+  datatype ManifestOptions =
+    | Decrypt(
+        nameonly manifestPath: string,
+        nameonly testName: Option<string> := None
+      )
+    | Encrypt(
+        nameonly manifestPath: string,
+        nameonly manifest: string,
+        nameonly decryptManifestOutput: string,
+        nameonly testName: Option<string> := None
+      )
+    | DecryptSingle(
+        nameonly keysPath: string,
+        nameonly keyDescription: string,
+        nameonly base64Bytes: string
+      )
+      // | EncryptManifest(nameonly encryptManifestOutput: string version?)
+
+}