diff --git a/.gitignore b/.gitignore index 33f67729c..6143b41af 100644 --- a/.gitignore +++ b/.gitignore @@ -6,6 +6,7 @@ build/* test/**/Output/* /package-lock.json **/node_modules +*.log # Duvet output specification_compliance_report.html diff --git a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.9.0.patch b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.9.0.patch new file mode 100644 index 000000000..60d69d7da --- /dev/null +++ b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.9.0.patch @@ -0,0 +1,130 @@ +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/CollectionOfErrors.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs +index 2a22994b..f39ded66 100644 +--- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs ++++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs +@@ -1,16 +1,27 @@ + // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. + // SPDX-License-Identifier: Apache-2.0 + // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. ++ + using System; +-using AWS.Cryptography.EncryptionSDK; ++using System.Collections.Generic; ++ + namespace AWS.Cryptography.EncryptionSDK + { + public class CollectionOfErrors : Exception + { + public readonly System.Collections.Generic.List list; +- public CollectionOfErrors(System.Collections.Generic.List list, string message) : base(message) { this.list = list; } ++ public CollectionOfErrors(System.Collections.Generic.List list, string message) : base(message + $"\n List: \n{ListAsString(list)}") { this.list = list; } + public CollectionOfErrors(string message) : base(message) { this.list = new System.Collections.Generic.List(); } + public CollectionOfErrors() : base("CollectionOfErrors") { this.list = new System.Collections.Generic.List(); } ++ ++ private static string ListAsString(List list) ++ { ++ if (list.Count < 1) return ""; ++ string [] msgArr = new string [list.Count]; ++ for (int i = 0; i < list.Count; i++) ++ msgArr[i] = $"{list[i].GetType().Name} :: {list[i].Message}"; ++ return String.Join("\n\t", msgArr); ++ } + } + + } +diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs +index 2f431c9a..e4f6b17e 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/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs index 2a22994b7..f39ded66d 100644 --- a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs +++ b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/CollectionOfErrors.cs @@ -1,16 +1,27 @@ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten. + using System; -using AWS.Cryptography.EncryptionSDK; +using System.Collections.Generic; + namespace AWS.Cryptography.EncryptionSDK { public class CollectionOfErrors : Exception { public readonly System.Collections.Generic.List list; - public CollectionOfErrors(System.Collections.Generic.List list, string message) : base(message) { this.list = list; } + public CollectionOfErrors(System.Collections.Generic.List list, string message) : base(message + $"\n List: \n{ListAsString(list)}") { this.list = list; } public CollectionOfErrors(string message) : base(message) { this.list = new System.Collections.Generic.List(); } public CollectionOfErrors() : base("CollectionOfErrors") { this.list = new System.Collections.Generic.List(); } + + private static string ListAsString(List list) + { + if (list.Count < 1) return ""; + string [] msgArr = new string [list.Count]; + for (int i = 0; i < list.Count; i++) + msgArr[i] = $"{list[i].GetType().Name} :: {list[i].Message}"; + return String.Join("\n\t", msgArr); + } } }