From 0b4b47e5db84b80cdb1d8dd2e1c44c6856a122c0 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 7 May 2025 10:02:11 -0700 Subject: [PATCH 01/10] Add GetDefaultKeysPath --- TestVectors/dafny/DDBEncryption/src/Index.dfy | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/Index.dfy b/TestVectors/dafny/DDBEncryption/src/Index.dfy index 18bbec5f9..0eef6cba0 100644 --- a/TestVectors/dafny/DDBEncryption/src/Index.dfy +++ b/TestVectors/dafny/DDBEncryption/src/Index.dfy @@ -19,8 +19,14 @@ module WrappedDDBEncryptionMain { import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes import WrappedItemEncryptor - // TODO: Add extern for DEFAULT_KEYS - const DEFAULT_KEYS : string := "../../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json" + function method GetDefaultKeysPath(): string + { + var mplKeysPath := "submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"; + if OsLang.GetLanguageShort() == "Go" then + "../../../../" + mplKeysPath + else + "../../../" + mplKeysPath + } method AddJson(prev : TestVectorConfig, file : string, keyVectors: KeyVectors.KeyVectorsClient) returns (output : Result) @@ -52,7 +58,7 @@ module WrappedDDBEncryptionMain { // Parsing JSON is very slow in Python. Parse JSON as infrequently as possible. var keyVectors :- expect KeyVectors.KeyVectors( KeyVectorsTypes.KeyVectorsConfig( - keyManifestPath := DEFAULT_KEYS + keyManifestPath := GetDefaultKeysPath() ) ); From cd65595ed4f6701465d4dbfb2a7b50abf8bbf81e Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 7 May 2025 10:04:34 -0700 Subject: [PATCH 02/10] emtpy commit to run CI From 562e86eb9b7524e2c972c927c6e9398b2386b6f3 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 7 May 2025 10:08:08 -0700 Subject: [PATCH 03/10] CI fix --- .github/workflows/pull.yml | 156 ++++++++++++++++++------------------- 1 file changed, 77 insertions(+), 79 deletions(-) diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index 3263bdf7d..8d8871dbe 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -7,93 +7,91 @@ on: push: branches: - Golang/reviewed - schedule: - - cron: "00 16 * * 1-5" jobs: getVersion: uses: ./.github/workflows/dafny_version.yml getVerifyVersion: uses: ./.github/workflows/dafny_verify_version.yml - # pr-ci-format: - # needs: getVersion - # uses: ./.github/workflows/library_format.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} - # pr-ci-codegen: - # needs: getVersion - # uses: ./.github/workflows/ci_codegen.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} - # pr-ci-verification: - # needs: getVerifyVersion - # uses: ./.github/workflows/library_dafny_verification.yml - # with: - # dafny: ${{needs.getVerifyVersion.outputs.version}} - # pr-ci-test-vector-verification: - # needs: getVerifyVersion - # uses: ./.github/workflows/test_vector_verification.yml - # with: - # dafny: ${{needs.getVerifyVersion.outputs.version}} - # pr-ci-java: - # needs: getVersion - # uses: ./.github/workflows/ci_test_java.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} - # pr-ci-java-test-vectors: - # needs: getVersion - # uses: ./.github/workflows/ci_test_vector_java.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} - # pr-ci-java-examples: - # needs: getVersion - # uses: ./.github/workflows/ci_examples_java.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} - # pr-ci-net: - # needs: getVersion - # uses: ./.github/workflows/ci_test_net.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} - # pr-ci-rust: - # needs: getVersion - # uses: ./.github/workflows/library_rust_tests.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} + pr-ci-format: + needs: getVersion + uses: ./.github/workflows/library_format.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-codegen: + needs: getVersion + uses: ./.github/workflows/ci_codegen.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-verification: + needs: getVerifyVersion + uses: ./.github/workflows/library_dafny_verification.yml + with: + dafny: ${{needs.getVerifyVersion.outputs.version}} + pr-ci-test-vector-verification: + needs: getVerifyVersion + uses: ./.github/workflows/test_vector_verification.yml + with: + dafny: ${{needs.getVerifyVersion.outputs.version}} + pr-ci-java: + needs: getVersion + uses: ./.github/workflows/ci_test_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-java-test-vectors: + needs: getVersion + uses: ./.github/workflows/ci_test_vector_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-java-examples: + needs: getVersion + uses: ./.github/workflows/ci_examples_java.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-net: + needs: getVersion + uses: ./.github/workflows/ci_test_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-rust: + needs: getVersion + uses: ./.github/workflows/library_rust_tests.yml + with: + dafny: ${{needs.getVersion.outputs.version}} pr-ci-go: needs: getVersion uses: ./.github/workflows/ci_test_go.yml with: dafny: ${{needs.getVersion.outputs.version}} - # pr-ci-net-test-vectors: - # needs: getVersion - # uses: ./.github/workflows/ci_test_vector_net.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} - # pr-ci-net-examples: - # needs: getVersion - # uses: ./.github/workflows/ci_examples_net.yml - # with: - # dafny: ${{needs.getVersion.outputs.version}} - # pr-ci-all-required: - # if: always() - # needs: - # - getVersion - # - getVerifyVersion - # - pr-ci-format - # - pr-ci-codegen - # - pr-ci-verification - # - pr-ci-test-vector-verification - # - pr-ci-java - # - pr-ci-java-test-vectors - # - pr-ci-java-examples - # - pr-ci-net - # - pr-ci-rust - # - pr-ci-net-test-vectors - # - pr-ci-net-examples - # runs-on: ubuntu-22.04 - # steps: - # - name: Verify all required jobs passed - # uses: re-actors/alls-green@release/v1 - # with: - # jobs: ${{ toJSON(needs) }} + pr-ci-net-test-vectors: + needs: getVersion + uses: ./.github/workflows/ci_test_vector_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-net-examples: + needs: getVersion + uses: ./.github/workflows/ci_examples_net.yml + with: + dafny: ${{needs.getVersion.outputs.version}} + pr-ci-all-required: + if: always() + needs: + - getVersion + - getVerifyVersion + - pr-ci-format + - pr-ci-codegen + - pr-ci-verification + - pr-ci-test-vector-verification + - pr-ci-java + - pr-ci-java-test-vectors + - pr-ci-java-examples + - pr-ci-net + - pr-ci-rust + - pr-ci-net-test-vectors + - pr-ci-net-examples + runs-on: ubuntu-22.04 + steps: + - name: Verify all required jobs passed + uses: re-actors/alls-green@release/v1 + with: + jobs: ${{ toJSON(needs) }} From 104ccf80a286a417f3276e63935cafa8b3b711aa Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 7 May 2025 10:09:48 -0700 Subject: [PATCH 04/10] push CI --- .github/workflows/push.yml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 87e339c11..a650ef74b 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -5,7 +5,7 @@ name: Push CI on: push: branches: - - main + - Golang/reviewed jobs: getVersion: @@ -57,6 +57,11 @@ jobs: uses: ./.github/workflows/library_rust_tests.yml with: dafny: ${{needs.getVersion.outputs.version}} + pr-ci-go: + needs: getVersion + uses: ./.github/workflows/ci_test_go.yml + with: + dafny: ${{needs.getVersion.outputs.version}} pr-ci-net-test-vectors: needs: getVersion uses: ./.github/workflows/ci_test_vector_net.yml From 0c2de3554f4411270ebb36e91c1dc827f843a981 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 7 May 2025 10:12:35 -0700 Subject: [PATCH 05/10] formatting --- .github/workflows/ci_test_go.yml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci_test_go.yml b/.github/workflows/ci_test_go.yml index 30fd1d363..be82f2954 100644 --- a/.github/workflows/ci_test_go.yml +++ b/.github/workflows/ci_test_go.yml @@ -45,7 +45,7 @@ jobs: with: port: 8000 cors: "*" - + - name: Support longpaths run: | git config --global core.longpaths true @@ -68,7 +68,7 @@ jobs: - name: Create temporary global.json run: echo '{"sdk":{"rollForward":"latestFeature","version":"6.0.0"}}' > ./global.json - + - name: Setup Java 17 for codegen uses: actions/setup-java@v3 with: @@ -104,7 +104,7 @@ jobs: run: | git submodule update --init --recursive submodules/smithy-dafny git submodule update --init --recursive submodules/MaterialProviders - + - name: Install Smithy-Dafny codegen dependencies uses: ./.github/actions/install_smithy_dafny_codegen_dependencies @@ -121,14 +121,14 @@ jobs: working-directory: ./${{ matrix.library }} run: | make polymorph_go - + - name: Copy ${{ matrix.library }} Vector Files if: ${{ matrix.library == 'TestVectors' }} shell: bash working-directory: ./${{ matrix.library }} run: | cp runtimes/java/*.json runtimes/go/TestsFromDafny-go/ - + - name: Test ${{ matrix.library }} working-directory: ./${{ matrix.library }} run: | From 9d288cd21689e3b2a8a3de73919c2a8e58edaead Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 7 May 2025 10:22:58 -0700 Subject: [PATCH 06/10] formatting --- .github/workflows/ci_todos.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci_todos.yml b/.github/workflows/ci_todos.yml index 045e051bf..98911f419 100644 --- a/.github/workflows/ci_todos.yml +++ b/.github/workflows/ci_todos.yml @@ -22,4 +22,4 @@ # GOOD_TODO_COUNT=$( { grep -r "TODO.*\(github.com\/.*issues.*\/[1-9][0-9]*\|CrypTool-[1-9][0-9]*\)" . --exclude-dir=./releases --exclude-dir=./submodules --exclude-dir=./.git --exclude-dir=./TestVectors/runtimes --exclude=./.github/workflows/ci_todos.yml || true; } | wc -l) # if [ "$ALL_TODO_COUNT" != "$GOOD_TODO_COUNT" ]; then # exit 1; -# fi \ No newline at end of file +# fi From c48a7fd92559bc85d2743fd84a6fbfffd69a4dcb Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 7 May 2025 10:38:13 -0700 Subject: [PATCH 07/10] submodules update --- submodules/smithy-dafny | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny index 276aacb93..2f83e28ad 160000 --- a/submodules/smithy-dafny +++ b/submodules/smithy-dafny @@ -1 +1 @@ -Subproject commit 276aacb938b78401f0f50006c01195e7d241b216 +Subproject commit 2f83e28ad9532b24c93d2229476c9a268355d338 From e9834045ac7ed362158da20ba4ccc8880f99ecd3 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 7 May 2025 10:40:26 -0700 Subject: [PATCH 08/10] formatting --- DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy | 2 +- .../dafny/DynamoDbEncryptionTransforms/src/Index.dfy | 2 +- DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy | 2 +- DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy index d4dc6e5ff..13624c005 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy @@ -16,7 +16,7 @@ include "UpdateExpr.dfy" include "Util.dfy" include "Virtual.dfy" -module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny" } DynamoDbEncryption +module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny" } DynamoDbEncryption refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbService { import Operations = AwsCryptographyDbEncryptionSdkDynamoDbOperations diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy index c99791695..e0031bf6e 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy @@ -5,7 +5,7 @@ include "DdbMiddlewareConfig.dfy" include "AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations.dfy" include "../../DynamoDbEncryption/src/ConfigToInfo.dfy" -module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transforms.internaldafny" } DynamoDbEncryptionTransforms +module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transforms.internaldafny" } DynamoDbEncryptionTransforms refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService { import opened DdbMiddlewareConfig diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy index e6a6c53da..4c207afad 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy @@ -4,7 +4,7 @@ include "AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy" include "Util.dfy" -module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny" } DynamoDbItemEncryptor +module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny" } DynamoDbItemEncryptor refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService { import opened DynamoDbItemEncryptorUtil diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy index 2279441ea..5b6d2271b 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy @@ -3,7 +3,7 @@ include "AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy" -module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny" } StructuredEncryption +module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny" } StructuredEncryption refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionService { From d35916e6201e020798ef87e15b641bfe67960cd9 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Wed, 7 May 2025 11:52:18 -0700 Subject: [PATCH 09/10] auto commit --- .github/workflows/ci_test_go.yml | 2 +- .github/workflows/pull.yml | 4 ---- .github/workflows/push.yml | 3 +-- 3 files changed, 2 insertions(+), 7 deletions(-) diff --git a/.github/workflows/ci_test_go.yml b/.github/workflows/ci_test_go.yml index be82f2954..ae0819451 100644 --- a/.github/workflows/ci_test_go.yml +++ b/.github/workflows/ci_test_go.yml @@ -28,7 +28,7 @@ jobs: strategy: matrix: library: [DynamoDbEncryption, TestVectors] - os: [ubuntu-22.04] + os: [ubuntu-22.04, macos-13] go-version: ["1.23"] runs-on: ${{ matrix.os }} permissions: diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index 8d8871dbe..f30d207f9 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -1,12 +1,8 @@ # This workflow runs for every pull request -# TODO: CI for Go name: PR CI on: pull_request: - push: - branches: - - Golang/reviewed jobs: getVersion: diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index a650ef74b..759b154aa 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -1,11 +1,10 @@ # This workflow runs for every push to main -# TODO: CI for Go name: Push CI on: push: branches: - - Golang/reviewed + - main jobs: getVersion: From 1c963108ba26340b63650a96d1b35597ced510be Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 8 May 2025 09:42:42 -0700 Subject: [PATCH 10/10] Add pr-ci-go in pr-ci-all-required --- .github/workflows/pull.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index f30d207f9..0814af19c 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -83,6 +83,7 @@ jobs: - pr-ci-java-examples - pr-ci-net - pr-ci-rust + - pr-ci-go - pr-ci-net-test-vectors - pr-ci-net-examples runs-on: ubuntu-22.04