Consider removing Client Side Validation for AWS SDK Service Operations

[texastony]

User Story

As a Smithy-Dafny user,
I do not want to enforce AWS Services' server side validations
in my Smithy-Dafny generated clients,
as that makes the clients brittle to Service changes.

Details

The Smithy Models parsed by Smithy-Dafny MUST support
some "client-side" constraints on user input,
such as @required.

But these user input validations SHOULD NOT
be applied to the responses of AWS SDK Services,
and it is questionable if the requests to AWS SDK Services
need any of these of validations as well.

(I believe) The Smithy Specification designates what
constraints/validations should be applied client side,
and which should be left to the server.

For non-local services,
Smithy-Dafny should follow this guidance.

Example

Some Dafny code that is likely unnecessary:

    var maybeReEncryptResponse := kmsClient.ReEncrypt(reEncryptRequest);
    var reEncryptResponse :- maybeReEncryptResponse
    .MapFailure(e => Types.ComAmazonawsKms(ComAmazonawsKms := e));

    :- Need(
      && reEncryptResponse.CiphertextBlob.Some?
      && KMS.IsValid_CiphertextType(reEncryptResponse.CiphertextBlob.value),
      Types.KeyManagementException(
        message := "Invalid response from AWS KMS ReEncrypt: Invalid ciphertext.")
    );

It is very hard to imagine that KMS would return an invalid ciphertext.

Alternative

If Smithy-Dafny wants to continue enforce client side validation
for AWS Service requests and responses,
Smithy-Dafny may want to consider generating additional Error
shapes for AWS Service's: InvalidRequestException & InvalidResponseException.

These can be used to clearly signal to the Dafny developers
writing logic that it was local validation that failed
as compared to server side.

[texastony]

I think I am going to use the Alternative to unblock me.

I have created KeyManagementException as a catch all for
either request or response validation errors.

Then,
I can create:

  type KmsError = e: Types.Error | (e.ComAmazonawsKms? || e.KeyManagementException?) witness *

Any methods that call KMS can return KmsError as the failure type,
and the business logic does not need to un-wrap the Local Service error,
Types.Error,
to understand if it is Server Side or Client Side validation that failed the request.

[robin-aws]

I think it depends on how you're using the Dafny service SDK. If you're using it in production code, you will want the client to follow the Smithy specification and bias for returning a response even if it's invalid according to the model. But it can also be useful to assume all responses are valid and explicitly catch cases when they are not, if you're using Dafny to test if the service always behaves according to its model. So I think this should eventually at least be a configuration option, even if the default should probably be the first mode.

Will your alternative involve having smithy-dafny emit that KeyManagementException type itself, or can you safely add that in the MPL instead?

[texastony]

I just added it to the MPL,
in my branch.

Which allows me to distinguish between KMS Errors,
which maybe opaque and access denied,
or our potentially overzealous client side validation.

See aws/aws-cryptographic-material-providers-library@8f17d17

[rishav-karanjit]

Will polymorph not validating aws sdk shape cause any issue?

Our polymoph code does not validate the SDK shapes and we assume it will be validated by AWS SDK. One such example is this PutItemInputTransformInput structure in DBESDK. In Java, the constraints inside PutItemInput of PutItemInputTransformInput is never validated (example of PutItemInputTransformInput class) and this MUST be validated by AWS SDK. Our Dafny proofs which assumes PutItemInput in PutItemInputTransformInput is valid is not true because we don't check constraint of PutItemInput before converting native to dafny.

[robin-aws]

Strongly related: #751