File tree Expand file tree Collapse file tree 3 files changed +3
-4
lines changed
TestVectors/dafny/DDBEncryption/src Expand file tree Collapse file tree 3 files changed +3
-4
lines changed Original file line number Diff line number Diff line change @@ -23,8 +23,6 @@ module {:options "-functionSyntax:4"} EncryptManifest {
23
23
import ENC = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
24
24
import KeyVectors
25
25
26
- const DEFAULT_KEYS : string := ".. / .. / .. / submodules/ MaterialProviders/ TestVectorsAwsCryptographicMaterialProviders/ dafny/ TestVectorsAwsCryptographicMaterialProviders/ test/ keys. json"
27
-
28
26
function Manifest () : (string , JSON)
29
27
{
30
28
var result : seq < (string , JSON)> :=
Original file line number Diff line number Diff line change @@ -17,6 +17,9 @@ module WrappedDDBEncryptionMain {
17
17
import KeyVectors
18
18
import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
19
19
20
+
21
+ const DEFAULT_KEYS : string := ".. / .. / .. / submodules/ MaterialProviders/ TestVectorsAwsCryptographicMaterialProviders/ dafny/ TestVectorsAwsCryptographicMaterialProviders/ test/ keys. json"
22
+
20
23
method AddJson (prev : TestVectorConfig , file : string , keyVectors: KeyVectors .KeyVectorsClient)
21
24
returns (output : Result< TestVectorConfig, string > )
22
25
requires keyVectors. ValidState ()
Original file line number Diff line number Diff line change @@ -43,8 +43,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
43
43
import ParseJsonManifests
44
44
45
45
46
- const DEFAULT_KEYS : string := ".. / .. / .. / submodules/ MaterialProviders/ TestVectorsAwsCryptographicMaterialProviders/ dafny/ TestVectorsAwsCryptographicMaterialProviders/ test/ keys. json"
47
-
48
46
datatype TestVectorConfig = TestVectorConfig (
49
47
schemaOnEncrypt : DDB .CreateTableInput,
50
48
globalRecords : seq <Record >,
You can’t perform that action at this time.
0 commit comments