From 9436a9c6b6d8c4efcf3ab59636a389c38f9ad379 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 30 Nov 2023 20:46:42 +0000 Subject: [PATCH] Refactor SHA2 defines and machine capability setup --- .../SHA512/SHA384-aarch64-neoverse-n1.saw | 34 ++----------------- .../SHA512/SHA384-aarch64-neoverse-v1.saw | 34 ++----------------- .../{SHA512-384.saw => SHA384-defines.saw} | 0 .../SHA512/SHA384-x86_64-sandybridge+.saw | 34 ++----------------- .../SHA512/SHA512-aarch64-neoverse-n1.saw | 34 ++----------------- .../SHA512/SHA512-aarch64-neoverse-v1.saw | 33 ++---------------- .../{SHA512-512.saw => SHA512-defines.saw} | 0 .../SHA512/SHA512-x86_64-sandybridge+.saw | 34 ++----------------- SAW/proof/SHA512/aarch64-neoverse-n1.saw | 15 ++++++++ SAW/proof/SHA512/aarch64-neoverse-v1.saw | 15 ++++++++ .../verify-SHA384-aarch64-neoverse-n1.saw | 3 +- .../verify-SHA384-aarch64-neoverse-v1.saw | 3 +- SAW/proof/SHA512/verify-SHA384-x86.saw | 3 +- .../verify-SHA512-aarch64-neoverse-n1.saw | 3 +- .../verify-SHA512-aarch64-neoverse-v1.saw | 3 +- SAW/proof/SHA512/verify-SHA512-x86.saw | 3 +- SAW/proof/SHA512/x86_64-sandybridge+.saw | 15 ++++++++ 17 files changed, 69 insertions(+), 197 deletions(-) rename SAW/proof/SHA512/{SHA512-384.saw => SHA384-defines.saw} (100%) rename SAW/proof/SHA512/{SHA512-512.saw => SHA512-defines.saw} (100%) create mode 100644 SAW/proof/SHA512/aarch64-neoverse-n1.saw create mode 100644 SAW/proof/SHA512/aarch64-neoverse-v1.saw create mode 100644 SAW/proof/SHA512/x86_64-sandybridge+.saw diff --git a/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw b/SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw index 17b91cfb..894944a7 100644 --- 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 index f9fb631f..c5492b24 100644 --- 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 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 index 9be9fde3..4aecbada 100644 --- 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 index a8130ecb..95acc2f8 100644 --- 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 index 2cd8b307..696d161c 100644 --- 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 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 index ad950540..131be360 100644 --- 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 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";