m

ajewellamz · ajewellamz · commit 7f93ea57ffb9 · 2025-04-22T16:48:50.000-04:00
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
@@ -62,7 +62,7 @@ module StructuredEncryptionHeader {
     requires pos <= |data| as uint32
     requires forall i | 0 <= i < pos :: data[i].action != SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
     decreases |data| as uint32 - pos
-    ensures ret ==> (exists x <- data :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT)
+    ensures ret <==> (exists x <- data :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT)
   {
     if pos == |data| as uint32 then
       false

Original file line number	Diff line number	Diff line change
`@@ -62,7 +62,7 @@ module StructuredEncryptionHeader {`
`62`	`62`	`requires pos <= \|data\| as uint32`
`63`	`63`	`requires forall i \| 0 <= i < pos :: data[i].action != SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT`
`64`	`64`	`decreases \|data\| as uint32 - pos`
`65`		`- ensures ret ==> (exists x <- data :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT)`
	`65`	`+ ensures ret <==> (exists x <- data :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT)`
`66`	`66`	`{`
`67`	`67`	`if pos == \|data\| as uint32 then`
`68`	`68`	`false`