chore: Fail verification on warnings (#766)

Author: seebees

.github/workflows/library_dafny_verification.yml

@@ -40,7 +40,7 @@ jobs:
       - name: Setup .NET Core SDK '6.0.x'
         uses: actions/setup-dotnet@v3
         with:
-          dotnet-version: "6.0.x"
+          dotnet-version: "9.0.x"
 
       - name: Setup Dafny
         uses: ./mpl/.github/actions/setup_dafny

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy

@@ -652,7 +652,7 @@ module EncryptDecryptHelpers {
 
     ensures res.Success? ==>
               && mpl.EncryptionMaterialsHasPlaintextDataKey(res.value).Success?
-              && !res.value.algorithmSuite.commitment.IDENTITY?;
+              && !res.value.algorithmSuite.commitment.IDENTITY?
 
     ensures res.Success? ==>
               && SerializableTypes.IsESDKEncryptionContext(res.value.encryptionContext)

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy

@@ -251,7 +251,7 @@ module MessageBody {
       invariant |regularFrames| == (sequenceNumber - START_SEQUENCE_NUMBER) as nat
       invariant |crypto.History.AESEncrypt| - |old(crypto.History.AESEncrypt)|
              == |regularFrames|
-      invariant 0 < |regularFrames| ==> Seq.First(regularFrames).header == header;
+      invariant 0 < |regularFrames| ==> Seq.First(regularFrames).header == header
       invariant IsMessageRegularFrames(regularFrames)
 
       invariant forall i: nat, j: nat, frame: Frames.Frame, callEvent

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/SerializableTypes.dfy

@@ -30,7 +30,7 @@ module SerializableTypes {
   // The AAD section is the total length|number of pairs|key|value|key|value...
   // The total length is uint16, so the maximum length for the keys and values
   // MUST be able to include the uint16 for the number of pairs.
-  const ESDK_CANONICAL_ENCRYPTION_CONTEXT_MAX_LENGTH := UINT16_LIMIT - 2;
+  const ESDK_CANONICAL_ENCRYPTION_CONTEXT_MAX_LENGTH := UINT16_LIMIT - 2
 
   predicate method IsESDKEncryptionContext(ec: MPL.EncryptionContext) {
     && |ec| < UINT16_LIMIT

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/V2HeaderBody.dfy

@@ -176,7 +176,7 @@ module V2HeaderBody {
   }
 
   // version + suiteId + messageId
-  const headerBytesToAADStart := 1 + 2 + 32;
+  const headerBytesToAADStart := 1 + 2 + 32
   predicate IsV2ExpandedAADSection(
     buffer: ReadableBuffer
   )

AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy

@@ -47,7 +47,7 @@ module TestCreateEsdkClient {
     71, 110, 211, 189, 2, 48, 99, 98, 250, 36, 53, 182, 2, 204, 198, 55, 150, 51,
     159, 101, 231, 34, 42, 30, 57, 204, 88, 114, 138, 94, 12, 79, 52, 71, 178,
     34, 61, 246, 55, 163, 145, 95, 80, 61, 85, 143, 32, 0, 98, 20, 88, 251, 204, 5
-  ];
+  ]
 
   method {:test} TestClientCreation() {
     var defaultConfig := ESDK.DefaultAwsEncryptionSdkConfig();

AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/TestRequiredEncryptionContext.dfy

@@ -24,7 +24,7 @@ module TestRequiredEncryptionContext {
 
   // THIS IS A TESTING RESOURCE DO NOT USE IN A PRODUCTION ENVIRONMENT
   const keyArn := Fixtures.keyArn
-  const hierarchyKeyArn := Fixtures.hierarchyKeyArn;
+  const hierarchyKeyArn := Fixtures.hierarchyKeyArn
   const branchKeyStoreName: DDBTypes.TableName := Fixtures.branchKeyStoreName
   const logicalKeyStoreName := branchKeyStoreName
   // These tests require a keystore populated with these keys

SharedMakefileV2.mk

@@ -13,9 +13,9 @@ VERIFY_TIMEOUT := 150
 
 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