Skip to content

Commit 954a2b6

Browse files
ajewellamzajewellamz
committed
m
1 parent 4888c2d commit 954a2b6

File tree

1 file changed

+49
-55
lines changed

1 file changed

+49
-55
lines changed

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

Lines changed: 49 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -74,60 +74,54 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
7474
modifies keyVectors.Modifies
7575
ensures keyVectors.ValidState()
7676
{
77-
// print "DBE Test Vectors\n";
78-
// print |globalRecords|, " records.\n";
79-
// print |tableEncryptionConfigs|, " tableEncryptionConfigs.\n";
80-
// print |largeEncryptionConfigs|, " largeEncryptionConfigs.\n";
81-
// print |queries|, " queries.\n";
82-
// print |names|, " names.\n";
83-
// print |values|, " values.\n";
84-
// print |failingQueries|, " failingQueries.\n";
85-
// print |complexTests|, " complexTests.\n";
86-
// print |ioTests|, " ioTests.\n";
87-
// print |configsForIoTest|, " configsForIoTest.\n";
88-
// print |configsForModTest|, " configsForModTest.\n";
89-
// print |strings|, " strings.\n";
90-
// print |large|, " large.\n";
91-
// if |roundTripTests| != 0 {
92-
// print |roundTripTests[0].configs|, " configs and ", |roundTripTests[0].records|, " records for round trip.\n";
93-
// }
94-
// if |roundTripTests| > 1 {
95-
// print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n";
96-
// }
97-
98-
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors);
99-
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors);
100-
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors);
101-
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors);
102-
// var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors);
103-
// var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors);
104-
// var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors);
105-
// var _ :- expect WriteManifest.Write("encrypt.json");
106-
// var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors);
107-
// var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors);
108-
// if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 {
109-
// print "\nRunning no tests\n";
110-
// return;
111-
// }
112-
// Validate();
113-
// // Because of Dafny-Rust's lack of modules, there is no way to make an interceptor for the wrapped DB-ESDK client.
114-
// // So we create runtimes/rust/SkipLocal.txt to skip those tests that need the wrapped client.
115-
// var skipLocal := FileIO.ReadBytesFromFile("SkipLocal.txt");
116-
// if skipLocal.Success? {
117-
// return;
118-
// }
119-
// StringOrdering();
77+
print "DBE Test Vectors\n";
78+
print |globalRecords|, " records.\n";
79+
print |tableEncryptionConfigs|, " tableEncryptionConfigs.\n";
80+
print |largeEncryptionConfigs|, " largeEncryptionConfigs.\n";
81+
print |queries|, " queries.\n";
82+
print |names|, " names.\n";
83+
print |values|, " values.\n";
84+
print |failingQueries|, " failingQueries.\n";
85+
print |complexTests|, " complexTests.\n";
86+
print |ioTests|, " ioTests.\n";
87+
print |configsForIoTest|, " configsForIoTest.\n";
88+
print |configsForModTest|, " configsForModTest.\n";
89+
print |strings|, " strings.\n";
90+
print |large|, " large.\n";
91+
if |roundTripTests| != 0 {
92+
print |roundTripTests[0].configs|, " configs and ", |roundTripTests[0].records|, " records for round trip.\n";
93+
}
94+
if |roundTripTests| > 1 {
95+
print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n";
96+
}
97+
98+
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors);
99+
var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors);
100+
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors);
101+
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors);
102+
var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors);
103+
var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors);
104+
var _ :- expect DecryptManifest.Decrypt("decrypt_rust_38.json", keyVectors);
105+
var _ :- expect WriteManifest.Write("encrypt.json");
106+
var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors);
107+
var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors);
108+
if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 {
109+
print "\nRunning no tests\n";
110+
return;
111+
}
112+
Validate();
113+
StringOrdering();
120114
LargeTests();
121-
// BasicIoTest();
122-
// RunIoTests();
123-
// BasicQueryTest();
124-
// ConfigModTest();
125-
// ComplexTests();
126-
// WriteTests();
127-
// RoundTripTests();
128-
// DecryptTests();
129-
// var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient();
130-
// DeleteTable(client);
115+
BasicIoTest();
116+
RunIoTests();
117+
BasicQueryTest();
118+
ConfigModTest();
119+
ComplexTests();
120+
WriteTests();
121+
RoundTripTests();
122+
DecryptTests();
123+
var client :- expect CreateInterceptedDDBClient.CreateVanillaDDBClient();
124+
DeleteTable(client);
131125
}
132126

133127
function NewOrderRecord(i : nat, str : string) : Record
@@ -495,8 +489,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
495489
}
496490
}
497491

498-
const TestConfigs : set<string> := {"full_sign_nosign"}
499-
const TestRecords : set<string> := {"flat"}
492+
const TestConfigs : set<string> := {"all"}
493+
const TestRecords : set<string> := {"all"}
500494

501495
predicate DoTestConfig(name : string)
502496
{

0 commit comments

Comments
 (0)