Fixing the "points_to" definition for the EC methods struct.

apetcher-amazon · May 14, 2024 · c92aa1a · c92aa1a
1 parent f569cb1
commit c92aa1a
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 11 deletions.
diff --git a/SAW/proof/EC/EC.saw b/SAW/proof/EC/EC.saw
@@ -42,8 +42,8 @@ let points_to_AWSLC_fips_evp_pkey_methods = do {
 let points_to_ec_method_st ptr = do {
   crucible_points_to (crucible_field ptr "point_get_affine_coordinates") (crucible_global "ec_GFp_nistp384_point_get_affine_coordinates");
   crucible_points_to (crucible_field ptr "jacobian_to_affine_batch") (crucible_global "ec_GFp_mont_jacobian_to_affine_batch");
-  crucible_points_to (crucible_field ptr "add") (crucible_global "ec_GFp_mont_add");
-  crucible_points_to (crucible_field ptr "dbl") (crucible_global "ec_GFp_mont_dbl");
+  crucible_points_to (crucible_field ptr "add") (crucible_global "ec_GFp_nistp384_add");
+  crucible_points_to (crucible_field ptr "dbl") (crucible_global "ec_GFp_nistp384_dbl");
   crucible_points_to (crucible_field ptr "mul") (crucible_global "ec_GFp_nistp384_point_mul");
   crucible_points_to (crucible_field ptr "mul_base") (crucible_global "ec_GFp_nistp384_point_mul_base");
   crucible_points_to (crucible_field ptr "mul_batch") (crucible_global "ec_GFp_mont_mul_batch");
@@ -59,7 +59,7 @@ let points_to_ec_method_st ptr = do {
   crucible_points_to (crucible_field ptr "felem_exp") (crucible_global "ec_GFp_mont_felem_exp");
   crucible_points_to (crucible_field ptr "scalar_inv0_montgomery") (crucible_global "ec_simple_scalar_inv0_montgomery");
   crucible_points_to (crucible_field ptr "scalar_to_montgomery_inv_vartime") (crucible_global "ec_simple_scalar_to_montgomery_inv_vartime");
-  crucible_points_to (crucible_field ptr "cmp_x_coordinate") (crucible_global "ec_GFp_mont_cmp_x_coordinate");
+  crucible_points_to (crucible_field ptr "cmp_x_coordinate") (crucible_global "ec_GFp_nistp384_cmp_x_coordinate");
 };
 
 let points_to_built_in_curve ptr ec_method_ptr = do {
@@ -706,10 +706,10 @@ let ec_cmp_x_coordinate_spec = do {
 };
 
 // This spec is identical to that of ec_cmp_x_coordinate, as that
-// function directly invokes ec_GFp_mont_cmp_x_coordinate. When compiled with
+// function directly invokes ec_GFp_nistp384_cmp_x_coordinate. When compiled with
 // optimizations, ec_cmp_x_coordinate will be inlined away, exposing a
-// call site to ec_GFp_mont_cmp_x_coordinate.
-let ec_GFp_mont_cmp_x_coordinate_spec = ec_cmp_x_coordinate_spec;
+// call site to ec_GFp_nistp384_cmp_x_coordinate.
+let ec_GFp_nistp384_cmp_x_coordinate_spec = ec_cmp_x_coordinate_spec;
 
 let ec_get_x_coordinate_as_scalar_spec = do {
   group_ptr <- pointer_to_fresh_ec_group_st;
@@ -1292,10 +1292,10 @@ ec_cmp_x_coordinate_ov <- crucible_llvm_unsafe_assume_spec
   "ec_cmp_x_coordinate"
   ec_cmp_x_coordinate_spec;
 
-ec_GFp_mont_cmp_x_coordinate_ov <- llvm_unsafe_assume_spec
+ec_GFp_nistp384_cmp_x_coordinate_ov <- llvm_unsafe_assume_spec
   m
-  "ec_GFp_mont_cmp_x_coordinate"
-  ec_GFp_mont_cmp_x_coordinate_spec;
+  "ec_GFp_nistp384_cmp_x_coordinate"
+  ec_GFp_nistp384_cmp_x_coordinate_spec;
 
 
 BN_num_bytes_ec_bits_ov <- llvm_verify m "BN_num_bytes"

diff --git a/SAW/proof/ECDSA/verify-ECDSA.saw b/SAW/proof/ECDSA/verify-ECDSA.saw
@@ -86,7 +86,7 @@ ECDSA_do_sign_ov <- llvm_verify m "ECDSA_do_sign"
   , ec_point_mul_scalar_base_ov
   , ec_GFp_simple_is_on_curve_ov
   , ec_GFp_mont_mul_public_batch_ov
-  , ec_GFp_mont_cmp_x_coordinate_ov
+  , ec_GFp_nistp384_cmp_x_coordinate_ov
   , value_barrier_w_ov
   , value_barrier_u32_ov
   ]
@@ -136,7 +136,7 @@ ecdsa_do_verify_no_self_test_ov <- llvm_verify m "ecdsa_do_verify_no_self_test"
   , ERR_put_error_ov
   , ec_GFp_simple_is_on_curve_ov
   , p384_point_mul_public_ov
-  , ec_GFp_mont_cmp_x_coordinate_ov
+  , ec_GFp_nistp384_cmp_x_coordinate_ov
   ]
   true
   ecdsa_do_verify_no_self_test_spec