F* term ordering issue with hax attribute

[ROMemories]

It seems to me that F* terms are not issued in the right order in some cases involving hax attributes.

For instance, the following Rust snippet

const FOO_LEN: usize = 42;

#[hax_lib::attributes]
struct Foo {
    #[refine(foo < FOO_LEN)]
    foo: usize,
}

view in hax playground

results in the following F*:

type t_Foo = {
  f_foo:f_foo: usize{f_foo <. v_FOO_LEN}
}

let v_FOO_LEN: usize = sz 42

As the declaration of FOO_LEN gets issued after its use, lax checking fails with the following error:

* Error 72 at Playground.fst(7,30-7,39):
  - Identifier not found: [v_FOO_LEN]

My understanding is that there is already a dependency detection mechanism inside the engine (in engine/lib/dependencies.ml I think) where dependencies between items are modeled as graph vertices, which then allows backends to issue terms in topological order (I believe some of it happens in engine/backends/fstar/fstar_backend.ml but I am not sure where/how these vertices are inserted into the graph).

Is my understanding correct? Could you quickly explain where these vertices are inserted?

I suppose that dependencies resulting from hax attributes are not currently modeled in that graph, hence why these terms do not get issued in the correct order.

[franziskuskiefer]

@W95Psp can you give an update on this? Also, this may be more of a discussion rather than an issue.

[ROMemories]

Also, this may be more of a discussion rather than an issue.

Why? Lax checking fails on a snippet of code that seems totally reasonable; looks to me like in the bug in the order in which F* terms are issued by the backend.

[W95Psp]

Sorry for the late reply.

I investigated a bit just now. Indeed, there is a dependency detection mechanism in the engine.

How attributes work

The hax-specific Rust attributes most of the case desugars to items tagged with a UUID, linking e.g. the refinement on a field and a field in a struct.

Why do you get this bug

This UUID relation is taken into account by the dependency analysis, but only for proper items: in your snippet, the UUID relation implies an item and a struct field.

So that's the bug here: the dependency analysis not taking in account this relation between your predicate foo < FOO_LEN and the item foo.

How to fix it

To fix this issue, I think we need to collect all the attributes of an item instead of just using the shallow attributes that exist on the item itself.

How things are inserted in the graph?

Concerning your other question about the dependency analysis in general, everything takes place in dependencies.ml, and the ordering takes place just after importing the items, here: https://github.com/hacspec/hax/blob/4291b195f4dee2bec5568ee6a0b6fe6a108623fb/engine/bin/lib.ml#L76.

The backends can use the dependency analysis, but by default, they get items in a topological order.

A vertice exists between an item f and g whenever:

1. the name g occurs somewhere in the definition of f, or
2. when both the item f and g have a direct UUID relationship (i.e. a direct, top-level attribute on them)

(again, here (2) is forgetting some relations, basically)

Is that helping? Also, I agree, that's a bug. I'll try to find time to patch this, it should be fairly easy to fix.