chore(RSA): limit RSA Key Gen to 4096 bits

[texastony]

Issue #, if available: N/A

Description of changes:

• Limit RSA Key Generation input to 4096 bits

This does NOT impact the public behavior of the ESDK in any way.

The RSA Key Generator is ONLY used for testing.

4096 is the largest RSA Key size KMS supports.

Squash/merge commit message, if applicable: chore(RSA): limit RSA Key Gen to 4096 bits

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

Due to dafny-lang/dafny#2500, Traits are dangerous:

1. Does this PR add any traits or classes that extend a trait?
2. Are these traits annotated with {:termination false}?

The override checks on
the specifications on
a class' functions/methods/etc. validating
that specifications are
at least as strong as those on
the traits it implements
are not working correctly when
that trait is defined in a different module
(and hence must have {:termination false} on it).

As such, if either (1.) or (2.) is true:

• manually verified all the trait specifications are copied onto classes that extend them?

[robin-aws]

The fact that CI accepted this without any failures is a big problem.

[robin-aws]

Thinking more deeply beyond the initial reaction (just wanted to block the PR in case): is this all we need to do because all callers of the method already satisfy this precondition? I was worried about this being indirectly callable from outside Dafny.

[texastony]

In response to @robin-aws concerns,
I am putting this into Draft.

[texastony]

4096 is the KMS Max, so we are going to refactor to that.
RSA is substantially slower at any key size greater than this.

[robin-aws]

Concerns put to rest - I managed to miss the fact that this existing in src but is only called from test code.