feat: enforce input constraints (#646)

The AWS Encryption SDK in .NET (ESDK-NET) failed to enforce user input constraints.
Input shapes without required members set would always result in a `NullReferenceException`.
Now, the ESDK-NET will throw it's own Exceptions when illegal user input
is submitted.

AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.2.0.patch

@@ -15,7 +15,7 @@ diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConver
 index cc922a3..161bcf3 100644
 --- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs
 +++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs
-@@ -11,13 +11,17 @@ namespace AWS.Cryptography.EncryptionSDK
+@@ -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);
@@ -26,6 +26,7 @@ index cc922a3..161bcf3 100644
          }
          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;
@@ -62,7 +63,7 @@ index cc922a3..161bcf3 100644
              throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value");
          }
          public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(Wrappers_Compile._IOption<software.amazon.cryptography.materialproviders.internaldafny.types._IESDKCommitmentPolicy> value)
-@@ -115,13 +125,20 @@ namespace AWS.Cryptography.EncryptionSDK
+@@ -115,13 +125,19 @@ namespace AWS.Cryptography.EncryptionSDK
          {
              return value == null ? Wrappers_Compile.Option<long>.create_None() : Wrappers_Compile.Option<long>.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers((long)value));
          }
@@ -71,7 +72,6 @@ index cc922a3..161bcf3 100644
 +        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<software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy> 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<software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy> ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value)

AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/AwsCryptographyEncryptionSdkTypes.dfy

@@ -187,17 +187,17 @@ abstract module AbstractAwsCryptographyEncryptionSdkService
   import Operations : AbstractAwsCryptographyEncryptionSdkOperations
   function method DefaultAwsEncryptionSdkConfig(): AwsEncryptionSdkConfig
   method ESDK(config: AwsEncryptionSdkConfig := DefaultAwsEncryptionSdkConfig())
-    returns (res: Result<IAwsEncryptionSdkClient, Error>)
+    returns (res: Result<ESDKClient, Error>)
     ensures res.Success? ==>
               && fresh(res.value)
               && fresh(res.value.Modifies)
               && fresh(res.value.History)
               && res.value.ValidState()
 
-  // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals
+  // Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals
   function method CreateSuccessOfClient(client: IAwsEncryptionSdkClient): Result<IAwsEncryptionSdkClient, Error> {
     Success(client)
-  } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals
+  }
   function method CreateFailureOfError(error: Error): Result<IAwsEncryptionSdkClient, Error> {
     Failure(error)
   }

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy

@@ -23,7 +23,7 @@ module
   }
 
   method ESDK(config: AwsEncryptionSdkConfig)
-    returns (res: Result<IAwsEncryptionSdkClient, Error>)
+    returns (res: Result<ESDKClient, Error>)
   {
     var maybeCrypto := Primitives.AtomicPrimitives();
     var cryptoX: AwsCryptographyPrimitivesTypes.IAwsCryptographicPrimitivesClient :- maybeCrypto

AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/ESDK.java

@@ -6,6 +6,7 @@
 import Wrappers_Compile.Result;
 import java.lang.IllegalArgumentException;
 import java.util.Objects;
+import software.amazon.cryptography.encryptionsdk.internaldafny.ESDKClient;
 import software.amazon.cryptography.encryptionsdk.internaldafny.__default;
 import software.amazon.cryptography.encryptionsdk.internaldafny.types.Error;
 import software.amazon.cryptography.encryptionsdk.internaldafny.types.IAwsEncryptionSdkClient;
@@ -23,7 +24,7 @@ protected ESDK(BuilderImpl builder) {
     AwsEncryptionSdkConfig input = builder.AwsEncryptionSdkConfig();
     software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig dafnyValue =
       ToDafny.AwsEncryptionSdkConfig(input);
-    Result<IAwsEncryptionSdkClient, Error> result = __default.ESDK(dafnyValue);
+    Result<ESDKClient, Error> result = __default.ESDK(dafnyValue);
     if (result.is_Failure()) {
       throw ToNative.Error(result.dtor_error());
     }

AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs

@@ -39,7 +39,14 @@ public bool IsSetNetV4__0__0__RetryPolicy()
         }
         public void Validate()
         {
-
+            if (IsSetMaxEncryptedDataKeys())
+            {
+                if (MaxEncryptedDataKeys < 1)
+                {
+                    throw new System.ArgumentException(
+                        String.Format("Member MaxEncryptedDataKeys of structure AwsEncryptionSdkConfig has type CountingNumbers which has a minimum of 1 but was given the value {0}.", MaxEncryptedDataKeys));
+                }
+            }
         }
     }
 }

AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/EncryptInput.cs

@@ -70,7 +70,19 @@ public bool IsSetFrameLength()
         public void Validate()
         {
             if (!IsSetPlaintext()) throw new System.ArgumentException("Missing value for required property 'Plaintext'");
-
+            if (IsSetFrameLength())
+            {
+                if (FrameLength < 1)
+                {
+                    throw new System.ArgumentException(
+                        String.Format("Member FrameLength of structure EncryptInput has type FrameLength which has a minimum of 1 but was given the value {0}.", FrameLength));
+                }
+                if (FrameLength > 4294967296)
+                {
+                    throw new System.ArgumentException(
+                        String.Format("Member FrameLength of structure EncryptInput has type FrameLength which has a maximum of 4294967296 but was given the value {0}.", FrameLength));
+                }
+            }
         }
     }
 }

AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs

@@ -17,6 +17,7 @@ public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig FromDafny_N3
         }
         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
@@ -46,6 +47,7 @@ public static AWS.Cryptography.EncryptionSDK.DecryptInput FromDafny_N3_aws__N12_
         }
         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<string, string> var_encryptionContext = value.IsSetEncryptionContext() ? value.EncryptionContext : (System.Collections.Generic.Dictionary<string, string>)null;
@@ -59,6 +61,7 @@ public static AWS.Cryptography.EncryptionSDK.DecryptOutput FromDafny_N3_aws__N12
         }
         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));
         }
@@ -73,6 +76,7 @@ public static AWS.Cryptography.EncryptionSDK.EncryptInput FromDafny_N3_aws__N12_
         }
         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<string, string> var_encryptionContext = value.IsSetEncryptionContext() ? value.EncryptionContext : (System.Collections.Generic.Dictionary<string, string>)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;
@@ -88,6 +92,7 @@ public static AWS.Cryptography.EncryptionSDK.EncryptOutput FromDafny_N3_aws__N12
         }
         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));
         }
@@ -129,7 +134,6 @@ public static Wrappers_Compile._IOption<long> ToDafny_N3_aws__N12_cryptography__
         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<software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy> 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