Skip to content

Panic freemdom for AVX2 and NEON SHA-3 backends #1238

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
parrot7483 wants to merge 5 commits into
base: main
Choose a base branch
from
Open

Panic freemdom for AVX2 and NEON SHA-3 backends #1238

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
70f73b9
Add post condition for mm256_storeu_si256_u8
parrot7483 Sep 25, 2025
9b52d62
Add post condition for _vst1q_bytes_u64
parrot7483 Nov 11, 2025
4042305
Add full type check for SHA3 NEON
parrot7483 Mar 9, 2026
6c0096c
Add full type check for SHA3 AVX2
parrot7483 Mar 9, 2026
e908bc1
Extract and type-check with SIMD features
parrot7483 Mar 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 14 additions & 14 deletions .github/workflows/sha3-hax.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ jobs:
get-hax-ref:
uses: ./.github/workflows/get-hax-ref.yml

extract-portable:
extract:
if: ${{ github.event_name != 'merge_group' }}
runs-on: ubuntu-latest
needs:
Expand All @@ -45,23 +45,23 @@ jobs:
hax_reference: ${{ github.event.inputs.hax_ref || needs.get-hax-ref.outputs.hax_ref }}
fstar: v2025.12.15

- name: 🏃 Extract SHA3 crate (portable)
- name: 🏃 Extract SHA3 crate
working-directory: crates/algorithms/sha3
run: ./hax.sh extract

- name: ↑ Upload F* extraction (standard)
uses: actions/upload-artifact@v7
with:
name: fstar-extractions-portable
name: fstar-extractions
path: "**/proofs/fstar"
include-hidden-files: true
if-no-files-found: error

lax-portable:
lax:
runs-on: ubuntu-latest
needs:
- get-hax-ref
- extract-portable
- extract
if: ${{ github.event_name != 'merge_group' }}
steps:
- uses: actions/checkout@v6
Expand All @@ -72,18 +72,18 @@ jobs:

- uses: actions/download-artifact@v8
with:
name: fstar-extractions-portable
name: fstar-extractions
path: .

- name: 🏃 Lax SHA3 crate (portable)
- name: 🏃 Lax SHA3 crate
working-directory: crates/algorithms/sha3
run: ./hax.sh prove --admit

type-check-portable:
type-check:
runs-on: ubuntu-latest
needs:
- get-hax-ref
- extract-portable
- extract
if: ${{ github.event_name != 'merge_group' }}
steps:
- uses: actions/checkout@v6
Expand All @@ -94,16 +94,16 @@ jobs:

- uses: actions/download-artifact@v8
with:
name: fstar-extractions-portable
name: fstar-extractions
path: .

- name: 🏃 Full type check SHA3 crate (portable)
- name: 🏃 Full type check SHA3 crate
working-directory: crates/algorithms/sha3
run: ./hax.sh prove

sha3-extract-hax-status:
if: ${{ always() }}
needs: [get-hax-ref, extract-portable]
needs: [get-hax-ref, extract]
runs-on: ubuntu-latest
steps:
- name: Successful
Expand All @@ -113,9 +113,9 @@ jobs:
if: ${{ (contains(needs.*.result, 'failure')) }}
run: exit 1

sha3-type-check-portable-hax-status:
sha3-type-check-hax-status:
if: ${{ always() }}
needs: [get-hax-ref, lax-portable, type-check-portable]
needs: [get-hax-ref, lax, type-check]
runs-on: ubuntu-latest
steps:
- name: Successful
Expand Down
6 changes: 2 additions & 4 deletions crates/algorithms/sha3/hax.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ function extract_all() {
rename_core_models_files crates/utils/core-models

extract crates/utils/intrinsics \
-C --features simd128,simd256 ";" \
into -i "-core_models::**" \
fstar --z3rlimit 80 --interfaces "+**"

Expand All @@ -18,11 +19,8 @@ function extract_all() {
fstar --z3rlimit 80

extract crates/algorithms/sha3 \
-C --features simd128,simd256 ";" \
into -i "+**" \
-i "-**::avx2::**" \
-i "-**::neon::**" \
-i "-**::simd128::**" \
-i "-**::simd256::**" \
fstar --z3rlimit 80
}

Expand Down
90 changes: 90 additions & 0 deletions crates/algorithms/sha3/src/avx2.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,20 @@ pub mod x4 {

/// Perform 4 SHAKE256 operations in parallel
#[allow(clippy::too_many_arguments)]
#[hax_lib::requires(
input0.len() == input1.len() &&
input0.len() == input2.len() &&
input0.len() == input3.len() &&
out0.len() == out1.len() &&
out0.len() == out2.len() &&
out0.len() == out3.len()
)]
#[hax_lib::ensures(|_|
future(out0).len() == out0.len() &&
future(out1).len() == out1.len() &&
future(out2).len() == out2.len() &&
future(out3).len() == out3.len()
)]
#[inline(always)]
pub fn shake256(
input0: &[u8],
Expand All @@ -20,10 +34,14 @@ pub mod x4 {

/// An incremental API to perform 4 operations in parallel
pub mod incremental {
#[cfg(hax)]
use hax_lib::ToInt;

use crate::generic_keccak::KeccakState as GenericState;
use libcrux_intrinsics::avx2::*;

/// The Keccak state for the incremental API.
#[hax_lib::fstar::before("noeq")]
pub struct KeccakState {
state: GenericState<4, Vec256>,
}
Expand All @@ -37,6 +55,12 @@ pub mod x4 {
}

/// Absorb
#[hax_lib::requires(
data0.len().to_int() < hax_lib::int!(168) &&
data0.len() == data1.len() &&
data0.len() == data2.len() &&
data0.len() == data3.len()
)]
#[inline(always)]
pub fn shake128_absorb_final(
s: &mut KeccakState,
Expand All @@ -51,6 +75,12 @@ pub mod x4 {

/// Absorb
#[inline(always)]
#[hax_lib::requires(
data0.len().to_int() < hax_lib::int!(136) &&
data0.len() == data1.len() &&
data0.len() == data2.len() &&
data0.len() == data3.len()
)]
pub fn shake256_absorb_final(
s: &mut KeccakState,
data0: &[u8],
Expand All @@ -64,6 +94,18 @@ pub mod x4 {

/// Squeeze block
#[inline(always)]
#[hax_lib::requires(
out0.len().to_int() >= hax_lib::int!(136) &&
out0.len() == out1.len() &&
out0.len() == out2.len() &&
out0.len() == out3.len()
)]
#[hax_lib::ensures(|_|
future(out0).len() == out0.len() &&
future(out1).len() == out1.len() &&
future(out2).len() == out2.len() &&
future(out3).len() == out3.len()
)]
pub fn shake256_squeeze_first_block(
s: &mut KeccakState,
out0: &mut [u8],
Expand All @@ -76,6 +118,18 @@ pub mod x4 {

/// Squeeze next block
#[inline(always)]
#[hax_lib::requires(
out0.len().to_int() >= hax_lib::int!(136) &&
out0.len() == out1.len() &&
out0.len() == out2.len() &&
out0.len() == out3.len()
)]
#[hax_lib::ensures(|_|
future(out0).len() == out0.len() &&
future(out1).len() == out1.len() &&
future(out2).len() == out2.len() &&
future(out3).len() == out3.len()
)]
pub fn shake256_squeeze_next_block(
s: &mut KeccakState,
out0: &mut [u8],
Expand All @@ -88,6 +142,18 @@ pub mod x4 {

/// Squeeze three blocks
#[inline(always)]
#[hax_lib::requires(
out0.len().to_int() >= hax_lib::int!(504) && // 3 * 168 = 504
out0.len() == out1.len() &&
out0.len() == out2.len() &&
out0.len() == out3.len()
)]
#[hax_lib::ensures(|_|
future(out0).len() == out0.len() &&
future(out1).len() == out1.len() &&
future(out2).len() == out2.len() &&
future(out3).len() == out3.len()
)]
pub fn shake128_squeeze_first_three_blocks(
s: &mut KeccakState,
out0: &mut [u8],
Expand All @@ -101,6 +167,18 @@ pub mod x4 {

/// Squeeze five blocks
#[inline(always)]
#[hax_lib::requires(
out0.len().to_int() >= hax_lib::int!(840) && // 5 * 168 = 840
out0.len() == out1.len() &&
out0.len() == out2.len() &&
out0.len() == out3.len()
)]
#[hax_lib::ensures(|_|
future(out0).len() == out0.len() &&
future(out1).len() == out1.len() &&
future(out2).len() == out2.len() &&
future(out3).len() == out3.len()
)]
pub fn shake128_squeeze_first_five_blocks(
s: &mut KeccakState,
out0: &mut [u8],
Expand All @@ -114,6 +192,18 @@ pub mod x4 {

/// Squeeze another block
#[inline(always)]
#[hax_lib::requires(
out0.len().to_int() >= hax_lib::int!(168) &&
out0.len() == out1.len() &&
out0.len() == out2.len() &&
out0.len() == out3.len()
)]
#[hax_lib::ensures(|_|
future(out0).len() == out0.len() &&
future(out1).len() == out1.len() &&
future(out2).len() == out2.len() &&
future(out3).len() == out3.len()
)]
pub fn shake128_squeeze_next_block(
s: &mut KeccakState,
out0: &mut [u8],
Expand Down
Loading
Loading