diff --git a/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw
deleted file mode 100644
index 17b91cfb..00000000
--- a/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw
+++ /dev/null
@@ -1,37 +0,0 @@
-/* 
- * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
- * 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";
diff --git a/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw
deleted file mode 100644
index f9fb631f..00000000
--- a/SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw
+++ /dev/null
@@ -1,37 +0,0 @@
-/* 
- * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
- * 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";
diff --git a/SAW/proof/SHA512/SHA512-384.saw b/SAW/proof/SHA512/SHA384-defines.saw
similarity index 100%
rename from SAW/proof/SHA512/SHA512-384.saw
rename to 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
deleted file mode 100644
index 9be9fde3..00000000
--- a/SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw
+++ /dev/null
@@ -1,37 +0,0 @@
-/* 
- * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
- * 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";
diff --git a/SAW/proof/SHA512/SHA512-384-common.saw b/SAW/proof/SHA512/SHA512-384-common.saw
index b8956f73..7396dd3c 100644
--- a/SAW/proof/SHA512/SHA512-384-common.saw
+++ b/SAW/proof/SHA512/SHA512-384-common.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-common.saw";
diff --git a/SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw
deleted file mode 100644
index a8130ecb..00000000
--- a/SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw
+++ /dev/null
@@ -1,37 +0,0 @@
-/* 
- * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
- * 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";
diff --git a/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw b/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw
deleted file mode 100644
index 2cd8b307..00000000
--- a/SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw
+++ /dev/null
@@ -1,37 +0,0 @@
-/* 
- * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
- * 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 = 0xffffffff : [32] }};
-// Set the architecture variable for controlling proof settings
-let ARCH = "AARCH64";
diff --git a/SAW/proof/SHA512/SHA512-512.saw b/SAW/proof/SHA512/SHA512-defines.saw
similarity index 100%
rename from SAW/proof/SHA512/SHA512-512.saw
rename to 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
deleted file mode 100644
index ad950540..00000000
--- a/SAW/proof/SHA512/SHA512-x86_64-sandybridge+.saw
+++ /dev/null
@@ -1,37 +0,0 @@
-/* 
- * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
- * 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";
diff --git a/SAW/proof/SHA512/aarch64-neoverse-n1.saw b/SAW/proof/SHA512/aarch64-neoverse-n1.saw
new file mode 100644
index 00000000..10e7fcea
--- /dev/null
+++ 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
new file mode 100644
index 00000000..b0b3d1b6
--- /dev/null
+++ 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
index fc01775f..efe7f171 100644
--- 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
index 70fc9cf9..a5660e87 100644
--- 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
index ace99851..3449bf98 100644
--- 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
index 470f987a..d3d42d29 100644
--- 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
index 6cb479bd..35dc73f1 100644
--- 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
index 08e2eecd..e92165e5 100644
--- 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
new file mode 100644
index 00000000..b702c05a
--- /dev/null
+++ 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";