Correctness Proofs for SHA-3 (Part 1): A Rust Specification for SHA-3#1399
Correctness Proofs for SHA-3 (Part 1): A Rust Specification for SHA-3#1399karthikbhargavan wants to merge 8 commits into
Conversation
Adds a Hacspec specification of FIPS 202 (SHA-3 / SHAKE) under specs/sha3, with hax extraction to F* and verification of the four root modules (Hacspec_sha3, .Keccak_f, .Sha3, .Sponge). The spec compiles against hax-lib 0.3.6 and verifies at the default rlimit (no Proof_Utils dependency, no fstar! escape hatches): properties beyond well-typedness and bound checks are deferred to a follow-up that brings the implementation proofs. Adds the new crate to the specs/ sub-workspace. Spec authored by Karthik Bhargavan. Claude (Opus 4.7) was used to review and test the spec; it did not author the spec content.
The KeccakState helpers used 5*j+i but the rest of the impl (and the corresponding hacspec spec, see specs/sha3) treats the lane layout as 5*i+j. Aligns with FIPS 202 §3.1.2 lane indexing. Authored by Karthik Bhargavan with Claude (Opus 4.7) used to review and test.
Adds crates/algorithms/sha3/tests/cross_spec.rs comparing the public SHA-3/SHAKE API (including AVX2 x4 SHAKE256 and Neon x2 parallel variants) against hacspec_sha3 on boundary input sizes. Adds an embedded #[cfg(test)] mod cross_spec_tests in generic_keccak.rs that compares each permutation step (theta, rho, pi, chi, iota, keccakf1600) and the simd::portable load_block / load_last / store_block helpers against the spec. Exposes generic_keccak::constants as pub(crate) for the test mod. Adds hacspec_sha3 as a [dev-dependencies] entry in the sha3 crate's Cargo.toml. Tests authored by Karthik Bhargavan. Claude (Opus 4.7) was used to review and test.
|
I ran One issue with extraction: Aeneas says The extracted Lean code cannot be compiled yet, mostly because of missing defs in core models: There is also one slightly more serious issue with Lean compilation: AeneasVerif/aeneas#984 So overall, I think these specs are suitable for |
| : t_Array v_T v_N | ||
| = Rust_primitives.Arrays.createi v_N f | ||
| "# | ||
| )] |
There was a problem hiding this comment.
We need to use createi instead of using array::from_fn directly for F*, right?
Maybe we could call it array_from_fn instead of createi? That would be more self-explanatory.
| pub fn absorb_rec(state: State, rate: usize, delim: u8, message: &[u8]) -> State { | ||
| if message.len() < rate { | ||
| absorb_final(state, message, 0, message.len(), rate, delim) | ||
| } else { | ||
| let state = absorb_block(state, &message[0..rate], rate); | ||
| absorb_rec(state, rate, delim, &message[rate..]) | ||
| } | ||
| } |
There was a problem hiding this comment.
In this form, a recursive function doesn't seem to be more useful for verification than a for-loop.
It would help if the recursive function would only call absorb_block, and leave the absorb_final call to be implemented in the absorb function below. Then we could use absorb_rec to write down a loop invariant on the implementation's for-loop, I think.
| let state = test_state(); | ||
| let mut impl_out = [0u8; 200]; | ||
| crate::simd::portable::store_block::<136>(&state, &mut impl_out, 0, 136); | ||
| let mut spec_out = [0u8; 200]; | ||
| spec_out = spec_sponge::squeeze_state(&state, spec_out, 0, 136); | ||
| assert_eq!(impl_out[..136], spec_out[..136]); |
There was a problem hiding this comment.
We can even assert assert_eq!(impl_out, spec_out);, can't we?
| assert_eq!( | ||
| impl_out[..len], | ||
| spec_out[..len], | ||
| "store_block mismatch at len={len}" | ||
| ); |
There was a problem hiding this comment.
Again, can't we test equality of the entire array?
| assert_eq!( | ||
| impl_out[offset..offset + len], | ||
| spec_out[offset..offset + len] | ||
| ); |
| } | ||
|
|
||
| // --------------------------------------------------------------------------- | ||
| // Path to the test vector files (shared with reference implementation) |
There was a problem hiding this comment.
When I read "reference implementation", I'd think of the hacspec version. So maybe better:
| // Path to the test vector files (shared with reference implementation) | |
| // Path to the test vector files (shared with implementation) |
|
Other than the small nitpicks above, this looks good! I haven't compared the hacspec implementation with the official FIPS spec, though. Let me know if I should do that. |
jschneider-bensch
added
the
waiting-on-review
specs/sha3: additions from libcrux-iot
3 participants
This PR adds a specification of SHA-3 in a purely functional subset of Rust (sometimes called hacspec).
The spec uses some specific proof-friendly styles.
The spec itself verifies in F* (
hax.sh extract; hax.sh prove) and is tested against the typical test vectors.We also added cross-spec tests to the SHA-3 implementation in libcrux, testing that the code matches the spec.
As a drive-by change, we aligned the array layout in the implementation state to match that of the specification state.
This eases all subsequent proofs.