@@ -33,6 +33,8 @@ module {:options "-functionSyntax:4"} JsonConfig {
33
33
import DynamoDbItemEncryptor
34
34
35
35
36
+ const DEFAULT_KEYS := ".. / .. / .. / submodules/ MaterialProviders/ TestVectorsAwsCryptographicMaterialProviders/ dafny/ TestVectorsAwsCryptographicMaterialProviders/ test/ keys. json"
37
+
36
38
predicate IsValidInt32 (x: int ) { - 0x8000_0000 <= x < 0x8000_0000}
37
39
type ConfigName = string
38
40
@@ -296,7 +298,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
296
298
297
299
var keys :- expect KeyVectors. KeyVectors (
298
300
KeyVectorsTypes.KeyVectorsConfig(
299
- keyManifiestPath := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
301
+ keyManifiestPath := DEFAULT_KEYS
300
302
)
301
303
);
302
304
var keyDescription :-
@@ -398,7 +400,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
398
400
399
401
var keys :- expect KeyVectors. KeyVectors (
400
402
KeyVectorsTypes.KeyVectorsConfig(
401
- keyManifiestPath := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
403
+ keyManifiestPath := DEFAULT_KEYS
402
404
)
403
405
);
404
406
var keyDescription :-
@@ -545,7 +547,7 @@ module {:options "-functionSyntax:4"} JsonConfig {
545
547
case "ENCRYPT_AND_SIGN" => return Success (SE.ENCRYPT_AND_SIGN);
546
548
case "SIGN_ONLY" => return Success (SE.SIGN_ONLY);
547
549
case "DO_NOTHING" => return Success (SE.DO_NOTHING);
548
- case _ => return Failure (data.str + " is not a value CryptoAction.");
550
+ case _ => return Failure (data.str + " is not a valid CryptoAction.");
549
551
}
550
552
}
551
553
@@ -922,9 +924,6 @@ module {:options "-functionSyntax:4"} JsonConfig {
922
924
return Success (Types.CompoundBeacon(name := name, split := split, encrypted := OptSeq(Encrypted), signed := OptSeq (Signed), constructors := OptSeq (constructors)));
923
925
}
924
926
925
- // datatype Type = Type
926
- // method JsonToType(data : JSON) returns (output : Result<Type, string>)
927
-
928
927
method GetConstructors (data : JSON ) returns (output : Result< seq < Types. Constructor> , string > )
929
928
{
930
929
:- Need (data.Array?, "Constructor list must be an array.");
0 commit comments