Expressing invariant of a an array used to index into another array

[ROMemories]

The following invariant (1) seems to correctly allow hax to verify that values of the indices array can always be used to index into the foo array, in the context of the f function below:

const LEN: usize = 2;
const FOO_LEN: usize = 3;
const SENTINEL: u8 = 0xff;

#[hax_lib::attributes]
struct Foo {
    foo: [u8; FOO_LEN],
    // (1) Enforce that all values of `indices` can be used for indexing `foo`
    #[refine(hax_lib::forall(|i: usize| hax_lib::implies(
        i < indices.len(),
        || indices[i] == SENTINEL || indices[i] as (usize) < FOO_LEN
    )))]
    indices: [u8; LEN],
}

#[hax_lib::attributes]
impl Foo {
    fn new() -> Self {
        Self {
            foo: [42, 43, 44],
            indices: [0, SENTINEL],
        }
    }

    // Invariant (1) required for the following function:
    #[requires(i < LEN)]
    fn f(&self, i: usize) -> Option<u8> {
        if self.indices[i] != SENTINEL {
            Some(self.foo[self.indices[i] as usize])
        } else {
            None
        }
    }
}

view in hax playground

Is there a better/shorter/cleaner way of expressing this invariant, maybe without relying on forall + implies?

Would there be a simpler way if we didn't have sentinel values in that indices array?

That same invariant may prove useful in other functions so I think it is best to express that invariant on the struct field rather than on the f function directly (i.e., express it as a refined type "globally" instead of a function precondition).

[W95Psp]

Hi!

Indeed, here, the invariant is a bit verbose.
Instead of having the invariant on the level of the struct Foo, I think that here, putting the invariant on the items of the array would be nicer.

hax provides a way of creating newtype-style refinement types: here you want to have a wrapper around u8 that guarantees the property you need.

You probably wants something like the following:
https://hax-playground.cryspen.com/#fstar/latest-main/gist=9a358635fb2712c9484c3f99effdc99a

We should document that better however. It is documented in the library here: https://hacspec.org/hax/frontend/hax_lib/attr.refinement_type.html, but we should have a chapter in the book that describes that.

Do you think that it's what you need?

[ROMemories]

hax provides a way of creating newtype-style refinement types: here you want to have a wrapper around u8 that guarantees the property you need.

Yes I did find that in the docs, and that's definitely the way we're going to go in the future. Currently the goal was to first add annotations to prove panic-freedom, before refactoring in a second stage in a more idiomatic way.

we should have a chapter in the book that describes that

👍