From 70f73b945dd25e04fd52305b52073cceca50b7f6 Mon Sep 17 00:00:00 2001 From: Parrot7483 <47054801+Parrot7483@users.noreply.github.com> Date: Thu, 25 Sep 2025 13:29:39 +0200 Subject: [PATCH 1/5] Add post condition for mm256_storeu_si256_u8 --- crates/utils/intrinsics/src/avx2.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/crates/utils/intrinsics/src/avx2.rs b/crates/utils/intrinsics/src/avx2.rs index bdc9df5f54..4a1f1f8563 100644 --- a/crates/utils/intrinsics/src/avx2.rs +++ b/crates/utils/intrinsics/src/avx2.rs @@ -13,6 +13,9 @@ pub type Vec128 = __m128i; pub type Vec256Float = __m256; #[hax_lib::opaque] +#[hax_lib::ensures(|_| + future(output).len() == output.len() +)] #[inline(always)] pub fn mm256_storeu_si256_u8(output: &mut [u8], vector: Vec256) { // Note: in this module the `debug_assert_eq!` are essentially sanity From 9b52d6254aca7a3ed165328b02ff73dfe2b62c0d Mon Sep 17 00:00:00 2001 From: Parrot7483 <47054801+Parrot7483@users.noreply.github.com> Date: Tue, 11 Nov 2025 18:09:45 +0100 Subject: [PATCH 2/5] Add post condition for _vst1q_bytes_u64 --- crates/utils/intrinsics/src/arm64_extract.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/crates/utils/intrinsics/src/arm64_extract.rs b/crates/utils/intrinsics/src/arm64_extract.rs index 188e501230..8020cbdae8 100644 --- a/crates/utils/intrinsics/src/arm64_extract.rs +++ b/crates/utils/intrinsics/src/arm64_extract.rs @@ -68,6 +68,7 @@ pub fn _vst1q_u64(out: &mut [u64], v: _uint64x2_t) { } #[inline(always)] +#[hax_lib::ensures(|_| future(out).len() == out.len())] pub fn _vst1q_bytes_u64(out: &mut [_int16x8_t], v: _uint64x2_t) { unimplemented!() } From 4042305f74581b69723ff7c33139470398d917a9 Mon Sep 17 00:00:00 2001 From: Parrot7483 <47054801+Parrot7483@users.noreply.github.com> Date: Mon, 9 Mar 2026 18:05:53 +0100 Subject: [PATCH 3/5] Add full type check for SHA3 NEON --- .../sha3/src/generic_keccak/simd128.rs | 135 +++++++++++++----- crates/algorithms/sha3/src/neon.rs | 112 ++++++++------- crates/algorithms/sha3/src/simd/arm64.rs | 109 ++++++++++++-- crates/algorithms/sha3/src/traits.rs | 71 +++++++++ 4 files changed, 326 insertions(+), 101 deletions(-) diff --git a/crates/algorithms/sha3/src/generic_keccak/simd128.rs b/crates/algorithms/sha3/src/generic_keccak/simd128.rs index 8cdcd40590..9827aa2a0b 100644 --- a/crates/algorithms/sha3/src/generic_keccak/simd128.rs +++ b/crates/algorithms/sha3/src/generic_keccak/simd128.rs @@ -2,46 +2,21 @@ use super::*; use libcrux_intrinsics::arm64::_uint64x2_t; -#[inline] -pub(crate) fn keccak2( - data: &[&[u8]; 2], - out0: &mut [u8], - out1: &mut [u8], -) { - #[cfg(not(eurydice))] - debug_assert!(out0.len() == out1.len()); - #[cfg(not(eurydice))] - debug_assert!(data[0].len() == data[1].len()); - - let mut s = KeccakState::<2, _uint64x2_t>::new(); - let data_len = data[0].len(); - for i in 0..data_len / RATE { - s.absorb_block::(data, i * RATE); - } - let rem = data_len % RATE; - s.absorb_final::(data, data_len - rem, rem); - - let outlen = out0.len(); - let blocks = outlen / RATE; - let last = outlen - (outlen % RATE); - - if blocks == 0 { - s.squeeze2::(out0, out1, 0, outlen); - } else { - s.squeeze2::(out0, out1, 0, RATE); - for i in 1..blocks { - s.keccakf1600(); - s.squeeze2::(out0, out1, i * RATE, RATE); - } - if last < outlen { - s.keccakf1600(); - s.squeeze2::(out0, out1, last, outlen - last); - } - } -} +#[cfg(hax)] +use crate::proof_utils::{lemma_mul_succ_le, valid_rate}; +#[hax_lib::attributes] impl KeccakState<2, _uint64x2_t> { #[inline(always)] + #[hax_lib::requires( + valid_rate(RATE) && + start.to_int() + RATE.to_int() <= out0.len().to_int() && + out0.len() == out1.len() + )] + #[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() + )] pub(crate) fn squeeze_next_block( &mut self, out0: &mut [u8], @@ -57,11 +32,29 @@ impl KeccakState<2, _uint64x2_t> { /// This function MUST NOT be called after any of the other `squeeze_*` /// functions have been called, since that would result in a duplicate output /// block. + #[hax_lib::requires( + valid_rate(RATE) && + RATE <= out0.len() && + out0.len() == out1.len() + )] + #[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() + )] pub(crate) fn squeeze_first_block(&self, out0: &mut [u8], out1: &mut [u8]) { self.squeeze2::(out0, out1, 0, RATE); } #[inline(always)] + #[hax_lib::requires( + valid_rate(RATE) && + 3 * RATE <= out0.len() && + out0.len() == out1.len() + )] + #[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() + )] pub(crate) fn squeeze_first_three_blocks( &mut self, out0: &mut [u8], @@ -77,6 +70,15 @@ impl KeccakState<2, _uint64x2_t> { } #[inline(always)] + #[hax_lib::requires( + valid_rate(RATE) && + 5 * RATE <= out0.len() && + out0.len() == out1.len() + )] + #[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() + )] pub(crate) fn squeeze_first_five_blocks( &mut self, out0: &mut [u8], @@ -97,3 +99,62 @@ impl KeccakState<2, _uint64x2_t> { self.squeeze2::(out0, out1, 4 * RATE, RATE); } } + +#[hax_lib::requires( + valid_rate(RATE) && + data[0].len() == data[1].len() && + out0.len() == out1.len() +)] +#[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() +)] +#[hax_lib::fstar::options("--split_queries always --z3rlimit 300")] +#[inline] +pub(crate) fn keccak2( + data: &[&[u8]; 2], + out0: &mut [u8], + out1: &mut [u8], +) { + debug_assert!(data[0].len() == data[1].len()); + debug_assert!(out0.len() == out1.len()); + + // Initialize Keccak state + let mut s = KeccakState::<2, _uint64x2_t>::new(); + + // Absorb input + let input_len = data[0].len(); + let input_blocks = input_len / RATE; + let input_rem = input_len % RATE; + for i in 0..input_blocks { + #[cfg(hax)] + lemma_mul_succ_le(i, input_blocks, RATE); + + s.absorb_block::(data, i * RATE); + } + s.absorb_final::(data, input_len - input_rem, input_rem); + + // Squeeze output + let output_len = out0.len(); + let output_blocks = output_len / RATE; + let output_rem = output_len % RATE; + if output_blocks == 0 { + s.squeeze2::(out0, out1, 0, output_len); + } else { + s.squeeze2::(out0, out1, 0, RATE); + for i in 1..output_blocks { + hax_lib::loop_invariant!( + |_: usize| out0.len() == output_len && out0.len() == out1.len() + ); + #[cfg(hax)] + lemma_mul_succ_le(i, output_blocks, RATE); + + s.keccakf1600(); + s.squeeze2::(out0, out1, i * RATE, RATE); + } + if output_rem != 0 { + s.keccakf1600(); + s.squeeze2::(out0, out1, output_len - output_rem, output_rem); + } + } +} diff --git a/crates/algorithms/sha3/src/neon.rs b/crates/algorithms/sha3/src/neon.rs index 3d103bbf9a..0d6505ea01 100644 --- a/crates/algorithms/sha3/src/neon.rs +++ b/crates/algorithms/sha3/src/neon.rs @@ -1,61 +1,19 @@ -use crate::generic_keccak::simd128::keccak2; - -/// A SHA3 224 implementation. -#[allow(unused_variables)] -#[inline(always)] -pub fn sha224(digest: &mut [u8], data: &[u8]) { - let mut dummy = [0u8; 28]; - keccak2::<144, 0x06u8>(&[data, data], digest, &mut dummy); -} - -/// A SHA3 256 implementation. -#[allow(unused_variables)] -#[inline(always)] -pub fn sha256(digest: &mut [u8], data: &[u8]) { - let mut dummy = [0u8; 32]; - keccak2::<136, 0x06u8>(&[data, data], digest, &mut dummy); -} - -/// A SHA3 384 implementation. -#[allow(unused_variables)] -#[inline(always)] -pub fn sha384(digest: &mut [u8], data: &[u8]) { - let mut dummy = [0u8; 48]; - keccak2::<104, 0x06u8>(&[data, data], digest, &mut dummy); -} - -/// A SHA3 512 implementation. -#[allow(unused_variables)] -#[inline(always)] -pub fn sha512(digest: &mut [u8], data: &[u8]) { - let mut dummy = [0u8; 64]; - keccak2::<72, 0x06u8>(&[data, data], digest, &mut dummy); -} - -/// A SHAKE128 implementation. -#[allow(unused_variables)] -#[inline(always)] -pub fn shake128(digest: &mut [u8; LEN], data: &[u8]) { - let mut dummy = [0u8; LEN]; - keccak2::<168, 0x1fu8>(&[data, data], digest, &mut dummy); -} - -/// A SHAKE256 implementation. -#[allow(unused_variables)] -#[inline(always)] -pub fn shake256(digest: &mut [u8; LEN], data: &[u8]) { - let mut dummy = [0u8; LEN]; - keccak2::<136, 0x1fu8>(&[data, data], digest, &mut dummy); -} - /// Performing 2 operations in parallel pub mod x2 { - use super::*; + use crate::generic_keccak::simd128::keccak2; /// Run SHAKE256 on both inputs in parallel. /// /// Writes the two results into `out0` and `out1` #[allow(unused_variables)] + #[hax_lib::requires( + input0.len() == input1.len() && + out0.len() == out1.len() + )] + #[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() + )] #[inline(always)] pub fn shake256(input0: &[u8], input1: &[u8], out0: &mut [u8], out1: &mut [u8]) { keccak2::<136, 0x1fu8>(&[input0, input1], out0, out1); @@ -63,9 +21,13 @@ pub mod x2 { /// An incremental API to perform 2 operations in parallel pub mod incremental { + #[cfg(hax)] + use hax_lib::ToInt; + use crate::generic_keccak::KeccakState as GenericState; /// The Keccak state for the incremental API. + #[hax_lib::fstar::before("noeq")] pub struct KeccakState { state: GenericState<2, crate::simd::arm64::uint64x2_t>, } @@ -81,6 +43,10 @@ pub mod x2 { } /// Shake128 absorb `data0` and `data1` in the [`KeccakState`] `s`. + #[hax_lib::requires( + data0.len().to_int() < hax_lib::int!(168) && + data0.len() == data1.len() + )] #[inline(always)] pub fn shake128_absorb_final(s: &mut KeccakState, data0: &[u8], data1: &[u8]) { s.state @@ -89,6 +55,10 @@ pub mod x2 { /// Shake256 absorb `data0` and `data1` in the [`KeccakState`] `s`. #[inline(always)] + #[hax_lib::requires( + data0.len().to_int() < hax_lib::int!(136) && + data0.len() == data1.len() + )] pub fn shake256_absorb_final(s: &mut KeccakState, data0: &[u8], data1: &[u8]) { s.state .absorb_final::<136, 0x1fu8>(&[data0, data1], 0, data0.len()); @@ -97,6 +67,14 @@ pub mod x2 { /// Squeeze 2 times the first three blocks in parallel in the /// [`KeccakState`] and return the output in `out0` and `out1`. #[inline(always)] + #[hax_lib::requires( + out0.len().to_int() >= hax_lib::int!(504) && // 3 * 168 = 504 + out0.len() == out1.len() + )] + #[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() + )] pub fn shake128_squeeze_first_three_blocks( s: &mut KeccakState, out0: &mut [u8], @@ -107,6 +85,14 @@ pub mod x2 { /// Squeeze five blocks #[inline(always)] + #[hax_lib::requires( + out0.len().to_int() >= hax_lib::int!(840) && // 5 * 168 = 504 + out0.len() == out1.len() + )] + #[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() + )] pub fn shake128_squeeze_first_five_blocks( s: &mut KeccakState, out0: &mut [u8], @@ -117,12 +103,28 @@ pub mod x2 { /// Squeeze block #[inline(always)] + #[hax_lib::requires( + out0.len().to_int() >= hax_lib::int!(136) && + out0.len() == out1.len() + )] + #[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() + )] pub fn shake256_squeeze_first_block(s: &mut KeccakState, out0: &mut [u8], out1: &mut [u8]) { s.state.squeeze_first_block::<136>(out0, out1); } /// Squeeze next block #[inline(always)] + #[hax_lib::requires( + out0.len().to_int() >= hax_lib::int!(136) && + out0.len() == out1.len() + )] + #[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() + )] pub fn shake256_squeeze_next_block(s: &mut KeccakState, out0: &mut [u8], out1: &mut [u8]) { s.state.squeeze_next_block::<136>(out0, out1, 0); } @@ -130,6 +132,14 @@ pub mod x2 { /// Squeeze 2 times the next block in parallel in the /// [`KeccakState`] and return the output in `out0` and `out1`. #[inline(always)] + #[hax_lib::requires( + out0.len().to_int() >= hax_lib::int!(168) && + out0.len() == out1.len() + )] + #[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() + )] pub fn shake128_squeeze_next_block(s: &mut KeccakState, out0: &mut [u8], out1: &mut [u8]) { s.state.squeeze_next_block::<168>(out0, out1, 0) } diff --git a/crates/algorithms/sha3/src/simd/arm64.rs b/crates/algorithms/sha3/src/simd/arm64.rs index 852279b8e1..5bf6132037 100644 --- a/crates/algorithms/sha3/src/simd/arm64.rs +++ b/crates/algorithms/sha3/src/simd/arm64.rs @@ -2,6 +2,12 @@ use libcrux_intrinsics::arm64::*; use crate::{generic_keccak::KeccakState, traits::*}; +#[cfg(hax)] +use hax_lib::int::*; + +#[cfg(hax)] +use crate::proof_utils::valid_rate; + #[allow(non_camel_case_types)] pub type uint64x2_t = _uint64x2_t; @@ -22,6 +28,11 @@ fn _vrax1q_u64(a: uint64x2_t, b: uint64x2_t) -> uint64x2_t { } #[inline(always)] +#[hax_lib::requires( + LEFT.to_int() + RIGHT.to_int() == 64.to_int() && + RIGHT > 0 && + RIGHT < 64 +)] fn _vxarq_u64(a: uint64x2_t, b: uint64x2_t) -> uint64x2_t { libcrux_intrinsics::arm64::_vxarq_u64::(a, b) } @@ -38,6 +49,11 @@ fn _veorq_n_u64(a: uint64x2_t, c: u64) -> uint64x2_t { } #[inline(always)] +#[hax_lib::requires( + valid_rate(RATE) && + offset.to_int() + RATE.to_int() <= blocks[0].len().to_int() && + blocks[0].len() == blocks[1].len() +)] pub(crate) fn load_block( s: &mut [uint64x2_t; 25], blocks: &[&[u8]; 2], @@ -78,22 +94,28 @@ pub(crate) fn load_block( } #[inline(always)] +#[hax_lib::requires( + valid_rate(RATE) && + len < RATE && + start.to_int() + len.to_int() <= blocks[0].len().to_int() && + blocks[0].len() == blocks[1].len() +)] pub(crate) fn load_last( state: &mut [uint64x2_t; 25], blocks: &[&[u8]; 2], - offset: usize, + start: usize, len: usize, ) { #[cfg(not(eurydice))] - debug_assert!(offset + len <= blocks[0].len() && blocks[0].len() == blocks[1].len()); + debug_assert!(start + len <= blocks[0].len() && blocks[0].len() == blocks[1].len()); let mut buffer0 = [0u8; RATE]; - buffer0[0..len].copy_from_slice(&blocks[0][offset..offset + len]); + buffer0[0..len].copy_from_slice(&blocks[0][start..start + len]); buffer0[len] = DELIMITER; buffer0[RATE - 1] |= 0x80; let mut buffer1 = [0u8; RATE]; - buffer1[0..len].copy_from_slice(&blocks[1][offset..offset + len]); + buffer1[0..len].copy_from_slice(&blocks[1][start..start + len]); buffer1[len] = DELIMITER; buffer1[RATE - 1] |= 0x80; @@ -101,6 +123,16 @@ pub(crate) fn load_last( } #[inline(always)] +#[hax_lib::requires( + valid_rate(RATE) && + len <= RATE && + start.to_int() + len.to_int() <= out0.len().to_int() && + out0.len() == out1.len() +)] +#[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() +)] pub(crate) fn store_block( s: &[uint64x2_t; 25], out0: &mut [u8], @@ -110,40 +142,63 @@ pub(crate) fn store_block( ) { #[cfg(not(eurydice))] debug_assert!(len <= RATE && start + len <= out0.len() && out0.len() == out1.len()); - for i in 0..len / 16 { + + #[cfg(hax)] + let (out0_len, out1_len) = (out0.len(), out1.len()); + + let chunks = len / 16; + for i in 0..chunks { + #[cfg(hax)] + hax_lib::loop_invariant!(|_: usize| out0.len() == out0_len && out1.len() == out1_len); let i0 = (2 * i) / 5; let j0 = (2 * i) % 5; let i1 = (2 * i + 1) / 5; let j1 = (2 * i + 1) % 5; let v0 = _vtrn1q_u64(*get_ij(s, i0, j0), *get_ij(s, i1, j1)); let v1 = _vtrn2q_u64(*get_ij(s, i0, j0), *get_ij(s, i1, j1)); - _vst1q_bytes_u64(&mut out0[start + 16 * i..start + 16 * (i + 1)], v0); - _vst1q_bytes_u64(&mut out1[start + 16 * i..start + 16 * (i + 1)], v1); + + let base = start + 16 * i; + let limit = base + 16; + + _vst1q_bytes_u64(&mut out0[base..limit], v0); + _vst1q_bytes_u64(&mut out1[base..limit], v1); } + let remaining = len % 16; if remaining > 8 { let mut out0_tmp = [0u8; 16]; let mut out1_tmp = [0u8; 16]; - let i = 2 * (len / 16); + let i = 2 * (chunks); let i0 = i / 5; let j0 = i % 5; let i1 = (i + 1) / 5; let j1 = (i + 1) % 5; let v0 = _vtrn1q_u64(*get_ij(s, i0, j0), *get_ij(s, i1, j1)); let v1 = _vtrn2q_u64(*get_ij(s, i0, j0), *get_ij(s, i1, j1)); + _vst1q_bytes_u64(&mut out0_tmp, v0); _vst1q_bytes_u64(&mut out1_tmp, v1); - out0[start + len - remaining..start + len].copy_from_slice(&out0_tmp[0..remaining]); - out1[start + len - remaining..start + len].copy_from_slice(&out1_tmp[0..remaining]); + + let limit = start + len; + let base = limit - remaining; + + out0[base..limit].copy_from_slice(&out0_tmp[0..remaining]); + out1[base..limit].copy_from_slice(&out1_tmp[0..remaining]); } else if remaining > 0 { let mut out01 = [0u8; 16]; - let i = 2 * (len / 16); + let i = 2 * (chunks); + _vst1q_bytes_u64(&mut out01, *get_ij(s, i / 5, i % 5)); - out0[start + len - remaining..start + len].copy_from_slice(&out01[0..remaining]); - out1[start + len - remaining..start + len].copy_from_slice(&out01[8..8 + remaining]); + + let limit = start + len; + let base = limit - remaining; + + out0[base..limit].copy_from_slice(&out01[0..remaining]); + out1[base..limit].copy_from_slice(&out01[8..8 + remaining]); } } +#[hax_lib::attributes] impl KeccakItem<2> for uint64x2_t { #[inline(always)] fn zero() -> Self { @@ -158,6 +213,11 @@ impl KeccakItem<2> for uint64x2_t { _vrax1q_u64(a, b) } #[inline(always)] + #[hax_lib::requires( + LEFT.to_int() + RIGHT.to_int() == 64.to_int() && + RIGHT > 0 && + RIGHT < 64 + )] fn xor_and_rotate(a: Self, b: Self) -> Self { _vxarq_u64::(a, b) } @@ -175,11 +235,23 @@ impl KeccakItem<2> for uint64x2_t { } } +#[hax_lib::attributes] impl Absorb<2> for KeccakState<2, uint64x2_t> { + #[hax_lib::requires( + valid_rate(RATE) && + start.to_int() + RATE.to_int() <= input[0].len().to_int() && + input[0].len() == input[1].len() + )] fn load_block(&mut self, input: &[&[u8]; 2], start: usize) { load_block::(&mut self.st, input, start); } + #[hax_lib::requires( + valid_rate(RATE) && + len < RATE && + start.to_int() + len.to_int() <= input[0].len().to_int() && + input[0].len() == input[1].len() + )] fn load_last( &mut self, input: &[&[u8]; 2], @@ -190,7 +262,18 @@ impl Absorb<2> for KeccakState<2, uint64x2_t> { } } +#[hax_lib::attributes] impl Squeeze2 for KeccakState<2, uint64x2_t> { + #[hax_lib::requires( + valid_rate(RATE) && + len <= RATE && + start.to_int() + len.to_int() <= out0.len().to_int() && + out0.len() == out1.len() + )] + #[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() + )] fn squeeze2( &self, out0: &mut [u8], diff --git a/crates/algorithms/sha3/src/traits.rs b/crates/algorithms/sha3/src/traits.rs index 99b9328d0b..767172aaa6 100644 --- a/crates/algorithms/sha3/src/traits.rs +++ b/crates/algorithms/sha3/src/traits.rs @@ -167,7 +167,78 @@ pub(crate) trait Squeeze> { /// /// Store blocks `N = 2` #[cfg(feature = "simd128")] +#[hax_lib::fstar::replace( + interface, + " +class t_Squeeze2 (v_Self: Type0) (v_T: Type0) = { + // TODO: This super variable is problematic and makes typecheck fail + // https://github.com/cryspen/hax/issues/1554 + // [@@@ FStar.Tactics.Typeclasses.no_method]_super_i0:t_KeccakItem v_T (mk_usize 2); + f_squeeze2_pre: + v_RATE: usize -> + self_: v_Self -> + out0: t_Slice u8 -> + out1: t_Slice u8 -> + start: usize -> + len: usize + -> pred: + Type0 + { Libcrux_sha3.Proof_utils.valid_rate v_RATE && len <=. v_RATE && + ((Rust_primitives.Hax.Int.from_machine start <: Hax_lib.Int.t_Int) + + (Rust_primitives.Hax.Int.from_machine len <: Hax_lib.Int.t_Int) + <: + Hax_lib.Int.t_Int) <= + (Rust_primitives.Hax.Int.from_machine (Core_models.Slice.impl__len #u8 out0 <: usize) + <: + Hax_lib.Int.t_Int) && + (Core_models.Slice.impl__len #u8 out0 <: usize) =. + (Core_models.Slice.impl__len #u8 out1 <: usize) ==> + pred }; + f_squeeze2_post: + v_RATE: usize -> + self_: v_Self -> + out0: t_Slice u8 -> + out1: t_Slice u8 -> + start: usize -> + len: usize -> + x: (t_Slice u8 & t_Slice u8) + -> pred: + Type0 + { pred ==> + (let (out0_future: t_Slice u8), (out1_future: t_Slice u8) = x in + (Core_models.Slice.impl__len #u8 out0_future <: usize) =. + (Core_models.Slice.impl__len #u8 out0 <: usize) && + (Core_models.Slice.impl__len #u8 out1_future <: usize) =. + (Core_models.Slice.impl__len #u8 out1 <: usize)) }; + f_squeeze2: + v_RATE: usize -> + x0: v_Self -> + x1: t_Slice u8 -> + x2: t_Slice u8 -> + x3: usize -> + x4: usize + -> Prims.Pure (t_Slice u8 & t_Slice u8) + (f_squeeze2_pre v_RATE x0 x1 x2 x3 x4) + (fun result -> f_squeeze2_post v_RATE x0 x1 x2 x3 x4 result) +} + +// TODO: See above +// [@@ FStar.Tactics.Typeclasses.tcinstance] +// let _ = fun (v_Self:Type0) (v_T:Type0) {|i: t_Squeeze2 v_Self v_T|} -> i._super_i0 +" +)] +#[hax_lib::attributes] pub(crate) trait Squeeze2> { + #[hax_lib::requires( + valid_rate(RATE) && + len <= RATE && + start.to_int() + len.to_int() <= out0.len().to_int() && + out0.len() == out1.len() + )] + #[hax_lib::ensures(|_| + future(out0).len() == out0.len() && + future(out1).len() == out1.len() + )] fn squeeze2( &self, out0: &mut [u8], From 6c0096ce889fa54a9cfea3e87f8a8ed0e0d1cb59 Mon Sep 17 00:00:00 2001 From: Parrot7483 <47054801+Parrot7483@users.noreply.github.com> Date: Mon, 9 Mar 2026 17:32:59 +0100 Subject: [PATCH 4/5] Add full type check for SHA3 AVX2 --- crates/algorithms/sha3/src/avx2.rs | 90 ++++++++++ .../sha3/src/generic_keccak/simd256.rs | 170 +++++++++++++----- crates/algorithms/sha3/src/simd/avx2.rs | 158 +++++++++++++--- crates/algorithms/sha3/src/traits.rs | 95 ++++++++++ 4 files changed, 448 insertions(+), 65 deletions(-) diff --git a/crates/algorithms/sha3/src/avx2.rs b/crates/algorithms/sha3/src/avx2.rs index 79df89d937..bee6f9b306 100644 --- a/crates/algorithms/sha3/src/avx2.rs +++ b/crates/algorithms/sha3/src/avx2.rs @@ -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], @@ -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>, } @@ -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, @@ -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], @@ -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], @@ -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], @@ -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], @@ -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], @@ -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], diff --git a/crates/algorithms/sha3/src/generic_keccak/simd256.rs b/crates/algorithms/sha3/src/generic_keccak/simd256.rs index 5b1566e0f4..2f7f732974 100644 --- a/crates/algorithms/sha3/src/generic_keccak/simd256.rs +++ b/crates/algorithms/sha3/src/generic_keccak/simd256.rs @@ -2,51 +2,24 @@ use super::*; use libcrux_intrinsics::avx2::Vec256; -#[inline(always)] -pub(crate) fn keccak4( - data: &[&[u8]; 4], - out0: &mut [u8], - out1: &mut [u8], - out2: &mut [u8], - out3: &mut [u8], -) { - #[cfg(not(eurydice))] - debug_assert!(out0.len() == out1.len() && out0.len() == out2.len() && out0.len() == out3.len()); - #[cfg(not(eurydice))] - debug_assert!( - data[0].len() == data[1].len() - && data[0].len() == data[2].len() - && data[0].len() == data[3].len() - ); - - let mut s = KeccakState::<4, Vec256>::new(); - let data_len = data[0].len(); - for i in 0..data_len / RATE { - s.absorb_block::(data, i * RATE); - } - let rem = data_len % RATE; - s.absorb_final::(data, data_len - rem, rem); - - let outlen = out0.len(); - let blocks = outlen / RATE; - let last = outlen - (outlen % RATE); - - if blocks == 0 { - s.squeeze4::(out0, out1, out2, out3, 0, outlen); - } else { - s.squeeze4::(out0, out1, out2, out3, 0, RATE); - for i in 1..blocks { - s.keccakf1600(); - s.squeeze4::(out0, out1, out2, out3, i * RATE, RATE); - } - if last < outlen { - s.keccakf1600(); - s.squeeze4::(out0, out1, out2, out3, last, outlen - last); - } - } -} +#[cfg(hax)] +use crate::proof_utils::{lemma_mul_succ_le, valid_rate}; +#[hax_lib::attributes] impl KeccakState<4, Vec256> { + #[hax_lib::requires( + valid_rate(RATE) && + start.to_int() + RATE.to_int() <= out0.len().to_int() && + 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(crate) fn squeeze_next_block( &mut self, @@ -60,6 +33,19 @@ impl KeccakState<4, Vec256> { self.squeeze4::(out0, out1, out2, out3, start, RATE); } + #[hax_lib::requires( + valid_rate(RATE) && + RATE <= out0.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(crate) fn squeeze_first_block( &self, @@ -71,6 +57,19 @@ impl KeccakState<4, Vec256> { self.squeeze4::(out0, out1, out2, out3, 0, RATE); } + #[hax_lib::requires( + valid_rate(RATE) && + 3 * RATE <= out0.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(crate) fn squeeze_first_three_blocks( &mut self, @@ -88,6 +87,19 @@ impl KeccakState<4, Vec256> { self.squeeze4::(out0, out1, out2, out3, 2 * RATE, RATE); } + #[hax_lib::requires( + valid_rate(RATE) && + 5 * RATE <= out0.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(crate) fn squeeze_first_five_blocks( &mut self, @@ -111,3 +123,75 @@ impl KeccakState<4, Vec256> { self.squeeze4::(out0, out1, out2, out3, 4 * RATE, RATE); } } + +#[hax_lib::requires( + valid_rate(RATE) && + data[0].len() == data[1].len() && + data[0].len() == data[2].len() && + data[0].len() == data[3].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() +)] +#[hax_lib::fstar::options("--split_queries always --z3rlimit 300")] +#[inline] +pub(crate) fn keccak4( + data: &[&[u8]; 4], + out0: &mut [u8], + out1: &mut [u8], + out2: &mut [u8], + out3: &mut [u8], +) { + debug_assert!( + data[0].len() == data[1].len() + && data[0].len() == data[2].len() + && data[0].len() == data[3].len() + ); + debug_assert!(out0.len() == out1.len() && out0.len() == out2.len() && out0.len() == out3.len()); + + // Initialize Keccak state + let mut s = KeccakState::<4, Vec256>::new(); + + // Absorb input + let input_len = data[0].len(); + let input_blocks = input_len / RATE; + let input_rem = input_len % RATE; + for i in 0..input_blocks { + #[cfg(hax)] + lemma_mul_succ_le(i, input_blocks, RATE); + + s.absorb_block::(data, i * RATE); + } + s.absorb_final::(data, input_len - input_rem, input_rem); + + // Squeeze output + let output_len = out0.len(); + let output_blocks = output_len / RATE; + let output_rem = output_len % RATE; + if output_blocks == 0 { + s.squeeze4::(out0, out1, out2, out3, 0, output_len); + } else { + s.squeeze4::(out0, out1, out2, out3, 0, RATE); + for i in 1..output_blocks { + hax_lib::loop_invariant!(|_: usize| out0.len() == output_len + && out0.len() == out1.len() + && out0.len() == out2.len() + && out0.len() == out3.len()); + #[cfg(hax)] + lemma_mul_succ_le(i, output_blocks, RATE); + + s.keccakf1600(); + s.squeeze4::(out0, out1, out2, out3, i * RATE, RATE); + } + if output_rem != 0 { + s.keccakf1600(); + s.squeeze4::(out0, out1, out2, out3, output_len - output_rem, output_rem); + } + } +} diff --git a/crates/algorithms/sha3/src/simd/avx2.rs b/crates/algorithms/sha3/src/simd/avx2.rs index 40a38e77ef..b74f484268 100644 --- a/crates/algorithms/sha3/src/simd/avx2.rs +++ b/crates/algorithms/sha3/src/simd/avx2.rs @@ -2,10 +2,23 @@ use libcrux_intrinsics::avx2::*; use crate::{generic_keccak::KeccakState, traits::*}; +#[cfg(hax)] +use hax_lib::int::*; + +#[cfg(hax)] +use crate::proof_utils::valid_rate; + #[inline(always)] +#[hax_lib::requires( + LEFT.to_int() + RIGHT.to_int() == 64.to_int() && + RIGHT > 0 && + RIGHT < 64 +)] fn rotate_left(x: Vec256) -> Vec256 { #[cfg(not(eurydice))] debug_assert!(LEFT + RIGHT == 64); + debug_assert!(RIGHT > 0); + debug_assert!(RIGHT < 64); // This could be done more efficiently, if the shift values are multiples of 8. // However, in SHA-3 this function is only called twice with such inputs (8/56). mm256_xor_si256(mm256_slli_epi64::(x), mm256_srli_epi64::(x)) @@ -25,6 +38,11 @@ fn _vrax1q_u64(a: Vec256, b: Vec256) -> Vec256 { } #[inline(always)] +#[hax_lib::requires( + LEFT.to_int() + RIGHT.to_int() == 64.to_int() && + RIGHT > 0 && + RIGHT < 64 +)] fn _vxarq_u64(a: Vec256, b: Vec256) -> Vec256 { let ab = mm256_xor_si256(a, b); rotate_left::(ab) @@ -43,6 +61,13 @@ fn _veorq_n_u64(a: Vec256, c: u64) -> Vec256 { } #[inline(always)] +#[hax_lib::requires( + valid_rate(RATE) && + offset.to_int() + RATE.to_int() <= blocks[0].len().to_int() && + blocks[0].len() == blocks[1].len() && + blocks[0].len() == blocks[2].len() && + blocks[0].len() == blocks[3].len() +)] pub(crate) fn load_block( state: &mut [Vec256; 25], blocks: &[&[u8]; 4], @@ -107,6 +132,14 @@ pub(crate) fn load_block( } #[inline(always)] +#[hax_lib::requires( + valid_rate(RATE) && + len < RATE && + start.to_int() + len.to_int() <= blocks[0].len().to_int() && + blocks[0].len() == blocks[1].len() && + blocks[0].len() == blocks[2].len() && + blocks[0].len() == blocks[3].len() +)] pub(crate) fn load_last( state: &mut [Vec256; 25], blocks: &[&[u8]; 4], @@ -133,6 +166,20 @@ pub(crate) fn load_last( } #[inline(always)] +#[hax_lib::requires( + valid_rate(RATE) && + len <= RATE && + start.to_int() + len.to_int() <= out0.len().to_int() && + 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(crate) fn store_block( s: &[Vec256; 25], out0: &mut [u8], @@ -143,7 +190,17 @@ pub(crate) fn store_block( len: usize, ) { let chunks = len / 32; + + #[cfg(hax)] + let (out0_len, out1_len, out2_len, out3_len) = (out0.len(), out1.len(), out2.len(), out3.len()); + for i in 0..chunks { + #[cfg(hax)] + hax_lib::loop_invariant!(|_: usize| out0.len() == out0_len + && out1.len() == out1_len + && out2.len() == out2_len + && out3.len() == out3_len); + let i0 = (4 * i) / 5; let j0 = (4 * i) % 5; let i1 = (4 * i + 1) / 5; @@ -153,8 +210,7 @@ pub(crate) fn store_block( let i3 = (4 * i + 3) / 5; let j3 = (4 * i + 3) % 5; - let v0l = mm256_permute2x128_si256::<0x20>(*get_ij(s, i0, j0), *get_ij(s, i2, j2)); - // 0 0 2 2 + let v0l = mm256_permute2x128_si256::<0x20>(*get_ij(s, i0, j0), *get_ij(s, i2, j2)); // 0 0 2 2 let v1h = mm256_permute2x128_si256::<0x20>(*get_ij(s, i1, j1), *get_ij(s, i3, j3)); // 1 1 3 3 let v2l = mm256_permute2x128_si256::<0x31>(*get_ij(s, i0, j0), *get_ij(s, i2, j2)); // 0 0 2 2 let v3h = mm256_permute2x128_si256::<0x31>(*get_ij(s, i1, j1), *get_ij(s, i3, j3)); // 1 1 3 3 @@ -164,39 +220,61 @@ pub(crate) fn store_block( let v2 = mm256_unpacklo_epi64(v2l, v3h); // 0 1 2 3 let v3 = mm256_unpackhi_epi64(v2l, v3h); // 0 1 2 3 - mm256_storeu_si256_u8(&mut out0[start + 32 * i..start + 32 * (i + 1)], v0); - mm256_storeu_si256_u8(&mut out1[start + 32 * i..start + 32 * (i + 1)], v1); - mm256_storeu_si256_u8(&mut out2[start + 32 * i..start + 32 * (i + 1)], v2); - mm256_storeu_si256_u8(&mut out3[start + 32 * i..start + 32 * (i + 1)], v3); + let base = start + 32 * i; + let limit = base + 32; + + mm256_storeu_si256_u8(&mut out0[base..limit], v0); + mm256_storeu_si256_u8(&mut out1[base..limit], v1); + mm256_storeu_si256_u8(&mut out2[base..limit], v2); + mm256_storeu_si256_u8(&mut out3[base..limit], v3); } let rem = len % 32; if rem > 0 { - let start = start + 32 * chunks; - let mut u8s = [0u8; 32]; + let mut tmp = [0u8; 32]; let chunks8 = rem / 8; + for k in 0..chunks8 { - let i = (4 * chunks + k) / 5; - let j = (4 * chunks + k) % 5; - mm256_storeu_si256_u8(&mut u8s, *get_ij(s, i, j)); - out0[start + 8 * k..start + 8 * (k + 1)].copy_from_slice(&u8s[0..8]); - out1[start + 8 * k..start + 8 * (k + 1)].copy_from_slice(&u8s[8..16]); - out2[start + 8 * k..start + 8 * (k + 1)].copy_from_slice(&u8s[16..24]); - out3[start + 8 * k..start + 8 * (k + 1)].copy_from_slice(&u8s[24..32]); + hax_lib::loop_invariant!(|_: usize| out0.len() == out0_len + && out1.len() == out1_len + && out2.len() == out2_len + && out3.len() == out3_len); + + let idx = 4 * chunks + k; + let i = idx / 5; + let j = idx % 5; + + mm256_storeu_si256_u8(&mut tmp, *get_ij(s, i, j)); + + let base = start + 32 * chunks + 8 * k; + let limit = base + 8; + + out0[base..limit].copy_from_slice(&tmp[0..8]); + out1[base..limit].copy_from_slice(&tmp[8..16]); + out2[base..limit].copy_from_slice(&tmp[16..24]); + out3[base..limit].copy_from_slice(&tmp[24..32]); } + let rem8 = rem % 8; if rem8 > 0 { - let i = (4 * chunks + chunks8) / 5; - let j = (4 * chunks + chunks8) % 5; - mm256_storeu_si256_u8(&mut u8s, *get_ij(s, i, j)); - out0[start + len - rem8..start + len].copy_from_slice(&u8s[0..rem8]); - out1[start + len - rem8..start + len].copy_from_slice(&u8s[8..8 + rem8]); - out2[start + len - rem8..start + len].copy_from_slice(&u8s[16..16 + rem8]); - out3[start + len - rem8..start + len].copy_from_slice(&u8s[24..24 + rem8]); + let idx = 4 * chunks + chunks8; + let i = idx / 5; + let j = idx % 5; + + mm256_storeu_si256_u8(&mut tmp, *get_ij(s, i, j)); + + let limit = start + len; + let base = limit - rem8; + + out0[base..limit].copy_from_slice(&tmp[0..rem8]); + out1[base..limit].copy_from_slice(&tmp[8..8 + rem8]); + out2[base..limit].copy_from_slice(&tmp[16..16 + rem8]); + out3[base..limit].copy_from_slice(&tmp[24..24 + rem8]); } } } +#[hax_lib::attributes] impl KeccakItem<4> for Vec256 { #[inline(always)] fn zero() -> Self { @@ -211,6 +289,11 @@ impl KeccakItem<4> for Vec256 { _vrax1q_u64(a, b) } #[inline(always)] + #[hax_lib::requires( + LEFT.to_int() + RIGHT.to_int() == 64.to_int() && + RIGHT > 0 && + RIGHT < 64 + )] fn xor_and_rotate(a: Self, b: Self) -> Self { _vxarq_u64::(a, b) } @@ -228,11 +311,27 @@ impl KeccakItem<4> for Vec256 { } } +#[hax_lib::attributes] impl Absorb<4> for KeccakState<4, Vec256> { + #[hax_lib::requires( + valid_rate(RATE) && + start.to_int() + RATE.to_int() <= input[0].len().to_int() && + input[0].len() == input[1].len() && + input[0].len() == input[2].len() && + input[0].len() == input[3].len() + )] fn load_block(&mut self, input: &[&[u8]; 4], start: usize) { load_block::(&mut self.st, input, start); } + #[hax_lib::requires( + valid_rate(RATE) && + len < RATE && + start.to_int() + len.to_int() <= input[0].len().to_int() && + input[0].len() == input[1].len() && + input[0].len() == input[2].len() && + input[0].len() == input[3].len() + )] fn load_last( &mut self, input: &[&[u8]; 4], @@ -243,7 +342,22 @@ impl Absorb<4> for KeccakState<4, Vec256> { } } +#[hax_lib::attributes] impl Squeeze4 for KeccakState<4, Vec256> { + #[hax_lib::requires( + valid_rate(RATE) && + len <= RATE && + start.to_int() + len.to_int() <= out0.len().to_int() && + 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() + )] fn squeeze4( &self, out0: &mut [u8], diff --git a/crates/algorithms/sha3/src/traits.rs b/crates/algorithms/sha3/src/traits.rs index 767172aaa6..4faef5ef38 100644 --- a/crates/algorithms/sha3/src/traits.rs +++ b/crates/algorithms/sha3/src/traits.rs @@ -255,7 +255,102 @@ pub(crate) trait Squeeze2> { /// /// Store blocks `N = 4` #[cfg(feature = "simd256")] +#[hax_lib::fstar::replace( + interface, + " +class t_Squeeze4 (v_Self: Type0) (v_T: Type0) = { + // TODO: This super variable is problematic and makes typecheck fail + // https://github.com/cryspen/hax/issues/1554 + // [@@@ FStar.Tactics.Typeclasses.no_method]_super_i0:t_KeccakItem v_T (mk_usize 4); + f_squeeze4_pre: + v_RATE: usize -> + self_: v_Self -> + out0: t_Slice u8 -> + out1: t_Slice u8 -> + out2: t_Slice u8 -> + out3: t_Slice u8 -> + start: usize -> + len: usize + -> pred: + Type0 + { Libcrux_sha3.Proof_utils.valid_rate v_RATE && len <=. v_RATE && + ((Rust_primitives.Hax.Int.from_machine start <: Hax_lib.Int.t_Int) + + (Rust_primitives.Hax.Int.from_machine len <: Hax_lib.Int.t_Int) + <: + Hax_lib.Int.t_Int) <= + (Rust_primitives.Hax.Int.from_machine (Core_models.Slice.impl__len #u8 out0 <: usize) + <: + Hax_lib.Int.t_Int) && + (Core_models.Slice.impl__len #u8 out0 <: usize) =. + (Core_models.Slice.impl__len #u8 out1 <: usize) && + (Core_models.Slice.impl__len #u8 out1 <: usize) =. + (Core_models.Slice.impl__len #u8 out2 <: usize) && + (Core_models.Slice.impl__len #u8 out2 <: usize) =. + (Core_models.Slice.impl__len #u8 out3 <: usize) ==> + pred }; + f_squeeze4_post: + v_RATE: usize -> + self_: v_Self -> + out0: t_Slice u8 -> + out1: t_Slice u8 -> + out2: t_Slice u8 -> + out3: t_Slice u8 -> + start: usize -> + len: usize -> + x: (t_Slice u8 & t_Slice u8 & t_Slice u8 & t_Slice u8) + -> pred: + Type0 + { pred ==> + (let + (out0_future: t_Slice u8), + (out1_future: t_Slice u8), + (out2_future: t_Slice u8), + (out3_future: t_Slice u8) = + x + in + (Core_models.Slice.impl__len #u8 out0_future <: usize) =. + (Core_models.Slice.impl__len #u8 out0 <: usize) && + (Core_models.Slice.impl__len #u8 out1_future <: usize) =. + (Core_models.Slice.impl__len #u8 out1 <: usize) && + (Core_models.Slice.impl__len #u8 out2_future <: usize) =. + (Core_models.Slice.impl__len #u8 out2 <: usize) && + (Core_models.Slice.impl__len #u8 out3_future <: usize) =. + (Core_models.Slice.impl__len #u8 out3 <: usize)) }; + f_squeeze4: + v_RATE: usize -> + x0: v_Self -> + x1: t_Slice u8 -> + x2: t_Slice u8 -> + x3: t_Slice u8 -> + x4: t_Slice u8 -> + x5: usize -> + x6: usize + -> Prims.Pure (t_Slice u8 & t_Slice u8 & t_Slice u8 & t_Slice u8) + (f_squeeze4_pre v_RATE x0 x1 x2 x3 x4 x5 x6) + (fun result -> f_squeeze4_post v_RATE x0 x1 x2 x3 x4 x5 x6 result) +} + +// TODO: See above +// [@@ FStar.Tactics.Typeclasses.tcinstance] +// let _ = fun (v_Self:Type0) (v_T:Type0) {|i: t_Squeeze4 v_Self v_T|} -> i._super_i0 +" +)] +#[hax_lib::attributes] pub(crate) trait Squeeze4> { + #[hax_lib::requires( + valid_rate(RATE) && + len <= RATE && + start.to_int() + len.to_int() <= out0.len().to_int() && + out0.len() == out1.len() && + out1.len() == out2.len() && + out2.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() + )] fn squeeze4( &self, out0: &mut [u8], From e908bc1b164f390159e395546dee4b135b82e71b Mon Sep 17 00:00:00 2001 From: Parrot7483 <47054801+Parrot7483@users.noreply.github.com> Date: Mon, 9 Mar 2026 18:23:04 +0100 Subject: [PATCH 5/5] Extract and type-check with SIMD features Enable simd128,simd256 in hax.sh and update the CI workflow to cover all modules. --- .github/workflows/sha3-hax.yml | 28 ++++++++++++++-------------- crates/algorithms/sha3/hax.sh | 6 ++---- 2 files changed, 16 insertions(+), 18 deletions(-) diff --git a/.github/workflows/sha3-hax.yml b/.github/workflows/sha3-hax.yml index 569912f0f9..942365df44 100644 --- a/.github/workflows/sha3-hax.yml +++ b/.github/workflows/sha3-hax.yml @@ -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: @@ -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 @@ -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 @@ -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 @@ -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 diff --git a/crates/algorithms/sha3/hax.sh b/crates/algorithms/sha3/hax.sh index b3572ecdb5..72c80c2178 100755 --- a/crates/algorithms/sha3/hax.sh +++ b/crates/algorithms/sha3/hax.sh @@ -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 "+**" @@ -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 }