m

Lucas McDonald · Lucas McDonald · commit 3368712e5290 · 2025-04-17T13:40:31.000-07:00
diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
@@ -257,7 +257,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
   }
 
   method GetItemEncryptor(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)
-    returns (encryptor : Result<DynamoDbItemEncryptor.DynamoDbItemEncryptorClient, string>)
+    returns (encryptor : Result<ENC.IDynamoDbItemEncryptorClient, string>)
     requires keys.ValidState()
     modifies keys.Modifies
     ensures keys.ValidState()

Original file line number	Diff line number	Diff line change
`@@ -257,7 +257,7 @@ module {:options "-functionSyntax:4"} JsonConfig {`
`257`	`257`	`}`
`258`	`258`
`259`	`259`	`method GetItemEncryptor(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)`
`260`		`- returns (encryptor : Result<DynamoDbItemEncryptor.DynamoDbItemEncryptorClient, string>)`
	`260`	`+ returns (encryptor : Result<ENC.IDynamoDbItemEncryptorClient, string>)`
`261`	`261`	`requires keys.ValidState()`
`262`	`262`	`modifies keys.Modifies`
`263`	`263`	`ensures keys.ValidState()`