@@ -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