m

Lucas McDonald · Lucas McDonald · commit 68804576ddb0 · 2025-04-30T11:54:33.000-07:00
diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
@@ -269,7 +269,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
     ensures encryptor.Success? ==>
               && encryptor.value.ValidState()
               && fresh(encryptor.value)
-              && fresh(encryptor.value.Modifies - Operations.ModifiesInternalConfig(encryptor.value.config))
+              && fresh(encryptor.value.Modifies)
   {
     :- Need(data.Object?, "A Table Config must be an object.");
     var logicalTableName := TableName;

Original file line number	Diff line number	Diff line change
`@@ -269,7 +269,7 @@ module {:options "-functionSyntax:4"} JsonConfig {`
`269`	`269`	`ensures encryptor.Success? ==>`
`270`	`270`	`&& encryptor.value.ValidState()`
`271`	`271`	`&& fresh(encryptor.value)`
`272`		`- && fresh(encryptor.value.Modifies - Operations.ModifiesInternalConfig(encryptor.value.config))`
	`272`	`+ && fresh(encryptor.value.Modifies)`
`273`	`273`	`{`
`274`	`274`	`:- Need(data.Object?, "A Table Config must be an object.");`
`275`	`275`	`var logicalTableName := TableName;`