Remove extra EC requirement from GetEncryptionMaterials in CMM interface

[lavaleri]

The CMM interface should not require that the EC on GetEncryptionMaterials not have the reserved keys, or require an EC that is serializable. This is because we do not specify all CMMs to have this requirement on inputs, and also because the Default CMM should be checking this dynamically anyway. Either the check logic needs to be in the shim code or in the dafny code, so we might as well put it in the dafny code and verify the expected behavior for particular inputs.

A result of this is that we no longer can statically verify that the DefaultCMM's EC does not have the reserved field. This is because a class implementing a method from an interface cannot have more restrictive preconditions than the interface. Instead we must dynamically check that the EC has those extra requirements, and decide what to do if the EC is not as we expect. This requires should be replaced by an ensures that makes sure the implementation performs the correct behavior.

[seebees]

Is this a candidate for expect @robin-aws ?

[robin-aws]

Possibly: depends on whether the API has to raise a specific type of error for this case, i.e. something that becomes a specific exception class that we document. If it does, we need to use Result<T> types and :- statements to propagate the error. expect is definitely simpler if not.