Fix duvet annotation after nits in specs

rishav-karanjit · rishav-karanjit · commit dff2be691487 · 2024-05-06T08:32:47.000-07:00
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy
@@ -53,7 +53,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
     match input.input
     {
       //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
-      //# - If the input is a encrypted DynamoDB item, it MUST attempt to extract "aws_dbe_head" attribute from the DynamoDB item to get binary header.
+      //# - If the input is an encrypted DynamoDB item, it MUST attempt to extract "aws_dbe_head" attribute from the DynamoDB item to get the binary header.
       case item(item) =>{
         :- Need("aws_dbe_head" in item && item["aws_dbe_head"].B?, E("Header not found in the DynamoDB item."));
         header := item["aws_dbe_head"].B;

Original file line number	Diff line number	Diff line change
`@@ -53,7 +53,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt`
`53`	`53`	`match input.input`
`54`	`54`	`{`
`55`	`55`	`//= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior`
`56`		`- //# - If the input is a encrypted DynamoDB item, it MUST attempt to extract "aws_dbe_head" attribute from the DynamoDB item to get binary header.`
	`56`	`+ //# - If the input is an encrypted DynamoDB item, it MUST attempt to extract "aws_dbe_head" attribute from the DynamoDB item to get the binary header.`
`57`	`57`	`case item(item) =>{`
`58`	`58`	`:- Need("aws_dbe_head" in item && item["aws_dbe_head"].B?, E("Header not found in the DynamoDB item."));`
`59`	`59`	`header := item["aws_dbe_head"].B;`