chore: Remove Dafny warnings (#1742)

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 aws/aws-cryptographic-material-providers-library#517.
This would now cause CI verification to fail.

Author: seebees

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy

@@ -47,9 +47,11 @@ module DdbMiddlewareConfig {
   function SearchModifies(config: Config) : set<object>
   {
     //set x, y | y in config.tableEncryptionConfigs && x in OneSearchModifies(config.tableEncryptionConfigs[y]) :: x
-    set versions <- set configValue <- config.tableEncryptionConfigs.Values | configValue.search.Some? :: configValue.search.value.versions,
-      keyStore <- set version <- versions :: version.keySource.store,
-      obj <- keyStore.Modifies | obj in keyStore.Modifies :: obj
+    set
+      versions <- (set configValue <- config.tableEncryptionConfigs.Values | configValue.search.Some? :: configValue.search.value.versions),
+      keyStore <- (set version <- versions :: version.keySource.store),
+      obj <- keyStore.Modifies
+             {:nowarn} :: obj
 
   }
 

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy

@@ -132,7 +132,7 @@ module
              + (if tableConfig.legacyOverride.Some? then tableConfig.legacyOverride.value.encryptor.Modifies else {})
              + (if tableConfig.search.Some? then tableConfig.search.value.versions[0].keyStore.Modifies else {})
            )
-      :: o;
+           {:nowarn} :: o; // ignore warning for missing trigger on quantifier
 
     var allLogicalTableNames := {};
     var i := 0;

SharedMakefile.mk

@@ -13,9 +13,9 @@ include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk
 
 VERIFY_TIMEOUT := 250
 
-verify:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
-verify_single:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
-verify_service:DAFNY_OPTIONS=--allow-warnings --allow-external-contracts --log-format csv
+verify:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts --log-format csv
+verify_single:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts --log-format csv
+verify_service:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts --log-format csv
 
 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