chore: Remove Dafny warnings (#875)

* chore: Remove Dafny warnings

Remove all Dafny warnings and set warnings to error.
By removing all the errors, --allow-warnings can be removed from verification. This means that any verification warning will now fail the build. This is especially relevant if {:only} is ever committed. See #517. This would now cause CI verification to fail.

Author: seebees

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

@@ -114,7 +114,7 @@ module AwsKmsUtils {
               && getPublicKeyResponse.KeyUsage.value == KMS.KeyUsageType.KEY_AGREEMENT
               && getPublicKeyResponse.PublicKey.Some?
               && var publicKey := getPublicKeyResponse.PublicKey.value;
-              && KMS.IsValid_PublicKeyType(publicKey);
+              && KMS.IsValid_PublicKeyType(publicKey)
   {
     var getPublicKeyRequest := KMS.GetPublicKeyRequest(
       KeyId := awsKmsKey,

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

@@ -68,16 +68,16 @@ module Constants {
     s
 
   // UTF-8 Encoded "aws-kms-ecdh"
-  const KMS_ECDH_PROVIDER_ID: UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("aws-kms-ecdh");
+  const KMS_ECDH_PROVIDER_ID: UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("aws-kms-ecdh")
 
   // UTF-8 Encoded "raw-ecdh"
-  const RAW_ECDH_PROVIDER_ID: UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("raw-ecdh");
+  const RAW_ECDH_PROVIDER_ID: UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("raw-ecdh")
 
   // UTF-8 Encoded "HMAC_SHA384"
-  const ECDH_KDF_PRF_NAME: UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("HMAC_SHA384");
+  const ECDH_KDF_PRF_NAME: UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("HMAC_SHA384")
 
   // UTF-8 Encoded "ecdh-key-derivation"
-  const ECDH_KDF_UTF8: UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("ecdh-key-derivation");
+  const ECDH_KDF_UTF8: UTF8.ValidUTF8Bytes := UTF8.EncodeAscii("ecdh-key-derivation")
 
   type AwsKmsEncryptedDataKey = edk: Types.EncryptedDataKey |
       && edk.keyProviderId == PROVIDER_ID

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/TestEcdhCalculation.dfy

@@ -20,13 +20,13 @@ module TestEcdhCalculation {
   import Base64
 
   // ECC Curve P256 Keys
-  const senderKmsKey    := "arn:aws:kms:us-west-2:370957321024:key/eabdf483-6be2-4d2d-8ee4-8c2583d416e9";
-  const recipientKmsKey := "arn:aws:kms:us-west-2:370957321024:key/0265c8e9-5b6a-4055-8f70-63719e09fda5";
-  const senderArns := [TestUtils.KMS_ECC_256_KEY_ARN_S, TestUtils.KMS_ECC_384_KEY_ARN_S, TestUtils.KMS_ECC_521_KEY_ARN_S];
-  const senderArnPublicKeys := [TestUtils.KMS_ECC_256_PUBLIC_KEY_S, TestUtils.KMS_ECC_384_PUBLIC_KEY_S, TestUtils.KMS_ECC_521_PUBLIC_KEY_S];
-  const privateKeyReceivers := [TestUtils.ECC_P256_PRIVATE, TestUtils.ECC_P384_PRIVATE, TestUtils.ECC_P521_PRIVATE];
-  const publicKeyReceivers := [TestUtils.ECC_P256_PUBLIC, TestUtils.ECC_P384_PUBLIC, TestUtils.ECC_P521_PUBLIC];
-  const curveSpecs := [PrimitiveTypes.ECC_NIST_P256, PrimitiveTypes.ECC_NIST_P384, PrimitiveTypes.ECC_NIST_P521];
+  const senderKmsKey    := "arn:aws:kms:us-west-2:370957321024:key/eabdf483-6be2-4d2d-8ee4-8c2583d416e9"
+  const recipientKmsKey := "arn:aws:kms:us-west-2:370957321024:key/0265c8e9-5b6a-4055-8f70-63719e09fda5"
+  const senderArns := [TestUtils.KMS_ECC_256_KEY_ARN_S, TestUtils.KMS_ECC_384_KEY_ARN_S, TestUtils.KMS_ECC_521_KEY_ARN_S]
+  const senderArnPublicKeys := [TestUtils.KMS_ECC_256_PUBLIC_KEY_S, TestUtils.KMS_ECC_384_PUBLIC_KEY_S, TestUtils.KMS_ECC_521_PUBLIC_KEY_S]
+  const privateKeyReceivers := [TestUtils.ECC_P256_PRIVATE, TestUtils.ECC_P384_PRIVATE, TestUtils.ECC_P521_PRIVATE]
+  const publicKeyReceivers := [TestUtils.ECC_P256_PUBLIC, TestUtils.ECC_P384_PUBLIC, TestUtils.ECC_P521_PUBLIC]
+  const curveSpecs := [PrimitiveTypes.ECC_NIST_P256, PrimitiveTypes.ECC_NIST_P384, PrimitiveTypes.ECC_NIST_P521]
 
   method {:test} TestKmsDeriveSharedSecretOfflineCalculation() {
     var kmsClient :- expect Kms.KMSClient();

AwsCryptographyPrimitives/test/TestRSA.dfy

@@ -117,7 +117,7 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA {
   }
 
   method {:test} TestingPemParsingInRSAEncryptionForRSAKeyPairStoredInPEM() {
-    var allPadding := set p: AtomicPrimitives.Types.RSAPaddingMode | true :: p;
+    var allPadding := set p: AtomicPrimitives.Types.RSAPaddingMode {:nowarn} | true :: p;
 
     var PublicKeyFromGenerateRSAKeyPairPemBytes :- expect UTF8.Encode(StaticPublicKeyFromGenerateRSAKeyPair());
     var PrivateKeyFromGenerateRSAKeyPairPemBytes :- expect UTF8.Encode(StaticPrivateKeyFromGenerateRSAKeyPair());
@@ -150,7 +150,7 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA {
   }
 
   method {:test} TestingPemParsingInRSAEncryptionForOnlyRSAPrivateKeyStoredInPEM() {
-    var allPadding := set p: AtomicPrimitives.Types.RSAPaddingMode | true :: p;
+    var allPadding := set p: AtomicPrimitives.Types.RSAPaddingMode {:nowarn} | true :: p;
 
     var PublicKeyFromTestVectorsPemBytes :- expect UTF8.Encode(StaticPublicKeyFromTestVectors());
     var PrivateKeyFromTestVectorsPemBytes :- expect UTF8.Encode(StaticPrivateKeyFromTestVectors());

SharedMakefileV2.mk

@@ -11,9 +11,9 @@ GRADLEW := ./runtimes/java/gradlew
 
 include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk
 
-verify:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts
-verify_single:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts
-verify_service:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts
+verify:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts
+verify_single:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts
+verify_service:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts
 
 transpile_implementation_net: DAFNY_OPTIONS=--allow-warnings --compile-suffix --legacy-module-names --allow-external-contracts
 transpile_test_net: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix --legacy-module-names --allow-external-contracts