feat: Add smithy->Java codegen to CryptoPrimitives and KMS (#56)

aws · Oct 11, 2023 · 6a5ef00 · 6a5ef00
1 parent 6f61e4e
commit 6a5ef00
Show file tree

Hide file tree

Showing 58 changed files with 8,405 additions and 83 deletions.
diff --git a/.github/workflows/library_java-tests.yml b/.github/workflows/library_java-tests.yml
@@ -32,14 +32,31 @@ jobs:
         uses: aws-actions/configure-aws-credentials@v1
         with:
           aws-region: us-west-2
-          role-to-assume: arn:aws:iam::405437749609:role/Github-OICD-for-private-aws-encryption-sdk-da-Role-15BEGAP519YZV
-          role-session-name: NetTests
+          # TODO: This role was manually created.
+          role-to-assume: arn:aws:iam::370957321024:role/ESDK-Dafny-Private-CA-Read
+          role-session-name: JavaPrivateESDKDafnyTests
 
       - uses: actions/checkout@v3
       # The specification submodule is private so we don't have access, but we don't need
       # it to verify the Dafny code. Instead we manually pull the submodule we DO need.
       - run: git submodule update --init libraries
 
+      # Set up env vars for CodeArtifact
+      - name: Set Up Env Vars for CodeArtifact
+        run: |
+          export URL=`aws codeartifact get-repository-endpoint \
+            --domain github-polymorph \
+            --domain-owner "370957321024" \
+            --repository DafnyJavaConversion \
+            --format maven | jq -r .repositoryEndpoint`
+          export TOKEN=`aws codeartifact get-authorization-token \
+            --domain github-polymorph \
+            --domain-owner "370957321024" \
+            --query authorizationToken \
+            --output text`
+          echo "CODEARTIFACT_URL_JAVA_CONVERSION=$URL" >> $GITHUB_ENV
+          echo "CODEARTIFACT_AUTH_TOKEN=$TOKEN" >> $GITHUB_ENV
+
       - name: Setup Dafny
         uses: dafny-lang/setup-dafny-action@v1.4.0
         with:
@@ -65,17 +82,17 @@ jobs:
           -DgeneratePom=true \
           -Dpackaging=jar
 
-      - name: Compile ${{ matrix.library }} implementation
+      - name: Build ${{ matrix.library }} implementation
         shell: bash
         working-directory: ./${{ matrix.library }}
         run: |
           # This works because `node` is installed by default on GHA runners
           CORES=$(node -e 'console.log(os.cpus().length)')
-          make compile_java CORES=$CORES
+          make build_java CORES=$CORES
 
-      # Currently tests do not pass.
+      # TODO: No tests can run without extern implementations
       # - name: Test ${{ matrix.library }}
-      #  working-directory: ./${{ matrix.library }}
-      #  shell: bash
-      #  run: |
-      #    make test_java
+      #   working-directory: ./${{ matrix.library }}
+      #   shell: bash
+      #   run: |
+      #     make test_java
diff --git a/.github/workflows/library_net_tests.yml b/.github/workflows/library_net_tests.yml
@@ -55,7 +55,7 @@ jobs:
         run: |
           # This works because `node` is installed by default on GHA runners
           CORES=$(node -e 'console.log(os.cpus().length)')
-          make compile_net CORES=$CORES
+          make transpile_net CORES=$CORES
 
       - name: Test ${{ matrix.library }}
         working-directory: ./${{ matrix.library }}

diff --git a/AwsCryptographicMaterialProviders/Makefile b/AwsCryptographicMaterialProviders/Makefile
@@ -19,9 +19,9 @@ dafny-reportgenerator:
 		--max-resource-count 10000000 \
 		TestResults/*.csv
 
-compile_net: | compile_implementation_net compile_test_net compile_net_dependencies
+transpile_net: | transpile_implementation_net transpile_test_net transpile_net_dependencies
 
-compile_implementation_net:
+transpile_implementation_net:
 	dafny \
 		-vcsCores:$(CORES) \
 		-compileTarget:cs \
@@ -34,7 +34,7 @@ compile_implementation_net:
 		-library:../ComAmazonawsKms/src/Index.dfy \
 		-library:../StandardLibrary/src/Index.dfy
 
-compile_test_net:
+transpile_test_net:
 	dafny \
 		-vcsCores:$(CORES) \
 		-compileTarget:cs \
@@ -46,10 +46,10 @@ compile_test_net:
 		`find ./test -name '*.dfy'` \
 		-library:src/Index.dfy
 
-compile_net_dependencies:
-	$(MAKE) -C ../StandardLibrary compile_implementation_net
-	$(MAKE) -C ../AwsCryptographyPrimitives compile_implementation_net
-	$(MAKE) -C ../ComAmazonawsKms compile_implementation_net
+transpile_net_dependencies:
+	$(MAKE) -C ../StandardLibrary transpile_implementation_net
+	$(MAKE) -C ../AwsCryptographyPrimitives transpile_implementation_net
+	$(MAKE) -C ../ComAmazonawsKms transpile_implementation_net
 
 test_net:
 	dotnet run \

diff --git a/AwsCryptographyPrimitives/Makefile b/AwsCryptographyPrimitives/Makefile
@@ -19,9 +19,9 @@ dafny-reportgenerator:
 		--max-resource-count 10000000 \
 		TestResults/*.csv
 
-compile_net: | compile_implementation_net compile_test_net compile_net_dependencies
+transpile_net: | transpile_implementation_net transpile_test_net transpile_net_dependencies
 
-compile_implementation_net:
+transpile_implementation_net:
 	dafny \
 		-vcsCores:$(CORES) \
 		-compileTarget:cs \
@@ -32,7 +32,7 @@ compile_implementation_net:
 		./src/Index.dfy \
 		-library:../StandardLibrary/src/Index.dfy
 
-compile_test_net:
+transpile_test_net:
 	dafny \
 		-vcsCores:$(CORES) \
 		-compileTarget:cs \
@@ -44,8 +44,8 @@ compile_test_net:
 		`find ./test -name '*.dfy'` \
 		-library:src/Index.dfy
 
-compile_net_dependencies:
-	$(MAKE) -C ../StandardLibrary compile_implementation_net
+transpile_net_dependencies:
+	$(MAKE) -C ../StandardLibrary transpile_implementation_net
 
 test_net:
 	dotnet run \
@@ -60,14 +60,14 @@ test_net_mac_intel:
 setup_net:
 	dotnet restore runtimes/net/
 
-compile_java: | compile_implementation_java compile_test_java compile_java_dependencies
+transpile_java: | transpile_implementation_java transpile_test_java
 
-compile_implementation_java: | _clean_implementation_java _compile_implementation_java _mv_implementation_java
+transpile_implementation_java: | _clean_implementation_java _transpile_implementation_java _mv_implementation_java
 
 _clean_implementation_java:
 	rm -rf runtimes/java/temp/AwsCryptographyPrimitives-java/* && rm -rf runtimes/java/src/main/dafny-generated/*
 
-_compile_implementation_java:
+_transpile_implementation_java:
 	dafny \
 		-vcsCores:$(CORES) \
 		-compileTarget:java \
@@ -81,12 +81,13 @@ _compile_implementation_java:
 _mv_implementation_java:
 	./runtimes/java/makefile_helper.sh implementation
 
-compile_test_java: | _clean_test_java _compile_test_java _mv_test_java
+transpile_test_java: | _clean_test_java _transpile_test_java _mv_test_java
 
 _clean_test_java:
 	rm -rf runtimes/java/temp-tests/AwsCryptographyPrimitivesTests-java/* && rm -rf runtimes/java/src/test/dafny-generated/*
 
-_compile_test_java:
+# TODO test all Dafny tests. Currently only testing a subset of implemented externs
+_transpile_test_java:
 	dafny \
 		-vcsCores:$(CORES) \
 		-compileTarget:java \
@@ -101,8 +102,11 @@ _compile_test_java:
 _mv_test_java:
 	./runtimes/java/makefile_helper.sh test
 
-compile_java_dependencies:
+build_java_dependencies:
 	$(MAKE) -C ../StandardLibrary mvn_local_deploy
 
+build_java: transpile_java build_java_dependencies
+	gradle -p runtimes/java build
+
 test_java:
 	gradle -p runtimes/java runTests
diff --git a/AwsCryptographyPrimitives/runtimes/java/build.gradle.kts b/AwsCryptographyPrimitives/runtimes/java/build.gradle.kts
@@ -1,3 +1,6 @@
+import java.net.URI
+import javax.annotation.Nullable
+
 plugins {
     `java-library`
     `maven-publish`
@@ -19,13 +22,38 @@ java {
     }
 }
 
+var caUrl: URI? = null
+@Nullable
+val caUrlStr: String? = System.getenv("CODEARTIFACT_URL_JAVA_CONVERSION")
+if (!caUrlStr.isNullOrBlank()) {
+    caUrl = URI.create(caUrlStr)
+}
+
+var caPassword: String? = null
+@Nullable
+val caPasswordString: String? = System.getenv("CODEARTIFACT_AUTH_TOKEN")
+if (!caPasswordString.isNullOrBlank()) {
+    caPassword = caPasswordString
+}
+
 repositories {
     mavenCentral()
     mavenLocal()
+    if (caUrl != null && caPassword != null) {
+        maven {
+            name = "CodeArtifact"
+            url = caUrl!!
+            credentials {
+                username = "aws"
+                password = caPassword!!
+            }
+        }
+    }
 }
 
 dependencies {
     implementation("dafny.lang:DafnyRuntime:3.10.0")
+    implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
     implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
 }
 

diff --git a/AwsCryptographyPrimitives/runtimes/java/makefile_helper.sh b/AwsCryptographyPrimitives/runtimes/java/makefile_helper.sh
@@ -1,21 +1,21 @@
 #!/bin/bash
 
 if [[ "$1" == "implementation" ]]; then
-    mkdir -p runtimes/java/src/main/dafny-generated
+  mkdir -p runtimes/java/src/main/dafny-generated
 	for directory in runtimes/java/temp/AwsCryptographyPrimitives-java/*; do
 		mv "$directory" "runtimes/java/src/main/dafny-generated/"
 	done
-    exit 0
+  exit 0
 elif [[ "$1" == "test" ]]; then
-    # With the runAllTests flag, dafny generates an entry point for the tests that we want,
-    # so we copy all files to the test destination.
-    mkdir -p runtimes/java/src/test/dafny-generated
-    for allFiles in runtimes/java/temp-tests/AwsCryptographyPrimitivesTests-java/*; do
+  # With the runAllTests flag, dafny generates an entry point for the tests that we want,
+  # so we copy all files to the test destination.
+  mkdir -p runtimes/java/src/test/dafny-generated
+  for allFiles in runtimes/java/temp-tests/AwsCryptographyPrimitivesTests-java/*; do
 		mv "$allFiles" "runtimes/java/src/test/dafny-generated/"
 	done
-    exit 0
+  exit 0
 else
-    echo "makefile_helper needs either implementation or test argument"
-    echo "i.e: ./runtimes/java/makefile_helper.sh test"
-    exit 1
+  echo "makefile_helper needs either implementation or test argument"
+  echo "i.e: ./runtimes/java/makefile_helper.sh test"
+  exit 1
 fi