diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml new file mode 100644 index 0000000000..ca900aae66 --- /dev/null +++ b/.github/actions/polymorph_codegen/action.yml @@ -0,0 +1,91 @@ +# +# This local action serves two purposes: +# +# 1. For core workflows like pull.yml and push.yml, +# it is uses to check that the checked in copy of generated code +# matches what the current submodule version of smithy-dafny generates. +# This is important to ensure whenever someone changes the models +# or needs to regenerate to pick up smithy-dafny improvements, +# they don't have to deal with unpleasant surprises. +# +# 2. For workflows that check compatibility with other Dafny versions, +# such as nightly_dafny.yml, it is necessary to regenerate the code +# for that version of Dafny first. +# This is ultimately because some of the code smithy-dafny generates +# is tightly coupled to what code Dafny itself generates. +# A concrete example is that Dafny 4.3 added TypeDescriptors +# as parameters when constructing datatypes like Option and Result. +# +# This is why this is a composite action instead of a reusable workflow: +# the latter executes in a separate runner environment, +# but here we need to actually overwrite the generated code in place +# so that subsequent steps can work correctly. +# +# This action assumes that the given version of Dafny and .NET 6.0.x +# have already been set up, since they are used to format generated code. + +name: "Polymorph code generation" +description: "Regenerates code using smithy-dafny, and optionally checks that the result matches the checked in state" +inputs: + dafny: + description: "The Dafny version to run" + required: true + type: string + library: + description: "Name of the library to regenerate code for" + required: true + type: string + diff-generated-code: + description: "Diff regenerated code against committed state" + required: true + type: boolean +outputs: + random-number: + description: "Random number" + value: ${{ steps.random-number-generator.outputs.random-number }} +runs: + using: "composite" + steps: + # Replace the project.properties file so that we pick up the right runtimes etc., + # in cases where inputs.dafny is different from the current value in that file. + - name: Update top-level project.properties file + env: + DAFNY_VERSION: ${{ inputs.dafny }} + shell: bash + run: | + make generate_properties_file + + - name: Regenerate Dafny code using smithy-dafny + # Unfortunately Dafny codegen doesn't work on Windows: + # https://github.com/smithy-lang/smithy-dafny/issues/317 + if: runner.os != 'Windows' + working-directory: ./${{ inputs.library }} + shell: bash + run: | + make polymorph_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 -C .. setup_prettier + make polymorph_java + + - name: Regenerate .NET code using smithy-dafny + working-directory: ./${{ inputs.library }} + shell: bash + run: | + make polymorph_dotnet + + - name: Check regenerated code against commited code + # Composite action inputs seem to not actually support booleans properly for some reason + if: inputs.diff-generated-code == 'true' + working-directory: ./${{ inputs.library }} + shell: bash + run: | + make check_polymorph_diff diff --git a/.github/workflows/daily_ci.yml b/.github/workflows/daily_ci.yml index a2ca962339..3691ec40dd 100644 --- a/.github/workflows/daily_ci.yml +++ b/.github/workflows/daily_ci.yml @@ -16,6 +16,12 @@ jobs: uses: ./.github/workflows/library_format.yml with: dafny: ${{needs.getVersion.outputs.version}} + daily-ci-codegen: + needs: getVersion + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/library_codegen.yml + with: + dafny: ${{needs.getVersion.outputs.version}} daily-ci-verification: needs: getVersion if: github.event_name != 'schedule' || github.repository_owner == 'aws' diff --git a/.github/workflows/library_codegen.yml b/.github/workflows/library_codegen.yml new file mode 100644 index 0000000000..08c5fbd51c --- /dev/null +++ b/.github/workflows/library_codegen.yml @@ -0,0 +1,64 @@ +# This workflow regenerates code using smithy-dafny and checks that the output matches what's checked in. +name: Library Code Generation +on: + workflow_call: + inputs: + dafny: + description: "The Dafny version to run" + required: true + type: string + +jobs: + code-generation: + strategy: + fail-fast: false + matrix: + library: + [ + TestVectorsAwsCryptographicMaterialProviders, + AwsCryptographyPrimitives, + ComAmazonawsKms, + ComAmazonawsDynamodb, + AwsCryptographicMaterialProviders, + StandardLibrary, + ] + # Note dotnet is only used for formatting generated code + # in this workflow + dotnet-version: ["6.0.x"] + os: [ubuntu-latest] + runs-on: ${{ matrix.os }} + defaults: + run: + shell: bash + env: + DOTNET_CLI_TELEMETRY_OPTOUT: 1 + DOTNET_NOLOGO: 1 + steps: + - name: Support longpaths + run: | + git config --global core.longpaths true + + - uses: actions/checkout@v4 + # 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 submodules we DO need. + - run: git submodule update --init libraries + - run: git submodule update --init smithy-dafny + + # Only used to format generated code + # and to translate version strings such as "nightly-latest" + # to an actual DAFNY_VERSION. + - name: Setup Dafny + uses: dafny-lang/setup-dafny-action@v1.7.0 + with: + dafny-version: ${{ inputs.dafny }} + + - name: Setup .NET Core SDK ${{ matrix.dotnet-version }} + uses: actions/setup-dotnet@v3 + with: + dotnet-version: ${{ matrix.dotnet-version }} + + - uses: ./.github/actions/polymorph_codegen + with: + dafny: ${{ env.DAFNY_VERSION }} + library: ${{ matrix.library }} + diff-generated-code: true diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml index ca4faf8e21..16f5dd7eff 100644 --- a/.github/workflows/library_dafny_verification.yml +++ b/.github/workflows/library_dafny_verification.yml @@ -8,9 +8,16 @@ on: description: "The Dafny version to run" required: true type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" + required: false + default: false + type: boolean + jobs: verification: strategy: + fail-fast: false matrix: library: [ @@ -23,6 +30,9 @@ jobs: ] os: [macos-latest-large] runs-on: ${{ matrix.os }} + defaults: + run: + shell: bash env: DOTNET_CLI_TELEMETRY_OPTOUT: 1 DOTNET_NOLOGO: 1 @@ -33,11 +43,12 @@ jobs: - uses: actions/checkout@v4 # 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. + # 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 smithy-dafny - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.6.1 + uses: dafny-lang/setup-dafny-action@v1.7.0 with: dafny-version: ${{ inputs.dafny }} @@ -48,8 +59,15 @@ jobs: with: dotnet-version: "6.0.x" + - name: Regenerate code using smithy-dafny if necessary + if: ${{ inputs.regenerate-code }} + uses: ./.github/actions/polymorph_codegen + with: + dafny: ${{ env.DAFNY_VERSION }} + library: ${{ matrix.library }} + diff-generated-code: false + - name: Verify ${{ matrix.library }} Dafny code - shell: bash working-directory: ./${{ matrix.library }} run: | # This works because `node` is installed by default on GHA runners @@ -58,7 +76,6 @@ jobs: - name: Check solver resource use if: success() || failure() - shell: bash working-directory: ./${{ matrix.library }} run: | make dafny-reportgenerator diff --git a/.github/workflows/library_format.yml b/.github/workflows/library_format.yml index 17a82003f8..16ab8ab8ab 100644 --- a/.github/workflows/library_format.yml +++ b/.github/workflows/library_format.yml @@ -26,6 +26,9 @@ jobs: ] os: [ubuntu-latest] runs-on: ${{ matrix.os }} + defaults: + run: + shell: bash env: DOTNET_CLI_TELEMETRY_OPTOUT: 1 DOTNET_NOLOGO: 1 @@ -40,12 +43,11 @@ jobs: - run: git submodule update --init libraries - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.6.1 + uses: dafny-lang/setup-dafny-action@v1.7.0 with: dafny-version: ${{ inputs.dafny }} - name: Check format of ${{ matrix.library }} Dafny code - shell: bash working-directory: ./${{ matrix.library }} run: | # This works because `node` is installed by default on GHA runners @@ -53,7 +55,6 @@ jobs: make format_dafny-check - name: Check format of ${{ matrix.library }} Net code - shell: bash working-directory: ./${{ matrix.library }} run: | # This works because `node` is installed by default on GHA runners diff --git a/.github/workflows/library_java_tests.yml b/.github/workflows/library_java_tests.yml index 048228606e..202896e9e8 100644 --- a/.github/workflows/library_java_tests.yml +++ b/.github/workflows/library_java_tests.yml @@ -8,10 +8,16 @@ on: description: "The Dafny version to run" required: true type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" + required: false + default: false + type: boolean jobs: testJava: strategy: + fail-fast: false matrix: library: [ @@ -32,6 +38,9 @@ jobs: permissions: id-token: write contents: read + defaults: + run: + shell: bash steps: - name: Support longpaths on Git checkout run: | @@ -47,14 +56,23 @@ jobs: - uses: actions/checkout@v4 # 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. + # 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 smithy-dafny - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.6.1 + uses: dafny-lang/setup-dafny-action@v1.7.0 with: dafny-version: ${{ inputs.dafny }} + - name: Regenerate code using smithy-dafny if necessary + if: ${{ inputs.regenerate-code }} + uses: ./.github/actions/polymorph_codegen + with: + dafny: ${{ env.DAFNY_VERSION }} + library: ${{ matrix.library }} + diff-generated-code: false + - name: Setup Java 8 uses: actions/setup-java@v3 with: @@ -62,7 +80,6 @@ jobs: java-version: 8 - name: Build ${{ matrix.library }} implementation - shell: bash working-directory: ./${{ matrix.library }} run: | # This works because `node` is installed by default on GHA runners diff --git a/.github/workflows/library_net_tests.yml b/.github/workflows/library_net_tests.yml index 56ff65f20a..f51884ac5e 100644 --- a/.github/workflows/library_net_tests.yml +++ b/.github/workflows/library_net_tests.yml @@ -8,10 +8,16 @@ on: description: "The Dafny version to run" required: true type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" + required: false + default: false + type: boolean jobs: testDotNet: strategy: + fail-fast: false matrix: library: [ @@ -25,6 +31,9 @@ jobs: dotnet-version: ["6.0.x"] os: [windows-latest, ubuntu-latest, macos-latest] runs-on: ${{ matrix.os }} + defaults: + run: + shell: bash permissions: id-token: write contents: read @@ -45,8 +54,9 @@ jobs: - uses: actions/checkout@v4 # 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. + # 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 smithy-dafny - name: Setup .NET Core SDK ${{ matrix.dotnet-version }} uses: actions/setup-dotnet@v3 @@ -54,16 +64,23 @@ jobs: dotnet-version: ${{ matrix.dotnet-version }} - name: Setup Dafny - uses: dafny-lang/setup-dafny-action@v1.6.1 + uses: dafny-lang/setup-dafny-action@v1.7.0 with: dafny-version: ${{ inputs.dafny }} + - name: Regenerate code using smithy-dafny if necessary + if: ${{ inputs.regenerate-code }} + uses: ./.github/actions/polymorph_codegen + with: + dafny: ${{ env.DAFNY_VERSION }} + library: ${{ matrix.library }} + diff-generated-code: false + - name: Download Dependencies working-directory: ./${{ matrix.library }} run: make setup_net - name: Compile ${{ matrix.library }} implementation - shell: bash working-directory: ./${{ matrix.library }} run: | # This works because `node` is installed by default on GHA runners diff --git a/.github/workflows/manual.yml b/.github/workflows/manual.yml index 6f770998c9..5eb939070b 100644 --- a/.github/workflows/manual.yml +++ b/.github/workflows/manual.yml @@ -10,6 +10,11 @@ on: description: "The Dafny version to use" required: true type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" + required: false + default: true + type: boolean jobs: manual-ci-format: @@ -20,11 +25,14 @@ jobs: uses: ./.github/workflows/library_dafny_verification.yml with: dafny: ${{ inputs.dafny }} + regenerate-code: ${{ inputs.regenerate-code }} manual-ci-java: uses: ./.github/workflows/library_java_tests.yml with: dafny: ${{ inputs.dafny }} + regenerate-code: ${{ inputs.regenerate-code }} manual-ci-net: uses: ./.github/workflows/library_net_tests.yml with: dafny: ${{ inputs.dafny }} + regenerate-code: ${{ inputs.regenerate-code }} diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index 9ddcc2001f..7f6c004944 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -12,6 +12,11 @@ jobs: uses: ./.github/workflows/library_format.yml with: dafny: ${{needs.getVersion.outputs.version}} + pr-ci-codegen: + needs: getVersion + uses: ./.github/workflows/library_codegen.yml + with: + dafny: ${{needs.getVersion.outputs.version}} pr-ci-verification: needs: getVersion uses: ./.github/workflows/library_dafny_verification.yml diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 31214c00b6..4b34342253 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -14,6 +14,11 @@ jobs: uses: ./.github/workflows/library_format.yml with: dafny: ${{needs.getVersion.outputs.version}} + push-ci-codegen: + needs: getVersion + uses: ./.github/workflows/library_codegen.yml + with: + dafny: ${{needs.getVersion.outputs.version}} push-ci-verification: needs: getVersion uses: ./.github/workflows/library_dafny_verification.yml diff --git a/.gitmodules b/.gitmodules index 3498e87e0d..4f98034318 100644 --- a/.gitmodules +++ b/.gitmodules @@ -4,3 +4,6 @@ [submodule "aws-encryption-sdk-specification"] path = aws-encryption-sdk-specification url = https://github.com/awslabs/aws-encryption-sdk-specification.git +[submodule "smithy-dafny"] + path = smithy-dafny + url = https://robin-aws@github.com/smithy-lang/smithy-dafny.git diff --git a/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dafny/dafny-4.3.0.patch b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dafny/dafny-4.3.0.patch new file mode 100644 index 0000000000..70e091bc2b --- /dev/null +++ b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dafny/dafny-4.3.0.patch @@ -0,0 +1,13 @@ +diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy +index b318ab09..3684bd23 100644 +--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy ++++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy +@@ -386,7 +386,7 @@ module AwsKmsKeyring { + //# OnDecrypt MUST take [decryption materials] + //# (../structures.md#decryption-materials) and a list of [encrypted data + //# keys](../structures.md#encrypted-data-key) as input. +- method {:vcs_split_on_every_assert} OnDecrypt'( ++ method OnDecrypt'( + input: Types.OnDecryptInput + ) + returns (res: Result) diff --git a/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch new file mode 100644 index 0000000000..27a455a72d --- /dev/null +++ b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch @@ -0,0 +1,15 @@ +diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs +index b10e603c..89561181 100644 +--- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs ++++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs +@@ -3436,7 +3436,9 @@ namespace AWS.Cryptography.MaterialProviders + dafnyVal._ComAmazonawsDynamodb + ); + case software.amazon.cryptography.materialproviders.internaldafny.types.Error_ComAmazonawsKms dafnyVal: +- return Com.Amazonaws.KMS.TypeConversion.FromDafny_CommonError( ++ // BEGIN MANUAL EDIT ++ return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError( ++ // END MANUAL EDIT + dafnyVal._ComAmazonawsKms + ); + case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographicMaterialProvidersException dafnyVal: diff --git a/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.2.0.patch b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.2.0.patch new file mode 100644 index 0000000000..f9ee0bc558 --- /dev/null +++ b/AwsCryptographicMaterialProviders/codegen-patches/AwsCryptographyKeyStore/dotnet/dafny-4.2.0.patch @@ -0,0 +1,26 @@ +diff --git b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs +index f5ef0458..f846a946 100644 +--- b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs ++++ a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs +@@ -629,7 +629,9 @@ namespace AWS.Cryptography.KeyStore + dafnyVal._ComAmazonawsDynamodb + ); + case software.amazon.cryptography.keystore.internaldafny.types.Error_ComAmazonawsKms dafnyVal: +- return Com.Amazonaws.KMS.TypeConversion.FromDafny_CommonError( ++ // BEGIN MANUAL EDIT ++ return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError( ++ // END MANUAL EDIT + dafnyVal._ComAmazonawsKms + ); + case software.amazon.cryptography.keystore.internaldafny.types.Error_KeyStoreException dafnyVal: +@@ -652,7 +654,9 @@ namespace AWS.Cryptography.KeyStore + { + case "Com.Amazonaws.KMS": + return software.amazon.cryptography.keystore.internaldafny.types.Error.create_ComAmazonawsKms( +- Com.Amazonaws.KMS.TypeConversion.ToDafny_CommonError(value) ++ // BEGIN MANUAL EDIT ++ Com.Amazonaws.Kms.TypeConversion.ToDafny_CommonError(value) ++ // END MANUAL EDIT + ); + case "Com.Amazonaws.Dynamodb": + return software.amazon.cryptography.keystore.internaldafny.types.Error.create_ComAmazonawsDynamodb( diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/StormTrackingCMC.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/StormTrackingCMC.dfy index 10ee97653f..2e50252202 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/StormTrackingCMC.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/StormTrackingCMC.dfy @@ -71,6 +71,18 @@ module {:options "/functionSyntax:4" } {:extern "software.amazon.cryptography.in modifies Modifies - {History} decreases Modifies - {History} ensures ValidState() + } + + // The next two functions are for the benefit of the extern implementation to call, + // avoiding direct references to generic datatype constructors + // since their calling pattern is different between different versions of Dafny + // (i.e. after 4.2, explicit type descriptors are required). + + function CreateGetCacheEntrySuccess(output: Types.GetCacheEntryOutput): Result { + Success(output) + } + function CreateGetCacheEntryFailure(error: Types.Error): Result { + Failure(error) } } diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/internaldafny/StormTrackingCMC/StormTrackingCMC.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/internaldafny/StormTrackingCMC/StormTrackingCMC.java index c4f487147f..df5cfb803a 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/internaldafny/StormTrackingCMC/StormTrackingCMC.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/internaldafny/StormTrackingCMC/StormTrackingCMC.java @@ -1,5 +1,8 @@ package software.amazon.cryptography.internaldafny.StormTrackingCMC; +import static software.amazon.cryptography.internaldafny.StormTrackingCMC._ExternBase___default.CreateGetCacheEntryFailure; +import static software.amazon.cryptography.internaldafny.StormTrackingCMC._ExternBase___default.CreateGetCacheEntrySuccess; + import StormTracker_Compile.CacheState; import StormTracker_Compile.StormTracker; import software.amazon.cryptography.materialproviders.internaldafny.*; @@ -94,13 +97,11 @@ > GetCacheEntry_k( software.amazon.cryptography.materialproviders.internaldafny.types.Error > result = GetFromCacheInner(input); if (result.is_Failure()) { - return Wrappers_Compile.Result.create_Failure((result).dtor_error()); + return CreateGetCacheEntryFailure((result).dtor_error()); } else if (result.dtor_value().is_Full()) { - return Wrappers_Compile.Result.create_Success( - result.dtor_value().dtor_data() - ); + return CreateGetCacheEntrySuccess(result.dtor_value().dtor_data()); } else if (result.dtor_value().is_EmptyFetch()) { - return Wrappers_Compile.Result.create_Failure( + return CreateGetCacheEntryFailure( software.amazon.cryptography.materialproviders.internaldafny.types.Error.create_EntryDoesNotExist( dafny.DafnySequence.asString("Entry does not exist") ) diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviders/types/__default.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviders/types/__default.java index 50b927aef7..476fc8bb02 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviders/types/__default.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviders/types/__default.java @@ -1,4 +1,4 @@ package software.amazon.cryptography.materialproviders.internaldafny.types; public class __default - extends software.amazon.cryptography.materialproviders.internaldafny._ExternBase___default {} + extends software.amazon.cryptography.materialproviders.internaldafny.types._ExternBase___default {} diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/KeyStore.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/KeyStore.java index 8c783ef9f4..68bf0666dc 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/KeyStore.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/KeyStore.java @@ -6,7 +6,6 @@ import Wrappers_Compile.Result; import java.lang.IllegalArgumentException; import java.util.Objects; -import software.amazon.cryptography.keystore.internaldafny.KeyStoreClient; import software.amazon.cryptography.keystore.internaldafny.__default; import software.amazon.cryptography.keystore.internaldafny.types.Error; import software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient; @@ -33,9 +32,7 @@ protected KeyStore(BuilderImpl builder) { KeyStoreConfig input = builder.KeyStoreConfig(); software.amazon.cryptography.keystore.internaldafny.types.KeyStoreConfig dafnyValue = ToDafny.KeyStoreConfig(input); - //BEGIN MANUAL FIX Result result = __default.KeyStore(dafnyValue); - //END MANUAL FIX if (result.is_Failure()) { throw ToNative.Error(result.dtor_error()); } diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/MaterialProviders.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/MaterialProviders.java index 6d773ca9a6..ac695b9746 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/MaterialProviders.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/MaterialProviders.java @@ -10,7 +10,6 @@ import java.lang.IllegalArgumentException; import java.nio.ByteBuffer; import java.util.Objects; -import software.amazon.cryptography.materialproviders.internaldafny.MaterialProvidersClient; import software.amazon.cryptography.materialproviders.internaldafny.__default; import software.amazon.cryptography.materialproviders.internaldafny.types.Error; import software.amazon.cryptography.materialproviders.internaldafny.types.IAwsCryptographicMaterialProvidersClient; @@ -50,10 +49,8 @@ protected MaterialProviders(BuilderImpl builder) { MaterialProvidersConfig input = builder.MaterialProvidersConfig(); software.amazon.cryptography.materialproviders.internaldafny.types.MaterialProvidersConfig dafnyValue = ToDafny.MaterialProvidersConfig(input); - //BEGIN MANUAL FIX Result result = __default.MaterialProviders(dafnyValue); - //END MANUAL FIX if (result.is_Failure()) { throw ToNative.Error(result.dtor_error()); } diff --git a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs index dd16664526..895611816e 100644 --- a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs +++ b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs @@ -2438,7 +2438,12 @@ public static System.IO.MemoryStream FromDafny_N6_smithy__N3_api__S4_Blob(Dafny. } public static Dafny.ISequence ToDafny_N6_smithy__N3_api__S4_Blob(System.IO.MemoryStream value) { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } return Dafny.Sequence.FromArray(value.ToArray()); + } public static int FromDafny_N6_smithy__N3_api__S7_Integer(int value) { @@ -2637,7 +2642,12 @@ public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N17_mat } public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S6_Secret(System.IO.MemoryStream value) { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } return Dafny.Sequence.FromArray(value.ToArray()); + } public static Amazon.KeyManagementService.EncryptionAlgorithmSpec FromDafny_N3_com__N9_amazonaws__N3_kms__S23_EncryptionAlgorithmSpec(software.amazon.cryptography.services.kms.internaldafny.types._IEncryptionAlgorithmSpec value) { @@ -3308,7 +3318,12 @@ public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N8_keyS } public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N8_keyStore__S6_Secret(System.IO.MemoryStream value) { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } return Dafny.Sequence.FromArray(value.ToArray()); + } public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N8_keyStore__S10_HmacKeyMap(Dafny.IMap, Dafny.ISequence> value) { @@ -3408,23 +3423,23 @@ public static System.Exception FromDafny_CommonError(software.amazon.cryptograph { switch (value) { + case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographyKeyStore dafnyVal: + return AWS.Cryptography.KeyStore.TypeConversion.FromDafny_CommonError( + dafnyVal._AwsCryptographyKeyStore + ); case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographyPrimitives dafnyVal: return AWS.Cryptography.Primitives.TypeConversion.FromDafny_CommonError( dafnyVal._AwsCryptographyPrimitives ); - case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographyKeyStore dafnyVal: - return AWS.Cryptography.KeyStore.TypeConversion.FromDafny_CommonError( - dafnyVal._AwsCryptographyKeyStore + case software.amazon.cryptography.materialproviders.internaldafny.types.Error_ComAmazonawsDynamodb dafnyVal: + return Com.Amazonaws.Dynamodb.TypeConversion.FromDafny_CommonError( + dafnyVal._ComAmazonawsDynamodb ); case software.amazon.cryptography.materialproviders.internaldafny.types.Error_ComAmazonawsKms dafnyVal: // BEGIN MANUAL EDIT return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError( - // END MANUAL EDIT - dafnyVal._ComAmazonawsKms - ); - case software.amazon.cryptography.materialproviders.internaldafny.types.Error_ComAmazonawsDynamodb dafnyVal: - return Com.Amazonaws.Dynamodb.TypeConversion.FromDafny_CommonError( - dafnyVal._ComAmazonawsDynamodb + // END MANUAL EDIT + dafnyVal._ComAmazonawsKms ); case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographicMaterialProvidersException dafnyVal: return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S42_AwsCryptographicMaterialProvidersException(dafnyVal); diff --git a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs index cb856dd55d..f846a946b0 100644 --- a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs +++ b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs @@ -587,7 +587,12 @@ public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N8_keyS } public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N8_keyStore__S6_Secret(System.IO.MemoryStream value) { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } return Dafny.Sequence.FromArray(value.ToArray()); + } public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N8_keyStore__S10_HmacKeyMap(Dafny.IMap, Dafny.ISequence> value) { @@ -619,16 +624,16 @@ public static System.Exception FromDafny_CommonError(software.amazon.cryptograph { switch (value) { + case software.amazon.cryptography.keystore.internaldafny.types.Error_ComAmazonawsDynamodb dafnyVal: + return Com.Amazonaws.Dynamodb.TypeConversion.FromDafny_CommonError( + dafnyVal._ComAmazonawsDynamodb + ); case software.amazon.cryptography.keystore.internaldafny.types.Error_ComAmazonawsKms dafnyVal: // BEGIN MANUAL EDIT return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError( // END MANUAL EDIT dafnyVal._ComAmazonawsKms ); - case software.amazon.cryptography.keystore.internaldafny.types.Error_ComAmazonawsDynamodb dafnyVal: - return Com.Amazonaws.Dynamodb.TypeConversion.FromDafny_CommonError( - dafnyVal._ComAmazonawsDynamodb - ); case software.amazon.cryptography.keystore.internaldafny.types.Error_KeyStoreException dafnyVal: return FromDafny_N3_aws__N12_cryptography__N8_keyStore__S17_KeyStoreException(dafnyVal); case software.amazon.cryptography.keystore.internaldafny.types.Error_CollectionOfErrors dafnyVal: @@ -647,12 +652,12 @@ public static software.amazon.cryptography.keystore.internaldafny.types._IError { switch (value.GetType().Namespace) { - // BEGIN MANUAL EDIT case "Com.Amazonaws.KMS": return software.amazon.cryptography.keystore.internaldafny.types.Error.create_ComAmazonawsKms( + // BEGIN MANUAL EDIT Com.Amazonaws.Kms.TypeConversion.ToDafny_CommonError(value) + // END MANUAL EDIT ); - // END MANUAL EDIT case "Com.Amazonaws.Dynamodb": return software.amazon.cryptography.keystore.internaldafny.types.Error.create_ComAmazonawsDynamodb( Com.Amazonaws.Dynamodb.TypeConversion.ToDafny_CommonError(value) diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/AESEncryption/AES_GCM.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/AESEncryption/AES_GCM.java index 04e675f3d9..8aa098e60e 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/java/AESEncryption/AES_GCM.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/java/AESEncryption/AES_GCM.java @@ -16,7 +16,7 @@ import software.amazon.cryptography.primitives.internaldafny.types.Error; import software.amazon.cryptography.primitives.model.OpaqueError; -public class AES_GCM { +public class AES_GCM extends _ExternBase___default { public static Result AESEncryptExtern( AES__GCM encAlg, @@ -52,9 +52,9 @@ public static Result AESEncryptExtern( DafnySequence.fromBytes(cipherOutput), encAlg ); - return Result.create_Success(aesEncryptOutput); + return CreateAESEncryptExternSuccess(aesEncryptOutput); } catch (GeneralSecurityException e) { - return Result.create_Failure( + return CreateAESEncryptExternFailure( ToDafny.Error(OpaqueError.builder().obj(e).build()) ); } @@ -109,9 +109,11 @@ public static Result, Error> AESDecryptExtern( cipher_.updateAAD(aadBytes); } byte[] cipherOutput = cipher_.doFinal(ciphertextAndTag); - return Result.create_Success(DafnySequence.fromBytes(cipherOutput)); + return CreateAESDecryptExternSuccess( + DafnySequence.fromBytes(cipherOutput) + ); } catch (GeneralSecurityException e) { - return Result.create_Failure( + return CreateAESDecryptExternFailure( ToDafny.Error(OpaqueError.builder().obj(e).build()) ); } diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/AesKdfCtr/__default.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/AesKdfCtr/__default.java index 557e60bf86..af310b2c8c 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/java/AesKdfCtr/__default.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/java/AesKdfCtr/__default.java @@ -11,7 +11,7 @@ import software.amazon.cryptography.primitives.ToDafny; import software.amazon.cryptography.primitives.model.OpaqueError; -public class __default { +public class __default extends _ExternBase___default { public static Wrappers_Compile.Result< dafny.DafnySequence, @@ -30,9 +30,9 @@ > AesKdfCtrStream( IvParameterSpec ivSpec = new IvParameterSpec(nonceBytes); cipher.init(Cipher.ENCRYPT_MODE, secretKey, ivSpec); byte[] ciphertext = cipher.doFinal(plaintext); - return Result.create_Success(DafnySequence.fromBytes(ciphertext)); + return CreateStreamSuccess(DafnySequence.fromBytes(ciphertext)); } catch (GeneralSecurityException e) { - return Result.create_Failure( + return CreateStreamFailure( ToDafny.Error(OpaqueError.builder().obj(e).build()) ); } diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/Dafny/Aws/Cryptography/Primitives/Types/InternalResult.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Dafny/Aws/Cryptography/Primitives/Types/InternalResult.java new file mode 100644 index 0000000000..273822ef43 --- /dev/null +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Dafny/Aws/Cryptography/Primitives/Types/InternalResult.java @@ -0,0 +1,59 @@ +package Dafny.Aws.Cryptography.Primitives.Types; + +/** + * Similar to the translation of Dafny's Wrappers.Result type, + * but without the complexity of dealing with TypeDescriptors. + * The former is necessary when extern methods need to return + * results to Dafny code, but InteralResult is easier to work with + * when just passing results between internal helper methods. + * + * This class was created mainly to ease refactorings. + * New code should strongly consider using Java exceptions + * idiomatically instead. + */ +public class InternalResult { + + private final boolean isSuccess; + private final T value; + private final E error; + + private InternalResult(boolean isSuccess, T value, E error) { + this.isSuccess = isSuccess; + this.value = value; + this.error = error; + } + + public static InternalResult success(T t) { + return new InternalResult(true, t, null); + } + + public static InternalResult failure(E e) { + return new InternalResult(false, null, e); + } + + public boolean isSuccess() { + return isSuccess; + } + + public boolean isFailure() { + return !isSuccess; + } + + public T value() { + if (!isSuccess) { + throw new IllegalStateException( + "Tried to extract a value from a failure: " + this + ); + } + return value; + } + + public E error() { + if (isSuccess) { + throw new IllegalStateException( + "Tried to extract an error from a success: " + this + ); + } + return error; + } +} diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/Digest_Compile/ExternDigest.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Digest_Compile/ExternDigest.java index 46ad9b02c7..d3d1b36a63 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/java/Digest_Compile/ExternDigest.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Digest_Compile/ExternDigest.java @@ -1,5 +1,7 @@ package Digest_Compile; +import Dafny.Aws.Cryptography.Primitives.Types.InternalResult; +import ExternDigest._ExternBase___default; import Wrappers_Compile.Result; import dafny.Array; import dafny.DafnySequence; @@ -12,25 +14,23 @@ public class ExternDigest { - public static class __default { + public static class __default extends _ExternBase___default { public static Result, Error> Digest( DigestAlgorithm digestAlgorithm, DafnySequence dtor_message ) { - final Result maybeDigest = internalDigest( + final InternalResult maybeDigest = internalDigest( digestAlgorithm, dtor_message ); - if (maybeDigest.is_Failure()) { - return Result.create_Failure(maybeDigest.dtor_error()); + if (maybeDigest.isFailure()) { + return CreateDigestFailure(maybeDigest.error()); } - return Result.create_Success( - DafnySequence.fromBytes(maybeDigest.dtor_value()) - ); + return CreateDigestSuccess(DafnySequence.fromBytes(maybeDigest.value())); } - public static Result internalDigest( + public static InternalResult internalDigest( DigestAlgorithm digestAlgorithm, DafnySequence dtor_message ) { @@ -41,7 +41,7 @@ public static Result internalDigest( ); hash.update(messageBytes); final byte[] digest = hash.digest(); - return Result.create_Success(digest); + return InternalResult.success(digest); } catch (NoSuchAlgorithmException ex) { final Error err = ToDafny.Error( AwsCryptographicPrimitivesError @@ -50,7 +50,7 @@ public static Result internalDigest( .cause(ex) .build() ); - return Result.create_Failure(err); + return InternalResult.failure(err); } } diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/HMAC/HMac.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/HMAC/HMac.java index b8224183e1..41325fb1a9 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/java/HMAC/HMac.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/java/HMAC/HMac.java @@ -20,7 +20,7 @@ public class HMac extends _ExternBase_HMac { public static Result Build(DigestAlgorithm digest) { try { final HMac output = new HMac(digest); - return Result.create_Success(output); + return CreateHMacSuccess(output); } catch (NoSuchAlgorithmException ex) { final Error err = ToDafny.Error( AwsCryptographicPrimitivesError @@ -29,7 +29,7 @@ public static Result Build(DigestAlgorithm digest) { .cause(ex) .build() ); - return Result.create_Failure(err); + return CreateHMacFailure(err); } } diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/HMAC/__default.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/HMAC/__default.java index 8fec89b5bf..909c75436e 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/java/HMAC/__default.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/java/HMAC/__default.java @@ -4,22 +4,22 @@ import dafny.DafnySequence; import software.amazon.cryptography.primitives.internaldafny.types.Error; -public class __default { +public class __default extends _ExternBase___default { public static Result, Error> Digest( software.amazon.cryptography.primitives.internaldafny.types.HMacInput input ) { Result maybeHMac = HMac.Build(input._digestAlgorithm); if (maybeHMac.is_Failure()) { - return Result.create_Failure(maybeHMac.dtor_error()); + return CreateDigestFailure(maybeHMac.dtor_error()); } final HMac hmac = maybeHMac.Extract( - HMac._typeDescriptor(), + dafny.TypeDescriptor.referenceWithInitializer(HMac.class, () -> null), Error._typeDescriptor() ); hmac.Init(input._key); hmac.BlockUpdate(input._message); final DafnySequence output = hmac.GetResult(); - return Result.create_Success(output); + return CreateDigestSuccess(output); } } diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/RSAEncryption/RSA.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/RSAEncryption/RSA.java index f4dbe900b5..bc81b3a57c 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/java/RSAEncryption/RSA.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/java/RSAEncryption/RSA.java @@ -43,7 +43,7 @@ import software.amazon.cryptography.primitives.internaldafny.types.RSAPaddingMode; import software.amazon.cryptography.primitives.model.OpaqueError; -public class RSA { +public class RSA extends _ExternBase___default { private static int RSA_KEY_LEN_MAX = 4096; private static int RSA_PUBLIC_EXPONENT = 65537; @@ -88,9 +88,11 @@ public static Result GetRSAKeyModulusLengthExtern( try { byte[] pemBytes = (byte[]) Array.unwrap(dtor_publicKey.toArray()); RSAKeyParameters keyParams = ParsePublicRsaPemBytes(pemBytes); - return Result.create_Success(keyParams.getModulus().bitLength()); + return CreateGetRSAKeyModulusLengthExternSuccess( + keyParams.getModulus().bitLength() + ); } catch (Exception e) { - return Result.create_Failure( + return CreateGetRSAKeyModulusLengthExternFailure( ToDafny.Error( OpaqueError.builder().obj(e).message(e.getMessage()).cause(e).build() ) @@ -199,13 +201,13 @@ public static Result, Error> DecryptExtern( AsymmetricBlockCipher engine = GetEngineForPadding(dtor_padding); engine.init(false, keyParameter); - return Result.create_Success( + return CreateBytesSuccess( DafnySequence.fromBytes( engine.processBlock(ciphertext, 0, ciphertext.length) ) ); } catch (Exception e) { - return Result.create_Failure( + return CreateBytesFailure( ToDafny.Error( OpaqueError.builder().obj(e).message(e.getMessage()).cause(e).build() ) @@ -225,7 +227,7 @@ public static Result, Error> EncryptExtern( AsymmetricBlockCipher engine = GetEngineForPadding(dtor_padding); engine.init(true, publicKeyParam); - return Result.create_Success( + return CreateBytesSuccess( DafnySequence.fromBytes( engine.processBlock( (byte[]) Array.unwrap(dtor_plaintext.toArray()), @@ -235,7 +237,7 @@ public static Result, Error> EncryptExtern( ) ); } catch (Exception e) { - return Result.create_Failure( + return CreateBytesFailure( ToDafny.Error( OpaqueError.builder().obj(e).message(e.getMessage()).cause(e).build() ) diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/Random_Compile/ExternRandom.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Random_Compile/ExternRandom.java index e46968c603..8accefa293 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/java/Random_Compile/ExternRandom.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Random_Compile/ExternRandom.java @@ -3,6 +3,7 @@ package Random_Compile; +import ExternRandom._ExternBase___default; import Wrappers_Compile.Result; import dafny.DafnySequence; import java.security.SecureRandom; @@ -12,7 +13,7 @@ public class ExternRandom { - public static class __default { + public static class __default extends _ExternBase___default { public static Result, Error> GenerateBytes( final int len @@ -23,9 +24,9 @@ public static Result, Error> GenerateBytes( final byte[] result = new byte[len]; final SecureRandom secureRandom = getSecureRandom(); secureRandom.nextBytes(result); - return Result.create_Success(DafnySequence.fromBytes(result)); + return CreateGenerateBytesSuccess(DafnySequence.fromBytes(result)); } catch (Exception e) { - return Result.create_Failure( + return CreateGenerateBytesFailure( ToDafny.Error( OpaqueError .builder() diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/ECDSA.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/ECDSA.java index 5b3813b903..5eac619938 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/ECDSA.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/ECDSA.java @@ -2,6 +2,7 @@ import static Signature.SignatureAlgorithm.signatureAlgorithm; +import Dafny.Aws.Cryptography.Primitives.Types.InternalResult; import Digest_Compile.ExternDigest; import Random_Compile.ExternRandom; import Wrappers_Compile.Result; @@ -25,7 +26,7 @@ import software.amazon.cryptography.primitives.model.AwsCryptographicPrimitivesError; import software.amazon.cryptography.primitives.model.OpaqueError; -public class ECDSA { +public class ECDSA extends _ExternBase___default { static final String ELLIPTIC_CURVE_ALGORITHM = "EC"; /* Standards for Efficient Cryptography over a prime field */ @@ -40,13 +41,13 @@ public class ECDSA { public static Result ExternKeyGen( ECDSASignatureAlgorithm dtor_signatureAlgorithm ) { - final Result maybeSignatureAlgorithm = + final InternalResult maybeSignatureAlgorithm = signatureAlgorithm(dtor_signatureAlgorithm); - if (maybeSignatureAlgorithm.is_Failure()) { - return Result.create_Failure(maybeSignatureAlgorithm.dtor_error()); + if (maybeSignatureAlgorithm.isFailure()) { + return CreateExternKeyGenFailure(maybeSignatureAlgorithm.error()); } final ECGenParameterSpec genParameterSpec = new ECGenParameterSpec( - maybeSignatureAlgorithm.dtor_value().curve + maybeSignatureAlgorithm.value().curve ); final SecureRandom secureRandom = ExternRandom.getSecureRandom(); final KeyPairGenerator keyGen; @@ -54,7 +55,7 @@ public static Result ExternKeyGen( keyGen = KeyPairGenerator.getInstance(ELLIPTIC_CURVE_ALGORITHM); keyGen.initialize(genParameterSpec, secureRandom); } catch (GeneralSecurityException e) { - return Result.create_Failure( + return CreateExternKeyGenFailure( ToDafny.Error( OpaqueError.builder().obj(e).message(e.getMessage()).cause(e).build() ) @@ -75,7 +76,7 @@ public static Result ExternKeyGen( (ECPrivateKey) keyPair.getPrivate() ); - return Result.create_Success( + return CreateExternKeyGenSuccess( SignatureKeyPair.create( DafnySequence.fromBytes(verificationKey), DafnySequence.fromBytes(signingKey) @@ -88,18 +89,18 @@ public static Result, Error> Sign( DafnySequence dtor_signingKey, DafnySequence dtor_message ) { - final Result maybeSignatureAlgorithm = + final InternalResult maybeSignatureAlgorithm = signatureAlgorithm(dtor_signatureAlgorithm); - if (maybeSignatureAlgorithm.is_Failure()) { - return Result.create_Failure(maybeSignatureAlgorithm.dtor_error()); + if (maybeSignatureAlgorithm.isFailure()) { + return CreateSignFailure(maybeSignatureAlgorithm.error()); } - SignatureAlgorithm algorithm = maybeSignatureAlgorithm.dtor_value(); + SignatureAlgorithm algorithm = maybeSignatureAlgorithm.value(); final Signature signatureCipher; try { signatureCipher = Signature.getInstance(algorithm.rawSignatureAlgorithm); } catch (NoSuchAlgorithmException ex) { - return Result.create_Failure( + return CreateSignFailure( ToDafny.Error( AwsCryptographicPrimitivesError .builder() @@ -115,27 +116,27 @@ public static Result, Error> Sign( ); } - Result maybePrivateKey = + InternalResult maybePrivateKey = PrivateKeyUtils.decodePrivateKey(algorithm, dtor_signingKey); - if (maybePrivateKey.is_Failure()) { - return Result.create_Failure(maybePrivateKey.dtor_error()); + if (maybePrivateKey.isFailure()) { + return CreateSignFailure(maybePrivateKey.error()); } - final ECPrivateKey privateKey = maybePrivateKey.dtor_value(); + final ECPrivateKey privateKey = maybePrivateKey.value(); - final Result maybeDigest = + final InternalResult maybeDigest = ExternDigest.__default.internalDigest( algorithm.messageDigestAlgorithm, dtor_message ); - if (maybeDigest.is_Failure()) { - return Result.create_Failure(maybeDigest.dtor_error()); + if (maybeDigest.isFailure()) { + return CreateSignFailure(maybeDigest.error()); } - final byte[] digest = maybeDigest.dtor_value(); + final byte[] digest = maybeDigest.value(); try { signatureCipher.initSign(privateKey, ExternRandom.getSecureRandom()); } catch (InvalidKeyException ex) { - return Result.create_Failure( + return CreateSignFailure( ToDafny.Error( AwsCryptographicPrimitivesError .builder() @@ -164,13 +165,13 @@ public static Result, Error> Sign( algorithm.expectedSignatureLength ); } catch (SignatureException e) { - return Result.create_Failure( + return CreateSignFailure( ToDafny.Error( OpaqueError.builder().obj(e).message(e.getMessage()).cause(e).build() ) ); } - return Result.create_Success(DafnySequence.fromBytes(signatureBytes)); + return CreateSignSuccess(DafnySequence.fromBytes(signatureBytes)); } public static Result Verify( @@ -179,27 +180,25 @@ public static Result Verify( DafnySequence dtor_message, DafnySequence dtor_signature ) { - final Result maybeSignatureAlgorithm = + final InternalResult maybeSignatureAlgorithm = signatureAlgorithm(dtor_signatureAlgorithm); - if (maybeSignatureAlgorithm.is_Failure()) { - return Result.create_Failure(maybeSignatureAlgorithm.dtor_error()); + if (maybeSignatureAlgorithm.isFailure()) { + return CreateVerifyFailure(maybeSignatureAlgorithm.error()); } - final SignatureAlgorithm algorithm = maybeSignatureAlgorithm.dtor_value(); + final SignatureAlgorithm algorithm = maybeSignatureAlgorithm.value(); - Result maybePublicKey = PublicKeyUtils.decodePublicKey( - algorithm, - dtor_verificationKey - ); - if (maybePublicKey.is_Failure()) { - return Result.create_Failure(maybePublicKey.dtor_error()); + InternalResult maybePublicKey = + PublicKeyUtils.decodePublicKey(algorithm, dtor_verificationKey); + if (maybePublicKey.isFailure()) { + return CreateVerifyFailure(maybePublicKey.error()); } - final ECPublicKey publicKey = maybePublicKey.dtor_value(); + final ECPublicKey publicKey = maybePublicKey.value(); final Signature signatureCipher; try { signatureCipher = Signature.getInstance(algorithm.rawSignatureAlgorithm); } catch (NoSuchAlgorithmException ex) { - return Result.create_Failure( + return CreateVerifyFailure( ToDafny.Error( AwsCryptographicPrimitivesError .builder() @@ -218,7 +217,7 @@ public static Result Verify( try { signatureCipher.initVerify(publicKey); } catch (InvalidKeyException ex) { - return Result.create_Failure( + return CreateVerifyFailure( ToDafny.Error( AwsCryptographicPrimitivesError .builder() @@ -237,15 +236,15 @@ public static Result Verify( ); } - final Result maybeDigest = + final InternalResult maybeDigest = ExternDigest.__default.internalDigest( algorithm.messageDigestAlgorithm, dtor_message ); - if (maybeDigest.is_Failure()) { - return Result.create_Failure(maybeDigest.dtor_error()); + if (maybeDigest.isFailure()) { + return CreateVerifyFailure(maybeDigest.error()); } - final byte[] digest = maybeDigest.dtor_value(); + final byte[] digest = maybeDigest.value(); try { signatureCipher.update(digest); @@ -274,7 +273,7 @@ public static Result Verify( ); success = signatureCipher.verify(signatureAsBytes); } catch (SignatureException ex) { - return Result.create_Failure( + return CreateVerifyFailure( ToDafny.Error( AwsCryptographicPrimitivesError .builder() @@ -293,6 +292,6 @@ public static Result Verify( ); } - return Result.create_Success(success); + return CreateVerifySuccess(success); } } diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/PrivateKeyUtils.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/PrivateKeyUtils.java index d266d9ad15..9d62ddffa6 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/PrivateKeyUtils.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/PrivateKeyUtils.java @@ -1,5 +1,6 @@ package Signature; +import Dafny.Aws.Cryptography.Primitives.Types.InternalResult; import Wrappers_Compile.Result; import dafny.Array; import dafny.DafnySequence; @@ -33,7 +34,7 @@ static byte[] encodePrivateKey(final ECPrivateKey privateKey) { return privateKey.getS().toByteArray(); } - static Result decodePrivateKey( + static InternalResult decodePrivateKey( SignatureAlgorithm algorithm, DafnySequence dtor_signingKey ) { @@ -64,12 +65,12 @@ static Result decodePrivateKey( ) { // The private key will always be generated in this runtime (Java); // these exceptions SHOULD BE impossible. - return Result.create_Failure( + return InternalResult.failure( ToDafny.Error( OpaqueError.builder().obj(e).message(e.getMessage()).cause(e).build() ) ); } - return Result.create_Success(privateKey); + return InternalResult.success(privateKey); } } diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/PublicKeyUtils.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/PublicKeyUtils.java index 4085ecb070..be6054a077 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/PublicKeyUtils.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/PublicKeyUtils.java @@ -6,6 +6,7 @@ import static java.math.BigInteger.ONE; import static java.math.BigInteger.ZERO; +import Dafny.Aws.Cryptography.Primitives.Types.InternalResult; import Wrappers_Compile.Result; import dafny.Array; import dafny.DafnySequence; @@ -107,7 +108,7 @@ static byte[] encodeAndCompressPublicKeyX( return paddedResult; } - static Result decodePublicKey( + static InternalResult decodePublicKey( SignatureAlgorithm algorithm, DafnySequence dtor_verificationKey ) { @@ -132,7 +133,7 @@ static Result decodePublicKey( .getInstance(ECDSA.ELLIPTIC_CURVE_ALGORITHM) .generatePublic(publicKeySpec); } catch (ECDecodingException ex) { - return Result.create_Failure( + return InternalResult.failure( ToDafny.Error( AwsCryptographicPrimitivesError .builder() @@ -151,13 +152,13 @@ static Result decodePublicKey( | InvalidKeySpecException | InvalidParameterSpecException e ) { - return Result.create_Failure( + return InternalResult.failure( ToDafny.Error( OpaqueError.builder().obj(e).message(e.getMessage()).cause(e).build() ) ); } - return Result.create_Success(publicKey); + return InternalResult.success(publicKey); } /** diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/SignatureAlgorithm.java b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/SignatureAlgorithm.java index 763c9796b1..ec5c64057a 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/SignatureAlgorithm.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/java/Signature/SignatureAlgorithm.java @@ -4,6 +4,7 @@ import static Signature.ECDSA.SEC_P384; import static Signature.ECDSA.SEC_PRIME_FIELD_PREFIX; +import Dafny.Aws.Cryptography.Primitives.Types.InternalResult; import Wrappers_Compile.Result; import java.security.AlgorithmParameters; import java.security.NoSuchAlgorithmException; @@ -47,7 +48,7 @@ public enum SignatureAlgorithm { this.expectedSignatureLength = expectedSignatureLength; } - static Result signatureAlgorithm( + static InternalResult signatureAlgorithm( ECDSASignatureAlgorithm dtor_signatureAlgorithm ) { final SignatureAlgorithm signatureAlgorithm; @@ -63,7 +64,7 @@ static Result signatureAlgorithm( } else if (dtor_signatureAlgorithm.is_ECDSA__P384()) { signatureAlgorithm = P384; } else { - return Result.create_Failure( + return InternalResult.failure( ToDafny.Error( AwsCryptographicPrimitivesError .builder() @@ -77,7 +78,7 @@ static Result signatureAlgorithm( ) ); } - return Result.create_Success(signatureAlgorithm); + return InternalResult.success(signatureAlgorithm); } static ECParameterSpec ecParameterSpec(SignatureAlgorithm algorithm) diff --git a/AwsCryptographyPrimitives/runtimes/net/Generated/TypeConversion.cs b/AwsCryptographyPrimitives/runtimes/net/Generated/TypeConversion.cs index 867434bc3d..5017facca7 100644 --- a/AwsCryptographyPrimitives/runtimes/net/Generated/TypeConversion.cs +++ b/AwsCryptographyPrimitives/runtimes/net/Generated/TypeConversion.cs @@ -1024,7 +1024,12 @@ public static System.IO.MemoryStream FromDafny_N6_smithy__N3_api__S4_Blob(Dafny. } public static Dafny.ISequence ToDafny_N6_smithy__N3_api__S4_Blob(System.IO.MemoryStream value) { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } return Dafny.Sequence.FromArray(value.ToArray()); + } public static int FromDafny_N3_aws__N12_cryptography__N10_primitives__S15_PositiveInteger(int value) { diff --git a/AwsCryptographyPrimitives/src/AESEncryption.dfy b/AwsCryptographyPrimitives/src/AESEncryption.dfy index 2099a4dc42..aa590b93d7 100644 --- a/AwsCryptographyPrimitives/src/AESEncryption.dfy +++ b/AwsCryptographyPrimitives/src/AESEncryption.dfy @@ -122,4 +122,24 @@ module {:extern "AESEncryption"} AESEncryption { return Success(value); } + // The next four functions are for the benefit of the extern implementation to call, + // avoiding direct references to generic datatype constructors + // since their calling pattern is different between different versions of Dafny + // (i.e. after 4.2, explicit type descriptors are required). + + function method CreateAESEncryptExternSuccess(output: Types.AESEncryptOutput): Result { + Success(output) + } + + function method CreateAESEncryptExternFailure(error: Types.OpaqueError): Result { + Failure(error) + } + + function method CreateAESDecryptExternSuccess(bytes: seq): Result, Types.OpaqueError> { + Success(bytes) + } + + function method CreateAESDecryptExternFailure(error: Types.OpaqueError): Result, Types.OpaqueError> { + Failure(error) + } } diff --git a/AwsCryptographyPrimitives/src/AesKdfCtr.dfy b/AwsCryptographyPrimitives/src/AesKdfCtr.dfy index 571a3655d1..c85f6e8867 100644 --- a/AwsCryptographyPrimitives/src/AesKdfCtr.dfy +++ b/AwsCryptographyPrimitives/src/AesKdfCtr.dfy @@ -59,4 +59,17 @@ module {:extern "AesKdfCtr"} AesKdfCtr { requires |nonce| == 16 requires |key| == 32 ensures res.Success? ==> |res.value| == length as nat + + // The next two functions are for the benefit of the extern implementation to call, + // avoiding direct references to generic datatype constructors + // since their calling pattern is different between different versions of Dafny + // (i.e. after 4.2, explicit type descriptors are required). + + function method CreateStreamSuccess(bytes: seq): Result, Types.Error> { + Success(bytes) + } + + function method CreateStreamFailure(error: Types.Error): Result, Types.Error> { + Failure(error) + } } diff --git a/AwsCryptographyPrimitives/src/AwsCryptographyPrimitivesOperations.dfy b/AwsCryptographyPrimitives/src/AwsCryptographyPrimitivesOperations.dfy index 8397692863..bf1e6c9992 100644 --- a/AwsCryptographyPrimitives/src/AwsCryptographyPrimitivesOperations.dfy +++ b/AwsCryptographyPrimitives/src/AwsCryptographyPrimitivesOperations.dfy @@ -10,6 +10,7 @@ include "AESEncryption.dfy" include "Digest.dfy" include "RSAEncryption.dfy" include "Signature.dfy" +include "AesKdfCtr.dfy" module AwsCryptographyPrimitivesOperations refines AbstractAwsCryptographyPrimitivesOperations { import Random diff --git a/AwsCryptographyPrimitives/src/Digest.dfy b/AwsCryptographyPrimitives/src/Digest.dfy index 2f448b987d..e97509c7a8 100644 --- a/AwsCryptographyPrimitives/src/Digest.dfy +++ b/AwsCryptographyPrimitives/src/Digest.dfy @@ -40,4 +40,17 @@ module {:extern "ExternDigest" } ExternDigest { method {:extern } Digest(alg: Types.DigestAlgorithm, msg: seq) returns (res: Result, Types.Error>) + + // The next two functions are for the benefit of the extern implementation to call, + // avoiding direct references to generic datatype constructors + // since their calling pattern is different between different versions of Dafny + // (i.e. after 4.2, explicit type descriptors are required). + + function method CreateDigestSuccess(bytes: seq): Result, Types.Error> { + Success(bytes) + } + + function method CreateDigestFailure(error: Types.Error): Result, Types.Error> { + Failure(error) + } } diff --git a/AwsCryptographyPrimitives/src/HKDF/HMAC.dfy b/AwsCryptographyPrimitives/src/HKDF/HMAC.dfy index 7218dafed5..4d8f4b5e68 100644 --- a/AwsCryptographyPrimitives/src/HKDF/HMAC.dfy +++ b/AwsCryptographyPrimitives/src/HKDF/HMAC.dfy @@ -56,8 +56,20 @@ module {:options "-functionSyntax:4"} {:extern "HMAC"} HMAC { ensures this.GetKey() == old(this.GetKey()) ensures this.HashSignature(old(this.GetInputSoFar()), s) - predicate {:axiom} HashSignature(message: seq, s: seq) + ghost predicate {:axiom} HashSignature(message: seq, s: seq) + // The next two functions are for the benefit of the extern implementation to call, + // avoiding direct references to generic datatype constructors + // since their calling pattern is different between different versions of Dafny + // (i.e. after 4.2, explicit type descriptors are required). + + static function CreateHMacSuccess(hmac: HMac): Result { + Success(hmac) + } + + static function CreateHMacFailure(error: Types.Error): Result { + Failure(error) + } } // HMAC Digest is safe to make a Dafny function @@ -66,4 +78,16 @@ module {:options "-functionSyntax:4"} {:extern "HMAC"} HMAC { : ( output: Result, Types.Error> ) ensures output.Success? ==> |output.value| == HashDigest.Length(input.digestAlgorithm) + // The next two functions are for the benefit of the extern implementation to call, + // avoiding direct references to generic datatype constructors + // since their calling pattern is different between different versions of Dafny + // (i.e. after 4.2, explicit type descriptors are required). + + function CreateDigestSuccess(bytes: seq): Result, Types.Error> { + Success(bytes) + } + + function CreateDigestFailure(error: Types.Error): Result, Types.Error> { + Failure(error) + } } diff --git a/AwsCryptographyPrimitives/src/RSAEncryption.dfy b/AwsCryptographyPrimitives/src/RSAEncryption.dfy index 08f7d245dd..c5b7f36060 100644 --- a/AwsCryptographyPrimitives/src/RSAEncryption.dfy +++ b/AwsCryptographyPrimitives/src/RSAEncryption.dfy @@ -58,4 +58,25 @@ module {:extern "RSAEncryption"} RSAEncryption { returns (res: Result, Types.Error>) requires |publicKey| > 0 requires |plaintextData| > 0 + + // The next four functions are for the benefit of the extern implementation to call, + // avoiding direct references to generic datatype constructors + // since their calling pattern is different between different versions of Dafny + // (i.e. after 4.2, explicit type descriptors are required). + + function method CreateGetRSAKeyModulusLengthExternSuccess(output: uint32): Result { + Success(output) + } + + function method CreateGetRSAKeyModulusLengthExternFailure(error: Types.Error): Result { + Failure(error) + } + + function method CreateBytesSuccess(bytes: seq): Result, Types.Error> { + Success(bytes) + } + + function method CreateBytesFailure(error: Types.Error): Result, Types.Error> { + Failure(error) + } } diff --git a/AwsCryptographyPrimitives/src/Random.dfy b/AwsCryptographyPrimitives/src/Random.dfy index d10254ebeb..5191805995 100644 --- a/AwsCryptographyPrimitives/src/Random.dfy +++ b/AwsCryptographyPrimitives/src/Random.dfy @@ -30,4 +30,17 @@ module {:extern "ExternRandom"} ExternRandom { import Types = AwsCryptographyPrimitivesTypes method {:extern} GenerateBytes(i: int32) returns (res: Result, Types.OpaqueError>) + + // The next two functions are for the benefit of the extern implementation to call, + // avoiding direct references to generic datatype constructors + // since their calling pattern is different between different versions of Dafny + // (i.e. after 4.2, explicit type descriptors are required). + + function method CreateGenerateBytesSuccess(bytes: seq): Result, Types.Error> { + Success(bytes) + } + + function method CreateGenerateBytesFailure(error: Types.Error): Result, Types.Error> { + Failure(error) + } } diff --git a/AwsCryptographyPrimitives/src/Signature.dfy b/AwsCryptographyPrimitives/src/Signature.dfy index ba6ef34fd8..b550b9fda5 100644 --- a/AwsCryptographyPrimitives/src/Signature.dfy +++ b/AwsCryptographyPrimitives/src/Signature.dfy @@ -74,4 +74,33 @@ module {:extern "Signature"} Signature { msg: seq, sig: seq ): (res: Result) + + // The next six functions are for the benefit of the extern implementation to call, + // avoiding direct references to generic datatype constructors + // since their calling pattern is different between different versions of Dafny + // (i.e. after 4.2, explicit type descriptors are required). + + function method CreateExternKeyGenSuccess(output: SignatureKeyPair): Result { + Success(output) + } + + function method CreateExternKeyGenFailure(error: Types.Error): Result { + Failure(error) + } + + function method CreateSignSuccess(bytes: seq): Result, Types.Error> { + Success(bytes) + } + + function method CreateSignFailure(error: Types.Error): Result, Types.Error> { + Failure(error) + } + + function method CreateVerifySuccess(b: bool): Result { + Success(b) + } + + function method CreateVerifyFailure(error: Types.Error): Result { + Failure(error) + } } diff --git a/ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.2.0.patch b/ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.2.0.patch new file mode 100644 index 0000000000..10981d791c --- /dev/null +++ b/ComAmazonawsDynamodb/codegen-patches/dotnet/dafny-4.2.0.patch @@ -0,0 +1,19 @@ +diff --git b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs +index 72738b20..83ba3510 100644 +--- b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs ++++ a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs +@@ -10809,7 +10809,13 @@ namespace Com.Amazonaws.Dynamodb + } + public static Wrappers_Compile._IOption>> ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S10_Projection__M16_NonKeyAttributes(System.Collections.Generic.List value) + { +- return value == null ? Wrappers_Compile.Option>>.create_None() : Wrappers_Compile.Option>>.create_Some(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_NonKeyAttributeNameList((System.Collections.Generic.List)value)); ++ // BEGIN MANUAL EDIT ++ if (value == null || value.Count == 0) ++ { ++ return Wrappers_Compile.Option>>.create_None(); ++ } ++ return Wrappers_Compile.Option>>.create_Some(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_NonKeyAttributeNameList((System.Collections.Generic.List)value)); ++ // END MANUAL EDIT + } + public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S30_LocalSecondaryIndexDescription__M9_IndexName(Wrappers_Compile._IOption> value) + { diff --git a/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch new file mode 100644 index 0000000000..3b6150cf13 --- /dev/null +++ b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch @@ -0,0 +1,193 @@ +diff --git b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java +index 04e0401..c2f8787 100644 +--- b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java ++++ a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java +@@ -10489,16 +10489,9 @@ public class ToDafny { + } + + public static Error Error(DynamoDbException nativeValue) { +- Option> message; +- message = +- Objects.nonNull(nativeValue.getMessage()) +- ? Option.create_Some( +- software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( +- nativeValue.getMessage() +- ) +- ) +- : Option.create_None(); +- return new Error_Opaque(message); ++ // BEGIN MANUAL EDIT ++ return new Error_Opaque(nativeValue); ++ // END MANUAL EDIT + } + + public static IDynamoDBClient DynamoDB_20120810(DynamoDbClient nativeValue) { +diff --git b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java +index e3fa41d..80bf84d 100644 +--- b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java ++++ a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java +@@ -109,6 +109,9 @@ import software.amazon.awssdk.services.dynamodb.model.DestinationStatus; + import software.amazon.awssdk.services.dynamodb.model.DisableKinesisStreamingDestinationRequest; + import software.amazon.awssdk.services.dynamodb.model.DisableKinesisStreamingDestinationResponse; + import software.amazon.awssdk.services.dynamodb.model.DuplicateItemException; ++// BEGIN MANUAL EDIT ++import software.amazon.awssdk.services.dynamodb.model.DynamoDbException; ++// END MANUAL EDIT + import software.amazon.awssdk.services.dynamodb.model.EnableKinesisStreamingDestinationRequest; + import software.amazon.awssdk.services.dynamodb.model.EnableKinesisStreamingDestinationResponse; + import software.amazon.awssdk.services.dynamodb.model.Endpoint; +@@ -349,6 +352,9 @@ import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_InvalidRestoreTimeException; + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ItemCollectionSizeLimitExceededException; + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_LimitExceededException; ++// BEGIN MANUAL EDIT ++import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_Opaque; ++// END MANUAL EDIT + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_PointInTimeRecoveryUnavailableException; + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ProvisionedThroughputExceededException; + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ReplicaAlreadyExistsException; +@@ -422,6 +428,19 @@ import software.amazon.cryptography.services.dynamodb.internaldafny.types.Update + + public class ToNative { + ++ // BEGIN MANUAL EDIT ++ public static RuntimeException Error(Error_Opaque dafnyValue) { ++ if (dafnyValue.dtor_obj() instanceof DynamoDbException) { ++ return (DynamoDbException) dafnyValue.dtor_obj(); ++ } ++ // Because we only ever put `DynamoDbException` into `Error_Opaque`, ++ // recieving any other type here indicates a bug with the codegen. ++ // Bubble up some error to indicate this failure state. ++ return new IllegalStateException("Unknown error recieved from DynamoDb."); ++ } ++ ++ // END MANUAL EDIT ++ + public static ArchivalSummary ArchivalSummary( + software.amazon.cryptography.services.dynamodb.internaldafny.types.ArchivalSummary dafnyValue + ) { +@@ -8035,6 +8054,124 @@ public class ToNative { + return builder.build(); + } + ++ // BEGIN MANUAL EDIT ++ public static RuntimeException Error( ++ software.amazon.cryptography.services.dynamodb.internaldafny.types.Error dafnyValue ++ ) { ++ if (dafnyValue.is_BackupInUseException()) { ++ return ToNative.Error((Error_BackupInUseException) dafnyValue); ++ } ++ if (dafnyValue.is_BackupNotFoundException()) { ++ return ToNative.Error((Error_BackupNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_ConditionalCheckFailedException()) { ++ return ToNative.Error((Error_ConditionalCheckFailedException) dafnyValue); ++ } ++ if (dafnyValue.is_ContinuousBackupsUnavailableException()) { ++ return ToNative.Error( ++ (Error_ContinuousBackupsUnavailableException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_DuplicateItemException()) { ++ return ToNative.Error((Error_DuplicateItemException) dafnyValue); ++ } ++ if (dafnyValue.is_ExportConflictException()) { ++ return ToNative.Error((Error_ExportConflictException) dafnyValue); ++ } ++ if (dafnyValue.is_ExportNotFoundException()) { ++ return ToNative.Error((Error_ExportNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_GlobalTableAlreadyExistsException()) { ++ return ToNative.Error( ++ (Error_GlobalTableAlreadyExistsException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_GlobalTableNotFoundException()) { ++ return ToNative.Error((Error_GlobalTableNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_IdempotentParameterMismatchException()) { ++ return ToNative.Error( ++ (Error_IdempotentParameterMismatchException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_ImportConflictException()) { ++ return ToNative.Error((Error_ImportConflictException) dafnyValue); ++ } ++ if (dafnyValue.is_ImportNotFoundException()) { ++ return ToNative.Error((Error_ImportNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_IndexNotFoundException()) { ++ return ToNative.Error((Error_IndexNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_InternalServerError()) { ++ return ToNative.Error((Error_InternalServerError) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidExportTimeException()) { ++ return ToNative.Error((Error_InvalidExportTimeException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidRestoreTimeException()) { ++ return ToNative.Error((Error_InvalidRestoreTimeException) dafnyValue); ++ } ++ if (dafnyValue.is_ItemCollectionSizeLimitExceededException()) { ++ return ToNative.Error( ++ (Error_ItemCollectionSizeLimitExceededException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_LimitExceededException()) { ++ return ToNative.Error((Error_LimitExceededException) dafnyValue); ++ } ++ if (dafnyValue.is_PointInTimeRecoveryUnavailableException()) { ++ return ToNative.Error( ++ (Error_PointInTimeRecoveryUnavailableException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_ProvisionedThroughputExceededException()) { ++ return ToNative.Error( ++ (Error_ProvisionedThroughputExceededException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_ReplicaAlreadyExistsException()) { ++ return ToNative.Error((Error_ReplicaAlreadyExistsException) dafnyValue); ++ } ++ if (dafnyValue.is_ReplicaNotFoundException()) { ++ return ToNative.Error((Error_ReplicaNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_RequestLimitExceeded()) { ++ return ToNative.Error((Error_RequestLimitExceeded) dafnyValue); ++ } ++ if (dafnyValue.is_ResourceInUseException()) { ++ return ToNative.Error((Error_ResourceInUseException) dafnyValue); ++ } ++ if (dafnyValue.is_ResourceNotFoundException()) { ++ return ToNative.Error((Error_ResourceNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_TableAlreadyExistsException()) { ++ return ToNative.Error((Error_TableAlreadyExistsException) dafnyValue); ++ } ++ if (dafnyValue.is_TableInUseException()) { ++ return ToNative.Error((Error_TableInUseException) dafnyValue); ++ } ++ if (dafnyValue.is_TableNotFoundException()) { ++ return ToNative.Error((Error_TableNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_TransactionCanceledException()) { ++ return ToNative.Error((Error_TransactionCanceledException) dafnyValue); ++ } ++ if (dafnyValue.is_TransactionConflictException()) { ++ return ToNative.Error((Error_TransactionConflictException) dafnyValue); ++ } ++ if (dafnyValue.is_TransactionInProgressException()) { ++ return ToNative.Error((Error_TransactionInProgressException) dafnyValue); ++ } ++ if (dafnyValue.is_Opaque()) { ++ return ToNative.Error((Error_Opaque) dafnyValue); ++ } ++ // TODO This should indicate a codegen bug ++ return new IllegalStateException("Unknown error recieved from DynamoDb."); ++ } ++ ++ // END MANUAL EDIT ++ + public static DynamoDbClient DynamoDB_20120810(IDynamoDBClient dafnyValue) { + return ((Shim) dafnyValue).impl(); + } diff --git a/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.3.0.patch b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.3.0.patch new file mode 100644 index 0000000000..a4a8b9249c --- /dev/null +++ b/ComAmazonawsDynamodb/codegen-patches/java/dafny-4.3.0.patch @@ -0,0 +1,196 @@ +diff --git b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java +index 04e0401..c2f8787 100644 +--- b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java ++++ a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java +@@ -10489,19 +10489,9 @@ public class ToDafny { + } + + public static Error Error(DynamoDbException nativeValue) { +- Option> message; +- message = +- Objects.nonNull(nativeValue.getMessage()) +- ? Option.create_Some( +- DafnySequence._typeDescriptor(TypeDescriptor.CHAR), +- software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( +- nativeValue.getMessage() +- ) +- ) +- : Option.create_None( +- DafnySequence._typeDescriptor(TypeDescriptor.CHAR) +- ); +- return new Error_Opaque(message); ++ // BEGIN MANUAL EDIT ++ return new Error_Opaque(nativeValue); ++ // END MANUAL EDIT + } + + public static IDynamoDBClient DynamoDB_20120810(DynamoDbClient nativeValue) { +diff --git b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java +index e3fa41d..80bf84d 100644 +--- b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java ++++ a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java +@@ -109,6 +109,9 @@ import software.amazon.awssdk.services.dynamodb.model.DestinationStatus; + import software.amazon.awssdk.services.dynamodb.model.DisableKinesisStreamingDestinationRequest; + import software.amazon.awssdk.services.dynamodb.model.DisableKinesisStreamingDestinationResponse; + import software.amazon.awssdk.services.dynamodb.model.DuplicateItemException; ++// BEGIN MANUAL EDIT ++import software.amazon.awssdk.services.dynamodb.model.DynamoDbException; ++// END MANUAL EDIT + import software.amazon.awssdk.services.dynamodb.model.EnableKinesisStreamingDestinationRequest; + import software.amazon.awssdk.services.dynamodb.model.EnableKinesisStreamingDestinationResponse; + import software.amazon.awssdk.services.dynamodb.model.Endpoint; +@@ -349,6 +352,9 @@ import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_InvalidRestoreTimeException; + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ItemCollectionSizeLimitExceededException; + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_LimitExceededException; ++// BEGIN MANUAL EDIT ++import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_Opaque; ++// END MANUAL EDIT + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_PointInTimeRecoveryUnavailableException; + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ProvisionedThroughputExceededException; + import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ReplicaAlreadyExistsException; +@@ -422,6 +428,19 @@ import software.amazon.cryptography.services.dynamodb.internaldafny.types.Update + + public class ToNative { + ++ // BEGIN MANUAL EDIT ++ public static RuntimeException Error(Error_Opaque dafnyValue) { ++ if (dafnyValue.dtor_obj() instanceof DynamoDbException) { ++ return (DynamoDbException) dafnyValue.dtor_obj(); ++ } ++ // Because we only ever put `DynamoDbException` into `Error_Opaque`, ++ // recieving any other type here indicates a bug with the codegen. ++ // Bubble up some error to indicate this failure state. ++ return new IllegalStateException("Unknown error recieved from DynamoDb."); ++ } ++ ++ // END MANUAL EDIT ++ + public static ArchivalSummary ArchivalSummary( + software.amazon.cryptography.services.dynamodb.internaldafny.types.ArchivalSummary dafnyValue + ) { +@@ -8035,6 +8054,124 @@ public class ToNative { + return builder.build(); + } + ++ // BEGIN MANUAL EDIT ++ public static RuntimeException Error( ++ software.amazon.cryptography.services.dynamodb.internaldafny.types.Error dafnyValue ++ ) { ++ if (dafnyValue.is_BackupInUseException()) { ++ return ToNative.Error((Error_BackupInUseException) dafnyValue); ++ } ++ if (dafnyValue.is_BackupNotFoundException()) { ++ return ToNative.Error((Error_BackupNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_ConditionalCheckFailedException()) { ++ return ToNative.Error((Error_ConditionalCheckFailedException) dafnyValue); ++ } ++ if (dafnyValue.is_ContinuousBackupsUnavailableException()) { ++ return ToNative.Error( ++ (Error_ContinuousBackupsUnavailableException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_DuplicateItemException()) { ++ return ToNative.Error((Error_DuplicateItemException) dafnyValue); ++ } ++ if (dafnyValue.is_ExportConflictException()) { ++ return ToNative.Error((Error_ExportConflictException) dafnyValue); ++ } ++ if (dafnyValue.is_ExportNotFoundException()) { ++ return ToNative.Error((Error_ExportNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_GlobalTableAlreadyExistsException()) { ++ return ToNative.Error( ++ (Error_GlobalTableAlreadyExistsException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_GlobalTableNotFoundException()) { ++ return ToNative.Error((Error_GlobalTableNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_IdempotentParameterMismatchException()) { ++ return ToNative.Error( ++ (Error_IdempotentParameterMismatchException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_ImportConflictException()) { ++ return ToNative.Error((Error_ImportConflictException) dafnyValue); ++ } ++ if (dafnyValue.is_ImportNotFoundException()) { ++ return ToNative.Error((Error_ImportNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_IndexNotFoundException()) { ++ return ToNative.Error((Error_IndexNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_InternalServerError()) { ++ return ToNative.Error((Error_InternalServerError) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidExportTimeException()) { ++ return ToNative.Error((Error_InvalidExportTimeException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidRestoreTimeException()) { ++ return ToNative.Error((Error_InvalidRestoreTimeException) dafnyValue); ++ } ++ if (dafnyValue.is_ItemCollectionSizeLimitExceededException()) { ++ return ToNative.Error( ++ (Error_ItemCollectionSizeLimitExceededException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_LimitExceededException()) { ++ return ToNative.Error((Error_LimitExceededException) dafnyValue); ++ } ++ if (dafnyValue.is_PointInTimeRecoveryUnavailableException()) { ++ return ToNative.Error( ++ (Error_PointInTimeRecoveryUnavailableException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_ProvisionedThroughputExceededException()) { ++ return ToNative.Error( ++ (Error_ProvisionedThroughputExceededException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_ReplicaAlreadyExistsException()) { ++ return ToNative.Error((Error_ReplicaAlreadyExistsException) dafnyValue); ++ } ++ if (dafnyValue.is_ReplicaNotFoundException()) { ++ return ToNative.Error((Error_ReplicaNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_RequestLimitExceeded()) { ++ return ToNative.Error((Error_RequestLimitExceeded) dafnyValue); ++ } ++ if (dafnyValue.is_ResourceInUseException()) { ++ return ToNative.Error((Error_ResourceInUseException) dafnyValue); ++ } ++ if (dafnyValue.is_ResourceNotFoundException()) { ++ return ToNative.Error((Error_ResourceNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_TableAlreadyExistsException()) { ++ return ToNative.Error((Error_TableAlreadyExistsException) dafnyValue); ++ } ++ if (dafnyValue.is_TableInUseException()) { ++ return ToNative.Error((Error_TableInUseException) dafnyValue); ++ } ++ if (dafnyValue.is_TableNotFoundException()) { ++ return ToNative.Error((Error_TableNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_TransactionCanceledException()) { ++ return ToNative.Error((Error_TransactionCanceledException) dafnyValue); ++ } ++ if (dafnyValue.is_TransactionConflictException()) { ++ return ToNative.Error((Error_TransactionConflictException) dafnyValue); ++ } ++ if (dafnyValue.is_TransactionInProgressException()) { ++ return ToNative.Error((Error_TransactionInProgressException) dafnyValue); ++ } ++ if (dafnyValue.is_Opaque()) { ++ return ToNative.Error((Error_Opaque) dafnyValue); ++ } ++ // TODO This should indicate a codegen bug ++ return new IllegalStateException("Unknown error recieved from DynamoDb."); ++ } ++ ++ // END MANUAL EDIT ++ + public static DynamoDbClient DynamoDB_20120810(IDynamoDBClient dafnyValue) { + return ((Shim) dafnyValue).impl(); + } diff --git a/ComAmazonawsDynamodb/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/__default.java b/ComAmazonawsDynamodb/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/__default.java index f5f41dadbc..ded56e790f 100644 --- a/ComAmazonawsDynamodb/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/__default.java +++ b/ComAmazonawsDynamodb/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/__default.java @@ -5,6 +5,7 @@ import static software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence; import static software.amazon.smithy.dafny.conversion.ToNative.Simple.String; +import StandardLibraryInterop_Compile.WrappersInterop; import Wrappers_Compile.Option; import Wrappers_Compile.Result; import dafny.DafnySequence; @@ -26,12 +27,12 @@ public static Result DynamoDBClient() { .build(); IDynamoDBClient shim = new Shim(ddbClient, region.toString()); - return Result.create_Success(shim); + return CreateSuccessOfClient(shim); } catch (Exception e) { Error dafny_error = Error.create_InternalServerError( - Option.create_Some(CharacterSequence(e.getMessage())) + WrappersInterop.CreateStringSome(CharacterSequence(e.getMessage())) ); - return Result.create_Failure(dafny_error); + return CreateFailureOfError(dafny_error); } } @@ -48,12 +49,12 @@ public static Result DDBClientForRegion( .build(); IDynamoDBClient shim = new Shim(ddbClient, regionString); - return Result.create_Success(shim); + return CreateSuccessOfClient(shim); } catch (Exception e) { Error dafny_error = Error.create_InternalServerError( - Option.create_Some(CharacterSequence(e.getMessage())) + WrappersInterop.CreateStringSome(CharacterSequence(e.getMessage())) ); - return Result.create_Failure(dafny_error); + return CreateFailureOfError(dafny_error); } } } diff --git a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs index b877415419..83ba3510b0 100644 --- a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs +++ b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs @@ -5274,7 +5274,12 @@ public static System.IO.MemoryStream FromDafny_N3_com__N9_amazonaws__N8_dynamodb } public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S20_BinaryAttributeValue(System.IO.MemoryStream value) { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } return Dafny.Sequence.FromArray(value.ToArray()); + } public static System.Collections.Generic.List FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_StringSetAttributeValue(Dafny.ISequence> value) { diff --git a/ComAmazonawsKms/codegen-patches/java/dafny-4.2.0.patch b/ComAmazonawsKms/codegen-patches/java/dafny-4.2.0.patch new file mode 100644 index 0000000000..15d5e519e5 --- /dev/null +++ b/ComAmazonawsKms/codegen-patches/java/dafny-4.2.0.patch @@ -0,0 +1,202 @@ +diff --git b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java +index 9084fae1..880ddcae 100644 +--- b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java ++++ a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java +@@ -4179,16 +4179,9 @@ public class ToDafny { + } + + public static Error Error(KmsException nativeValue) { +- Option> message; +- message = +- Objects.nonNull(nativeValue.getMessage()) +- ? Option.create_Some( +- software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( +- nativeValue.getMessage() +- ) +- ) +- : Option.create_None(); +- return new Error_Opaque(message); ++ // BEGIN MANUAL EDIT ++ return new Error_Opaque(nativeValue); ++ // END MANUAL EDIT + } + + public static IKMSClient TrentService(KmsClient nativeValue) { +diff --git b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java +index b4cc1964..98e53314 100644 +--- b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java ++++ a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java +@@ -103,6 +103,9 @@ import software.amazon.awssdk.services.kms.model.KeySpec; + import software.amazon.awssdk.services.kms.model.KeyState; + import software.amazon.awssdk.services.kms.model.KeyUnavailableException; + import software.amazon.awssdk.services.kms.model.KeyUsageType; ++// BEGIN MANUAL EDIT ++import software.amazon.awssdk.services.kms.model.KmsException; ++// END MANUAL EDIT + import software.amazon.awssdk.services.kms.model.KmsInternalException; + import software.amazon.awssdk.services.kms.model.KmsInvalidSignatureException; + import software.amazon.awssdk.services.kms.model.KmsInvalidStateException; +@@ -178,12 +181,30 @@ import software.amazon.cryptography.services.kms.internaldafny.types.Error_KeyUn + import software.amazon.cryptography.services.kms.internaldafny.types.Error_LimitExceededException; + import software.amazon.cryptography.services.kms.internaldafny.types.Error_MalformedPolicyDocumentException; + import software.amazon.cryptography.services.kms.internaldafny.types.Error_NotFoundException; ++import software.amazon.cryptography.services.kms.internaldafny.types.Error_Opaque; + import software.amazon.cryptography.services.kms.internaldafny.types.Error_TagException; ++// END MANUAL EDIT ++import software.amazon.cryptography.services.kms.internaldafny.types.Error_TagException; ++import software.amazon.cryptography.services.kms.internaldafny.types.Error_UnsupportedOperationException; + import software.amazon.cryptography.services.kms.internaldafny.types.Error_UnsupportedOperationException; ++// BEGIN MANUAL EDIT + import software.amazon.cryptography.services.kms.internaldafny.types.IKMSClient; + + public class ToNative { + ++ // BEGIN MANUAL EDIT ++ public static RuntimeException Error(Error_Opaque dafnyValue) { ++ if (dafnyValue.dtor_obj() instanceof KmsException) { ++ return (KmsException) dafnyValue.dtor_obj(); ++ } ++ // Because we only ever put `KmsException` into `Error_Opaque`, ++ // recieving any other type here indicates a bug with the codegen. ++ // Bubble up some error to indicate this failure state. ++ return new IllegalStateException("Unknown error recieved from KMS."); ++ } ++ ++ // END MANUAL EDIT ++ + public static AlgorithmSpec AlgorithmSpec( + software.amazon.cryptography.services.kms.internaldafny.types.AlgorithmSpec dafnyValue + ) { +@@ -3339,6 +3360,132 @@ public class ToNative { + return builder.build(); + } + ++ // BEGIN MANUAL EDIT ++ public static RuntimeException Error( ++ software.amazon.cryptography.services.kms.internaldafny.types.Error dafnyValue ++ ) { ++ if (dafnyValue.is_AlreadyExistsException()) { ++ return ToNative.Error((Error_AlreadyExistsException) dafnyValue); ++ } ++ if (dafnyValue.is_CloudHsmClusterInUseException()) { ++ return ToNative.Error((Error_CloudHsmClusterInUseException) dafnyValue); ++ } ++ if (dafnyValue.is_CloudHsmClusterInvalidConfigurationException()) { ++ return ToNative.Error( ++ (Error_CloudHsmClusterInvalidConfigurationException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_CloudHsmClusterNotActiveException()) { ++ return ToNative.Error( ++ (Error_CloudHsmClusterNotActiveException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_CloudHsmClusterNotFoundException()) { ++ return ToNative.Error( ++ (Error_CloudHsmClusterNotFoundException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_CloudHsmClusterNotRelatedException()) { ++ return ToNative.Error( ++ (Error_CloudHsmClusterNotRelatedException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_CustomKeyStoreHasCMKsException()) { ++ return ToNative.Error((Error_CustomKeyStoreHasCMKsException) dafnyValue); ++ } ++ if (dafnyValue.is_CustomKeyStoreInvalidStateException()) { ++ return ToNative.Error( ++ (Error_CustomKeyStoreInvalidStateException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_CustomKeyStoreNameInUseException()) { ++ return ToNative.Error( ++ (Error_CustomKeyStoreNameInUseException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_CustomKeyStoreNotFoundException()) { ++ return ToNative.Error((Error_CustomKeyStoreNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_DependencyTimeoutException()) { ++ return ToNative.Error((Error_DependencyTimeoutException) dafnyValue); ++ } ++ if (dafnyValue.is_DisabledException()) { ++ return ToNative.Error((Error_DisabledException) dafnyValue); ++ } ++ if (dafnyValue.is_ExpiredImportTokenException()) { ++ return ToNative.Error((Error_ExpiredImportTokenException) dafnyValue); ++ } ++ if (dafnyValue.is_IncorrectKeyException()) { ++ return ToNative.Error((Error_IncorrectKeyException) dafnyValue); ++ } ++ if (dafnyValue.is_IncorrectKeyMaterialException()) { ++ return ToNative.Error((Error_IncorrectKeyMaterialException) dafnyValue); ++ } ++ if (dafnyValue.is_IncorrectTrustAnchorException()) { ++ return ToNative.Error((Error_IncorrectTrustAnchorException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidAliasNameException()) { ++ return ToNative.Error((Error_InvalidAliasNameException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidArnException()) { ++ return ToNative.Error((Error_InvalidArnException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidCiphertextException()) { ++ return ToNative.Error((Error_InvalidCiphertextException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidGrantIdException()) { ++ return ToNative.Error((Error_InvalidGrantIdException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidGrantTokenException()) { ++ return ToNative.Error((Error_InvalidGrantTokenException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidImportTokenException()) { ++ return ToNative.Error((Error_InvalidImportTokenException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidKeyUsageException()) { ++ return ToNative.Error((Error_InvalidKeyUsageException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidMarkerException()) { ++ return ToNative.Error((Error_InvalidMarkerException) dafnyValue); ++ } ++ if (dafnyValue.is_KeyUnavailableException()) { ++ return ToNative.Error((Error_KeyUnavailableException) dafnyValue); ++ } ++ if (dafnyValue.is_KMSInternalException()) { ++ return ToNative.Error((Error_KMSInternalException) dafnyValue); ++ } ++ if (dafnyValue.is_KMSInvalidSignatureException()) { ++ return ToNative.Error((Error_KMSInvalidSignatureException) dafnyValue); ++ } ++ if (dafnyValue.is_KMSInvalidStateException()) { ++ return ToNative.Error((Error_KMSInvalidStateException) dafnyValue); ++ } ++ if (dafnyValue.is_LimitExceededException()) { ++ return ToNative.Error((Error_LimitExceededException) dafnyValue); ++ } ++ if (dafnyValue.is_MalformedPolicyDocumentException()) { ++ return ToNative.Error( ++ (Error_MalformedPolicyDocumentException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_NotFoundException()) { ++ return ToNative.Error((Error_NotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_TagException()) { ++ return ToNative.Error((Error_TagException) dafnyValue); ++ } ++ if (dafnyValue.is_UnsupportedOperationException()) { ++ return ToNative.Error((Error_UnsupportedOperationException) dafnyValue); ++ } ++ if (dafnyValue.is_Opaque()) { ++ return ToNative.Error((Error_Opaque) dafnyValue); ++ } ++ // TODO This should indicate a codegen bug ++ return new IllegalStateException("Unknown error recieved from KMS."); ++ } ++ ++ // END MANUAL EDIT ++ + public static KmsClient TrentService(IKMSClient dafnyValue) { + return ((Shim) dafnyValue).impl(); + } diff --git a/ComAmazonawsKms/codegen-patches/java/dafny-4.3.0.patch b/ComAmazonawsKms/codegen-patches/java/dafny-4.3.0.patch new file mode 100644 index 0000000000..48b08ea2b6 --- /dev/null +++ b/ComAmazonawsKms/codegen-patches/java/dafny-4.3.0.patch @@ -0,0 +1,205 @@ +diff --git b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java +index 31895371..6a3a24f6 100644 +--- b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java ++++ a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java +@@ -4948,19 +4813,9 @@ public class ToDafny { + } + + public static Error Error(KmsException nativeValue) { +- Option> message; +- message = +- Objects.nonNull(nativeValue.getMessage()) +- ? Option.create_Some( +- DafnySequence._typeDescriptor(TypeDescriptor.CHAR), +- software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( +- nativeValue.getMessage() +- ) +- ) +- : Option.create_None( +- DafnySequence._typeDescriptor(TypeDescriptor.CHAR) +- ); +- return new Error_Opaque(message); ++ // BEGIN MANUAL EDIT ++ return new Error_Opaque(nativeValue); ++ // END MANUAL EDIT + } + + public static IKMSClient TrentService(KmsClient nativeValue) { +diff --git b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java +index b4cc1964..98e53314 100644 +--- b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java ++++ a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java +@@ -103,6 +103,9 @@ import software.amazon.awssdk.services.kms.model.KeySpec; + import software.amazon.awssdk.services.kms.model.KeyState; + import software.amazon.awssdk.services.kms.model.KeyUnavailableException; + import software.amazon.awssdk.services.kms.model.KeyUsageType; ++// BEGIN MANUAL EDIT ++import software.amazon.awssdk.services.kms.model.KmsException; ++// END MANUAL EDIT + import software.amazon.awssdk.services.kms.model.KmsInternalException; + import software.amazon.awssdk.services.kms.model.KmsInvalidSignatureException; + import software.amazon.awssdk.services.kms.model.KmsInvalidStateException; +@@ -178,12 +181,30 @@ import software.amazon.cryptography.services.kms.internaldafny.types.Error_KeyUn + import software.amazon.cryptography.services.kms.internaldafny.types.Error_LimitExceededException; + import software.amazon.cryptography.services.kms.internaldafny.types.Error_MalformedPolicyDocumentException; + import software.amazon.cryptography.services.kms.internaldafny.types.Error_NotFoundException; ++import software.amazon.cryptography.services.kms.internaldafny.types.Error_Opaque; + import software.amazon.cryptography.services.kms.internaldafny.types.Error_TagException; ++// END MANUAL EDIT ++import software.amazon.cryptography.services.kms.internaldafny.types.Error_TagException; ++import software.amazon.cryptography.services.kms.internaldafny.types.Error_UnsupportedOperationException; + import software.amazon.cryptography.services.kms.internaldafny.types.Error_UnsupportedOperationException; ++// BEGIN MANUAL EDIT + import software.amazon.cryptography.services.kms.internaldafny.types.IKMSClient; + + public class ToNative { + ++ // BEGIN MANUAL EDIT ++ public static RuntimeException Error(Error_Opaque dafnyValue) { ++ if (dafnyValue.dtor_obj() instanceof KmsException) { ++ return (KmsException) dafnyValue.dtor_obj(); ++ } ++ // Because we only ever put `KmsException` into `Error_Opaque`, ++ // recieving any other type here indicates a bug with the codegen. ++ // Bubble up some error to indicate this failure state. ++ return new IllegalStateException("Unknown error recieved from KMS."); ++ } ++ ++ // END MANUAL EDIT ++ + public static AlgorithmSpec AlgorithmSpec( + software.amazon.cryptography.services.kms.internaldafny.types.AlgorithmSpec dafnyValue + ) { +@@ -3339,6 +3360,132 @@ public class ToNative { + return builder.build(); + } + ++ // BEGIN MANUAL EDIT ++ public static RuntimeException Error( ++ software.amazon.cryptography.services.kms.internaldafny.types.Error dafnyValue ++ ) { ++ if (dafnyValue.is_AlreadyExistsException()) { ++ return ToNative.Error((Error_AlreadyExistsException) dafnyValue); ++ } ++ if (dafnyValue.is_CloudHsmClusterInUseException()) { ++ return ToNative.Error((Error_CloudHsmClusterInUseException) dafnyValue); ++ } ++ if (dafnyValue.is_CloudHsmClusterInvalidConfigurationException()) { ++ return ToNative.Error( ++ (Error_CloudHsmClusterInvalidConfigurationException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_CloudHsmClusterNotActiveException()) { ++ return ToNative.Error( ++ (Error_CloudHsmClusterNotActiveException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_CloudHsmClusterNotFoundException()) { ++ return ToNative.Error( ++ (Error_CloudHsmClusterNotFoundException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_CloudHsmClusterNotRelatedException()) { ++ return ToNative.Error( ++ (Error_CloudHsmClusterNotRelatedException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_CustomKeyStoreHasCMKsException()) { ++ return ToNative.Error((Error_CustomKeyStoreHasCMKsException) dafnyValue); ++ } ++ if (dafnyValue.is_CustomKeyStoreInvalidStateException()) { ++ return ToNative.Error( ++ (Error_CustomKeyStoreInvalidStateException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_CustomKeyStoreNameInUseException()) { ++ return ToNative.Error( ++ (Error_CustomKeyStoreNameInUseException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_CustomKeyStoreNotFoundException()) { ++ return ToNative.Error((Error_CustomKeyStoreNotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_DependencyTimeoutException()) { ++ return ToNative.Error((Error_DependencyTimeoutException) dafnyValue); ++ } ++ if (dafnyValue.is_DisabledException()) { ++ return ToNative.Error((Error_DisabledException) dafnyValue); ++ } ++ if (dafnyValue.is_ExpiredImportTokenException()) { ++ return ToNative.Error((Error_ExpiredImportTokenException) dafnyValue); ++ } ++ if (dafnyValue.is_IncorrectKeyException()) { ++ return ToNative.Error((Error_IncorrectKeyException) dafnyValue); ++ } ++ if (dafnyValue.is_IncorrectKeyMaterialException()) { ++ return ToNative.Error((Error_IncorrectKeyMaterialException) dafnyValue); ++ } ++ if (dafnyValue.is_IncorrectTrustAnchorException()) { ++ return ToNative.Error((Error_IncorrectTrustAnchorException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidAliasNameException()) { ++ return ToNative.Error((Error_InvalidAliasNameException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidArnException()) { ++ return ToNative.Error((Error_InvalidArnException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidCiphertextException()) { ++ return ToNative.Error((Error_InvalidCiphertextException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidGrantIdException()) { ++ return ToNative.Error((Error_InvalidGrantIdException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidGrantTokenException()) { ++ return ToNative.Error((Error_InvalidGrantTokenException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidImportTokenException()) { ++ return ToNative.Error((Error_InvalidImportTokenException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidKeyUsageException()) { ++ return ToNative.Error((Error_InvalidKeyUsageException) dafnyValue); ++ } ++ if (dafnyValue.is_InvalidMarkerException()) { ++ return ToNative.Error((Error_InvalidMarkerException) dafnyValue); ++ } ++ if (dafnyValue.is_KeyUnavailableException()) { ++ return ToNative.Error((Error_KeyUnavailableException) dafnyValue); ++ } ++ if (dafnyValue.is_KMSInternalException()) { ++ return ToNative.Error((Error_KMSInternalException) dafnyValue); ++ } ++ if (dafnyValue.is_KMSInvalidSignatureException()) { ++ return ToNative.Error((Error_KMSInvalidSignatureException) dafnyValue); ++ } ++ if (dafnyValue.is_KMSInvalidStateException()) { ++ return ToNative.Error((Error_KMSInvalidStateException) dafnyValue); ++ } ++ if (dafnyValue.is_LimitExceededException()) { ++ return ToNative.Error((Error_LimitExceededException) dafnyValue); ++ } ++ if (dafnyValue.is_MalformedPolicyDocumentException()) { ++ return ToNative.Error( ++ (Error_MalformedPolicyDocumentException) dafnyValue ++ ); ++ } ++ if (dafnyValue.is_NotFoundException()) { ++ return ToNative.Error((Error_NotFoundException) dafnyValue); ++ } ++ if (dafnyValue.is_TagException()) { ++ return ToNative.Error((Error_TagException) dafnyValue); ++ } ++ if (dafnyValue.is_UnsupportedOperationException()) { ++ return ToNative.Error((Error_UnsupportedOperationException) dafnyValue); ++ } ++ if (dafnyValue.is_Opaque()) { ++ return ToNative.Error((Error_Opaque) dafnyValue); ++ } ++ // TODO This should indicate a codegen bug ++ return new IllegalStateException("Unknown error recieved from KMS."); ++ } ++ ++ // END MANUAL EDIT ++ + public static KmsClient TrentService(IKMSClient dafnyValue) { + return ((Shim) dafnyValue).impl(); + } diff --git a/ComAmazonawsKms/runtimes/java/src/main/java/software/amazon/cryptography/services/kms/internaldafny/__default.java b/ComAmazonawsKms/runtimes/java/src/main/java/software/amazon/cryptography/services/kms/internaldafny/__default.java index 16fa6dff40..b24b89c52d 100644 --- a/ComAmazonawsKms/runtimes/java/src/main/java/software/amazon/cryptography/services/kms/internaldafny/__default.java +++ b/ComAmazonawsKms/runtimes/java/src/main/java/software/amazon/cryptography/services/kms/internaldafny/__default.java @@ -6,6 +6,7 @@ import static software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence; import static software.amazon.smithy.dafny.conversion.ToNative.Simple.String; +import StandardLibraryInterop_Compile.WrappersInterop; import Wrappers_Compile.Option; import Wrappers_Compile.Result; import dafny.DafnySequence; @@ -40,12 +41,12 @@ public static Result KMSClient() { ) .build(); final IKMSClient shim = new Shim(client, region); - return Result.create_Success(shim); + return CreateSuccessOfClient(shim); } catch (Exception e) { Error dafny_error = Error.create_KMSInternalException( - Option.create_Some(CharacterSequence(e.getMessage())) + WrappersInterop.CreateStringSome(CharacterSequence(e.getMessage())) ); - return Result.create_Failure(dafny_error); + return CreateFailureOfError(dafny_error); } } @@ -76,12 +77,12 @@ public static Result KMSClientForRegion( ) .build(); final IKMSClient shim = new Shim(client, regionString); - return Result.create_Success(shim); + return CreateSuccessOfClient(shim); } catch (Exception e) { Error dafny_error = Error.create_KMSInternalException( - Option.create_Some(CharacterSequence(e.getMessage())) + WrappersInterop.CreateStringSome(CharacterSequence(e.getMessage())) ); - return Result.create_Failure(dafny_error); + return CreateFailureOfError(dafny_error); } } @@ -98,14 +99,14 @@ public static Wrappers_Compile.Option RegionMatch( // have no way to determine what region it is // configured with. if (shim.region() == null) { - return Option.create_None(); + return WrappersInterop.CreateBooleanNone(); } // Otherwise we kept record of the region // when we created the client. String shimRegion = shim.region(); String regionStr = String(region); - return Option.create_Some(regionStr.equals(shimRegion)); + return WrappersInterop.CreateBooleanSome(regionStr.equals(shimRegion)); } private static String UserAgentSuffix() { diff --git a/ComAmazonawsKms/runtimes/net/Generated/TypeConversion.cs b/ComAmazonawsKms/runtimes/net/Generated/TypeConversion.cs index a41e10d0b8..26b0b91339 100644 --- a/ComAmazonawsKms/runtimes/net/Generated/TypeConversion.cs +++ b/ComAmazonawsKms/runtimes/net/Generated/TypeConversion.cs @@ -3933,7 +3933,12 @@ public static System.IO.MemoryStream FromDafny_N3_com__N9_amazonaws__N3_kms__S14 } public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N3_kms__S14_CiphertextType(System.IO.MemoryStream value) { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } return Dafny.Sequence.FromArray(value.ToArray()); + } public static System.Collections.Generic.Dictionary FromDafny_N3_com__N9_amazonaws__N3_kms__S21_EncryptionContextType(Dafny.IMap, Dafny.ISequence> value) { @@ -3951,7 +3956,12 @@ public static System.IO.MemoryStream FromDafny_N3_com__N9_amazonaws__N3_kms__S13 } public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N3_kms__S13_PlaintextType(System.IO.MemoryStream value) { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } return Dafny.Sequence.FromArray(value.ToArray()); + } public static int FromDafny_N3_com__N9_amazonaws__N3_kms__S9_LimitType(int value) { @@ -3983,7 +3993,12 @@ public static System.IO.MemoryStream FromDafny_N3_com__N9_amazonaws__N3_kms__S13 } public static Dafny.ISequence ToDafny_N3_com__N9_amazonaws__N3_kms__S13_PublicKeyType(System.IO.MemoryStream value) { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } return Dafny.Sequence.FromArray(value.ToArray()); + } public static int FromDafny_N3_com__N9_amazonaws__N3_kms__S17_NumberOfBytesType(int value) { diff --git a/Makefile b/Makefile index e7a42ef5ea..64c691472c 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,8 @@ # Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. # SPDX-License-Identifier: Apache-2.0 +PROJECT_ROOT := $(abspath $(dir $(abspath $(lastword $(MAKEFILE_LIST))))) + # This finds all Dafny projects in this repository # This makes building root level targets for each project easy PROJECTS = $(shell find . -mindepth 2 -maxdepth 2 -type f -name "Makefile" | xargs dirname | xargs basename) @@ -73,3 +75,21 @@ duvet_report: --source-pattern "(# //=,# //#).github/workflows/duvet.yaml" \ --source-pattern "TestVectorsAwsCryptographicMaterialProviders/dafny/**/src/**/*.dfy" \ --html specification_compliance_report.html + +# Generate the top-level project.properties file using smithy-dafny. +# This is for the benefit of the nightly Dafny CI, +# to verify that everything works with the latest Dafny prerelease. +# We use smithy-dafny rather than just cat-ing the file directly +# because smithy-dafny currently maintains the knowledge +# of how Dafny release versions maps to Dafny runtime library versions, +# especially prerelease versions like 4.4.0-nightly-2024-01-30-908f95f. +generate_properties_file: + cd smithy-dafny/codegen/smithy-dafny-codegen-cli; \ + ./../gradlew run --args="\ + --dafny-version ${DAFNY_VERSION} \ + --library-root $(PROJECT_ROOT)/StandardLibrary \ + --model $(PROJECT_ROOT)/StandardLibrary/Model \ + --dependent-model $(PROJECT_ROOT)/StandardLibrary/Model \ + --namespace aws.polymorph \ + --properties-file $(PROJECT_ROOT)/project.properties \ + "; diff --git a/SharedMakefileV2.mk b/SharedMakefileV2.mk index c6c5bf887b..9789ce6f18 100644 --- a/SharedMakefileV2.mk +++ b/SharedMakefileV2.mk @@ -61,6 +61,10 @@ SMITHY_MODEL_ROOT := $(LIBRARY_ROOT)/Model # for now we know this will work across the three environmnets we test in (windows, macos, ubuntu) COMPILE_SUFFIX_OPTION := -compileSuffix:1 +# The path to the smithy-dafny code generation CLI. +# Defaults to the copy in the smithy-dafny submodule but can be overridden. +CODEGEN_CLI_ROOT := $(PROJECT_ROOT)/smithy-dafny/codegen/smithy-dafny-codegen-cli + ########################## Dafny targets # Proof of correctness for the math below @@ -227,11 +231,12 @@ transpile_dependencies: # a single target can decide what parts it wants to build. _polymorph: - @: $(if ${CODEGEN_CLI_ROOT},,$(error You must pass the path CODEGEN_CLI_ROOT: CODEGEN_CLI_ROOT=/[path]/[to]/smithy-dafny/codegen/smithy-dafny-codegen-cli)); @: $(if ${DAFNY_VERSION},,$(error You must pass the value DAFNY_VERSION : DAFNY_VERSION=4.1)); cd $(CODEGEN_CLI_ROOT); \ ./../gradlew run --args="\ --dafny-version $(DAFNY_VERSION) \ + --library-root $(LIBRARY_ROOT) \ + --patch-files-dir $(if $(DIR_STRUCTURE_V2),$(LIBRARY_ROOT)/codegen-patches/$(SERVICE),$(LIBRARY_ROOT)/codegen-patches) \ $(OUTPUT_DAFNY) \ $(INPUT_DAFNY) \ $(OUTPUT_JAVA) \ @@ -242,20 +247,29 @@ _polymorph: --namespace $($(namespace_var)) \ $(AWS_SDK_CMD) \ $(OUTPUT_LOCAL_SERVICE_$(SERVICE)) \ + $(POLYMORPH_OPTIONS) \ "; +_polymorph_dependencies: + @$(foreach dependency, \ + $(PROJECT_DEPENDENCIES), \ + $(MAKE) -C $(PROJECT_ROOT)/$(dependency) polymorph_$(POLYMORPH_LANGUAGE_TARGET); \ + ) + # Generates all target runtime code for all namespaces in this project. .PHONY: polymorph_code_gen +polymorph_code_gen: POLYMORPH_LANGUAGE_TARGET=code_gen +polymorph_code_gen: _polymorph_dependencies polymorph_code_gen: - for service in $(PROJECT_SERVICES) ; do \ + set -e; for service in $(PROJECT_SERVICES) ; do \ export service_deps_var=SERVICE_DEPS_$${service} ; \ export namespace_var=SERVICE_NAMESPACE_$${service} ; \ export SERVICE=$${service} ; \ - $(MAKE) _polymorph_code_gen || exit 1; \ + $(MAKE) _polymorph_code_gen ; \ done _polymorph_code_gen: OUTPUT_DAFNY=\ - --output-dafny $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(LIBRARY_ROOT)/Model) + --output-dafny $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(LIBRARY_ROOT)/Model) _polymorph_code_gen: INPUT_DAFNY=\ --include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy _polymorph_code_gen: OUTPUT_DOTNET=\ @@ -263,30 +277,37 @@ _polymorph_code_gen: OUTPUT_DOTNET=\ _polymorph_code_gen: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated _polymorph_code_gen: _polymorph +check_polymorph_diff: + git diff --exit-code $(LIBRARY_ROOT) || (echo "ERROR: polymorph-generated code does not match the committed code - see above for diff. Either commit the changes or regenerate with 'POLYMORPH_OPTIONS=--update-patch-files'." && exit 1) + # Generates dafny code for all namespaces in this project .PHONY: polymorph_dafny +polymorph_dafny: POLYMORPH_LANGUAGE_TARGET=dafny +polymorph_dafny: _polymorph_dependencies polymorph_dafny: - for service in $(PROJECT_SERVICES) ; do \ + set -e; for service in $(PROJECT_SERVICES) ; do \ export service_deps_var=SERVICE_DEPS_$${service} ; \ export namespace_var=SERVICE_NAMESPACE_$${service} ; \ export SERVICE=$${service} ; \ - $(MAKE) _polymorph_dafny || exit 1; \ + $(MAKE) _polymorph_dafny ; \ done _polymorph_dafny: OUTPUT_DAFNY=\ - --output-dafny $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(LIBRARY_ROOT)/Model) + --output-dafny $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(LIBRARY_ROOT)/Model) _polymorph_dafny: INPUT_DAFNY=\ --include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy _polymorph_dafny: _polymorph # Generates dotnet code for all namespaces in this project .PHONY: polymorph_dotnet +polymorph_dotnet: POLYMORPH_LANGUAGE_TARGET=dotnet +polymorph_dotnet: _polymorph_dependencies polymorph_dotnet: - for service in $(PROJECT_SERVICES) ; do \ + set -e; for service in $(PROJECT_SERVICES) ; do \ export service_deps_var=SERVICE_DEPS_$${service} ; \ export namespace_var=SERVICE_NAMESPACE_$${service} ; \ export SERVICE=$${service} ; \ - $(MAKE) _polymorph_dotnet || exit 1; \ + $(MAKE) _polymorph_dotnet ; \ done _polymorph_dotnet: OUTPUT_DOTNET=\ @@ -295,12 +316,14 @@ _polymorph_dotnet: _polymorph # Generates java code for all namespaces in this project .PHONY: polymorph_java +polymorph_java: POLYMORPH_LANGUAGE_TARGET=java +polymorph_java: _polymorph_dependencies polymorph_java: - for service in $(PROJECT_SERVICES) ; do \ + set -e; for service in $(PROJECT_SERVICES) ; do \ export service_deps_var=SERVICE_DEPS_$${service} ; \ export namespace_var=SERVICE_NAMESPACE_$${service} ; \ export SERVICE=$${service} ; \ - $(MAKE) _polymorph_java || exit 1; \ + $(MAKE) _polymorph_java ; \ done _polymorph_java: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated diff --git a/StandardLibrary/Model/stdlib.smithy b/StandardLibrary/Model/stdlib.smithy new file mode 100644 index 0000000000..a84d4316ed --- /dev/null +++ b/StandardLibrary/Model/stdlib.smithy @@ -0,0 +1,11 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +namespace aws.polymorph + +// Dummy service just to keep polymorph happy. +service StandardLibrary { + version: "2021-11-01", + resources: [], + operations: [], + errors: [], +} diff --git a/StandardLibrary/runtimes/java/src/main/java/Time/__default.java b/StandardLibrary/runtimes/java/src/main/java/Time/__default.java index 31718b5c45..0074d8f3ac 100644 --- a/StandardLibrary/runtimes/java/src/main/java/Time/__default.java +++ b/StandardLibrary/runtimes/java/src/main/java/Time/__default.java @@ -7,7 +7,7 @@ import java.util.Date; import java.util.TimeZone; -public class __default { +public class __default extends Time._ExternBase___default { public static Long CurrentRelativeTime() { return System.currentTimeMillis() / 1000; @@ -21,13 +21,13 @@ > GetCurrentTimeStamp() { TimeZone tz = TimeZone.getTimeZone("UTC"); DateFormat df = new SimpleDateFormat("yyyy-MM-dd'T'HH:mm:ss:SSSSSS'Z'"); // Quoted "Z" to indicate UTC, no timezone offset df.setTimeZone(tz); - return Result.create_Success( + return CreateGetCurrentTimeStampSuccess( software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( df.format(new Date()) ) ); } catch (Exception var1) { - return Result.create_Failure( + return CreateGetCurrentTimeStampFailure( software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( "Could not generate a timestamp in ISO8601." ) diff --git a/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java b/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java index be9e6216b4..a44d737e96 100644 --- a/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java +++ b/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java @@ -38,7 +38,7 @@ > Encode(final DafnySequence s) { // outBuffer's capacity can be much higher than the limit. // By taking just the limit, we ensure we do not include // any allocated but un-filled space. - return Result.create_Success( + return CreateEncodeSuccess( (DafnySequence) ByteSequence( outBuffer, 0, @@ -46,7 +46,7 @@ > Encode(final DafnySequence s) { ) ); } catch (CharacterCodingException ex) { - return Result.create_Failure( + return CreateEncodeFailure( (DafnySequence) CharacterSequence( "Could not encode input to Dafny Bytes." ) @@ -68,13 +68,13 @@ > Decode(final DafnySequence s) { try { CharBuffer outBuffer = coder.decode(inBuffer); outBuffer.position(0); - return Result.create_Success( + return CreateDecodeSuccess( (DafnySequence) CharacterSequence( outBuffer.toString() ) ); } catch (CharacterCodingException ex) { - return Result.create_Failure( + return CreateDecodeFailure( (DafnySequence) CharacterSequence( "Could not encode input to Dafny Bytes." ) diff --git a/StandardLibrary/runtimes/java/src/main/java/UUID/__default.java b/StandardLibrary/runtimes/java/src/main/java/UUID/__default.java index 21b0dfdba9..ceac7ac0c7 100644 --- a/StandardLibrary/runtimes/java/src/main/java/UUID/__default.java +++ b/StandardLibrary/runtimes/java/src/main/java/UUID/__default.java @@ -8,26 +8,25 @@ import dafny.Array; import dafny.DafnySequence; import java.nio.ByteBuffer; -import java.util.UUID; -public class __default { +public class __default extends UUID._ExternBase___default { public static Result< DafnySequence, DafnySequence > ToByteArray(final DafnySequence s) { try { - UUID fromString = UUID.fromString(String(s)); + java.util.UUID fromString = java.util.UUID.fromString(String(s)); ByteBuffer byteBuffer = ByteBuffer.wrap(new byte[16]); // In Java the UUID construction stores the 8 most significant bytes // and the 8 least significant bytes that add up to 16 byte UUID. byteBuffer.putLong(fromString.getMostSignificantBits()); byteBuffer.putLong(fromString.getLeastSignificantBits()); - return Result.create_Success( + return CreateBytesSuccess( (DafnySequence) ByteSequence(byteBuffer) ); } catch (Exception e) { - return Result.create_Failure( + return CreateBytesFailure( (DafnySequence) CharacterSequence( "Could not convert UUID to byte array." ) @@ -49,14 +48,14 @@ > FromByteArray(final DafnySequence b) { // 8 + 8 = 16 that make up the 16 bytes of the UUID construction. long high = byteBuffer.getLong(); long low = byteBuffer.getLong(); - UUID fromByte = new UUID(high, low); - return Result.create_Success( + java.util.UUID fromByte = new java.util.UUID(high, low); + return CreateStringSuccess( (DafnySequence) CharacterSequence( fromByte.toString() ) ); } catch (Exception e) { - return Result.create_Failure( + return CreateStringFailure( (DafnySequence) CharacterSequence( "Could not convert byte array to UUID." ) @@ -69,12 +68,12 @@ > FromByteArray(final DafnySequence b) { DafnySequence > GenerateUUID() { try { - UUID uuid = UUID.randomUUID(); - return Result.create_Success( + java.util.UUID uuid = java.util.UUID.randomUUID(); + return CreateStringSuccess( (DafnySequence) CharacterSequence(uuid.toString()) ); } catch (Exception e) { - return Result.create_Failure( + return CreateStringFailure( (DafnySequence) CharacterSequence( "Could not generate a UUID." ) diff --git a/StandardLibrary/src/Index.dfy b/StandardLibrary/src/Index.dfy index 9a284ef709..fd6bee9462 100644 --- a/StandardLibrary/src/Index.dfy +++ b/StandardLibrary/src/Index.dfy @@ -18,6 +18,7 @@ include "./Time.dfy" include "./UInt.dfy" include "./UTF8.dfy" include "./UUID.dfy" +include "./WrappersInterop.dfy" include "../../libraries/src/JSON/API.dfy" include "../../libraries/src/FileIO/FileIO.dfy" include "../../libraries/src/BoundedInts.dfy" diff --git a/StandardLibrary/src/Time.dfy b/StandardLibrary/src/Time.dfy index 3065d1e2dc..2c7da906e2 100644 --- a/StandardLibrary/src/Time.dfy +++ b/StandardLibrary/src/Time.dfy @@ -20,4 +20,17 @@ module {:extern "Time"} Time { // Returns a timestamp for the current time in ISO8601 format in UTC // to microsecond precision (e.g. “YYYY-MM-DDTHH:mm:ss.ssssssZ“) function method {:extern "GetCurrentTimeStamp"} GetCurrentTimeStamp(): (res: Result) + + // The next two functions are for the benefit of the extern implementation to call, + // avoiding direct references to generic datatype constructors + // since their calling pattern is different between different versions of Dafny + // (i.e. after 4.2, explicit type descriptors are required). + + function method CreateGetCurrentTimeStampSuccess(value: string): Result { + Success(value) + } + + function method CreateGetCurrentTimeStampFailure(error: string): Result { + Failure(error) + } } diff --git a/StandardLibrary/src/UTF8.dfy b/StandardLibrary/src/UTF8.dfy index 8232797571..5c63419878 100644 --- a/StandardLibrary/src/UTF8.dfy +++ b/StandardLibrary/src/UTF8.dfy @@ -33,6 +33,27 @@ module {:extern "UTF8"} UTF8 { function method {:extern "Decode"} Decode(b: seq): (res: Result) ensures res.Success? ==> ValidUTF8Seq(b) + // The next four functions are for the benefit of the extern implementation to call, + // avoiding direct references to generic datatype constructors + // since their calling pattern is different between different versions of Dafny + // (i.e. after 4.2, explicit type descriptors are required). + + function method CreateEncodeSuccess(bytes: ValidUTF8Bytes): Result { + Success(bytes) + } + + function method CreateEncodeFailure(error: string): Result { + Failure(error) + } + + function method CreateDecodeSuccess(s: string): Result { + Success(s) + } + + function method CreateDecodeFailure(error: string): Result { + Failure(error) + } + predicate method IsASCIIString(s: string) { forall i :: 0 <= i < |s| ==> s[i] as int < 128 } diff --git a/StandardLibrary/src/UUID.dfy b/StandardLibrary/src/UUID.dfy index 5d0b84e3ee..ae0602a60e 100644 --- a/StandardLibrary/src/UUID.dfy +++ b/StandardLibrary/src/UUID.dfy @@ -21,4 +21,25 @@ module {:extern "UUID"} UUID { // because functions MUST NOT mutate the heap. method {:extern "GenerateUUID"} GenerateUUID() returns (res: Result) ensures res.Success? ==> 0 < |res.value| + + // The next four functions are for the benefit of the extern implementation to call, + // avoiding direct references to generic datatype constructors + // since their calling pattern is different between different versions of Dafny + // (i.e. after 4.2, explicit type descriptors are required). + + function method CreateBytesSuccess(bytes: seq): Result, string> { + Success(bytes) + } + + function method CreateBytesFailure(error: string): Result, string> { + Failure(error) + } + + function method CreateStringSuccess(s: string): Result { + Success(s) + } + + function method CreateStringFailure(error: string): Result { + Failure(error) + } } diff --git a/StandardLibrary/src/WrappersInterop.dfy b/StandardLibrary/src/WrappersInterop.dfy new file mode 100644 index 0000000000..1ee8de25c3 --- /dev/null +++ b/StandardLibrary/src/WrappersInterop.dfy @@ -0,0 +1,48 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +include "../../libraries/src/Wrappers.dfy" + +// +// Helper functions for extern code to call in order to create common wrapper types. +// +// This is currently necessary to abstract away from differences in TypeDescriptor usage +// in the Java backend across different versions of Dafny: +// after Dafny 4.2 methods like Option.create_Some() +// also require explicit TypeDescriptor arguments. +// If we declare a `CreateSome(t: T)` function, +// the compiled version may or may not need a type descriptor, +// which means externs would need to have different Java code for different Dafny versions. +// But if we define a non-generic version for a specific type, +// Dafny will emit the right type descriptor instances inside the compiled method, +// so the calling signature is the same across Dafny versions. +// +// These may be useful for other target languages in the future as well, +// to similarly abstract away from Dafny compilation internal details. +// +// See also DafnyApiCodegen.generateResultOfClientHelperFunctions() in smithy-dafny, +// which solves the same problem by emitting similar helper methods for each client type. +// +module StandardLibraryInterop { + + import opened Wrappers + + class WrappersInterop { + + static function method CreateStringSome(s: string): Option { + Some(s) + } + + static function method CreateStringNone(): Option { + None + } + + static function method CreateBooleanSome(b: bool): Option { + Some(b) + } + + static function method CreateBooleanNone(): Option { + None + } + } +} \ No newline at end of file diff --git a/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/TestVectorsAwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch b/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/TestVectorsAwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch new file mode 100644 index 0000000000..e55782a7a0 --- /dev/null +++ b/TestVectorsAwsCryptographicMaterialProviders/codegen-patches/TestVectorsAwsCryptographicMaterialProviders/dotnet/dafny-4.2.0.patch @@ -0,0 +1,15 @@ +diff --git b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs +index 87b39a81..e57de1dd 100644 +--- b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs ++++ a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs +@@ -3399,7 +3399,9 @@ namespace AWS.Cryptography.MaterialProviders.Wrapped + dafnyVal._ComAmazonawsDynamodb + ); + case software.amazon.cryptography.materialproviders.internaldafny.types.Error_ComAmazonawsKms dafnyVal: +- return Com.Amazonaws.KMS.TypeConversion.FromDafny_CommonError( ++ // BEGIN MANUAL EDIT ++ return Com.Amazonaws.Kms.TypeConversion.FromDafny_CommonError( ++ // END MANUAL EDIT + dafnyVal._ComAmazonawsKms + ); + case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographicMaterialProvidersException dafnyVal: diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyDescription.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyDescription.dfy index 037850166a..69943c6f07 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyDescription.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyDescription.dfy @@ -218,8 +218,8 @@ module {:options "-functionSyntax:4"} KeyDescription { // SYMMETRIC_DEFAULT is not supported because RSA is asymmetric only ] - type KeyDescriptionVersion = v: nat | KeyDescriptionVersion?(v) witness 1 - predicate KeyDescriptionVersion?(v: nat) + type KeyDescriptionVersion = v: int | KeyDescriptionVersion?(v) witness 1 + predicate KeyDescriptionVersion?(v: int) { || v == 1 || v == 2 diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviders/internaldafny/wrapped/__default.java b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviders/internaldafny/wrapped/__default.java index 992ee83afc..6f8c755674 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviders/internaldafny/wrapped/__default.java +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/java/software/amazon/cryptography/materialproviders/internaldafny/wrapped/__default.java @@ -25,6 +25,8 @@ > WrappedMaterialProviders(MaterialProvidersConfig config) { .builder() .impl(impl) .build(); - return Result.create_Success(wrappedClient); + return software.amazon.cryptography.materialproviders.internaldafny.__default.CreateSuccessOfClient( + wrappedClient + ); } } diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/KeyVectors/TypeConversion.cs b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/KeyVectors/TypeConversion.cs index 06b14889a6..62cf47ee88 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/KeyVectors/TypeConversion.cs +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/KeyVectors/TypeConversion.cs @@ -409,7 +409,12 @@ public static System.IO.MemoryStream FromDafny_N6_smithy__N3_api__S4_Blob(Dafny. } public static Dafny.ISequence ToDafny_N6_smithy__N3_api__S4_Blob(System.IO.MemoryStream value) { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } return Dafny.Sequence.FromArray(value.ToArray()); + } public static AWS.Cryptography.MaterialProvidersTestVectorKeys.KMSInfo FromDafny_N3_aws__N12_cryptography__N31_materialProvidersTestVectorKeys__S7_KMSInfo(software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types._IKMSInfo value) { diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs index 93bec9fb14..e57de1dd01 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs @@ -2438,7 +2438,12 @@ public static System.IO.MemoryStream FromDafny_N6_smithy__N3_api__S4_Blob(Dafny. } public static Dafny.ISequence ToDafny_N6_smithy__N3_api__S4_Blob(System.IO.MemoryStream value) { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } return Dafny.Sequence.FromArray(value.ToArray()); + } public static int FromDafny_N6_smithy__N3_api__S7_Integer(int value) { @@ -2621,7 +2626,12 @@ public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N17_mat } public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S6_Secret(System.IO.MemoryStream value) { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } return Dafny.Sequence.FromArray(value.ToArray()); + } public static Amazon.KeyManagementService.EncryptionAlgorithmSpec FromDafny_N3_com__N9_amazonaws__N3_kms__S23_EncryptionAlgorithmSpec(software.amazon.cryptography.services.kms.internaldafny.types._IEncryptionAlgorithmSpec value) { @@ -3271,7 +3281,12 @@ public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N8_keyS } public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N8_keyStore__S6_Secret(System.IO.MemoryStream value) { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } return Dafny.Sequence.FromArray(value.ToArray()); + } public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N8_keyStore__S10_HmacKeyMap(Dafny.IMap, Dafny.ISequence> value) { @@ -3371,6 +3386,10 @@ public static System.Exception FromDafny_CommonError(software.amazon.cryptograph { switch (value) { + case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographyKeyStore dafnyVal: + return AWS.Cryptography.KeyStore.TypeConversion.FromDafny_CommonError( + dafnyVal._AwsCryptographyKeyStore + ); case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographyPrimitives dafnyVal: return AWS.Cryptography.Primitives.TypeConversion.FromDafny_CommonError( dafnyVal._AwsCryptographyPrimitives @@ -3385,10 +3404,6 @@ public static System.Exception FromDafny_CommonError(software.amazon.cryptograph // END MANUAL EDIT dafnyVal._ComAmazonawsKms ); - case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographyKeyStore dafnyVal: - return AWS.Cryptography.KeyStore.TypeConversion.FromDafny_CommonError( - dafnyVal._AwsCryptographyKeyStore - ); case software.amazon.cryptography.materialproviders.internaldafny.types.Error_AwsCryptographicMaterialProvidersException dafnyVal: return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S42_AwsCryptographicMaterialProvidersException(dafnyVal); case software.amazon.cryptography.materialproviders.internaldafny.types.Error_EntryAlreadyExists dafnyVal: diff --git a/smithy-dafny b/smithy-dafny new file mode 160000 index 0000000000..91b0908f55 --- /dev/null +++ b/smithy-dafny @@ -0,0 +1 @@ +Subproject commit 91b0908f55691dac3932eef1f5f279442baa368c