Added SAW proof for top-level constant validation function.

apetcher-amazon · Apr 8, 2024 · f5dad26 · f5dad26
1 parent f159c0a
commit f5dad26
Show file tree

Hide file tree

Showing 2 changed files with 38 additions and 6 deletions.
diff --git a/SAW/proof/EC/EC_P384_validate.saw b/SAW/proof/EC/EC_P384_validate.saw
@@ -152,17 +152,31 @@ let p384_validate_base_table_spec = do {
   crucible_return (crucible_term {{ (zero:[31]) # [validate_base_table pre_comp_table] }});
 };
 
-let p384_validate_one_spec = do {
+let p384_validate_one_constant_spec = do {
 
   global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
 
   crucible_execute_func [];
 
   global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};
 
-  crucible_return (crucible_term {{ (zero:[31]) # [validate_one p384_felem_one] }});
+  crucible_return (crucible_term {{ (zero:[31]) # [validate_one_wrapper u p384_felem_one] }});
 };
 
+let p384_validate_constants_spec = do {
+
+  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+  pre_comp_table <- crucible_fresh_var "pre_comp_table" (llvm_array 20 (llvm_array 16 (llvm_array 2 (llvm_array p384_felem_limbs (llvm_int limb_length)))));
+  global_points_to "p384_g_pre_comp" pre_comp_table;
+
+  crucible_execute_func [];
+
+  global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};
+
+  crucible_return (crucible_term {{ (zero:[31]) # [(validate_base_table pre_comp_table) && (validate_one p384_felem_one)] }});
+};
+
+
 p384_validate_base_table_ov <- llvm_verify m "p384_validate_base_table"
   [ p384_validate_base_table_row_ov,
 	point_double_n_20_ov
@@ -173,13 +187,28 @@ p384_validate_base_table_ov <- llvm_verify m "p384_validate_base_table"
     w4_unint_z3 ["validate_base_row", "point_double_base_tsize"];
   });
 
+validate_one_wrapper_validate_one_equiv <-
+  prove_print
+  (w4_unint_z3 ["validate_one"])
+  (rewrite (cryptol_ss ()) {{ \x y -> (validate_one_wrapper x y) == (validate_one y) }});
+
+
 p384_validate_one_ov <- llvm_verify m "p384_validate_one"
   [bignum_tomont_p384_same_constant_ov, felem_ne_constant_ov]
-  false
-  p384_validate_one_spec
+  true
+  p384_validate_one_constant_spec
+  (do {
+    simplify (addsimps [felem_ne_wrapper_felem_ne_equiv, felem_to_mont_wrapper_felem_to_mont_equiv, validate_one_wrapper_validate_one_equiv] empty_ss);
+    w4_unint_z3 ["felem_to_mont", "felem_ne"];
+  });
+
+p384_validate_constants_ov <- llvm_verify m "p384_validate_constants"
+  [p384_validate_base_table_ov, p384_validate_one_ov]
+  true
+  p384_validate_constants_spec
   (do {
-    simplify (addsimps [felem_ne_wrapper_felem_ne_equiv, felem_to_mont_wrapper_felem_to_mont_equiv] empty_ss);
-    w4_unint_z3 ["felem_to_mont", "felem_sub"];
+    simplify (addsimps [validate_one_wrapper_validate_one_equiv] empty_ss);
+    w4_unint_z3 ["validate_base_table", "validate_one"];
   });
 
 
diff --git a/SAW/spec/EC/EC_mul.cry b/SAW/spec/EC/EC_mul.cry
@@ -371,6 +371,9 @@ validate_one f = res
     cmp_f = felem_to_mont felem_one
     res = if (felem_ne cmp_f f) == 0 then 1 else 0
 
+validate_one_wrapper: () -> felem -> Bit
+validate_one_wrapper _ x = validate_one x
+
 
 ECDH_derive_bv : JacobianBVPoint -> scalar -> [bit_length]
 ECDH_derive_bv peer_pub_key priv_key =