fix: fix hax compilation of libcrux-hmac

[asraa]

Fixes #1641

This fixes the hax configuration build for hmac by exporting the sha3 types

[skip changelog]

[jschneider-bensch]

Thanks for filing!
It looks like the approach here does not work at the moment, because you can't apply the hax_lib::exclude macro on a file-based module:

error[E0658]: file modules in proc macro input are unstable
  --> crates/algorithms/sha3/src/lib.rs:15:1
   |
15 | mod impl_digest_trait;
   | ^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: see issue #54727 <https://github.com/rust-lang/rust/issues/54727> for more information
   = help: add `#![feature(proc_macro_hygiene)]` to the crate attributes to enable
   = note: this compiler was built on 2025-11-07; consider upgrading it if it is out of date

For more information about this error, try `rustc --explain E0658`.

ERROR rustc emitted an error, aborting hax custom driver.
error: could not compile `libcrux-sha3` (lib) due to 1 previous error

Would it resolve your issue if we #[cfg_attr(hax, hax_lib::exclude)]'ed the four impl_hash_traits! invocations in the impl_digest_trait module?

[asraa]

Ah thank you! Regrettably i only compiled with code with cfg hax and didn't run extraction, and now see that that was an issue.

Would it resolve your issue if we #[cfg_attr(hax, hax_lib::exclude)]'ed the four impl_hash_traits! invocations in the impl_digest_trait module?

That would also work. Do you have a preference on me excluding the length constants too? If so I'll remove the macro and add excludes in impl_digest_trait

[jschneider-bensch]

No worries!
I think we mainly want to avoid the trait impls in the extraction because they have mutability patterns that have historically often been an issue for hax, and probably we also don't want the Sha3_... structs in there. The const items shouldn't affect negatively any extraction (I hope), so there's no need to exclude them. So I'd be fine with excluding the impl_hash_traits invocations.

[asraa]

Rebased & updated!

[jschneider-bensch]

Thank you!

[asraa]

Awesome, thanks! If we could have a patch release for the hmac crate when convenient that would be great!

And to prevent our proof validation in the future, would it be possible to add hax extract / prove CI check for the hmac crate too? I can give it a stab