From bb741b48fd74c1f01a1bc01104ad115ccf91c12a Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 29 Aug 2024 10:43:41 -0400 Subject: [PATCH 1/2] chore: improve message for failed test vector test --- .../src/TestVectors.dfy | 22 +++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy index 5aff73b03..42f1b20fa 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy @@ -87,8 +87,26 @@ module {:options "-functionSyntax:4"} TestVectors { => !result.Success?; if !output { - if test.vector.PositiveDecryptKeyringTest? && result.Failure? { - print result.error; + if test.vector.PositiveDecryptKeyringTest? { + if result.Failure? { + print "Error : ", result.error, "\n"; + } else { + if (result.value.decryptionMaterials.plaintextDataKey != test.vector.expectedResult.plaintextDataKey) { + print "Error : plaintextDataKey does not match.\n", + test.vector.expectedResult.plaintextDataKey, "\n", + result.value.decryptionMaterials.plaintextDataKey, "\n"; + } + if (result.value.decryptionMaterials.symmetricSigningKey != test.vector.expectedResult.symmetricSigningKey) { + print "Error : symmetricSigningKey does not match.\n", + test.vector.expectedResult.symmetricSigningKey, "\n", + result.value.decryptionMaterials.symmetricSigningKey, "\n"; + } + if (result.value.decryptionMaterials.requiredEncryptionContextKeys != test.vector.expectedResult.requiredEncryptionContextKeys) { + print "Error : requiredEncryptionContextKeys does not match.\n", |result.value.decryptionMaterials.requiredEncryptionContextKeys|, + " ", |test.vector.expectedResult.requiredEncryptionContextKeys|, "\n", test.vector.expectedResult.requiredEncryptionContextKeys, + "\n", result.value.decryptionMaterials.requiredEncryptionContextKeys, "\n"; + } + } } print "\nFAILED! <-----------\n"; } From fd5aae1f515f319247f9d72a588c3d458631765b Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 29 Aug 2024 11:24:55 -0400 Subject: [PATCH 2/2] m --- .../src/TestVectors.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy index 42f1b20fa..25de33e48 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy @@ -82,7 +82,7 @@ module {:options "-functionSyntax:4"} TestVectors { && result.Success? && result.value.decryptionMaterials.plaintextDataKey == test.vector.expectedResult.plaintextDataKey && result.value.decryptionMaterials.symmetricSigningKey == test.vector.expectedResult.symmetricSigningKey - && result.value.decryptionMaterials.requiredEncryptionContextKeys == test.vector.expectedResult.requiredEncryptionContextKeys + && multiset(result.value.decryptionMaterials.requiredEncryptionContextKeys) == multiset(test.vector.expectedResult.requiredEncryptionContextKeys) case NegativeDecryptKeyringTest(_,_,_,_,_,_,_,_,_) => !result.Success?; @@ -101,7 +101,7 @@ module {:options "-functionSyntax:4"} TestVectors { test.vector.expectedResult.symmetricSigningKey, "\n", result.value.decryptionMaterials.symmetricSigningKey, "\n"; } - if (result.value.decryptionMaterials.requiredEncryptionContextKeys != test.vector.expectedResult.requiredEncryptionContextKeys) { + if (multiset(result.value.decryptionMaterials.requiredEncryptionContextKeys) != multiset(test.vector.expectedResult.requiredEncryptionContextKeys)) { print "Error : requiredEncryptionContextKeys does not match.\n", |result.value.decryptionMaterials.requiredEncryptionContextKeys|, " ", |test.vector.expectedResult.requiredEncryptionContextKeys|, "\n", test.vector.expectedResult.requiredEncryptionContextKeys, "\n", result.value.decryptionMaterials.requiredEncryptionContextKeys, "\n";