@@ -74,46 +74,46 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
74
74
modifies keyVectors. Modifies
75
75
ensures keyVectors. ValidState ()
76
76
{
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();
114
- // LargeTests();
115
- // BasicIoTest();
116
- // RunIoTests();
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 ();
114
+ LargeTests ();
115
+ BasicIoTest ();
116
+ RunIoTests ();
117
117
BasicQueryTest ();
118
118
ConfigModTest ();
119
119
ComplexTests ();
0 commit comments