Fixing a couple of bugs

apetcher-amazon · Mar 29, 2024 · df4d524 · df4d524
1 parent c1150bb
commit df4d524
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/SAW/patch/p384_validate.patch b/SAW/patch/p384_validate.patch
@@ -2,7 +2,7 @@ diff --git a/crypto/fipsmodule/ec/ec_test.cc b/crypto/fipsmodule/ec/ec_test.cc
 index b1d0f789c..e60c42b02 100644
 --- a/crypto/fipsmodule/ec/ec_test.cc
 +++ b/crypto/fipsmodule/ec/ec_test.cc
-@@ -2355,3 +2355,11 @@ TEST(ECTest, FelemBytes) {
+@@ -2355,3 +2355,4 @@ TEST(ECTest, FelemBytes) {
      ASSERT_EQ(test_group.get()->field.N.width, expected_felem_words);
    }
  }

diff --git a/SAW/proof/EC/EC_P384_primitives.saw b/SAW/proof/EC/EC_P384_primitives.saw
@@ -9,6 +9,7 @@ import "../../../cryptol-specs/Common/EC/EC_P384.cry";
 
 let limb_length = 64;
 let p384_felem_limbs = 6;
+let EC_MAX_BYTES = 66;
 
 let {{ ia32cap = [0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff] : [4][32] }};