Add full type check for SHA3 portable by parrot7483 · Pull Request #1157 · cryspen/libcrux

parrot7483 · 2025-09-18T11:00:19Z

This PR adds full type checking for the SHA3 portable version for #395

Extract using hax.py extract --portable, prove using hax.py prove.

Besides prove code the following things where changed:

reorder functions in libcrux-sha3/src/generic_keccak/xof.rs
The absorb_full function in libcrux-sha3/src/generic_keccak/xof.rs previously did not always consume the internal buffer when it was full. This state could only be reached by misusing the API. The only bug I found.
split up the rho and pi function for verification purpose

This version contains a few things I would consider "hacks"

The extraction for the squeeze does not work. We add the expected F* code using hax_lib::fstar::replace
impl From<u32> for Algorithm does not work because of the panic.
In libcrux-sha3/src/generic_keccak/xof.rs the #[hax_lib::fstar::options("...")] has no effect. I use an hax_lib::fstar::before instead

crates/algorithms/sha3/src/generic_keccak.rs

crates/algorithms/sha3/src/generic_keccak/xof.rs

franziskuskiefer

Sorry for being a little slow on this.
Here a couple first comments. Can you address them and update? Then we can do another round.

.github/workflows/sha3-hax.yml

libcrux-sha3/src/generic_keccak/portable.rs

libcrux-sha3/src/generic_keccak/xof.rs

franziskuskiefer · 2025-09-22T18:51:32Z

libcrux-sha3/src/generic_keccak/xof.rs

This requires the unconditional hax_lib dependency for debug builds. Is there a better way to do this?

I don't think I understand this correctly. Would putting a cfg(hax) be enough? It is only needed for proof.

libcrux-sha3/src/generic_keccak/xof.rs

crates/algorithms/sha3/src/generic_keccak/xof.rs

parrot7483 · 2025-11-12T12:14:41Z

@franziskuskiefer I applied your feedback and also cherry-picked one commit from my AVX/NEON branch adding the correct precondition on the traits and doing some light refactoring (mainly having consistent names for variables).

franziskuskiefer

Thanks, looks pretty good. A couple things and some cleanup, then this can go in.

.github/workflows/sha3-hax.yml

crates/algorithms/sha3/src/generic_keccak/xof.rs

crates/algorithms/sha3/src/lib.rs

franziskuskiefer · 2025-11-13T11:48:28Z

libcrux-sha3/src/simd/portable.rs

Are these changes needed for the proof? If yes, they'd need some explanation to why. If not, we should keep it as is.
Same for the similar change below.

Yes, if I inline everything F* can't figure out that the bounds are correct every time. Sometimes it works sometimes it doesn't.

I think inlining let bytes = get_ij(s, octets / 5, octets % 5).to_le_bytes() should be possible.

crates/algorithms/sha3/src/generic_keccak.rs

crates/algorithms/sha3/src/generic_keccak/xof.rs

franziskuskiefer · 2025-11-13T12:08:23Z

crates/algorithms/sha3/src/traits.rs

 "
 )]
-pub(crate) trait Squeeze1<T: KeccakItem<1>> {
+#[hax_lib::attributes]
+pub(crate) trait Squeeze<T: KeccakItem<1>> {


Why did this lose the 1?

I want to emphasize that having the Squeeze trait multiple times is because of HAX not supporting &[&mut [u8]; N] or other types with mutables inside. If that would work that would simplify a lot of things in this crate. I will write a comment explaining it.

libcrux-sha3/src/generic_keccak/xof.rs

crates/algorithms/sha3/src/simd/portable.rs

parrot7483 · 2025-11-19T14:32:20Z

@franziskuskiefer I applied your review. cherry-picked 1064d0d from SIMD branch. Merged main.

Review re-requested

parrot7483 · 2025-11-19T15:13:59Z

I have a tendency to pressing these big green buttons on github messing everything up. sorry.

parrot7483 · 2026-01-21T20:19:03Z

What do you want to do about these warnings?

warning: unused attribute
   --> crates/algorithms/sha3/src/lib.rs:181:1
    |
181 | #[inline(always)]
    | ^^^^^^^^^^^^^^^^^ help: remove this attribute
    |
note: attribute also specified here
   --> crates/algorithms/sha3/src/lib.rs:176:1
    |
176 | #[cfg_attr(not(eurydice), inline(always))]
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!`

parrot7483 · 2026-01-21T21:03:25Z

F* proofs failing with "Namespace 'Core' cannot be found" after core-models directory moved

Reproducer:

cd libcrux-ml-kem && ./hax.py extract && ./hax.py prove
cd crates/algorithms/sha3 && ./hax.py extract && ./hax.py prove

Both fail at prove step with same error. ML-KEM and SHA3 both have this issue.

Using the old name "Core_models" still works for single models.

parrot7483 · 2026-02-03T17:01:20Z

The auto-discovery in Makefile.generic doesn't find the Core F* library from the hax proof-libs, so I had to set HAX_HOME explicitly, which doesn't work in CI.

Fix F* Makefile include paths. Work around hax from_fn extraction bug: Add helper function with fstar::replace to fix incorrect type parameter extraction. See: cryspen/hax#1920.

franziskuskiefer

lgtm with those nits addressed

franziskuskiefer · 2026-02-04T12:16:44Z

crates/algorithms/sha3/src/traits.rs

+    interface, "
+class t_Squeeze (v_Self: Type0) (v_T: Type0) = {
+  // TODO: This super variable is problematic and makes typecheck fail
+  // https://github.com/cryspen/hax/issues/1554


Looks like that issue is closed and if it works without the commented code, let's drop it.

still a problem. I reopened the issue

franziskuskiefer · 2026-02-04T12:17:00Z

crates/algorithms/sha3/src/traits.rs

 }
+
+// TODO: See above
+// [@@ FStar.Tactics.Typeclasses.tcinstance]


Same here, let's remove when it's not used.

franziskuskiefer · 2026-02-04T12:32:07Z

What do you want to do about these warnings?

that should be fixed in a separate PR

jschneider-bensch · 2026-02-04T13:45:54Z

crates/algorithms/sha3/hax.py

            env=hax_env,
        )

+        # Extract Core models


From the output of ./hax.py extract --portable it looks like nothing is extracted here actually, and you also removed the core-models proof directory from FSTAR_INCLUDE_DIRS_EXTRA in the Makefile. So is this extraction step needed here, after all?

I am not sure. I am confused about the difference between Core and Core_models

jschneider-bensch · 2026-02-04T14:03:01Z

crates/algorithms/sha3/src/generic_keccak/portable.rs

Is it possible to avoid this manual F* dependency by making the lemmas in proof_utils::lemmas into Rust functions (nops which are replaced as they are now) and calling these from Rust instead of invoking them in inline fstar! blocks?

jschneider-bensch · 2026-02-04T14:08:01Z

crates/algorithms/sha3/src/generic_keccak/xof.rs

@@ -1,8 +1,25 @@
+use hax_lib::int::*;


This should be behind a #[cfg(hax)], no?

jschneider-bensch · 2026-02-04T14:09:07Z

crates/algorithms/sha3/src/generic_keccak/xof.rs

Same question about avoiding the manual F* open as in generic_keccak::portable.

jschneider-bensch · 2026-02-04T14:15:30Z

crates/algorithms/sha3/src/generic_keccak/xof.rs

Could you move it to proof_utils and pass in xof.buf_len from here instead of passing in xof and accessing it in the invariant body?

parrot7483 · 2026-02-10T18:43:01Z

@jschneider-bensch Does buf_len need to remain private, or is pub(crate) acceptable? I made it pub(crate) so portable.rs can access it when calling keccak_xof_state_inv in the trait implementations.

parrot7483 · 2026-02-16T14:53:30Z

@jschneider-bensch friendly ping

jschneider-bensch · 2026-02-17T14:17:49Z

@jschneider-bensch Does buf_len need to remain private, or is pub(crate) acceptable? I made it pub(crate) so portable.rs can access it when calling keccak_xof_state_inv in the trait implementations.

Sorry for the late reply!
I think having it pub(crate) is okay.

parrot7483 · 2026-02-17T18:26:11Z

Can we merge then?

parrot7483 force-pushed the Parrot7483/sha3-type-check branch from 8f7a614 to 223bcaf Compare September 18, 2025 11:07

parrot7483 commented Sep 18, 2025

View reviewed changes

crates/algorithms/sha3/src/generic_keccak.rs Show resolved Hide resolved

parrot7483 requested review from franziskuskiefer and karthikbhargavan September 18, 2025 11:49

parrot7483 marked this pull request as ready for review September 18, 2025 11:50

parrot7483 requested review from a team as code owners September 18, 2025 11:50

parrot7483 commented Sep 18, 2025

View reviewed changes

crates/algorithms/sha3/src/generic_keccak/xof.rs Outdated Show resolved Hide resolved

W95Psp mentioned this pull request Sep 22, 2025

Support all hax lib annotations on inherent impl blocks cryspen/hax#1698

Open

franziskuskiefer assigned parrot7483 Sep 22, 2025

franziskuskiefer reviewed Nov 1, 2025

View reviewed changes

parrot7483 requested a review from franziskuskiefer November 12, 2025 12:14

franziskuskiefer previously requested changes Nov 13, 2025

View reviewed changes

parrot7483 commented Nov 19, 2025

View reviewed changes

crates/algorithms/sha3/src/simd/portable.rs Show resolved Hide resolved

parrot7483 requested a review from franziskuskiefer November 19, 2025 14:32

parrot7483 force-pushed the Parrot7483/sha3-type-check branch from fb88708 to 153b003 Compare November 19, 2025 15:12

franziskuskiefer added the keep-open label Jan 15, 2026

jschneider-bensch added the waiting-on-author Status: This is awaiting some action from the author. label Jan 20, 2026

parrot7483 force-pushed the Parrot7483/sha3-type-check branch from 589ff18 to 14e49e7 Compare January 21, 2026 20:15

parrot7483 added 5 commits February 3, 2026 14:50

Add full type check for SHA3 portable

3ced362

apply feedback from franziskuskiefer

78a62c7

light refactor and correct trait preconditions

22cb4b0

Extract Core Models on build and Fix portable extraction

713cde3

apply feedback from franziskuskiefer 2

1e9d43c

parrot7483 added 2 commits February 3, 2026 14:50

revert auto lib.rs changes

7d575f6

sha3: Fix F* extraction paths for type checking

2c33cb9

parrot7483 force-pushed the Parrot7483/sha3-type-check branch from 14e49e7 to 2c33cb9 Compare February 3, 2026 16:19

parrot7483 added 4 commits February 4, 2026 09:51

sha3: fix CI and use Makefile.basic

ced16a5

fix(sha3):

c66d2fc

Fix F* Makefile include paths. Work around hax from_fn extraction bug: Add helper function with fstar::replace to fix incorrect type parameter extraction. See: cryspen/hax#1920.

fix(sha3): Fix typo in comment

360389e

refactor(sha3): Remove lemma.rs (moved to proof_utils)

0144a6c

franziskuskiefer reviewed Feb 4, 2026

View reviewed changes

parrot7483 requested a review from franziskuskiefer February 4, 2026 12:46

jschneider-bensch reviewed Feb 4, 2026

View reviewed changes

apply feedback from jschneider-bensch

6e58f40

parrot7483 requested review from jschneider-bensch and removed request for karthikbhargavan February 10, 2026 19:12

Conversation

parrot7483 commented Sep 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

franziskuskiefer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

parrot7483 commented Nov 12, 2025

Uh oh!

franziskuskiefer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

parrot7483 commented Nov 19, 2025

Uh oh!

parrot7483 commented Nov 19, 2025

Uh oh!

parrot7483 commented Jan 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

parrot7483 commented Jan 21, 2026

Uh oh!

parrot7483 commented Feb 3, 2026

Uh oh!

franziskuskiefer left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

franziskuskiefer commented Feb 4, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

parrot7483 commented Sep 18, 2025 •

edited

Loading

parrot7483 commented Jan 21, 2026 •

edited

Loading

parrot7483 commented Feb 17, 2026 •

edited

Loading