Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 90f229b

Browse files
ajewellamzlucasmcdonald3
andauthoredApr 25, 2024··
Update TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy
Co-authored-by: Lucas McDonald <[email protected]>
1 parent 69340a6 commit 90f229b

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed
 

‎TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -274,6 +274,7 @@ module {:options "-functionSyntax:4"} WriteManifest {
274274
var record := TextToJson(ConfigRecord);
275275
var actionWrittenOuter := 0;
276276
var actionWrittenInner := 0;
277+
// 4096 == 4 ^ 6 == size of all possible values of `actions`
277278
for i := 0 to 4096 {
278279
actions := Increment(actions);
279280
if IsConsistent(actions) {

0 commit comments

Comments
 (0)
Please sign in to comment.