From 126392941ab8c6174dcd0fb7a99f8ad733f982fb Mon Sep 17 00:00:00 2001 From: seebees Date: Thu, 20 Mar 2025 13:31:30 -0700 Subject: [PATCH 1/4] 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 https://github.com/aws/aws-cryptographic-material-providers-library/pull/517. This would now cause CI verification to fail. --- .../src/DdbMiddlewareConfig.dfy | 8 +++++--- .../dafny/DynamoDbEncryptionTransforms/src/Index.dfy | 2 +- SharedMakefile.mk | 6 +++--- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy index e2c4036f7..68fc8e521 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy @@ -47,9 +47,11 @@ module DdbMiddlewareConfig { function SearchModifies(config: Config) : set { //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 } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy index 77f3b7aab..04587c1c0 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy +++ b/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; var allLogicalTableNames := {}; var i := 0; diff --git a/SharedMakefile.mk b/SharedMakefile.mk index 37f18d5f6..06e523004 100644 --- a/SharedMakefile.mk +++ b/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 From 15563071f958bc37a6491cb55a66381c43aff6a9 Mon Sep 17 00:00:00 2001 From: seebees Date: Thu, 20 Mar 2025 13:50:14 -0700 Subject: [PATCH 2/4] format --- .../DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy index 68fc8e521..e841deb98 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy @@ -51,7 +51,7 @@ module DdbMiddlewareConfig { 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 + {:nowarn} :: obj } From a4b2cbb5a98f7bf295eff5db95cbfc8f572f5c5a Mon Sep 17 00:00:00 2001 From: seebees Date: Mon, 24 Mar 2025 09:04:14 -0700 Subject: [PATCH 3/4] format --- .../dafny/DynamoDbEncryptionTransforms/src/Index.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy index 04587c1c0..15a67e18a 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy +++ b/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 {}) ) - {:nowarn} :: o; + {:nowarn} :: o; var allLogicalTableNames := {}; var i := 0; From a672ef63d17d233d1230ee79da31942048d7fd49 Mon Sep 17 00:00:00 2001 From: seebees Date: Mon, 24 Mar 2025 09:11:54 -0700 Subject: [PATCH 4/4] additional comment --- .../dafny/DynamoDbEncryptionTransforms/src/Index.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy index 15a67e18a..56ba4ea1f 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy +++ b/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 {}) ) - {:nowarn} :: o; + {:nowarn} :: o; // ignore warning for missing trigger on quantifier var allLogicalTableNames := {}; var i := 0;