Cannot access previous struct fields in `refine` attributes

ROMemories commented 2 months ago

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 commented 1 week ago

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

W95Psp commented 1 week ago

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.

hacspec / hax