start decrypt vectors

TestVectors/dafny/ESDK/src/EsdkTestManifests.dfy

@@ -29,25 +29,26 @@ module {:options "-functionSyntax:4"} EsdkTestManifests {
   import opened EsdkTestVectors
   import WriteVectors
 
-  // method StartDecryptVectors(
-  //   op: EsdkManifestOptions.ManifestOptions
-  // )
-  //   returns (output: Result<seq<BoundedInts.byte>, string>)
-  //   requires op.Decrypt?
-  //   requires 0 < |op.manifestPath|
-  //   requires Seq.Last(op.manifestPath) == '/'
-  // {
-  //   var decryptManifest :- expect GetManifest(op.manifestPath, "manifest.json");
-  //   :- Need(decryptManifest.DecryptManifest?, "Not a decrypt manifest");
-
-  //   var decryptVectors :- ParseEsdkJsonManifest.BuildDecryptTestVector(
-  //     op,
-  //     decryptManifest.version,
-  //     decryptManifest.keys,
-  //     decryptManifest.jsonTests
-  //   );
-  //   output := TestDecrypts(decryptManifest.keys, decryptVectors);
-  // }
+  method StartDecryptVectors(
+    op: EsdkManifestOptions.ManifestOptions
+  )
+    returns (output: Result<seq<BoundedInts.byte>, string>)
+    requires op.Decrypt?
+    requires 0 < |op.manifestPath|
+    requires Seq.Last(op.manifestPath) == '/'
+  {
+    var decryptManifest :- expect GetManifest(op.manifestPath, "decrypt-manifest.json");
+    :- Need(decryptManifest.DecryptManifest?, "Not a decrypt manifest");
+
+    // var decryptVectors :- ParseEsdkJsonManifest.BuildDecryptTestVector(
+    //   op,
+    //   decryptManifest.version,
+    //   decryptManifest.keys,
+    //   decryptManifest.jsonTests
+    // );
+    // output := TestDecrypts(decryptManifest.keys, decryptVectors);
+    return Failure("Implement me!");
+  }
 
   predicate TestDecryptVector?(v: EsdkDecryptTestVector)
   {

TestVectors/dafny/ESDK/src/EsdkTestVectors.dfy

@@ -79,6 +79,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
         commitmentPolicy: mplTypes.ESDKCommitmentPolicy := mplTypes.FORBID_ENCRYPT_ALLOW_DECRYPT,
         frameLength: Option<int64>,
         algorithmSuiteId: Option<mplTypes.AlgorithmSuiteInfo>,
+        description: string,
         maxEncryptedDataKeys: Option<Types.CountingNumbers> := Some(1)
       )
     | PositiveEncryptNegativeDecryptTestVector (
@@ -96,6 +97,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
         frameLength: Option<int64>,
         algorithmSuiteId: Option<mplTypes.AlgorithmSuiteInfo>,
         decryptErrorDescription: string,
+        description: string,
         maxEncryptedDataKeys: Option<Types.CountingNumbers> := Some(1)
       )
     | NegativeEncryptTestVector(
@@ -111,6 +113,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
         frameLength: Option<int64>,
         algorithmSuiteId: Option<mplTypes.AlgorithmSuiteInfo>,
         errorDescription: string,
+        description: string,
         maxEncryptedDataKeys: Option<Types.CountingNumbers> := Some(1)
       )
 
@@ -135,6 +138,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
         commitmentPolicy: mplTypes.ESDKCommitmentPolicy := mplTypes.FORBID_ENCRYPT_ALLOW_DECRYPT,
         frameLength: Option<int64>,
         algorithmSuiteId: Option<mplTypes.AlgorithmSuiteInfo>,
+        description: string,
         decryptionMethod: DecryptionMethod
       )
     | NegativeDecryptTestVector(
@@ -144,8 +148,12 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
         ciphertextPath: string,
         errorDescription: string,
         encryptionContext: Option<mplTypes.EncryptionContext> := None,
+        requiredEncryptionContextKeys: Option<mplTypes.EncryptionContextKeys> := None,
         decryptDescriptions: KeyVectorsTypes.KeyDescription,
         commitmentPolicy: mplTypes.ESDKCommitmentPolicy := mplTypes.FORBID_ENCRYPT_ALLOW_DECRYPT,
+        frameLength: Option<int64>,
+        algorithmSuiteId: Option<mplTypes.AlgorithmSuiteInfo>,
+        description: string,
         decryptionMethod: DecryptionMethod
       )
 
@@ -277,7 +285,8 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
     requires test.vector.frameLength.Some? ==> Types.IsValid_FrameLength(test.vector.frameLength.value)
     requires test.vector.algorithmSuiteId.Some? && test.vector.algorithmSuiteId.value.id.ESDK?
   {
-    print "\nTEST===> ", test.vector.name, "\n";
+    var id := AllAlgorithmSuites.ToHex(test.vector.algorithmSuiteId.value);
+    print "\nTEST===> ", test.vector.name, "\n", id, " ", test.vector.description, "\n";
 
     // The decrypt test vectors also test initialization
     // This is because they were developed when the MPL
@@ -305,8 +314,7 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
             || test.vector.PositiveEncryptNegativeDecryptTestVector?
           )
     {
-      var name :- expect UUID.GenerateUUID();
-      var decryptVector :- EncryptTestToDecryptVector(name, test, result.value);
+      var decryptVector :- EncryptTestToDecryptVector(test, result.value);
       output := Success(EncryptTestOutput(
         vector := Some(decryptVector),
         output := true
@@ -370,7 +378,6 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
   }
 
   method EncryptTestToDecryptVector(
-    name: string,
     test: EncryptTest,
     result: Types.EncryptOutput
   ) returns (output: Result<EsdkDecryptTestVector, string>)
@@ -380,36 +387,26 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
     requires test.vector.algorithmSuiteId.Some?
   {
     output := match test.vector
-      case PositiveEncryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_,_) =>
+      case PositiveEncryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_,_,_) =>
         Success(PositiveDecryptTestVector(
-          name := name,
+          name := test.vector.name,
           version := 3,
           manifestPath := test.vector.decryptManifestPath,
-          ciphertextPath := ciphertextPathPathRoot + name,
+          ciphertextPath := ciphertextPathPathRoot + test.vector.name,
           plaintextPath := plaintextPathRoot + test.vector.plaintextPath,
           encryptionContext := test.vector.encryptionContext,
           requiredEncryptionContextKeys := test.vector.requiredEncryptionContextKeys,
           decryptDescriptions := test.vector.decryptDescriptions,
           commitmentPolicy := test.vector.commitmentPolicy,
           frameLength := test.vector.frameLength,
           algorithmSuiteId := test.vector.algorithmSuiteId,
+          description := test.vector.description,
           decryptionMethod := DecryptionMethod.OneShot
         ))
       case _ =>
         Failure("Only postive tests supported");
-      // case PositiveEncryptNegativeDecryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_,_,_) =>
-      //   NegativeDecryptTestVector(
-      //     name := name,
-      //     version := 2,
-      //     manifestPath := test.vector.decryptManifestPath,
-      //     ciphertextPath := ciphertextPathPathRoot + name,
-      //     errorDescription := test.vector.decryptErrorDescription,
-      //     encryptionContext := test.vector.encryptionContext,
-      //     decryptDescriptions := [test.vector.decryptDescriptions],
-      //     commitmentPolicy := test.vector.commitmentPolicy,
-      //     decryptionMethod := DecryptionMethod.OneShot
-      //   );
-    var decryptManifestCiphertext := test.vector.decryptManifestPath + ciphertextPathPathRoot + name;
+
+    var decryptManifestCiphertext := test.vector.decryptManifestPath + ciphertextPathPathRoot + test.vector.name;
     // Side effect, to avoid thousands of ciphertext in memory...
     var _ :- expect WriteVectorsFile(decryptManifestCiphertext, result.ciphertext);
   }
@@ -487,4 +484,4 @@ module {:options "-functionSyntax:4"} EsdkTestVectors {
     var bv := BytesBv(bytes);
     output := FileIO.WriteBytesToFile(location, bv);
   }
-}
+}

TestVectors/dafny/ESDK/src/ParseEsdkJsonManifest.dfy

@@ -262,6 +262,7 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest {
 
     var encryptionContextStrings :- SmallObjectToStringStringMap(encryptionContextJsonKey, scenario);
     var encryptionContext :- utf8EncodeMap(encryptionContextStrings);
+    var description :- GetString("description", scenario);
 
     match typ
     case "positive-esdk" =>
@@ -278,7 +279,8 @@ module {:options "-functionSyntax:4"} ParseEsdkJsonManifest {
         encryptionContext := Some(encryptionContext),
         commitmentPolicy := mplTypes.FORBID_ENCRYPT_ALLOW_DECRYPT,
         frameLength := frameLength,
-        algorithmSuiteId := Some(algorithmSuite)
+        algorithmSuiteId := Some(algorithmSuite),
+        description := description
       ))
     case _ => Failure("Unsupported ESDK TestVector type: " + typ)
 

TestVectors/dafny/ESDK/src/VectorsComposition/AllEsdkV4NoReqEc.dfy

@@ -77,7 +77,8 @@ module {:options "/functionSyntax:4" } AllEsdkV4NoReqEc {
         encryptDescriptions := keyringConfig.encryptDescription,
         decryptDescriptions := keyringConfig.decryptDescription,
         frameLength := Some(frameSize),
-        algorithmSuiteId := Some(algorithmSuite)
+        algorithmSuiteId := Some(algorithmSuite),
+        description := keyringConfig.name
       )
 
   const AllPositiveKeyringTestsNoDBEKmsRsa :=
@@ -94,7 +95,8 @@ module {:options "/functionSyntax:4" } AllEsdkV4NoReqEc {
         encryptDescriptions := keyringConfig.encryptDescription,
         decryptDescriptions := keyringConfig.decryptDescription,
         frameLength := Some(frameSize),
-        algorithmSuiteId := Some(algorithmSuite)
+        algorithmSuiteId := Some(algorithmSuite),
+        description := keyringConfig.name
       )
 
   const Tests := 

TestVectors/dafny/ESDK/src/VectorsComposition/AllEsdkV4WithReqEc.dfy

@@ -90,7 +90,8 @@ module {:options "/functionSyntax:4" } AllEsdkV4WithReqEc {
           requiredEncryptionContextKeys := config.requiredEncryptionContextKeys,
           requiredECDescription := Some(config.name),
           frameLength := Some(frameSize),
-          algorithmSuiteId := Some(algorithmSuite)
+          algorithmSuiteId := Some(algorithmSuite),
+          description := config.name
         )
 
   const Tests := 

TestVectors/dafny/ESDK/src/WriteEsdkJsonManifests.dfy

@@ -80,12 +80,13 @@ module {:options "-functionSyntax:4"} WriteEsdkJsonManifests {
     var optionalValues := requiredEncryptionContextKeys + encryptionContext;
 
     match test
-    case PositiveEncryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_,_) =>
+    case PositiveEncryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_,_,_) =>
       var encrypt :- KeyDescription.ToJson(test.encryptDescriptions, 3);
       var decrypt :- KeyDescription.ToJson(test.decryptDescriptions, 3);
       var scenario := Object([
                                 ("type", String("positive-esdk")),
                                 ("plaintext", String("small")),
+                                ("description", String(test.description)),
                                 ("algorithmSuiteId", String(id)),
                                 ("frame-size", Number(Int(test.frameLength.value as int))),
                                 ("encryptKeyDescription", encrypt),
@@ -195,11 +196,46 @@ module {:options "-functionSyntax:4"} WriteEsdkJsonManifests {
   //                    ] + reproducedEc + encryptionContext))
   // }
 
-  function DecryptTestVectorToJson(
+  function {:vcs_split_on_every_assert} DecryptTestVectorToJson(
     test: EsdkTestVectors.EsdkDecryptTestVector
   ): Result<JSON, string>
   {
-    // var id := AllAlgorithmSuites.ToHex(test);
-    Failure("whelp")
+    :- Need(
+      && test.algorithmSuiteId.Some?
+      && test.frameLength.Some?,
+      "test is missing algorithmSuite ID, or frameLength"
+    );
+    var id := AllAlgorithmSuites.ToHex(test.algorithmSuiteId.value);
+    var description := test.name + " " + id;
+
+    var encryptionContext 
+      :- if test.encryptionContext.Some? then
+          EncryptionContextToJson("encryption-context", test.encryptionContext.value)
+        else
+          EncryptionContextToJson("encryption-context", map[]);
+
+    :- Need(
+      |encryptionContext| == 1,
+      "Error parsing encryption context"
+    );
+
+    var requiredEncryptionContextKeys :- EncryptionContextKeysToJson(test.requiredEncryptionContextKeys);
+    var optionalValues := requiredEncryptionContextKeys + encryptionContext;
+
+    match test
+    case PositiveDecryptTestVector(_,_,_,_,_,_,_,_,_,_,_,_,_) =>
+      var decrypt :- KeyDescription.ToJson(test.decryptDescriptions, 3);
+      var scenario := Object([
+                                ("type", String("positive-esdk")),
+                                ("ciphertext", String("file://ciphertexts/" + test.name)),
+                                ("algorithmSuiteId", String(id)),
+                                ("frame-size", Number(Int(test.frameLength.value as int))),
+                                ("decryptKeyDescription", decrypt)
+                              ] + optionalValues);
+      Success(Object([
+                      ("decryption-scenario", scenario)
+                      ]))
+    case _ =>
+      Failure("Only Positive Tests supported :(")
   }
 }

TestVectors/dafny/ESDK/src/WriteVectors.dfy

@@ -74,9 +74,8 @@ module {:options "-functionSyntax:4"} WriteVectors {
 
       var id := AllAlgorithmSuites.ToHex(tests[i].algorithmSuiteId.value);
       var uuid :- expect UUID.GenerateUUID();
-      var name := id + "-" + tests[i].name + "-" + uuid;
       var test :- WriteEsdkJsonManifests.EncryptTestVectorToJson(tests[i]);
-      testsJSON := testsJSON + [(name, test)];
+      testsJSON := testsJSON + [(uuid, test)];
     }
 
     var manifestJson := Object([
@@ -98,7 +97,7 @@ module {:options "-functionSyntax:4"} WriteVectors {
     var esdkEncryptManifestBv := JSONHelpers.BytesBv(esdkEncryptManifestBytes);
 
     var _ :- expect FileIO.WriteBytesToFile(
-      op.encryptManifestOutput + "manifest.json",
+      op.encryptManifestOutput + "encrypt-manifest.json",
       esdkEncryptManifestBv
     );
 
@@ -119,12 +118,34 @@ module {:options "-functionSyntax:4"} WriteVectors {
 
     for i := 0 to |tests|
     {
-      var name :- UUID.GenerateUUID();
+      var name := tests[i].name; 
       var test :- WriteEsdkJsonManifests.DecryptTestVectorToJson(tests[i]);
       testsJSON := testsJSON + [(name, test)];
     }
 
-    return Failure("Whelp");
+    var manifestJson := Object([
+          ("type", String("awses-decrypt")),
+          ("version", Number(Int(3)))]);
+
+    var esdkDecryptManifest := Object(
+      [
+        ("manifest", manifestJson),
+        // TODO create an extern that gets that runtimes namespace and latest version
+        ("client", String("aws-encryption-sdk-dafny")),
+        ("keys", String("file://keys.json")),
+        ("tests", Object(testsJSON))
+      ]
+    );
+
+    var esdkDecryptManifestBytes :- expect API.Serialize(esdkDecryptManifest);
+    var esdkDecryptManifestBv := JSONHelpers.BytesBv(esdkDecryptManifestBytes);
+
+    var _ :- expect FileIO.WriteBytesToFile(
+      op.decryptManifestOutput + "decrypt-manifest.json",
+      esdkDecryptManifestBv
+    );
+
+    output := Success(());
   }
 
   function getVersionTests(version: nat): (ret: Result<set<EsdkTestVectors.EsdkEncryptTestVector>, string>)

TestVectors/dafny/ESDK/test/RunMain.dfy

@@ -70,7 +70,7 @@ module {:extern} TestWrappedESDKMain {
   method {:test} RunManifestTests() {
     TestGenerateEncryptManifest();
     TestEncryptManifest();
-    // TestDecryptManifest();
+    TestDecryptManifest();
   }
 
   method TestGenerateEncryptManifest() {
@@ -91,8 +91,8 @@ module {:extern} TestWrappedESDKMain {
     var result := EsdkTestManifests.StartEncryptVectors(
       EsdkManifestOptions.Encrypt(
         manifestPath := directory + "dafny/TestVectors/test/",
-        manifest := "manifest.json",
-        decryptManifestOutput := directory + "dafny/TestVectors/"
+        manifest := "encrypt-manifest.json",
+        decryptManifestOutput := directory + "dafny/TestVectors/test"
       )
     );
     if result.Failure? {
@@ -101,4 +101,18 @@ module {:extern} TestWrappedESDKMain {
     expect result.Success?;
   }
 
+  method TestDecryptManifest()
+  {
+    var directory := GetTestVectorExecutionDirectory();
+    var result := EsdkTestManifests.StartDecryptVectors(
+      EsdkManifestOptions.Decrypt(
+        manifestPath := directory + "dafny/TestVectors/"
+      )
+    );
+
+    if result.Failure? {
+      print result.error;
+    }
+    expect result.Success?;
+  }
 }