From 2c9bb7454696789411d0ad89728ffecdc43e7a65 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Wed, 21 Aug 2024 13:43:29 -0700 Subject: [PATCH 1/8] chore: Rename AtomicPrimitives Dafny module name --- .../dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy | 2 +- AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy | 2 +- AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy | 2 +- AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy | 2 +- AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy | 2 +- AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy | 2 +- mpl | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy index 695b3379d..1a89973e7 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy @@ -17,7 +17,7 @@ include "Serialize/EncryptionContext.dfy" module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOperations { - import Aws.Cryptography.Primitives + import Primitives = AtomicPrimitives import MPL = AwsCryptographyMaterialProvidersTypes import MaterialProviders import EncryptDecryptHelpers diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy index 6a3762abe..5825b02cf 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy @@ -15,7 +15,7 @@ module EncryptDecryptHelpers { import Types = AwsCryptographyEncryptionSdkTypes import MPL = AwsCryptographyMaterialProvidersTypes import MaterialProviders - import Aws.Cryptography.Primitives + import Primitives = AtomicPrimitives import MessageBody import SerializableTypes import opened SerializeFunctions diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy index cf46c3714..ab851b1a8 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy @@ -7,7 +7,7 @@ module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny" } EncryptionSdk refines AbstractAwsCryptographyEncryptionSdkService { import Operations = AwsEncryptionSdkOperations - import Aws.Cryptography.Primitives + import Primitives = AtomicPrimitives import MaterialProviders import AwsCryptographyMaterialProvidersTypes diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy index 2607f528c..2456f756e 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy @@ -12,7 +12,7 @@ module KeyDerivation { import Types = AwsCryptographyEncryptionSdkTypes import MPL = AwsCryptographyMaterialProvidersTypes import AwsCryptographyPrimitivesTypes - import Aws.Cryptography.Primitives + import Primitives = AtomicPrimitives import HeaderTypes import SerializableTypes diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy index 68315907a..0c0199111 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy @@ -22,7 +22,7 @@ module MessageBody { import opened UInt = StandardLibrary.UInt import Types = AwsCryptographyEncryptionSdkTypes import MPL = AwsCryptographyMaterialProvidersTypes - import Aws.Cryptography.Primitives + import Primitives = AtomicPrimitives import Streams import UTF8 import SerializableTypes diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy index b7edf42a6..a7d7d5652 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy @@ -9,7 +9,7 @@ module Fixtures { import primitivesTypes = AwsCryptographyPrimitivesTypes import mplTypes = AwsCryptographyMaterialProvidersTypes import opened UInt = StandardLibrary.UInt - import Aws.Cryptography.Primitives + import Primitives = AtomicPrimitives // The following are test resources that exist in tests accounts: diff --git a/mpl b/mpl index cdd4885cb..1baeefb60 160000 --- a/mpl +++ b/mpl @@ -1 +1 @@ -Subproject commit cdd4885cb22957b04167b11d8b40edbdf4301d8d +Subproject commit 1baeefb6064199cc899b8c10203e7f5b0a503702 From a7d37c5732af71e2338851f6ecd907399277f1c3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Corella?= <39066999+josecorella@users.noreply.github.com> Date: Mon, 26 Aug 2024 14:07:24 -0700 Subject: [PATCH 2/8] chore: update mpl submodule name gha (#675) --- .github/workflows/dafny_interop_test_net.yml | 2 +- .github/workflows/dafny_interop_test_vector_net.yml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/dafny_interop_test_net.yml b/.github/workflows/dafny_interop_test_net.yml index 7c4b447a2..54c4db81b 100644 --- a/.github/workflows/dafny_interop_test_net.yml +++ b/.github/workflows/dafny_interop_test_net.yml @@ -55,7 +55,7 @@ jobs: dafny-version: ${{ inputs.mpl-dafny }} - name: Update MPL submodule - working-directory: submodules/MaterialProviders + working-directory: mpl run: | git fetch git checkout ${{inputs.mpl-commit}} diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml index 7343e363d..3e403b60d 100644 --- a/.github/workflows/dafny_interop_test_vector_net.yml +++ b/.github/workflows/dafny_interop_test_vector_net.yml @@ -65,7 +65,7 @@ jobs: dafny-version: ${{ inputs.mpl-dafny }} - name: Update MPL submodule - working-directory: submodules/MaterialProviders + working-directory: mpl run: | git fetch git checkout ${{inputs.mpl-commit}} @@ -175,7 +175,7 @@ jobs: dafny-version: ${{ inputs.mpl-dafny }} - name: Update MPL submodule - working-directory: submodules/MaterialProviders + working-directory: mpl run: | git fetch git checkout ${{inputs.mpl-commit}} @@ -305,4 +305,4 @@ jobs: run: | NET_41_VECTOR_PATH=net41/vectors cd $NET_41_VECTOR_PATH - npx -y @aws-crypto/integration-node decrypt -v net41.zip -c cpu -f 100 \ No newline at end of file + npx -y @aws-crypto/integration-node decrypt -v net41.zip -c cpu -f 100 From 44ae65ee64cb68def6fc6a8395c4fa7597b04389 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Corella?= <39066999+josecorella@users.noreply.github.com> Date: Mon, 26 Aug 2024 14:45:18 -0700 Subject: [PATCH 3/8] chore: fix permissions and add env vars (#676) Co-authored-by: Lucas McDonald --- .github/workflows/dafny_interop_test_net.yml | 15 +++++++++++++-- .../workflows/dafny_interop_test_vector_net.yml | 4 ++-- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/.github/workflows/dafny_interop_test_net.yml b/.github/workflows/dafny_interop_test_net.yml index 54c4db81b..5027b630e 100644 --- a/.github/workflows/dafny_interop_test_net.yml +++ b/.github/workflows/dafny_interop_test_net.yml @@ -18,6 +18,17 @@ on: required: true type: string +env: + # Used in examples + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_KEY_ID: arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_KEY_ID_2: arn:aws:kms:eu-central-1:658956600833:key/75414c93-5285-4b57-99c9-30c1cf0a22c2 + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_MRK_KEY_ID: arn:aws:kms:us-east-1:658956600833:key/mrk-80bd8ecdcd4342aebd84b7dc9da498a7 + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_MRK_KEY_ID_2: arn:aws:kms:eu-west-1:658956600833:key/mrk-80bd8ecdcd4342aebd84b7dc9da498a7 + AWS_ENCRYPTION_SDK_EXAMPLE_LIMITED_ROLE_ARN_US_EAST_1: arn:aws:iam::370957321024:role/GitHub-CI-ESDK-Dafny-Role-us-west-2 + AWS_ENCRYPTION_SDK_EXAMPLE_LIMITED_ROLE_ARN_EU_WEST_1: arn:aws:iam::370957321024:role/GitHub-CI-ESDK-Dafny-Role-us-west-2 + # Used for Test Vectors + VECTORS_URL: https://github.com/awslabs/aws-encryption-sdk-test-vectors/raw/master/vectors/awses-decrypt/python-2.3.0.zip + jobs: testDotNet: strategy: @@ -71,8 +82,8 @@ jobs: uses: aws-actions/configure-aws-credentials@v4 with: aws-region: us-west-2 - role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2 - role-session-name: DDBEC-Dafny-Net-Tests + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 + role-session-name: NetTests - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} shell: bash diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml index 3e403b60d..d8fb938ae 100644 --- a/.github/workflows/dafny_interop_test_vector_net.yml +++ b/.github/workflows/dafny_interop_test_vector_net.yml @@ -81,8 +81,8 @@ jobs: uses: aws-actions/configure-aws-credentials@v4 with: aws-region: us-west-2 - role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2 - role-session-name: DDBEC-Dafny-Net-Tests + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 + role-session-name: NetTests - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} shell: bash From 6256eca532ec1bb83e5c104b1231ecaa42185deb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Corella?= <39066999+josecorella@users.noreply.github.com> Date: Mon, 26 Aug 2024 16:18:11 -0700 Subject: [PATCH 4/8] chore: use correct dirs in gha (#677) --- .github/workflows/dafny_interop_test_net.yml | 4 ++-- .github/workflows/dafny_interop_test_vector_net.yml | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/dafny_interop_test_net.yml b/.github/workflows/dafny_interop_test_net.yml index 5027b630e..fd56e893e 100644 --- a/.github/workflows/dafny_interop_test_net.yml +++ b/.github/workflows/dafny_interop_test_net.yml @@ -87,7 +87,7 @@ jobs: - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} shell: bash - working-directory: mpl + working-directory: mpl/TestVectorsAwsCryptographicMaterialProviders run: | make setup_net # This works because `node` is installed by default on GHA runners @@ -101,7 +101,7 @@ jobs: - name: Build ESDK implementation shell: bash - working-directory: AwsEncryptionSDK + working-directory: ./AwsEncryptionSDK run: | # This works because `node` is installed by default on GHA runners make transpile_implementation_net diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml index d8fb938ae..2940a1a67 100644 --- a/.github/workflows/dafny_interop_test_vector_net.yml +++ b/.github/workflows/dafny_interop_test_vector_net.yml @@ -86,7 +86,7 @@ jobs: - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} shell: bash - working-directory: mpl + working-directory: mpl/TestVectorsAwsCryptographicMaterialProviders run: | make setup_net # This works because `node` is installed by default on GHA runners @@ -100,7 +100,7 @@ jobs: - name: Build ESDK implementation shell: bash - working-directory: AwsEncryptionSDK + working-directory: ./AwsEncryptionSDK run: | # This works because `node` is installed by default on GHA runners make transpile_implementation_net @@ -191,12 +191,12 @@ jobs: uses: aws-actions/configure-aws-credentials@v4 with: aws-region: us-west-2 - role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2 - role-session-name: DDBEC-Dafny-Net-Tests + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 + role-session-name: NetTests - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} shell: bash - working-directory: mpl + working-directory: mpl/TestVectorsAwsCryptographicMaterialProviders run: | make setup_net # This works because `node` is installed by default on GHA runners From a5c94eee1f3127b4ee3228d23676380de1e450e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Corella?= <39066999+josecorella@users.noreply.github.com> Date: Thu, 29 Aug 2024 11:51:17 -0700 Subject: [PATCH 5/8] chore: add check only keyword action (#679) --- .github/workflows/check_only_keyword.yml | 40 ++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 .github/workflows/check_only_keyword.yml diff --git a/.github/workflows/check_only_keyword.yml b/.github/workflows/check_only_keyword.yml new file mode 100644 index 000000000..94e2fe95a --- /dev/null +++ b/.github/workflows/check_only_keyword.yml @@ -0,0 +1,40 @@ +# This workflow checks if you are checking in dafny code +# with the keyword {:only}, it adds a message to the pull +# request to remind you to remove it. +name: Check {:only} decorator presence + +on: + pull_request: + +jobs: + grep-only-verification-keyword: + runs-on: ubuntu-latest + permissions: + issues: write + pull-requests: write + steps: + - uses: actions/checkout@v3 + with: + fetch-depth: 0 + + - name: Check only keyword + id: only-keyword + shell: bash + run: + # checking in code with the dafny decorator {:only} + # will not verify the entire file or maybe the entire project depending on its configuration + # This action checks if you are either adding or removing the {:only} decorator and posting on the pr if you are. + echo "ONLY_KEYWORD=$(git diff origin/main origin/${GITHUB_HEAD_REF} **/*.dfy | grep -i {:only})" >> "$GITHUB_OUTPUT" + + - name: Check if ONLY_KEYWORD is not empty + id: comment + env: + PR_NUMBER: ${{ github.event.number }} + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + ONLY_KEYWORD: ${{ steps.only-keyword.outputs.ONLY_KEYWORD }} + if: ${{env.ONLY_KEYWORD != ''}} + run: | + COMMENT="It looks like you are adding or removing the dafny keyword {:only}.\nIs this intended?" + COMMENT_URL="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/comments" + curl -s -H "Authorization: token ${GITHUB_TOKEN}" -X POST $COMMENT_URL -d "{\"body\":\"$COMMENT\"}" + exit 1 From fc572659986a4fa63826f599132743b7f882898a Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 24 Sep 2024 15:44:05 -0700 Subject: [PATCH 6/8] merge --- .../action.yml | 21 ++++ .github/actions/polymorph_codegen/action.yml | 26 ++--- .github/workflows/library_codegen.yml | 11 ++- .github/workflows/pull.yml | 8 +- .github/workflows/push.yml | 8 +- .github/workflows/smithy-diff.yml | 11 ++- .../AwsEncryptionSdk/dotnet/dafny-4.8.0.patch | 96 +++++++++++++++++++ .../dafny/AwsEncryptionSdk/Model/esdk.smithy | 3 - AwsEncryptionSDK/project.properties | 3 +- AwsEncryptionSDK/runtimes/net/ESDK.csproj | 2 +- SharedMakefileV2.mk | 7 ++ mpl | 2 +- smithy-dafny | 2 +- 13 files changed, 168 insertions(+), 32 deletions(-) create mode 100644 .github/actions/install_smithy_dafny_codegen_dependencies/action.yml create mode 100644 AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.8.0.patch diff --git a/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml new file mode 100644 index 000000000..da00a4c70 --- /dev/null +++ b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml @@ -0,0 +1,21 @@ +# +# This local action sets up code dependencies +# to run Smithy-Dafny CI in GitHub Actions workflows. +# + +name: "Install Smithy-Dafny codegen dependencies" +description: "Install Java package dependencies required to run Smithy-Dafny codegen" +runs: + using: "composite" + steps: + - name: Install smithy-dafny-codegen Rust dependencies locally + uses: gradle/gradle-build-action@v2 + with: + arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML + build-root-directory: smithy-dafny/smithy-dafny-codegen-modules/smithy-rs + + - name: Install smithy-dafny-codegen Python dependencies locally + uses: gradle/gradle-build-action@v2 + with: + arguments: :smithy-python-codegen:pTML + build-root-directory: smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index 691f1d09c..7f6b4f29b 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -88,18 +88,20 @@ runs: make -C mpl/AwsCryptographicMaterialProviders setup_prettier make -C mpl/ComAmazonawsKms setup_prettier make -C mpl/ComAmazonawsDynamodb setup_prettier - - - name: Regenerate Java code using smithy-dafny - # npx seems to be unavailable on Windows GHA runners, - # so we don't regenerate Java code on them either. - if: runner.os != 'Windows' - working-directory: ./${{ inputs.library }} - shell: bash - # smithy-dafny also formats generated code itself now, - # so prettier is a necessary dependency. - run: | - make setup_prettier - make polymorph_java ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} + + # In the ESDK Dafny it does not make sense to run smithy dafny for java code + # since the java esdk written natively and not through dafny + #- name: Regenerate Java code using smithy-dafny + # # npx seems to be unavailable on Windows GHA runners, + # # so we don't regenerate Java code on them either. + # if: runner.os != 'Windows' + # working-directory: ./${{ inputs.library }} + # shell: bash + # # smithy-dafny also formats generated code itself now, + # # so prettier is a necessary dependency. + # run: | + # make setup_prettier + # make polymorph_java ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} - name: Regenerate .NET code using smithy-dafny working-directory: ./${{ inputs.library }} diff --git a/.github/workflows/library_codegen.yml b/.github/workflows/library_codegen.yml index 9780c1348..e11e71685 100644 --- a/.github/workflows/library_codegen.yml +++ b/.github/workflows/library_codegen.yml @@ -38,7 +38,7 @@ jobs: # it to verify the Dafny code. Instead we manually pull the submodules we DO need. - run: git submodule update --init libraries - run: git submodule update --init --recursive mpl - - run: git submodule update --init smithy-dafny + - run: git submodule update --init --recursive smithy-dafny # Only used to format generated code # and to translate version strings such as "nightly-latest" @@ -53,6 +53,15 @@ jobs: with: dotnet-version: ${{ matrix.dotnet-version }} + - name: Setup Java 17 for codegen + uses: actions/setup-java@v3 + with: + distribution: "corretto" + java-version: "17" + + - name: Install Smithy-Dafny codegen dependencies + uses: ./.github/actions/install_smithy_dafny_codegen_dependencies + - uses: ./.github/actions/polymorph_codegen with: dafny: ${{ env.DAFNY_VERSION }} diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index 523b5149b..655eea31c 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -8,11 +8,11 @@ jobs: pr-ci-codegen: uses: ./.github/workflows/library_codegen.yml with: - dafny: '4.2.0' + dafny: '4.8.0' pr-ci-verification: uses: ./.github/workflows/library_dafny_verification.yml with: - dafny: '4.7.0' + dafny: '4.8.0' # pr-ci-java: # uses: ./.github/workflows/library_java_tests.yml # with: @@ -20,8 +20,8 @@ jobs: pr-ci-net: uses: ./.github/workflows/library_net_tests.yml with: - dafny: '4.2.0' + dafny: '4.8.0' pr-test-vectors: uses: ./.github/workflows/library_interop_tests.yml with: - dafny: '4.2.0' + dafny: '4.8.0' diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 98de8408c..0df538b37 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -10,11 +10,11 @@ jobs: pr-ci-codegen: uses: ./.github/workflows/library_codegen.yml with: - dafny: '4.2.0' + dafny: '4.8.0' push-ci-verification: uses: ./.github/workflows/library_dafny_verification.yml with: - dafny: '4.7.0' + dafny: '4.8.0' # push-ci-java: # uses: ./.github/workflows/library_java_tests.yml # with: @@ -22,8 +22,8 @@ jobs: push-ci-net: uses: ./.github/workflows/library_net_tests.yml with: - dafny: '4.2.0' + dafny: '4.8.0' pr-test-vectors: uses: ./.github/workflows/library_interop_tests.yml with: - dafny: '4.2.0' + dafny: '4.8.0' diff --git a/.github/workflows/smithy-diff.yml b/.github/workflows/smithy-diff.yml index b874861c1..3092c9470 100644 --- a/.github/workflows/smithy-diff.yml +++ b/.github/workflows/smithy-diff.yml @@ -3,7 +3,8 @@ name: Check Smithy Files on: - pull_request: + pull_request_review: + types: [submitted] jobs: require-approvals: @@ -19,20 +20,22 @@ jobs: - name: Get Files changed id: file-changes shell: bash + env: + GITHUB_HEAD: ${{github.event.pull_request.head.ref}} run: # Checks to see if any of the smithy Models are being updated. # Doing this check allows us to catch things like, missing @javadoc trait documentation or bug in smithy dafny that has not be resolved. - echo "FILES=$(git diff --name-only origin/main origin/${GITHUB_HEAD_REF} | grep '\.smithy$' | tr '\n' ' ')" >> "$GITHUB_OUTPUT" + echo "FILES=$(git diff --name-only origin/main origin/${GITHUB_HEAD} | grep '\.smithy$' | tr '\n' ' ')" >> "$GITHUB_OUTPUT" - name: Check if FILES is not empty id: comment env: - PR_NUMBER: ${{ github.event.number }} + PR_NUMBER: ${{ github.event.pull_request.number }} GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} FILES: ${{ steps.file-changes.outputs.FILES }} if: ${{env.FILES != ''}} run: | # TODO: If https://github.com/smithy-lang/smithy-dafny/issues/491 is resolved, remove comment about this issue. - COMMENT="@${{github.actor}}, I noticed you are updating the smithy model files.\nDoes this update need new or updated javadoc trait documentation?\n Are you adding constraints inside list, map or union? Do you know about this issue: https://github.com/smithy-lang/smithy-dafny/issues/491?" + COMMENT="@${{github.event.pull_request.user.login}} and @${{github.actor}}, I noticed you are updating the smithy model files.\nDoes this update need new or updated javadoc trait documentation?\n Are you adding constraints inside list, map or union? Do you know about this issue: https://github.com/smithy-lang/smithy-dafny/issues/491?" COMMENT_URL="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/comments" curl -s -H "Authorization: token ${GITHUB_TOKEN}" -X POST $COMMENT_URL -d "{\"body\":\"$COMMENT\"}" diff --git a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.8.0.patch b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.8.0.patch new file mode 100644 index 000000000..9f2382998 --- /dev/null +++ b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.8.0.patch @@ -0,0 +1,96 @@ +diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs +index 1dc37f40..e2187b21 100644 +--- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs ++++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs +@@ -28,7 +28,7 @@ namespace AWS.Cryptography.EncryptionSDK + { + return this._maxEncryptedDataKeys.HasValue; + } +- public AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy NetV4__0__0__RetryPolicy ++ public AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy NetV4_0_0_RetryPolicy + { + get { return this._netV4_0_0_RetryPolicy; } + set { this._netV4_0_0_RetryPolicy = value; } +diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs +index cb1b30bb..dc6e24f9 100644 +--- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs ++++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs +@@ -7,22 +7,22 @@ namespace AWS.Cryptography.EncryptionSDK + { + public static class TypeConversion + { +- private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z"; +- +- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z"; +- + public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig value) + { + software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig concrete = (software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig)value; AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig converted = new AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig(); if (concrete._commitmentPolicy.is_Some) converted.CommitmentPolicy = (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(concrete._commitmentPolicy); + if (concrete._maxEncryptedDataKeys.is_Some) converted.MaxEncryptedDataKeys = (long)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(concrete._maxEncryptedDataKeys); +- if (concrete._netV4_0_0_RetryPolicy.is_Some) converted.NetV4__0__0__RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4_0_0_RetryPolicy); return converted; ++ // BEGIN MANUAL EDIT ++ if (concrete._netV4__0__0__RetryPolicy.is_Some) converted.NetV4_0_0_RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4__0__0__RetryPolicy); return converted; ++ // END MANUAL EDIT + } + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig value) + { + value.Validate(); + AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy var_commitmentPolicy = value.IsSetCommitmentPolicy() ? value.CommitmentPolicy : (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)null; + long? var_maxEncryptedDataKeys = value.IsSetMaxEncryptedDataKeys() ? value.MaxEncryptedDataKeys : (long?)null; +- AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = value.IsSetNetV4__0__0__RetryPolicy() ? value.NetV4__0__0__RetryPolicy : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; ++ // BEGIN MANUAL EDIT ++ AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = value.IsSetNetV4__0__0__RetryPolicy() ? value.NetV4_0_0_RetryPolicy : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; ++ // END MANUAL EDIT + return new software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(var_commitmentPolicy), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(var_maxEncryptedDataKeys), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(var_netV4_0_0_RetryPolicy)); + } + public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException(software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException value) +@@ -96,16 +96,22 @@ namespace AWS.Cryptography.EncryptionSDK + + return new software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(value.Ciphertext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(value.EncryptionContext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId(value.AlgorithmSuiteId)); + } +- public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy value) ++ // BEGIN MANUAL EDIT ++ public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy value) ++ // END MANUAL EDIT + { + if (value.is_FORBID__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY; + if (value.is_ALLOW__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY; + throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); + } +- public static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) ++ // BEGIN MANUAL EDIT ++ public static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) ++ // END MANUAL EDIT + { +- if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_FORBID__RETRY(); +- if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_ALLOW__RETRY(); ++ // BEGIN MANUAL EDIT ++ if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy.create_FORBID__RETRY(); ++ if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy.create_ALLOW__RETRY(); ++ // END MANUAL EDIT + throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); + } + public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(Wrappers_Compile._IOption value) +@@ -124,13 +130,19 @@ namespace AWS.Cryptography.EncryptionSDK + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers((long)value)); + } +- public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) ++ // BEGIN MANUAL EDIT ++ public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) ++ // END MANUAL EDIT + { + return value.is_None ? (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null : FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(value.Extract()); + } +- public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) ++ // BEGIN MANUAL EDIT ++ public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) ++ // END MANUAL EDIT + { +- return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); ++ // BEGIN MANUAL EDIT ++ return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); ++ // END MANUAL EDIT + } + public static string FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message(Dafny.ISequence value) + { diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/esdk.smithy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/esdk.smithy index ba12c4325..d184d5545 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/esdk.smithy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/esdk.smithy @@ -3,7 +3,6 @@ namespace aws.cryptography.encryptionSdk use aws.cryptography.primitives#AwsCryptographicPrimitives use aws.cryptography.materialProviders#AwsCryptographicMaterialProviders -///////////// // ESDK Client Creation // TODO add a trait to indicate that 'Client' should not be appended to this name, @@ -56,7 +55,6 @@ structure AwsEncryptionSdkConfig { string NetV4_0_0_RetryPolicy -///////////// // ESDK Operations operation Encrypt { @@ -127,7 +125,6 @@ structure DecryptOutput { // the message format and message header in Smithy. } -///////////// // Errors @error("client") diff --git a/AwsEncryptionSDK/project.properties b/AwsEncryptionSDK/project.properties index dd7eb37b9..02e193a7d 100644 --- a/AwsEncryptionSDK/project.properties +++ b/AwsEncryptionSDK/project.properties @@ -1,3 +1,4 @@ # This file stores the top level dafny version information. # All elements of the project need to agree on this version. -dafnyVersion=4.2.0 +dafnyVersion=4.8.0 +dafnyRuntimeJavaVersion=4.8.0 diff --git a/AwsEncryptionSDK/runtimes/net/ESDK.csproj b/AwsEncryptionSDK/runtimes/net/ESDK.csproj index 71d8aa95b..c2abb450e 100644 --- a/AwsEncryptionSDK/runtimes/net/ESDK.csproj +++ b/AwsEncryptionSDK/runtimes/net/ESDK.csproj @@ -31,7 +31,7 @@ - +