Cannot access previous struct fields in `refine` attributes

[ROMemories]

It seems that the refine attribute does not allow referring to struct fields defined before the field on which the attribute is applied on.

For instance, F* extraction fails on the following example:

const FOO_LEN: usize = 3;
const BAR_LEN: usize = 5;
const SENTINEL: u8 = 0xff;

#[hax_lib::attributes]
struct Foo {
    // Values indexed by `bar` values cannot be the sentinel value.
    #[refine(hax_lib::forall(|i: usize| hax_lib::implies(
        i < foo.len(),
        || bar[foo[i] as usize] != SENTINEL
    )))]
    bar: [u8; BAR_LEN],

    // All values can be used to index into `bar`.
    #[refine(hax_lib::forall(|i: usize| hax_lib::implies(
        i < foo.len(),
        || foo[i] as (usize) < BAR_LEN
    )))]
    foo: [u8; FOO_LEN],
}

view in hax playground

The first error message being:

error[E0425]: cannot find value `foo` in this scope
 --> src/lib.rs:9:13
  |
9 |         i < foo.len(),
  |             ^^^ not found in this scope

However, this example does extract (and verify) properly when swapping the struct fields in the struct definition.

This is an issue as the order of struct fields is significant in Rust (and thus cannot be reordered without a change in meaning), and because accessing fields defined before is required when introducing interdependent refine attributes on multiple fields.

Is there a way to work around this for now?

[emmanuelsearch]

@franziskuskiefer is there any news on that front? w.r.t. RIOT-rs CI integration ;)

[W95Psp]

Sorry, I missed this issue somehow.

Indeed, the refinements on the fields have an order constraint: in F*, having a refinement on a field that mentions another field that comes later will yield an error.

Workaround A

Here, a workaround would be to move the refinement of bar to the one of foo. It is a bit unidiomatic, but will work.

https://hax-playground.cryspen.com/#fstar/63432cffd5/gist=3b5cc5a8b290273de7a76a0887900e78

Sadly, we run into https://github.com/hacspec/hax/issues/1016 here.

Workaround B

You could remove the invariants from Foo, and have a new wrapper type that ensure properties on Foo, using the refinement types: https://docs.rs/hax-lib/0.1.0-alpha.1/hax_lib/attr.refinement_type.html

This is probably not very nice to use in your case. Workaround A is better I think.

Long-Term Solution

Currently the attributes macro translates your struct into (I used just expand):

const FOO_LEN: usize = 3;
const BAR_LEN: usize = 5;
const SENTINEL: u8 = 0xff;
#[cfg(hax_compilation)]
#[_hax::json("{\"ItemStatus\":{\"Included\":{\"late_skip\":true}}}")]
const _: () = {
    #[_hax::json("{\"Uid\":{\"uid\":\"d88c7bfc8fe54f2f8fb4892e30f37129\"}}")]
    #[_hax::json("{\"ItemStatus\":{\"Included\":{\"late_skip\":true}}}")]
    fn refinement(bar: [u8; BAR_LEN]) -> bool {
        hax_lib::forall(|i: usize| hax_lib::implies(
            i < foo.len(),
            || bar[foo[i] as usize] != SENTINEL,
        ))
    }
};
#[cfg(hax_compilation)]
#[_hax::json("{\"ItemStatus\":{\"Included\":{\"late_skip\":true}}}")]
const _: () = {
    #[_hax::json("{\"Uid\":{\"uid\":\"37fd0c5f65e84068828865bcc999c1e4\"}}")]
    #[_hax::json("{\"ItemStatus\":{\"Included\":{\"late_skip\":true}}}")]
    fn refinement(bar: [u8; BAR_LEN], foo: [u8; FOO_LEN]) -> bool {
        hax_lib::forall(|i: usize| hax_lib::implies(
            i < foo.len(),
            || (foo[i] as (usize)) < BAR_LEN,
        ))
    }
};
struct Foo {
    #[_hax::json(
        "{\"AssociatedItem\":{\"role\":\"Refine\",\"item\":{\"uid\":\"d88c7bfc8fe54f2f8fb4892e30f37129\"}}}"
    )]
    bar: [u8; BAR_LEN],
    #[_hax::json(
        "{\"AssociatedItem\":{\"role\":\"Refine\",\"item\":{\"uid\":\"37fd0c5f65e84068828865bcc999c1e4\"}}}"
    )]
    foo: [u8; FOO_LEN],
}

The arguments to the generated refinements functions contains only "visible" fields. We could change that to allow refering to any field, but erroring out if a cycle is detected: if both the invariant on foo mentions bar and the invariant of bar mentions foo, then we get invalid F* refinements, and the refinements should be written differently.

[franziskuskiefer]

@emmanuelsearch Does one of the workaround work for you?

[ROMemories]

Workaround A should work now that cryspen/hax#1016 is fixed. However I think the original limitation is still there so I'm not sure whether this issue can be closed.

We're currently preparing for a release but should be able to get back to this in a few weeks.

[W95Psp]

I'm taking a look at that right now.

My strategy is:

• cryspen/hax-evit#34
• cryspen/hax-evit#35

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

[maximebuyse]

hax_lib::order was introduced to fix this (with manual annotation), but apparently it doesn't work as intended:

const FOO_LEN: usize = 3;
const BAR_LEN: usize = 5;
const SENTINEL: u8 = 0xff;

#[hax_lib::attributes]
struct Foo {
    // Values indexed by `bar` values cannot be the sentinel value.
    #[hax_lib::order(1)]
    #[refine(hax_lib::forall(|i: usize| hax_lib::implies(
        i < foo.len(),
        bar[foo[i] as usize] != SENTINEL
    )))]
    bar: [u8; BAR_LEN],

    // All values can be used to index into `bar`.
    #[hax_lib::order(2)]
    #[refine(hax_lib::forall(|i: usize| hax_lib::implies(
        i < foo.len(),
        || foo[i] as (usize) < BAR_LEN
    )))]
    foo: [u8; FOO_LEN],
}

Open this code snippet in the playground

github.com/cryspen/hax-evit/pull/32 is where this was implemented but reordering happens only in the produced F* and not in Rust which does not fix the issue described here. Maybe the macro should allow access to all fields.