Use @smithy.test#smokeTests in test models (was: Add tests to verify how AWS SDKs handle optional types)

[seebees]

In the .NET SDK an optional value is stored privately as null.
There is also a private IsSet method that will identify if the value is set or not.

The .NET SDK will return never return null.
If you create a DDB input with Limit for example, but do not set the Limit value,
the underlying value will be null.
However, if you try and get this value, you will not get null you will get 0.

We should add a test model to check this.
Since it is likely to come up in other languages.

[texastony]

Internally,
we tracked this as CrypTool-5098,
which I will now resolve in favor of this Issue.

A similar edge case was addressed in Java via #191.

Additionally,
any Test Model we add to address this
will require Native (or Extern) code.

The request MUST originate on the Native side,
and then MUST be passed to Dafny,
for us to assert that the ToDafny conversion
respects unset values.

[robin-aws]

A great trait for this was just added to the Smithy specification: https://smithy.io/2.0/additional-specs/smoke-tests.html#smoketests-trait

The trait defines simple requests to send to a service and an assertion that the operation either succeeds or fails. This is fairly ideal for testing constraints such as @required in test models:

@aws.polymorph#localService(
  sdkId: "SimpleConstraints",
  config: SimpleConstraintsConfig,
)
service SimpleConstraints {
  version: "2021-11-01",
  resources: [],
  operations: [ GetConstraints ],
  errors: [ SimpleConstraintsException ],
}

@smithy.test#smokeTests(
    [
        {
            id: "PresentSuccess"
            params: {mustBePresent: "No problem"}
            expect: {
                success: {}
            }
        }
        {
            id: "AbsenceError"
            params: {}
            expect: {
                failure: {}
            }
        }
    ]
)
operation GetConstraints {
  input: GetConstraintsInput,
  output: GetConstraintsOutput,
}

structure GetConstraintsInput {
  @required mustBePresent: String
}

...

The key difference between this testing method and Dafny-based tests: the params document can specify invalid data, which Dafny code can't given that we embed constraint traits into verified preconditions/non-optional types/subset types/etc.

There is extra code generation to implement to generate target language shape values. For Java, for example, the tests should become something like (not even attempting to get the smithy-generated Java API exactly right):

  @Test
  public void PresentSuccess() {
    ConstraintsClient client = ...;
    GetConstraintsInput input = GetConstraintsInput.Builder()
      .mustBePresent("No problem")
      .build();
    GetConstraintsResult result = client.GetConstraints(input);
    assertTrue(result.isSuccess());
  }

  @Test
  public void AbsenceError() {
    ConstraintsClient client = ...;
    GetConstraintsInput input = GetConstraintsInput.Builder()
      .build();
    GetConstraintsResult result = client.GetConstraints(input);
    assertTrue(result.isError());
  }

[robin-aws]

Renamed the title to better reflect the scope of the solution: we can test constraints effectively with this for both local services and SDKs, and really anything where Dafny-based testing isn't as effective.