Update DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy

mahnushm · rishav-karanjit · web-flow · commit 1d449d835d43 · 2026-06-11T11:46:30.000-07:00
Co-authored-by: Rishav karanjit &lt;karanjitrishav4@gmail.com&gt;
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy
@@ -298,7 +298,7 @@ module DynamoDBSupport {
     var filterHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(filterExpr), actions, names);
     var keyHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(keyExpr), actions, names);
     if keyHasEncField.Some? || filterHasEncField.Some? {
-      return Failure(E("When numberOfPartitions is greater than one, XXXValues must contain " + PartitionName));
+      return Failure(E("When numberOfPartitions is greater than one, Values must contain " + PartitionName));
     } else {
       return Success((values, 0));
     }

Original file line number	Diff line number	Diff line change
`@@ -298,7 +298,7 @@ module DynamoDBSupport {`
`298`	`298`	`var filterHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(filterExpr), actions, names);`
`299`	`299`	`var keyHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(keyExpr), actions, names);`
`300`	`300`	`if keyHasEncField.Some? \|\| filterHasEncField.Some? {`
`301`		`- return Failure(E("When numberOfPartitions is greater than one, XXXValues must contain " + PartitionName));`
	`301`	`+ return Failure(E("When numberOfPartitions is greater than one, Values must contain " + PartitionName));`
`302`	`302`	`} else {`
`303`	`303`	`return Success((values, 0));`
`304`	`304`	`}`