Update points-to preconditions for ec_group_st and ec_method_st (#126)

.gitmodules

@@ -1,7 +1,7 @@
 [submodule "src"]
 	path = src
-	branch = main
-	url = https://github.com/aws/aws-lc.git
+	branch = upstream-merge-2023-11-20
+	url = https://github.com/torben-hansen/aws-lc.git
 [submodule "cryptol-specs"]
 	path = cryptol-specs
 	branch = sha-imperative

SAW/proof/BN/BN.saw

@@ -168,6 +168,24 @@ let pointer_to_bn_mont_ctx_st num N = do {
   return (RR_d_ptr, ptr);
 };
 
+let points_to_bn_mont_ctx_st ptr num N = do {
+  let num_bits = eval_size {| num * 64 |};
+  let RR_bn_dmax = eval_size {| 2 * num + 1 |};
+  let R = {{ 2 ^^ `num_bits }};
+
+  RR_d_ptr <- crucible_alloc_readonly (llvm_int num_bits);
+  crucible_points_to RR_d_ptr (crucible_term {{ (fromInteger ((R * R) % `N)) : [num_bits] }});
+  points_to_bignum_st (crucible_field ptr "RR") RR_d_ptr num RR_bn_dmax {{ 0 : [32] }};
+
+  let n0 = eval_int {{ bn_mont_n0`{N} }};
+  crucible_points_to_untyped (crucible_field ptr "n0") (crucible_term {{ `n0 : [64] }});
+
+  N_d_ptr <- crucible_alloc_readonly (llvm_int num_bits);
+  crucible_points_to N_d_ptr (crucible_term {{ (fromInteger `N) : [num_bits] }});
+  points_to_bignum_st (crucible_field ptr "N") N_d_ptr num num {{ 0 : [32] }};
+};
+
+
 let {{
 bn_mont_n0_with_N : {a} (fin a) => [a][64] -> [64]
 bn_mont_n0_with_N n = undefined

SAW/proof/EC/EC.saw

@@ -40,9 +40,6 @@ let points_to_AWSLC_fips_evp_pkey_methods = do {
 
 
 let points_to_ec_method_st ptr = do {
-  crucible_points_to (crucible_field ptr "group_init") (crucible_global "ec_GFp_mont_group_init");
-  crucible_points_to (crucible_field ptr "group_finish") (crucible_global "ec_GFp_mont_group_finish");
-  crucible_points_to (crucible_field ptr "group_set_curve") (crucible_global "ec_GFp_mont_group_set_curve");
   crucible_points_to (crucible_field ptr "point_get_affine_coordinates") (crucible_global "ec_GFp_mont_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");
@@ -151,21 +148,14 @@ let pointer_to_fresh_ec_group_st_with_curve_name curve_name = do {
 
   crucible_points_to (crucible_field ptr "curve_name") (crucible_term {{ `curve_name : [32] }});
 
-  (_, order_mont_ptr) <- pointer_to_bn_mont_ctx_st ec_words {| P384_n |};
-  crucible_points_to (crucible_field ptr "order") order_mont_ptr;
-
-  field_d_ptr <- crucible_alloc_readonly i384;
-  crucible_points_to field_d_ptr (crucible_term {{ fromInteger`{[P384_w]} `P384_p }});
-  points_to_p384_bignum_st (crucible_field ptr "field") field_d_ptr {{ 0 : [32] }};
+  points_to_bn_mont_ctx_st (crucible_field ptr "order") ec_words {| P384_n |};
+  points_to_bn_mont_ctx_st (crucible_field ptr "field") ec_words {| P384_p |};
 
   crucible_points_to_untyped (crucible_field ptr "a") (crucible_term {{ fieldElementToBV ((P384_a * P384_R_p) % `P384_p) }});
   crucible_points_to_untyped (crucible_field ptr "b") (crucible_term {{ fieldElementToBV ((P384_b * P384_R_p) % `P384_p) }});
   crucible_points_to (crucible_field ptr "a_is_minus3") (crucible_term {{ 1 : [32] }});
   crucible_points_to (crucible_field ptr "field_greater_than_order") (crucible_term {{ 1 : [32] }});
 
-  (_, mont_ptr) <- pointer_to_bn_mont_ctx_st ec_words {| P384_p |};
-  crucible_points_to (crucible_field ptr "mont") mont_ptr;
-
   crucible_points_to_untyped (crucible_field ptr "one") (crucible_term {{ fieldElementToBV P384_R_p }});
 
   return ptr;

SAW/proof/EC/EC_P384_private.saw

@@ -8,6 +8,7 @@ import "../../spec/EC/EC_P384_5.cry";
 include "../common/helpers.saw";
 include "../common/internal.saw";
 include "EC_P384_primitives.saw";
+include "../BN/BN.saw";
 
 let limb_length = 64;
 let p384_felem_limbs = 6;
@@ -197,19 +198,14 @@ ec_compute_wNAF_in_range_lemma <-
     (w4_unint_z3 [])
     (rewrite (cryptol_ss ()) {{ \scalar -> ec_compute_wNAF_in_range (ec_compute_wNAF scalar) }});
 
-let points_to_ec_group_st_initialized_order_width ptr width = do {
-  order_mont_ptr <- crucible_alloc_readonly (llvm_struct "struct.bn_mont_ctx_st");
-  crucible_points_to (crucible_field (crucible_field order_mont_ptr "N") "width") width;
-  crucible_points_to (crucible_field ptr "order") order_mont_ptr;
-};
 
 let ec_compute_wNAF_out = "ec_compute_wNAF.out";
 let ec_compute_wNAF_range = "ec_compute_wNAF.range";
 
 let ec_compute_wNAF_spec w order_width = do {
 
   group_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_group_st");
-  points_to_ec_group_st_initialized_order_width group_ptr (crucible_term {{ `order_width : [32] }});
+  points_to_bn_mont_ctx_st (crucible_field group_ptr "order") order_width {| P384_n |};
   out_ptr <- crucible_alloc (llvm_array 385 i8);
   (scalar, scalar_ptr) <- ptr_to_fresh_readonly "scalar" i384;
 
@@ -291,7 +287,7 @@ let ec_GFp_nistp384_point_mul_public_loop_spec = do {
 
   // pointer to group
   group_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_group_st");
-  points_to_ec_group_st_initialized_order_width group_ptr (crucible_term {{ `p384_felem_limbs : [32] }});
+  points_to_bn_mont_ctx_st (crucible_field group_ptr "order") p384_felem_limbs {| P384_n |};
   group_pp <- llvm_alloc (llvm_int 64);
   llvm_points_to group_pp group_ptr;
 
@@ -452,7 +448,7 @@ let p384_point_mul_public_spec order_width = do {
   global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
 
   group_ptr <- crucible_alloc_readonly (llvm_struct "struct.ec_group_st");
-  points_to_ec_group_st_initialized_order_width group_ptr (crucible_term {{ `order_width : [32] }});
+  points_to_bn_mont_ctx_st (crucible_field group_ptr "order") order_width {| P384_n |};
   r_ptr <- crucible_alloc (llvm_struct "struct.EC_JACOBIAN");
   (g_scalar, g_scalar_ptr) <- ptr_to_fresh_readonly "g_scalar" i384;
   p_ptr <- crucible_alloc_readonly (llvm_struct "struct.EC_JACOBIAN");

SAW/proof/EC/verify-P384.saw

@@ -1,3 +1,7 @@
+/*
+* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+* SPDX-License-Identifier: Apache-2.0
+*/
 
 enable_experimental;