update verification

seebees · seebees · commit f74a9f947515 · 2024-08-29T13:20:54.000-07:00
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy
@@ -237,7 +237,7 @@ module TestFixtures {
     assume {:axiom} fresh(encryption.Modifies);
   }
 
-  method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option<string>)
+  method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option<ComAmazonawsDynamodbTypes.KeySchemaAttributeName>)
     returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)
     ensures encryption.ValidState()
     ensures fresh(encryption)

Original file line number	Diff line number	Diff line change
`@@ -237,7 +237,7 @@ module TestFixtures {`
`237`	`237`	`assume {:axiom} fresh(encryption.Modifies);`
`238`	`238`	`}`
`239`	`239`
`240`		`- method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option<string>)`
	`240`	`+ method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option<ComAmazonawsDynamodbTypes.KeySchemaAttributeName>)`
`241`	`241`	`returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)`
`242`	`242`	`ensures encryption.ValidState()`
`243`	`243`	`ensures fresh(encryption)`