Attribute Macro attributes

#[attributes]

Enable the following attrubutes in the annotated item and sub-items.

refine (on a field in a struct)

Refine a type with a logical formula.

order (on a field in a struct or an enum)

Reorders a field in the extracted code.

Rust fields order matters for bit-level representation. Similarly, in some situations, fields order matters in the backends: for instance in F*, one may refine a field with a formula referring to a later field.

Those two orders may conflict. Adding #[hax_lib::order(n)] on a field with override its order at extraction time.

By default, the order of a field is its index, e.g. the first field has order 0, the i-th field has order i+1.

decreases, ensures and requires (on a fn in an impl)

decreases, ensures, requires: behave exactly as documented above on the proc attributes of the same name.

Example

#[hax_lib_macros::attributes]
mod foo {
    pub struct Hello {
        pub x: u32,
        #[refine(y > 3)]
        pub y: u32,
        #[refine(y + x + z > 3)]
        pub z: u32,
    }
    impl Hello {
        fn sum(&self) -> u32 {
            self.x + self.y + self.z
        }
        #[ensures(|result| result - n == self.sum())]
        fn plus(self, n: u32) -> u32 {
            self.sum() + n
        }
    }
}