From eb655410f1b01589a84fc35224fa9575dc62bfed Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 13 Mar 2025 12:00:30 -0700 Subject: [PATCH 1/3] Add extern --- TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy | 1 + .../runtimes/java/src/main/java/filepath/Constants.java | 7 +++++++ 2 files changed, 8 insertions(+) create mode 100644 TestVectors/runtimes/java/src/main/java/filepath/Constants.java diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy index d07e572c9..c8ecdea5b 100644 --- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy +++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy @@ -32,6 +32,7 @@ module {:options "-functionSyntax:4"} JsonConfig { import CreateInterceptedDDBClient import DynamoDbItemEncryptor + const {:extern "Utils.constants", "getDefaultKeys"} DEFAULT_KEYS : string predicate IsValidInt32(x: int) { -0x8000_0000 <= x < 0x8000_0000} type ConfigName = string 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"); + } +} From 223a413c8189cfd48a40680569bc70ab43749ddf Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 13 Mar 2025 12:34:45 -0700 Subject: [PATCH 2/3] Add extern --- TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy | 2 -- .../runtimes/java/src/main/java/Utils/constants.java | 7 +++++++ 2 files changed, 7 insertions(+), 2 deletions(-) create mode 100644 TestVectors/runtimes/java/src/main/java/Utils/constants.java diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy index c8ecdea5b..1acc50915 100644 --- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy +++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy @@ -32,8 +32,6 @@ module {:options "-functionSyntax:4"} JsonConfig { import CreateInterceptedDDBClient import DynamoDbItemEncryptor - const {:extern "Utils.constants", "getDefaultKeys"} DEFAULT_KEYS : string - 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"); + } +} From 97872f54f83e0d23cb231e966716674fef35f4e0 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 13 Mar 2025 12:34:53 -0700 Subject: [PATCH 3/3] Add extern --- TestVectors/dafny/DDBEncryption/src/Index.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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)