-
Notifications
You must be signed in to change notification settings - Fork 11
Description
In SmithyV2, enums can have values.
Attempting to add ListObjectsV2 to the S3 module does not “just” work. The culprit is this enum definition:
"com.amazonaws.s3#OptionalObjectAttributes": {
"type": "enum",
"members": {
"RESTORE_STATUS": {
"target": "smithy.api#Unit",
"traits": {
"smithy.api#enumValue": "RestoreStatus"
}
}
}
}
This enum breaks from the conventions followed by all other enums in the smithy-dafny AWS SDK ecosystem. The majority of enums, by convention, match their name and value (including all of the enums in KMS and DDB). Some enums diverge from this convention, but follow a more general rule; that the enum value may contain a non-standard delimiter which is replaced by the _ character, and thus match the name. For example:
"com.amazonaws.s3#ServerSideEncryption": {
"type": "enum",
"members": {
"AES256": {
"target": "smithy.api#Unit",
"traits": {
"smithy.api#enumValue": "AES256"
}
},
"aws_kms": {
"target": "smithy.api#Unit",
"traits": {
"smithy.api#enumValue": "aws:kms"
}
},
"aws_kms_dsse": {
"target": "smithy.api#Unit",
"traits": {
"smithy.api#enumValue": "aws:kms:dsse"
}
}
}
},
Or as in ObjectCannedACL:
"public_read": {
"target": "smithy.api#Unit",
"traits": {
"smithy.api#enumValue": "public-read"
}
},
During codegen, the non-standard delimiter is replaced with _ and so the names and values match.
In the case of RestoreStatus there is no delimiter so the names and values don’t match. This is a problem, because apparently the Dafny side of the AWS SDK codegen only ever uses the name, and the Python side only ever uses the (possibly edited) value.
There might be a simple band-aid fix; the dumbest of which is to merely treat RestoreStatus as a special case and replace it with RESTORE_STATUS in the Python AWS SDK codegen.
The better fix is to align use of names vs. values in general for AWS SDK codegen. So, what do other languages do?
Dafny
ComAmazonawsS3Types.dfy
datatype OptionalObjectAttributes =
| RESTORE_STATUS
Uses the name, not the value.
Python
dafny_to_aws_sdk.py
OptionalObjectAttributes_RestoreStatus
aws_sdk_to_dafny.py
OptionalObjectAttributes_RestoreStatus
Uses the value, unedited in this case.
(further investigation pending)