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 @@ - +