From 915ba281f8be4888c96dc182c2dfd5915e67c07e Mon Sep 17 00:00:00 2001
From: Lucas McDonald <lucasmcdonald3@gmail.com>
Date: Fri, 17 Jan 2025 09:37:16 -0800
Subject: [PATCH 1/6] m

---
 .../DDBEncryption/src/DecryptManifest.dfy     | 35 ++++++--
 .../DDBEncryption/src/EncryptManifest.dfy     | 39 +++++---
 TestVectors/dafny/DDBEncryption/src/Index.dfy | 35 ++++++--
 .../dafny/DDBEncryption/src/JsonConfig.dfy    | 89 ++++++++++++-------
 .../dafny/DDBEncryption/src/LibraryIndex.dfy  |  4 +-
 .../dafny/DDBEncryption/src/TestVectors.dfy   | 39 ++++----
 .../dafny/DDBEncryption/src/WriteManifest.dfy | 27 +++---
 7 files changed, 178 insertions(+), 90 deletions(-)

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<bool, string>)
+  method OnePositiveTest(name : string, config : JSON, encrypted : JSON, plaintext : JSON, keys : KeyVectors.KeyVectorsClient)
+    returns (output : Result<bool, string>)
+    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<bool, string>)
+  method OneNegativeTest(name : string, config : JSON, encrypted : JSON, keys: KeyVectors.KeyVectorsClient)
+    returns (output : Result<bool, string>)
+    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<bool, string>)
+  method OneTest(name : string, value : JSON, keys: KeyVectors.KeyVectorsClient)
+    returns (output : Result<bool, string>)
+    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<bool, string>)
+  method Decrypt(inFile : string, keyVectors: KeyVectors.KeyVectorsClient)
+    returns (output : Result<bool, string>)
+    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..55460b77d 100644
--- a/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy
@@ -21,6 +21,9 @@ module {:options "-functionSyntax:4"} EncryptManifest {
   import opened JSONHelpers
   import JsonConfig
   import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
+  import KeyVectors
+
+  const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
 
   function Manifest() : (string, JSON)
   {
@@ -42,10 +45,14 @@ module {:options "-functionSyntax:4"} EncryptManifest {
     ("client", Object(result))
   }
 
-  method OnePositiveTest(name : string, theType : string, desc : string, config : JSON, decryptConfig : Option<JSON>, record : JSON) returns (output : Result<(string, JSON), string>)
+  method OnePositiveTest(name : string, theType : string, desc : string, config : JSON, decryptConfig : Option<JSON>, 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 +71,14 @@ module {:options "-functionSyntax:4"} EncryptManifest {
     return Success((name, Object(result)));
   }
 
-  method OneNegativeTest(name : string, config : JSON, record : JSON) returns (output : Result<bool, string>)
+  method OneNegativeTest(name : string, config : JSON, record : JSON, keys: KeyVectors.KeyVectorsClient)
+    returns (output : Result<bool, 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 := encryptor.EncryptItem(
       ENC.EncryptItemInput(
         plaintextItem:=rec.item
@@ -80,7 +91,11 @@ module {:options "-functionSyntax:4"} EncryptManifest {
   }
 
 
-  method OneTest(name : string, value : JSON) returns (output : Result<Option<(string, JSON)>, string>)
+  method OneTest(name : string, value : JSON, keys: KeyVectors.KeyVectorsClient)
+    returns (output : Result<Option<(string, JSON)>, string>)
+    requires keys.ValidState()
+    modifies keys.Modifies
+    ensures keys.ValidState()
   {
     :- Need(value.Object?, "Test must be an object");
 
@@ -117,20 +132,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<bool, string>)
+  method Encrypt(inFile : string, outFile : string, lang : string, version : string, keyVectors: KeyVectors.KeyVectorsClient)
+    returns (output : Result<bool, string>)
+    requires keyVectors.ValidState()
+    modifies keyVectors.Modifies
+    ensures keyVectors.ValidState()
   {
     var timeStamp :- expect Time.GetCurrentTimeStamp();
     print timeStamp + " Encrypt : ", inFile, "\n";
@@ -187,7 +206,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..d7d163f40 100644
--- a/TestVectors/dafny/DDBEncryption/src/Index.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/Index.dfy
@@ -14,8 +14,14 @@ module WrappedDDBEncryptionMain {
   import FileIO
   import JSON.API
   import opened JSONHelpers
+  import KeyVectors
+  import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
 
-  method AddJson(prev : TestVectorConfig, file : string) returns (output : Result<TestVectorConfig, string>)
+  method AddJson(prev : TestVectorConfig, file : string, keyVectors: KeyVectors.KeyVectorsClient)
+    returns (output : Result<TestVectorConfig, string>)
+    requires keyVectors.ValidState()
+    modifies keyVectors.Modifies
+    ensures keyVectors.ValidState()
   {
     var configBv := FileIO.ReadBytesFromFile(file);
     if configBv.Failure? {
@@ -24,20 +30,31 @@ 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() 
+  {
+    // Create a singleton keyVectors client used in every test.
+    // Right now, all test vectors use the same keys manifest, located at DEFAULT_KEYS.
+    // Parsing JSON is expensive in some languages.
+    // 
+    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 d4eb1f144..0c00fd44c 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<seq<RoundTripTest>, string>)
+  method GetRoundTripTests(data : JSON, keys: KeyVectors.KeyVectorsClient)
+    returns (output : Result<seq<RoundTripTest>, string>)
+    requires keys.ValidState()
+    modifies keys.Modifies
+    ensures keys.ValidState()
   {
     :- Need(data.Object?, "RoundTripTest Test must be an object.");
     var configs : map<string, TableConfig> := 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<seq<WriteTest> , string>)
+  method GetWriteTests(data : JSON, keys: KeyVectors.KeyVectorsClient)
+    returns (output : Result<seq<WriteTest> , string>)
+    requires keys.ValidState()
+    modifies keys.Modifies
+    ensures keys.ValidState()
   {
     :- Need(data.Array?, "Write Test list must be an array.");
     var results : seq<WriteTest> := [];
     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<WriteTest, string>)
+  method GetOneWriteTest(data : JSON, keys: KeyVectors.KeyVectorsClient)
+    returns (output : Result<WriteTest, string>)
+    requires keys.ValidState()
+    modifies keys.Modifies
+    ensures keys.ValidState()
   {
     :- Need(data.Object?, "A Write Test must be an object.");
     var config : Option<TableConfig> := 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<seq<DecryptTest> , string>)
+  method GetDecryptTests(data : JSON, keys: KeyVectors.KeyVectorsClient)
+    returns (output : Result<seq<DecryptTest> , string>)
+    requires keys.ValidState()
+    modifies keys.Modifies
+    ensures keys.ValidState()
   {
     :- Need(data.Array?, "Decrypt Test list must be an array.");
     var results : seq<DecryptTest> := [];
     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<DecryptTest, string>)
+  method GetOneDecryptTest(data : JSON, keys: KeyVectors.KeyVectorsClient)
+    returns (output : Result<DecryptTest, string>)
+    requires keys.ValidState()
+    modifies keys.Modifies
+    ensures keys.ValidState()
   {
     :- Need(data.Object?, "A Decrypt Test must be an object.");
     var config : Option<TableConfig> := 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<map<string, TableConfig> , string>)
+  method GetTableConfigs(data : JSON, keys: KeyVectors.KeyVectorsClient)
+    returns (output : Result<map<string, TableConfig> , string>)
+    requires keys.ValidState()
+    modifies keys.Modifies
+    ensures keys.ValidState()
   {
     :- Need(data.Object?, "Search Config list must be an object.");
     var results : map<string, TableConfig> := 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<DynamoDbItemEncryptor.DynamoDbItemEncryptorClient, string>)
+    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<TableConfig, string>)
+  method GetOneTableConfig(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)
+    returns (output : Result<TableConfig, string>)
+    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(
@@ -1114,19 +1133,27 @@ module {:options "-functionSyntax:4"} JsonConfig {
                    ));
   }
 
-  method GetIoTests(data : JSON) returns (output : Result<seq<IoTest> , string>)
+  method GetIoTests(data : JSON, keys: KeyVectors.KeyVectorsClient)
+    returns (output : Result<seq<IoTest> , string>)
+    requires keys.ValidState()
+    modifies keys.Modifies
+    ensures keys.ValidState()
   {
     :- Need(data.Object?, "IoTests must be an object.");
     var results : seq<IoTest> := [];
     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<IoTest, string>)
+  method GetOneIoTest(name : string, data : JSON, keys: KeyVectors.KeyVectorsClient)
+    returns (output : Result<IoTest, string>)
+    requires keys.ValidState()
+    modifies keys.Modifies
+    ensures keys.ValidState()
   {
     :- Need(data.Object?, "IoTest must be an object.");
     var readConfig : Option<TableConfig> := None;
@@ -1138,8 +1165,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..b1855b7be 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -43,6 +43,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
   import ParseJsonManifests
 
 
+  const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
+
   datatype TestVectorConfig = TestVectorConfig (
     schemaOnEncrypt : DDB.CreateTableInput,
     globalRecords : seq<Record>,
@@ -61,7 +63,10 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
     strings : seq<string>
   ) {
 
-    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 +87,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 +1004,11 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
     TestVectorConfig(MakeCreateTableInput(), [], map[], [], map[], map[], [], [], [], [], [], [], [], [], [])
   }
 
-  method ParseTestVector(data : JSON, prev : TestVectorConfig) returns (output : Result<TestVectorConfig, string>)
+  method ParseTestVector(data : JSON, prev : TestVectorConfig, keyVectors: KeyVectors.KeyVectorsClient)
+    returns (output : Result<TestVectorConfig, string>)
+    requires keyVectors.ValidState()
+    modifies keyVectors.Modifies
+    ensures keyVectors.ValidState()
   {
     :- Need(data.Object?, "Top Level JSON must be an object.");
     var records : seq<Record> := [];
@@ -1028,12 +1037,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);
       }
diff --git a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy
index 325fc0412..ca4a095ee 100644
--- a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy
@@ -218,20 +218,21 @@ module {:options "-functionSyntax:4"} WriteManifest {
   const DoNothing : CryptoAction := 3
 
   const A : string := "A"
-  const B : string := "퀀" // Ud000"
-  const C : string := "﹌" // Ufe4c"
-  const D : string := "𐀁" // U10001
-  const E : string := "𐀂" // U10002 - same high surrogate as D
-  const F : string := "𠀂" // U20002 - different high surrogate as D
+  const B : string := "\ud000" // Ud000"
+  const C : string := "\ufe4c" // Ufe4c"
+  const D : string := "\u100001" // U10001
+  const E : string := "\u100002" // U10002 - same high surrogate as D
+  const F : string := "\u200002" // U20002 - different high surrogate as D
 
-  lemma CheckLengths()
-    ensures |A| == 1
-    ensures |B| == 1
-    ensures |C| == 1
-    ensures |D| == 2
-    ensures |E| == 2
-    ensures |F| == 2
-  {}
+  // Dafny doesn't handle unicode surrogates correctly.
+  // lemma CheckLengths()
+  //   ensures |A| == 1
+  //   ensures |B| == 1
+  //   ensures |C| == 1
+  //   ensures |D| == 2
+  //   ensures |E| == 2
+  //   ensures |F| == 2
+  // {}
 
   // Let's make attribute names with complex characters.
   // It shouldn't matter, but let's make sure

From 0d54190c768c44a858cf1d74b9a4b443d72908f5 Mon Sep 17 00:00:00 2001
From: Lucas McDonald <lucasmcdonald3@gmail.com>
Date: Fri, 17 Jan 2025 10:05:29 -0800
Subject: [PATCH 2/6] m

---
 TestVectors/dafny/DDBEncryption/src/Index.dfy | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/Index.dfy b/TestVectors/dafny/DDBEncryption/src/Index.dfy
index d7d163f40..aac17e758 100644
--- a/TestVectors/dafny/DDBEncryption/src/Index.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/Index.dfy
@@ -38,10 +38,14 @@ module WrappedDDBEncryptionMain {
 
   method ASDF() 
   {
-    // Create a singleton keyVectors client used in every test.
-    // Right now, all test vectors use the same keys manifest, located at DEFAULT_KEYS.
-    // Parsing JSON is expensive in some languages.
-    // 
+    // 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

From d9e2a4f1b4be7f05057a68b567a72237fb5cf023 Mon Sep 17 00:00:00 2001
From: Lucas McDonald <lucasmcdonald3@gmail.com>
Date: Fri, 17 Jan 2025 10:08:10 -0800
Subject: [PATCH 3/6] m

---
 .../dafny/DDBEncryption/src/WriteManifest.dfy | 27 +++++++++----------
 1 file changed, 13 insertions(+), 14 deletions(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy
index ca4a095ee..325fc0412 100644
--- a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy
@@ -218,21 +218,20 @@ module {:options "-functionSyntax:4"} WriteManifest {
   const DoNothing : CryptoAction := 3
 
   const A : string := "A"
-  const B : string := "\ud000" // Ud000"
-  const C : string := "\ufe4c" // Ufe4c"
-  const D : string := "\u100001" // U10001
-  const E : string := "\u100002" // U10002 - same high surrogate as D
-  const F : string := "\u200002" // U20002 - different high surrogate as D
+  const B : string := "퀀" // Ud000"
+  const C : string := "﹌" // Ufe4c"
+  const D : string := "𐀁" // U10001
+  const E : string := "𐀂" // U10002 - same high surrogate as D
+  const F : string := "𠀂" // U20002 - different high surrogate as D
 
-  // Dafny doesn't handle unicode surrogates correctly.
-  // lemma CheckLengths()
-  //   ensures |A| == 1
-  //   ensures |B| == 1
-  //   ensures |C| == 1
-  //   ensures |D| == 2
-  //   ensures |E| == 2
-  //   ensures |F| == 2
-  // {}
+  lemma CheckLengths()
+    ensures |A| == 1
+    ensures |B| == 1
+    ensures |C| == 1
+    ensures |D| == 2
+    ensures |E| == 2
+    ensures |F| == 2
+  {}
 
   // Let's make attribute names with complex characters.
   // It shouldn't matter, but let's make sure

From a591e7f914c7d039e9641cd4f52bdb94dc8453b5 Mon Sep 17 00:00:00 2001
From: Lucas McDonald <lucasmcdonald3@gmail.com>
Date: Fri, 17 Jan 2025 14:32:18 -0800
Subject: [PATCH 4/6] ubuntu-not-latest

---
 .github/workflows/check-files.yml                    | 2 +-
 .github/workflows/check_only_key_word.yml            | 2 +-
 .github/workflows/ci_codegen.yml                     | 2 +-
 .github/workflows/ci_duvet.yml                       | 2 +-
 .github/workflows/ci_static_analysis.yml             | 2 +-
 .github/workflows/ci_test_net.yml                    | 2 +-
 .github/workflows/ci_test_vector_java.yml            | 2 +-
 .github/workflows/ci_test_vector_net.yml             | 2 +-
 .github/workflows/dafny_interop_test_net.yml         | 2 +-
 .github/workflows/dafny_interop_test_vector_java.yml | 2 +-
 .github/workflows/dafny_interop_test_vector_net.yml  | 2 +-
 .github/workflows/dafny_verify_version.yml           | 2 +-
 .github/workflows/dafny_version.yml                  | 2 +-
 .github/workflows/library_rust_tests.yml             | 2 +-
 .github/workflows/mpl_head_version.yml               | 2 +-
 .github/workflows/nightly.yml                        | 2 +-
 .github/workflows/smithy-diff.yml                    | 2 +-
 17 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/.github/workflows/check-files.yml b/.github/workflows/check-files.yml
index 08fb5eaf9..59f613d0c 100644
--- a/.github/workflows/check-files.yml
+++ b/.github/workflows/check-files.yml
@@ -7,7 +7,7 @@ on:
 
 jobs:
   require-approvals:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     permissions:
       issues: write
       pull-requests: write
diff --git a/.github/workflows/check_only_key_word.yml b/.github/workflows/check_only_key_word.yml
index 94e2fe95a..4a8a5c9f3 100644
--- a/.github/workflows/check_only_key_word.yml
+++ b/.github/workflows/check_only_key_word.yml
@@ -8,7 +8,7 @@ on:
 
 jobs:
   grep-only-verification-keyword:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     permissions:
       issues: write
       pull-requests: write
diff --git a/.github/workflows/ci_codegen.yml b/.github/workflows/ci_codegen.yml
index 6bbee248d..5fc05fcc8 100644
--- a/.github/workflows/ci_codegen.yml
+++ b/.github/workflows/ci_codegen.yml
@@ -17,7 +17,7 @@ jobs:
         # Note dotnet is only used for formatting generated code
         # in this workflow
         dotnet-version: ["6.0.x"]
-        os: [ubuntu-latest]
+        os: [ubuntu-22.04]
     runs-on: ${{ matrix.os }}
     defaults:
       run:
diff --git a/.github/workflows/ci_duvet.yml b/.github/workflows/ci_duvet.yml
index 0edbb0797..7bceb87b5 100644
--- a/.github/workflows/ci_duvet.yml
+++ b/.github/workflows/ci_duvet.yml
@@ -11,7 +11,7 @@ on:
 
 jobs:
   duvet:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     steps:
       - uses: actions/checkout@v3
 
diff --git a/.github/workflows/ci_static_analysis.yml b/.github/workflows/ci_static_analysis.yml
index b5f0a81fa..fb0ec3779 100644
--- a/.github/workflows/ci_static_analysis.yml
+++ b/.github/workflows/ci_static_analysis.yml
@@ -9,7 +9,7 @@ on:
 
 jobs:
   not-grep:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     steps:
       - uses: actions/checkout@v2
       - name: not-grep
diff --git a/.github/workflows/ci_test_net.yml b/.github/workflows/ci_test_net.yml
index 9a9767262..f8e6f7dec 100644
--- a/.github/workflows/ci_test_net.yml
+++ b/.github/workflows/ci_test_net.yml
@@ -25,7 +25,7 @@ jobs:
       matrix:
         library: [DynamoDbEncryption]
         dotnet-version: ["6.0.x"]
-        os: [macos-13, ubuntu-latest, windows-latest]
+        os: [macos-13, ubuntu-22.04, windows-latest]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
diff --git a/.github/workflows/ci_test_vector_java.yml b/.github/workflows/ci_test_vector_java.yml
index 08cb684b9..5c6fee636 100644
--- a/.github/workflows/ci_test_vector_java.yml
+++ b/.github/workflows/ci_test_vector_java.yml
@@ -31,7 +31,7 @@ jobs:
         java-version: [8, 11, 16, 17]
         os: [
             # Run on ubuntu image that comes pre-configured with docker
-            ubuntu-latest,
+            ubuntu-22.04,
           ]
     runs-on: ${{ matrix.os }}
     permissions:
diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml
index a06af88df..657c5f87f 100644
--- a/.github/workflows/ci_test_vector_net.yml
+++ b/.github/workflows/ci_test_vector_net.yml
@@ -27,7 +27,7 @@ jobs:
         dotnet-version: ["6.0.x"]
         os: [
             # Run on ubuntu image that comes pre-configured with docker
-            ubuntu-latest,
+            ubuntu-22.04,
           ]
     runs-on: ${{ matrix.os }}
     permissions:
diff --git a/.github/workflows/dafny_interop_test_net.yml b/.github/workflows/dafny_interop_test_net.yml
index b87519059..1316765d2 100644
--- a/.github/workflows/dafny_interop_test_net.yml
+++ b/.github/workflows/dafny_interop_test_net.yml
@@ -24,7 +24,7 @@ jobs:
       matrix:
         library: [DynamoDbEncryption]
         dotnet-version: ["6.0.x"]
-        os: [macos-13, ubuntu-latest, windows-latest]
+        os: [macos-13, ubuntu-22.04, windows-latest]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
diff --git a/.github/workflows/dafny_interop_test_vector_java.yml b/.github/workflows/dafny_interop_test_vector_java.yml
index 57f5f57ab..a4c6472ec 100644
--- a/.github/workflows/dafny_interop_test_vector_java.yml
+++ b/.github/workflows/dafny_interop_test_vector_java.yml
@@ -30,7 +30,7 @@ jobs:
         java-version: [8, 11, 16, 17]
         os: [
             # Run on ubuntu image that comes pre-configured with docker
-            ubuntu-latest,
+            ubuntu-22.04,
           ]
     runs-on: ${{ matrix.os }}
     permissions:
diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml
index 33d45ebb7..12f6693be 100644
--- a/.github/workflows/dafny_interop_test_vector_net.yml
+++ b/.github/workflows/dafny_interop_test_vector_net.yml
@@ -24,7 +24,7 @@ jobs:
       matrix:
         library: [TestVectors]
         dotnet-version: ["6.0.x"]
-        os: [ubuntu-latest]
+        os: [ubuntu-22.04]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
diff --git a/.github/workflows/dafny_verify_version.yml b/.github/workflows/dafny_verify_version.yml
index 139e4ddb1..ec9ce95b9 100644
--- a/.github/workflows/dafny_verify_version.yml
+++ b/.github/workflows/dafny_verify_version.yml
@@ -12,7 +12,7 @@ on:
 
 jobs:
   getDafnyVerifyVersion:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     outputs:
       version: ${{ steps.read_property.outputs.dafnyVerifyVersion }}
     steps:
diff --git a/.github/workflows/dafny_version.yml b/.github/workflows/dafny_version.yml
index 1a04f1e65..c20e01a43 100644
--- a/.github/workflows/dafny_version.yml
+++ b/.github/workflows/dafny_version.yml
@@ -12,7 +12,7 @@ on:
 
 jobs:
   getDafnyVersion:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     outputs:
       version: ${{ steps.read_property.outputs.dafnyVersion }}
     steps:
diff --git a/.github/workflows/library_rust_tests.yml b/.github/workflows/library_rust_tests.yml
index e921284a8..0e3d3cb42 100644
--- a/.github/workflows/library_rust_tests.yml
+++ b/.github/workflows/library_rust_tests.yml
@@ -21,7 +21,7 @@ jobs:
       matrix:
         library: [DynamoDbEncryption, TestVectors]
         # removed windows-latest because somehow it can't build aws-lc in CI
-        os: [ubuntu-latest, macos-13]
+        os: [ubuntu-22.04, macos-13]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
diff --git a/.github/workflows/mpl_head_version.yml b/.github/workflows/mpl_head_version.yml
index f94200cda..0857aa502 100644
--- a/.github/workflows/mpl_head_version.yml
+++ b/.github/workflows/mpl_head_version.yml
@@ -18,7 +18,7 @@ on:
 
 jobs:
   getMplHeadVersion:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     outputs:
       version: ${{ steps.read_property.outputs.mplVersion }}
     steps:
diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml
index 8eff29fe2..eb4bc6e20 100644
--- a/.github/workflows/nightly.yml
+++ b/.github/workflows/nightly.yml
@@ -66,7 +66,7 @@ jobs:
       regenerate-code: true
 
   cut-issue-on-failure:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     permissions:
       id-token: write
       contents: read
diff --git a/.github/workflows/smithy-diff.yml b/.github/workflows/smithy-diff.yml
index 3092c9470..7661bc580 100644
--- a/.github/workflows/smithy-diff.yml
+++ b/.github/workflows/smithy-diff.yml
@@ -8,7 +8,7 @@ on:
 
 jobs:
   require-approvals:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     permissions:
       issues: write
       pull-requests: write

From 75325b000bfcb8bbc49a7c73549279bbb0123636 Mon Sep 17 00:00:00 2001
From: Lucas McDonald <lucasmcdonald3@gmail.com>
Date: Fri, 17 Jan 2025 14:38:28 -0800
Subject: [PATCH 5/6] m

---
 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 aac17e758..6b5f72490 100644
--- a/TestVectors/dafny/DDBEncryption/src/Index.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/Index.dfy
@@ -36,13 +36,13 @@ module WrappedDDBEncryptionMain {
     }
   }
 
-  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. 
+    // 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.

From 393c25ea06af48cae9fd15b224c4fe24ec1a7f19 Mon Sep 17 00:00:00 2001
From: Lucas McDonald <lucasmcdonald3@gmail.com>
Date: Fri, 17 Jan 2025 15:40:27 -0800
Subject: [PATCH 6/6] cleanup

---
 TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy | 2 --
 TestVectors/dafny/DDBEncryption/src/Index.dfy           | 3 +++
 TestVectors/dafny/DDBEncryption/src/TestVectors.dfy     | 2 --
 3 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy b/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy
index 55460b77d..a25c80724 100644
--- a/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy
@@ -23,8 +23,6 @@ module {:options "-functionSyntax:4"} EncryptManifest {
   import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
   import KeyVectors
 
-  const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
-
   function Manifest() : (string, JSON)
   {
     var result : seq<(string, JSON)> :=
diff --git a/TestVectors/dafny/DDBEncryption/src/Index.dfy b/TestVectors/dafny/DDBEncryption/src/Index.dfy
index 6b5f72490..77e49e3db 100644
--- a/TestVectors/dafny/DDBEncryption/src/Index.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/Index.dfy
@@ -17,6 +17,9 @@ module WrappedDDBEncryptionMain {
   import KeyVectors
   import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
 
+
+  const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
+
   method AddJson(prev : TestVectorConfig, file : string, keyVectors: KeyVectors.KeyVectorsClient)
     returns (output : Result<TestVectorConfig, string>)
     requires keyVectors.ValidState()
diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index b1855b7be..3d134d444 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -43,8 +43,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
   import ParseJsonManifests
 
 
-  const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
-
   datatype TestVectorConfig = TestVectorConfig (
     schemaOnEncrypt : DDB.CreateTableInput,
     globalRecords : seq<Record>,