m

ajewellamz · ajewellamz · commit 05cc97d74997 · 2025-07-23T15:17:33.000-04:00
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy
@@ -129,6 +129,7 @@ module DdbMiddlewareConfig {
   predicate OneSearchValidState(config : TableConfig)
   {
     && (config.search.Some? ==> config.search.value.ValidState())
+    && config.bucketSelector.ValidState()
   }
   predicate SearchValidState(config: Config)
   {
@@ -139,6 +140,7 @@ module DdbMiddlewareConfig {
   {
     (set t <- config.tableEncryptionConfigs.Keys, o <- config.tableEncryptionConfigs[t].itemEncryptor.Modifies :: o)
     + (set t <- config.tableEncryptionConfigs.Keys, o <- OneSearchModifies(config.tableEncryptionConfigs[t]) :: o)
+    + (set t <- config.tableEncryptionConfigs.Keys, o <- config.tableEncryptionConfigs[t].bucketSelector.Modifies :: o)
   }
 
   predicate ValidConfig?(config: Config)

Original file line number	Diff line number	Diff line change
`@@ -129,6 +129,7 @@ module DdbMiddlewareConfig {`
`129`	`129`	`predicate OneSearchValidState(config : TableConfig)`
`130`	`130`	`{`
`131`	`131`	`&& (config.search.Some? ==> config.search.value.ValidState())`
	`132`	`+ && config.bucketSelector.ValidState()`
`132`	`133`	`}`
`133`	`134`	`predicate SearchValidState(config: Config)`
`134`	`135`	`{`
`@@ -139,6 +140,7 @@ module DdbMiddlewareConfig {`
`139`	`140`	`{`
`140`	`141`	`(set t <- config.tableEncryptionConfigs.Keys, o <- config.tableEncryptionConfigs[t].itemEncryptor.Modifies :: o)`
`141`	`142`	`+ (set t <- config.tableEncryptionConfigs.Keys, o <- OneSearchModifies(config.tableEncryptionConfigs[t]) :: o)`
	`143`	`+ + (set t <- config.tableEncryptionConfigs.Keys, o <- config.tableEncryptionConfigs[t].bucketSelector.Modifies :: o)`
`142`	`144`	`}`
`143`	`145`
`144`	`146`	`predicate ValidConfig?(config: Config)`