diff --git a/TestVectors/dafny/DDBEncryption/src/Index.dfy b/TestVectors/dafny/DDBEncryption/src/Index.dfy index 77e49e3db..12d07318c 100644 --- a/TestVectors/dafny/DDBEncryption/src/Index.dfy +++ b/TestVectors/dafny/DDBEncryption/src/Index.dfy @@ -17,8 +17,8 @@ module WrappedDDBEncryptionMain { import KeyVectors import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes - - const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json" + const {:extern "Utils.constants", "getDefaultKeys"} DEFAULT_KEYS : string + // const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json" method AddJson(prev : TestVectorConfig, file : string, keyVectors: KeyVectors.KeyVectorsClient) returns (output : Result) diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy index d07e572c9..1acc50915 100644 --- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy +++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy @@ -32,7 +32,6 @@ module {:options "-functionSyntax:4"} JsonConfig { import CreateInterceptedDDBClient import DynamoDbItemEncryptor - predicate IsValidInt32(x: int) { -0x8000_0000 <= x < 0x8000_0000} type ConfigName = string diff --git a/TestVectors/runtimes/java/src/main/java/Utils/constants.java b/TestVectors/runtimes/java/src/main/java/Utils/constants.java new file mode 100644 index 000000000..99308f6ae --- /dev/null +++ b/TestVectors/runtimes/java/src/main/java/Utils/constants.java @@ -0,0 +1,7 @@ +package Utils; + +public class constants { + public static dafny.DafnySequence getDefaultKeys(){ + return dafny.DafnySequence.asString("../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"); + } +} diff --git a/TestVectors/runtimes/java/src/main/java/filepath/Constants.java b/TestVectors/runtimes/java/src/main/java/filepath/Constants.java new file mode 100644 index 000000000..dd21015bf --- /dev/null +++ b/TestVectors/runtimes/java/src/main/java/filepath/Constants.java @@ -0,0 +1,7 @@ +package filepath; + +public class Constants { + public static dafny.DafnySequence defaultKeys(){ + return dafny.DafnySequence.asString("../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"); + } +}