try and and consolidate some things

aws · Nov 24, 2024 · 9d801ae · 9d801ae
1 parent 7e8e60b
commit 9d801ae
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/src/Mutations.dfy
@@ -60,6 +60,16 @@ module {:options "/functionSyntax:4" } Mutations {
     nameonly keyManagerStrategy: KmsUtils.keyManagerStrat,
     nameonly storage: Types.AwsCryptographyKeyStoreTypes.IKeyStorageInterface
   )
+  {
+    ghost predicate ValidState()
+    {
+      && SystemKey.ValidState()
+      && keyManagerStrategy.ValidState()
+      && storage.ValidState()
+      && SystemKey.Modifies !! keyManagerStrategy.Modifies !! storage.Modifies
+    }
+    ghost const Modifies := SystemKey.Modifies + keyManagerStrategy.Modifies + storage.Modifies
+  }
 
   predicate ValidateQueryOutResults?(
     applyMutationInput: Types.ApplyMutationInput,