Merge branch 'ajewell/measure' into ajewell/ghost-encode-ascii

Author: ajewellamz

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

@@ -138,7 +138,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