Updating ECDSA specs.

apetcher-amazon · May 8, 2024 · 350908d · 350908d
1 parent dee351a
commit 350908d
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git a/SAW/proof/ECDSA/ECDSA.saw b/SAW/proof/ECDSA/ECDSA.saw
@@ -92,6 +92,7 @@ let nondeterministic_valid_k priv_key digest internal = do {
 
 let ECDSA_do_sign_spec = do {
   global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+  alloc_p384_felem_methods_globals;
 
   (digest, digest_ptr) <- ptr_to_fresh_readonly "digest" (llvm_array SHA_DIGEST_LENGTH i8);
 
@@ -124,6 +125,7 @@ let ECDSA_do_sign_spec = do {
 
 let ecdsa_do_verify_no_self_test_spec = do {
   global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+  alloc_p384_felem_methods_globals;
   (digest, digest_ptr) <- ptr_to_fresh_readonly "digest" (llvm_array SHA_DIGEST_LENGTH i8);
 
   sig_ptr <- crucible_alloc_readonly (llvm_struct ecdsa_sig_st);

diff --git a/SAW/proof/ECDSA/evp-function-specs.saw b/SAW/proof/ECDSA/evp-function-specs.saw
@@ -96,6 +96,7 @@ let EVP_DigestSignVerifyUpdate_spec is_sign = do {
 
 let EVP_DigestSignFinal_spec = do {
   global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+  alloc_p384_felem_methods_globals;
 
   ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_ctx_st");
 
@@ -145,6 +146,7 @@ let EVP_DigestSignFinal_spec = do {
 
 let EVP_DigestVerifyFinal_spec = do {
   global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+  alloc_p384_felem_methods_globals;
 
   ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_ctx_st");
 
@@ -184,6 +186,7 @@ let EVP_DigestVerifyFinal_spec = do {
 
 let EVP_DigestSign_spec = do {
   global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+  alloc_p384_felem_methods_globals;
 
   ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_ctx_st");
 
@@ -235,6 +238,7 @@ let EVP_DigestSign_spec = do {
 
 let EVP_DigestVerify_spec = do {
   global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
+  alloc_p384_felem_methods_globals;
 
   ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_ctx_st");