test: add net v4 retry flag test vectors (#711)

Co-authored-by: Rishav karanjit <[email protected]>

Author: josecorella

Diff for: .github/workflows/daily_ci.yml

@@ -39,3 +39,15 @@ jobs:
     uses: ./.github/workflows/library_interop_tests.yml
     with:
       dafny: '4.9.0'
+  
+  daily-dafny-test-vectors:
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    uses: ./.github/workflows/library_interop_test_vectors.yml
+    with:
+      dafny: '4.9.0'
+  
+  daily-dafny-legacy-test-vectors:
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    uses: ./.github/workflows/library_legacy_interop_test_vectors.yml
+    with:
+      dafny: '4.9.0'

Diff for: .github/workflows/library_net_tests.yml

@@ -30,6 +30,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
+        library: [AwsEncryptionSDK]
         os: [
           windows-latest,
           ubuntu-latest,
@@ -75,40 +76,30 @@ jobs:
         uses: ./.github/actions/polymorph_codegen
         with:
           dafny: ${{ env.DAFNY_VERSION }}
-          library: AwsEncryptionSDK
+          library: ${{ matrix.library }}
           diff-generated-code: false
           update-and-regenerate-mpl: true
 
       - name: Download Dependencies 
-        working-directory: ./AwsEncryptionSDK
+        working-directory: ${{ matrix.library }}
         run: make setup_net
 
-      - name: Compile AwsEncryptionSDK implementation
+      - name: Compile ${{ matrix.library }} implementation
         shell: bash
-        working-directory: ./AwsEncryptionSDK
-        run: |
-          # 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: Compile MPL TestVectors implementation
-        shell: bash
-        working-directory: ./mpl/TestVectorsAwsCryptographicMaterialProviders
+        working-directory: ${{ matrix.library }}
         run: |
           # 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: Test .NET Framework net48
-        working-directory: ./AwsEncryptionSDK
-        if: matrix.os == 'windows-latest' 
+        working-directory: ${{ matrix.library }}
         shell: bash
         run: |
           make test_net FRAMEWORK=net48
 
       - name: Test .NET net6.0
-        working-directory: ./AwsEncryptionSDK
+        working-directory: ${{ matrix.library }}
         shell: bash
         run: |
           if [ "$RUNNER_OS" == "macOS" ]; then
@@ -118,7 +109,7 @@ jobs:
           fi
 
       - name: Test Examples on .NET Framework net48
-        working-directory: ./AwsEncryptionSDK
+        working-directory: ${{ matrix.library }}
         if: matrix.os == 'windows-latest' 
         shell: bash
         run: |
@@ -127,7 +118,7 @@ jobs:
             --framework net48
 
       - name: Test Examples on .NET net6.0
-        working-directory: ./AwsEncryptionSDK
+        working-directory: ${{ matrix.library }}
         shell: bash
         run: |
           if [ "$RUNNER_OS" == "macOS" ]; then
@@ -140,118 +131,87 @@ jobs:
               runtimes/net/Examples \
               --framework net6.0
           fi
-
-      - name: Unzip ESDK-NET @ v4.0.0 Valid Vectors
-        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources
-        shell: bash
+  testVectors:
+    strategy:
+      fail-fast: false
+      matrix:
+        library: [TestVectors]
+        os: [
+          # Sed script doesn't work properly on windows
+          # windows-latest,
+          ubuntu-latest,
+          macos-13,
+        ]
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: write
+      contents: read
+    env:
+      DOTNET_CLI_TELEMETRY_OPTOUT: 1
+      DOTNET_NOLOGO: 1
+    steps:
+      - name: Support longpaths on Git checkout
         run: |
-          NET_400_VALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Valid/vectors
-          mkdir -p $NET_400_VALID_VECTORS
-          DOWNLOAD_NAME=valid-Net-4.0.0.zip
-          unzip -o -qq $DOWNLOAD_NAME -d $NET_400_VALID_VECTORS
-
-      - name: Run ESDK-NET @ v4.0.0 Valid Vectors expect success
-        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
-        continue-on-error: true
+          git config --global core.longpaths true
+      - uses: actions/checkout@v2
+      - name: Init Submodules
         shell: bash
         run: |
-          NET_400_VALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Valid/vectors
-          ESDK_NET_V400_POLICY="forbid" \
-          DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_VALID_VECTORS/manifest.json" \
-          dotnet test --framework net48
-          ESDK_NET_V400_POLICY="forbid" \
-          DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_VALID_VECTORS/manifest.json" \
-          dotnet test --framework net6.0 --logger "console;verbosity=quiet"
+          git submodule update --init libraries
+          git submodule update --init --recursive mpl
+          
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v2
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 
+          role-session-name: NetTests
+          
+      - name: Setup .NET Core SDK 6
+        uses: actions/setup-dotnet@v3
+        with:
+          dotnet-version: '6.0.x'
 
-      - name: Unzip ESDK-NET @ v4.0.0 Invalid Vectors
-        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources
-        shell: bash
-        run: |
-          NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors
-          mkdir -p $NET_400_INVALID_VECTORS
-          DOWNLOAD_NAME=invalid-Net-4.0.0.zip
-          unzip -o -qq $DOWNLOAD_NAME -d $NET_400_INVALID_VECTORS
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dafny }}
 
-      - name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET 48 expect failure
-        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
-        continue-on-error: true
-        shell: bash
-        run: |
-          NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors
-          ESDK_NET_V400_POLICY="forbid" \
-          DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
-          dotnet test --framework net48
-          # Dotnet test returns 1 for failure.
-          TEMP=$?; if [[ "$TEMP" -eq 1 ]]; then true; else false; fi;
-          # We want this to fail, so if it returned 1, step passes, else it fails
-          # TODO Post-#619: Refactor Test Vectors to expect failure,
-          # as I doubt this true false logic works
+      - name: Regenerate code using smithy-dafny if necessary
+        if: ${{ inputs.regenerate-code }}
+        uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ env.DAFNY_VERSION }}
+          library: ${{ matrix.library }}
+          diff-generated-code: false
+          update-and-regenerate-mpl: true
 
-      - name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET 6.0 expect failure
-        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
-        continue-on-error: true
-        shell: bash
-        run: |
-          NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors
-          if [ "$RUNNER_OS" == "macOS" ]; then
-            ESDK_NET_V400_POLICY="forbid" \
-            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
-            DYLD_LIBRARY_PATH="/usr/local/opt/[email protected]/lib" \
-            dotnet test --framework net6.0
-          else
-            ESDK_NET_V400_POLICY="forbid" \
-            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
-            dotnet test --framework net6.0
-          fi
-          # Dotnet test returns 1 for failure.
-          TEMP=$?; if [[ "$TEMP" -eq 1 ]]; then true; else false; fi;
-          # We want this to fail, so if it returned 1, step passes, else it fails
-          # TODO Post-#619: Refactor Test Vectors to expect failure,
-          # as I doubt this true false logic works
-          
-      - name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET expect Success
-        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
+      - name: Download Dependencies 
+        working-directory: ${{ matrix.library }}
+        run: make setup_net
+
+      - name: Compile ${{ matrix.library }} implementation
         shell: bash
+        working-directory: ${{ matrix.library }}
         run: |
-          NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors
-          DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
-          dotnet test --framework net48 --logger "console;verbosity=quiet"
-          if [ "$RUNNER_OS" == "macOS" ]; then
-            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
-            DYLD_LIBRARY_PATH="/usr/local/opt/[email protected]/lib" \
-            dotnet test --framework net6.0 --logger "console;verbosity=quiet"
-          else
-            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
-            dotnet test --framework net6.0 --logger "console;verbosity=quiet"
-          fi
-
-      - name: Unzip ESDK-NET @ v4.0.1 Vectors
-        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources
+          # 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: |
-          NET_401_VECTORS=$GITHUB_WORKSPACE/v4Net401/vectors
-          mkdir -p $NET_401_VECTORS
-          DOWNLOAD_NAME=v4-Net-4.0.1.zip
-          unzip -o -qq $DOWNLOAD_NAME -d $NET_401_VECTORS
+          unzip invalid-Net-4.0.0.zip -d invalid-Net-4.0.0
+          unzip v4-Net-4.0.1.zip -d v4-Net-4.0.1
+          unzip valid-Net-4.0.0.zip -d valid-Net-4.0.0
 
-      - name: Run ESDK-NET @ v4.0.1 Vectors expect success
-        working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
+      - name: Test .NET net6.0
+        working-directory: ${{ matrix.library }}
         shell: bash
         run: |
-          NET_401_VECTORS=$GITHUB_WORKSPACE/v4Net401/vectors
-          # We expect net48 to run only for Windows
-          if [ "$RUNNER_OS" == "Windows" ]; then
-            ESDK_NET_V400_POLICY="forbid" \
-            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \
-            dotnet test --framework net48
-          fi
           if [ "$RUNNER_OS" == "macOS" ]; then
-            DYLD_LIBRARY_PATH="/usr/local/opt/[email protected]/lib" \
-            ESDK_NET_V400_POLICY="forbid" \
-            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \
-            dotnet test --framework net6.0 --logger "console;verbosity=quiet"
+            make test_net_mac_intel FRAMEWORK=net6.0
           else
-            ESDK_NET_V400_POLICY="forbid" \
-            DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \
-            dotnet test --framework net6.0 --logger "console;verbosity=quiet"
+            make test_net FRAMEWORK=net6.0
           fi

Diff for: TestVectors/dafny/TestVectors/src/EsdkManifestOptions.dfy

@@ -5,11 +5,13 @@ include "LibraryIndex.dfy"
 
 module {:options "-functionSyntax:4"} EsdkManifestOptions {
   import opened Wrappers
+  import Types = AwsCryptographyEncryptionSdkTypes
 
   datatype ManifestOptions =
     | Decrypt(
         nameonly manifestPath: string,
         nameonly manifestFileName: string,
+        nameonly retryPolicy: Types.NetV4_0_0_RetryPolicy,
         nameonly testName: Option<string> := None
       )
     | Encrypt(

Diff for: TestVectors/dafny/TestVectors/src/EsdkTestManifests.dfy

@@ -42,6 +42,8 @@ module {:options "-functionSyntax:4"} EsdkTestManifests {
 
     var decryptVectors :- ParseEsdkJsonManifest.BuildDecryptTestVector(
       op,
+      decryptManifest.clientName,
+      decryptManifest.clientVersion,
       decryptManifest.version,
       decryptManifest.keys,
       decryptManifest.jsonTests
@@ -89,9 +91,7 @@ module {:options "-functionSyntax:4"} EsdkTestManifests {
       print "Skipped: ", skipped, "\n";
     }
 
-    expect !hasFailure;
-
-    manifest := Success([]);
+    manifest := if !hasFailure then Success([]) else Failure("Test Vectors failed, see errors above.\n");
   }
 
   method {:vcs_split_on_every_assert} StartEncryptVectors(
@@ -221,7 +221,8 @@ module {:options "-functionSyntax:4"} EsdkTestManifests {
     | DecryptManifest(
         version: nat,
         keys: KeyVectors.KeyVectorsClient,
-        client: Values.JSON,
+        clientName: string,
+        clientVersion: string,
         jsonTests: seq<(string, Values.JSON)>
       )
     | EncryptManifest(
@@ -250,13 +251,17 @@ module {:options "-functionSyntax:4"} EsdkTestManifests {
     var decryptManifestBv :- FileIO.ReadBytesFromFile(manifestPath + manifestFileName);
     var decryptManifestBytes := BvToBytes(decryptManifestBv);
     var manifestJson :- API.Deserialize(decryptManifestBytes)
-      .MapFailure(( e: Errors.DeserializationError ) => e.ToString());
+    .MapFailure(( e: Errors.DeserializationError ) => e.ToString());
     :- Need(manifestJson.Object?, "Not a JSON object");
 
     var manifest :- GetObject("manifest", manifestJson.obj);
     var version :- GetNat("version", manifest);
     var typ :- GetString("type", manifest);
 
+    var client :- GetObject("client", manifestJson.obj);
+    var clientName :- GetString("name", client);
+    var clientVersion :- GetString("version", client);
+
     var keyManifestUri :- GetString("keys", manifestJson.obj);
     :- Need("file://" < keyManifestUri, "Unexpected URI prefix");
     var keyManifestPath := manifestPath + keyManifestUri[7..];
@@ -269,11 +274,11 @@ module {:options "-functionSyntax:4"} EsdkTestManifests {
     match typ
     case "awses-decrypt" =>
       :- Need(SupportedDecryptVersion?(version), "Unsupported manifest version");
-      var client :- Get("client", manifestJson.obj);
       manifestData := Success(DecryptManifest(
                                 version := version,
                                 keys := keys,
-                                client := client,
+                                clientName := clientName,
+                                clientVersion := clientVersion,
                                 jsonTests := jsonTests
                               ));