From ac7d75b19ce5c1c17112cfc54c3222ebebff8207 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 09:46:57 -0800 Subject: [PATCH 01/31] Adopt SmithyDafnyMakefile.mk, apply codegen CI --- .github/actions/polymorph_codegen/action.yml | 116 +++++ .github/workflows/library_codegen.yml | 64 +++ .../workflows/library_dafny_verification.yml | 17 +- .github/workflows/library_java_tests.yml | 15 +- .github/workflows/library_net_tests.yml | 14 + .github/workflows/manual.yml | 34 ++ .github/workflows/nighly_dafny.yml | 3 + .gitmodules | 3 + SharedMakefileV2.mk | 418 +----------------- smithy-dafny | 1 + 10 files changed, 267 insertions(+), 418 deletions(-) create mode 100644 .github/actions/polymorph_codegen/action.yml create mode 100644 .github/workflows/library_codegen.yml create mode 100644 .github/workflows/manual.yml create mode 160000 smithy-dafny diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml new file mode 100644 index 000000000..9777a2137 --- /dev/null +++ b/.github/actions/polymorph_codegen/action.yml @@ -0,0 +1,116 @@ +# +# 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. +# +# Note that recursively generating code doesn't currently work in this repo +# with the version of the mpl pinned by the submodule, +# because the SharedMakefileV2.mk in it doesn't work with newer versions of smithy-dafny. +# Therefore by default we don't recursively regenerate code +# (accomplished by setting the POLYMORPH_DEPENDENCIES environment variable to ""). +# If `update-and-regenerate-mpl` is true, we first pull the latest mpl, +# which is necessary both for Makefile compatibility and so we can regenerate mpl code +# for compatibility with newer versions of Dafny. +# + +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 + update-and-regenerate-mpl: + description: "Locally update MPL to the tip of master and regenerate its code too" + required: false + default: false + 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: Update MPL submodule locally + if: inputs.update-and-regenerate-mpl == 'true' + run: | + git submodule update --init --recursive --remote --merge mpl + + - name: Don't regenerate dependencies + if: inputs.update-and-regenerate-mpl != 'true' + run: | + echo "POLYMORPH_DEPENDENCIES=" >> $GITHUB_ENV + + - 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/library_codegen.yml b/.github/workflows/library_codegen.yml new file mode 100644 index 000000000..08c5fbd51 --- /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 886e36b6e..645a6b1d9 100644 --- a/.github/workflows/library_dafny_verification.yml +++ b/.github/workflows/library_dafny_verification.yml @@ -7,7 +7,12 @@ on: dafny: description: 'The Dafny version to run' required: true - type: string + type: string + regenerate-code: + description: "Regenerate code using smithy-dafny" + required: false + default: false + type: boolean jobs: verification: @@ -33,10 +38,18 @@ jobs: git submodule update --init --recursive mpl - 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: Verify ${{ matrix.library }} Dafny code shell: bash working-directory: ./${{ matrix.library }} diff --git a/.github/workflows/library_java_tests.yml b/.github/workflows/library_java_tests.yml index 34e092a31..ab55a6a7b 100644 --- a/.github/workflows/library_java_tests.yml +++ b/.github/workflows/library_java_tests.yml @@ -8,6 +8,11 @@ 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: @@ -45,10 +50,18 @@ jobs: role-session-name: JavaTests - 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: diff --git a/.github/workflows/library_net_tests.yml b/.github/workflows/library_net_tests.yml index f55bf0b3f..a0e4856d6 100644 --- a/.github/workflows/library_net_tests.yml +++ b/.github/workflows/library_net_tests.yml @@ -8,6 +8,11 @@ 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 env: # Used in examples @@ -46,6 +51,7 @@ jobs: run: | git submodule update --init libraries git submodule update --init --recursive mpl + git submodule update --init smithy-dafny - name: Configure AWS Credentials uses: aws-actions/configure-aws-credentials@v2 @@ -64,6 +70,14 @@ jobs: 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: AwsEncryptionSDK + diff-generated-code: false + - name: Download Dependencies working-directory: ./AwsEncryptionSDK run: make setup_net diff --git a/.github/workflows/manual.yml b/.github/workflows/manual.yml new file mode 100644 index 000000000..74029c97d --- /dev/null +++ b/.github/workflows/manual.yml @@ -0,0 +1,34 @@ +# This workflow invokes other workflows with the requested Dafny build. +# It is primarily meant for manual compatibility testing, +# such as trying out what the next pending nightly build will do ahead of time. +name: Manual CI + +on: + workflow_dispatch: + inputs: + dafny: + 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-verification: + 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/nighly_dafny.yml b/.github/workflows/nighly_dafny.yml index 5da387431..1f93170c8 100644 --- a/.github/workflows/nighly_dafny.yml +++ b/.github/workflows/nighly_dafny.yml @@ -18,13 +18,16 @@ jobs: uses: ./.github/workflows/library_dafny_verification.yml with: dafny: 'nightly-latest' + regenerate-code: true # dafny-nightly-java: # if: github.event_name != 'schedule' || github.repository_owner == 'aws' # uses: ./.github/workflows/library_java_tests.yml # with: # dafny: 'nightly-latest' + # regenerate-code: true dafny-nightly-net: if: github.event_name != 'schedule' || github.repository_owner == 'aws' uses: ./.github/workflows/library_net_tests.yml with: dafny: 'nightly-latest' + regenerate-code: true diff --git a/.gitmodules b/.gitmodules index f2f326da7..1ab723319 100644 --- a/.gitmodules +++ b/.gitmodules @@ -8,3 +8,6 @@ [submodule "mpl"] path = mpl url = https://github.com/aws/aws-cryptographic-material-providers-library-dafny.git +[submodule "smithy-dafny"] + path = smithy-dafny + url = https://robin-aws@github.com/awslabs/smithy-dafny diff --git a/SharedMakefileV2.mk b/SharedMakefileV2.mk index e52d16d1f..49d545f68 100644 --- a/SharedMakefileV2.mk +++ b/SharedMakefileV2.mk @@ -1,424 +1,12 @@ # Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. # SPDX-License-Identifier: Apache-2.0 -# These make targets that are shared -# between all the projects in this repo. -# They will only function if executed inside a project directory. - -# There are several variables that are used here. -# The expectation is to define these variables -# inside each project. - -# Variables: -# MAX_RESOURCE_COUNT -- The Dafny report generator max resource count. -# This is is per project because the verification variability can differ. -# PROJECT_DEPENDENCIES -- List of dependencies for the project. -# It should be the list of top level directory names -# PROJECT_SERVICES -- List of names of each local service in the project -# SERVICE_NAMESPACE_ -- for each service in PROJECT_SERVICES, -# the list of dependencies for that smithy namespace. It should be a list -# of Model directories -# SERVICE_DEPS_ -- for each service in PROJECT_SERVICES, -# the list of dependencies for that smithy namespace. It should be a list -# of Model directories -# AWS_SDK_CMD -- the `--aws-sdk` command to generate AWS SDK style interfaces. -# STD_LIBRARY -- path from this file to the StandardLibrary Dafny project. -# SMITHY_DEPS -- path from this file to smithy dependencies, such as custom traits. - # This evaluates to the local path _of this file_. # This means that these are the project roots # that are shared by all libraries in this repo. PROJECT_ROOT := $(abspath $(dir $(abspath $(lastword $(MAKEFILE_LIST))))) -# This evaluates to the path of the current working directory. -# i.e. The specific library under consideration. -LIBRARY_ROOT := $(PWD) -# Smithy Dafny code gen needs to know -# where the smithy model is. -# This is generally in the same directory as the library. -# However in the case of a wrapped library, -# such as the test vectors -# the implementation MAY be in a different library -# than the model. -# By having two related variables -# test vector projects can point to -# the specific model they need -# but still build everything in their local library directory. -SMITHY_MODEL_ROOT := $(LIBRARY_ROOT)/Model - -# Later versions of Dafny no longer default to adding "_Compile" -# to the names of modules when translating. -# Our target language code still assumes it does, -# so IF the /compileSuffix option is available in our verion of Dafny -# we need to provide it. -# on 4.2.0 running on windows this shell command fails; we should fix this so the right -# thing happens on the right environment -# COMPILE_SUFFIX_OPTION_CHECK_EXIT_CODE := $(shell dafny /help | grep -q /compileSuffix; echo $$?) -# ifeq ($(COMPILE_SUFFIX_OPTION_CHECK_EXIT_CODE), 0) -# COMPILE_SUFFIX_OPTION := -compileSuffix:1 -# else -# COMPILE_SUFFIX_OPTION := -# endif -# for now we know this will work across the three environmnets we test in (windows, macos, ubuntu) -COMPILE_SUFFIX_OPTION := -compileSuffix:1 - -########################## Dafny targets - -# Verify the entire project -verify: - dafny \ - -vcsCores:$(CORES) \ - -compile:0 \ - -definiteAssignment:3 \ - -quantifierSyntax:3 \ - -unicodeChar:0 \ - -functionSyntax:3 \ - -verificationLogger:csv \ - -timeLimit:150 \ - -trace \ - `find . -name *.dfy` - -# Verify single file FILE with text logger. -# This is useful for debugging resource count usage within a file. -# Use PROC to further scope the verification -verify_single: - @: $(if ${CORES},,CORES=2); - dafny \ - -vcsCores:$(CORES) \ - -compile:0 \ - -definiteAssignment:3 \ - -quantifierSyntax:3 \ - -unicodeChar:0 \ - -functionSyntax:3 \ - -verificationLogger:text \ - -timeLimit:100 \ - -trace \ - $(if ${PROC},-proc:*$(PROC)*,) \ - $(FILE) - -#Verify only a specific namespace at env var $(SERVICE) -verify_service: - @: $(if ${SERVICE},,$(error You must pass the SERVICE to generate for)); - dafny \ - -vcsCores:$(CORES) \ - -compile:0 \ - -definiteAssignment:3 \ - -quantifierSyntax:3 \ - -unicodeChar:0 \ - -functionSyntax:3 \ - -verificationLogger:csv \ - -timeLimit:100 \ - -trace \ - `find ./dafny/$(SERVICE) -name '*.dfy'` \ - -format: - dafny format \ - --function-syntax 3 \ - --quantifier-syntax 3 \ - --unicode-char false \ - `find . -name '*.dfy'` - -format-check: - dafny format \ - --check \ - --function-syntax 3 \ - --quantifier-syntax 3 \ - --unicode-char false \ - `find . -name '*.dfy'` - -dafny-reportgenerator: - dafny-reportgenerator \ - summarize-csv-results \ - --max-resource-count $(MAX_RESOURCE_COUNT) \ - TestResults/*.csv - -# Dafny helper targets - -# Transpile the entire project's impl -_transpile_implementation_all: TRANSPILE_DEPENDENCIES=$(patsubst %, -library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX)) -_transpile_implementation_all: transpile_implementation - -# The `$(OUT)` and $(TARGET) variables are problematic. -# Ideally they are different for every target call. -# However the way make evaluates variables -# having a target specific variable is hard. -# This all comes up because a project -# will need to also transpile its dependencies. -# This is worked around for now, -# by the fact that the `TARGET` -# for all these transpile calls will be the same. -# For `OUT` this is solved by making the paths relative. -# So that the runtime is express once -# and can be the same for all such runtimes. -# Since such targets are all shared, -# this is tractable. - -# At this time is is *significatly* faster -# to give Dafny a single file -# that includes everything -# than it is to pass each file to the CLI. -# ~2m vs ~10s for our large projects. -# Also the expectation is that verification happens in the `verify` target -transpile_implementation: - find ./dafny/**/src ./src -name 'Index.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \ - -stdin \ - -noVerify \ - -vcsCores:$(CORES) \ - -compileTarget:$(TARGET) \ - -spillTargetCode:3 \ - -compile:0 \ - -optimizeErasableDatatypeWrapper:0 \ - $(COMPILE_SUFFIX_OPTION) \ - -quantifierSyntax:3 \ - -unicodeChar:0 \ - -functionSyntax:3 \ - -useRuntimeLib \ - -out $(OUT) \ - $(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \ - $(TRANSPILE_DEPENDENCIES) - -# Transpile the entire project's tests -_transpile_test_all: TRANSPILE_DEPENDENCIES=$(if ${DIR_STRUCTURE_V2}, $(patsubst %, -library:dafny/%/src/Index.dfy, $(PROJECT_SERVICES)), -library:src/Index.dfy) -_transpile_test_all: transpile_test - -transpile_test: - find ./dafny/**/test ./test -name "*.dfy" -name '*.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \ - -stdin \ - -noVerify \ - -vcsCores:$(CORES) \ - -compileTarget:$(TARGET) \ - -spillTargetCode:3 \ - -runAllTests:1 \ - -compile:0 \ - -optimizeErasableDatatypeWrapper:0 \ - $(COMPILE_SUFFIX_OPTION) \ - -quantifierSyntax:3 \ - -unicodeChar:0 \ - -functionSyntax:3 \ - -useRuntimeLib \ - -out $(OUT) \ - $(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \ - $(TRANSPILE_DEPENDENCIES) - - -# If we are not the StandardLibrary, transpile the StandardLibrary. -# Transpile all other dependencies -transpile_dependencies: - $(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) transpile_implementation_$(LANG), ) - $(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% transpile_implementation_$(LANG);, $(PROJECT_DEPENDENCIES)) - -########################## Code-Gen targets - -# StandardLibrary is filtered out from dependent-model patsubst list; -# Its model is contained in $(LIBRARY_ROOT)/model, not $(LIBRARY_ROOT)/../StandardLibrary/Model. - -# The OUTPUT variables are created this way -# so that it is possible to run _parts_ of polymorph. -# Otherwise it is difficult to run/test only a Dafny change. -# Since they are defined per target -# 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)); - cd $(CODEGEN_CLI_ROOT); \ - ./../gradlew run --args="\ - $(OUTPUT_DAFNY) \ - $(OUTPUT_JAVA) \ - $(OUTPUT_DOTNET) \ - --model $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(SMITHY_MODEL_ROOT)) \ - --dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \ - $(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \ - --namespace $($(namespace_var)) \ - $(AWS_SDK_CMD) \ - $(OUTPUT_LOCAL_SERVICE_$(SERVICE)) \ - "; - -# Generates all target runtime code for all namespaces in this project. -.PHONY: polymorph_code_gen -polymorph_code_gen: - 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; \ - done - -_polymorph_code_gen: OUTPUT_DAFNY=\ - --output-dafny $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(LIBRARY_ROOT)/Model) \ - --include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy -_polymorph_code_gen: OUTPUT_DOTNET=\ - $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/) -_polymorph_code_gen: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated -_polymorph_code_gen: _polymorph - -# Generates dafny code for all namespaces in this project -.PHONY: polymorph_dafny -polymorph_dafny: - 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; \ - done - -_polymorph_dafny: OUTPUT_DAFNY=\ - --output-dafny $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(LIBRARY_ROOT)/Model) \ - --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: - 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; \ - done - -_polymorph_dotnet: OUTPUT_DOTNET=\ - $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/) -_polymorph_dotnet: _polymorph - -# Generates java code for all namespaces in this project -.PHONY: polymorph_java -polymorph_java: - 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; \ - done - -_polymorph_java: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated -_polymorph_java: _polymorph - -########################## .NET targets - -transpile_net: | transpile_implementation_net transpile_test_net transpile_dependencies_net - -transpile_implementation_net: TARGET=cs -transpile_implementation_net: OUT=runtimes/net/ImplementationFromDafny -transpile_implementation_net: _transpile_implementation_all - -transpile_test_net: TARGET=cs -transpile_test_net: OUT=runtimes/net/tests/TestsFromDafny -transpile_test_net: _transpile_test_all - -transpile_dependencies_net: LANG=net -transpile_dependencies_net: transpile_dependencies - -test_net: FRAMEWORK=net6.0 -test_net: - dotnet run \ - --project runtimes/net/tests/ \ - --framework $(FRAMEWORK) - -test_net_mac_intel: FRAMEWORK=net6.0 -test_net_mac_intel: - DYLD_LIBRARY_PATH="/usr/local/opt/openssl@1.1/lib" dotnet run \ - --project runtimes/net/tests/ \ - --framework $(FRAMEWORK) - -test_net_mac_brew: FRAMEWORK=net6.0 -test_net_mac_brew: - DYLD_LIBRARY_PATH="$(shell brew --prefix)/opt/openssl@1.1/lib/" dotnet run \ - --project runtimes/net/tests/ \ - --framework $(FRAMEWORK) - -setup_net: - dotnet restore runtimes/net/ - -########################## Java targets - -build_java: transpile_java mvn_local_deploy_dependencies - gradle -p runtimes/java build - -transpile_java: | transpile_implementation_java transpile_test_java transpile_dependencies_java - -transpile_implementation_java: TARGET=java -transpile_implementation_java: OUT=runtimes/java/ImplementationFromDafny -transpile_implementation_java: _transpile_implementation_all _mv_implementation_java - -transpile_test_java: TARGET=java -transpile_test_java: OUT=runtimes/java/TestsFromDafny -transpile_test_java: _transpile_test_all _mv_test_java - -# Currently Dafny compiles to Java by changing the directory name. -# Java puts things under a `java` directory. -# To avoid `java/implementation-java` the code is generated and then moved. -_mv_implementation_java: - rm -rf runtimes/java/src/main/dafny-generated - mv runtimes/java/ImplementationFromDafny-java runtimes/java/src/main/dafny-generated -_mv_test_java: - rm -rf runtimes/java/src/test/dafny-generated - mkdir -p runtimes/java/src/test - mv runtimes/java/TestsFromDafny-java runtimes/java/src/test/dafny-generated - -transpile_dependencies_java: LANG=java -transpile_dependencies_java: transpile_dependencies - -# If we are not StandardLibrary, locally deploy the StandardLibrary. -# Locally deploy all other dependencies -mvn_local_deploy_dependencies: - $(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) mvn_local_deploy, ) - $(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% mvn_local_deploy;, $(PROJECT_DEPENDENCIES)) - -# The Java MUST all exist already through the transpile step. -mvn_local_deploy: - gradle -p runtimes/java publishToMavenLocal - -test_java: - # run Dafny generated tests - gradle -p runtimes/java runTests - -########################## local testing targets - -# These targets are added as a convenience for local development. -# If you experience weird behavior using these targets, -# fall back to the regular `build` or `test` targets. -# These targets MUST only be used for local testing, -# and MUST NOT be used in CI. - -# Targets to transpile single local service for convenience. -# Specify the local service to build by passing a SERVICE env var. -# Note that this does not generate identical files as `transpile_implementation_java` - -local_transpile_impl_java_single: TARGET=java -local_transpile_impl_java_single: OUT=runtimes/java/ImplementationFromDafny -local_transpile_impl_java_single: local_transpile_impl_single - cp -R runtimes/java/ImplementationFromDafny-java/* runtimes/java/src/main/dafny-generated - rm -rf runtimes/java/ImplementationFromDafny-java/ - -local_transpile_impl_net_single: TARGET=cs -local_transpile_impl_net_single: OUT=runtimes/net/ImplementationFromDafny -local_transpile_impl_net_single: local_transpile_impl_single - -local_transpile_impl_single: deps_var=SERVICE_DEPS_$(SERVICE) -local_transpile_impl_single: TRANSPILE_TARGETS=./dafny/$(SERVICE)/src/$(FILE) -local_transpile_impl_single: TRANSPILE_DEPENDENCIES= \ - $(patsubst %, -library:$(PROJECT_ROOT)/%/src/Index.dfy, $($(deps_var))) \ - $(patsubst %, -library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX)) \ - -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy -local_transpile_impl_single: transpile_implementation - -# Targets to transpile single local service for convenience. -# Specify the local service to build by passing a SERVICE env var. -# Note that this does not generate identical files as `transpile_test_java`, -# and will clobber tests generated by other services. - -local_transpile_test_java_single: TARGET=java -local_transpile_test_java_single: OUT=runtimes/java/TestsFromDafny -local_transpile_test_java_single: local_transpile_test_single - cp -R runtimes/java/TestsFromDafny-java/* runtimes/java/src/test/dafny-generated - rm -rf runtimes/java/TestsFromDafny-java -local_transpile_test_net_single: TARGET=cs -local_transpile_test_net_single: OUT=runtimes/net/tests/TestsFromDafny -local_transpile_test_net_single: local_transpile_test_single +SMITHY_DAFNY_ROOT := $(PROJECT_ROOT)/smithy-dafny +GRADLEW := ./runtimes/java/gradlew -local_transpile_test_single: TRANSPILE_TARGETS=./dafny/$(SERVICE)/test/$(FILE) -local_transpile_test_single: TRANSPILE_DEPENDENCIES= \ - $(patsubst %, -library:dafny/%/src/Index.dfy, $(PROJECT_SERVICES)) \ - $(patsubst %, -library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX)) \ - -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy -local_transpile_test_single: transpile_test +include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk diff --git a/smithy-dafny b/smithy-dafny new file mode 160000 index 000000000..16a8b6998 --- /dev/null +++ b/smithy-dafny @@ -0,0 +1 @@ +Subproject commit 16a8b699860edbffff3c3339dfccf046e3ccf213 From cc6a9aa46a3c47b948dcfd351a2376045e4aead9 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 09:55:35 -0800 Subject: [PATCH 02/31] Init submodule, include codegen workflow in relevant CI --- .github/workflows/daily_ci.yml | 6 ++++++ .github/workflows/library_dafny_verification.yml | 1 + .github/workflows/library_java_tests.yml | 1 + .github/workflows/pull.yml | 4 ++++ .github/workflows/push.yml | 4 ++++ 5 files changed, 16 insertions(+) diff --git a/.github/workflows/daily_ci.yml b/.github/workflows/daily_ci.yml index ce920fa9f..eae5b7bea 100644 --- a/.github/workflows/daily_ci.yml +++ b/.github/workflows/daily_ci.yml @@ -6,6 +6,12 @@ on: - cron: "00 15 * * 1-5" jobs: + daily-ci-codegen: + # Don't run the cron builds on forks + if: github.event_name != 'schedule' || github.repository_owner == 'aws' + uses: ./.github/workflows/library_dafny_codegen.yml + with: + dafny: '4.2.0' daily-ci-verification: # Don't run the cron builds on forks if: github.event_name != 'schedule' || github.repository_owner == 'aws' diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml index 645a6b1d9..b6d480fe5 100644 --- a/.github/workflows/library_dafny_verification.yml +++ b/.github/workflows/library_dafny_verification.yml @@ -36,6 +36,7 @@ jobs: run: | git submodule update --init libraries git submodule update --init --recursive mpl + git submodule update --init smithy-dafny - name: Setup Dafny uses: dafny-lang/setup-dafny-action@v1.7.0 diff --git a/.github/workflows/library_java_tests.yml b/.github/workflows/library_java_tests.yml index ab55a6a7b..d13f984ab 100644 --- a/.github/workflows/library_java_tests.yml +++ b/.github/workflows/library_java_tests.yml @@ -41,6 +41,7 @@ jobs: run: | git submodule update --init libraries git submodule update --init --recursive mpl + git submodule update --init smithy-dafny - name: Configure AWS Credentials uses: aws-actions/configure-aws-credentials@v2 diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index 1133bf1de..c2ef7bbdc 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -5,6 +5,10 @@ on: pull_request: jobs: + pr-ci-codegen: + uses: ./.github/workflows/library_codegen.yml + with: + dafny: '4.2.0' pr-ci-verification: uses: ./.github/workflows/library_dafny_verification.yml with: diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 3261cb06c..50ebc0b2b 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -7,6 +7,10 @@ on: - main jobs: + pr-ci-codegen: + uses: ./.github/workflows/library_codegen.yml + with: + dafny: '4.2.0' push-ci-verification: uses: ./.github/workflows/library_dafny_verification.yml with: From 1edaf938d0bce37dfaa1eddd96e82c14c2d82667 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 10:02:01 -0800 Subject: [PATCH 03/31] shell: bash --- .github/actions/polymorph_codegen/action.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index 9777a2137..e22ae1fe7 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -72,11 +72,13 @@ runs: - name: Update MPL submodule locally if: inputs.update-and-regenerate-mpl == 'true' + shell: bash run: | git submodule update --init --recursive --remote --merge mpl - name: Don't regenerate dependencies if: inputs.update-and-regenerate-mpl != 'true' + shell: bash run: | echo "POLYMORPH_DEPENDENCIES=" >> $GITHUB_ENV From bb550a63033f766257e6d32f2779beccc199b0a2 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 10:27:18 -0800 Subject: [PATCH 04/31] Add project.properties file --- .github/actions/polymorph_codegen/action.yml | 9 --------- AwsEncryptionSDK/project.properties | 3 +++ AwsEncryptionSDK/runtimes/java/build.gradle.kts | 11 ++++++++++- 3 files changed, 13 insertions(+), 10 deletions(-) create mode 100644 AwsEncryptionSDK/project.properties diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index e22ae1fe7..485d67a18 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -61,15 +61,6 @@ outputs: 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: Update MPL submodule locally if: inputs.update-and-regenerate-mpl == 'true' shell: bash diff --git a/AwsEncryptionSDK/project.properties b/AwsEncryptionSDK/project.properties new file mode 100644 index 000000000..dd7eb37b9 --- /dev/null +++ b/AwsEncryptionSDK/project.properties @@ -0,0 +1,3 @@ +# This file stores the top level dafny version information. +# All elements of the project need to agree on this version. +dafnyVersion=4.2.0 diff --git a/AwsEncryptionSDK/runtimes/java/build.gradle.kts b/AwsEncryptionSDK/runtimes/java/build.gradle.kts index d56f6b01c..86db09935 100644 --- a/AwsEncryptionSDK/runtimes/java/build.gradle.kts +++ b/AwsEncryptionSDK/runtimes/java/build.gradle.kts @@ -6,18 +6,27 @@ * User Manual available at https://docs.gradle.org/8.1.1/userguide/building_java_projects.html */ +import java.io.File +import java.io.FileInputStream +import java.util.Properties + plugins { // Apply the java-library plugin for API and implementation separation. `java-library` } +var props = Properties().apply { + load(FileInputStream(File(rootProject.rootDir, "../../project.properties"))) +} +var dafnyVersion = props.getProperty("dafnyVersion") + repositories { // Use Maven Central for resolving dependencies. mavenCentral() } dependencies { - implementation("org.dafny:DafnyRuntime:4.2.0") + implementation("org.dafny:DafnyRuntime:${dafnyVersion}") implementation("software.amazon.smithy.dafny:conversion:0.1") implementation("software.amazon.cryptography:aws-cryptographic-material-providers:1.0.1") From e9b89dfea830d0ef9d5ad39f3df269e0786a1bbb Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 10:42:11 -0800 Subject: [PATCH 05/31] Fix library list --- .github/workflows/library_codegen.yml | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/.github/workflows/library_codegen.yml b/.github/workflows/library_codegen.yml index 08c5fbd51..ec51ead7b 100644 --- a/.github/workflows/library_codegen.yml +++ b/.github/workflows/library_codegen.yml @@ -15,12 +15,7 @@ jobs: matrix: library: [ - TestVectorsAwsCryptographicMaterialProviders, - AwsCryptographyPrimitives, - ComAmazonawsKms, - ComAmazonawsDynamodb, - AwsCryptographicMaterialProviders, - StandardLibrary, + AwsEncryptionSDK, ] # Note dotnet is only used for formatting generated code # in this workflow From 7fb27cc0201d95dc2194ac082865dfaa41364ded Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 11:05:07 -0800 Subject: [PATCH 06/31] Another missing submodule init --- .github/workflows/library_codegen.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/library_codegen.yml b/.github/workflows/library_codegen.yml index ec51ead7b..9780c1348 100644 --- a/.github/workflows/library_codegen.yml +++ b/.github/workflows/library_codegen.yml @@ -37,6 +37,7 @@ jobs: # 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 --recursive mpl - run: git submodule update --init smithy-dafny # Only used to format generated code From 6928635813056103818ab2e8f342015e655e5255 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 11:27:41 -0800 Subject: [PATCH 07/31] Fix skipping dependencies --- .github/actions/polymorph_codegen/action.yml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index 485d67a18..0715d9cd2 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -61,17 +61,17 @@ outputs: runs: using: "composite" steps: - - name: Update MPL submodule locally + - name: Update MPL submodule locally if requested if: inputs.update-and-regenerate-mpl == 'true' shell: bash run: | git submodule update --init --recursive --remote --merge mpl - - name: Don't regenerate dependencies + - name: Don't regenerate dependencies unless requested if: inputs.update-and-regenerate-mpl != 'true' shell: bash run: | - echo "POLYMORPH_DEPENDENCIES=" >> $GITHUB_ENV + echo "SKIP_DEPENDENCIES=POLYMORPH_DEPENDENCIES=" >> $GITHUB_ENV - name: Regenerate Dafny code using smithy-dafny # Unfortunately Dafny codegen doesn't work on Windows: @@ -80,7 +80,7 @@ runs: working-directory: ./${{ inputs.library }} shell: bash run: | - make polymorph_dafny + make polymorph_dafny $SKIP_DEPENDENCIES - name: Regenerate Java code using smithy-dafny # npx seems to be unavailable on Windows GHA runners, @@ -92,13 +92,13 @@ runs: # so prettier is a necessary dependency. run: | make -C .. setup_prettier - make polymorph_java + make polymorph_java $SKIP_DEPENDENCIES - name: Regenerate .NET code using smithy-dafny working-directory: ./${{ inputs.library }} shell: bash run: | - make polymorph_dotnet + make polymorph_dotnet $SKIP_DEPENDENCIES - name: Check regenerated code against commited code # Composite action inputs seem to not actually support booleans properly for some reason From 59523988a60bf20f57a7965ab694bd0760327340 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 11:53:29 -0800 Subject: [PATCH 08/31] Use step outputs instead --- .github/actions/polymorph_codegen/action.yml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index 0715d9cd2..881d6100c 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -68,10 +68,10 @@ runs: git submodule update --init --recursive --remote --merge mpl - name: Don't regenerate dependencies unless requested - if: inputs.update-and-regenerate-mpl != 'true' + id: dependencies shell: bash run: | - echo "SKIP_DEPENDENCIES=POLYMORPH_DEPENDENCIES=" >> $GITHUB_ENV + echo "POLYMORPH_DEPENDENCIES=${{ inputs.update-and-regenerate-mpl != 'true' && 'POLYMORPH_DEPENDENCIES=' || '' }}" >> $GITHUB_OUTPUT - name: Regenerate Dafny code using smithy-dafny # Unfortunately Dafny codegen doesn't work on Windows: @@ -80,7 +80,7 @@ runs: working-directory: ./${{ inputs.library }} shell: bash run: | - make polymorph_dafny $SKIP_DEPENDENCIES + make polymorph_dafny ${{ steps.dependencies.outputs.POLYMORPH_DEPENDENCIES }} - name: Regenerate Java code using smithy-dafny # npx seems to be unavailable on Windows GHA runners, @@ -92,13 +92,13 @@ runs: # so prettier is a necessary dependency. run: | make -C .. setup_prettier - make polymorph_java $SKIP_DEPENDENCIES + make polymorph_java ${{ steps.dependencies.outputs.POLYMORPH_DEPENDENCIES }} - name: Regenerate .NET code using smithy-dafny working-directory: ./${{ inputs.library }} shell: bash run: | - make polymorph_dotnet $SKIP_DEPENDENCIES + make polymorph_dotnet ${{ steps.dependencies.outputs.POLYMORPH_DEPENDENCIES }} - name: Check regenerated code against commited code # Composite action inputs seem to not actually support booleans properly for some reason From 9230d0d78d64112d6b8810b4fff9f4b33298ae4a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 11:56:58 -0800 Subject: [PATCH 09/31] Correct variable name --- .github/actions/polymorph_codegen/action.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index 881d6100c..38f9968d0 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -71,7 +71,7 @@ runs: id: dependencies shell: bash run: | - echo "POLYMORPH_DEPENDENCIES=${{ inputs.update-and-regenerate-mpl != 'true' && 'POLYMORPH_DEPENDENCIES=' || '' }}" >> $GITHUB_OUTPUT + echo "PROJECT_DEPENDENCIES=${{ inputs.update-and-regenerate-mpl != 'true' && 'PROJECT_DEPENDENCIES=' || '' }}" >> $GITHUB_OUTPUT - name: Regenerate Dafny code using smithy-dafny # Unfortunately Dafny codegen doesn't work on Windows: @@ -80,7 +80,7 @@ runs: working-directory: ./${{ inputs.library }} shell: bash run: | - make polymorph_dafny ${{ steps.dependencies.outputs.POLYMORPH_DEPENDENCIES }} + make polymorph_dafny ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} - name: Regenerate Java code using smithy-dafny # npx seems to be unavailable on Windows GHA runners, @@ -92,13 +92,13 @@ runs: # so prettier is a necessary dependency. run: | make -C .. setup_prettier - make polymorph_java ${{ steps.dependencies.outputs.POLYMORPH_DEPENDENCIES }} + make polymorph_java ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} - name: Regenerate .NET code using smithy-dafny working-directory: ./${{ inputs.library }} shell: bash run: | - make polymorph_dotnet ${{ steps.dependencies.outputs.POLYMORPH_DEPENDENCIES }} + make polymorph_dotnet ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} - name: Check regenerated code against commited code # Composite action inputs seem to not actually support booleans properly for some reason From 89258ff31dd56096eb965c0263f337167163d8ad Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 11:59:31 -0800 Subject: [PATCH 10/31] Prettier path --- .github/actions/polymorph_codegen/action.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index 38f9968d0..2319002e0 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -91,7 +91,7 @@ runs: # smithy-dafny also formats generated code itself now, # so prettier is a necessary dependency. run: | - make -C .. setup_prettier + make setup_prettier make polymorph_java ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} - name: Regenerate .NET code using smithy-dafny From 9ae8669101771bf480a0ef65cc8b5946abf59fb4 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 13:08:36 -0800 Subject: [PATCH 11/31] regenerate Dafny, Java and C# code --- .../AwsCryptographyEncryptionSdkTypes.dfy | 31 +- .../cryptography/encryptionsdk/ESDK.java | 41 +- .../cryptography/encryptionsdk/ToDafny.java | 238 ++++- .../cryptography/encryptionsdk/ToNative.java | 179 +++- .../model/AwsEncryptionSdkConfig.java | 46 +- .../model/AwsEncryptionSdkException.java | 11 +- .../model/CollectionOfErrors.java | 5 +- .../encryptionsdk/model/DecryptInput.java | 18 +- .../encryptionsdk/model/DecryptOutput.java | 23 +- .../encryptionsdk/model/EncryptInput.java | 26 +- .../encryptionsdk/model/EncryptOutput.java | 23 +- .../model/NetV4_0_0_RetryPolicy.java | 23 + .../encryptionsdk/model/OpaqueError.java | 9 +- .../AwsEncryptionSdkConfig.cs | 70 +- .../AwsEncryptionSdkException.cs | 13 +- .../AwsEncryptionSdk/CollectionOfErrors.cs | 17 +- .../AwsEncryptionSdk/DecryptInput.cs | 88 +- .../AwsEncryptionSdk/DecryptOutput.cs | 74 +- .../net/Generated/AwsEncryptionSdk/ESDK.cs | 71 +- .../AwsEncryptionSdk/EncryptInput.cs | 124 ++- .../AwsEncryptionSdk/EncryptOutput.cs | 74 +- .../AwsEncryptionSdk/NetV4_0_0_RetryPolicy.cs | 24 +- .../Generated/AwsEncryptionSdk/OpaqueError.cs | 17 +- .../AwsEncryptionSdk/TypeConversion.cs | 991 ++++-------------- 24 files changed, 1062 insertions(+), 1174 deletions(-) create mode 100644 AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/NetV4_0_0_RetryPolicy.java diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/AwsCryptographyEncryptionSdkTypes.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/AwsCryptographyEncryptionSdkTypes.dfy index 2cf7013f2..ca650be5a 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/AwsCryptographyEncryptionSdkTypes.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/AwsCryptographyEncryptionSdkTypes.dfy @@ -103,9 +103,9 @@ module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny.types" } datatype AwsEncryptionSdkConfig = | AwsEncryptionSdkConfig ( - nameonly commitmentPolicy: Option , - nameonly maxEncryptedDataKeys: Option , - nameonly netV4_0_0_RetryPolicy: Option + nameonly commitmentPolicy: Option := Option.None , + nameonly maxEncryptedDataKeys: Option := Option.None , + nameonly netV4_0_0_RetryPolicy: Option := Option.None ) type CountingNumbers = x: int64 | IsValid_CountingNumbers(x) witness * predicate method IsValid_CountingNumbers(x: int64) { @@ -113,9 +113,9 @@ module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny.types" } datatype DecryptInput = | DecryptInput ( nameonly ciphertext: seq , - nameonly materialsManager: Option , - nameonly keyring: Option , - nameonly encryptionContext: Option + nameonly materialsManager: Option := Option.None , + nameonly keyring: Option := Option.None , + nameonly encryptionContext: Option := Option.None ) datatype DecryptOutput = | DecryptOutput ( nameonly plaintext: seq , @@ -124,11 +124,11 @@ module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny.types" ) datatype EncryptInput = | EncryptInput ( nameonly plaintext: seq , - nameonly encryptionContext: Option , - nameonly materialsManager: Option , - nameonly keyring: Option , - nameonly algorithmSuiteId: Option , - nameonly frameLength: Option + nameonly encryptionContext: Option := Option.None , + nameonly materialsManager: Option := Option.None , + nameonly keyring: Option := Option.None , + nameonly algorithmSuiteId: Option := Option.None , + nameonly frameLength: Option := Option.None ) datatype EncryptOutput = | EncryptOutput ( nameonly ciphertext: seq , @@ -187,13 +187,20 @@ abstract module AbstractAwsCryptographyEncryptionSdkService import Operations : AbstractAwsCryptographyEncryptionSdkOperations function method DefaultAwsEncryptionSdkConfig(): AwsEncryptionSdkConfig method ESDK(config: AwsEncryptionSdkConfig := DefaultAwsEncryptionSdkConfig()) - returns (res: Result) + returns (res: Result) ensures res.Success? ==> && fresh(res.value) && fresh(res.value.Modifies) && fresh(res.value.History) && res.value.ValidState() + // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals + function method CreateSuccessOfClient(client: IAwsEncryptionSdkClient): Result { + Success(client) + } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals + function method CreateFailureOfError(error: Error): Result { + Failure(error) + } class ESDKClient extends IAwsEncryptionSdkClient { constructor(config: Operations.InternalConfig) diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/ESDK.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/ESDK.java index 273ba8a64..25a7411b6 100644 --- a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/ESDK.java +++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/ESDK.java @@ -6,7 +6,6 @@ import Wrappers_Compile.Result; import java.lang.IllegalArgumentException; import java.util.Objects; -import software.amazon.cryptography.encryptionsdk.internaldafny.ESDKClient; import software.amazon.cryptography.encryptionsdk.internaldafny.__default; import software.amazon.cryptography.encryptionsdk.internaldafny.types.Error; import software.amazon.cryptography.encryptionsdk.internaldafny.types.IAwsEncryptionSdkClient; @@ -17,12 +16,14 @@ import software.amazon.cryptography.encryptionsdk.model.EncryptOutput; public class ESDK { + private final IAwsEncryptionSdkClient _impl; protected ESDK(BuilderImpl builder) { AwsEncryptionSdkConfig input = builder.AwsEncryptionSdkConfig(); - software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig dafnyValue = ToDafny.AwsEncryptionSdkConfig(input); - Result result = __default.ESDK(dafnyValue); + software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig dafnyValue = + ToDafny.AwsEncryptionSdkConfig(input); + Result result = __default.ESDK(dafnyValue); if (result.is_Failure()) { throw ToNative.Error(result.dtor_error()); } @@ -38,8 +39,12 @@ public static Builder builder() { } public DecryptOutput Decrypt(DecryptInput input) { - software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptInput dafnyValue = ToDafny.DecryptInput(input); - Result result = this._impl.Decrypt(dafnyValue); + software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptInput dafnyValue = + ToDafny.DecryptInput(input); + Result< + software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptOutput, + Error + > result = this._impl.Decrypt(dafnyValue); if (result.is_Failure()) { throw ToNative.Error(result.dtor_error()); } @@ -47,8 +52,12 @@ public DecryptOutput Decrypt(DecryptInput input) { } public EncryptOutput Encrypt(EncryptInput input) { - software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptInput dafnyValue = ToDafny.EncryptInput(input); - Result result = this._impl.Encrypt(dafnyValue); + software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptInput dafnyValue = + ToDafny.EncryptInput(input); + Result< + software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput, + Error + > result = this._impl.Encrypt(dafnyValue); if (result.is_Failure()) { throw ToNative.Error(result.dtor_error()); } @@ -60,7 +69,9 @@ protected IAwsEncryptionSdkClient impl() { } public interface Builder { - Builder AwsEncryptionSdkConfig(AwsEncryptionSdkConfig AwsEncryptionSdkConfig); + Builder AwsEncryptionSdkConfig( + AwsEncryptionSdkConfig AwsEncryptionSdkConfig + ); AwsEncryptionSdkConfig AwsEncryptionSdkConfig(); @@ -68,12 +79,14 @@ public interface Builder { } static class BuilderImpl implements Builder { + protected AwsEncryptionSdkConfig AwsEncryptionSdkConfig; - protected BuilderImpl() { - } + protected BuilderImpl() {} - public Builder AwsEncryptionSdkConfig(AwsEncryptionSdkConfig AwsEncryptionSdkConfig) { + public Builder AwsEncryptionSdkConfig( + AwsEncryptionSdkConfig AwsEncryptionSdkConfig + ) { this.AwsEncryptionSdkConfig = AwsEncryptionSdkConfig; return this; } @@ -83,8 +96,10 @@ public AwsEncryptionSdkConfig AwsEncryptionSdkConfig() { } public ESDK build() { - if (Objects.isNull(this.AwsEncryptionSdkConfig())) { - throw new IllegalArgumentException("Missing value for required field `AwsEncryptionSdkConfig`"); + if (Objects.isNull(this.AwsEncryptionSdkConfig())) { + throw new IllegalArgumentException( + "Missing value for required field `AwsEncryptionSdkConfig`" + ); } return new ESDK(this); } diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/ToDafny.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/ToDafny.java index 7339bf28d..537dafc94 100644 --- a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/ToDafny.java +++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/ToDafny.java @@ -19,8 +19,10 @@ import software.amazon.cryptography.encryptionsdk.internaldafny.types.Error; import software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException; import software.amazon.cryptography.encryptionsdk.internaldafny.types.IAwsEncryptionSdkClient; +import software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy; import software.amazon.cryptography.encryptionsdk.model.AwsEncryptionSdkException; import software.amazon.cryptography.encryptionsdk.model.CollectionOfErrors; +import software.amazon.cryptography.encryptionsdk.model.NetV4_0_0_RetryPolicy; import software.amazon.cryptography.encryptionsdk.model.OpaqueError; import software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId; import software.amazon.cryptography.materialproviders.internaldafny.types.ESDKCommitmentPolicy; @@ -28,6 +30,7 @@ import software.amazon.cryptography.materialproviders.internaldafny.types.IKeyring; public class ToDafny { + public static Error Error(RuntimeException nativeValue) { if (nativeValue instanceof AwsEncryptionSdkException) { return ToDafny.Error((AwsEncryptionSdkException) nativeValue); @@ -46,101 +49,244 @@ public static Error Error(OpaqueError nativeValue) { } public static Error Error(CollectionOfErrors nativeValue) { - DafnySequence list = software.amazon.smithy.dafny.conversion.ToDafny.Aggregate.GenericToSequence( - nativeValue.list(), - ToDafny::Error, - Error._typeDescriptor()); - DafnySequence message = software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(nativeValue.getMessage()); + DafnySequence list = + software.amazon.smithy.dafny.conversion.ToDafny.Aggregate.GenericToSequence( + nativeValue.list(), + ToDafny::Error, + Error._typeDescriptor() + ); + DafnySequence message = + software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( + nativeValue.getMessage() + ); return Error.create_CollectionOfErrors(list, message); } public static AwsEncryptionSdkConfig AwsEncryptionSdkConfig( - software.amazon.cryptography.encryptionsdk.model.AwsEncryptionSdkConfig nativeValue) { + software.amazon.cryptography.encryptionsdk.model.AwsEncryptionSdkConfig nativeValue + ) { Option commitmentPolicy; - commitmentPolicy = Objects.nonNull(nativeValue.commitmentPolicy()) ? - Option.create_Some(software.amazon.cryptography.materialproviders.ToDafny.ESDKCommitmentPolicy(nativeValue.commitmentPolicy())) + commitmentPolicy = + Objects.nonNull(nativeValue.commitmentPolicy()) + ? Option.create_Some( + software.amazon.cryptography.materialproviders.ToDafny.ESDKCommitmentPolicy( + nativeValue.commitmentPolicy() + ) + ) : Option.create_None(); Option maxEncryptedDataKeys; - maxEncryptedDataKeys = Objects.nonNull(nativeValue.maxEncryptedDataKeys()) ? - Option.create_Some((nativeValue.maxEncryptedDataKeys())) + maxEncryptedDataKeys = + Objects.nonNull(nativeValue.maxEncryptedDataKeys()) + ? Option.create_Some((nativeValue.maxEncryptedDataKeys())) + : Option.create_None(); + Option netV4_0_0_RetryPolicy; + netV4_0_0_RetryPolicy = + Objects.nonNull(nativeValue.netV4_0_0_RetryPolicy()) + ? Option.create_Some( + ToDafny.NetV4_0_0_RetryPolicy(nativeValue.netV4_0_0_RetryPolicy()) + ) : Option.create_None(); - return new AwsEncryptionSdkConfig(commitmentPolicy, maxEncryptedDataKeys); + return new AwsEncryptionSdkConfig( + commitmentPolicy, + maxEncryptedDataKeys, + netV4_0_0_RetryPolicy + ); } public static DecryptInput DecryptInput( - software.amazon.cryptography.encryptionsdk.model.DecryptInput nativeValue) { + software.amazon.cryptography.encryptionsdk.model.DecryptInput nativeValue + ) { DafnySequence ciphertext; - ciphertext = software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence(nativeValue.ciphertext()); + ciphertext = + software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence( + nativeValue.ciphertext() + ); Option materialsManager; - materialsManager = Objects.nonNull(nativeValue.materialsManager()) ? - Option.create_Some(software.amazon.cryptography.materialproviders.ToDafny.CryptographicMaterialsManager(nativeValue.materialsManager())) + materialsManager = + Objects.nonNull(nativeValue.materialsManager()) + ? Option.create_Some( + software.amazon.cryptography.materialproviders.ToDafny.CryptographicMaterialsManager( + nativeValue.materialsManager() + ) + ) : Option.create_None(); Option keyring; - keyring = Objects.nonNull(nativeValue.keyring()) ? - Option.create_Some(software.amazon.cryptography.materialproviders.ToDafny.Keyring(nativeValue.keyring())) + keyring = + Objects.nonNull(nativeValue.keyring()) + ? Option.create_Some( + software.amazon.cryptography.materialproviders.ToDafny.Keyring( + nativeValue.keyring() + ) + ) : Option.create_None(); - Option, ? extends DafnySequence>> encryptionContext; - encryptionContext = (Objects.nonNull(nativeValue.encryptionContext()) && nativeValue.encryptionContext().size() > 0) ? - Option.create_Some(software.amazon.cryptography.materialproviders.ToDafny.EncryptionContext(nativeValue.encryptionContext())) + Option< + DafnyMap< + ? extends DafnySequence, + ? extends DafnySequence + > + > encryptionContext; + encryptionContext = + (Objects.nonNull(nativeValue.encryptionContext()) && + nativeValue.encryptionContext().size() > 0) + ? Option.create_Some( + software.amazon.cryptography.materialproviders.ToDafny.EncryptionContext( + nativeValue.encryptionContext() + ) + ) : Option.create_None(); - return new DecryptInput(ciphertext, materialsManager, keyring, encryptionContext); + return new DecryptInput( + ciphertext, + materialsManager, + keyring, + encryptionContext + ); } public static DecryptOutput DecryptOutput( - software.amazon.cryptography.encryptionsdk.model.DecryptOutput nativeValue) { + software.amazon.cryptography.encryptionsdk.model.DecryptOutput nativeValue + ) { DafnySequence plaintext; - plaintext = software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence(nativeValue.plaintext()); - DafnyMap, ? extends DafnySequence> encryptionContext; - encryptionContext = software.amazon.cryptography.materialproviders.ToDafny.EncryptionContext(nativeValue.encryptionContext()); + plaintext = + software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence( + nativeValue.plaintext() + ); + DafnyMap< + ? extends DafnySequence, + ? extends DafnySequence + > encryptionContext; + encryptionContext = + software.amazon.cryptography.materialproviders.ToDafny.EncryptionContext( + nativeValue.encryptionContext() + ); ESDKAlgorithmSuiteId algorithmSuiteId; - algorithmSuiteId = software.amazon.cryptography.materialproviders.ToDafny.ESDKAlgorithmSuiteId(nativeValue.algorithmSuiteId()); + algorithmSuiteId = + software.amazon.cryptography.materialproviders.ToDafny.ESDKAlgorithmSuiteId( + nativeValue.algorithmSuiteId() + ); return new DecryptOutput(plaintext, encryptionContext, algorithmSuiteId); } public static EncryptInput EncryptInput( - software.amazon.cryptography.encryptionsdk.model.EncryptInput nativeValue) { + software.amazon.cryptography.encryptionsdk.model.EncryptInput nativeValue + ) { DafnySequence plaintext; - plaintext = software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence(nativeValue.plaintext()); - Option, ? extends DafnySequence>> encryptionContext; - encryptionContext = (Objects.nonNull(nativeValue.encryptionContext()) && nativeValue.encryptionContext().size() > 0) ? - Option.create_Some(software.amazon.cryptography.materialproviders.ToDafny.EncryptionContext(nativeValue.encryptionContext())) + plaintext = + software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence( + nativeValue.plaintext() + ); + Option< + DafnyMap< + ? extends DafnySequence, + ? extends DafnySequence + > + > encryptionContext; + encryptionContext = + (Objects.nonNull(nativeValue.encryptionContext()) && + nativeValue.encryptionContext().size() > 0) + ? Option.create_Some( + software.amazon.cryptography.materialproviders.ToDafny.EncryptionContext( + nativeValue.encryptionContext() + ) + ) : Option.create_None(); Option materialsManager; - materialsManager = Objects.nonNull(nativeValue.materialsManager()) ? - Option.create_Some(software.amazon.cryptography.materialproviders.ToDafny.CryptographicMaterialsManager(nativeValue.materialsManager())) + materialsManager = + Objects.nonNull(nativeValue.materialsManager()) + ? Option.create_Some( + software.amazon.cryptography.materialproviders.ToDafny.CryptographicMaterialsManager( + nativeValue.materialsManager() + ) + ) : Option.create_None(); Option keyring; - keyring = Objects.nonNull(nativeValue.keyring()) ? - Option.create_Some(software.amazon.cryptography.materialproviders.ToDafny.Keyring(nativeValue.keyring())) + keyring = + Objects.nonNull(nativeValue.keyring()) + ? Option.create_Some( + software.amazon.cryptography.materialproviders.ToDafny.Keyring( + nativeValue.keyring() + ) + ) : Option.create_None(); Option algorithmSuiteId; - algorithmSuiteId = Objects.nonNull(nativeValue.algorithmSuiteId()) ? - Option.create_Some(software.amazon.cryptography.materialproviders.ToDafny.ESDKAlgorithmSuiteId(nativeValue.algorithmSuiteId())) + algorithmSuiteId = + Objects.nonNull(nativeValue.algorithmSuiteId()) + ? Option.create_Some( + software.amazon.cryptography.materialproviders.ToDafny.ESDKAlgorithmSuiteId( + nativeValue.algorithmSuiteId() + ) + ) : Option.create_None(); Option frameLength; - frameLength = Objects.nonNull(nativeValue.frameLength()) ? - Option.create_Some((nativeValue.frameLength())) + frameLength = + Objects.nonNull(nativeValue.frameLength()) + ? Option.create_Some((nativeValue.frameLength())) : Option.create_None(); - return new EncryptInput(plaintext, encryptionContext, materialsManager, keyring, algorithmSuiteId, frameLength); + return new EncryptInput( + plaintext, + encryptionContext, + materialsManager, + keyring, + algorithmSuiteId, + frameLength + ); } public static EncryptOutput EncryptOutput( - software.amazon.cryptography.encryptionsdk.model.EncryptOutput nativeValue) { + software.amazon.cryptography.encryptionsdk.model.EncryptOutput nativeValue + ) { DafnySequence ciphertext; - ciphertext = software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence(nativeValue.ciphertext()); - DafnyMap, ? extends DafnySequence> encryptionContext; - encryptionContext = software.amazon.cryptography.materialproviders.ToDafny.EncryptionContext(nativeValue.encryptionContext()); + ciphertext = + software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence( + nativeValue.ciphertext() + ); + DafnyMap< + ? extends DafnySequence, + ? extends DafnySequence + > encryptionContext; + encryptionContext = + software.amazon.cryptography.materialproviders.ToDafny.EncryptionContext( + nativeValue.encryptionContext() + ); ESDKAlgorithmSuiteId algorithmSuiteId; - algorithmSuiteId = software.amazon.cryptography.materialproviders.ToDafny.ESDKAlgorithmSuiteId(nativeValue.algorithmSuiteId()); + algorithmSuiteId = + software.amazon.cryptography.materialproviders.ToDafny.ESDKAlgorithmSuiteId( + nativeValue.algorithmSuiteId() + ); return new EncryptOutput(ciphertext, encryptionContext, algorithmSuiteId); } public static Error Error(AwsEncryptionSdkException nativeValue) { DafnySequence message; - message = software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(nativeValue.message()); + message = + software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence( + nativeValue.message() + ); return new Error_AwsEncryptionSdkException(message); } + public static NetV4__0__0__RetryPolicy NetV4_0_0_RetryPolicy( + NetV4_0_0_RetryPolicy nativeValue + ) { + switch (nativeValue) { + case FORBID_RETRY: + { + return NetV4__0__0__RetryPolicy.create_FORBID__RETRY(); + } + case ALLOW_RETRY: + { + return NetV4__0__0__RetryPolicy.create_ALLOW__RETRY(); + } + default: + { + throw new RuntimeException( + "Cannot convert " + + nativeValue + + " to software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy." + ); + } + } + } + public static IAwsEncryptionSdkClient AwsEncryptionSdk(ESDK nativeValue) { return nativeValue.impl(); } diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/ToNative.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/ToNative.java index 5b1ff3d27..674cd9dad 100644 --- a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/ToNative.java +++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/ToNative.java @@ -3,12 +3,14 @@ // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. package software.amazon.cryptography.encryptionsdk; +import java.lang.IllegalArgumentException; import java.lang.RuntimeException; import software.amazon.cryptography.encryptionsdk.internaldafny.types.Error; import software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException; import software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_CollectionOfErrors; import software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_Opaque; import software.amazon.cryptography.encryptionsdk.internaldafny.types.IAwsEncryptionSdkClient; +import software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy; import software.amazon.cryptography.encryptionsdk.model.AwsEncryptionSdkConfig; import software.amazon.cryptography.encryptionsdk.model.AwsEncryptionSdkException; import software.amazon.cryptography.encryptionsdk.model.CollectionOfErrors; @@ -16,9 +18,11 @@ import software.amazon.cryptography.encryptionsdk.model.DecryptOutput; import software.amazon.cryptography.encryptionsdk.model.EncryptInput; import software.amazon.cryptography.encryptionsdk.model.EncryptOutput; +import software.amazon.cryptography.encryptionsdk.model.NetV4_0_0_RetryPolicy; import software.amazon.cryptography.encryptionsdk.model.OpaqueError; public class ToNative { + public static OpaqueError Error(Error_Opaque dafnyValue) { OpaqueError.Builder nativeBuilder = OpaqueError.builder(); nativeBuilder.obj(dafnyValue.dtor_obj()); @@ -28,16 +32,29 @@ public static OpaqueError Error(Error_Opaque dafnyValue) { public static CollectionOfErrors Error(Error_CollectionOfErrors dafnyValue) { CollectionOfErrors.Builder nativeBuilder = CollectionOfErrors.builder(); nativeBuilder.list( - software.amazon.smithy.dafny.conversion.ToNative.Aggregate.GenericToList( - dafnyValue.dtor_list(), - ToNative::Error)); - nativeBuilder.message(software.amazon.smithy.dafny.conversion.ToNative.Simple.String(dafnyValue.dtor_message())); + software.amazon.smithy.dafny.conversion.ToNative.Aggregate.GenericToList( + dafnyValue.dtor_list(), + ToNative::Error + ) + ); + nativeBuilder.message( + software.amazon.smithy.dafny.conversion.ToNative.Simple.String( + dafnyValue.dtor_message() + ) + ); return nativeBuilder.build(); } - public static AwsEncryptionSdkException Error(Error_AwsEncryptionSdkException dafnyValue) { - AwsEncryptionSdkException.Builder nativeBuilder = AwsEncryptionSdkException.builder(); - nativeBuilder.message(software.amazon.smithy.dafny.conversion.ToNative.Simple.String(dafnyValue.dtor_message())); + public static AwsEncryptionSdkException Error( + Error_AwsEncryptionSdkException dafnyValue + ) { + AwsEncryptionSdkException.Builder nativeBuilder = + AwsEncryptionSdkException.builder(); + nativeBuilder.message( + software.amazon.smithy.dafny.conversion.ToNative.Simple.String( + dafnyValue.dtor_message() + ) + ); return nativeBuilder.build(); } @@ -52,10 +69,14 @@ public static RuntimeException Error(Error dafnyValue) { return ToNative.Error((Error_CollectionOfErrors) dafnyValue); } if (dafnyValue.is_AwsCryptographyPrimitives()) { - return software.amazon.cryptography.primitives.ToNative.Error(dafnyValue.dtor_AwsCryptographyPrimitives()); + return software.amazon.cryptography.primitives.ToNative.Error( + dafnyValue.dtor_AwsCryptographyPrimitives() + ); } if (dafnyValue.is_AwsCryptographyMaterialProviders()) { - return software.amazon.cryptography.materialproviders.ToNative.Error(dafnyValue.dtor_AwsCryptographyMaterialProviders()); + return software.amazon.cryptography.materialproviders.ToNative.Error( + dafnyValue.dtor_AwsCryptographyMaterialProviders() + ); } OpaqueError.Builder nativeBuilder = OpaqueError.builder(); nativeBuilder.obj(dafnyValue); @@ -63,57 +84,123 @@ public static RuntimeException Error(Error dafnyValue) { } public static AwsEncryptionSdkConfig AwsEncryptionSdkConfig( - software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig dafnyValue) { - AwsEncryptionSdkConfig.Builder nativeBuilder = AwsEncryptionSdkConfig.builder(); + software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig dafnyValue + ) { + AwsEncryptionSdkConfig.Builder nativeBuilder = + AwsEncryptionSdkConfig.builder(); if (dafnyValue.dtor_commitmentPolicy().is_Some()) { - nativeBuilder.commitmentPolicy(software.amazon.cryptography.materialproviders.ToNative.ESDKCommitmentPolicy(dafnyValue.dtor_commitmentPolicy().dtor_value())); + nativeBuilder.commitmentPolicy( + software.amazon.cryptography.materialproviders.ToNative.ESDKCommitmentPolicy( + dafnyValue.dtor_commitmentPolicy().dtor_value() + ) + ); } if (dafnyValue.dtor_maxEncryptedDataKeys().is_Some()) { - nativeBuilder.maxEncryptedDataKeys((dafnyValue.dtor_maxEncryptedDataKeys().dtor_value())); + nativeBuilder.maxEncryptedDataKeys( + (dafnyValue.dtor_maxEncryptedDataKeys().dtor_value()) + ); + } + if (dafnyValue.dtor_netV4__0__0__RetryPolicy().is_Some()) { + nativeBuilder.netV4_0_0_RetryPolicy( + ToNative.NetV4_0_0_RetryPolicy( + dafnyValue.dtor_netV4__0__0__RetryPolicy().dtor_value() + ) + ); } return nativeBuilder.build(); } public static DecryptInput DecryptInput( - software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptInput dafnyValue) { + software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptInput dafnyValue + ) { DecryptInput.Builder nativeBuilder = DecryptInput.builder(); - nativeBuilder.ciphertext(software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer(dafnyValue.dtor_ciphertext())); + nativeBuilder.ciphertext( + software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer( + dafnyValue.dtor_ciphertext() + ) + ); if (dafnyValue.dtor_materialsManager().is_Some()) { - nativeBuilder.materialsManager(software.amazon.cryptography.materialproviders.ToNative.CryptographicMaterialsManager(dafnyValue.dtor_materialsManager().dtor_value())); + nativeBuilder.materialsManager( + software.amazon.cryptography.materialproviders.ToNative.CryptographicMaterialsManager( + dafnyValue.dtor_materialsManager().dtor_value() + ) + ); } if (dafnyValue.dtor_keyring().is_Some()) { - nativeBuilder.keyring(software.amazon.cryptography.materialproviders.ToNative.Keyring(dafnyValue.dtor_keyring().dtor_value())); + nativeBuilder.keyring( + software.amazon.cryptography.materialproviders.ToNative.Keyring( + dafnyValue.dtor_keyring().dtor_value() + ) + ); } if (dafnyValue.dtor_encryptionContext().is_Some()) { - nativeBuilder.encryptionContext(software.amazon.cryptography.materialproviders.ToNative.EncryptionContext(dafnyValue.dtor_encryptionContext().dtor_value())); + nativeBuilder.encryptionContext( + software.amazon.cryptography.materialproviders.ToNative.EncryptionContext( + dafnyValue.dtor_encryptionContext().dtor_value() + ) + ); } return nativeBuilder.build(); } public static DecryptOutput DecryptOutput( - software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptOutput dafnyValue) { + software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptOutput dafnyValue + ) { DecryptOutput.Builder nativeBuilder = DecryptOutput.builder(); - nativeBuilder.plaintext(software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer(dafnyValue.dtor_plaintext())); - nativeBuilder.encryptionContext(software.amazon.cryptography.materialproviders.ToNative.EncryptionContext(dafnyValue.dtor_encryptionContext())); - nativeBuilder.algorithmSuiteId(software.amazon.cryptography.materialproviders.ToNative.ESDKAlgorithmSuiteId(dafnyValue.dtor_algorithmSuiteId())); + nativeBuilder.plaintext( + software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer( + dafnyValue.dtor_plaintext() + ) + ); + nativeBuilder.encryptionContext( + software.amazon.cryptography.materialproviders.ToNative.EncryptionContext( + dafnyValue.dtor_encryptionContext() + ) + ); + nativeBuilder.algorithmSuiteId( + software.amazon.cryptography.materialproviders.ToNative.ESDKAlgorithmSuiteId( + dafnyValue.dtor_algorithmSuiteId() + ) + ); return nativeBuilder.build(); } public static EncryptInput EncryptInput( - software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptInput dafnyValue) { + software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptInput dafnyValue + ) { EncryptInput.Builder nativeBuilder = EncryptInput.builder(); - nativeBuilder.plaintext(software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer(dafnyValue.dtor_plaintext())); + nativeBuilder.plaintext( + software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer( + dafnyValue.dtor_plaintext() + ) + ); if (dafnyValue.dtor_encryptionContext().is_Some()) { - nativeBuilder.encryptionContext(software.amazon.cryptography.materialproviders.ToNative.EncryptionContext(dafnyValue.dtor_encryptionContext().dtor_value())); + nativeBuilder.encryptionContext( + software.amazon.cryptography.materialproviders.ToNative.EncryptionContext( + dafnyValue.dtor_encryptionContext().dtor_value() + ) + ); } if (dafnyValue.dtor_materialsManager().is_Some()) { - nativeBuilder.materialsManager(software.amazon.cryptography.materialproviders.ToNative.CryptographicMaterialsManager(dafnyValue.dtor_materialsManager().dtor_value())); + nativeBuilder.materialsManager( + software.amazon.cryptography.materialproviders.ToNative.CryptographicMaterialsManager( + dafnyValue.dtor_materialsManager().dtor_value() + ) + ); } if (dafnyValue.dtor_keyring().is_Some()) { - nativeBuilder.keyring(software.amazon.cryptography.materialproviders.ToNative.Keyring(dafnyValue.dtor_keyring().dtor_value())); + nativeBuilder.keyring( + software.amazon.cryptography.materialproviders.ToNative.Keyring( + dafnyValue.dtor_keyring().dtor_value() + ) + ); } if (dafnyValue.dtor_algorithmSuiteId().is_Some()) { - nativeBuilder.algorithmSuiteId(software.amazon.cryptography.materialproviders.ToNative.ESDKAlgorithmSuiteId(dafnyValue.dtor_algorithmSuiteId().dtor_value())); + nativeBuilder.algorithmSuiteId( + software.amazon.cryptography.materialproviders.ToNative.ESDKAlgorithmSuiteId( + dafnyValue.dtor_algorithmSuiteId().dtor_value() + ) + ); } if (dafnyValue.dtor_frameLength().is_Some()) { nativeBuilder.frameLength((dafnyValue.dtor_frameLength().dtor_value())); @@ -122,14 +209,42 @@ public static EncryptInput EncryptInput( } public static EncryptOutput EncryptOutput( - software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput dafnyValue) { + software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput dafnyValue + ) { EncryptOutput.Builder nativeBuilder = EncryptOutput.builder(); - nativeBuilder.ciphertext(software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer(dafnyValue.dtor_ciphertext())); - nativeBuilder.encryptionContext(software.amazon.cryptography.materialproviders.ToNative.EncryptionContext(dafnyValue.dtor_encryptionContext())); - nativeBuilder.algorithmSuiteId(software.amazon.cryptography.materialproviders.ToNative.ESDKAlgorithmSuiteId(dafnyValue.dtor_algorithmSuiteId())); + nativeBuilder.ciphertext( + software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer( + dafnyValue.dtor_ciphertext() + ) + ); + nativeBuilder.encryptionContext( + software.amazon.cryptography.materialproviders.ToNative.EncryptionContext( + dafnyValue.dtor_encryptionContext() + ) + ); + nativeBuilder.algorithmSuiteId( + software.amazon.cryptography.materialproviders.ToNative.ESDKAlgorithmSuiteId( + dafnyValue.dtor_algorithmSuiteId() + ) + ); return nativeBuilder.build(); } + public static NetV4_0_0_RetryPolicy NetV4_0_0_RetryPolicy( + NetV4__0__0__RetryPolicy dafnyValue + ) { + if (dafnyValue.is_FORBID__RETRY()) { + return NetV4_0_0_RetryPolicy.FORBID_RETRY; + } + if (dafnyValue.is_ALLOW__RETRY()) { + return NetV4_0_0_RetryPolicy.ALLOW_RETRY; + } + throw new IllegalArgumentException( + "No entry of software.amazon.cryptography.encryptionsdk.model.NetV4_0_0_RetryPolicy matches the input : " + + dafnyValue + ); + } + public static ESDK AwsEncryptionSdk(IAwsEncryptionSdkClient dafnyValue) { return new ESDK(dafnyValue); } diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/AwsEncryptionSdkConfig.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/AwsEncryptionSdkConfig.java index cdc69cba6..0729ea4a6 100644 --- a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/AwsEncryptionSdkConfig.java +++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/AwsEncryptionSdkConfig.java @@ -6,13 +6,20 @@ import software.amazon.cryptography.materialproviders.model.ESDKCommitmentPolicy; public class AwsEncryptionSdkConfig { + private final ESDKCommitmentPolicy commitmentPolicy; private final long maxEncryptedDataKeys; + /** + * During Decryption, Allow or Forbid ESDK-NET v4.0.0 Behavior if the ESDK Message Header fails the Header Authentication check. + */ + private final NetV4_0_0_RetryPolicy netV4_0_0_RetryPolicy; + protected AwsEncryptionSdkConfig(BuilderImpl builder) { this.commitmentPolicy = builder.commitmentPolicy(); this.maxEncryptedDataKeys = builder.maxEncryptedDataKeys(); + this.netV4_0_0_RetryPolicy = builder.netV4_0_0_RetryPolicy(); } public ESDKCommitmentPolicy commitmentPolicy() { @@ -23,6 +30,13 @@ public long maxEncryptedDataKeys() { return this.maxEncryptedDataKeys; } + /** + * @return During Decryption, Allow or Forbid ESDK-NET v4.0.0 Behavior if the ESDK Message Header fails the Header Authentication check. + */ + public NetV4_0_0_RetryPolicy netV4_0_0_RetryPolicy() { + return this.netV4_0_0_RetryPolicy; + } + public Builder toBuilder() { return new BuilderImpl(this); } @@ -40,23 +54,36 @@ public interface Builder { long maxEncryptedDataKeys(); + /** + * @param netV4_0_0_RetryPolicy During Decryption, Allow or Forbid ESDK-NET v4.0.0 Behavior if the ESDK Message Header fails the Header Authentication check. + */ + Builder netV4_0_0_RetryPolicy(NetV4_0_0_RetryPolicy netV4_0_0_RetryPolicy); + + /** + * @return During Decryption, Allow or Forbid ESDK-NET v4.0.0 Behavior if the ESDK Message Header fails the Header Authentication check. + */ + NetV4_0_0_RetryPolicy netV4_0_0_RetryPolicy(); + AwsEncryptionSdkConfig build(); } static class BuilderImpl implements Builder { + protected ESDKCommitmentPolicy commitmentPolicy; protected long maxEncryptedDataKeys; private boolean _maxEncryptedDataKeysSet = false; - protected BuilderImpl() { - } + protected NetV4_0_0_RetryPolicy netV4_0_0_RetryPolicy; + + protected BuilderImpl() {} protected BuilderImpl(AwsEncryptionSdkConfig model) { this.commitmentPolicy = model.commitmentPolicy(); this.maxEncryptedDataKeys = model.maxEncryptedDataKeys(); this._maxEncryptedDataKeysSet = true; + this.netV4_0_0_RetryPolicy = model.netV4_0_0_RetryPolicy(); } public Builder commitmentPolicy(ESDKCommitmentPolicy commitmentPolicy) { @@ -78,9 +105,22 @@ public long maxEncryptedDataKeys() { return this.maxEncryptedDataKeys; } + public Builder netV4_0_0_RetryPolicy( + NetV4_0_0_RetryPolicy netV4_0_0_RetryPolicy + ) { + this.netV4_0_0_RetryPolicy = netV4_0_0_RetryPolicy; + return this; + } + + public NetV4_0_0_RetryPolicy netV4_0_0_RetryPolicy() { + return this.netV4_0_0_RetryPolicy; + } + public AwsEncryptionSdkConfig build() { if (this._maxEncryptedDataKeysSet && this.maxEncryptedDataKeys() < 1) { - throw new IllegalArgumentException("`maxEncryptedDataKeys` must be greater than or equal to 1"); + throw new IllegalArgumentException( + "`maxEncryptedDataKeys` must be greater than or equal to 1" + ); } return new AwsEncryptionSdkConfig(this); } diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/AwsEncryptionSdkException.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/AwsEncryptionSdkException.java index 7e1dc72a3..37553aeb0 100644 --- a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/AwsEncryptionSdkException.java +++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/AwsEncryptionSdkException.java @@ -6,6 +6,7 @@ import java.util.Objects; public class AwsEncryptionSdkException extends RuntimeException { + protected AwsEncryptionSdkException(BuilderImpl builder) { super(messageFromBuilder(builder), builder.cause()); } @@ -67,12 +68,12 @@ public interface Builder { } static class BuilderImpl implements Builder { + protected String message; protected Throwable cause; - protected BuilderImpl() { - } + protected BuilderImpl() {} protected BuilderImpl(AwsEncryptionSdkException model) { this.message = model.message(); @@ -98,8 +99,10 @@ public Throwable cause() { } public AwsEncryptionSdkException build() { - if (Objects.isNull(this.message())) { - throw new IllegalArgumentException("Missing value for required field `message`"); + if (Objects.isNull(this.message())) { + throw new IllegalArgumentException( + "Missing value for required field `message`" + ); } return new AwsEncryptionSdkException(this); } diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/CollectionOfErrors.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/CollectionOfErrors.java index c91eb0e48..524adbd26 100644 --- a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/CollectionOfErrors.java +++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/CollectionOfErrors.java @@ -6,6 +6,7 @@ import java.util.List; public class CollectionOfErrors extends RuntimeException { + /** * The list of Exceptions encountered. */ @@ -90,14 +91,14 @@ public interface Builder { } static class BuilderImpl implements Builder { + protected String message; protected Throwable cause; protected List list; - protected BuilderImpl() { - } + protected BuilderImpl() {} protected BuilderImpl(CollectionOfErrors model) { this.cause = model.getCause(); diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/DecryptInput.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/DecryptInput.java index d3b0bb6ac..4030978cf 100644 --- a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/DecryptInput.java +++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/DecryptInput.java @@ -12,6 +12,7 @@ import software.amazon.cryptography.materialproviders.Keyring; public class DecryptInput { + private final ByteBuffer ciphertext; private final ICryptographicMaterialsManager materialsManager; @@ -72,6 +73,7 @@ public interface Builder { } static class BuilderImpl implements Builder { + protected ByteBuffer ciphertext; protected ICryptographicMaterialsManager materialsManager; @@ -80,8 +82,7 @@ static class BuilderImpl implements Builder { protected Map encryptionContext; - protected BuilderImpl() { - } + protected BuilderImpl() {} protected BuilderImpl(DecryptInput model) { this.ciphertext = model.ciphertext(); @@ -99,8 +100,11 @@ public ByteBuffer ciphertext() { return this.ciphertext; } - public Builder materialsManager(ICryptographicMaterialsManager materialsManager) { - this.materialsManager = CryptographicMaterialsManager.wrap(materialsManager); + public Builder materialsManager( + ICryptographicMaterialsManager materialsManager + ) { + this.materialsManager = + CryptographicMaterialsManager.wrap(materialsManager); return this; } @@ -127,8 +131,10 @@ public Map encryptionContext() { } public DecryptInput build() { - if (Objects.isNull(this.ciphertext())) { - throw new IllegalArgumentException("Missing value for required field `ciphertext`"); + if (Objects.isNull(this.ciphertext())) { + throw new IllegalArgumentException( + "Missing value for required field `ciphertext`" + ); } return new DecryptInput(this); } diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/DecryptOutput.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/DecryptOutput.java index 721c1a380..c2a9cd878 100644 --- a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/DecryptOutput.java +++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/DecryptOutput.java @@ -9,6 +9,7 @@ import software.amazon.cryptography.materialproviders.model.ESDKAlgorithmSuiteId; public class DecryptOutput { + private final ByteBuffer plaintext; private final Map encryptionContext; @@ -58,14 +59,14 @@ public interface Builder { } static class BuilderImpl implements Builder { + protected ByteBuffer plaintext; protected Map encryptionContext; protected ESDKAlgorithmSuiteId algorithmSuiteId; - protected BuilderImpl() { - } + protected BuilderImpl() {} protected BuilderImpl(DecryptOutput model) { this.plaintext = model.plaintext(); @@ -101,14 +102,20 @@ public ESDKAlgorithmSuiteId algorithmSuiteId() { } public DecryptOutput build() { - if (Objects.isNull(this.plaintext())) { - throw new IllegalArgumentException("Missing value for required field `plaintext`"); + if (Objects.isNull(this.plaintext())) { + throw new IllegalArgumentException( + "Missing value for required field `plaintext`" + ); } - if (Objects.isNull(this.encryptionContext())) { - throw new IllegalArgumentException("Missing value for required field `encryptionContext`"); + if (Objects.isNull(this.encryptionContext())) { + throw new IllegalArgumentException( + "Missing value for required field `encryptionContext`" + ); } - if (Objects.isNull(this.algorithmSuiteId())) { - throw new IllegalArgumentException("Missing value for required field `algorithmSuiteId`"); + if (Objects.isNull(this.algorithmSuiteId())) { + throw new IllegalArgumentException( + "Missing value for required field `algorithmSuiteId`" + ); } return new DecryptOutput(this); } diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/EncryptInput.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/EncryptInput.java index 7eb6be51b..67ac13048 100644 --- a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/EncryptInput.java +++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/EncryptInput.java @@ -13,6 +13,7 @@ import software.amazon.cryptography.materialproviders.model.ESDKAlgorithmSuiteId; public class EncryptInput { + private final ByteBuffer plaintext; private final Map encryptionContext; @@ -95,6 +96,7 @@ public interface Builder { } static class BuilderImpl implements Builder { + protected ByteBuffer plaintext; protected Map encryptionContext; @@ -109,8 +111,7 @@ static class BuilderImpl implements Builder { private boolean _frameLengthSet = false; - protected BuilderImpl() { - } + protected BuilderImpl() {} protected BuilderImpl(EncryptInput model) { this.plaintext = model.plaintext(); @@ -140,8 +141,11 @@ public Map encryptionContext() { return this.encryptionContext; } - public Builder materialsManager(ICryptographicMaterialsManager materialsManager) { - this.materialsManager = CryptographicMaterialsManager.wrap(materialsManager); + public Builder materialsManager( + ICryptographicMaterialsManager materialsManager + ) { + this.materialsManager = + CryptographicMaterialsManager.wrap(materialsManager); return this; } @@ -178,14 +182,20 @@ public long frameLength() { } public EncryptInput build() { - if (Objects.isNull(this.plaintext())) { - throw new IllegalArgumentException("Missing value for required field `plaintext`"); + if (Objects.isNull(this.plaintext())) { + throw new IllegalArgumentException( + "Missing value for required field `plaintext`" + ); } if (this._frameLengthSet && this.frameLength() < 1) { - throw new IllegalArgumentException("`frameLength` must be greater than or equal to 1"); + throw new IllegalArgumentException( + "`frameLength` must be greater than or equal to 1" + ); } if (this._frameLengthSet && this.frameLength() > 4294967296) { - throw new IllegalArgumentException("`frameLength` must be less than or equal to 4294967296."); + throw new IllegalArgumentException( + "`frameLength` must be less than or equal to 4294967296." + ); } return new EncryptInput(this); } diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/EncryptOutput.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/EncryptOutput.java index 8b5426237..9e3da246f 100644 --- a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/EncryptOutput.java +++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/EncryptOutput.java @@ -9,6 +9,7 @@ import software.amazon.cryptography.materialproviders.model.ESDKAlgorithmSuiteId; public class EncryptOutput { + private final ByteBuffer ciphertext; private final Map encryptionContext; @@ -58,14 +59,14 @@ public interface Builder { } static class BuilderImpl implements Builder { + protected ByteBuffer ciphertext; protected Map encryptionContext; protected ESDKAlgorithmSuiteId algorithmSuiteId; - protected BuilderImpl() { - } + protected BuilderImpl() {} protected BuilderImpl(EncryptOutput model) { this.ciphertext = model.ciphertext(); @@ -101,14 +102,20 @@ public ESDKAlgorithmSuiteId algorithmSuiteId() { } public EncryptOutput build() { - if (Objects.isNull(this.ciphertext())) { - throw new IllegalArgumentException("Missing value for required field `ciphertext`"); + if (Objects.isNull(this.ciphertext())) { + throw new IllegalArgumentException( + "Missing value for required field `ciphertext`" + ); } - if (Objects.isNull(this.encryptionContext())) { - throw new IllegalArgumentException("Missing value for required field `encryptionContext`"); + if (Objects.isNull(this.encryptionContext())) { + throw new IllegalArgumentException( + "Missing value for required field `encryptionContext`" + ); } - if (Objects.isNull(this.algorithmSuiteId())) { - throw new IllegalArgumentException("Missing value for required field `algorithmSuiteId`"); + if (Objects.isNull(this.algorithmSuiteId())) { + throw new IllegalArgumentException( + "Missing value for required field `algorithmSuiteId`" + ); } return new EncryptOutput(this); } diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/NetV4_0_0_RetryPolicy.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/NetV4_0_0_RetryPolicy.java new file mode 100644 index 000000000..bf7ac1d84 --- /dev/null +++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/NetV4_0_0_RetryPolicy.java @@ -0,0 +1,23 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +package software.amazon.cryptography.encryptionsdk.model; + +/** + * During Decryption, Allow or Forbid ESDK-NET v4.0.0 Behavior if the ESDK Message Header fails the Header Authentication check. + */ +public enum NetV4_0_0_RetryPolicy { + FORBID_RETRY("FORBID_RETRY"), + + ALLOW_RETRY("ALLOW_RETRY"); + + private final String value; + + private NetV4_0_0_RetryPolicy(String value) { + this.value = value; + } + + public String toString() { + return String.valueOf(value); + } +} diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/OpaqueError.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/OpaqueError.java index 90184967f..c24a0e9ec 100644 --- a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/OpaqueError.java +++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/OpaqueError.java @@ -4,6 +4,7 @@ package software.amazon.cryptography.encryptionsdk.model; public class OpaqueError extends RuntimeException { + /** * The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. */ @@ -88,14 +89,14 @@ public interface Builder { } static class BuilderImpl implements Builder { + protected String message; protected Throwable cause; protected Object obj; - protected BuilderImpl() { - } + protected BuilderImpl() {} protected BuilderImpl(OpaqueError model) { this.cause = model.getCause(); @@ -131,7 +132,9 @@ public Object obj() { } public OpaqueError build() { - if (this.obj != null && this.cause == null && this.obj instanceof Throwable) { + if ( + this.obj != null && this.cause == null && this.obj instanceof Throwable + ) { this.cause = (Throwable) this.obj; } else if (this.obj == null && this.cause != null) { this.obj = this.cause; diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs index badb3e515..31352342d 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs @@ -2,34 +2,44 @@ // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. using System; - using AWS.Cryptography.EncryptionSDK; namespace AWS.Cryptography.EncryptionSDK { - public class AwsEncryptionSdkConfig { - private AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy _commitmentPolicy ; - private long? _maxEncryptedDataKeys ; - private AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy _netV4_0_0_RetryPolicy ; - public AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy CommitmentPolicy { - get { return this._commitmentPolicy; } - set { this._commitmentPolicy = value; } -} - public bool IsSetCommitmentPolicy () { - return this._commitmentPolicy != null; -} - public long MaxEncryptedDataKeys { - get { return this._maxEncryptedDataKeys.GetValueOrDefault(); } - set { this._maxEncryptedDataKeys = value; } -} - public bool IsSetMaxEncryptedDataKeys () { - return this._maxEncryptedDataKeys.HasValue; -} - public AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy NetV4_0_0_RetryPolicy { - get { return this._netV4_0_0_RetryPolicy; } - set { this._netV4_0_0_RetryPolicy = value; } -} - public bool IsSetNetV4__0__0__RetryPolicy () { - return this._netV4_0_0_RetryPolicy != null; -} - public void Validate() { - -} -} +using AWS.Cryptography.EncryptionSDK; +namespace AWS.Cryptography.EncryptionSDK +{ + public class AwsEncryptionSdkConfig + { + private AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy _commitmentPolicy; + private long? _maxEncryptedDataKeys; + private AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy _netV4_0_0_RetryPolicy; + public AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy CommitmentPolicy + { + get { return this._commitmentPolicy; } + set { this._commitmentPolicy = value; } + } + public bool IsSetCommitmentPolicy() + { + return this._commitmentPolicy != null; + } + public long MaxEncryptedDataKeys + { + get { return this._maxEncryptedDataKeys.GetValueOrDefault(); } + set { this._maxEncryptedDataKeys = value; } + } + public bool IsSetMaxEncryptedDataKeys() + { + return this._maxEncryptedDataKeys.HasValue; + } + public AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy NetV4__0__0__RetryPolicy + { + get { return this._netV4_0_0_RetryPolicy; } + set { this._netV4_0_0_RetryPolicy = value; } + } + public bool IsSetNetV4__0__0__RetryPolicy() + { + return this._netV4_0_0_RetryPolicy != null; + } + public void Validate() + { + + } + } } diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkException.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkException.cs index 7ab9dafeb..810204bdd 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkException.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkException.cs @@ -2,9 +2,12 @@ // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. using System; - using AWS.Cryptography.EncryptionSDK; namespace AWS.Cryptography.EncryptionSDK { - public class AwsEncryptionSdkException : Exception { - public AwsEncryptionSdkException(string message) : base(message) {} -public string getMessage() { return this.Message; } -} +using AWS.Cryptography.EncryptionSDK; +namespace AWS.Cryptography.EncryptionSDK +{ + public class AwsEncryptionSdkException : Exception + { + public AwsEncryptionSdkException(string message) : base(message) { } + public string getMessage() { return this.Message; } + } } diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs index a3ba46226..2a22994b7 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs @@ -2,12 +2,15 @@ // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. using System; - using AWS.Cryptography.EncryptionSDK; namespace AWS.Cryptography.EncryptionSDK { - public class CollectionOfErrors : Exception { - public readonly System.Collections.Generic.List list; - public CollectionOfErrors(System.Collections.Generic.List list, string message) : base(message) { this.list = list; } - public CollectionOfErrors(string message) : base(message) { this.list = new System.Collections.Generic.List(); } - public CollectionOfErrors() : base("CollectionOfErrors") { this.list = new System.Collections.Generic.List(); } -} +using AWS.Cryptography.EncryptionSDK; +namespace AWS.Cryptography.EncryptionSDK +{ + public class CollectionOfErrors : Exception + { + public readonly System.Collections.Generic.List list; + public CollectionOfErrors(System.Collections.Generic.List list, string message) : base(message) { this.list = list; } + public CollectionOfErrors(string message) : base(message) { this.list = new System.Collections.Generic.List(); } + public CollectionOfErrors() : base("CollectionOfErrors") { this.list = new System.Collections.Generic.List(); } + } } diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/DecryptInput.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/DecryptInput.cs index e0c3dfd62..f686e88a3 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/DecryptInput.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/DecryptInput.cs @@ -2,43 +2,55 @@ // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. using System; - using AWS.Cryptography.EncryptionSDK; namespace AWS.Cryptography.EncryptionSDK { - public class DecryptInput { - private System.IO.MemoryStream _ciphertext ; - private AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager _materialsManager ; - private AWS.Cryptography.MaterialProviders.IKeyring _keyring ; - private System.Collections.Generic.Dictionary _encryptionContext ; - public System.IO.MemoryStream Ciphertext { - get { return this._ciphertext; } - set { this._ciphertext = value; } -} - public bool IsSetCiphertext () { - return this._ciphertext != null; -} - public AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager MaterialsManager { - get { return this._materialsManager; } - set { this._materialsManager = value; } -} - public bool IsSetMaterialsManager () { - return this._materialsManager != null; -} - public AWS.Cryptography.MaterialProviders.IKeyring Keyring { - get { return this._keyring; } - set { this._keyring = value; } -} - public bool IsSetKeyring () { - return this._keyring != null; -} - public System.Collections.Generic.Dictionary EncryptionContext { - get { return this._encryptionContext; } - set { this._encryptionContext = value; } -} - public bool IsSetEncryptionContext () { - return this._encryptionContext != null; -} - public void Validate() { - if (!IsSetCiphertext()) throw new System.ArgumentException("Missing value for required property 'Ciphertext'"); +using AWS.Cryptography.EncryptionSDK; +namespace AWS.Cryptography.EncryptionSDK +{ + public class DecryptInput + { + private System.IO.MemoryStream _ciphertext; + private AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager _materialsManager; + private AWS.Cryptography.MaterialProviders.IKeyring _keyring; + private System.Collections.Generic.Dictionary _encryptionContext; + public System.IO.MemoryStream Ciphertext + { + get { return this._ciphertext; } + set { this._ciphertext = value; } + } + public bool IsSetCiphertext() + { + return this._ciphertext != null; + } + public AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager MaterialsManager + { + get { return this._materialsManager; } + set { this._materialsManager = value; } + } + public bool IsSetMaterialsManager() + { + return this._materialsManager != null; + } + public AWS.Cryptography.MaterialProviders.IKeyring Keyring + { + get { return this._keyring; } + set { this._keyring = value; } + } + public bool IsSetKeyring() + { + return this._keyring != null; + } + public System.Collections.Generic.Dictionary EncryptionContext + { + get { return this._encryptionContext; } + set { this._encryptionContext = value; } + } + public bool IsSetEncryptionContext() + { + return this._encryptionContext != null; + } + public void Validate() + { + if (!IsSetCiphertext()) throw new System.ArgumentException("Missing value for required property 'Ciphertext'"); -} -} + } + } } diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/DecryptOutput.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/DecryptOutput.cs index 3986debb6..776837c71 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/DecryptOutput.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/DecryptOutput.cs @@ -2,37 +2,47 @@ // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. using System; - using AWS.Cryptography.EncryptionSDK; namespace AWS.Cryptography.EncryptionSDK { - public class DecryptOutput { - private System.IO.MemoryStream _plaintext ; - private System.Collections.Generic.Dictionary _encryptionContext ; - private AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId _algorithmSuiteId ; - public System.IO.MemoryStream Plaintext { - get { return this._plaintext; } - set { this._plaintext = value; } -} - public bool IsSetPlaintext () { - return this._plaintext != null; -} - public System.Collections.Generic.Dictionary EncryptionContext { - get { return this._encryptionContext; } - set { this._encryptionContext = value; } -} - public bool IsSetEncryptionContext () { - return this._encryptionContext != null; -} - public AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId AlgorithmSuiteId { - get { return this._algorithmSuiteId; } - set { this._algorithmSuiteId = value; } -} - public bool IsSetAlgorithmSuiteId () { - return this._algorithmSuiteId != null; -} - public void Validate() { - if (!IsSetPlaintext()) throw new System.ArgumentException("Missing value for required property 'Plaintext'"); - if (!IsSetEncryptionContext()) throw new System.ArgumentException("Missing value for required property 'EncryptionContext'"); - if (!IsSetAlgorithmSuiteId()) throw new System.ArgumentException("Missing value for required property 'AlgorithmSuiteId'"); +using AWS.Cryptography.EncryptionSDK; +namespace AWS.Cryptography.EncryptionSDK +{ + public class DecryptOutput + { + private System.IO.MemoryStream _plaintext; + private System.Collections.Generic.Dictionary _encryptionContext; + private AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId _algorithmSuiteId; + public System.IO.MemoryStream Plaintext + { + get { return this._plaintext; } + set { this._plaintext = value; } + } + public bool IsSetPlaintext() + { + return this._plaintext != null; + } + public System.Collections.Generic.Dictionary EncryptionContext + { + get { return this._encryptionContext; } + set { this._encryptionContext = value; } + } + public bool IsSetEncryptionContext() + { + return this._encryptionContext != null; + } + public AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId AlgorithmSuiteId + { + get { return this._algorithmSuiteId; } + set { this._algorithmSuiteId = value; } + } + public bool IsSetAlgorithmSuiteId() + { + return this._algorithmSuiteId != null; + } + public void Validate() + { + if (!IsSetPlaintext()) throw new System.ArgumentException("Missing value for required property 'Plaintext'"); + if (!IsSetEncryptionContext()) throw new System.ArgumentException("Missing value for required property 'EncryptionContext'"); + if (!IsSetAlgorithmSuiteId()) throw new System.ArgumentException("Missing value for required property 'AlgorithmSuiteId'"); -} -} + } + } } diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/ESDK.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/ESDK.cs index e1ef39ff8..1810a4933 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/ESDK.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/ESDK.cs @@ -2,36 +2,43 @@ // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. using System; - using System.IO; - using System.Collections.Generic; - using AWS.Cryptography.EncryptionSDK; - using software.amazon.cryptography.encryptionsdk.internaldafny.types; namespace AWS.Cryptography.EncryptionSDK { - public class ESDK { - private readonly software.amazon.cryptography.encryptionsdk.internaldafny.types.IAwsEncryptionSdkClient _impl; - public ESDK(software.amazon.cryptography.encryptionsdk.internaldafny.types.IAwsEncryptionSdkClient impl) { - this._impl = impl; -} - public software.amazon.cryptography.encryptionsdk.internaldafny.types.IAwsEncryptionSdkClient impl() { - return this._impl; -} - public ESDK(AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig input) - { - software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig internalInput = TypeConversion.ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(input); - var result = software.amazon.cryptography.encryptionsdk.internaldafny.__default.ESDK(internalInput); - if (result.is_Failure) throw TypeConversion.FromDafny_CommonError(result.dtor_error); - this._impl = result.dtor_value; -} - public AWS.Cryptography.EncryptionSDK.EncryptOutput Encrypt(AWS.Cryptography.EncryptionSDK.EncryptInput input) { - software.amazon.cryptography.encryptionsdk.internaldafny.types._IEncryptInput internalInput = TypeConversion.ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput(input); - Wrappers_Compile._IResult result = _impl.Encrypt(internalInput); - if (result.is_Failure) throw TypeConversion.FromDafny_CommonError(result.dtor_error); - return TypeConversion.FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput(result.dtor_value); -} - public AWS.Cryptography.EncryptionSDK.DecryptOutput Decrypt(AWS.Cryptography.EncryptionSDK.DecryptInput input) { - software.amazon.cryptography.encryptionsdk.internaldafny.types._IDecryptInput internalInput = TypeConversion.ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput(input); - Wrappers_Compile._IResult result = _impl.Decrypt(internalInput); - if (result.is_Failure) throw TypeConversion.FromDafny_CommonError(result.dtor_error); - return TypeConversion.FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput(result.dtor_value); -} -} +using System.IO; +using System.Collections.Generic; +using AWS.Cryptography.EncryptionSDK; +using software.amazon.cryptography.encryptionsdk.internaldafny.types; +namespace AWS.Cryptography.EncryptionSDK +{ + public class ESDK + { + private readonly software.amazon.cryptography.encryptionsdk.internaldafny.types.IAwsEncryptionSdkClient _impl; + public ESDK(software.amazon.cryptography.encryptionsdk.internaldafny.types.IAwsEncryptionSdkClient impl) + { + this._impl = impl; + } + public software.amazon.cryptography.encryptionsdk.internaldafny.types.IAwsEncryptionSdkClient impl() + { + return this._impl; + } + public ESDK(AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig input) + { + software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig internalInput = TypeConversion.ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(input); + var result = software.amazon.cryptography.encryptionsdk.internaldafny.__default.ESDK(internalInput); + if (result.is_Failure) throw TypeConversion.FromDafny_CommonError(result.dtor_error); + this._impl = result.dtor_value; + } + public AWS.Cryptography.EncryptionSDK.EncryptOutput Encrypt(AWS.Cryptography.EncryptionSDK.EncryptInput input) + { + software.amazon.cryptography.encryptionsdk.internaldafny.types._IEncryptInput internalInput = TypeConversion.ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput(input); + Wrappers_Compile._IResult result = _impl.Encrypt(internalInput); + if (result.is_Failure) throw TypeConversion.FromDafny_CommonError(result.dtor_error); + return TypeConversion.FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput(result.dtor_value); + } + public AWS.Cryptography.EncryptionSDK.DecryptOutput Decrypt(AWS.Cryptography.EncryptionSDK.DecryptInput input) + { + software.amazon.cryptography.encryptionsdk.internaldafny.types._IDecryptInput internalInput = TypeConversion.ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput(input); + Wrappers_Compile._IResult result = _impl.Decrypt(internalInput); + if (result.is_Failure) throw TypeConversion.FromDafny_CommonError(result.dtor_error); + return TypeConversion.FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput(result.dtor_value); + } + } } diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/EncryptInput.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/EncryptInput.cs index 53602ab63..ca34b8c64 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/EncryptInput.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/EncryptInput.cs @@ -2,59 +2,75 @@ // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. using System; - using AWS.Cryptography.EncryptionSDK; namespace AWS.Cryptography.EncryptionSDK { - public class EncryptInput { - private System.IO.MemoryStream _plaintext ; - private System.Collections.Generic.Dictionary _encryptionContext ; - private AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager _materialsManager ; - private AWS.Cryptography.MaterialProviders.IKeyring _keyring ; - private AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId _algorithmSuiteId ; - private long? _frameLength ; - public System.IO.MemoryStream Plaintext { - get { return this._plaintext; } - set { this._plaintext = value; } -} - public bool IsSetPlaintext () { - return this._plaintext != null; -} - public System.Collections.Generic.Dictionary EncryptionContext { - get { return this._encryptionContext; } - set { this._encryptionContext = value; } -} - public bool IsSetEncryptionContext () { - return this._encryptionContext != null; -} - public AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager MaterialsManager { - get { return this._materialsManager; } - set { this._materialsManager = value; } -} - public bool IsSetMaterialsManager () { - return this._materialsManager != null; -} - public AWS.Cryptography.MaterialProviders.IKeyring Keyring { - get { return this._keyring; } - set { this._keyring = value; } -} - public bool IsSetKeyring () { - return this._keyring != null; -} - public AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId AlgorithmSuiteId { - get { return this._algorithmSuiteId; } - set { this._algorithmSuiteId = value; } -} - public bool IsSetAlgorithmSuiteId () { - return this._algorithmSuiteId != null; -} - public long FrameLength { - get { return this._frameLength.GetValueOrDefault(); } - set { this._frameLength = value; } -} - public bool IsSetFrameLength () { - return this._frameLength.HasValue; -} - public void Validate() { - if (!IsSetPlaintext()) throw new System.ArgumentException("Missing value for required property 'Plaintext'"); +using AWS.Cryptography.EncryptionSDK; +namespace AWS.Cryptography.EncryptionSDK +{ + public class EncryptInput + { + private System.IO.MemoryStream _plaintext; + private System.Collections.Generic.Dictionary _encryptionContext; + private AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager _materialsManager; + private AWS.Cryptography.MaterialProviders.IKeyring _keyring; + private AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId _algorithmSuiteId; + private long? _frameLength; + public System.IO.MemoryStream Plaintext + { + get { return this._plaintext; } + set { this._plaintext = value; } + } + public bool IsSetPlaintext() + { + return this._plaintext != null; + } + public System.Collections.Generic.Dictionary EncryptionContext + { + get { return this._encryptionContext; } + set { this._encryptionContext = value; } + } + public bool IsSetEncryptionContext() + { + return this._encryptionContext != null; + } + public AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager MaterialsManager + { + get { return this._materialsManager; } + set { this._materialsManager = value; } + } + public bool IsSetMaterialsManager() + { + return this._materialsManager != null; + } + public AWS.Cryptography.MaterialProviders.IKeyring Keyring + { + get { return this._keyring; } + set { this._keyring = value; } + } + public bool IsSetKeyring() + { + return this._keyring != null; + } + public AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId AlgorithmSuiteId + { + get { return this._algorithmSuiteId; } + set { this._algorithmSuiteId = value; } + } + public bool IsSetAlgorithmSuiteId() + { + return this._algorithmSuiteId != null; + } + public long FrameLength + { + get { return this._frameLength.GetValueOrDefault(); } + set { this._frameLength = value; } + } + public bool IsSetFrameLength() + { + return this._frameLength.HasValue; + } + public void Validate() + { + if (!IsSetPlaintext()) throw new System.ArgumentException("Missing value for required property 'Plaintext'"); -} -} + } + } } diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/EncryptOutput.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/EncryptOutput.cs index 858c0bbad..f04d490df 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/EncryptOutput.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/EncryptOutput.cs @@ -2,37 +2,47 @@ // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. using System; - using AWS.Cryptography.EncryptionSDK; namespace AWS.Cryptography.EncryptionSDK { - public class EncryptOutput { - private System.IO.MemoryStream _ciphertext ; - private System.Collections.Generic.Dictionary _encryptionContext ; - private AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId _algorithmSuiteId ; - public System.IO.MemoryStream Ciphertext { - get { return this._ciphertext; } - set { this._ciphertext = value; } -} - public bool IsSetCiphertext () { - return this._ciphertext != null; -} - public System.Collections.Generic.Dictionary EncryptionContext { - get { return this._encryptionContext; } - set { this._encryptionContext = value; } -} - public bool IsSetEncryptionContext () { - return this._encryptionContext != null; -} - public AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId AlgorithmSuiteId { - get { return this._algorithmSuiteId; } - set { this._algorithmSuiteId = value; } -} - public bool IsSetAlgorithmSuiteId () { - return this._algorithmSuiteId != null; -} - public void Validate() { - if (!IsSetCiphertext()) throw new System.ArgumentException("Missing value for required property 'Ciphertext'"); - if (!IsSetEncryptionContext()) throw new System.ArgumentException("Missing value for required property 'EncryptionContext'"); - if (!IsSetAlgorithmSuiteId()) throw new System.ArgumentException("Missing value for required property 'AlgorithmSuiteId'"); +using AWS.Cryptography.EncryptionSDK; +namespace AWS.Cryptography.EncryptionSDK +{ + public class EncryptOutput + { + private System.IO.MemoryStream _ciphertext; + private System.Collections.Generic.Dictionary _encryptionContext; + private AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId _algorithmSuiteId; + public System.IO.MemoryStream Ciphertext + { + get { return this._ciphertext; } + set { this._ciphertext = value; } + } + public bool IsSetCiphertext() + { + return this._ciphertext != null; + } + public System.Collections.Generic.Dictionary EncryptionContext + { + get { return this._encryptionContext; } + set { this._encryptionContext = value; } + } + public bool IsSetEncryptionContext() + { + return this._encryptionContext != null; + } + public AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId AlgorithmSuiteId + { + get { return this._algorithmSuiteId; } + set { this._algorithmSuiteId = value; } + } + public bool IsSetAlgorithmSuiteId() + { + return this._algorithmSuiteId != null; + } + public void Validate() + { + if (!IsSetCiphertext()) throw new System.ArgumentException("Missing value for required property 'Ciphertext'"); + if (!IsSetEncryptionContext()) throw new System.ArgumentException("Missing value for required property 'EncryptionContext'"); + if (!IsSetAlgorithmSuiteId()) throw new System.ArgumentException("Missing value for required property 'AlgorithmSuiteId'"); -} -} + } + } } diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/NetV4_0_0_RetryPolicy.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/NetV4_0_0_RetryPolicy.cs index e6712f6e0..b119cfe58 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/NetV4_0_0_RetryPolicy.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/NetV4_0_0_RetryPolicy.cs @@ -2,16 +2,20 @@ // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. using System; - using AWS.Cryptography.EncryptionSDK; namespace AWS.Cryptography.EncryptionSDK { - using Amazon.Runtime; public class NetV4_0_0_RetryPolicy : ConstantClass { +using AWS.Cryptography.EncryptionSDK; +namespace AWS.Cryptography.EncryptionSDK +{ + using Amazon.Runtime; + public class NetV4_0_0_RetryPolicy : ConstantClass + { - - public static readonly NetV4_0_0_RetryPolicy FORBID_RETRY = new NetV4_0_0_RetryPolicy ("FORBID_RETRY"); - - public static readonly NetV4_0_0_RetryPolicy ALLOW_RETRY = new NetV4_0_0_RetryPolicy ("ALLOW_RETRY"); - public static readonly NetV4_0_0_RetryPolicy [] Values = { + + public static readonly NetV4_0_0_RetryPolicy FORBID_RETRY = new NetV4_0_0_RetryPolicy("FORBID_RETRY"); + + public static readonly NetV4_0_0_RetryPolicy ALLOW_RETRY = new NetV4_0_0_RetryPolicy("ALLOW_RETRY"); + public static readonly NetV4_0_0_RetryPolicy[] Values = { ALLOW_RETRY , FORBID_RETRY -} ; - public NetV4_0_0_RetryPolicy (string value) : base(value) {} -} +}; + public NetV4_0_0_RetryPolicy(string value) : base(value) { } + } } diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/OpaqueError.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/OpaqueError.cs index 453f726c1..fbdc58e23 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/OpaqueError.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/OpaqueError.cs @@ -2,12 +2,15 @@ // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. using System; - using AWS.Cryptography.EncryptionSDK; namespace AWS.Cryptography.EncryptionSDK { - public class OpaqueError : Exception { - public readonly object obj; - public OpaqueError(Exception ex) : base("OpaqueError:", ex) { this.obj = ex; } - public OpaqueError() : base("Unknown Unexpected Error") { } - public OpaqueError(object obj) : base(obj is Exception ? "OpaqueError:" : "Opaque obj is not an Exception.", obj as Exception) { this.obj = obj;} -} +using AWS.Cryptography.EncryptionSDK; +namespace AWS.Cryptography.EncryptionSDK +{ + public class OpaqueError : Exception + { + public readonly object obj; + public OpaqueError(Exception ex) : base("OpaqueError:", ex) { this.obj = ex; } + public OpaqueError() : base("Unknown Unexpected Error") { } + public OpaqueError(object obj) : base(obj is Exception ? "OpaqueError:" : "Opaque obj is not an Exception.", obj as Exception) { this.obj = obj; } + } } diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs index 91aed7400..cc922a333 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs @@ -1,991 +1,423 @@ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. - using System.Linq; using System; - namespace AWS.Cryptography.EncryptionSDK { public static class TypeConversion { - public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig( - software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig value) - { - software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig concrete = - (software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig)value; - AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig converted = - new AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig(); - if (concrete._commitmentPolicy.is_Some) - converted.CommitmentPolicy = - (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy( - concrete._commitmentPolicy); - if (concrete._maxEncryptedDataKeys.is_Some) - converted.MaxEncryptedDataKeys = - (long) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys( - concrete._maxEncryptedDataKeys); - // BEGIN MANUAL EDIT - if (concrete._netV4__0__0__RetryPolicy.is_Some) - // END MANUAL EDIT - converted.NetV4_0_0_RetryPolicy = - (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy( - // BEGIN MANUAL EDIT - concrete._netV4__0__0__RetryPolicy); - // END MANUAL EDIT - return converted; + public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig value) + { + software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig concrete = (software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig)value; AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig converted = new AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig(); if (concrete._commitmentPolicy.is_Some) converted.CommitmentPolicy = (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(concrete._commitmentPolicy); + if (concrete._maxEncryptedDataKeys.is_Some) converted.MaxEncryptedDataKeys = (long)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(concrete._maxEncryptedDataKeys); + if (concrete._netV4_0_0_RetryPolicy.is_Some) converted.NetV4__0__0__RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4_0_0_RetryPolicy); return converted; } - - public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig( - AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig value) - { - AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy var_commitmentPolicy = value.IsSetCommitmentPolicy() - ? value.CommitmentPolicy - : (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)null; - long? var_maxEncryptedDataKeys = - value.IsSetMaxEncryptedDataKeys() ? value.MaxEncryptedDataKeys : (long?)null; - AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = - value.IsSetNetV4__0__0__RetryPolicy() - ? value.NetV4_0_0_RetryPolicy - : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; - return new software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig( - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy( - var_commitmentPolicy), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys( - var_maxEncryptedDataKeys), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy( - var_netV4_0_0_RetryPolicy)); + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig value) + { + AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy var_commitmentPolicy = value.IsSetCommitmentPolicy() ? value.CommitmentPolicy : (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)null; + long? var_maxEncryptedDataKeys = value.IsSetMaxEncryptedDataKeys() ? value.MaxEncryptedDataKeys : (long?)null; + AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = value.IsSetNetV4__0__0__RetryPolicy() ? value.NetV4__0__0__RetryPolicy : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; + return new software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(var_commitmentPolicy), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(var_maxEncryptedDataKeys), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(var_netV4_0_0_RetryPolicy)); } - - public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException( - software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException value) + public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException(software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException value) { return new AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException( - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message( - value._message) + FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message(value._message) ); } - - public static software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException( - AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException value) + public static software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException(AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException value) { + return new software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException( - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message( - value.Message) + ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message(value.Message) ); } - - public static AWS.Cryptography.EncryptionSDK.DecryptInput - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput( - software.amazon.cryptography.encryptionsdk.internaldafny.types._IDecryptInput value) - { - software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptInput concrete = - (software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptInput)value; - AWS.Cryptography.EncryptionSDK.DecryptInput converted = new AWS.Cryptography.EncryptionSDK.DecryptInput(); - converted.Ciphertext = - (System.IO.MemoryStream) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M10_ciphertext( - concrete._ciphertext); - if (concrete._materialsManager.is_Some) - converted.MaterialsManager = - (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M16_materialsManager( - concrete._materialsManager); - if (concrete._keyring.is_Some) - converted.Keyring = - (AWS.Cryptography.MaterialProviders.IKeyring) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M7_keyring( - concrete._keyring); - if (concrete._encryptionContext.is_Some) - converted.EncryptionContext = - (System.Collections.Generic.Dictionary) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M17_encryptionContext( - concrete._encryptionContext); - return converted; - } - - public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IDecryptInput - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput( - AWS.Cryptography.EncryptionSDK.DecryptInput value) - { - AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager var_materialsManager = - value.IsSetMaterialsManager() - ? value.MaterialsManager - : (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)null; - AWS.Cryptography.MaterialProviders.IKeyring var_keyring = - value.IsSetKeyring() ? value.Keyring : (AWS.Cryptography.MaterialProviders.IKeyring)null; - System.Collections.Generic.Dictionary var_encryptionContext = value.IsSetEncryptionContext() - ? value.EncryptionContext - : (System.Collections.Generic.Dictionary)null; - return new software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptInput( - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M10_ciphertext(value.Ciphertext), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M16_materialsManager( - var_materialsManager), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M7_keyring(var_keyring), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M17_encryptionContext( - var_encryptionContext)); + public static AWS.Cryptography.EncryptionSDK.DecryptInput FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput(software.amazon.cryptography.encryptionsdk.internaldafny.types._IDecryptInput value) + { + software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptInput concrete = (software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptInput)value; AWS.Cryptography.EncryptionSDK.DecryptInput converted = new AWS.Cryptography.EncryptionSDK.DecryptInput(); converted.Ciphertext = (System.IO.MemoryStream)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M10_ciphertext(concrete._ciphertext); + if (concrete._materialsManager.is_Some) converted.MaterialsManager = (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M16_materialsManager(concrete._materialsManager); + if (concrete._keyring.is_Some) converted.Keyring = (AWS.Cryptography.MaterialProviders.IKeyring)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M7_keyring(concrete._keyring); + if (concrete._encryptionContext.is_Some) converted.EncryptionContext = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M17_encryptionContext(concrete._encryptionContext); return converted; } - - public static AWS.Cryptography.EncryptionSDK.DecryptOutput - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput( - software.amazon.cryptography.encryptionsdk.internaldafny.types._IDecryptOutput value) - { - software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptOutput concrete = - (software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptOutput)value; - AWS.Cryptography.EncryptionSDK.DecryptOutput converted = new AWS.Cryptography.EncryptionSDK.DecryptOutput(); - converted.Plaintext = - (System.IO.MemoryStream) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M9_plaintext( - concrete._plaintext); - converted.EncryptionContext = - (System.Collections.Generic.Dictionary) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M17_encryptionContext( - concrete._encryptionContext); - converted.AlgorithmSuiteId = - (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M16_algorithmSuiteId( - concrete._algorithmSuiteId); - return converted; + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IDecryptInput ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput(AWS.Cryptography.EncryptionSDK.DecryptInput value) + { + AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager var_materialsManager = value.IsSetMaterialsManager() ? value.MaterialsManager : (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)null; + AWS.Cryptography.MaterialProviders.IKeyring var_keyring = value.IsSetKeyring() ? value.Keyring : (AWS.Cryptography.MaterialProviders.IKeyring)null; + System.Collections.Generic.Dictionary var_encryptionContext = value.IsSetEncryptionContext() ? value.EncryptionContext : (System.Collections.Generic.Dictionary)null; + return new software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptInput(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M10_ciphertext(value.Ciphertext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M16_materialsManager(var_materialsManager), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M7_keyring(var_keyring), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M17_encryptionContext(var_encryptionContext)); } - - public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IDecryptOutput - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput( - AWS.Cryptography.EncryptionSDK.DecryptOutput value) + public static AWS.Cryptography.EncryptionSDK.DecryptOutput FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput(software.amazon.cryptography.encryptionsdk.internaldafny.types._IDecryptOutput value) { - return new software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptOutput( - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M9_plaintext(value.Plaintext), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M17_encryptionContext( - value.EncryptionContext), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M16_algorithmSuiteId( - value.AlgorithmSuiteId)); + software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptOutput concrete = (software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptOutput)value; AWS.Cryptography.EncryptionSDK.DecryptOutput converted = new AWS.Cryptography.EncryptionSDK.DecryptOutput(); converted.Plaintext = (System.IO.MemoryStream)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M9_plaintext(concrete._plaintext); + converted.EncryptionContext = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M17_encryptionContext(concrete._encryptionContext); + converted.AlgorithmSuiteId = (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M16_algorithmSuiteId(concrete._algorithmSuiteId); return converted; } + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IDecryptOutput ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput(AWS.Cryptography.EncryptionSDK.DecryptOutput value) + { - public static AWS.Cryptography.EncryptionSDK.EncryptInput - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput( - software.amazon.cryptography.encryptionsdk.internaldafny.types._IEncryptInput value) - { - software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptInput concrete = - (software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptInput)value; - AWS.Cryptography.EncryptionSDK.EncryptInput converted = new AWS.Cryptography.EncryptionSDK.EncryptInput(); - converted.Plaintext = - (System.IO.MemoryStream) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M9_plaintext( - concrete._plaintext); - if (concrete._encryptionContext.is_Some) - converted.EncryptionContext = - (System.Collections.Generic.Dictionary) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M17_encryptionContext( - concrete._encryptionContext); - if (concrete._materialsManager.is_Some) - converted.MaterialsManager = - (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_materialsManager( - concrete._materialsManager); - if (concrete._keyring.is_Some) - converted.Keyring = - (AWS.Cryptography.MaterialProviders.IKeyring) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M7_keyring( - concrete._keyring); - if (concrete._algorithmSuiteId.is_Some) - converted.AlgorithmSuiteId = - (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_algorithmSuiteId( - concrete._algorithmSuiteId); - if (concrete._frameLength.is_Some) - converted.FrameLength = - (long)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M11_frameLength( - concrete._frameLength); - return converted; + return new software.amazon.cryptography.encryptionsdk.internaldafny.types.DecryptOutput(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M9_plaintext(value.Plaintext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M17_encryptionContext(value.EncryptionContext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M16_algorithmSuiteId(value.AlgorithmSuiteId)); } - - public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IEncryptInput - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput( - AWS.Cryptography.EncryptionSDK.EncryptInput value) - { - System.Collections.Generic.Dictionary var_encryptionContext = value.IsSetEncryptionContext() - ? value.EncryptionContext - : (System.Collections.Generic.Dictionary)null; - AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager var_materialsManager = - value.IsSetMaterialsManager() - ? value.MaterialsManager - : (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)null; - AWS.Cryptography.MaterialProviders.IKeyring var_keyring = - value.IsSetKeyring() ? value.Keyring : (AWS.Cryptography.MaterialProviders.IKeyring)null; - AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId var_algorithmSuiteId = value.IsSetAlgorithmSuiteId() - ? value.AlgorithmSuiteId - : (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId)null; + public static AWS.Cryptography.EncryptionSDK.EncryptInput FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput(software.amazon.cryptography.encryptionsdk.internaldafny.types._IEncryptInput value) + { + software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptInput concrete = (software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptInput)value; AWS.Cryptography.EncryptionSDK.EncryptInput converted = new AWS.Cryptography.EncryptionSDK.EncryptInput(); converted.Plaintext = (System.IO.MemoryStream)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M9_plaintext(concrete._plaintext); + if (concrete._encryptionContext.is_Some) converted.EncryptionContext = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M17_encryptionContext(concrete._encryptionContext); + if (concrete._materialsManager.is_Some) converted.MaterialsManager = (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_materialsManager(concrete._materialsManager); + if (concrete._keyring.is_Some) converted.Keyring = (AWS.Cryptography.MaterialProviders.IKeyring)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M7_keyring(concrete._keyring); + if (concrete._algorithmSuiteId.is_Some) converted.AlgorithmSuiteId = (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_algorithmSuiteId(concrete._algorithmSuiteId); + if (concrete._frameLength.is_Some) converted.FrameLength = (long)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M11_frameLength(concrete._frameLength); return converted; + } + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IEncryptInput ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput(AWS.Cryptography.EncryptionSDK.EncryptInput value) + { + System.Collections.Generic.Dictionary var_encryptionContext = value.IsSetEncryptionContext() ? value.EncryptionContext : (System.Collections.Generic.Dictionary)null; + AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager var_materialsManager = value.IsSetMaterialsManager() ? value.MaterialsManager : (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)null; + AWS.Cryptography.MaterialProviders.IKeyring var_keyring = value.IsSetKeyring() ? value.Keyring : (AWS.Cryptography.MaterialProviders.IKeyring)null; + AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId var_algorithmSuiteId = value.IsSetAlgorithmSuiteId() ? value.AlgorithmSuiteId : (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId)null; long? var_frameLength = value.IsSetFrameLength() ? value.FrameLength : (long?)null; - return new software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptInput( - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M9_plaintext(value.Plaintext), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M17_encryptionContext( - var_encryptionContext), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_materialsManager( - var_materialsManager), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M7_keyring(var_keyring), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_algorithmSuiteId( - var_algorithmSuiteId), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M11_frameLength( - var_frameLength)); + return new software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptInput(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M9_plaintext(value.Plaintext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M17_encryptionContext(var_encryptionContext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_materialsManager(var_materialsManager), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M7_keyring(var_keyring), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_algorithmSuiteId(var_algorithmSuiteId), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M11_frameLength(var_frameLength)); } - - public static AWS.Cryptography.EncryptionSDK.EncryptOutput - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput( - software.amazon.cryptography.encryptionsdk.internaldafny.types._IEncryptOutput value) - { - software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput concrete = - (software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput)value; - AWS.Cryptography.EncryptionSDK.EncryptOutput converted = new AWS.Cryptography.EncryptionSDK.EncryptOutput(); - converted.Ciphertext = - (System.IO.MemoryStream) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext( - concrete._ciphertext); - converted.EncryptionContext = - (System.Collections.Generic.Dictionary) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext( - concrete._encryptionContext); - converted.AlgorithmSuiteId = - (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId) - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId( - concrete._algorithmSuiteId); - return converted; + public static AWS.Cryptography.EncryptionSDK.EncryptOutput FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput(software.amazon.cryptography.encryptionsdk.internaldafny.types._IEncryptOutput value) + { + software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput concrete = (software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput)value; AWS.Cryptography.EncryptionSDK.EncryptOutput converted = new AWS.Cryptography.EncryptionSDK.EncryptOutput(); converted.Ciphertext = (System.IO.MemoryStream)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(concrete._ciphertext); + converted.EncryptionContext = (System.Collections.Generic.Dictionary)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(concrete._encryptionContext); + converted.AlgorithmSuiteId = (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId(concrete._algorithmSuiteId); return converted; } + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IEncryptOutput ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput(AWS.Cryptography.EncryptionSDK.EncryptOutput value) + { - public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IEncryptOutput - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput( - AWS.Cryptography.EncryptionSDK.EncryptOutput value) - { - return new software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput( - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext( - value.Ciphertext), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext( - value.EncryptionContext), - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId( - value.AlgorithmSuiteId)); + return new software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(value.Ciphertext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(value.EncryptionContext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId(value.AlgorithmSuiteId)); } - - public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy( - // BEGIN MANUAL EDIT - software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy value) - // END MANUAL EDIT + public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy value) { if (value.is_FORBID__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY; if (value.is_ALLOW__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY; throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); } - - // BEGIN MANUAL EDIT - internal static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy( - AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) - { - if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) - // BEGIN MANUAL EDIT - return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy - // END MANUAL EDIT - .create_FORBID__RETRY(); - if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) - // BEGIN MANUAL EDIT - return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy - // END MANUAL EDIT - .create_ALLOW__RETRY(); + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) + { + if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_FORBID__RETRY(); + if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_ALLOW__RETRY(); throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); } - - public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy( - Wrappers_Compile._IOption value) + public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(Wrappers_Compile._IOption value) { - return value.is_None - ? (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)null - : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy(value.Extract()); + return value.is_None ? (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy(value.Extract()); } - - public static - Wrappers_Compile._IOption< - software.amazon.cryptography.materialproviders.internaldafny.types._IESDKCommitmentPolicy> - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy( - AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy value) - { - return value == null - ? Wrappers_Compile - .Option - .create_None() - : Wrappers_Compile - .Option - .create_Some( - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy( - (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)value)); + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy((AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)value)); } - - public static long? - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys( - Wrappers_Compile._IOption value) + public static long? FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(Wrappers_Compile._IOption value) { - return value.is_None - ? (long?)null - : FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers(value.Extract()); + return value.is_None ? (long?)null : FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers(value.Extract()); } - - public static Wrappers_Compile._IOption - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys( - long? value) + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(long? value) { - return value == null - ? Wrappers_Compile.Option.create_None() - : Wrappers_Compile.Option.create_Some( - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers((long)value)); + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers((long)value)); } - - public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy( - Wrappers_Compile._IOption value) - // END MANUAL EDIT + public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) { - return value.is_None - ? (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null - : FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(value.Extract()); + return value.is_None ? (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null : FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(value.Extract()); } - - public static - Wrappers_Compile._IOption< - // BEGIN MANUAL EDIT - software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy> - // END MANUAL EDIT - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy( - AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) - { - return value == null - ? Wrappers_Compile - // BEGIN MANUAL EDIT - .Option - // END MANUAL EDIT - .create_None() - : Wrappers_Compile - // BEGIN MANUAL EDIT - .Option - // END MANUAL EDIT - .create_Some( - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy( - (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); } - - public static string - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message( - Dafny.ISequence value) + public static string FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message(Dafny.ISequence value) { return FromDafny_N6_smithy__N3_api__S6_String(value); } - - public static Dafny.ISequence - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message(string value) + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message(string value) { return ToDafny_N6_smithy__N3_api__S6_String(value); } - - public static System.IO.MemoryStream - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M10_ciphertext( - Dafny.ISequence value) + public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M10_ciphertext(Dafny.ISequence value) { return FromDafny_N6_smithy__N3_api__S4_Blob(value); } - - public static Dafny.ISequence - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M10_ciphertext( - System.IO.MemoryStream value) + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M10_ciphertext(System.IO.MemoryStream value) { return ToDafny_N6_smithy__N3_api__S4_Blob(value); } - - public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M16_materialsManager( - Wrappers_Compile._IOption value) + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M16_materialsManager(Wrappers_Compile._IOption value) { - return value.is_None - ? (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)null - : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference( - value.Extract()); + return value.is_None ? (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(value.Extract()); } - - public static - Wrappers_Compile._IOption - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M16_materialsManager( - AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager value) - { - return value == null - ? Wrappers_Compile - .Option< - software.amazon.cryptography.materialproviders.internaldafny.types. - ICryptographicMaterialsManager>.create_None() - : Wrappers_Compile - .Option< - software.amazon.cryptography.materialproviders.internaldafny.types. - ICryptographicMaterialsManager> - .create_Some( - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference( - (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)value)); + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M16_materialsManager(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference((AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)value)); } - - public static AWS.Cryptography.MaterialProviders.IKeyring - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M7_keyring( - Wrappers_Compile._IOption - value) + public static AWS.Cryptography.MaterialProviders.IKeyring FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M7_keyring(Wrappers_Compile._IOption value) { - return value.is_None - ? (AWS.Cryptography.MaterialProviders.IKeyring)null - : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(value.Extract()); + return value.is_None ? (AWS.Cryptography.MaterialProviders.IKeyring)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(value.Extract()); } - - public static - Wrappers_Compile._IOption - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M7_keyring( - AWS.Cryptography.MaterialProviders.IKeyring value) - { - return value == null - ? Wrappers_Compile.Option - .create_None() - : Wrappers_Compile.Option - .create_Some( - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference( - (AWS.Cryptography.MaterialProviders.IKeyring)value)); + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M7_keyring(AWS.Cryptography.MaterialProviders.IKeyring value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference((AWS.Cryptography.MaterialProviders.IKeyring)value)); } - - public static System.Collections.Generic.Dictionary - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M17_encryptionContext( - Wrappers_Compile._IOption, Dafny.ISequence>> value) + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M17_encryptionContext(Wrappers_Compile._IOption, Dafny.ISequence>> value) { - return value.is_None - ? (System.Collections.Generic.Dictionary)null - : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value.Extract()); + return value.is_None ? (System.Collections.Generic.Dictionary)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value.Extract()); } - - public static Wrappers_Compile._IOption, Dafny.ISequence>> - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M17_encryptionContext( - System.Collections.Generic.Dictionary value) + public static Wrappers_Compile._IOption, Dafny.ISequence>> ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M17_encryptionContext(System.Collections.Generic.Dictionary value) { - return value == null - ? Wrappers_Compile.Option, Dafny.ISequence>>.create_None() - : Wrappers_Compile.Option, Dafny.ISequence>>.create_Some( - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext( - (System.Collections.Generic.Dictionary)value)); + return value == null ? Wrappers_Compile.Option, Dafny.ISequence>>.create_None() : Wrappers_Compile.Option, Dafny.ISequence>>.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext((System.Collections.Generic.Dictionary)value)); } - - public static System.IO.MemoryStream - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M9_plaintext( - Dafny.ISequence value) + public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M9_plaintext(Dafny.ISequence value) { return FromDafny_N6_smithy__N3_api__S4_Blob(value); } - - public static Dafny.ISequence - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M9_plaintext( - System.IO.MemoryStream value) + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M9_plaintext(System.IO.MemoryStream value) { return ToDafny_N6_smithy__N3_api__S4_Blob(value); } - - public static System.Collections.Generic.Dictionary - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M17_encryptionContext( - Dafny.IMap, Dafny.ISequence> value) + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M17_encryptionContext(Dafny.IMap, Dafny.ISequence> value) { return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value); } - - public static Dafny.IMap, Dafny.ISequence> - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M17_encryptionContext( - System.Collections.Generic.Dictionary value) + public static Dafny.IMap, Dafny.ISequence> ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M17_encryptionContext(System.Collections.Generic.Dictionary value) { return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value); } - - public static AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M16_algorithmSuiteId( - software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId value) + public static AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M16_algorithmSuiteId(software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId value) { return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId(value); } - - public static software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M16_algorithmSuiteId( - AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId value) + public static software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M16_algorithmSuiteId(AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId value) { return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId(value); } - - public static System.IO.MemoryStream - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M9_plaintext( - Dafny.ISequence value) + public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M9_plaintext(Dafny.ISequence value) { return FromDafny_N6_smithy__N3_api__S4_Blob(value); } - - public static Dafny.ISequence - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M9_plaintext( - System.IO.MemoryStream value) + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M9_plaintext(System.IO.MemoryStream value) { return ToDafny_N6_smithy__N3_api__S4_Blob(value); } - - public static System.Collections.Generic.Dictionary - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M17_encryptionContext( - Wrappers_Compile._IOption, Dafny.ISequence>> value) + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M17_encryptionContext(Wrappers_Compile._IOption, Dafny.ISequence>> value) { - return value.is_None - ? (System.Collections.Generic.Dictionary)null - : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value.Extract()); + return value.is_None ? (System.Collections.Generic.Dictionary)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value.Extract()); } - - public static Wrappers_Compile._IOption, Dafny.ISequence>> - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M17_encryptionContext( - System.Collections.Generic.Dictionary value) + public static Wrappers_Compile._IOption, Dafny.ISequence>> ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M17_encryptionContext(System.Collections.Generic.Dictionary value) { - return value == null - ? Wrappers_Compile.Option, Dafny.ISequence>>.create_None() - : Wrappers_Compile.Option, Dafny.ISequence>>.create_Some( - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext( - (System.Collections.Generic.Dictionary)value)); + return value == null ? Wrappers_Compile.Option, Dafny.ISequence>>.create_None() : Wrappers_Compile.Option, Dafny.ISequence>>.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext((System.Collections.Generic.Dictionary)value)); } - - public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_materialsManager( - Wrappers_Compile._IOption value) + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_materialsManager(Wrappers_Compile._IOption value) { - return value.is_None - ? (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)null - : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference( - value.Extract()); + return value.is_None ? (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(value.Extract()); } - - public static - Wrappers_Compile._IOption - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_materialsManager( - AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager value) - { - return value == null - ? Wrappers_Compile - .Option< - software.amazon.cryptography.materialproviders.internaldafny.types. - ICryptographicMaterialsManager>.create_None() - : Wrappers_Compile - .Option< - software.amazon.cryptography.materialproviders.internaldafny.types. - ICryptographicMaterialsManager> - .create_Some( - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference( - (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)value)); + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_materialsManager(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference((AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)value)); } - - public static AWS.Cryptography.MaterialProviders.IKeyring - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M7_keyring( - Wrappers_Compile._IOption - value) + public static AWS.Cryptography.MaterialProviders.IKeyring FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M7_keyring(Wrappers_Compile._IOption value) { - return value.is_None - ? (AWS.Cryptography.MaterialProviders.IKeyring)null - : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(value.Extract()); + return value.is_None ? (AWS.Cryptography.MaterialProviders.IKeyring)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(value.Extract()); } - - public static - Wrappers_Compile._IOption - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M7_keyring( - AWS.Cryptography.MaterialProviders.IKeyring value) - { - return value == null - ? Wrappers_Compile.Option - .create_None() - : Wrappers_Compile.Option - .create_Some( - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference( - (AWS.Cryptography.MaterialProviders.IKeyring)value)); + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M7_keyring(AWS.Cryptography.MaterialProviders.IKeyring value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference((AWS.Cryptography.MaterialProviders.IKeyring)value)); } - - public static AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_algorithmSuiteId( - Wrappers_Compile._IOption value) + public static AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_algorithmSuiteId(Wrappers_Compile._IOption value) { - return value.is_None - ? (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId)null - : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId(value.Extract()); + return value.is_None ? (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId(value.Extract()); } - - public static - Wrappers_Compile._IOption< - software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId> - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_algorithmSuiteId( - AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId value) - { - return value == null - ? Wrappers_Compile - .Option - .create_None() - : Wrappers_Compile - .Option - .create_Some( - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId( - (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId)value)); + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_algorithmSuiteId(AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId((AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId)value)); } - - public static long? FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M11_frameLength( - Wrappers_Compile._IOption value) + public static long? FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M11_frameLength(Wrappers_Compile._IOption value) { - return value.is_None - ? (long?)null - : FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S11_FrameLength(value.Extract()); + return value.is_None ? (long?)null : FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S11_FrameLength(value.Extract()); } - - public static Wrappers_Compile._IOption - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M11_frameLength(long? value) + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M11_frameLength(long? value) { - return value == null - ? Wrappers_Compile.Option.create_None() - : Wrappers_Compile.Option.create_Some( - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S11_FrameLength((long)value)); + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S11_FrameLength((long)value)); } - - public static System.IO.MemoryStream - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext( - Dafny.ISequence value) + public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(Dafny.ISequence value) { return FromDafny_N6_smithy__N3_api__S4_Blob(value); } - - public static Dafny.ISequence - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext( - System.IO.MemoryStream value) + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(System.IO.MemoryStream value) { return ToDafny_N6_smithy__N3_api__S4_Blob(value); } - - public static System.Collections.Generic.Dictionary - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext( - Dafny.IMap, Dafny.ISequence> value) + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(Dafny.IMap, Dafny.ISequence> value) { return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value); } - - public static Dafny.IMap, Dafny.ISequence> - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext( - System.Collections.Generic.Dictionary value) + public static Dafny.IMap, Dafny.ISequence> ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(System.Collections.Generic.Dictionary value) { return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value); } - - public static AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId - FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId( - software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId value) + public static AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId(software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId value) { return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId(value); } - - public static software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId - ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId( - AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId value) + public static software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId(AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId value) { return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId(value); } - - public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy - FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy( - software.amazon.cryptography.materialproviders.internaldafny.types._IESDKCommitmentPolicy value) - { - if (value.is_FORBID__ENCRYPT__ALLOW__DECRYPT) - return AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy.FORBID_ENCRYPT_ALLOW_DECRYPT; - if (value.is_REQUIRE__ENCRYPT__ALLOW__DECRYPT) - return AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy.REQUIRE_ENCRYPT_ALLOW_DECRYPT; - if (value.is_REQUIRE__ENCRYPT__REQUIRE__DECRYPT) - return AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT; + public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy(software.amazon.cryptography.materialproviders.internaldafny.types._IESDKCommitmentPolicy value) + { + if (value.is_FORBID__ENCRYPT__ALLOW__DECRYPT) return AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy.FORBID_ENCRYPT_ALLOW_DECRYPT; + if (value.is_REQUIRE__ENCRYPT__ALLOW__DECRYPT) return AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy.REQUIRE_ENCRYPT_ALLOW_DECRYPT; + if (value.is_REQUIRE__ENCRYPT__REQUIRE__DECRYPT) return AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT; throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy value"); } - - public static software.amazon.cryptography.materialproviders.internaldafny.types._IESDKCommitmentPolicy - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy( - AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy value) - { - if (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy.FORBID_ENCRYPT_ALLOW_DECRYPT.Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKCommitmentPolicy - .create_FORBID__ENCRYPT__ALLOW__DECRYPT(); - if (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy.REQUIRE_ENCRYPT_ALLOW_DECRYPT.Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKCommitmentPolicy - .create_REQUIRE__ENCRYPT__ALLOW__DECRYPT(); - if (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT.Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKCommitmentPolicy - .create_REQUIRE__ENCRYPT__REQUIRE__DECRYPT(); + public static software.amazon.cryptography.materialproviders.internaldafny.types._IESDKCommitmentPolicy ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy(AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy value) + { + if (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy.FORBID_ENCRYPT_ALLOW_DECRYPT.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKCommitmentPolicy.create_FORBID__ENCRYPT__ALLOW__DECRYPT(); + if (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy.REQUIRE_ENCRYPT_ALLOW_DECRYPT.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKCommitmentPolicy.create_REQUIRE__ENCRYPT__ALLOW__DECRYPT(); + if (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKCommitmentPolicy.create_REQUIRE__ENCRYPT__REQUIRE__DECRYPT(); throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy value"); } - public static long FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers(long value) { return value; } - public static long ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers(long value) { return value; } - public static string FromDafny_N6_smithy__N3_api__S6_String(Dafny.ISequence value) { return new string(value.Elements); } - public static Dafny.ISequence ToDafny_N6_smithy__N3_api__S6_String(string value) { return Dafny.Sequence.FromString(value); } - public static System.IO.MemoryStream FromDafny_N6_smithy__N3_api__S4_Blob(Dafny.ISequence value) { return new System.IO.MemoryStream(value.Elements); } - public static Dafny.ISequence ToDafny_N6_smithy__N3_api__S4_Blob(System.IO.MemoryStream value) { - // BEGIN MANUAL EDIT - // It is possible for a MemoryStream to be implemented by another stream, - // which may or may not be backed with an array. - // If the array is empty, but the stream isn't, then - // the backing stream cannot be treated as a MemoryStream - // for purposes of type conversion through ToArray(). if (value.ToArray().Length == 0 && value.Length > 0) { throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); } - // END MANUAL EDIT return Dafny.Sequence.FromArray(value.ToArray()); - } - public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager - FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference( - software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsManager value) + } + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsManager value) { // This is converting a reference type in a dependant module. // Therefore it defers to the dependant module for conversion - return AWS.Cryptography.MaterialProviders.TypeConversion - .FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference( - value); + return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(value); } - - public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsManager - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference( - AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager value) + public static software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsManager ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager value) { // This is converting a reference type in a dependant module. // Therefore it defers to the dependant module for conversion - return AWS.Cryptography.MaterialProviders.TypeConversion - .ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference( - value); + return AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(value); } - - public static AWS.Cryptography.MaterialProviders.IKeyring - FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference( - software.amazon.cryptography.materialproviders.internaldafny.types.IKeyring value) + public static AWS.Cryptography.MaterialProviders.IKeyring FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(software.amazon.cryptography.materialproviders.internaldafny.types.IKeyring value) { // This is converting a reference type in a dependant module. // Therefore it defers to the dependant module for conversion - return AWS.Cryptography.MaterialProviders.TypeConversion - .FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(value); + return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(value); } - - public static software.amazon.cryptography.materialproviders.internaldafny.types.IKeyring - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference( - AWS.Cryptography.MaterialProviders.IKeyring value) + public static software.amazon.cryptography.materialproviders.internaldafny.types.IKeyring ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(AWS.Cryptography.MaterialProviders.IKeyring value) { // This is converting a reference type in a dependant module. // Therefore it defers to the dependant module for conversion - return AWS.Cryptography.MaterialProviders.TypeConversion - .ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(value); + return AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(value); } - - public static System.Collections.Generic.Dictionary - FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext( - Dafny.IMap, Dafny.ISequence> value) + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(Dafny.IMap, Dafny.ISequence> value) { - return value.ItemEnumerable.ToDictionary( - pair => - FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M3_key(pair.Car), - pair => - FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value( - pair.Cdr)); + return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value(pair.Cdr)); } - - public static Dafny.IMap, Dafny.ISequence> - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext( - System.Collections.Generic.Dictionary value) + public static Dafny.IMap, Dafny.ISequence> ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(System.Collections.Generic.Dictionary value) { return Dafny.Map, Dafny.ISequence>.FromCollection(value.Select(pair => - new Dafny.Pair, Dafny.ISequence>( - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M3_key(pair.Key), - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value( - pair.Value)) - )); - } - - public static AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId - FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId( - software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId value) - { - if (value.is_ALG__AES__128__GCM__IV12__TAG16__NO__KDF) - return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_128_GCM_IV12_TAG16_NO_KDF; - if (value.is_ALG__AES__192__GCM__IV12__TAG16__NO__KDF) - return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_192_GCM_IV12_TAG16_NO_KDF; - if (value.is_ALG__AES__256__GCM__IV12__TAG16__NO__KDF) - return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_IV12_TAG16_NO_KDF; - if (value.is_ALG__AES__128__GCM__IV12__TAG16__HKDF__SHA256) - return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_128_GCM_IV12_TAG16_HKDF_SHA256; - if (value.is_ALG__AES__192__GCM__IV12__TAG16__HKDF__SHA256) - return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_192_GCM_IV12_TAG16_HKDF_SHA256; - if (value.is_ALG__AES__256__GCM__IV12__TAG16__HKDF__SHA256) - return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_IV12_TAG16_HKDF_SHA256; - if (value.is_ALG__AES__128__GCM__IV12__TAG16__HKDF__SHA256__ECDSA__P256) - return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId - .ALG_AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256; - if (value.is_ALG__AES__192__GCM__IV12__TAG16__HKDF__SHA384__ECDSA__P384) - return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId - .ALG_AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384; - if (value.is_ALG__AES__256__GCM__IV12__TAG16__HKDF__SHA384__ECDSA__P384) - return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId - .ALG_AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384; - if (value.is_ALG__AES__256__GCM__HKDF__SHA512__COMMIT__KEY) - return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY; - if (value.is_ALG__AES__256__GCM__HKDF__SHA512__COMMIT__KEY__ECDSA__P384) - return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId - .ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384; + new Dafny.Pair, Dafny.ISequence>(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M3_key(pair.Key), ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value(pair.Value)) + )); + } + public static AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId(software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId value) + { + if (value.is_ALG__AES__128__GCM__IV12__TAG16__NO__KDF) return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_128_GCM_IV12_TAG16_NO_KDF; + if (value.is_ALG__AES__192__GCM__IV12__TAG16__NO__KDF) return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_192_GCM_IV12_TAG16_NO_KDF; + if (value.is_ALG__AES__256__GCM__IV12__TAG16__NO__KDF) return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_IV12_TAG16_NO_KDF; + if (value.is_ALG__AES__128__GCM__IV12__TAG16__HKDF__SHA256) return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_128_GCM_IV12_TAG16_HKDF_SHA256; + if (value.is_ALG__AES__192__GCM__IV12__TAG16__HKDF__SHA256) return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_192_GCM_IV12_TAG16_HKDF_SHA256; + if (value.is_ALG__AES__256__GCM__IV12__TAG16__HKDF__SHA256) return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_IV12_TAG16_HKDF_SHA256; + if (value.is_ALG__AES__128__GCM__IV12__TAG16__HKDF__SHA256__ECDSA__P256) return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256; + if (value.is_ALG__AES__192__GCM__IV12__TAG16__HKDF__SHA384__ECDSA__P384) return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384; + if (value.is_ALG__AES__256__GCM__IV12__TAG16__HKDF__SHA384__ECDSA__P384) return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384; + if (value.is_ALG__AES__256__GCM__HKDF__SHA512__COMMIT__KEY) return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY; + if (value.is_ALG__AES__256__GCM__HKDF__SHA512__COMMIT__KEY__ECDSA__P384) return AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384; throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId value"); } - - public static software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId( - AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId value) - { - if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_128_GCM_IV12_TAG16_NO_KDF.Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId - .create_ALG__AES__128__GCM__IV12__TAG16__NO__KDF(); - if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_192_GCM_IV12_TAG16_NO_KDF.Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId - .create_ALG__AES__192__GCM__IV12__TAG16__NO__KDF(); - if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_IV12_TAG16_NO_KDF.Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId - .create_ALG__AES__256__GCM__IV12__TAG16__NO__KDF(); - if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_128_GCM_IV12_TAG16_HKDF_SHA256 - .Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId - .create_ALG__AES__128__GCM__IV12__TAG16__HKDF__SHA256(); - if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_192_GCM_IV12_TAG16_HKDF_SHA256 - .Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId - .create_ALG__AES__192__GCM__IV12__TAG16__HKDF__SHA256(); - if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_IV12_TAG16_HKDF_SHA256 - .Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId - .create_ALG__AES__256__GCM__IV12__TAG16__HKDF__SHA256(); - if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId - .ALG_AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256.Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId - .create_ALG__AES__128__GCM__IV12__TAG16__HKDF__SHA256__ECDSA__P256(); - if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId - .ALG_AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384.Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId - .create_ALG__AES__192__GCM__IV12__TAG16__HKDF__SHA384__ECDSA__P384(); - if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId - .ALG_AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384.Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId - .create_ALG__AES__256__GCM__IV12__TAG16__HKDF__SHA384__ECDSA__P384(); - if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY - .Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId - .create_ALG__AES__256__GCM__HKDF__SHA512__COMMIT__KEY(); - if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId - .ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384.Equals(value)) - return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId - .create_ALG__AES__256__GCM__HKDF__SHA512__COMMIT__KEY__ECDSA__P384(); + public static software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId(AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId value) + { + if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_128_GCM_IV12_TAG16_NO_KDF.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId.create_ALG__AES__128__GCM__IV12__TAG16__NO__KDF(); + if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_192_GCM_IV12_TAG16_NO_KDF.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId.create_ALG__AES__192__GCM__IV12__TAG16__NO__KDF(); + if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_IV12_TAG16_NO_KDF.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId.create_ALG__AES__256__GCM__IV12__TAG16__NO__KDF(); + if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_128_GCM_IV12_TAG16_HKDF_SHA256.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId.create_ALG__AES__128__GCM__IV12__TAG16__HKDF__SHA256(); + if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_192_GCM_IV12_TAG16_HKDF_SHA256.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId.create_ALG__AES__192__GCM__IV12__TAG16__HKDF__SHA256(); + if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_IV12_TAG16_HKDF_SHA256.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId.create_ALG__AES__256__GCM__IV12__TAG16__HKDF__SHA256(); + if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_128_GCM_IV12_TAG16_HKDF_SHA256_ECDSA_P256.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId.create_ALG__AES__128__GCM__IV12__TAG16__HKDF__SHA256__ECDSA__P256(); + if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_192_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId.create_ALG__AES__192__GCM__IV12__TAG16__HKDF__SHA384__ECDSA__P384(); + if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_IV12_TAG16_HKDF_SHA384_ECDSA_P384.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId.create_ALG__AES__256__GCM__IV12__TAG16__HKDF__SHA384__ECDSA__P384(); + if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId.create_ALG__AES__256__GCM__HKDF__SHA512__COMMIT__KEY(); + if (AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId.ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384.Equals(value)) return software.amazon.cryptography.materialproviders.internaldafny.types.ESDKAlgorithmSuiteId.create_ALG__AES__256__GCM__HKDF__SHA512__COMMIT__KEY__ECDSA__P384(); throw new System.ArgumentException("Invalid AWS.Cryptography.MaterialProviders.ESDKAlgorithmSuiteId value"); } - public static long FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S11_FrameLength(long value) { return value; } - public static long ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S11_FrameLength(long value) { return value; } - - public static string FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M3_key( - Dafny.ISequence value) + public static string FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M3_key(Dafny.ISequence value) { return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(value); } - - public static Dafny.ISequence - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M3_key(string value) + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M3_key(string value) { return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(value); } - - public static string FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value( - Dafny.ISequence value) + public static string FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value(Dafny.ISequence value) { return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(value); } - - public static Dafny.ISequence - ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value(string value) + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value(string value) { return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(value); } - - public static string FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes( - Dafny.ISequence value) + public static string FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(Dafny.ISequence value) { System.Text.UTF8Encoding utf8 = new System.Text.UTF8Encoding(false, true); return utf8.GetString(value.Elements); } - - public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes( - string value) + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(string value) { System.Text.UTF8Encoding utf8 = new System.Text.UTF8Encoding(false, true); return Dafny.Sequence.FromArray(utf8.GetBytes(value)); } - - public static System.Exception FromDafny_CommonError( - software.amazon.cryptography.encryptionsdk.internaldafny.types._IError value) + public static System.Exception FromDafny_CommonError(software.amazon.cryptography.encryptionsdk.internaldafny.types._IError value) { switch (value) { - case software.amazon.cryptography.encryptionsdk.internaldafny.types. - Error_AwsCryptographyMaterialProviders dafnyVal: + case software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsCryptographyMaterialProviders dafnyVal: return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_CommonError( - dafnyVal._AwsCryptographyMaterialProviders + dafnyVal._AwsCryptographyMaterialProviders ); - case software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsCryptographyPrimitives - dafnyVal: + case software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsCryptographyPrimitives dafnyVal: return AWS.Cryptography.Primitives.TypeConversion.FromDafny_CommonError( - dafnyVal._AwsCryptographyPrimitives + dafnyVal._AwsCryptographyPrimitives ); - case software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException - dafnyVal: - return FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException( - dafnyVal); + case software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException dafnyVal: + return FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException(dafnyVal); case software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_CollectionOfErrors dafnyVal: return new CollectionOfErrors( new System.Collections.Generic.List(dafnyVal.dtor_list.CloneAsArray() - .Select(x => TypeConversion.FromDafny_CommonError(x))), + .Select(x => TypeConversion.FromDafny_CommonError(x))), new string(dafnyVal.dtor_message.Elements)); case software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_Opaque dafnyVal: return new OpaqueError(dafnyVal._obj); @@ -994,32 +426,27 @@ public static System.Exception FromDafny_CommonError( return new OpaqueError(); } } - - public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IError ToDafny_CommonError( - System.Exception value) + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IError ToDafny_CommonError(System.Exception value) { switch (value.GetType().Namespace) { case "AWS.Cryptography.MaterialProviders": - return software.amazon.cryptography.encryptionsdk.internaldafny.types.Error - .create_AwsCryptographyMaterialProviders( - AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_CommonError(value) - ); + return software.amazon.cryptography.encryptionsdk.internaldafny.types.Error.create_AwsCryptographyMaterialProviders( + AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_CommonError(value) + ); } - switch (value) { case AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException exception: - return ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException( - exception); + return ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException(exception); case CollectionOfErrors collectionOfErrors: return new software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_CollectionOfErrors( - Dafny.Sequence - .FromArray( - collectionOfErrors.list.Select - (x => TypeConversion.ToDafny_CommonError(x)) - .ToArray()), - Dafny.Sequence.FromString(collectionOfErrors.Message) + Dafny.Sequence + .FromArray( + collectionOfErrors.list.Select + (x => TypeConversion.ToDafny_CommonError(x)) + .ToArray()), + Dafny.Sequence.FromString(collectionOfErrors.Message) ); // OpaqueError is redundant, but listed for completeness. case OpaqueError exception: From c45fda49e3df7d3f34901eee504e62a8fe4b599a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 13:25:16 -0800 Subject: [PATCH 12/31] Account for change in client factory method return type --- .../dafny/AwsEncryptionSdk/src/Index.dfy | 2 +- .../AwsEncryptionSdk/test/TestCreateEsdkClient.dfy | 12 +++++++----- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy index 057ab8d96..9125c8d31 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy @@ -23,7 +23,7 @@ module } method ESDK(config: AwsEncryptionSdkConfig) - returns (res: Result) + returns (res: Result) { var maybeCrypto := Primitives.AtomicPrimitives(); var crypto :- maybeCrypto diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy index 1d29adba5..7f8ec2943 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy @@ -52,11 +52,13 @@ module TestCreateEsdkClient { method {:test} TestClientCreation() { var defaultConfig := EncryptionSdk.DefaultAwsEncryptionSdkConfig(); - var esdk :- expect EncryptionSdk.ESDK(config := defaultConfig); - - expect esdk.config.commitmentPolicy == defaultConfig.commitmentPolicy.value; - expect esdk.config.maxEncryptedDataKeys == defaultConfig.maxEncryptedDataKeys; - expect esdk.config.netV4_0_0_RetryPolicy == Types.NetV4_0_0_RetryPolicy.ALLOW_RETRY; + var esdk: Types.IAwsEncryptionSdkClient :- expect EncryptionSdk.ESDK(config := defaultConfig); + expect esdk is EncryptionSdk.ESDKClient; + var esdkClient := esdk as EncryptionSdk.ESDKClient; + + expect esdkClient.config.commitmentPolicy == defaultConfig.commitmentPolicy.value; + expect esdkClient.config.maxEncryptedDataKeys == defaultConfig.maxEncryptedDataKeys; + expect esdkClient.config.netV4_0_0_RetryPolicy == Types.NetV4_0_0_RetryPolicy.ALLOW_RETRY; } method {:test} TestNetRetryFlag() { From b34b9afdda2707151e3d440b2bf55cc70a55701a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 13:44:14 -0800 Subject: [PATCH 13/31] Update MPL when regenerating code for potentially different Dafny version --- .github/workflows/library_dafny_verification.yml | 1 + .github/workflows/library_java_tests.yml | 1 + .github/workflows/library_net_tests.yml | 1 + 3 files changed, 3 insertions(+) diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml index b6d480fe5..50280736d 100644 --- a/.github/workflows/library_dafny_verification.yml +++ b/.github/workflows/library_dafny_verification.yml @@ -50,6 +50,7 @@ jobs: dafny: ${{ env.DAFNY_VERSION }} library: ${{ matrix.library }} diff-generated-code: false + update-and-regenerate-mpl: true - name: Verify ${{ matrix.library }} Dafny code shell: bash diff --git a/.github/workflows/library_java_tests.yml b/.github/workflows/library_java_tests.yml index d13f984ab..c1d601d32 100644 --- a/.github/workflows/library_java_tests.yml +++ b/.github/workflows/library_java_tests.yml @@ -62,6 +62,7 @@ jobs: dafny: ${{ env.DAFNY_VERSION }} library: ${{ matrix.library }} diff-generated-code: false + update-and-regenerate-mpl: true - name: Setup Java 8 uses: actions/setup-java@v3 diff --git a/.github/workflows/library_net_tests.yml b/.github/workflows/library_net_tests.yml index a0e4856d6..ea6d6d6d5 100644 --- a/.github/workflows/library_net_tests.yml +++ b/.github/workflows/library_net_tests.yml @@ -77,6 +77,7 @@ jobs: dafny: ${{ env.DAFNY_VERSION }} library: AwsEncryptionSDK diff-generated-code: false + update-and-regenerate-mpl: true - name: Download Dependencies working-directory: ./AwsEncryptionSDK From 289c92a17b3e843eb8d11063d43c9197846ec531 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 14:12:45 -0800 Subject: [PATCH 14/31] fail-fast: false --- .github/workflows/library_net_tests.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/library_net_tests.yml b/.github/workflows/library_net_tests.yml index ea6d6d6d5..6f75cfd5f 100644 --- a/.github/workflows/library_net_tests.yml +++ b/.github/workflows/library_net_tests.yml @@ -28,6 +28,7 @@ env: jobs: testDotNet: strategy: + fail-fast: false matrix: os: [ windows-latest, From 6066d4ead5b975d3d3d772eeac9ce5e66c81d694 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 15:55:07 -0800 Subject: [PATCH 15/31] Restore manual edits --- .../AwsEncryptionSdk/TypeConversion.cs | 31 ++++++++++++++----- 1 file changed, 23 insertions(+), 8 deletions(-) diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs index cc922a333..87137c37c 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs @@ -11,7 +11,9 @@ public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig FromDafny_N3 { software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig concrete = (software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig)value; AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig converted = new AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig(); if (concrete._commitmentPolicy.is_Some) converted.CommitmentPolicy = (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(concrete._commitmentPolicy); if (concrete._maxEncryptedDataKeys.is_Some) converted.MaxEncryptedDataKeys = (long)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(concrete._maxEncryptedDataKeys); - if (concrete._netV4_0_0_RetryPolicy.is_Some) converted.NetV4__0__0__RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4_0_0_RetryPolicy); return converted; + // BEGIN MANUAL EDIT + if (concrete._netV4__0__0__RetryPolicy.is_Some) converted.NetV4__0__0__RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4__0__0__RetryPolicy); return converted; + // END MANUAL EDIT } public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig value) { @@ -87,16 +89,22 @@ public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IE return new software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(value.Ciphertext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(value.EncryptionContext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId(value.AlgorithmSuiteId)); } - public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy value) + // BEGIN MANUAL EDIT + public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy value) + // END MANUAL EDIT { if (value.is_FORBID__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY; if (value.is_ALLOW__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY; throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); } - public static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) + // BEGIN MANUAL EDIT + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) + // END MANUAL EDIT { - if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_FORBID__RETRY(); - if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_ALLOW__RETRY(); + // BEGIN MANUAL EDIT + if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy.create_FORBID__RETRY(); + if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy.create_ALLOW__RETRY(); + // END MANUAL EDIT throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); } public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(Wrappers_Compile._IOption value) @@ -115,13 +123,20 @@ public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__ { return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers((long)value)); } - public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) + // BEGIN MANUAL EDIT + public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) + // END MANUAL EDIT { + return value.is_None ? (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null : FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(value.Extract()); } - public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) + // BEGIN MANUAL EDIT + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) + // END MANUAL EDIT { - return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); + // BEGIN MANUAL EDIT + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); + // END MANUAL EDIT } public static string FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message(Dafny.ISequence value) { From 1d8df320d8b745ab4cf44bfea07c73f03e058f7d Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 15:55:51 -0800 Subject: [PATCH 16/31] Create patch file --- .../AwsEncryptionSdk/dotnet/dafny-4.2.0.patch | 66 +++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch diff --git a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch new file mode 100644 index 000000000..9f7a81e82 --- /dev/null +++ b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch @@ -0,0 +1,66 @@ +diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs +index cc922a3..87137c3 100644 +--- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs ++++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs +@@ -11,7 +11,9 @@ namespace AWS.Cryptography.EncryptionSDK + { + software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig concrete = (software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig)value; AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig converted = new AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig(); if (concrete._commitmentPolicy.is_Some) converted.CommitmentPolicy = (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(concrete._commitmentPolicy); + if (concrete._maxEncryptedDataKeys.is_Some) converted.MaxEncryptedDataKeys = (long)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(concrete._maxEncryptedDataKeys); +- if (concrete._netV4_0_0_RetryPolicy.is_Some) converted.NetV4__0__0__RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4_0_0_RetryPolicy); return converted; ++ // BEGIN MANUAL EDIT ++ if (concrete._netV4__0__0__RetryPolicy.is_Some) converted.NetV4__0__0__RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4__0__0__RetryPolicy); return converted; ++ // END MANUAL EDIT + } + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig value) + { +@@ -87,16 +89,22 @@ namespace AWS.Cryptography.EncryptionSDK + + return new software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(value.Ciphertext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(value.EncryptionContext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId(value.AlgorithmSuiteId)); + } +- public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy value) ++ // BEGIN MANUAL EDIT ++ public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy value) ++ // END MANUAL EDIT + { + if (value.is_FORBID__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY; + if (value.is_ALLOW__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY; + throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); + } +- public static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) ++ // BEGIN MANUAL EDIT ++ public static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) ++ // END MANUAL EDIT + { +- if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_FORBID__RETRY(); +- if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_ALLOW__RETRY(); ++ // BEGIN MANUAL EDIT ++ if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy.create_FORBID__RETRY(); ++ if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy.create_ALLOW__RETRY(); ++ // END MANUAL EDIT + throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); + } + public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(Wrappers_Compile._IOption value) +@@ -115,13 +123,20 @@ namespace AWS.Cryptography.EncryptionSDK + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers((long)value)); + } +- public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) ++ // BEGIN MANUAL EDIT ++ public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) ++ // END MANUAL EDIT + { ++ + return value.is_None ? (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null : FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(value.Extract()); + } +- public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) ++ // BEGIN MANUAL EDIT ++ public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) ++ // END MANUAL EDIT + { +- return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); ++ // BEGIN MANUAL EDIT ++ return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); ++ // END MANUAL EDIT + } + public static string FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message(Dafny.ISequence value) + { From 49ab6ea2fb0901756002d22e98cf797892442fa0 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 16:14:53 -0800 Subject: [PATCH 17/31] Missing manual edit --- .../Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs | 2 +- .../net/Generated/AwsEncryptionSdk/TypeConversion.cs | 6 ++++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs index 31352342d..58b415434 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs @@ -28,7 +28,7 @@ public bool IsSetMaxEncryptedDataKeys() { return this._maxEncryptedDataKeys.HasValue; } - public AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy NetV4__0__0__RetryPolicy + public AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy NetV4_0_0_RetryPolicy { get { return this._netV4_0_0_RetryPolicy; } set { this._netV4_0_0_RetryPolicy = value; } diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs index 87137c37c..161bcf35a 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs @@ -12,14 +12,16 @@ public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig FromDafny_N3 software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig concrete = (software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig)value; AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig converted = new AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig(); if (concrete._commitmentPolicy.is_Some) converted.CommitmentPolicy = (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(concrete._commitmentPolicy); if (concrete._maxEncryptedDataKeys.is_Some) converted.MaxEncryptedDataKeys = (long)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(concrete._maxEncryptedDataKeys); // BEGIN MANUAL EDIT - if (concrete._netV4__0__0__RetryPolicy.is_Some) converted.NetV4__0__0__RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4__0__0__RetryPolicy); return converted; + if (concrete._netV4__0__0__RetryPolicy.is_Some) converted.NetV4_0_0_RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4__0__0__RetryPolicy); return converted; // END MANUAL EDIT } public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig value) { AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy var_commitmentPolicy = value.IsSetCommitmentPolicy() ? value.CommitmentPolicy : (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)null; long? var_maxEncryptedDataKeys = value.IsSetMaxEncryptedDataKeys() ? value.MaxEncryptedDataKeys : (long?)null; - AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = value.IsSetNetV4__0__0__RetryPolicy() ? value.NetV4__0__0__RetryPolicy : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; + // BEGIN MANUAL EDIT + AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = value.IsSetNetV4__0__0__RetryPolicy() ? value.NetV4_0_0_RetryPolicy : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; + // END MANUAL EDIT return new software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(var_commitmentPolicy), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(var_maxEncryptedDataKeys), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(var_netV4_0_0_RetryPolicy)); } public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException(software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException value) From 8b55fd66e7fcc5228867a41c3620b9a3b8c6c760 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 16:22:52 -0800 Subject: [PATCH 18/31] Update patch file --- .../AwsEncryptionSdk/dotnet/dafny-4.2.0.patch | 32 ++++++++++++++++--- 1 file changed, 27 insertions(+), 5 deletions(-) diff --git a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch index 9f7a81e82..14d2190cc 100644 --- a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch +++ b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch @@ -1,19 +1,41 @@ +diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs +index 3135234..58b4154 100644 +--- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs ++++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs +@@ -28,7 +28,7 @@ namespace AWS.Cryptography.EncryptionSDK + { + return this._maxEncryptedDataKeys.HasValue; + } +- public AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy NetV4__0__0__RetryPolicy ++ public AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy NetV4_0_0_RetryPolicy + { + get { return this._netV4_0_0_RetryPolicy; } + set { this._netV4_0_0_RetryPolicy = value; } diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs -index cc922a3..87137c3 100644 +index cc922a3..161bcf3 100644 --- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs +++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs -@@ -11,7 +11,9 @@ namespace AWS.Cryptography.EncryptionSDK +@@ -11,13 +11,17 @@ namespace AWS.Cryptography.EncryptionSDK { software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig concrete = (software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig)value; AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig converted = new AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig(); if (concrete._commitmentPolicy.is_Some) converted.CommitmentPolicy = (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(concrete._commitmentPolicy); if (concrete._maxEncryptedDataKeys.is_Some) converted.MaxEncryptedDataKeys = (long)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(concrete._maxEncryptedDataKeys); - if (concrete._netV4_0_0_RetryPolicy.is_Some) converted.NetV4__0__0__RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4_0_0_RetryPolicy); return converted; + // BEGIN MANUAL EDIT -+ if (concrete._netV4__0__0__RetryPolicy.is_Some) converted.NetV4__0__0__RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4__0__0__RetryPolicy); return converted; ++ if (concrete._netV4__0__0__RetryPolicy.is_Some) converted.NetV4_0_0_RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4__0__0__RetryPolicy); return converted; + // END MANUAL EDIT } public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig value) { -@@ -87,16 +89,22 @@ namespace AWS.Cryptography.EncryptionSDK + AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy var_commitmentPolicy = value.IsSetCommitmentPolicy() ? value.CommitmentPolicy : (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)null; + long? var_maxEncryptedDataKeys = value.IsSetMaxEncryptedDataKeys() ? value.MaxEncryptedDataKeys : (long?)null; +- AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = value.IsSetNetV4__0__0__RetryPolicy() ? value.NetV4__0__0__RetryPolicy : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; ++ // BEGIN MANUAL EDIT ++ AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = value.IsSetNetV4__0__0__RetryPolicy() ? value.NetV4_0_0_RetryPolicy : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; ++ // END MANUAL EDIT + return new software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(var_commitmentPolicy), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(var_maxEncryptedDataKeys), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(var_netV4_0_0_RetryPolicy)); + } + public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException(software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException value) +@@ -87,16 +91,22 @@ namespace AWS.Cryptography.EncryptionSDK return new software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(value.Ciphertext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(value.EncryptionContext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId(value.AlgorithmSuiteId)); } @@ -40,7 +62,7 @@ index cc922a3..87137c3 100644 throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); } public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(Wrappers_Compile._IOption value) -@@ -115,13 +123,20 @@ namespace AWS.Cryptography.EncryptionSDK +@@ -115,13 +125,20 @@ namespace AWS.Cryptography.EncryptionSDK { return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers((long)value)); } From 357e4c9da7a886eee5414daaced3a9cb72edf571 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 16:46:11 -0800 Subject: [PATCH 19/31] update setup-dafny-action --- .github/workflows/library_net_tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/library_net_tests.yml b/.github/workflows/library_net_tests.yml index 6f75cfd5f..63128036a 100644 --- a/.github/workflows/library_net_tests.yml +++ b/.github/workflows/library_net_tests.yml @@ -67,7 +67,7 @@ jobs: dotnet-version: '6.0.x' - 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 }} From 94f279903fdc81c5b2749627e2009c9382a07d2a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 21:41:00 -0800 Subject: [PATCH 20/31] setup_prettier is annoying --- .github/actions/polymorph_codegen/action.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index 2319002e0..b5a03577d 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -54,10 +54,6 @@ inputs: required: false default: false type: boolean -outputs: - random-number: - description: "Random number" - value: ${{ steps.random-number-generator.outputs.random-number }} runs: using: "composite" steps: @@ -92,6 +88,10 @@ runs: # so prettier is a necessary dependency. run: | make setup_prettier + make -C mpl/AwsCryptographyPrimitives setup_prettier + make -C mpl/AwsCryptographicMaterialProviders setup_prettier + make -C mpl/ComAmazonawsKms setup_prettier + make -C mpl/ComAmazonawsDynamodb setup_prettier make polymorph_java ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} - name: Regenerate .NET code using smithy-dafny From c92d0fe041142956a23d8772d526a875e7f83ed9 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 22:01:07 -0800 Subject: [PATCH 21/31] Account for MPL client types changing --- .../dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy index 695b3379d..ef0308ecb 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy @@ -38,8 +38,8 @@ module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOp import opened Seq datatype Config = Config( - nameonly crypto: Primitives.AtomicPrimitivesClient, - nameonly mpl: MaterialProviders.MaterialProvidersClient, + nameonly crypto: Primitives.Types.IAwsCryptographicPrimitivesClient, + nameonly mpl: MaterialProviders.Types.IAwsCryptographicMaterialProvidersClient, nameonly commitmentPolicy: AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy, nameonly maxEncryptedDataKeys: Option, nameonly netV4_0_0_RetryPolicy: NetV4_0_0_RetryPolicy From 495ad81e1f4c04570d0dfc58e4e435be5fd7b5ad Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 6 Mar 2024 22:07:56 -0800 Subject: [PATCH 22/31] Doh --- .github/actions/polymorph_codegen/action.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index b5a03577d..78da65b2c 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -88,10 +88,10 @@ runs: # so prettier is a necessary dependency. run: | make setup_prettier - make -C mpl/AwsCryptographyPrimitives setup_prettier - make -C mpl/AwsCryptographicMaterialProviders setup_prettier - make -C mpl/ComAmazonawsKms setup_prettier - make -C mpl/ComAmazonawsDynamodb setup_prettier + make -C ../mpl/AwsCryptographyPrimitives setup_prettier + make -C ../mpl/AwsCryptographicMaterialProviders setup_prettier + make -C ../mpl/ComAmazonawsKms setup_prettier + make -C ../mpl/ComAmazonawsDynamodb setup_prettier make polymorph_java ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} - name: Regenerate .NET code using smithy-dafny From 683976a34f2231614ceb5ae755424b362949bc3e Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 7 Mar 2024 11:01:45 -0800 Subject: [PATCH 23/31] Using ProjectReference to MPL, update SDK version --- AwsEncryptionSDK/runtimes/net/ESDK.csproj | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/AwsEncryptionSDK/runtimes/net/ESDK.csproj b/AwsEncryptionSDK/runtimes/net/ESDK.csproj index 8cbf4b900..84a2bd825 100644 --- a/AwsEncryptionSDK/runtimes/net/ESDK.csproj +++ b/AwsEncryptionSDK/runtimes/net/ESDK.csproj @@ -29,10 +29,11 @@ - + + - +