chore: Refactor to build into single artifact (#74)

Author: lavaleri

.github/workflows/ci_test_java.yml

@@ -12,9 +12,6 @@ jobs:
     strategy:
       matrix:
         library: [
-          StructuredEncryption,
-          DynamoDbItemEncryptor,
-          DynamoDbEncryptionMiddlewareInternal,
           DynamoDbEncryption,
         ]
         java-version: [ 8, 11, 16, 17 ]
@@ -49,7 +46,7 @@ jobs:
           AUTH="$(echo -n "pat:${PRIVATE_ESDK_PAT}" | base64 | tr -d '\n')"
           git config --global http.https://github.com/.extraheader "AUTHORIZATION: basic $AUTH"
           git config --global --add url.https://github.com/.insteadOf [email protected]:
-          git submodule update --init --recursive private-aws-encryption-sdk-dafny-staging
+          git submodule update --init --recursive submodules/MaterialProviders
 
       # Set up env vars for CodeArtifact
       - name: Set Up Env Vars for CodeArtifact

.github/workflows/ci_test_net.yml

@@ -12,9 +12,7 @@ jobs:
     strategy:
       matrix:
         library: [
-          DynamoDbEncryptionMiddlewareInternal,
-          DynamoDbItemEncryptor,
-          StructuredEncryption, 
+          DynamoDbEncryption,
         ]
         dotnet-version: [ '6.0.x' ]
         os: [
@@ -43,7 +41,7 @@ jobs:
           AUTH="$(echo -n "pat:${PRIVATE_ESDK_PAT}" | base64 | tr -d '\n')"
           git config --global http.https://github.com/.extraheader "AUTHORIZATION: basic $AUTH"
           git config --global --add url.https://github.com/.insteadOf [email protected]:
-          git submodule update --init --recursive private-aws-encryption-sdk-dafny-staging
+          git submodule update --init --recursive submodules/MaterialProviders
 
       - name: Setup Dafny
         uses: dafny-lang/[email protected]

.github/workflows/ci_verification.yml

@@ -11,10 +11,13 @@ jobs:
   verification:
     strategy:
       matrix:
-        library: [
-          DynamoDbEncryptionMiddlewareInternal,
+        # Break up verification between namespaces over multiple
+        # actions to take advantage of parallelization
+        namespace: [
+          DynamoDbEncryption,
+          DynamoDbEncryptionTransforms,
           DynamoDbItemEncryptor,
-          StructuredEncryption, 
+          StructuredEncryption
         ]
         os: [
           macos-latest,
@@ -34,7 +37,7 @@ jobs:
           AUTH="$(echo -n "pat:${PRIVATE_ESDK_PAT}" | base64 | tr -d '\n')"
           git config --global http.https://github.com/.extraheader "AUTHORIZATION: basic $AUTH"
           git config --global --add url.https://github.com/.insteadOf [email protected]:
-          git submodule update --init --recursive private-aws-encryption-sdk-dafny-staging
+          git submodule update --init --recursive submodules/MaterialProviders
       
       - name: Setup Dafny
         uses: dafny-lang/setup-dafny-action@v1
@@ -43,14 +46,14 @@ jobs:
 
       - name: Verify ${{ matrix.library }} Dafny code
         shell: bash
-        working-directory: ./${{ matrix.library }}
+        working-directory: ./DynamoDbEncryption
         run: |
           # This works because `node` is installed by default on GHA runners
           CORES=$(node -e 'console.log(os.cpus().length)')
-          make verify CORES=$CORES
+          make verify_namespace CORES=$CORES SMITHY_NAMESPACE=${{ matrix.namespace }}
 
       - name: Check solver resource use
         shell: bash
-        working-directory: ./${{ matrix.library }}
+        working-directory: ./DynamoDbEncryption
         run: |
           make dafny-reportgenerator

.gitmodules

@@ -1,6 +1,3 @@
-[submodule "polymorph"]
-	path = polymorph
-	url = [email protected]:awslabs/polymorph.git
-[submodule "private-aws-encryption-sdk-dafny-staging"]
-	path = private-aws-encryption-sdk-dafny-staging
+[submodule "submodules/MaterialProviders"]
+	path = submodules/MaterialProviders
 	url = [email protected]:aws/private-aws-encryption-sdk-dafny-staging.git

DynamoDbEncryptionMiddlewareInternal/.gitignore renamed to DynamoDbEncryption/.gitignore

@@ -1,18 +1,70 @@
 # Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: Apache-2.0
 
-ROOT_DIR:=$(shell dirname $(realpath $(firstword $(MAKEFILE_LIST))))
-DEPS_DIR:=$(ROOT_DIR)/../private-aws-encryption-sdk-dafny-staging
+CORES=2
 
-build_java_dependencies:
-	$(MAKE) -C $(ROOT_DIR)/../DynamoDbEncryptionMiddlewareInternal build_java
-	$(MAKE) -C $(ROOT_DIR)/../DynamoDbEncryptionMiddlewareInternal mvn_local_deploy
+include ../SharedMakefile.mk
 
-build_java: build_java_dependencies
-	gradle -p runtimes/java build
+SMITHY_NAMESPACES := \
+	aws.cryptography.structuredEncryption \
+	aws.cryptography.dynamoDbEncryption \
+	aws.cryptography.dynamoDbEncryption.itemEncryptor \
+	aws.cryptography.dynamoDbEncryption.transforms
+MAX_RESOURCE_COUNT=10000000
+# Order is important
+# In java they MUST be built
+# in the order they depend on each other
+LIBRARIES := \
+	submodules/MaterialProviders/AwsCryptographyPrimitives \
+	submodules/MaterialProviders/ComAmazonawsKms \
+	submodules/MaterialProviders/ComAmazonawsDynamodb \
+	submodules/MaterialProviders/AwsCryptographicMaterialProviders
+STD_LIBRARY=submodules/MaterialProviders/StandardLibrary
+SMITHY_DEPS=submodules/MaterialProviders/model
 
-mvn_local_deploy:
-	gradle -p runtimes/java publishToMavenLocal
+format_net:
+	pushd runtimes/net && dotnet format DynamoDbEncryption.csproj && popd
 
-test_java:
-	gradle -p runtimes/java test
+# Transpiling the entire project can take a while (~10 minutes),
+# So these custom written targets can be used to short-circuit the process
+# and only transpile Dafny code for a specific namespace,
+# e.g. No transpiling other namespaces
+# and no transpiling and deploying dependencies.
+# Note that these targets don't do any sort of 'clean'.
+# If you are adding/renaming files, you should use `make build_java` first,
+# and then can use these targets if you need to re-transpile after making
+# smaller adjustments.
+# TODO Improve/Generalize these targets into the SharedMakefile
+transpile_impl_namespace_%: TARGET=java
+transpile_impl_namespace_%: OUT=runtimes/java/ImplementationFromDafny
+transpile_impl_namespace_%:
+	dafny \
+		-vcsCores:$(CORES) \
+		-compileTarget:$(TARGET) \
+		-spillTargetCode:3 \
+		-compile:0 \
+		-optimizeErasableDatatypeWrapper:0 \
+		-useRuntimeLib \
+		-out $(OUT) \
+		./src/$*/Index.dfy \
+		-library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy \
+		$(patsubst %, -library:$(PROJECT_ROOT)/%/src/Index.dfy, $(LIBRARIES));
+	cp -R runtimes/java/ImplementationFromDafny-java/* runtimes/java/src/main/dafny-generated
+	rm -rf runtimes/java/ImplementationFromDafny-java/
+
+transpile_test_namespace_%: TARGET=java
+transpile_test_namespace_%: OUT=runtimes/java/TestsFromDafny
+transpile_test_namespace_%:
+	dafny \
+		-vcsCores:$(CORES) \
+		-compileTarget:$(TARGET) \
+		-spillTargetCode:3 \
+		-runAllTests:1 \
+		-compile:0 \
+		-optimizeErasableDatatypeWrapper:0 \
+		-useRuntimeLib \
+		-out $(OUT) \
+		`find ./test/$* -name '*.dfy'` \
+		-library:src/Index.dfy;
+	cp -R runtimes/java/TestsFromDafny-java/* runtimes/java/src/test/dafny-generated
+	rm -rf runtimes/java/TestsFromDafny-java

DynamoDbEncryption/Makefile

@@ -1,17 +1,17 @@
 // 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 "../../private-aws-encryption-sdk-dafny-staging/StandardLibrary/src/Index.dfy"
- include "../../StructuredEncryption/src/Index.dfy"
- include "../../private-aws-encryption-sdk-dafny-staging/AwsCryptographicMaterialProviders/src/Index.dfy"
- include "../../private-aws-encryption-sdk-dafny-staging/AwsCryptographyPrimitives/src/Index.dfy"
- include "../../private-aws-encryption-sdk-dafny-staging/ComAmazonawsDynamodb/src/Index.dfy"
- module {:extern "Dafny.Aws.Cryptography.DynamoDbItemEncryptor.Types" } AwsCryptographyDynamoDbItemEncryptorTypes
+include "../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
+ include "../src/Index.dfy"
+ include "../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/src/Index.dfy"
+ include "../../submodules/MaterialProviders/AwsCryptographyPrimitives/src/Index.dfy"
+ include "../../submodules/MaterialProviders/ComAmazonawsDynamodb/src/Index.dfy"
+ module {:extern "Dafny.Aws.Cryptography.DynamoDbEncryption.ItemEncryptor.Types" } AwsCryptographyDynamoDbEncryptionItemEncryptorTypes
  {
  import opened Wrappers
  import opened StandardLibrary.UInt
  import opened UTF8
- import AwsCryptographyStructuredEncryptionTypes
+ import AwsCryptographyDynamoDbEncryptionTypes
  import AwsCryptographyMaterialProvidersTypes
  import AwsCryptographyPrimitivesTypes
  import ComAmazonawsDynamodbTypes
@@ -20,7 +20,6 @@ include "../../private-aws-encryption-sdk-dafny-staging/StandardLibrary/src/Inde
 
  // Begin Generated Types
 
- type AttributeActions = map<ComAmazonawsDynamodbTypes.AttributeName, AwsCryptographyStructuredEncryptionTypes.CryptoAction>
  datatype DecryptItemInput = | DecryptItemInput (
  nameonly encryptedItem: ComAmazonawsDynamodbTypes.AttributeMap
  )
@@ -97,72 +96,27 @@ include "../../private-aws-encryption-sdk-dafny-staging/StandardLibrary/src/Inde
  nameonly tableName: ComAmazonawsDynamodbTypes.TableName ,
  nameonly partitionKeyName: ComAmazonawsDynamodbTypes.KeySchemaAttributeName ,
  nameonly sortKeyName: Option<ComAmazonawsDynamodbTypes.KeySchemaAttributeName> ,
- nameonly attributeActions: AttributeActions ,
+ nameonly attributeActions: AwsCryptographyDynamoDbEncryptionTypes.AttributeActions ,
  nameonly allowedUnauthenticatedAttributes: Option<ComAmazonawsDynamodbTypes.AttributeNameList> ,
  nameonly allowedUnauthenticatedAttributePrefix: Option<string> ,
  nameonly algorithmSuiteId: Option<AwsCryptographyMaterialProvidersTypes.DBEAlgorithmSuiteId> ,
  nameonly keyring: Option<AwsCryptographyMaterialProvidersTypes.IKeyring> ,
  nameonly cmm: Option<AwsCryptographyMaterialProvidersTypes.ICryptographicMaterialsManager> ,
- nameonly legacyConfig: Option<LegacyConfig>
+ nameonly legacyConfig: Option<AwsCryptographyDynamoDbEncryptionTypes.LegacyConfig>
  )
  datatype EncryptItemInput = | EncryptItemInput (
  nameonly plaintextItem: ComAmazonawsDynamodbTypes.AttributeMap
  )
  datatype EncryptItemOutput = | EncryptItemOutput (
  nameonly encryptedItem: ComAmazonawsDynamodbTypes.AttributeMap
  )
- datatype LegacyConfig = | LegacyConfig (
- nameonly policy: LegacyPolicy ,
- nameonly encryptor: ILegacyDynamoDbEncryptor ,
- nameonly attributeFlags: AttributeActions ,
- nameonly defaultAttributeFlag: Option<AwsCryptographyStructuredEncryptionTypes.CryptoAction>
- )
- class ILegacyDynamoDbEncryptorCallHistory {
- ghost constructor() {
- 
-}
- 
-}
- trait {:termination false} ILegacyDynamoDbEncryptor
- {
- // Helper to define any additional modifies/reads clauses.
- // If your operations need to mutate state,
- // add it in your constructor function:
- // Modifies := {your, fields, here, History};
- // If you do not need to mutate anything:
-// Modifies := {History};
-
- ghost const Modifies: set<object>
- // For an unassigned field defined in a trait,
- // Dafny can only assign a value in the constructor.
- // This means that for Dafny to reason about this value,
- // it needs some way to know (an invariant),
- // about the state of the object.
- // This builds on the Valid/Repr paradigm
- // To make this kind requires safe to add
- // to methods called from unverified code,
- // the predicate MUST NOT take any arguments.
- // This means that the correctness of this requires
- // MUST only be evaluated by the class itself.
- // If you require any additional mutation,
- // then you MUST ensure everything you need in ValidState.
- // You MUST also ensure ValidState in your constructor.
- predicate ValidState()
- ensures ValidState() ==> History in Modifies
-  ghost const History: ILegacyDynamoDbEncryptorCallHistory
- 
-}
- datatype LegacyPolicy =
-	| REQUIRE_ENCRYPT_ALLOW_DECRYPT
-	| FORBID_ENCRYPT_ALLOW_DECRYPT
-	| FORBID_ENCRYPT_FORBID_DECRYPT
  datatype Error =
  // Local Error structures are listed here
  | DynamoDbItemEncryptorException (
  nameonly message: string
  )
  // Any dependent models are listed here
- | AwsCryptographyStructuredEncryption(AwsCryptographyStructuredEncryption: AwsCryptographyStructuredEncryptionTypes.Error)
+ | AwsCryptographyDynamoDbEncryption(AwsCryptographyDynamoDbEncryption: AwsCryptographyDynamoDbEncryptionTypes.Error)
  | AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders: AwsCryptographyMaterialProvidersTypes.Error)
  | AwsCryptographyPrimitives(AwsCryptographyPrimitives: AwsCryptographyPrimitivesTypes.Error)
  | ComAmazonawsDynamodb(ComAmazonawsDynamodb: ComAmazonawsDynamodbTypes.Error)
@@ -194,13 +148,13 @@ include "../../private-aws-encryption-sdk-dafny-staging/StandardLibrary/src/Inde
  | Opaque(obj: object)
  type OpaqueError = e: Error | e.Opaque? witness *
 }
- abstract module AbstractAwsCryptographyDynamoDbItemEncryptorService
+ abstract module AbstractAwsCryptographyDynamoDbEncryptionItemEncryptorService
  {
  import opened Wrappers
  import opened StandardLibrary.UInt
  import opened UTF8
- import opened Types = AwsCryptographyDynamoDbItemEncryptorTypes
- import Operations : AbstractAwsCryptographyDynamoDbItemEncryptorOperations
+ import opened Types = AwsCryptographyDynamoDbEncryptionItemEncryptorTypes
+ import Operations : AbstractAwsCryptographyDynamoDbEncryptionItemEncryptorOperations
  function method DefaultDynamoDbItemEncryptorConfig(): DynamoDbItemEncryptorConfig
  method DynamoDbItemEncryptor(config: DynamoDbItemEncryptorConfig := DefaultDynamoDbItemEncryptorConfig())
  returns (res: Result<DynamoDbItemEncryptorClient, Error>)
@@ -297,11 +251,11 @@ include "../../private-aws-encryption-sdk-dafny-staging/StandardLibrary/src/Inde
 
 }
 }
- abstract module AbstractAwsCryptographyDynamoDbItemEncryptorOperations {
+ abstract module AbstractAwsCryptographyDynamoDbEncryptionItemEncryptorOperations {
  import opened Wrappers
  import opened StandardLibrary.UInt
  import opened UTF8
- import opened Types = AwsCryptographyDynamoDbItemEncryptorTypes
+ import opened Types = AwsCryptographyDynamoDbEncryptionItemEncryptorTypes
  type InternalConfig
  predicate ValidInternalConfig?(config: InternalConfig)
  function ModifiesInternalConfig(config: InternalConfig): set<object>