Extraction error with `const` generics and hax attribute on a struct field

[ROMemories]

I'm hitting an error during F* extraction, when having a hax attribute on a struct field using a const generic.

Here is a reproducer (the actual attribute contents may not have much importance):

#[hax_lib::attributes]
struct Foo<const LEN: usize> {
    #[refine(hax_lib::forall(|i: usize| hax_lib::implies(
        i < indices.len(),
        || indices[i] as (usize) < 2
    )))]
    indices: [u8; LEN],
}

view in hax playground

The error message mentions error: [HAX0001] (FStar backend) something is not implemented yet. associated_refinement_in_type: zip two lists of different lenghts, but I can't clearly attribute this to the input Rust code.

If I move the const generic as a standalone const (e.g., const LEN: usize = 42;), F* extraction proceeds successfully. Likewise if I just comment out the hax attribute while keeping the const generic.

[W95Psp]

Thanks for your bug report! That's indeed a bug related to constants and struct refinements, I recall stumbling upon it quite some time ago.

From what I recall, the proc macro attributes sometimes remove const generics when it should not. I will try to investigate but I have no idea about when :/

[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.

[ROMemories]

This issue is still relevant.

[chrysn]

This is also relevant for use in lakers; there, we have a simpler example:

#[hax_lib::attributes]
struct Buffer<const N: usize> {
    data: [u8; N],
    #[refine(length < N)]
    length: usize,
}

Interestingly, I can work around it to some extent by having attributes and then on each function demanding from the caller that #[hax_lib::requires(self.len <= N)] -- but I don't know how far that'll get me.

[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.

[chrysn]

This is still a current issue.

[maximebuyse]

The reproducer can be adapted for current hax to:

#[hax_lib::attributes]
struct Foo<const LEN: usize> {
    #[hax_lib::refine(hax_lib::forall(|i: usize| hax_lib::implies(
        i < indices.len(),
        indices[i] as (usize) < 2
    )))]
    indices: [u8; LEN],
}

Open this code snippet in the playground