fix

.github/workflows/library_net_tests.yml

@@ -36,6 +36,11 @@ jobs:
           ubuntu-latest,
           macos-13,
         ]
+        net_retry_zips: [
+          invalid-Net-4.0.0.zip,
+          v4-Net-4.0.1.zip,
+          valid-Net-4.0.0.zip
+        ]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
@@ -91,6 +96,14 @@ jobs:
           # This works because `node` is installed by default on GHA runners
           CORES=$(node -e 'console.log(os.cpus().length)')
           make transpile_net CORES=$CORES
+      
+      - name: Unzip .NET Retry Flag Manifests
+        shell: bash
+        working-directory: TestVectors/dafny/TestVectors/test/
+        run: |
+          unzip invalid-Net-4.0.0.zip -d invalid-Net-4.0.0.zip
+          unzip v4-Net-4.0.1.zip -d v4-Net-4.0.1.zip
+          unzip valid-Net-4.0.0.zip -d valid-Net-4.0.0.zip
 
       - name: Test .NET Framework net48
         working-directory: ${{ matrix.library }}

TestVectors/dafny/TestVectors/src/WriteVectors.dfy

@@ -87,12 +87,17 @@ module {:options "-functionSyntax:4"} WriteVectors {
     var manifestJson := Object([
                                  ("type", String("awses-encrypt")),
                                  ("version", Number(Int(5)))]);
+
+    var clientJson := Object([
+                               ("name", String("aws-encryption-sdk-dafny")),
+                               ("version", String("4.1.0"))]);
 
     var plaintexts := Object([("small", Number(Int(10240)))]);
 
     var esdkEncryptManifests := Object(
       [
         ("manifest", manifestJson),
+        ("client", clientJson),
         ("keys", String("file://keys.json")),
         ("plaintexts", plaintexts),
         ("tests", Object(testsJSON))

TestVectors/dafny/TestVectors/test/RunMain.dfy

@@ -50,9 +50,6 @@ module {:extern} TestWrappedESDKMain {
   // to correctly pass when this configuration runs the invalid net 4.0.0 tests.
   // The errors that we get back from the MPL are opaque errors, not opaque with text...
   // This means that in dafny code we cannot check the error message :(
-  // So if you need to see that the esdk-x where x is a language that the esdk-dafny supports
-  // correctly fails to decrypt these test vectors, just uncomment this test.
-
   method {:test} TestNetInvalidTestVectorsExpectFailure() {
     var directory := GetTestVectorExecutionDirectory();
     var result := EsdkTestManifests.StartDecryptVectors(
@@ -63,6 +60,7 @@ module {:extern} TestWrappedESDKMain {
       )
     );
     print "ONLY WORRY IF THE ABOVE TESTS PASSED!!! THESE TESTS ARE SUPPOSED TO FAIL!\n";
+    print "IF THE TESTS FAIL OTHER THAN A AES GCM TAG VALIDATION EXCEPTION, CUT AN ISSUE.\n";
     expect result.Failure?;
   }