Frontend: support nightly feature `generic_const_exprs`

[EschericHya]

Hello,

I was trying to run Charon on libcrux and got the following error:

error[E9999]: Supposely unreachable place in the Rust AST. The label is "TranslateUneval".
              This error report happend because some assumption about the Rust AST was broken.

              Context:
               - self: UnevaluatedConst { def: libcrux::kem::kyber::hash_functions::G::{constant#0}, args: [] }
               - ucv: UnevaluatedConst {
                  def: libcrux::kem::kyber::hash_functions::G::{constant#0},
                  args: [],
              }
  |
  = note: ⚠ This is a bug in Hax's frontend.
          Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!

The function is

pub(crate) fn G(input: &[u8]) -> [u8; digest_size(Algorithm::Sha3_512)] {
    digest::sha3_512(input)
}

from https://github.com/cryspen/libcrux/blob/a6286d7d5652264175cb1c2a184d8e00c169d463/src/kem/kyber/hash_functions.rs

The problem seems to happen because it cannot evaluate digest_size(Algorithm::Sha3_512).

[W95Psp]

Hi!

I think this is because the crate you're looking at uses the generic_const_exprs nightly feature, which is not yet supported by the frontend of hax.

(clearly digest_size(...) is nightly)

I'm gonna label correctly the issue, if this is needed for you we can schedule when to spend time on that. The faulty code is there: https://github.com/hacspec/hax/blob/b285b13ff2ca0a508c4f35c849a11612c3d1f2a4/frontend/exporter/src/constant_utils.rs#L375C37-L378.

We should

• [ ] make the error better, and/or
• [ ] support for constants.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.