From 46aee65edb5b07d488a760ef82b1cbdabc8717e5 Mon Sep 17 00:00:00 2001
From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com>
Date: Tue, 6 Aug 2024 18:07:44 -0400
Subject: [PATCH] fix: add ECDH error message for Rust (#574)

* fix: add ECDH error message for Rust
---
 AwsCryptographyPrimitives/test/TestECDH.dfy | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/AwsCryptographyPrimitives/test/TestECDH.dfy b/AwsCryptographyPrimitives/test/TestECDH.dfy
index b1ad68033..4039e7145 100644
--- a/AwsCryptographyPrimitives/test/TestECDH.dfy
+++ b/AwsCryptographyPrimitives/test/TestECDH.dfy
@@ -124,6 +124,9 @@ module TestECDH {
   const OUT_OF_BOUNDS_ERR_MSG_NET6 := "value invalid for Fp field element (Parameter 'x')"
   const OUT_OF_BOUNDS_ERR_MSG_NE48 := "value invalid for Fp field element\r\nParameter name: x"
 
+  // Rust does not provide a separate error message for infinity or out of bounds
+  const BAD_X509_KEY_ERR_MSG_RUST := "Invalid X509 Public Key."
+
   method {:test} TestKeyGen()
   {
     var supportedCurves := [P256, P384, P521];
@@ -285,6 +288,7 @@ module TestECDH {
       var errMsg := validPublicKey.error.message;
 
       expect (
+          errMsg == BAD_X509_KEY_ERR_MSG_RUST ||
           errMsg == INFINITY_POINT_ERR_MSG_JAVA ||
           errMsg == INFINITY_POINT_ERR_MSG_NET6 ||
           errMsg == INFINITY_POINT_ERR_MSG_NET48
@@ -334,6 +338,7 @@ module TestECDH {
       var errMsg := validPublicKey.error.message;
       expect (
           seq_contains(errMsg, OUT_OF_BOUNDS_ERR_MSG_JAVA) ||
+          errMsg == BAD_X509_KEY_ERR_MSG_RUST ||
           errMsg == OUT_OF_BOUNDS_ERR_MSG_NET6 ||
           errMsg == OUT_OF_BOUNDS_ERR_MSG_NE48
         );