diff --git a/.github/workflows/library_rust_tests.yml b/.github/workflows/library_rust_tests.yml index 17f77cdc0..93e914835 100644 --- a/.github/workflows/library_rust_tests.yml +++ b/.github/workflows/library_rust_tests.yml @@ -68,6 +68,12 @@ jobs: if: matrix.os == 'windows-latest' uses: ilammy/setup-nasm@v1 + # Go is needed for aws-lc-FIPS + - name: Install Go + uses: actions/setup-go@v5 + with: + go-version: ">=1.18" + - name: Install Smithy-Dafny codegen dependencies uses: ./.github/actions/install_smithy_dafny_codegen_dependencies @@ -208,3 +214,11 @@ jobs: # Without this, running test vectors fails due to `fatal runtime error: stack overflow` export RUST_MIN_STACK=104857600 cargo test --release -- --test-threads 1 --nocapture + + - name: Test ${{ matrix.library }} Rust Fips + shell: bash + working-directory: ./${{ matrix.library }}/runtimes/rust + run: | + # Without this, running test vectors fails due to `fatal runtime error: stack overflow` + export RUST_MIN_STACK=104857600 + cargo test --release --features fips -- --nocapture diff --git a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch deleted file mode 100644 index 6cc829983..000000000 --- a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch +++ /dev/null @@ -1,88 +0,0 @@ -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..161bcf3 100644 ---- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs -+++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs -@@ -11,14 +11,18 @@ 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) - { - value.Validate(); - AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy var_commitmentPolicy = value.IsSetCommitmentPolicy() ? value.CommitmentPolicy : (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)null; - long? var_maxEncryptedDataKeys = value.IsSetMaxEncryptedDataKeys() ? value.MaxEncryptedDataKeys : (long?)null; -- AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = value.IsSetNetV4__0__0__RetryPolicy() ? value.NetV4__0__0__RetryPolicy : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; -+ // BEGIN MANUAL EDIT -+ AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = value.IsSetNetV4__0__0__RetryPolicy() ? value.NetV4_0_0_RetryPolicy : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; -+ // END MANUAL EDIT - return new software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(var_commitmentPolicy), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(var_maxEncryptedDataKeys), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(var_netV4_0_0_RetryPolicy)); - } - public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException(software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException value) -@@ -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)); - } -- 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 +125,19 @@ namespace AWS.Cryptography.EncryptionSDK - { - return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers((long)value)); - } -- public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) -+ // BEGIN MANUAL EDIT -+ public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) -+ // END MANUAL EDIT - { - return value.is_None ? (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null : FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(value.Extract()); - } -- public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) -+ // BEGIN MANUAL EDIT -+ public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) -+ // END MANUAL EDIT - { -- return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); -+ // BEGIN MANUAL EDIT -+ return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); -+ // END MANUAL EDIT - } - public static string FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message(Dafny.ISequence value) - { diff --git a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.8.0.patch b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.8.0.patch deleted file mode 100644 index 9f2382998..000000000 --- a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.8.0.patch +++ /dev/null @@ -1,96 +0,0 @@ -diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs -index 1dc37f40..e2187b21 100644 ---- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs -+++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs -@@ -28,7 +28,7 @@ namespace AWS.Cryptography.EncryptionSDK - { - return this._maxEncryptedDataKeys.HasValue; - } -- public AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy NetV4__0__0__RetryPolicy -+ public AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy NetV4_0_0_RetryPolicy - { - get { return this._netV4_0_0_RetryPolicy; } - set { this._netV4_0_0_RetryPolicy = value; } -diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs -index cb1b30bb..dc6e24f9 100644 ---- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs -+++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs -@@ -7,22 +7,22 @@ namespace AWS.Cryptography.EncryptionSDK - { - public static class TypeConversion - { -- private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z"; -- -- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z"; -- - public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig value) - { - software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig concrete = (software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig)value; AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig converted = new AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig(); if (concrete._commitmentPolicy.is_Some) converted.CommitmentPolicy = (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(concrete._commitmentPolicy); - if (concrete._maxEncryptedDataKeys.is_Some) converted.MaxEncryptedDataKeys = (long)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(concrete._maxEncryptedDataKeys); -- if (concrete._netV4_0_0_RetryPolicy.is_Some) converted.NetV4__0__0__RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4_0_0_RetryPolicy); return converted; -+ // BEGIN MANUAL EDIT -+ if (concrete._netV4__0__0__RetryPolicy.is_Some) converted.NetV4_0_0_RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4__0__0__RetryPolicy); return converted; -+ // END MANUAL EDIT - } - public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig value) - { - value.Validate(); - AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy var_commitmentPolicy = value.IsSetCommitmentPolicy() ? value.CommitmentPolicy : (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)null; - long? var_maxEncryptedDataKeys = value.IsSetMaxEncryptedDataKeys() ? value.MaxEncryptedDataKeys : (long?)null; -- AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = value.IsSetNetV4__0__0__RetryPolicy() ? value.NetV4__0__0__RetryPolicy : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; -+ // BEGIN MANUAL EDIT -+ AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = value.IsSetNetV4__0__0__RetryPolicy() ? value.NetV4_0_0_RetryPolicy : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; -+ // END MANUAL EDIT - return new software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(var_commitmentPolicy), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(var_maxEncryptedDataKeys), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(var_netV4_0_0_RetryPolicy)); - } - public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException(software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException value) -@@ -96,16 +96,22 @@ namespace AWS.Cryptography.EncryptionSDK - - return new software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(value.Ciphertext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(value.EncryptionContext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId(value.AlgorithmSuiteId)); - } -- public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy value) -+ // BEGIN MANUAL EDIT -+ public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy value) -+ // END MANUAL EDIT - { - if (value.is_FORBID__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY; - if (value.is_ALLOW__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY; - throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); - } -- public static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) -+ // BEGIN MANUAL EDIT -+ public static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) -+ // END MANUAL EDIT - { -- if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_FORBID__RETRY(); -- if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_ALLOW__RETRY(); -+ // BEGIN MANUAL EDIT -+ if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy.create_FORBID__RETRY(); -+ if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy.create_ALLOW__RETRY(); -+ // END MANUAL EDIT - throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); - } - public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(Wrappers_Compile._IOption value) -@@ -124,13 +130,19 @@ namespace AWS.Cryptography.EncryptionSDK - { - return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers((long)value)); - } -- public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) -+ // BEGIN MANUAL EDIT -+ public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) -+ // END MANUAL EDIT - { - return value.is_None ? (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null : FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(value.Extract()); - } -- public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) -+ // BEGIN MANUAL EDIT -+ public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) -+ // END MANUAL EDIT - { -- return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); -+ // BEGIN MANUAL EDIT -+ return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); -+ // END MANUAL EDIT - } - public static string FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message(Dafny.ISequence value) - { diff --git a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.9.0.patch b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.9.0.patch index 12ed7918d..552a5cc3f 100644 --- a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.9.0.patch +++ b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.9.0.patch @@ -12,7 +12,7 @@ index 1dc37f40..e2187b21 100644 get { return this._netV4_0_0_RetryPolicy; } set { this._netV4_0_0_RetryPolicy = value; } diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs -index 2a22994b..f39ded66 100644 +index 2a22994b..0a3ba615 100644 --- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs +++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs @@ -1,16 +1,27 @@ @@ -46,25 +46,15 @@ index 2a22994b..f39ded66 100644 } diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs -index 2f431c9a..e4f6b17e 100644 +index 3dce5cdb..9722d9f4 100644 --- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs +++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs -@@ -7,22 +7,22 @@ namespace AWS.Cryptography.EncryptionSDK - { - public static class TypeConversion - { -- private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z"; -- -- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z"; -- - public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig value) +@@ -31,14 +31,14 @@ 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) { @@ -72,59 +62,45 @@ index 2f431c9a..e4f6b17e 100644 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.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(Wrappers_Compile._IOption value) +@@ -57,13 +57,13 @@ 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) ++ 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()); + } +- 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) ++ 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)); ++ 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 AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException(software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException value) -@@ -96,16 +96,22 @@ namespace AWS.Cryptography.EncryptionSDK - - return new software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(value.Ciphertext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(value.EncryptionContext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId(value.AlgorithmSuiteId)); + { +@@ -304,16 +304,16 @@ namespace AWS.Cryptography.EncryptionSDK + } + throw new System.ArgumentException("Custom implementations of AWS.Cryptography.MaterialProviders.MaterialProviders are not supported yet"); } - public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy value) -+ // BEGIN MANUAL EDIT + public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy value) -+ // END MANUAL EDIT { if (value.is_FORBID__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY; if (value.is_ALLOW__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY; throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); } - public static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) -+ // BEGIN MANUAL EDIT + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) -+ // END MANUAL EDIT { - if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_FORBID__RETRY(); - if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_ALLOW__RETRY(); -+ // BEGIN MANUAL EDIT + if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy.create_FORBID__RETRY(); + if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy.create_ALLOW__RETRY(); -+ // END MANUAL EDIT throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); } - public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(Wrappers_Compile._IOption value) -@@ -124,13 +130,19 @@ namespace AWS.Cryptography.EncryptionSDK - { - return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers((long)value)); - } -- public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) -+ // BEGIN MANUAL EDIT -+ public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) -+ // END MANUAL EDIT - { - return value.is_None ? (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null : FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(value.Extract()); - } -- public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) -+ // BEGIN MANUAL EDIT -+ public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) -+ // END MANUAL EDIT - { -- return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); -+ // BEGIN MANUAL EDIT -+ return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); -+ // END MANUAL EDIT - } - public static string FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message(Dafny.ISequence value) - { + public static AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(software.amazon.cryptography.materialproviders.internaldafny.types.ICryptographicMaterialsManager value) diff --git a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs index e4f6b17e6..9722d9f4b 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs @@ -7,113 +7,40 @@ namespace AWS.Cryptography.EncryptionSDK { public static class TypeConversion { + private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z"; + + private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z"; + + public static AWS.Cryptography.Primitives.AtomicPrimitives FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AtomicPrimitivesReference(software.amazon.cryptography.primitives.internaldafny.types.IAwsCryptographicPrimitivesClient value) + { + if (value is software.amazon.cryptography.primitives.internaldafny.types.IAwsCryptographicPrimitivesClient dafnyValue) + { + return new AWS.Cryptography.Primitives.AtomicPrimitives(dafnyValue); + } + throw new System.ArgumentException("Custom implementations of AWS.Cryptography.Primitives.AtomicPrimitives are not supported yet"); + } + public static software.amazon.cryptography.primitives.internaldafny.types.IAwsCryptographicPrimitivesClient ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AtomicPrimitivesReference(AWS.Cryptography.Primitives.AtomicPrimitives value) + { + if (value is AWS.Cryptography.Primitives.AtomicPrimitives nativeValue) + { + return nativeValue.impl(); + } + throw new System.ArgumentException("Custom implementations of AWS.Cryptography.Primitives.AtomicPrimitives are not supported yet"); + } 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) converted.NetV4_0_0_RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4__0__0__RetryPolicy); return converted; - // END MANUAL EDIT } public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig value) { value.Validate(); AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy var_commitmentPolicy = value.IsSetCommitmentPolicy() ? value.CommitmentPolicy : (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)null; long? var_maxEncryptedDataKeys = value.IsSetMaxEncryptedDataKeys() ? value.MaxEncryptedDataKeys : (long?)null; - // 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) - { - return new AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException( - 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) - { - - return new software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException( - 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) - { - value.Validate(); - 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.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._IDecryptOutput ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput(AWS.Cryptography.EncryptionSDK.DecryptOutput value) - { - value.Validate(); - - 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 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) - { - value.Validate(); - 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)); - } - 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) - { - value.Validate(); - - 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)); - } - // 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"); - } - // 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 - { - // 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) { return value.is_None ? (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy(value.Extract()); @@ -130,19 +57,26 @@ 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)); } - // 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()); } - // 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 { - // 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 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) + ); + } + 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) + ); } public static string FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message(Dafny.ISequence value) { @@ -152,6 +86,29 @@ public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N13_encryp { return ToDafny_N6_smithy__N3_api__S6_String(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 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) + { + value.Validate(); + 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 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); @@ -160,13 +117,13 @@ public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N13_encryp { 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 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 ? (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(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 ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M16_materialsManager(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager 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.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference((AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)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.IKeyring FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M7_keyring(Wrappers_Compile._IOption value) { @@ -176,21 +133,33 @@ public static AWS.Cryptography.MaterialProviders.IKeyring FromDafny_N3_aws__N12_ { 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 AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M16_materialsManager(Wrappers_Compile._IOption 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 ? (AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)null : FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(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 ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_DecryptInput__M16_materialsManager(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager 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.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference((AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)value)); } - public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M9_plaintext(Dafny.ISequence 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 FromDafny_N6_smithy__N3_api__S4_Blob(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 Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M9_plaintext(System.IO.MemoryStream value) + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IDecryptOutput ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput(AWS.Cryptography.EncryptionSDK.DecryptOutput value) { - return ToDafny_N6_smithy__N3_api__S4_Blob(value); + value.Validate(); + + 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 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) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId(value); } public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M17_encryptionContext(Dafny.IMap, Dafny.ISequence> value) { @@ -200,21 +169,40 @@ public static System.Collections.Generic.Dictionary FromDafny_N3 { 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 System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M9_plaintext(Dafny.ISequence value) { - return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId(value); + return FromDafny_N6_smithy__N3_api__S4_Blob(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 Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_DecryptOutput__M9_plaintext(System.IO.MemoryStream value) { - return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKAlgorithmSuiteId(value); + return ToDafny_N6_smithy__N3_api__S4_Blob(value); } - public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M9_plaintext(Dafny.ISequence value) + public static AWS.Cryptography.EncryptionSDK.EncryptInput FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput(software.amazon.cryptography.encryptionsdk.internaldafny.types._IEncryptInput value) { - return FromDafny_N6_smithy__N3_api__S4_Blob(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 Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M9_plaintext(System.IO.MemoryStream value) + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IEncryptInput ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput(AWS.Cryptography.EncryptionSDK.EncryptInput value) { - return ToDafny_N6_smithy__N3_api__S4_Blob(value); + value.Validate(); + 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)); + } + 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()); + } + 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 System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M17_encryptionContext(Wrappers_Compile._IOption, Dafny.ISequence>> value) { @@ -224,13 +212,13 @@ public static System.Collections.Generic.Dictionary FromDafny_N3 { 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 long? FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M11_frameLength(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 ? (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__M16_materialsManager(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager 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__N17_materialProviders__S38_CryptographicMaterialsManagerReference((AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager)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 AWS.Cryptography.MaterialProviders.IKeyring FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M7_keyring(Wrappers_Compile._IOption value) { @@ -240,37 +228,33 @@ public static AWS.Cryptography.MaterialProviders.IKeyring FromDafny_N3_aws__N12_ { 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) - { - 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 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 AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S12_EncryptInput__M16_materialsManager(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 ? (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__M11_frameLength(long? 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__N13_encryptionSdk__S11_FrameLength((long)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 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__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__S13_EncryptOutput__M10_ciphertext(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__S13_EncryptOutput__M17_encryptionContext(Dafny.IMap, Dafny.ISequence> value) + public static AWS.Cryptography.EncryptionSDK.EncryptOutput FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput(software.amazon.cryptography.encryptionsdk.internaldafny.types._IEncryptOutput value) { - return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(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 Dafny.IMap, Dafny.ISequence> ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(System.Collections.Generic.Dictionary 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 ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value); + value.Validate(); + + 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.MaterialProviders.ESDKAlgorithmSuiteId FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId(software.amazon.cryptography.materialproviders.internaldafny.types._IESDKAlgorithmSuiteId value) { @@ -280,72 +264,69 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types { 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) + public static System.IO.MemoryStream FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(Dafny.ISequence 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"); + return FromDafny_N6_smithy__N3_api__S4_Blob(value); } - public static software.amazon.cryptography.materialproviders.internaldafny.types._IESDKCommitmentPolicy ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy(AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy value) + public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(System.IO.MemoryStream 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"); + return ToDafny_N6_smithy__N3_api__S4_Blob(value); } - public static long FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers(long value) + public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(Dafny.IMap, Dafny.ISequence> value) { - return value; + return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value); } - public static long ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers(long value) + public static Dafny.IMap, Dafny.ISequence> ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(System.Collections.Generic.Dictionary value) { - return value; + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(value); } - public static string FromDafny_N6_smithy__N3_api__S6_String(Dafny.ISequence value) + public static long FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S11_FrameLength(long value) { - return new string(value.Elements); + return value; } - public static Dafny.ISequence ToDafny_N6_smithy__N3_api__S6_String(string value) + public static long ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S11_FrameLength(long value) { - return Dafny.Sequence.FromString(value); + return value; } - public static System.IO.MemoryStream FromDafny_N6_smithy__N3_api__S4_Blob(Dafny.ISequence value) + public static AWS.Cryptography.MaterialProviders.MaterialProviders FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S26_MaterialProvidersReference(software.amazon.cryptography.materialproviders.internaldafny.types.IAwsCryptographicMaterialProvidersClient value) { - return new System.IO.MemoryStream(value.Elements); + if (value is software.amazon.cryptography.materialproviders.internaldafny.types.IAwsCryptographicMaterialProvidersClient dafnyValue) + { + return new AWS.Cryptography.MaterialProviders.MaterialProviders(dafnyValue); + } + throw new System.ArgumentException("Custom implementations of AWS.Cryptography.MaterialProviders.MaterialProviders are not supported yet"); } - public static Dafny.ISequence ToDafny_N6_smithy__N3_api__S4_Blob(System.IO.MemoryStream value) + public static software.amazon.cryptography.materialproviders.internaldafny.types.IAwsCryptographicMaterialProvidersClient ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S26_MaterialProvidersReference(AWS.Cryptography.MaterialProviders.MaterialProviders value) { - if (value.ToArray().Length == 0 && value.Length > 0) + if (value is AWS.Cryptography.MaterialProviders.MaterialProviders nativeValue) { - throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + return nativeValue.impl(); } - return Dafny.Sequence.FromArray(value.ToArray()); - + throw new System.ArgumentException("Custom implementations of AWS.Cryptography.MaterialProviders.MaterialProviders are not supported yet"); } - 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.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) { - // 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); + 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.materialproviders.internaldafny.types.ICryptographicMaterialsManager ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(AWS.Cryptography.MaterialProviders.ICryptographicMaterialsManager 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) { - // 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); + 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.IKeyring FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(software.amazon.cryptography.materialproviders.internaldafny.types.IKeyring 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__S16_KeyringReference(value); + return AWS.Cryptography.MaterialProviders.TypeConversion.FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(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.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__S16_KeyringReference(value); + return AWS.Cryptography.MaterialProviders.TypeConversion.ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S38_CryptographicMaterialsManagerReference(value); } public static System.Collections.Generic.Dictionary FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext(Dafny.IMap, Dafny.ISequence> value) { @@ -357,6 +338,22 @@ public static System.Collections.Generic.Dictionary FromDafny_N3 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 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) + { + 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) + { + 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) + { + return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(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; @@ -387,29 +384,31 @@ public static software.amazon.cryptography.materialproviders.internaldafny.types 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 AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy(software.amazon.cryptography.materialproviders.internaldafny.types._IESDKCommitmentPolicy value) { - return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(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 Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M3_key(string value) + public static software.amazon.cryptography.materialproviders.internaldafny.types._IESDKCommitmentPolicy ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S20_ESDKCommitmentPolicy(AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy value) { - return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(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 string FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value(Dafny.ISequence value) + public static AWS.Cryptography.MaterialProviders.IKeyring FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(software.amazon.cryptography.materialproviders.internaldafny.types.IKeyring value) { - return FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(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); } - public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S17_EncryptionContext__M5_value(string value) + public static software.amazon.cryptography.materialproviders.internaldafny.types.IKeyring ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S16_KeyringReference(AWS.Cryptography.MaterialProviders.IKeyring value) { - return ToDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(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); } public static string FromDafny_N3_aws__N12_cryptography__N17_materialProviders__S9_Utf8Bytes(Dafny.ISequence value) { @@ -421,6 +420,27 @@ public static Dafny.ISequence ToDafny_N3_aws__N12_cryptography__N17_materi System.Text.UTF8Encoding utf8 = new System.Text.UTF8Encoding(false, true); return Dafny.Sequence.FromArray(utf8.GetBytes(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) + { + if (value.ToArray().Length == 0 && value.Length > 0) + { + throw new System.ArgumentException("Fatal Error: MemoryStream instance not backed by an array!"); + } + return Dafny.Sequence.FromArray(value.ToArray()); + + } + public static 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.Exception FromDafny_CommonError(software.amazon.cryptography.encryptionsdk.internaldafny.types._IError value) { switch (value) diff --git a/AwsEncryptionSDK/runtimes/rust/Cargo.toml b/AwsEncryptionSDK/runtimes/rust/Cargo.toml index 4d88e5312..68d145783 100644 --- a/AwsEncryptionSDK/runtimes/rust/Cargo.toml +++ b/AwsEncryptionSDK/runtimes/rust/Cargo.toml @@ -2,7 +2,7 @@ name = "aws-esdk" version = "1.1.1" edition = "2021" -rust-version = "1.81.0" +rust-version = "1.86.0" keywords = ["cryptography", "security", "dynamodb", "encryption", "client-side"] license = "ISC AND (Apache-2.0 OR ISC)" description = "aws-esdk is a library for implementing client side encryption." @@ -16,21 +16,27 @@ readme = "README.md" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -aws-config = "1.6.3" -aws-lc-rs = "=1.13.1" -aws-lc-sys = "=0.29.0" -aws-sdk-dynamodb = "1.73.0" -aws-sdk-kms = "1.67.0" -aws-smithy-runtime-api = {version = "1.8.0", features = ["client"] } -aws-smithy-types = "1.3.1" +aws-config = "1.8.5" +aws-lc-rs = {version = "1.13.3"} +aws-lc-sys = { version = "0.30", optional = true } +aws-lc-fips-sys = { version = "0.13", optional = true } +aws-sdk-dynamodb = "1.90.0" +aws-sdk-kms = "1.84.0" +aws-smithy-runtime-api = {version = "1.9.0", features = ["client"] } +aws-smithy-types = "1.3.2" chrono = "0.4.41" cpu-time = "1.0.0" dafny_runtime = { path = "../../../mpl/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync","small-int"]} dashmap = "6.1.0" pem = "3.0.5" -rand = "0.9.1" -tokio = {version = "1.45.1", features = ["full"] } -uuid = { version = "1.17.0", features = ["v4"] } +rand = "0.9.2" +tokio = {version = "1.47.1", features = ["full"] } +uuid = { version = "1.18.0", features = ["v4"] } [[example]] name = "main" + +[features] +fips = ["aws-lc-rs/fips", "dep:aws-lc-fips-sys"] +non-fips = ["aws-lc-rs/aws-lc-sys", "dep:aws-lc-sys"] +default = ["non-fips"] diff --git a/AwsEncryptionSDK/runtimes/rust/src/lib.rs b/AwsEncryptionSDK/runtimes/rust/src/lib.rs index 7432afd37..c012e1986 100644 --- a/AwsEncryptionSDK/runtimes/rust/src/lib.rs +++ b/AwsEncryptionSDK/runtimes/rust/src/lib.rs @@ -75,6 +75,12 @@ pub mod operation; /// Types for the transform client. pub mod types; +#[cfg(feature = "fips")] +use aws_lc_fips_sys as aws_lc_sys_impl; + +#[cfg(not(feature = "fips"))] +use aws_lc_sys as aws_lc_sys_impl; + pub use client::Client; pub use types::aws_encryption_sdk_config::AwsEncryptionSdkConfig; diff --git a/TestVectors/runtimes/rust/Cargo.toml b/TestVectors/runtimes/rust/Cargo.toml index 607fdd42f..9b08443d1 100644 --- a/TestVectors/runtimes/rust/Cargo.toml +++ b/TestVectors/runtimes/rust/Cargo.toml @@ -2,7 +2,7 @@ name = "aws-esdk-test-vectors" version = "0.1.0" edition = "2021" -rust-version = "1.81.0" +rust-version = "1.86.0" description = "aws-esdk-test-vectors is a library for testing aws-esdk." authors = ["AWS-CryptoTools"] autoexamples = false @@ -10,25 +10,23 @@ readme = "README.md" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html -[features] -wrapped-client = [] - [dependencies] -aws-config = "1.6.3" -aws-lc-rs = "=1.13.1" -aws-lc-sys = "=0.29.0" -aws-sdk-dynamodb = "1.73.0" -aws-sdk-kms = "1.67.0" -aws-smithy-runtime-api = {version = "1.8.0", features = ["client"] } -aws-smithy-types = "1.3.1" +aws-config = "1.8.5" +aws-lc-rs = {version = "1.13.3"} +aws-lc-sys = { version = "0.30", optional = true } +aws-lc-fips-sys = { version = "0.13", optional = true } +aws-sdk-dynamodb = "1.90.0" +aws-sdk-kms = "1.84.0" +aws-smithy-runtime-api = {version = "1.9.0", features = ["client"] } +aws-smithy-types = "1.3.2" chrono = "0.4.41" cpu-time = "1.0.0" dafny_runtime = { path = "../../../mpl/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync","small-int"]} dashmap = "6.1.0" pem = "3.0.5" -rand = "0.9.1" -tokio = {version = "1.45.1", features = ["full"] } -uuid = { version = "1.17.0", features = ["v4"] } +rand = "0.9.2" +tokio = {version = "1.47.1", features = ["full"] } +uuid = { version = "1.18.0", features = ["v4"] } ring = "=0.17.14" [dev-dependencies] @@ -37,3 +35,9 @@ aws-esdk-test-vectors = { path = ".", features = ["wrapped-client"] } [[bin]] name = "test-vectors" path = "src/main.rs" + +[features] +wrapped-client = [] +fips = ["aws-lc-rs/fips", "dep:aws-lc-fips-sys"] +non-fips = ["aws-lc-rs/aws-lc-sys", "dep:aws-lc-sys"] +default = ["non-fips"] diff --git a/TestVectors/runtimes/rust/src/main.rs b/TestVectors/runtimes/rust/src/main.rs index f2859937d..dfc3810ee 100644 --- a/TestVectors/runtimes/rust/src/main.rs +++ b/TestVectors/runtimes/rust/src/main.rs @@ -14,6 +14,12 @@ pub mod operation; pub mod types; pub mod validation; +#[cfg(feature = "fips")] +use aws_lc_fips_sys as aws_lc_sys_impl; + +#[cfg(not(feature = "fips"))] +use aws_lc_sys as aws_lc_sys_impl; + #[cfg(feature = "wrapped-client")] pub mod wrapped; diff --git a/mpl b/mpl index ec013f6ba..f6bdd23d4 160000 --- a/mpl +++ b/mpl @@ -1 +1 @@ -Subproject commit ec013f6ba85d62ab41db48fec92baca85625e4b9 +Subproject commit f6bdd23d4ef83e3513554abb41d0ddbd3d89e8b8 diff --git a/project.properties b/project.properties index 3e44ddb9d..cc17413a5 100644 --- a/project.properties +++ b/project.properties @@ -4,6 +4,6 @@ dafnyVersion=4.9.0 dafnyVerifyVersion=4.9.0 dafnyFormatVersion=4.9.0 projectJavaVersion=4.1.0 -mplDependencyJavaVersion=1.11.0-SNAPSHOT +mplDependencyJavaVersion=1.11.1-SNAPSHOT dafnyRuntimeJavaVersion=4.9.0 smithyDafnyJavaConversionVersion=0.1.1