Skip to content

Commit 153b003

Browse files
Parrot7483Parrot7483
committed
apply feedback from franziskuskiefer 2
1 parent 8dd8df7 commit 153b003

File tree

8 files changed

+166
-169
lines changed

8 files changed

+166
-169
lines changed

‎libcrux-sha3/src/generic_keccak.rs‎

Lines changed: 11 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,10 @@ use core::ops::Index;
66
use crate::traits::*;
77

88
#[cfg(hax)]
9-
use hax_lib::{constructors::from_bool, forall, implies, int::ToInt};
9+
use crate::proof_utils::{slices_same_len, valid_rate};
10+
11+
#[cfg(hax)]
12+
use hax_lib::{constructors::from_bool, int::ToInt};
1013

1114
/// A generic Xof API.
1215
pub(crate) mod xof;
@@ -99,6 +102,9 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
99102
]
100103
}
101104

105+
// Splitting rho and pi into multiple functions is needed for formal verification in F*.
106+
// Having to many manipulations of the keccak state in a single function causes the
107+
// verification condition explode exponentially and never completes.
102108
#[inline(always)]
103109
fn rho_0(&mut self, t: [T; 5]) {
104110
self.set(0, 0, T::xor(self[(0, 0)], t[0]));
@@ -245,17 +251,10 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
245251
#[hax_lib::requires(
246252
from_bool(
247253
N != 0 &&
248-
RATE <= 200 &&
249-
RATE % 8 == 0 &&
250-
(RATE % 32 == 8 || RATE % 32 == 16) &&
254+
valid_rate(RATE) &&
251255
start.to_int() + RATE.to_int() <= input[0].len().to_int()
252256
).and(
253-
forall(|i: usize|
254-
implies(
255-
i < N,
256-
input[0].len() == input[i].len()
257-
)
258-
)
257+
slices_same_len(input)
259258
)
260259
)]
261260
fn absorb_block<const RATE: usize>(&mut self, input: &[&[u8]; N], start: usize)
@@ -273,18 +272,11 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
273272
#[hax_lib::requires(
274273
from_bool(
275274
N != 0 &&
276-
RATE <= 200 &&
277-
RATE % 8 == 0 &&
278-
(RATE % 32 == 8 || RATE % 32 == 16) &&
275+
valid_rate(RATE) &&
279276
len < RATE &&
280277
start.to_int() + len.to_int() <= input[0].len().to_int()
281278
).and(
282-
forall(|i: usize|
283-
implies(
284-
i < N,
285-
input[0].len() == input[i].len()
286-
)
287-
)
279+
slices_same_len(input)
288280
)
289281
)]
290282
pub(crate) fn absorb_final<const RATE: usize, const DELIM: u8>(

‎libcrux-sha3/src/generic_keccak/portable.rs‎

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,17 @@
11
use super::*;
22

33
#[cfg(hax)]
4-
#[hax_lib::fstar::replace("open Libcrux_sha3.Lemmas")]
4+
use crate::proof_utils::valid_rate;
5+
6+
#[cfg(hax)]
7+
#[hax_lib::fstar::replace("open Libcrux_sha3.Proof_utils.Lemmas")]
58
const _: () = ();
69

710
#[hax_lib::attributes]
811
impl KeccakState<1, u64> {
912
#[inline(always)]
1013
#[hax_lib::requires(
11-
RATE <= 200 &&
14+
valid_rate(RATE) &&
1215
start.to_int() + RATE.to_int() <= out.len().to_int()
1316
)]
1417
#[hax_lib::ensures(|_| future(out).len() == out.len())]
@@ -19,7 +22,7 @@ impl KeccakState<1, u64> {
1922

2023
#[inline(always)]
2124
#[hax_lib::requires(
22-
RATE <= 200 &&
25+
valid_rate(RATE) &&
2326
RATE <= out.len()
2427
)]
2528
#[hax_lib::ensures(|_| future(out).len() == out.len())]
@@ -29,7 +32,7 @@ impl KeccakState<1, u64> {
2932

3033
#[inline(always)]
3134
#[hax_lib::requires(
32-
RATE <= 200 &&
35+
valid_rate(RATE) &&
3336
3 * RATE <= out.len()
3437
)]
3538
#[hax_lib::ensures(|_| future(out).len() == out.len())]
@@ -45,7 +48,7 @@ impl KeccakState<1, u64> {
4548

4649
#[inline(always)]
4750
#[hax_lib::requires(
48-
RATE <= 200 &&
51+
valid_rate(RATE) &&
4952
5 * RATE <= out.len()
5053
)]
5154
#[hax_lib::ensures(|_| future(out).len() == out.len())]
@@ -66,11 +69,7 @@ impl KeccakState<1, u64> {
6669
}
6770
}
6871

69-
#[hax_lib::requires(
70-
RATE != 0 &&
71-
RATE <= 200 &&
72-
RATE % 8 == 0
73-
)]
72+
#[hax_lib::requires(valid_rate(RATE))]
7473
#[hax_lib::ensures(|_| future(output).len() == output.len())]
7574
#[hax_lib::fstar::options("--split_queries always --z3rlimit 300")]
7675
#[inline]

‎libcrux-sha3/src/generic_keccak/xof.rs‎

Lines changed: 48 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,14 @@ use crate::{
66
};
77

88
#[cfg(hax)]
9-
#[hax_lib::fstar::replace("open Libcrux_sha3.Lemmas")]
9+
use crate::proof_utils::valid_rate;
10+
11+
#[cfg(hax)]
12+
#[hax_lib::fstar::replace("open Libcrux_sha3.Proof_utils.Lemmas")]
1013
const _: () = ();
1114

12-
// TODO: Should not be needed. Use hax_lib::fstar::options("")
15+
// TODO: Should not be needed. Use hax_lib::fstar::options("") below.
16+
// Known bug: https://github.com/cryspen/hax/issues/1698
1317
#[hax_lib::fstar::before(
1418
r#"
1519
#push-options "--split_queries always --z3rlimit 300"
@@ -18,7 +22,6 @@ const _: () = ();
1822

1923
/// The internal keccak state that can also buffer inputs to absorb.
2024
/// This is used in the general xof APIs.
21-
#[hax_lib::attributes]
2225
pub(crate) struct KeccakXofState<
2326
const PARALLEL_LANES: usize,
2427
const RATE: usize,
@@ -44,15 +47,11 @@ pub(crate) fn keccak_xof_state_inv<
4447
>(
4548
xof: &KeccakXofState<PARALLEL_LANES, RATE, STATE>,
4649
) -> bool {
47-
RATE != 0
48-
&& RATE <= 200
49-
&& RATE % 8 == 0
50-
&& (RATE % 32 == 8 || RATE % 32 == 16)
51-
&& xof.buf_len <= RATE
50+
valid_rate(RATE) && xof.buf_len <= RATE
5251
}
5352

5453
#[hax_lib::attributes]
55-
#[hax_lib::fstar::options("--split_queries always --z3rlimit 300")] // TODO: Has no effect
54+
#[hax_lib::fstar::options("--split_queries always --z3rlimit 300")] // TODO: Has no effect. See above.
5655
impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_LANES>>
5756
KeccakXofState<PARALLEL_LANES, RATE, STATE>
5857
{
@@ -63,10 +62,8 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
6362

6463
/// Generate a new keccak xof state.
6564
#[hax_lib::requires(
66-
PARALLEL_LANES == 1 && // TODO: Generalize for the parallel case
67-
RATE != 0 &&
68-
RATE <= 200 &&
69-
RATE % 8 == 0
65+
PARALLEL_LANES == 1 &&
66+
valid_rate(RATE)
7067
)]
7168
#[hax_lib::ensures(|result| keccak_xof_state_inv(&result))]
7269
pub(crate) fn new() -> Self {
@@ -97,7 +94,6 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
9794
/// If `consumed > 0` is returned, `self.buf` contains a full block to be
9895
/// loaded.
9996
// Note: consciously not inlining this function to avoid using too much stack
100-
// #[hax_lib::fstar::options("--fuel 5")]
10197
#[hax_lib::requires(
10298
PARALLEL_LANES == 1 &&
10399
keccak_xof_state_inv(self)
@@ -186,13 +182,11 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
186182
let remainder = input_to_consume % RATE;
187183

188184
#[cfg(hax)]
189-
let self_buf_len = self.buf_len;
190-
191-
#[cfg(hax)]
192-
let end = consumed + num_blocks * RATE;
193-
194-
#[cfg(hax)]
195-
hax_lib::assert!(end <= inputs[0].len());
185+
let (self_buf_len, end) = {
186+
let end = consumed + num_blocks * RATE;
187+
hax_lib::assert!(end <= inputs[0].len());
188+
(self.buf_len, end)
189+
};
196190

197191
for i in 0..num_blocks {
198192
hax_lib::loop_invariant!(|_: usize| self.buf_len == self_buf_len);
@@ -298,54 +292,55 @@ impl<const RATE: usize, STATE: KeccakItem<1>> KeccakXofState<1, RATE, STATE> {
298292
where
299293
KeccakState<1, STATE>: Squeeze<STATE>,
300294
{
295+
let out_len = out.len();
296+
297+
if out_len == 0 {
298+
return;
299+
}
300+
301301
if self.sponge {
302302
// If we called `squeeze` before, call f1600 first.
303303
// We do it this way around so that we don't call f1600 at the end
304304
// when we don't need it.
305305
self.inner.keccakf1600();
306306
}
307307

308-
let out_len = out.len();
309-
310-
if out_len > 0 {
311-
if out_len <= RATE {
312-
self.inner.squeeze::<RATE>(out, 0, out_len);
313-
} else {
314-
// How many blocks do we need to squeeze out?
315-
let blocks = out_len / RATE;
308+
if out_len <= RATE {
309+
self.inner.squeeze::<RATE>(out, 0, out_len);
310+
} else {
311+
// How many blocks do we need to squeeze out?
312+
let blocks = out_len / RATE;
313+
let remaining = out_len % RATE;
316314

317-
#[cfg(hax)]
318-
let self_buf_len = self.buf_len;
315+
#[cfg(hax)]
316+
let self_buf_len = self.buf_len;
319317

320-
for i in 0..blocks {
321-
hax_lib::loop_invariant!(
322-
|_: usize| out.len() == out_len && self_buf_len == self.buf_len
323-
);
324-
hax_lib::fstar!("assert (v i * v v_RATE <= v out_len)");
318+
for i in 0..blocks {
319+
hax_lib::loop_invariant!(
320+
|_: usize| out.len() == out_len && self_buf_len == self.buf_len
321+
);
322+
hax_lib::assert!(i.to_int() * RATE.to_int() <= out.len().to_int());
325323

326-
#[cfg(hax)]
327-
hax_lib::assert!(i.to_int() * RATE.to_int() <= out.len().to_int());
324+
// Here we know that we always have full blocks to write out.
325+
self.inner.keccakf1600();
326+
self.inner.squeeze::<RATE>(out, i * RATE, RATE);
327+
}
328328

329-
// Here we know that we always have full blocks to write out.
330-
self.inner.keccakf1600();
331-
self.inner.squeeze::<RATE>(out, i * RATE, RATE);
332-
}
329+
if remaining > 0 {
330+
// Squeeze out the last partial block
331+
self.inner.keccakf1600();
333332

334333
// For a and b with b < a
335334
// (a / b) * b + a % b = a
335+
hax_lib::fstar!("lemma_div_mul_mod out_len v_RATE");
336+
hax_lib::assert!(
337+
blocks.to_int() * RATE.to_int() + remaining.to_int() == out.len().to_int()
338+
);
336339

337-
let remaining = out_len % RATE;
338-
if remaining > 0 {
339-
// Squeeze out the last partial block
340-
self.inner.keccakf1600();
341-
342-
hax_lib::fstar!("lemma_div_mul_mod out_len v_RATE");
343-
hax_lib::fstar!("assert (v blocks * v v_RATE + v remaining == v out_len)");
344-
345-
self.inner.squeeze::<RATE>(out, blocks * RATE, remaining);
346-
}
340+
self.inner.squeeze::<RATE>(out, blocks * RATE, remaining);
347341
}
348-
self.sponge = true;
349342
}
343+
344+
self.sponge = true;
350345
}
351346
}

‎libcrux-sha3/src/lemmas.rs‎

Lines changed: 0 additions & 44 deletions
This file was deleted.

‎libcrux-sha3/src/lib.rs‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -21,9 +21,9 @@ use hax_lib::int::*;
2121

2222
mod traits;
2323

24-
/// F* verification lemmas
24+
/// F* verification helper
2525
#[cfg(hax)]
26-
pub(crate) mod lemmas;
26+
pub(crate) mod proof_utils;
2727

2828
/// A SHA3 224 Digest
2929
pub type Sha3_224Digest = [u8; 28];
@@ -54,10 +54,9 @@ pub enum Algorithm {
5454
Sha512 = 4,
5555
}
5656

57-
// TODO: Verification fails because of the panic
57+
// Verification fails because of the panic
5858
#[cfg(not(any(hax, eurydice)))]
5959
impl From<u32> for Algorithm {
60-
#[hax_lib::requires(v == 1 || v == 2 || v == 3 || v == 4)]
6160
fn from(v: u32) -> Algorithm {
6261
match v {
6362
1 => Algorithm::Sha224,

0 commit comments

Comments
 (0)