Skip to content

Commit f69edbc

Browse files
Update TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy
Co-authored-by: Lucas McDonald <[email protected]>
1 parent 90f229b commit f69edbc

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy

+1
Original file line numberDiff line numberDiff line change
@@ -291,6 +291,7 @@ module {:options "-functionSyntax:4"} WriteManifest {
291291
// make a test to decrypt with every possible valid combination of Crypto Actions
292292
if (actionWrittenOuter % 100) == 0 {
293293
var otherActions : CryptoActions := [0,0,0,0,0,0];
294+
// 4096 == 4 ^ 6 == size of all possible values of `otherActions`
294295
for j := 0 to 4096 {
295296
otherActions := Increment(otherActions);
296297
if IsConsistentWith(actions, otherActions) {

0 commit comments

Comments
 (0)