m

ajewellamz · ajewellamz · commit 4bb289a98001 · 2025-02-11T11:49:22.000-05:00
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy
@@ -85,7 +85,7 @@ module BatchWriteItemTransform {
     tableConfig : ValidTableConfig,
     srcRequests : DDB.WriteRequests,
     itemReq : DDB.WriteRequest
-    ) returns (ret : Result<DDB.WriteRequest, Error>)
+  ) returns (ret : Result<DDB.WriteRequest, Error>)
     requires itemReq.PutRequest.Some?
     ensures ret.Success? ==> ret.value.PutRequest.Some?
   {

Original file line number	Diff line number	Diff line change
`@@ -85,7 +85,7 @@ module BatchWriteItemTransform {`
`85`	`85`	`tableConfig : ValidTableConfig,`
`86`	`86`	`srcRequests : DDB.WriteRequests,`
`87`	`87`	`itemReq : DDB.WriteRequest`
`88`		`- ) returns (ret : Result<DDB.WriteRequest, Error>)`
	`88`	`+ ) returns (ret : Result<DDB.WriteRequest, Error>)`
`89`	`89`	`requires itemReq.PutRequest.Some?`
`90`	`90`	`ensures ret.Success? ==> ret.value.PutRequest.Some?`
`91`	`91`	`{`