Refactor SHA2 defines and machine capability setup

awslabs · Nov 30, 2023 · 9436a9c · 9436a9c
1 parent 0316cd9
commit 9436a9c
Show file tree

Hide file tree

Showing 17 changed files with 69 additions and 197 deletions.
diff --git a/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw
@@ -3,35 +3,5 @@
  * SPDX-License-Identifier: Apache-2.0
 */
 
-
-/*
- * SHA384 defines
- */
-
-// Identifier for type of env_md_st struct.  SHA384 has NID 673
-let NID = 673;
-
-// Length of message digest in bytes
-let SHA_DIGEST_LENGTH = 48;
-
-// Names of init, update, and final functions in C code.
-let SHA_INIT = "sha384_init";
-let SHA_UPDATE = "sha384_update";
-let SHA_FINAL = "sha384_final";
-
-// Name of EVP storage global
-let EVP_SHA_STORAGE = "EVP_sha384_storage";
-
-// Name of EVP init function in C code.
-let EVP_SHA_INIT = "EVP_sha384_init";
-
-/*
-* Machine capabilities and architecture
-*/
-
-// Name of the OPENSSL machine cap variable
-let cap_sym = "OPENSSL_armcap_P";
-// Set machine cap value
-let {{ machine_cap = 0x00000000 : [32] }};
-// Set the architecture variable for controlling proof settings
-let ARCH = "AARCH64";
+include "SHA384-defines.saw";
+include "aarch64-neoverse-n1.saw";
diff --git a/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw
@@ -3,35 +3,5 @@
  * SPDX-License-Identifier: Apache-2.0
 */
 
-
-/*
- * SHA384 defines
- */
-
-// Identifier for type of env_md_st struct.  SHA384 has NID 673
-let NID = 673;
-
-// Length of message digest in bytes
-let SHA_DIGEST_LENGTH = 48;
-
-// Names of init, update, and final functions in C code.
-let SHA_INIT = "sha384_init";
-let SHA_UPDATE = "sha384_update";
-let SHA_FINAL = "sha384_final";
-
-// Name of EVP storage global
-let EVP_SHA_STORAGE = "EVP_sha384_storage";
-
-// Name of EVP init function in C code.
-let EVP_SHA_INIT = "EVP_sha384_init";
-
-/*
-* Machine capabilities and architecture
-*/
-
-// Name of the OPENSSL machine cap variable
-let cap_sym = "OPENSSL_armcap_P";
-// Set machine cap value
-let {{ machine_cap = 0xffffffff : [32] }};
-// Set the architecture variable for controlling proof settings
-let ARCH = "AARCH64";
+include "SHA384-defines.saw";
+include "aarch64-neoverse-v1.saw";
diff --git a/SAW/proof/SHA512/SHA512-384.saw → SAW/proof/SHA512/SHA384-defines.saw b/SAW/proof/SHA512/SHA512-384.saw → SAW/proof/SHA512/SHA384-defines.saw
diff --git a/SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw b/SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw
@@ -3,35 +3,5 @@
  * SPDX-License-Identifier: Apache-2.0
 */
 
-
-/*
- * SHA384 defines
- */
-
-// Identifier for type of env_md_st struct.  SHA384 has NID 673
-let NID = 673;
-
-// Length of message digest in bytes
-let SHA_DIGEST_LENGTH = 48;
-
-// Names of init, update, and final functions in C code.
-let SHA_INIT = "sha384_init";
-let SHA_UPDATE = "sha384_update";
-let SHA_FINAL = "sha384_final";
-
-// Name of EVP storage global
-let EVP_SHA_STORAGE = "EVP_sha384_storage";
-
-// Name of EVP init function in C code.
-let EVP_SHA_INIT = "EVP_sha384_init";
-
-/*
-* Machine capabilities and architecture
-*/
-
-// Name of the OPENSSL machine cap variable
-let cap_sym = "OPENSSL_ia32cap_P";
-// Set machine cap value
-let {{ machine_cap = [0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff] : [4][32] }};
-// Set the architecture variable for controlling proof settings
-let ARCH = "X86_64";
+include "SHA384-defines.saw";
+include "x86_64-sandybridge+.saw";
diff --git a/SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw
@@ -3,35 +3,5 @@
  * SPDX-License-Identifier: Apache-2.0
 */
 
-
-/*
- * SHA512 defines
- */
-
-// Identifier for type of env_md_st struct.  SHA512 has NID 674
-let NID = 674;
-
-// Length of message digest in bytes
-let SHA_DIGEST_LENGTH = 64;
-
-// Names of init, update, and final functions in C code.
-let SHA_INIT = "sha512_init";
-let SHA_UPDATE = "sha512_update";
-let SHA_FINAL = "sha512_final";
-
-// Name of EVP storage global
-let EVP_SHA_STORAGE = "EVP_sha512_storage";
-
-// Name of EVP init function in C code.
-let EVP_SHA_INIT = "EVP_sha512_init";
-
-/*
-* Machine capabilities and architecture
-*/
-
-// Name of the OPENSSL machine cap variable
-let cap_sym = "OPENSSL_armcap_P";
-// Set machine cap value
-let {{ machine_cap = 0x00000000 : [32] }};
-// Set the architecture variable for controlling proof settings
-let ARCH = "AARCH64";
+include "SHA512-defines.saw";
+include "aarch64-neoverse-n1.saw";
diff --git a/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw
@@ -4,34 +4,5 @@
 */
 
 
-/*
- * SHA512 defines
- */
-
-// Identifier for type of env_md_st struct.  SHA512 has NID 674
-let NID = 674;
-
-// Length of message digest in bytes
-let SHA_DIGEST_LENGTH = 64;
-
-// Names of init, update, and final functions in C code.
-let SHA_INIT = "sha512_init";
-let SHA_UPDATE = "sha512_update";
-let SHA_FINAL = "sha512_final";
-
-// Name of EVP storage global
-let EVP_SHA_STORAGE = "EVP_sha512_storage";
-
-// Name of EVP init function in C code.
-let EVP_SHA_INIT = "EVP_sha512_init";
-
-/*
-* Machine capabilities and architecture
-*/
-
-// Name of the OPENSSL machine cap variable
-let cap_sym = "OPENSSL_armcap_P";
-// Set machine cap value
-let {{ machine_cap = 0xffffffff : [32] }};
-// Set the architecture variable for controlling proof settings
-let ARCH = "AARCH64";
+include "SHA512-defines.saw";
+include "aarch64-neoverse-v1.saw";
diff --git a/SAW/proof/SHA512/SHA512-512.saw → SAW/proof/SHA512/SHA512-defines.saw b/SAW/proof/SHA512/SHA512-512.saw → SAW/proof/SHA512/SHA512-defines.saw
diff --git a/SAW/proof/SHA512/SHA512-x86_64-sandybridge+.saw b/SAW/proof/SHA512/SHA512-x86_64-sandybridge+.saw
@@ -3,35 +3,5 @@
  * SPDX-License-Identifier: Apache-2.0
 */
 
-
-/*
- * SHA512 defines
- */
-
-// Identifier for type of env_md_st struct.  SHA512 has NID 674
-let NID = 674;
-
-// Length of message digest in bytes
-let SHA_DIGEST_LENGTH = 64;
-
-// Names of init, update, and final functions in C code.
-let SHA_INIT = "sha512_init";
-let SHA_UPDATE = "sha512_update";
-let SHA_FINAL = "sha512_final";
-
-// Name of EVP storage global
-let EVP_SHA_STORAGE = "EVP_sha512_storage";
-
-// Name of EVP init function in C code.
-let EVP_SHA_INIT = "EVP_sha512_init";
-
-/*
-* Machine capabilities and architecture
-*/
-
-// Name of the OPENSSL machine cap variable
-let cap_sym = "OPENSSL_ia32cap_P";
-// Set machine cap value
-let {{ machine_cap = [0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff] : [4][32] }};
-// Set the architecture variable for controlling proof settings
-let ARCH = "X86_64";
+include "SHA512-defines.saw";
+include "x86_64-sandybridge+.saw";
diff --git a/SAW/proof/SHA512/aarch64-neoverse-n1.saw b/SAW/proof/SHA512/aarch64-neoverse-n1.saw
@@ -0,0 +1,15 @@
+/* 
+* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+* SPDX-License-Identifier: Apache-2.0
+*/
+
+/*
+* Machine capabilities and architecture
+*/
+
+// Name of the OPENSSL machine cap variable
+let cap_sym = "OPENSSL_armcap_P";
+// Set machine cap value
+let {{ machine_cap = 0x00000000 : [32] }};
+// Set the architecture variable for controlling proof settings
+let ARCH = "AARCH64";
diff --git a/SAW/proof/SHA512/aarch64-neoverse-v1.saw b/SAW/proof/SHA512/aarch64-neoverse-v1.saw
@@ -0,0 +1,15 @@
+/* 
+* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+* SPDX-License-Identifier: Apache-2.0
+*/
+
+/*
+* Machine capabilities and architecture
+*/
+
+// Name of the OPENSSL machine cap variable
+let cap_sym = "OPENSSL_armcap_P";
+// Set machine cap value
+let {{ machine_cap = 0xffffffff : [32] }};
+// Set the architecture variable for controlling proof settings
+let ARCH = "AARCH64";
diff --git a/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw
@@ -5,5 +5,6 @@
 
 import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry";
 
-include "SHA384-aarch64-neoverse-n1.saw";
+include "SHA384-defines.saw";
+include "aarch64-neoverse-n1.saw";
 include "SHA512.saw";
diff --git a/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw
@@ -5,5 +5,6 @@
 
 import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry";
 
-include "SHA384-aarch64-neoverse-v1.saw";
+include "SHA384-defines.saw";
+include "aarch64-neoverse-v1.saw";
 include "SHA512.saw";
diff --git a/SAW/proof/SHA512/verify-SHA384-x86.saw b/SAW/proof/SHA512/verify-SHA384-x86.saw
@@ -5,5 +5,6 @@
 
 import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA384.cry";
 
-include "SHA384-x86_64-sandybridge+.saw";
+include "SHA384-defines";
+include "x86_64-sandybridge+.saw";
 include "SHA512.saw";
diff --git a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw
@@ -5,5 +5,6 @@
 
 import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry";
 
-include "SHA512-aarch64-neoverse-n1.saw";
+include "SHA512-defines.saw";
+include "aarch64-neoverse-n1.saw";
 include "SHA512.saw";
diff --git a/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw
@@ -5,5 +5,6 @@
 
 import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry";
 
-include "SHA512-aarch64-neoverse-v1.saw";
+include "SHA512-defines.saw";
+include "aarch64-neoverse-v1.saw";
 include "SHA512.saw";
diff --git a/SAW/proof/SHA512/verify-SHA512-x86.saw b/SAW/proof/SHA512/verify-SHA512-x86.saw
@@ -5,5 +5,6 @@
 
 import "../../../cryptol-specs/Primitive/Keyless/Hash/SHA512.cry";
 
-include "SHA512-x86_64-sandybridge+.saw";
+include "SHA512-defines";
+include "x86_64-sandybridge+.saw";
 include "SHA512.saw";
diff --git a/SAW/proof/SHA512/x86_64-sandybridge+.saw b/SAW/proof/SHA512/x86_64-sandybridge+.saw
@@ -0,0 +1,15 @@
+/* 
+* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+* SPDX-License-Identifier: Apache-2.0
+*/
+
+/*
+* Machine capabilities and architecture
+*/
+
+// Name of the OPENSSL machine cap variable
+let cap_sym = "OPENSSL_ia32cap_P";
+// Set machine cap value
+let {{ machine_cap = [0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff] : [4][32] }};
+// Set the architecture variable for controlling proof settings
+let ARCH = "X86_64";