Skip to content

Commit d83759a

Browse files
ajewellamzajewellamz
committed
chore: make EncodeAscii ghost
1 parent f6ef3f4 commit d83759a

File tree

14 files changed

+223
-63
lines changed

14 files changed

+223
-63
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy

+6-1
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,11 @@ module TestBaseBeacon {
1818
import DDB = ComAmazonawsDynamodbTypes
1919
import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
2020

21+
const x123 : UTF8.ValidUTF8Bytes :=
22+
var s := [0x31, 0x32, 0x33];
23+
assert s == UTF8.EncodeAscii("123");
24+
s
25+
2126
method {:test} TestBeacon() {
2227
var primitives :- expect Primitives.AtomicPrimitives();
2328

@@ -31,7 +36,7 @@ module TestBaseBeacon {
3136
expect bytes[7] == 0x80;
3237
str :- expect b.hash([], key := [1,2]);
3338
expect str == "80";
34-
bytes :- expect bb.getHmac(UTF8.EncodeAscii("123"), key := [1,2]);
39+
bytes :- expect bb.getHmac(x123, key := [1,2]);
3540
expect bytes[7] == 0x61;
3641
}
3742

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbEncryptionBranchKeyIdSupplierTest.dfy

+22-4
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,12 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest {
2727

2828
// These tests require a keystore populated with a key with this Id
2929
const BRANCH_KEY_ID := "75789115-1deb-4fe3-a2ec-be9e885d1945"
30-
const BRANCH_KEY_ID_UTF8 := UTF8.EncodeAscii(BRANCH_KEY_ID)
30+
31+
const BRANCH_KEY_ID_UTF8 : UTF8.ValidUTF8Bytes :=
32+
var s := [0x37, 0x35, 0x37, 0x38, 0x39, 0x31, 0x31, 0x35, 0x2d, 0x31, 0x64, 0x65, 0x62, 0x2d, 0x34, 0x66, 0x65, 0x33, 0x2d, 0x61, 0x32, 0x65, 0x63, 0x2d, 0x62, 0x65, 0x39, 0x65, 0x38, 0x38, 0x35, 0x64, 0x31, 0x39, 0x34, 0x35];
33+
assert s == UTF8.EncodeAscii(BRANCH_KEY_ID);
34+
s
35+
3136
const ALTERNATE_BRANCH_KEY_ID := "4bb57643-07c1-419e-92ad-0df0df149d7c"
3237

3338
// Constants for TestBranchKeySupplier
@@ -41,10 +46,23 @@ module DynamoDbEncryptionBranchKeyIdSupplierTest {
4146
const CASE_B_BYTES: seq<uint8> := STRING_TYPE_ID + [0x43, 0x41, 0x53, 0x45, 0x5f, 0x42]
4247
const BRANCH_KEY_ID_A := BRANCH_KEY_ID
4348
const BRANCH_KEY_ID_B := ALTERNATE_BRANCH_KEY_ID
44-
const EC_PARTITION_NAME := UTF8.EncodeAscii("aws-crypto-partition-name")
49+
50+
const EC_PARTITION_NAME : UTF8.ValidUTF8Bytes :=
51+
var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x70, 0x61, 0x72, 0x74, 0x69, 0x74, 0x69, 0x6f, 0x6e, 0x2d, 0x6e, 0x61, 0x6d, 0x65];
52+
assert s == UTF8.EncodeAscii("aws-crypto-partition-name");
53+
s
54+
4555
const RESERVED_PREFIX := "aws-crypto-attr."
46-
const KEY_ATTR_NAME := UTF8.EncodeAscii(RESERVED_PREFIX + BRANCH_KEY)
47-
const BRANCH_KEY_NAME := UTF8.EncodeAscii(BRANCH_KEY)
56+
57+
const KEY_ATTR_NAME : UTF8.ValidUTF8Bytes :=
58+
var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x61, 0x74, 0x74, 0x72, 0x2e, 0x62, 0x72, 0x61, 0x6e, 0x63, 0x68, 0x4b, 0x65, 0x79];
59+
assert s == UTF8.EncodeAscii(RESERVED_PREFIX + BRANCH_KEY);
60+
s
61+
62+
const BRANCH_KEY_NAME : UTF8.ValidUTF8Bytes :=
63+
var s := [0x62, 0x72, 0x61, 0x6e, 0x63, 0x68, 0x4b, 0x65, 0x79];
64+
assert s == UTF8.EncodeAscii(BRANCH_KEY);
65+
s
4866

4967
method {:test} {:vcs_split_on_every_assert} TestHappyCase()
5068
{

‎DynamoDbEncryption/dafny/DynamoDbEncryption/test/DynamoDbGetEncryptedDataKeyDescriptionTest.dfy

+43-8
Original file line numberDiff line numberDiff line change
@@ -14,20 +14,55 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
1414
import EdkWrapping
1515
import AlgorithmSuites
1616

17+
const abc : UTF8.ValidUTF8Bytes :=
18+
var s := [0x61, 0x62, 0x63];
19+
assert s == UTF8.EncodeAscii("abc");
20+
s
21+
22+
const def : UTF8.ValidUTF8Bytes :=
23+
var s := [0x64, 0x65, 0x66];
24+
assert s == UTF8.EncodeAscii("def");
25+
s
26+
27+
const awskms : UTF8.ValidUTF8Bytes :=
28+
var s := [0x61, 0x77, 0x73, 0x2d, 0x6b, 0x6d, 0x73];
29+
assert s == UTF8.EncodeAscii("aws-kms");
30+
s
31+
32+
const keyproviderInfo : UTF8.ValidUTF8Bytes :=
33+
var s := [0x6b, 0x65, 0x79, 0x70, 0x72, 0x6f, 0x76, 0x69, 0x64, 0x65, 0x72, 0x49, 0x6e, 0x66, 0x6f];
34+
assert s == UTF8.EncodeAscii("keyproviderInfo");
35+
s
36+
37+
const aws_kms_hierarchy : UTF8.ValidUTF8Bytes :=
38+
var s := [0x61, 0x77, 0x73, 0x2d, 0x6b, 0x6d, 0x73, 0x2d, 0x68, 0x69, 0x65, 0x72, 0x61, 0x72, 0x63, 0x68, 0x79];
39+
assert s == UTF8.EncodeAscii("aws-kms-hierarchy");
40+
s
41+
42+
const raw_rsa : UTF8.ValidUTF8Bytes :=
43+
var s := [0x72, 0x61, 0x77, 0x2d, 0x72, 0x73, 0x61];
44+
assert s == UTF8.EncodeAscii("raw-rsa");
45+
s
46+
47+
const aws_kms_rsa : UTF8.ValidUTF8Bytes :=
48+
var s := [0x61, 0x77, 0x73, 0x2d, 0x6b, 0x6d, 0x73, 0x2d, 0x72, 0x73, 0x61];
49+
assert s == UTF8.EncodeAscii("aws-kms-rsa");
50+
s
51+
1752
// THIS IS A TESTING RESOURCE DO NOT USE IN A PRODUCTION ENVIRONMENT
1853
const testVersion : Version := 1
1954
const testFlavor0 : Flavor := 0
2055
const testFlavor1 : Flavor := 1
2156
const testMsgID : MessageID := [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32]
2257
const testLegend : Legend := [0x65, 0x73]
23-
const testEncContext : CMPEncryptionContext := map[EncodeAscii("abc") := EncodeAscii("def")]
58+
const testEncContext : CMPEncryptionContext := map[abc := def]
2459
const testAwsKmsDataKey := CMP.EncryptedDataKey(
25-
keyProviderId := EncodeAscii("aws-kms") ,
26-
keyProviderInfo := EncodeAscii("keyproviderInfo"),
60+
keyProviderId := awskms ,
61+
keyProviderInfo := keyproviderInfo,
2762
ciphertext := [1, 2, 3, 4, 5])
2863
const testAwsKmsHDataKey := CMP.EncryptedDataKey(
29-
keyProviderId := EncodeAscii("aws-kms-hierarchy") ,
30-
keyProviderInfo := EncodeAscii("keyproviderInfo"),
64+
keyProviderId := aws_kms_hierarchy,
65+
keyProviderInfo := keyproviderInfo,
3166
ciphertext := [
3267
64, 92, 115, 7, 85, 121, 112, 79, 69, 12, 82, 25, 67, 34,
3368
11, 66, 93, 45, 40, 23, 90, 61, 16, 28, 59, 114, 52, 122,
@@ -40,12 +75,12 @@ module DynamoDbGetEncryptedDataKeyDescriptionTest {
4075
114, 76, 18, 103, 84, 34, 123, 1, 125, 61, 33, 13, 18, 81,
4176
24, 53, 53, 26, 60, 52, 85, 81, 96, 85, 72])
4277
const testRawRsaDataKey := CMP.EncryptedDataKey(
43-
keyProviderId := EncodeAscii("raw-rsa") ,
78+
keyProviderId := raw_rsa,
4479
keyProviderInfo := [1, 2, 3, 4, 5],
4580
ciphertext := [6, 7, 8, 9])
4681
const testAwsKmsRsaDataKey := CMP.EncryptedDataKey(
47-
keyProviderId := EncodeAscii("aws-kms-rsa") ,
48-
keyProviderInfo := EncodeAscii("keyproviderInfo"),
82+
keyProviderId := aws_kms_rsa,
83+
keyProviderInfo := keyproviderInfo,
4984
ciphertext := [1, 2, 3, 4, 5])
5085

5186
method CreatePartialHeader(version : Version, flavor : Flavor, msgID : MessageID, legend : Legend, encContext : CMPEncryptionContext, dataKeyList : CMPEncryptedDataKeyList)

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy

+4-1
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,10 @@ module DynamoDbMiddlewareSupport {
121121
.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e))
122122
}
123123

124-
const HierarchicalKeyringId := UTF8.EncodeAscii("aws-kms-hierarchy")
124+
const HierarchicalKeyringId : UTF8.ValidUTF8Bytes :=
125+
var s := [0x61, 0x77, 0x73, 0x2d, 0x6b, 0x6d, 0x73, 0x2d, 0x68, 0x69, 0x65, 0x72, 0x61, 0x72, 0x63, 0x68, 0x79];
126+
assert s == UTF8.EncodeAscii("aws-kms-hierarchy");
127+
s
125128

126129
// Return Beacon Key ID for use in beaconizing records to be written
127130
function method GetKeyIdFromHeader(config : ValidTableConfig, output : AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.EncryptItemOutput) :

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy

+14-3
Original file line numberDiff line numberDiff line change
@@ -35,9 +35,20 @@ module DynamoDbItemEncryptorUtil {
3535
x < y
3636
}
3737

38-
const TABLE_NAME : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("aws-crypto-table-name")
39-
const PARTITION_NAME : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("aws-crypto-partition-name")
40-
const SORT_NAME : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("aws-crypto-sort-name")
38+
const TABLE_NAME : UTF8.ValidUTF8Bytes :=
39+
var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x74, 0x61, 0x62, 0x6c, 0x65, 0x2d, 0x6e, 0x61, 0x6d, 0x65];
40+
assert s == UTF8.EncodeAscii("aws-crypto-table-name");
41+
s
42+
43+
const PARTITION_NAME : UTF8.ValidUTF8Bytes :=
44+
var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x70, 0x61, 0x72, 0x74, 0x69, 0x74, 0x69, 0x6f, 0x6e, 0x2d, 0x6e, 0x61, 0x6d, 0x65];
45+
assert s == UTF8.EncodeAscii("aws-crypto-partition-name");
46+
s
47+
48+
const SORT_NAME : UTF8.ValidUTF8Bytes :=
49+
var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x73, 0x6f, 0x72, 0x74, 0x2d, 0x6e, 0x61, 0x6d, 0x65];
50+
assert s == UTF8.EncodeAscii("aws-crypto-sort-name");
51+
s
4152

4253
const SELECTOR_TABLE_NAME : DDB.AttributeName := "aws_dbe_table_name"
4354
const SELECTOR_PARTITION_NAME : DDB.AttributeName := "aws_dbe_partition_name"

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy

+4-1
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,10 @@ module DynamoDbItemEncryptorTest {
2525
// encrypt => encrypted fields changed, others did not
2626
// various errors
2727

28-
const PublicKeyUtf8 : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("aws-crypto-public-key")
28+
const PublicKeyUtf8 : UTF8.ValidUTF8Bytes :=
29+
var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x70, 0x75, 0x62, 0x6c, 0x69, 0x63, 0x2d, 0x6b, 0x65, 0x79];
30+
assert s == UTF8.EncodeAscii("aws-crypto-public-key");
31+
s
2932

3033
function method DDBS(x : string) : DDB.AttributeValue {
3134
DDB.AttributeValue.S(x)

‎DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy

+16-4
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,11 @@ module StructuredEncryptionCrypt {
4949
keyR.MapFailure(e => AwsCryptographyPrimitives(e))
5050
}
5151

52+
const AwsDbeField : UTF8.ValidUTF8Bytes :=
53+
var s := [0x41, 0x77, 0x73, 0x44, 0x62, 0x65, 0x46, 0x69, 0x65, 0x6c, 0x64];
54+
assert s == UTF8.EncodeAscii("AwsDbeField");
55+
s
56+
5257
function method FieldKeyNonce(offset : uint32)
5358
: (ret : Bytes)
5459
ensures |ret| == 16 // NOT NonceSize
@@ -61,17 +66,24 @@ module StructuredEncryptionCrypt {
6166
//# | 0x2c | 1 | 44, the length of the eventual FieldKey |
6267
//# | offset | 4 | 32 bit integer representation of offset |
6368
ensures ret ==
64-
UTF8.EncodeAscii("AwsDbeField")
69+
AwsDbeField
6570
+ [(KeySize+NonceSize) as uint8]
6671
+ UInt32ToSeq(offset)
6772
{
68-
UTF8.EncodeAscii("AwsDbeField")
73+
AwsDbeField
6974
+ [(KeySize+NonceSize) as uint8] // length
7075
+ UInt32ToSeq(offset)
7176
}
7277

73-
const LABEL_COMMITMENT_KEY := UTF8.EncodeAscii("AWS_DBE_COMMIT_KEY")
74-
const LABEL_ENCRYPTION_KEY := UTF8.EncodeAscii("AWS_DBE_DERIVE_KEY")
78+
const LABEL_COMMITMENT_KEY : UTF8.ValidUTF8Bytes :=
79+
var s := [0x41, 0x57, 0x53, 0x5f, 0x44, 0x42, 0x45, 0x5f, 0x43, 0x4f, 0x4d, 0x4d, 0x49, 0x54, 0x5f, 0x4b, 0x45, 0x59];
80+
assert s == UTF8.EncodeAscii("AWS_DBE_COMMIT_KEY");
81+
s
82+
83+
const LABEL_ENCRYPTION_KEY : UTF8.ValidUTF8Bytes :=
84+
var s := [0x41, 0x57, 0x53, 0x5f, 0x44, 0x42, 0x45, 0x5f, 0x44, 0x45, 0x52, 0x49, 0x56, 0x45, 0x5f, 0x4b, 0x45, 0x59];
85+
assert s == UTF8.EncodeAscii("AWS_DBE_DERIVE_KEY");
86+
s
7587

7688
// suitable for header field
7789
method GetCommitKey(

‎DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy

+18-6
Original file line numberDiff line numberDiff line change
@@ -140,16 +140,28 @@ module StructuredEncryptionFooter {
140140
}
141141
}
142142

143+
const ENCRYPTED : UTF8.ValidUTF8Bytes :=
144+
var s := [0x45, 0x4e, 0x43, 0x52, 0x59, 0x50, 0x54, 0x45, 0x44];
145+
assert s == UTF8.EncodeAscii("ENCRYPTED");
146+
s
147+
148+
const PLAINTEXT : UTF8.ValidUTF8Bytes :=
149+
var s := [0x50, 0x4c, 0x41, 0x49, 0x4e, 0x54, 0x45, 0x58, 0x54];
150+
assert s == UTF8.EncodeAscii("PLAINTEXT");
151+
s
152+
153+
154+
143155
// Given a StructuredDataTerminal, return the canonical value for the type, for use in the footer checksum calculations
144156
function method GetCanonicalType(value : StructuredDataTerminal, isEncrypted : bool)
145157
: Result<Bytes, Error>
146158
{
147159
if isEncrypted then
148160
:- Need(2 <= |value.value| < UINT64_LIMIT, E("Bad length."));
149-
Success(UInt64ToSeq((|value.value| - 2) as uint64) + UTF8.EncodeAscii("ENCRYPTED"))
161+
Success(UInt64ToSeq((|value.value| - 2) as uint64) + ENCRYPTED)
150162
else
151163
:- Need(|value.value| < UINT64_LIMIT, E("Bad length."));
152-
Success(UInt64ToSeq((|value.value|) as uint64) + UTF8.EncodeAscii("PLAINTEXT") + value.typeId)
164+
Success(UInt64ToSeq((|value.value|) as uint64) + PLAINTEXT + value.typeId)
153165
}
154166

155167
function method GetCanonicalEncryptedField(fieldName : CanonicalPath, value : StructuredDataTerminal)
@@ -169,14 +181,14 @@ module StructuredEncryptionFooter {
169181
&& ret.value ==
170182
fieldName
171183
+ UInt64ToSeq((|value.value| - 2) as uint64)
172-
+ UTF8.EncodeAscii("ENCRYPTED")
184+
+ ENCRYPTED
173185
+ value.value // this is 2 bytes of unencrypted type, followed by encrypted value
174186
{
175187
:- Need(2 <= |value.value| < UINT64_LIMIT, E("Bad length."));
176188
Success(
177189
fieldName
178190
+ UInt64ToSeq((|value.value| - 2) as uint64)
179-
+ UTF8.EncodeAscii("ENCRYPTED")
191+
+ ENCRYPTED
180192
+ value.value
181193
)
182194
}
@@ -198,15 +210,15 @@ module StructuredEncryptionFooter {
198210
&& ret.value ==
199211
fieldName
200212
+ UInt64ToSeq((|value.value|) as uint64)
201-
+ UTF8.EncodeAscii("PLAINTEXT")
213+
+ PLAINTEXT
202214
+ value.typeId
203215
+ value.value
204216
{
205217
:- Need(|value.value| < UINT64_LIMIT, E("Bad length."));
206218
Success(
207219
fieldName
208220
+ UInt64ToSeq((|value.value|) as uint64)
209-
+ UTF8.EncodeAscii("PLAINTEXT")
221+
+ PLAINTEXT
210222
+ value.typeId
211223
+ value.value
212224
)

‎DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy

+34-8
Original file line numberDiff line numberDiff line change
@@ -26,23 +26,48 @@ module StructuredEncryptionUtil {
2626
const FooterPath : Path := [member(StructureSegment(key := FooterField))]
2727
const HeaderPaths : seq<Path> := [HeaderPath, FooterPath]
2828
const ReservedCryptoContextPrefixString := "aws-crypto-"
29-
const ReservedCryptoContextPrefixUTF8 := UTF8.EncodeAscii(ReservedCryptoContextPrefixString)
29+
30+
const ReservedCryptoContextPrefixUTF8 : UTF8.ValidUTF8Bytes :=
31+
var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d];
32+
assert s == UTF8.EncodeAscii(ReservedCryptoContextPrefixString);
33+
s
3034

3135
const ATTR_PREFIX := ReservedCryptoContextPrefixString + "attr."
32-
const EC_ATTR_PREFIX : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii(ATTR_PREFIX)
36+
37+
const EC_ATTR_PREFIX : UTF8.ValidUTF8Bytes :=
38+
var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x61, 0x74, 0x74, 0x72, 0x2e];
39+
assert s == UTF8.EncodeAscii(ATTR_PREFIX);
40+
s
41+
3342
const LEGEND := ReservedCryptoContextPrefixString + "legend"
34-
const LEGEND_UTF8 : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii(LEGEND)
43+
44+
const LEGEND_UTF8 : UTF8.ValidUTF8Bytes :=
45+
var s := [0x61, 0x77, 0x73, 0x2d, 0x63, 0x72, 0x79, 0x70, 0x74, 0x6f, 0x2d, 0x6c, 0x65, 0x67, 0x65, 0x6e, 0x64];
46+
assert s == UTF8.EncodeAscii(LEGEND);
47+
s
48+
3549
const LEGEND_STRING : char := 'S'
3650
const LEGEND_NUMBER : char := 'N'
3751
const LEGEND_LITERAL : char := 'L'
3852
const LEGEND_BINARY : char := 'B'
3953

4054
const NULL_STR : string := "null"
41-
const NULL_UTF8 : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii(NULL_STR)
55+
const NULL_UTF8 : UTF8.ValidUTF8Bytes :=
56+
var s := [0x6e, 0x75, 0x6c, 0x6c];
57+
assert s == UTF8.EncodeAscii(NULL_STR);
58+
s
59+
4260
const TRUE_STR : string := "true"
43-
const TRUE_UTF8 : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii(TRUE_STR)
61+
const TRUE_UTF8 : UTF8.ValidUTF8Bytes :=
62+
var s := [0x74, 0x72, 0x75, 0x65];
63+
assert s == UTF8.EncodeAscii(TRUE_STR);
64+
s
65+
4466
const FALSE_STR : string := "false"
45-
const FALSE_UTF8 : UTF8.ValidUTF8Bytes := UTF8.EncodeAscii(FALSE_STR)
67+
const FALSE_UTF8 : UTF8.ValidUTF8Bytes :=
68+
var s := [0x66, 0x61, 0x6c, 0x73, 0x65];
69+
assert s == UTF8.EncodeAscii(FALSE_STR);
70+
s
4671

4772
datatype CanonCryptoItem = CanonCryptoItem (
4873
key : CanonicalPath,
@@ -290,9 +315,10 @@ module StructuredEncryptionUtil {
290315
//# where `typeId` is the attribute's [type ID](./ddb-attribute-serialization.md#type-id)
291316
//# and `serializedValue` is the attribute's value serialized according to
292317
//# [Attribute Value Serialization](./ddb-attribute-serialization.md#attribute-value-serialization).
293-
ensures ret == UTF8.EncodeAscii(Base64.Encode(t.typeId + t.value))
318+
ensures ret == UTF8.Encode(Base64.Encode(t.typeId + t.value)).value
294319
{
295-
UTF8.EncodeAscii(Base64.Encode(t.typeId + t.value))
320+
var base := Base64.Encode(t.typeId + t.value);
321+
UTF8.Encode(base).value
296322
}
297323

298324
function method DecodeTerminal(t : UTF8.ValidUTF8Bytes) : (ret : Result<StructuredDataTerminal, string>)

‎DynamoDbEncryption/dafny/StructuredEncryption/test/HappyCaseTests.dfy

+11-1
Original file line numberDiff line numberDiff line change
@@ -13,12 +13,22 @@ module HappyCaseTests {
1313
import MaterialProviders
1414
import StructuredDataTestFixtures
1515

16+
const some : UTF8.ValidUTF8Bytes :=
17+
var s := [0x73, 0x6f, 0x6d, 0x65];
18+
assert s == UTF8.EncodeAscii("some");
19+
s
20+
21+
const value : UTF8.ValidUTF8Bytes :=
22+
var s := [0x76, 0x61, 0x6c, 0x75, 0x65];
23+
assert s == UTF8.EncodeAscii("value");
24+
s
25+
1626
method {:test} TestRoundTrip() {
1727
var structuredEncryption :-
1828
expect StructuredEncryption.StructuredEncryption(StructuredEncryption.DefaultStructuredEncryptionConfig());
1929
var cmm := StructuredDataTestFixtures.GetDefaultCMMWithKMSKeyring();
2030

21-
var encContext := map[UTF8.EncodeAscii("some") := UTF8.EncodeAscii("value")];
31+
var encContext := map[some := value];
2232
var algSuiteId := AlgorithmSuites.DBE_ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384_SYMSIG_HMAC_SHA384.id.DBE;
2333

2434
assert && structuredEncryption.ValidState();

0 commit comments

Comments
 (0)