From 6a703de9442d920a12b74f4ebf64730ee18beccb Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 29 Apr 2024 07:15:10 -0400 Subject: [PATCH 1/8] chore: Update MPL to 1.3.0 --- project.properties | 2 +- submodules/MaterialProviders | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/project.properties b/project.properties index 30877786f..b4cf8f582 100644 --- a/project.properties +++ b/project.properties @@ -1,4 +1,4 @@ projectJavaVersion=3.3.0 -mplDependencyJavaVersion=1.2.0 +mplDependencyJavaVersion=1.3.0 dafnyRuntimeJavaVersion=4.2.0 smithyDafnyJavaConversionVersion=0.1 diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index 3e2a1654a..0b9567d85 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit 3e2a1654a12e64fc0e76a117f6641ec761f8f241 +Subproject commit 0b9567d85de6e5af6d21603ff547a1f184649dfd From 1937d6370488a65883bf6a0bf4ee9a1a0fa84d65 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 29 Apr 2024 08:59:29 -0400 Subject: [PATCH 2/8] typos --- TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy index 1471408bc..ad3c6d49a 100644 --- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy +++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy @@ -33,7 +33,7 @@ module {:options "-functionSyntax:4"} JsonConfig { import DynamoDbItemEncryptor - const DEFAULT_KEYS := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json" + const DEFAULT_KEYS : string := "../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json" predicate IsValidInt32(x: int) { -0x8000_0000 <= x < 0x8000_0000} type ConfigName = string @@ -298,7 +298,7 @@ module {:options "-functionSyntax:4"} JsonConfig { var keys :- expect KeyVectors.KeyVectors( KeyVectorsTypes.KeyVectorsConfig( - keyManifiestPath := DEFAULT_KEYS + keyManifestPath := DEFAULT_KEYS ) ); var keyDescription :- @@ -311,7 +311,7 @@ module {:options "-functionSyntax:4"} JsonConfig { .MapFailure(ParseJsonManifests.ErrorToString); Success(keyOut.keyDescription); - var keyring :- expect keys.CreateWappedTestVectorKeyring(KeyVectorsTypes.TestVectorKeyringInput(keyDescription := keyDescription)); + var keyring :- expect keys.CreateWrappedTestVectorKeyring(KeyVectorsTypes.TestVectorKeyringInput(keyDescription := keyDescription)); var encryptorConfig := ENC.DynamoDbItemEncryptorConfig( @@ -402,7 +402,7 @@ module {:options "-functionSyntax:4"} JsonConfig { var keys :- expect KeyVectors.KeyVectors( KeyVectorsTypes.KeyVectorsConfig( - keyManifiestPath := DEFAULT_KEYS + keyManifestPath := DEFAULT_KEYS ) ); var keyDescription :- @@ -415,7 +415,7 @@ module {:options "-functionSyntax:4"} JsonConfig { .MapFailure(ParseJsonManifests.ErrorToString); Success(keyOut.keyDescription); - var keyring :- expect keys.CreateWappedTestVectorKeyring(KeyVectorsTypes.TestVectorKeyringInput(keyDescription := keyDescription)); + var keyring :- expect keys.CreateWrappedTestVectorKeyring(KeyVectorsTypes.TestVectorKeyringInput(keyDescription := keyDescription)); var config := Types.DynamoDbTableEncryptionConfig( From f8e5ac387d3b831b1cafff73b0ed4b404b858d71 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 29 Apr 2024 11:34:19 -0400 Subject: [PATCH 3/8] verify --- .../dafny/DynamoDbItemEncryptor/src/Index.dfy | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy index 0c8dc3566..c42bd2698 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy @@ -214,6 +214,13 @@ module var client := new DynamoDbItemEncryptorClient(internalConfig); + assert fresh(client.History); + assert client.Modifies == Operations.ModifiesInternalConfig(internalConfig) + {client.History}; + assert Operations.ModifiesInternalConfig(internalConfig) == + internalConfig.cmm.Modifies + + internalConfig.structuredEncryption.Modifies + + internalConfig.cmpClient.Modifies; + assert fresh(client.Modifies - ( if config.keyring.Some? then config.keyring.value.Modifies else {}) - ( if config.cmm.Some? then config.cmm.value.Modifies else {} ) From 6299194fcc7193fde20efa90d5c90e9da5f0cbf0 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 29 Apr 2024 15:33:18 -0400 Subject: [PATCH 4/8] resolve issue with extra main entry point in dotnet --- .github/workflows/ci_test_vector_net.yml | 2 ++ TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 4 ---- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index 34d3f0017..74fbc4f02 100644 --- a/.github/workflows/ci_test_vector_net.yml +++ b/.github/workflows/ci_test_vector_net.yml @@ -52,6 +52,8 @@ jobs: shell: bash working-directory: ./TestVectors run: | + # this is evil, but the MPL test vectors defines an extra Main + sed -i '' 's/method Main/method NotMain/' ../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy # This works because `node` is installed by default on GHA runners make transpile_net diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index b8ff98b15..09a490d7d 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -31,12 +31,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { import DDB = ComAmazonawsDynamodbTypes import Filter = DynamoDBFilterExpr import SE = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes - import SKS = CreateStaticKeyStores - import KeyMaterial import UTF8 - import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes import CMP = AwsCryptographyMaterialProvidersTypes - import KeyVectors import CreateInterceptedDDBClient import SortedSets import Seq From 82c6bb645d458198056add96f049053e0cfd1ebc Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 29 Apr 2024 15:35:53 -0400 Subject: [PATCH 5/8] m --- .github/workflows/ci_test_vector_net.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index 74fbc4f02..e9c626e76 100644 --- a/.github/workflows/ci_test_vector_net.yml +++ b/.github/workflows/ci_test_vector_net.yml @@ -53,7 +53,7 @@ jobs: working-directory: ./TestVectors run: | # this is evil, but the MPL test vectors defines an extra Main - sed -i '' 's/method Main/method NotMain/' ../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy + sed -i "" "s/method Main/method NotMain/" ../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy # This works because `node` is installed by default on GHA runners make transpile_net From 0ae62351926007dda1b4280e0bd40618db9b9280 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 29 Apr 2024 15:38:02 -0400 Subject: [PATCH 6/8] m --- .github/workflows/ci_test_vector_net.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index e9c626e76..10eea53f7 100644 --- a/.github/workflows/ci_test_vector_net.yml +++ b/.github/workflows/ci_test_vector_net.yml @@ -53,7 +53,7 @@ jobs: working-directory: ./TestVectors run: | # this is evil, but the MPL test vectors defines an extra Main - sed -i "" "s/method Main/method NotMain/" ../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy + sed -i "s/method Main/method NotMain/" ../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy # This works because `node` is installed by default on GHA runners make transpile_net From ce326512b49fed2e89df50bceaeb04dee1e96a34 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 29 Apr 2024 15:58:15 -0400 Subject: [PATCH 7/8] m --- .github/workflows/ci_test_vector_net.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index 10eea53f7..5680d1c97 100644 --- a/.github/workflows/ci_test_vector_net.yml +++ b/.github/workflows/ci_test_vector_net.yml @@ -54,6 +54,7 @@ jobs: run: | # this is evil, but the MPL test vectors defines an extra Main sed -i "s/method Main/method NotMain/" ../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy + sed -i "s/Exe/Library/" ../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/TestVectors.csproj # This works because `node` is installed by default on GHA runners make transpile_net From 166a94597828f16c77eb9c2f6725fb075a93a6c0 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 29 Apr 2024 17:16:11 -0400 Subject: [PATCH 8/8] update to latest MPL --- .github/workflows/ci_test_vector_net.yml | 3 --- submodules/MaterialProviders | 2 +- 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml index 5680d1c97..34d3f0017 100644 --- a/.github/workflows/ci_test_vector_net.yml +++ b/.github/workflows/ci_test_vector_net.yml @@ -52,9 +52,6 @@ jobs: shell: bash working-directory: ./TestVectors run: | - # this is evil, but the MPL test vectors defines an extra Main - sed -i "s/method Main/method NotMain/" ../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/Index.dfy - sed -i "s/Exe/Library/" ../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/TestVectors.csproj # This works because `node` is installed by default on GHA runners make transpile_net diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index 0b9567d85..5f8d816df 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit 0b9567d85de6e5af6d21603ff547a1f184649dfd +Subproject commit 5f8d816df1febed28bed1ba6c63cc9c826ae61a8