m

ajewellamz · ajewellamz · commit b3552931b515 · 2024-08-22T18:30:37.000-04:00
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy
@@ -243,7 +243,7 @@ module TestFixtures {
     ensures fresh(encryption)
     ensures fresh(encryption.Modifies)
   {
-    expect sortKey.None? || IsValid_KeySchemaAttributeName(sortKey.value);
+    expect sortKey.None? || DDB.IsValid_KeySchemaAttributeName(sortKey.value);
     var keyring := GetKmsKeyring();
     encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
       DynamoDbTablesEncryptionConfig(

Original file line number	Diff line number	Diff line change
`@@ -243,7 +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`	`+ expect sortKey.None? \|\| DDB.IsValid_KeySchemaAttributeName(sortKey.value);`
`247`	`247`	`var keyring := GetKmsKeyring();`
`248`	`248`	`encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(`
`249`	`249`	`DynamoDbTablesEncryptionConfig(`