Skip to content

Commit

Permalink
Refactor SHA2 defines and machine capability setup
Browse files Browse the repository at this point in the history
  • Loading branch information
pennyannn committed Nov 30, 2023
1 parent 0316cd9 commit dd0325f
Show file tree
Hide file tree
Showing 18 changed files with 59 additions and 229 deletions.
37 changes: 0 additions & 37 deletions SAW/proof/SHA512/SHA384-aarch64-neoverse-n1.saw

This file was deleted.

37 changes: 0 additions & 37 deletions SAW/proof/SHA512/SHA384-aarch64-neoverse-v1.saw

This file was deleted.

File renamed without changes.
37 changes: 0 additions & 37 deletions SAW/proof/SHA512/SHA384-x86_64-sandybridge+.saw

This file was deleted.

3 changes: 2 additions & 1 deletion SAW/proof/SHA512/SHA512-384-common.saw
Original file line number Diff line number Diff line change
Expand Up @@ -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";
37 changes: 0 additions & 37 deletions SAW/proof/SHA512/SHA512-aarch64-neoverse-n1.saw

This file was deleted.

37 changes: 0 additions & 37 deletions SAW/proof/SHA512/SHA512-aarch64-neoverse-v1.saw

This file was deleted.

File renamed without changes.
37 changes: 0 additions & 37 deletions SAW/proof/SHA512/SHA512-x86_64-sandybridge+.saw

This file was deleted.

15 changes: 15 additions & 0 deletions SAW/proof/SHA512/aarch64-neoverse-n1.saw
Original file line number Diff line number Diff line change
@@ -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";
15 changes: 15 additions & 0 deletions SAW/proof/SHA512/aarch64-neoverse-v1.saw
Original file line number Diff line number Diff line change
@@ -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";
3 changes: 2 additions & 1 deletion SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-n1.saw
Original file line number Diff line number Diff line change
Expand Up @@ -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";
3 changes: 2 additions & 1 deletion SAW/proof/SHA512/verify-SHA384-aarch64-neoverse-v1.saw
Original file line number Diff line number Diff line change
Expand Up @@ -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";
3 changes: 2 additions & 1 deletion SAW/proof/SHA512/verify-SHA384-x86.saw
Original file line number Diff line number Diff line change
Expand Up @@ -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";
3 changes: 2 additions & 1 deletion SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-n1.saw
Original file line number Diff line number Diff line change
Expand Up @@ -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";
3 changes: 2 additions & 1 deletion SAW/proof/SHA512/verify-SHA512-aarch64-neoverse-v1.saw
Original file line number Diff line number Diff line change
Expand Up @@ -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";
3 changes: 2 additions & 1 deletion SAW/proof/SHA512/verify-SHA512-x86.saw
Original file line number Diff line number Diff line change
Expand Up @@ -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";
15 changes: 15 additions & 0 deletions SAW/proof/SHA512/x86_64-sandybridge+.saw
Original file line number Diff line number Diff line change
@@ -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";

0 comments on commit dd0325f

Please sign in to comment.