diff --git a/.github/workflows/ci_test_go.yml b/.github/workflows/ci_test_go.yml index 30fd1d363..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: @@ -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: | 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 diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index 3263bdf7d..0814af19c 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -1,99 +1,94 @@ # This workflow runs for every pull request -# TODO: CI for Go name: PR CI on: pull_request: - 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-go + - 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) }} diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 87e339c11..759b154aa 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -1,5 +1,4 @@ # This workflow runs for every push to main -# TODO: CI for Go name: Push CI on: @@ -57,6 +56,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 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/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 { 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() ) ); 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