feat: ddbv2 TestModel (#644)

* feat: ddbv2 TestModel

* fix: comments

* fix: formatting

---------

Co-authored-by: Shubham Chaturvedi <[email protected]>

TestModels/aws-sdks/ddbv2/Makefile

@@ -0,0 +1,62 @@
+# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+CORES=2
+
+ENABLE_EXTERN_PROCESSING=1
+
+TRANSPILE_TESTS_IN_RUST=1
+
+RUST_OTHER_FILES := \
+	runtimes/rust/src/ddb.rs
+
+include ../../SharedMakefile.mk
+
+PROJECT_SERVICES := \
+	ComAmazonawsDynamodb \
+
+MAIN_SERVICE_FOR_RUST := ComAmazonawsDynamodb
+
+SERVICE_NAMESPACE_ComAmazonawsDynamodb=com.amazonaws.dynamodb
+
+SERVICE_DEPS_ComAmazonawsDynamodb :=
+
+SMITHY_DEPS=dafny-dependencies/Model/traits.smithy
+
+AWS_SDK_CMD=--aws-sdk
+
+# This project has no dependencies 
+# DEPENDENT-MODELS:= 
+
+
+# There is no wrapped target for aws-sdk types
+_polymorph_wrapped: ;
+_polymorph_wrapped_dafny: ;
+_polymorph_wrapped_net: ;
+_polymorph_wrapped_java: ;
+_polymorph_wrapped_python: ;
+
+format_net:
+	pushd runtimes/net && dotnet format && popd
+
+clean: _clean
+	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated
+	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
+	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated
+
+# Python
+
+PYTHON_MODULE_NAME=com_amazonaws_dynamodb
+
+TRANSLATION_RECORD_PYTHON := \
+    --translation-record ../../dafny-dependencies/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/generated/dafny_src-py.dtr
+
+# Constants for languages that drop extern names (Python, Go)
+
+TYPES_FILE_PATH=Model/ComAmazonawsDynamodbTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.services.dynamodb.internaldafny.types\" } ComAmazonawsDynamodbTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module ComAmazonawsDynamodbTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.services.dynamodb.internaldafny\"} Com.Amazonaws.Dynamodb refines AbstractComAmazonawsDynamodbService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module Com.Amazonaws.Dynamodb refines AbstractComAmazonawsDynamodbService {"

TestModels/aws-sdks/ddbv2/README.md

@@ -0,0 +1,38 @@
+# AWS-SDK-DDB
+
+This project tests the [AWS DynamoDB](https://aws.amazon.com/dynamodb/) Operations `QUERY, GET, and PUT` in `dafny`. The project utilizes the `aws-sdk-ddb smithy model` to generate the dafny types using `polymorph`. This interface is then used in the dafny to call the appropriate operations. The actual implementation of the DynamoDB Operations are provided by the underlying native runtime. These integration tests aim to verify the correctness of the polymorph generated code and is run either as CI actions or manually.
+
+NOTE: The `model.json` in this project comes from [private-aws-encryption-sdk-dafny-staging/ComAmazonawsDynamodb/Model/dynamodb](https://github.com/aws/private-aws-encryption-sdk-dafny-staging/tree/v4-seperate-modules/ComAmazonawsDynamodb/Model/dynamodb), and is different from the standard model at https://github.com/aws/aws-models/ddb/
+This v2 version uses the smithy 2.0 model and should be compatible with the latest/v2 sdk of a runtime.
+
+## Build
+
+### Python
+
+1. Generate the Wrappers using `polymorph`
+
+```
+make polymorph_dafny polymorph_python
+```
+
+2. Transpile the tests (and implementation) to the target runtime.
+
+```
+make transpile_python
+```
+
+3. Generate the executable in the .NET and execute the tests
+
+```
+make test_python
+```
+
+## Development
+
+1. To add another target runtime support, edit the `Makefile` and add the appropriate recipe to generate the `polymorph` wrappers, and dafny transpilation.
+2. Provide any glue code between dafny and target runtime if required.
+3. Build, execute, and test in the target runtime.
+
+_Example_
+
+`--output-python <PATH>` in the `gradlew run` is used to generate the polymorph wrappers. Similarly `translate <RUNTIME>` flags is used in dafny recipe to transpile to runtime.

TestModels/aws-sdks/ddbv2/runtimes/python/pyproject.toml

@@ -0,0 +1,26 @@
+[tool.poetry]
+name = "amazon-cryptography-internal-dafny-shim-ddb"
+version = "0.1.0"
+description = ""
+authors = ["AWS <[email protected]>"]
+packages = [
+    { include = "com_amazonaws_dynamodb", from = "src" }
+]
+# Include all of the following .gitignored files in package distributions,
+# even though it is not included in version control
+include = ["**/smithygenerated/**/*.py", "**/dafnygenerated/*.py"]
+
+[tool.poetry.dependencies]
+python = "^3.11.0"
+boto3 = "^1.28.38"
+# TODO: Depend on PyPi once Smithy-Python publishes their Python package there
+smithy-python = { path = "../../../../../codegen/smithy-dafny-codegen-modules/smithy-python/python-packages/smithy-python", develop = false}
+smithy-dafny-standard-library = {path = "../../../../dafny-dependencies/StandardLibrary/runtimes/python", develop = false}
+DafnyRuntimePython = "^4.7.0"
+
+[tool.poetry.group.test.dependencies]
+pytest = "^7.4.0"
+
+[build-system]
+requires = ["poetry-core"]
+build-backend = "poetry.core.masonry.api"

TestModels/aws-sdks/ddbv2/runtimes/python/src/com_amazonaws_dynamodb/__init__.py

@@ -0,0 +1,8 @@
+# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+# Initialize generated Dafny
+from .internaldafny.generated import module_
+
+# Initialize externs
+from .internaldafny import extern

TestModels/aws-sdks/ddbv2/runtimes/python/src/com_amazonaws_dynamodb/internaldafny/extern/Com_Amazonaws_Dynamodb.py

@@ -0,0 +1,60 @@
+import boto3
+import _dafny
+
+from botocore.config import Config
+from boto3.session import Session
+
+from smithy_dafny_standard_library.internaldafny.generated.Wrappers import Option_Some
+from com_amazonaws_dynamodb.smithygenerated.com_amazonaws_dynamodb.shim import DynamoDBClientShim
+from com_amazonaws_dynamodb.internaldafny.generated.Com_Amazonaws_Dynamodb import *
+import com_amazonaws_dynamodb.internaldafny.generated.Com_Amazonaws_Dynamodb
+
+
+# Persist this across calls; this doesn't change
+available_aws_regions: list[str] = None
+
+def get_available_aws_regions():
+    global available_aws_regions
+    if available_aws_regions is not None:
+        return available_aws_regions
+    available_aws_regions = Session().get_available_regions("dynamodb")
+    return available_aws_regions
+
+class default__(com_amazonaws_dynamodb.internaldafny.generated.Com_Amazonaws_Dynamodb.default__):
+    @staticmethod
+    def DynamoDBClient(boto_client = None, region = None):
+        if boto_client is None:
+            if region is not None and region in get_available_aws_regions():
+                boto_config = Config(
+                    region_name=region
+                )
+                boto_client = boto3.client("dynamodb", config=boto_config)
+            else:
+                # If no region is provided,
+                # boto_client will use the default region provided by boto3
+                boto_client = boto3.client("dynamodb")
+                region = boto_client.meta.region_name
+        wrapped_client = DynamoDBClientShim(boto_client, region)
+        return Wrappers.Result_Success(wrapped_client)
+
+    @staticmethod
+    def DDBClientForRegion(region: _dafny.Seq):
+        region_string = _dafny.string_of(region)
+        return default__.DynamoDBClient(region=region_string)
+
+    @staticmethod
+    def RegionMatch(client, region):
+        # We should never be passing anything other than Shim as the 'client'.
+        # If this assertion fails, that indicates that there is something wrong with
+        # our code generation.
+        try:
+            assert isinstance(client, DynamoDBClientShim)
+        except AssertionError:
+            raise TypeError("Client provided to RegionMatch is not a DynamoDBClientShim: " + client)
+
+        # Since client is a DynamoDBClientShim, we can reach into its _impl, which is a boto3 client,
+        # then into the client's .meta.region_name attribute
+        client_region_name = client._impl.meta.region_name
+        return Option_Some(region.VerbatimString(False) == client_region_name)
+
+com_amazonaws_dynamodb.internaldafny.generated.Com_Amazonaws_Dynamodb.default__ = default__

TestModels/aws-sdks/ddbv2/runtimes/python/src/com_amazonaws_dynamodb/internaldafny/extern/__init__.py

@@ -0,0 +1,3 @@
+from . import (
+    Com_Amazonaws_Dynamodb
+)

TestModels/aws-sdks/ddbv2/runtimes/python/test/internaldafny/__init__.py

@@ -0,0 +1,2 @@
+# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0

TestModels/aws-sdks/ddbv2/runtimes/python/test/internaldafny/test_dafny_wrapper.py

@@ -0,0 +1,17 @@
+"""
+Wrapper file for executing Dafny tests from pytest.
+This allows us to import modules required by Dafny-generated tests
+before executing Dafny-generated tests.
+pytest will find and execute the `test_dafny` method below,
+which will execute the `internaldafny_test_executor.py` file in the `dafny` directory.
+"""
+
+import sys
+
+internaldafny_dir = '/'.join(__file__.split("/")[:-1])
+
+sys.path.append(internaldafny_dir + "/extern")
+sys.path.append(internaldafny_dir + "/generated")
+
+def test_dafny():
+  from .generated import __main__

TestModels/aws-sdks/ddbv2/runtimes/python/tox.ini

@@ -0,0 +1,14 @@
+[tox]
+isolated_build = True
+envlist =
+  py{311,312}
+
+[testenv]
+skip_install = true
+allowlist_externals = poetry
+passenv = AWS_*
+commands_pre =
+    poetry lock
+    poetry install
+commands =
+    poetry run pytest -s -v test/

TestModels/aws-sdks/ddbv2/src/Index.dfy

@@ -0,0 +1,12 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "../Model/ComAmazonawsDynamodbTypes.dfy"
+
+module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny"} Com.Amazonaws.Dynamodb refines AbstractComAmazonawsDynamodbService {
+
+  function method DefaultDynamoDBClientConfigType() : DynamoDBClientConfigType {
+    DynamoDBClientConfigType
+  }
+
+}