From a86a193349003d3c11127c8e9db81cf41be57902 Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Thu, 29 Aug 2024 12:29:45 -0400 Subject: [PATCH] chore: improve message for failed test vector test (#649) * chore: improve message for failed test vector test --- .../src/TestVectors.dfy | 24 ++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy index 5aff73b03..25de33e48 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestVectors.dfy @@ -82,13 +82,31 @@ 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?; 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 (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"; + } + } } print "\nFAILED! <-----------\n"; }