feat(.net): support aws sdk .net v4

ComAmazonawsDynamodb/runtimes/net/ComAmazonawsDynamodb.csproj

@@ -59,8 +59,8 @@
   <ItemGroup>
     <PackageReference Include="DafnyRuntime" Version="[4.2.0,$(DafnyVersion)]" />
     <!-- See https://learn.microsoft.com/en-us/nuget/concepts/package-versioning?tabs=semver20sort#version-ranges   -->
-    <PackageReference Include="AWSSDK.Core" Version="[3.7.*, 4.0)" />
-    <PackageReference Include="AWSSDK.DynamoDBv2" Version="[3.7.*, 4.0)" />
+    <PackageReference Include="AWSSDK.Core" Version="4.0.*" />
+    <PackageReference Include="AWSSDK.DynamoDBv2" Version="4.0.*" />
     <ProjectReference Include="../../../StandardLibrary/runtimes/net/STD.csproj" />
     <!--
       System.Collections.Immutable can be removed once dafny.msbuild is updated with

ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs

@@ -80,33 +80,33 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_B(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_B(value.B));
             }
-            if (value.SS.Any())
+            if (value.SS != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_SS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_SS(value.SS));
             }
-            if (value.NS.Any())
+            if (value.NS != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_NS(value.NS));
             }
-            if (value.BS.Any())
+            if (value.BS != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BS(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M2_BS(value.BS));
             }
-            if (value.IsMSet)
+            if (value.M != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_M(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_M(value.M));
             }
-            if (value.IsLSet)
+            if (value.L != null)
             {
                 return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_L(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M1_L(value.L));
             }
             if (value.NULL == true)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL(value.NULL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_NULL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_NULL((bool)value.NULL));
             }
-            if (value.IsBOOLSet)
+            if (value.BOOL != null)
             {
-                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL(value.BOOL));
+                return software.amazon.cryptography.services.dynamodb.internaldafny.types.AttributeValue.create_BOOL(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_AttributeValue__M4_BOOL((bool)value.BOOL));
             }
             throw new System.ArgumentException("Invalid Amazon.DynamoDBv2.Model.AttributeValue state");
         }
@@ -5462,7 +5462,7 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
 
             long? var_backupSizeBytes = value.BackupSizeBytes;
             System.DateTime? var_backupExpiryDateTime = value.BackupExpiryDateTime;
-            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.BackupDetails(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M9_BackupArn(value.BackupArn), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M10_BackupName(value.BackupName), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M15_BackupSizeBytes(var_backupSizeBytes), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M12_BackupStatus(value.BackupStatus), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M10_BackupType(value.BackupType), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M22_BackupCreationDateTime(value.BackupCreationDateTime), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M20_BackupExpiryDateTime(var_backupExpiryDateTime));
+            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.BackupDetails(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M9_BackupArn(value.BackupArn), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M10_BackupName(value.BackupName), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M15_BackupSizeBytes(var_backupSizeBytes), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M12_BackupStatus(value.BackupStatus), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M10_BackupType(value.BackupType), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M22_BackupCreationDateTime((System.DateTime)value.BackupCreationDateTime), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S13_BackupDetails__M20_BackupExpiryDateTime(var_backupExpiryDateTime));
         }
         public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S9_TableName(Dafny.ISequence<char> value)
         {
@@ -5551,7 +5551,7 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
         {
 
 
-            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.ProvisionedThroughput(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_ProvisionedThroughput__M17_ReadCapacityUnits(value.ReadCapacityUnits), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_ProvisionedThroughput__M18_WriteCapacityUnits(value.WriteCapacityUnits));
+            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.ProvisionedThroughput(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_ProvisionedThroughput__M17_ReadCapacityUnits((long)value.ReadCapacityUnits), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S21_ProvisionedThroughput__M18_WriteCapacityUnits((long)value.WriteCapacityUnits));
         }
         public static Amazon.DynamoDBv2.Model.StreamSpecification FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S19_StreamSpecification(software.amazon.cryptography.services.dynamodb.internaldafny.types._IStreamSpecification value)
         {
@@ -5562,7 +5562,7 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
         {
 
             Amazon.DynamoDBv2.StreamViewType var_streamViewType = value.StreamViewType;
-            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.StreamSpecification(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S19_StreamSpecification__M13_StreamEnabled(value.StreamEnabled), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S19_StreamSpecification__M14_StreamViewType(var_streamViewType));
+            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.StreamSpecification(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S19_StreamSpecification__M13_StreamEnabled((bool)value.StreamEnabled), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S19_StreamSpecification__M14_StreamViewType(var_streamViewType));
         }
         public static Amazon.DynamoDBv2.Model.SSESpecification FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S16_SSESpecification(software.amazon.cryptography.services.dynamodb.internaldafny.types._ISSESpecification value)
         {
@@ -6697,7 +6697,7 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
         {
 
 
-            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.PointInTimeRecoverySpecification(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S32_PointInTimeRecoverySpecification__M26_PointInTimeRecoveryEnabled(value.PointInTimeRecoveryEnabled));
+            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.PointInTimeRecoverySpecification(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S32_PointInTimeRecoverySpecification__M26_PointInTimeRecoveryEnabled((bool)value.PointInTimeRecoveryEnabled));
         }
         public static Amazon.DynamoDBv2.ContributorInsightsAction FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S25_ContributorInsightsAction(software.amazon.cryptography.services.dynamodb.internaldafny.types._IContributorInsightsAction value)
         {
@@ -6822,7 +6822,7 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
         {
 
 
-            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.TimeToLiveSpecification(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_TimeToLiveSpecification__M7_Enabled(value.Enabled), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_TimeToLiveSpecification__M13_AttributeName(value.AttributeName));
+            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.TimeToLiveSpecification(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_TimeToLiveSpecification__M7_Enabled((bool)value.Enabled), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_TimeToLiveSpecification__M13_AttributeName(value.AttributeName));
         }
         public static string FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S23_StringSetAttributeValue__M6_member(Dafny.ISequence<char> value)
         {
@@ -8776,7 +8776,7 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
 
             string var_sourceBackupArn = value.SourceBackupArn;
             string var_sourceTableArn = value.SourceTableArn;
-            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.RestoreSummary(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_RestoreSummary__M15_SourceBackupArn(var_sourceBackupArn), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_RestoreSummary__M14_SourceTableArn(var_sourceTableArn), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_RestoreSummary__M15_RestoreDateTime(value.RestoreDateTime), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_RestoreSummary__M17_RestoreInProgress(value.RestoreInProgress));
+            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.RestoreSummary(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_RestoreSummary__M15_SourceBackupArn(var_sourceBackupArn), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_RestoreSummary__M14_SourceTableArn(var_sourceTableArn), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_RestoreSummary__M15_RestoreDateTime((System.DateTime)value.RestoreDateTime), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_RestoreSummary__M17_RestoreInProgress((bool)value.RestoreInProgress));
         }
         public static Amazon.DynamoDBv2.Model.SSEDescription FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S14_SSEDescription(software.amazon.cryptography.services.dynamodb.internaldafny.types._ISSEDescription value)
         {
@@ -8841,7 +8841,7 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
             Amazon.DynamoDBv2.Model.OnDemandThroughput var_onDemandThroughput = value.OnDemandThroughput;
             long? var_itemCount = value.ItemCount;
             Amazon.DynamoDBv2.BillingMode var_billingMode = value.BillingMode;
-            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.SourceTableDetails(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M9_TableName(value.TableName), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M7_TableId(value.TableId), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M8_TableArn(var_tableArn), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M14_TableSizeBytes(var_tableSizeBytes), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M9_KeySchema(value.KeySchema), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M21_TableCreationDateTime(value.TableCreationDateTime), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M21_ProvisionedThroughput(value.ProvisionedThroughput), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M18_OnDemandThroughput(var_onDemandThroughput), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M9_ItemCount(var_itemCount), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M11_BillingMode(var_billingMode));
+            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.SourceTableDetails(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M9_TableName(value.TableName), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M7_TableId(value.TableId), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M8_TableArn(var_tableArn), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M14_TableSizeBytes(var_tableSizeBytes), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M9_KeySchema(value.KeySchema), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M21_TableCreationDateTime((System.DateTime)value.TableCreationDateTime), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M21_ProvisionedThroughput(value.ProvisionedThroughput), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M18_OnDemandThroughput(var_onDemandThroughput), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M9_ItemCount(var_itemCount), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S18_SourceTableDetails__M11_BillingMode(var_billingMode));
         }
         public static Amazon.DynamoDBv2.Model.SourceTableFeatureDetails FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S25_SourceTableFeatureDetails(software.amazon.cryptography.services.dynamodb.internaldafny.types._ISourceTableFeatureDetails value)
         {
@@ -9002,7 +9002,7 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types
         {
 
 
-            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.Endpoint(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S8_Endpoint__M7_Address(value.Address), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S8_Endpoint__M20_CachePeriodInMinutes(value.CachePeriodInMinutes));
+            return new software.amazon.cryptography.services.dynamodb.internaldafny.types.Endpoint(ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S8_Endpoint__M7_Address(value.Address), ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S8_Endpoint__M20_CachePeriodInMinutes((long)value.CachePeriodInMinutes));
         }
         public static Amazon.DynamoDBv2.ExportStatus FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S12_ExportStatus(software.amazon.cryptography.services.dynamodb.internaldafny.types._IExportStatus value)
         {

ComAmazonawsKms/runtimes/net/AWS-KMS.csproj

@@ -59,8 +59,8 @@
   <ItemGroup>
     <PackageReference Include="DafnyRuntime" Version="[4.2.0,$(DafnyVersion)]" />
     <!-- See https://learn.microsoft.com/en-us/nuget/concepts/package-versioning?tabs=semver20sort#version-ranges   -->
-    <PackageReference Include="AWSSDK.Core" Version="[3.7.*, 4.0)" />
-    <PackageReference Include="AWSSDK.KeyManagementService" Version="[3.7.*, 4.0)" />
+    <PackageReference Include="AWSSDK.Core" Version="4.0.*" />
+    <PackageReference Include="AWSSDK.KeyManagementService" Version="4.0.*" />
     <ProjectReference Include="../../../StandardLibrary/runtimes/net/STD.csproj" />
     <!--
       System.Collections.Immutable can be removed once dafny.msbuild is updated with

ComAmazonawsKms/runtimes/net/Extern/KMSClient.cs

@@ -120,7 +120,16 @@ public override Task<T> InvokeAsync<T>(IExecutionContext executionContext)
             private static void AddUserAgent(IExecutionContext executionContext)
             {
                 var request = executionContext.RequestContext.Request;
-                request.Headers[AWSSDKUtils.UserAgentHeader] += UserAgentSuffix;
+                // Check for User - Agent header and add to it.
+                if (request.Headers.ContainsKey(AWSSDKUtils.UserAgentHeader))
+                {
+                    request.Headers[AWSSDKUtils.UserAgentHeader] += " " + UserAgentSuffix;
+                }
+                else
+                {
+                    // Create new User-Agent header
+                    request.Headers[AWSSDKUtils.UserAgentHeader] = UserAgentSuffix;
+                }
             }
         }
     }