fix(go): enum and map in type conversion

[rishav-karanjit]

Issue:

Background: Some aws-sdk shapes can be non pointer variable even if it does not have a required trait.

Actual Issue:

1. If a aws-sdk shape is a non pointer variable and is not required, enum shape defaults to "" because in Go default value for string is "". However, if it defaults to "", based on my type conversion function enum will be set to one of enum constant which is wrong.
2. Map shape in ToDafny does isPointer check to do to do the nil check . However, mapShape never gets isPointer = True because mapShape can be nil and is never generated with pointer. So, this isPointer check is never executed. Since, this isPointer check map defaults to map[] but it should default to nil .Note: dafnyMap is a structure which cannot be nil. So, this is generated as wrapper optional if its not required.

Description of changes:

• This PR adds a if check for it and sets the dafny variable to none if none of the enums matched.
• Added nilCheck inside isOptional check and removed nil check

Callouts
MPL PR to see the diff: aws/aws-cryptographic-material-providers-library#1285
ESDK PR to see if the examples panics or not: aws/aws-encryption-sdk#754

This PR will brings code changes in MPL which is already released. But, this code change does not impact customer at all. The reason customer is not impact is because:

1. We take a specific shape (Like com.amazonaws.dynamodb#TableName) from customers but not the whole operation (like com.amazonaws.dynamodb#GetItemInput). So, we never use the function in type conversion layer that has been changed in MPL.

2. We explicitly assign None those shapes which we don't use. So, we never allow the type conversion layer default value issue impact the customers. Examples of this:

   • DecryptInput.EncryptionAlgorithm

   var decryptInput := Kms.Types.DecryptRequest(
         CiphertextBlob := CiphertextBlob.value,
         EncryptionContext := input.EncryptionContext,
         GrantTokens := input.GrantTokens,
         KeyId := Kms.Wrappers.Some(KeyId.value),
         EncryptionAlgorithm := Kms.Wrappers.None
       );
   

   • GenerateDataKeyRequest.KeySpec

   var generatorRequest := KMS.GenerateDataKeyRequest(
           EncryptionContext := Some(stringifiedEncCtx),
           GrantTokens := Some(grantTokens),
           KeyId := awsKmsKey,
           NumberOfBytes := Some(AlgorithmSuites.GetEncryptKeyLength(suite)),
           KeySpec := None
         );
   

   • GenerateDataKeyWithoutPlaintextRequest.KeySpec

   var generatorRequest := KMS.GenerateDataKeyWithoutPlaintextRequest(
         KeyId := kmsKeyArn,
         EncryptionContext := Some(encryptionContext),
         KeySpec := None,
         NumberOfBytes := Some(32),
         GrantTokens := Some(grantTokens)
       );
   

   • DDB GetItemInput

   DDB.GetItemInput(
         Key := dynamoDbKey,
         TableName := tableName,
         AttributesToGet := None,
         ConsistentRead :=  None,
         ReturnConsumedCapacity := None,
         ProjectionExpression := None,
         ExpressionAttributeNames := None
       );
   

   • DDB TransactWriteItem

   DDB.TransactWriteItem(
         ConditionCheck := None,
         Put := Some(
           DDB.Put(
             Item := item,
             TableName := tableName,
             ConditionExpression := Some(
               match conditionExpression
               case BRANCH_KEY_NOT_EXIST() => BRANCH_KEY_NOT_EXIST_CONDITION
               case BRANCH_KEY_EXISTS() => BRANCH_KEY_EXISTS_CONDITION
             ),
             ExpressionAttributeNames := Some(BRANCH_KEY_EXISTS_EXPRESSION_ATTRIBUTE_NAMES),
             ExpressionAttributeValues := None,
             ReturnValuesOnConditionCheckFailure := None)),
         Delete := None,
         Update := None
       )
   

   • TransactWriteItemsInput

   var transactRequest := DDB.TransactWriteItemsInput(
         TransactItems := items,
         ReturnConsumedCapacity := None,
         ReturnItemCollectionMetrics := None,
         ClientRequestToken := None
       );
   

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[ShubhamChaturvedi7]

Let's be defensive and error out in case of it being required and not matching an enum value.

[rishav-karanjit]

There was a chance where this input could have been defaulted to a value. This specific case is also fine (in a wrong way but still fine.)

• For enums we iterate on length of kmstypes.EncryptionAlgorithmSpec (this comes from go sdk) and its length if 4 and we set the index.
• On second loop, we iterate based on dafny shape ComAmazonawsKmsTypes.EncryptionAlgorithmSpec which only has 3 values (Not 4). Since go sdk shape has 4 values but dafny has only 3 enum will be set into none (luckily).
  (edited)
• The error we get after not sending the encryption algorithm spec is from here: https://github.com/aws/aws-cryptographic-material-providers-library/blob/main/AwsC[…]ialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy