From 7df5d98b983a2542288368a1167f7eb6acd34d58 Mon Sep 17 00:00:00 2001 From: Ritvik Kapila Date: Mon, 18 Nov 2024 09:37:11 -0800 Subject: [PATCH 1/3] chore(TestVectors): add DefaultCmm Tests --- .../TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy | 1 + 1 file changed, 1 insertion(+) diff --git a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy index 64fd2441e..5d750d326 100644 --- a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy +++ b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy @@ -46,6 +46,7 @@ module {:options "/functionSyntax:4"} AllEsdkV4NoReqEc { const AllPositiveKeyringTestsNoReqCmmNoKmsRsa := {} + + AllDefaultCmm.Tests + AllHierarchy.Tests + AllKms.Tests + AllKmsMrkAware.Tests From e23afabef2fb493faa948998a824c5c6bb2b5acb Mon Sep 17 00:00:00 2001 From: Ritvik Kapila Date: Mon, 18 Nov 2024 10:01:16 -0800 Subject: [PATCH 2/3] add only SuccessTestingRequiredECKeysReproducedEC --- .../TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy index 5d750d326..32b45ef0c 100644 --- a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy +++ b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy @@ -46,7 +46,7 @@ module {:options "/functionSyntax:4"} AllEsdkV4NoReqEc { const AllPositiveKeyringTestsNoReqCmmNoKmsRsa := {} - + AllDefaultCmm.Tests + + AllDefaultCmm.SuccessTestingRequiredEncryptionContextKeysReproducedEncryptionContext + AllHierarchy.Tests + AllKms.Tests + AllKmsMrkAware.Tests From 43b94ced6ca5d39a8eef3431beeea8d32903d3ef Mon Sep 17 00:00:00 2001 From: Ritvik Kapila Date: Mon, 18 Nov 2024 12:35:32 -0800 Subject: [PATCH 3/3] fix --- .../TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy index beacc23b6..c74b1b460 100644 --- a/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy +++ b/TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy @@ -34,7 +34,7 @@ module {:options "/functionSyntax:4" } AllEsdkV4WithReqEc { const AllPositiveReqEcTests := AllRequiredEncryptionContextCmm.SuccessTestingRequiredEncryptionContextKeysReproducedEncryptionContext // These are only required encryption context vectors with static aes keyrings - const AllPositveReqEcEsdkTests := + const AllPositiveReqEcEsdkTests := set config <- AllPositiveReqEcTests, algorithmSuite <- @@ -55,5 +55,5 @@ module {:options "/functionSyntax:4" } AllEsdkV4WithReqEc { ) const Tests := - AllPositveReqEcEsdkTests + AllPositiveReqEcEsdkTests } \ No newline at end of file