diff --git a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy index 2f0a70689..5ee680b4e 100644 --- a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy +++ b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy @@ -20,12 +20,17 @@ module {:options "-functionSyntax:4"} DecryptManifest { import opened JSONHelpers import JsonConfig import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes + import KeyVectors - method OnePositiveTest(name : string, config : JSON, encrypted : JSON, plaintext : JSON) returns (output : Result) + method OnePositiveTest(name : string, config : JSON, encrypted : JSON, plaintext : JSON, keys : KeyVectors.KeyVectorsClient) + returns (output : Result) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { var enc :- JsonConfig.GetRecord(encrypted); var plain :- JsonConfig.GetRecord(plaintext); - var encryptor :- JsonConfig.GetItemEncryptor(name, config); + var encryptor :- JsonConfig.GetItemEncryptor(name, config, keys); var decrypted :- expect encryptor.DecryptItem( ENC.DecryptItemInput( encryptedItem:=enc.item @@ -36,10 +41,14 @@ module {:options "-functionSyntax:4"} DecryptManifest { return Success(true); } - method OneNegativeTest(name : string, config : JSON, encrypted : JSON) returns (output : Result) + method OneNegativeTest(name : string, config : JSON, encrypted : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { var enc :- JsonConfig.GetRecord(encrypted); - var encryptor :- JsonConfig.GetItemEncryptor(name, config); + var encryptor :- JsonConfig.GetItemEncryptor(name, config, keys); var decrypted := encryptor.DecryptItem( ENC.DecryptItemInput( encryptedItem:=enc.item @@ -51,7 +60,11 @@ module {:options "-functionSyntax:4"} DecryptManifest { return Success(true); } - method OneTest(name : string, value : JSON) returns (output : Result) + method OneTest(name : string, value : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { :- Need(value.Object?, "Test must be an object"); @@ -89,15 +102,19 @@ module {:options "-functionSyntax:4"} DecryptManifest { if types.value == "positive-decrypt" { :- Need(plaintext.Some?, "positive-decrypt Test requires a 'plaintext' member."); - output := OnePositiveTest(name, config.value, encrypted.value, plaintext.value); + output := OnePositiveTest(name, config.value, encrypted.value, plaintext.value, keys); } else if types.value == "negative-decrypt" { - output := OneNegativeTest(name, config.value, encrypted.value); + output := OneNegativeTest(name, config.value, encrypted.value, keys); } else { return Failure("Invalid encrypt type : '" + types.value + "'."); } } - method Decrypt(inFile : string) returns (output : Result) + method Decrypt(inFile : string, keyVectors: KeyVectors.KeyVectorsClient) + returns (output : Result) + requires keyVectors.ValidState() + modifies keyVectors.Modifies + ensures keyVectors.ValidState() { var timeStamp :- expect Time.GetCurrentTimeStamp(); print timeStamp + " Decrypt : ", inFile, "\n"; @@ -154,7 +171,7 @@ module {:options "-functionSyntax:4"} DecryptManifest { for i := 0 to |tests.value| { var obj := tests.value[i]; :- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object."); - var _ :- OneTest(obj.0, obj.1); + var _ :- OneTest(obj.0, obj.1, keyVectors); } timeStamp :- expect Time.GetCurrentTimeStamp(); diff --git a/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy b/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy index 299752c93..a25c80724 100644 --- a/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy +++ b/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy @@ -21,6 +21,7 @@ module {:options "-functionSyntax:4"} EncryptManifest { import opened JSONHelpers import JsonConfig import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes + import KeyVectors function Manifest() : (string, JSON) { @@ -42,10 +43,14 @@ module {:options "-functionSyntax:4"} EncryptManifest { ("client", Object(result)) } - method OnePositiveTest(name : string, theType : string, desc : string, config : JSON, decryptConfig : Option, record : JSON) returns (output : Result<(string, JSON), string>) + method OnePositiveTest(name : string, theType : string, desc : string, config : JSON, decryptConfig : Option, record : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result<(string, JSON), string>) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { var rec :- JsonConfig.GetRecord(record); - var encryptor :- JsonConfig.GetItemEncryptor(name, config); + var encryptor :- JsonConfig.GetItemEncryptor(name, config, keys); var encrypted :- expect encryptor.EncryptItem( ENC.EncryptItemInput( plaintextItem:=rec.item @@ -64,10 +69,14 @@ module {:options "-functionSyntax:4"} EncryptManifest { return Success((name, Object(result))); } - method OneNegativeTest(name : string, config : JSON, record : JSON) returns (output : Result) + method OneNegativeTest(name : string, config : JSON, record : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { var rec :- JsonConfig.GetRecord(record); - var encryptor :- JsonConfig.GetItemEncryptor(name, config); + var encryptor :- JsonConfig.GetItemEncryptor(name, config, keys); var encrypted := encryptor.EncryptItem( ENC.EncryptItemInput( plaintextItem:=rec.item @@ -80,7 +89,11 @@ module {:options "-functionSyntax:4"} EncryptManifest { } - method OneTest(name : string, value : JSON) returns (output : Result, string>) + method OneTest(name : string, value : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result, string>) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { :- Need(value.Object?, "Test must be an object"); @@ -117,20 +130,24 @@ module {:options "-functionSyntax:4"} EncryptManifest { :- Need(record.Some?, "Test requires a 'record' member."); if types.value == "positive-encrypt" { - var x :- OnePositiveTest(name, "positive-decrypt", description.value, config.value, decryptConfig, record.value); + var x :- OnePositiveTest(name, "positive-decrypt", description.value, config.value, decryptConfig, record.value, keys); return Success(Some(x)); } else if types.value == "negative-decrypt" { - var x :- OnePositiveTest(name, "negative-decrypt", description.value, config.value, decryptConfig, record.value); + var x :- OnePositiveTest(name, "negative-decrypt", description.value, config.value, decryptConfig, record.value, keys); return Success(Some(x)); } else if types.value == "negative-encrypt" { - var _ := OneNegativeTest(name, config.value, record.value); + var _ := OneNegativeTest(name, config.value, record.value, keys); return Success(None); } else { return Failure("Invalid encrypt type : '" + types.value + "'."); } } - method Encrypt(inFile : string, outFile : string, lang : string, version : string) returns (output : Result) + method Encrypt(inFile : string, outFile : string, lang : string, version : string, keyVectors: KeyVectors.KeyVectorsClient) + returns (output : Result) + requires keyVectors.ValidState() + modifies keyVectors.Modifies + ensures keyVectors.ValidState() { var timeStamp :- expect Time.GetCurrentTimeStamp(); print timeStamp + " Encrypt : ", inFile, "\n"; @@ -187,7 +204,7 @@ module {:options "-functionSyntax:4"} EncryptManifest { for i := 0 to |tests.value| { var obj := tests.value[i]; :- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object."); - var newTest :- OneTest(obj.0, obj.1); + var newTest :- OneTest(obj.0, obj.1, keyVectors); if newTest.Some? { test := test + [newTest.value]; } diff --git a/TestVectors/dafny/DDBEncryption/src/Index.dfy b/TestVectors/dafny/DDBEncryption/src/Index.dfy index 262c04b58..77e49e3db 100644 --- a/TestVectors/dafny/DDBEncryption/src/Index.dfy +++ b/TestVectors/dafny/DDBEncryption/src/Index.dfy @@ -14,8 +14,17 @@ module WrappedDDBEncryptionMain { import FileIO import JSON.API import opened JSONHelpers + import KeyVectors + import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes - method AddJson(prev : TestVectorConfig, file : string) returns (output : Result) + + const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json" + + method AddJson(prev : TestVectorConfig, file : string, keyVectors: KeyVectors.KeyVectorsClient) + returns (output : Result) + requires keyVectors.ValidState() + modifies keyVectors.Modifies + ensures keyVectors.ValidState() { var configBv := FileIO.ReadBytesFromFile(file); if configBv.Failure? { @@ -24,20 +33,35 @@ module WrappedDDBEncryptionMain { } var configBytes := BvToBytes(configBv.value); var json :- expect API.Deserialize(configBytes); - output := ParseTestVector(json, prev); + output := ParseTestVector(json, prev, keyVectors); if output.Failure? { print output.error, "\n"; } } - method ASDF() { + method ASDF() + { + // KeyVectors client passed to every test. + // All test vectors currently use the same keys manifest, located at DEFAULT_KEYS. + // All test vectors can share this same KeyVectors client. + + // To use a different keys manifest, create a new KeyVectors client. + // If you need to create a new KeyVectors client, create it as infrequently as possible. + // Creating this client frequently means JSON is parsed frequently. + // Parsing JSON is very slow in Python. Parse JSON as infrequently as possible. + var keyVectors :- expect KeyVectors.KeyVectors( + KeyVectorsTypes.KeyVectorsConfig( + keyManifestPath := DEFAULT_KEYS + ) + ); + WriteSetPermutations.WriteSetPermutations(); var config := MakeEmptyTestVector(); - config :- expect AddJson(config, "records.json"); - config :- expect AddJson(config, "configs.json"); - config :- expect AddJson(config, "data.json"); - config :- expect AddJson(config, "iotest.json"); - config :- expect AddJson(config, "PermTest.json"); - config.RunAllTests(); + config :- expect AddJson(config, "records.json", keyVectors); + config :- expect AddJson(config, "configs.json", keyVectors); + config :- expect AddJson(config, "data.json", keyVectors); + config :- expect AddJson(config, "iotest.json", keyVectors); + config :- expect AddJson(config, "PermTest.json", keyVectors); + config.RunAllTests(keyVectors); } } diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy index 46605a425..d07e572c9 100644 --- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy +++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy @@ -33,8 +33,6 @@ module {:options "-functionSyntax:4"} JsonConfig { import DynamoDbItemEncryptor - const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json" - predicate IsValidInt32(x: int) { -0x8000_0000 <= x < 0x8000_0000} type ConfigName = string @@ -130,7 +128,11 @@ module {:options "-functionSyntax:4"} JsonConfig { } } - method GetRoundTripTests(data : JSON) returns (output : Result, string>) + method GetRoundTripTests(data : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result, string>) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { :- Need(data.Object?, "RoundTripTest Test must be an object."); var configs : map := map[]; @@ -139,7 +141,7 @@ module {:options "-functionSyntax:4"} JsonConfig { for i := 0 to |data.obj| { var obj := data.obj[i]; match obj.0 { - case "Configs" => var src :- GetTableConfigs(obj.1); configs := src; + case "Configs" => var src :- GetTableConfigs(obj.1, keys); configs := src; case "Records" => var src :- GetRecords(obj.1); records := src; case _ => return Failure("Unexpected part of a write test : '" + obj.0 + "'"); } @@ -147,18 +149,26 @@ module {:options "-functionSyntax:4"} JsonConfig { return Success([RoundTripTest(configs, records)]); } - method GetWriteTests(data : JSON) returns (output : Result , string>) + method GetWriteTests(data : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result , string>) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { :- Need(data.Array?, "Write Test list must be an array."); var results : seq := []; for i := 0 to |data.arr| { var obj := data.arr[i]; - var item :- GetOneWriteTest(obj); + var item :- GetOneWriteTest(obj, keys); results := results + [item]; } return Success(results); } - method GetOneWriteTest(data : JSON) returns (output : Result) + method GetOneWriteTest(data : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { :- Need(data.Object?, "A Write Test must be an object."); var config : Option := None; @@ -168,7 +178,7 @@ module {:options "-functionSyntax:4"} JsonConfig { for i := 0 to |data.obj| { var obj := data.obj[i]; match obj.0 { - case "Config" => var src :- GetOneTableConfig("foo", obj.1); config := Some(src); + case "Config" => var src :- GetOneTableConfig("foo", obj.1, keys); config := Some(src); case "FileName" => :- Need(obj.1.String?, "Write Test file name must be a string."); fileName := obj.1.str; @@ -181,18 +191,26 @@ module {:options "-functionSyntax:4"} JsonConfig { return Success(WriteTest(config.value, records, fileName)); } - method GetDecryptTests(data : JSON) returns (output : Result , string>) + method GetDecryptTests(data : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result , string>) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { :- Need(data.Array?, "Decrypt Test list must be an array."); var results : seq := []; for i := 0 to |data.arr| { var obj := data.arr[i]; - var item :- GetOneDecryptTest(obj); + var item :- GetOneDecryptTest(obj, keys); results := results + [item]; } return Success(results); } - method GetOneDecryptTest(data : JSON) returns (output : Result) + method GetOneDecryptTest(data : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { :- Need(data.Object?, "A Decrypt Test must be an object."); var config : Option := None; @@ -202,7 +220,7 @@ module {:options "-functionSyntax:4"} JsonConfig { for i := 0 to |data.obj| { var obj := data.obj[i]; match obj.0 { - case "Config" => var src :- GetOneTableConfig("foo", obj.1); config := Some(src); + case "Config" => var src :- GetOneTableConfig("foo", obj.1, keys); config := Some(src); case "EncryptedRecords" => encRecords :- GetRecords(obj.1); case "PlainTextRecords" => plainRecords :- GetRecords(obj.1); case _ => return Failure("Unexpected part of a encrypt test : '" + obj.0 + "'"); @@ -214,20 +232,27 @@ module {:options "-functionSyntax:4"} JsonConfig { return Success(DecryptTest(config.value, encRecords, plainRecords)); } - method GetTableConfigs(data : JSON) returns (output : Result , string>) + method GetTableConfigs(data : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result , string>) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { :- Need(data.Object?, "Search Config list must be an object."); var results : map := map[]; for i := 0 to |data.obj| { var obj := data.obj[i]; - var item :- GetOneTableConfig(obj.0, obj.1); + var item :- GetOneTableConfig(obj.0, obj.1, keys); results := results[obj.0 := item]; } return Success(results); } - method GetItemEncryptor(name : string, data : JSON) + method GetItemEncryptor(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient) returns (encryptor : Result) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() ensures encryptor.Success? ==> && encryptor.value.ValidState() && fresh(encryptor.value) @@ -296,11 +321,6 @@ module {:options "-functionSyntax:4"} JsonConfig { } } - var keys :- expect KeyVectors.KeyVectors( - KeyVectorsTypes.KeyVectorsConfig( - keyManifestPath := DEFAULT_KEYS - ) - ); var keyDescription :- if |key| == 0 then Success(KeyVectorsTypes.Hierarchy(KeyVectorsTypes.HierarchyKeyring( @@ -333,7 +353,11 @@ module {:options "-functionSyntax:4"} JsonConfig { return Success(encr); } - method GetOneTableConfig(name : string, data : JSON) returns (output : Result) + method GetOneTableConfig(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { :- Need(data.Object?, "A Table Config must be an object."); var logicalTableName := TableName; @@ -400,11 +424,6 @@ module {:options "-functionSyntax:4"} JsonConfig { } } - var keys :- expect KeyVectors.KeyVectors( - KeyVectorsTypes.KeyVectorsConfig( - keyManifestPath := DEFAULT_KEYS - ) - ); var keyDescription :- if |key| == 0 then Success(KeyVectorsTypes.Hierarchy(KeyVectorsTypes.HierarchyKeyring( @@ -1129,19 +1148,27 @@ module {:options "-functionSyntax:4"} JsonConfig { )); } - method GetIoTests(data : JSON) returns (output : Result , string>) + method GetIoTests(data : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result , string>) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { :- Need(data.Object?, "IoTests must be an object."); var results : seq := []; for i := 0 to |data.obj| { var obj := data.obj[i]; - var item :- GetOneIoTest(obj.0, obj.1); + var item :- GetOneIoTest(obj.0, obj.1, keys); results := results + [item]; } return Success(results); } - method GetOneIoTest(name : string, data : JSON) returns (output : Result) + method GetOneIoTest(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient) + returns (output : Result) + requires keys.ValidState() + modifies keys.Modifies + ensures keys.ValidState() { :- Need(data.Object?, "IoTest must be an object."); var readConfig : Option := None; @@ -1153,8 +1180,8 @@ module {:options "-functionSyntax:4"} JsonConfig { for i := 0 to |data.obj| { var obj := data.obj[i]; match obj.0 { - case "WriteConfig" => var config :- GetOneTableConfig(obj.0, obj.1); writeConfig := Some(config); - case "ReadConfig" => var config :- GetOneTableConfig(obj.0, obj.1); readConfig := Some(config); + case "WriteConfig" => var config :- GetOneTableConfig(obj.0, obj.1, keys); writeConfig := Some(config); + case "ReadConfig" => var config :- GetOneTableConfig(obj.0, obj.1, keys); readConfig := Some(config); case "Records" => records :- GetRecords(obj.1); case "Values" => values :- GetValueMap(data.obj[i].1); case "Queries" => queries :- GetSimpleQueries(data.obj[i].1); diff --git a/TestVectors/dafny/DDBEncryption/src/LibraryIndex.dfy b/TestVectors/dafny/DDBEncryption/src/LibraryIndex.dfy index 7e5d34ea3..7d26c9846 100644 --- a/TestVectors/dafny/DDBEncryption/src/LibraryIndex.dfy +++ b/TestVectors/dafny/DDBEncryption/src/LibraryIndex.dfy @@ -3,9 +3,7 @@ include "../Model/AwsCryptographyDynamoDbEncryptionTypesWrapped.dfy" -module - {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.wrapped"} - WrappedDynamoDbEncryption refines WrappedAbstractAwsCryptographyDynamoDbEncryptionService +module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.wrapped"} WrappedDynamoDbEncryption refines WrappedAbstractAwsCryptographyDynamoDbEncryptionService { import WrappedService = DynamoDbEncryption diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index c0f494301..3d134d444 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -61,7 +61,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { strings : seq ) { - method RunAllTests() + method RunAllTests(keyVectors: KeyVectors.KeyVectorsClient) + requires keyVectors.ValidState() + modifies keyVectors.Modifies + ensures keyVectors.ValidState() { print "DBE Test Vectors\n"; print |globalRecords|, " records.\n"; @@ -82,15 +85,15 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { print |roundTripTests[1].configs|, " configs and ", |roundTripTests[1].records|, " records for round trip.\n"; } - var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json"); - var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json"); - var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json"); - var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json"); - var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json"); - var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json"); + var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_32.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_java_32.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_java_33.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_dotnet_33a.json", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt_java_33a.json", keyVectors); var _ :- expect WriteManifest.Write("encrypt.json"); - var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3"); - var _ :- expect DecryptManifest.Decrypt("decrypt.json"); + var _ :- expect EncryptManifest.Encrypt("encrypt.json", "decrypt.json", "java", "3.3", keyVectors); + var _ :- expect DecryptManifest.Decrypt("decrypt.json", keyVectors); if |globalRecords| + |tableEncryptionConfigs| + |queries| == 0 { print "\nRunning no tests\n"; return; @@ -999,7 +1002,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { TestVectorConfig(MakeCreateTableInput(), [], map[], [], map[], map[], [], [], [], [], [], [], [], [], []) } - method ParseTestVector(data : JSON, prev : TestVectorConfig) returns (output : Result) + method ParseTestVector(data : JSON, prev : TestVectorConfig, keyVectors: KeyVectors.KeyVectorsClient) + returns (output : Result) + requires keyVectors.ValidState() + modifies keyVectors.Modifies + ensures keyVectors.ValidState() { :- Need(data.Object?, "Top Level JSON must be an object."); var records : seq := []; @@ -1028,12 +1035,12 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { case "Names" => names :- GetNameMap(data.obj[i].1); case "Values" => values :- GetValueMap(data.obj[i].1); case "Complex" => complexTests :- GetComplexTests(data.obj[i].1); - case "IoTests" => ioTests :- GetIoTests(data.obj[i].1); + case "IoTests" => ioTests :- GetIoTests(data.obj[i].1, keyVectors); case "GSI" => gsi :- GetGSIs(data.obj[i].1); - case "tableEncryptionConfigs" => tableEncryptionConfigs :- GetTableConfigs(data.obj[i].1); - case "WriteTests" => writeTests :- GetWriteTests(data.obj[i].1); - case "RoundTripTest" => roundTripTests :- GetRoundTripTests(data.obj[i].1); - case "DecryptTests" => decryptTests :- GetDecryptTests(data.obj[i].1); + case "tableEncryptionConfigs" => tableEncryptionConfigs :- GetTableConfigs(data.obj[i].1, keyVectors); + case "WriteTests" => writeTests :- GetWriteTests(data.obj[i].1, keyVectors); + case "RoundTripTest" => roundTripTests :- GetRoundTripTests(data.obj[i].1, keyVectors); + case "DecryptTests" => decryptTests :- GetDecryptTests(data.obj[i].1, keyVectors); case "Strings" => strings :- GetStrings(data.obj[i].1); case _ => return Failure("Unexpected top level tag " + data.obj[i].0); }