chore(verfication): remove {:only} (aws#517)

Author: josecorella

.github/workflows/check_only_keyword.yml

@@ -0,0 +1,40 @@
+# This workflow checks if you are checking in dafny code
+# with the keyword {:only}, it adds a message to the pull
+# request to remind you to remove it.
+name: Check {:only} decorator presence
+
+on:
+  pull_request:
+
+jobs:
+  grep-only-verification-keyword:
+    runs-on: ubuntu-latest
+    permissions:
+      issues: write
+      pull-requests: write
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+
+      - name: Check only keyword
+        id: only-keyword
+        shell: bash
+        run:
+          # checking in code with the dafny decorator {:only}
+          # will not verify the entire file or maybe the entire project depending on its configuration
+          # This action checks if you are either adding or removing the {:only} decorator and posting on the pr if you are.
+          echo "ONLY_KEYWORD=$(git diff origin/main origin/${GITHUB_HEAD_REF} **/*.dfy | grep -i {:only})" >> "$GITHUB_OUTPUT"
+
+      - name: Check if ONLY_KEYWORD is not empty
+        id: comment
+        env:
+          PR_NUMBER: ${{ github.event.number }}
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          ONLY_KEYWORD: ${{ steps.only-keyword.outputs.ONLY_KEYWORD }}
+        if: ${{env.ONLY_KEYWORD != ''}}
+        run: |
+          COMMENT="It looks like you are adding or removing the dafny keyword {:only}.\nIs this intended?"
+          COMMENT_URL="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/comments"
+          curl -s -H "Authorization: token ${GITHUB_TOKEN}" -X POST $COMMENT_URL -d "{\"body\":\"$COMMENT\"}"
+          exit 1

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy

@@ -439,7 +439,6 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
   {
     const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey
     const cryptoPrimitives: Primitives.AtomicPrimitivesClient
-    const senderPublicKey: seq<uint8>
     const recipientPublicKey: seq<uint8>
     const client: KMS.IKMSClient
     const grantTokens: KMS.GrantTokenList
@@ -582,6 +581,11 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
           }
       }
 
+      :- Need(
+        KMS.IsValid_PublicKeyType(sharedSecretPublicKey),
+        E("Received Recipient Public Key of incorrect expected length")
+      );
+
       //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-ecdh-keyring.md#ondecrypt
       //# The keyring MUST derive the shared secret
       //# by calling [AWS KMS DeriveSharedSecret]()

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy

@@ -541,7 +541,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring {
         && Materials.DecryptionMaterialsTransitionIsValid(materials, res.value)
 
     }
-    method {:vcs_split_on_every_assert} {:only} Invoke(
+    method {:vcs_split_on_every_assert} Invoke(
       edk: Types.EncryptedDataKey,
       ghost attemptsState: seq<ActionInvoke<Types.EncryptedDataKey, Result<Materials.SealedDecryptionMaterials, Types.Error>>>
     ) returns (res: Result<Materials.SealedDecryptionMaterials, Types.Error>)
@@ -851,4 +851,4 @@ module {:options "/functionSyntax:4" } RawECDHKeyring {
   function E(s : string) : Types.Error {
     Types.AwsCryptographicMaterialProvidersException(message := s)
   }
-}
+}