m

ajewellamz · ajewellamz · commit 87b103c02a08 · 2025-02-10T09:00:36.000-05:00
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
@@ -826,6 +826,7 @@ module {:options "/functionSyntax:4" } Canonize {
     else if xs[pos].key in [HeaderPath, FooterPath] then
       RemoveHeaderPaths(xs, pos+1, acc)
     else
+      assert xs[pos] !in acc;
       RemoveHeaderPaths(xs, pos+1, acc + [xs[pos]])
   }
 

Original file line number	Diff line number	Diff line change
`@@ -826,6 +826,7 @@ module {:options "/functionSyntax:4" } Canonize {`
`826`	`826`	`else if xs[pos].key in [HeaderPath, FooterPath] then`
`827`	`827`	`RemoveHeaderPaths(xs, pos+1, acc)`
`828`	`828`	`else`
	`829`	`+ assert xs[pos] !in acc;`
`829`	`830`	`RemoveHeaderPaths(xs, pos+1, acc + [xs[pos]])`
`830`	`831`	`}`
`831`	`832`