m

ajewellamz · lucasmcdonald3 · commit 81d8b26581cf · 2024-08-23T12:44:11.000-07:00
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy
@@ -243,6 +243,7 @@ module TestFixtures {
     ensures fresh(encryption)
     ensures fresh(encryption.Modifies)
   {
+    expect sortKey.None? || IsValid_KeySchemaAttributeName(sortKey.value);
     var keyring := GetKmsKeyring();
     encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
       DynamoDbTablesEncryptionConfig(

Original file line number	Diff line number	Diff line change
`@@ -243,6 +243,7 @@ module TestFixtures {`
`243`	`243`	`ensures fresh(encryption)`
`244`	`244`	`ensures fresh(encryption.Modifies)`
`245`	`245`	`{`
	`246`	`+ expect sortKey.None? \|\| IsValid_KeySchemaAttributeName(sortKey.value);`
`246`	`247`	`var keyring := GetKmsKeyring();`
`247`	`248`	`encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(`
`248`	`249`	`DynamoDbTablesEncryptionConfig(`