Repository: cryspen/hax (language: rust)

Issue:
F* term ordering issue with hax attribute
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

```rust
const FOO_LEN: usize = 42;

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

[view in hax playground](https://hax-playground.cryspen.com/#fstar/e793beee0a/gist=19113ac424b694d69c1fded7e405a2a2)

results in the following F*:

```fstar
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](https://github.com/hacspec/hax/blob/e793beee0acf5a573ef9820c1e473ebd4a69c06b/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](https://github.com/hacspec/hax/blob/main/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.


Discussion / hints:
@W95Psp can you give an update on this? Also, this may be more of a discussion rather than an issue.
> 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.
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.
@W95Psp @franziskuskiefer any news on this? We are starting to make plans for 2025 and we'd love to have hax back in CI, and on our roadmap for our spring release!

Fix patch:
diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index 2aa8b2956..c93339617 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -655,6 +655,13 @@ module Make (F : Features.T) = struct
               self#zero
           | _ -> super#visit_expr' () e
       end
+
+    let collect_attrs =
+      object (_self)
+        inherit [_] Visitors.reduce
+        inherit [_] expr_list_monoid
+        method! visit_attrs () attrs = attrs
+      end
   end
 
   (** Produces a local identifier which is locally fresh **with respect
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
index 6637e60c8..46a32f42b 100644
--- a/engine/lib/dependencies.ml
+++ b/engine/lib/dependencies.ml
@@ -88,8 +88,9 @@ module Make (F : Features.T) = struct
         =
       List.concat_map
         ~f:(fun i ->
+          let attrs = U.Reducers.collect_attrs#visit_item () i in
           let assoc =
-            uid_associated_items i.attrs |> List.map ~f:(fun i -> i.ident)
+            uid_associated_items attrs |> List.map ~f:(fun i -> i.ident)
           in
           vertices_of_item i @ assoc |> List.map ~f:(Fn.const i.ident &&& Fn.id))
         items


Test patch:
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index f52788a03..8705e5981 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
@@ -130,12 +130,12 @@ module Attributes.Newtype_pattern
 open Core
 open FStar.Mul
 
+let v_MAX: usize = sz 10
+
 type t_SafeIndex = { f_i:f_i: usize{f_i <. v_MAX} }
 
 let impl__SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i
 
-let v_MAX: usize = sz 10
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
   {
@@ -156,6 +156,23 @@ module Attributes.Pre_post_on_traits_and_impls
 open Core
 open FStar.Mul
 
+type t_ViaAdd = | ViaAdd : t_ViaAdd
+
+type t_ViaMul = | ViaMul : t_ViaMul
+
+class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
+  f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. 100uy ==> pred};
+  f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. 88uy};
+  f_method:x0: v_Self -> x1: u8
+    -> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result)
+}
+
+let test
+      (#v_T: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_TraitWithRequiresAndEnsures v_T)
+      (x: v_T)
+    : u8 = (f_method #v_T #FStar.Tactics.Typeclasses.solve x 99uy <: u8) -! 88uy
+
 class t_Operation (v_Self: Type0) = {
   f_double_pre:x: u8
     -> pred:
@@ -174,17 +191,6 @@ class t_Operation (v_Self: Type0) = {
   f_double:x0: u8 -> Prims.Pure u8 (f_double_pre x0) (fun result -> f_double_post x0 result)
 }
 
-class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
-  f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. 100uy ==> pred};
-  f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. 88uy};
-  f_method:x0: v_Self -> x1: u8
-    -> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result)
-}
-
-type t_ViaAdd = | ViaAdd : t_ViaAdd
-
-type t_ViaMul = | ViaMul : t_ViaMul
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl: t_Operation t_ViaAdd =
   {
@@ -218,12 +224,6 @@ let impl_1: t_Operation t_ViaMul =
         (Rust_primitives.Hax.Int.from_machine result <: Hax_lib.Int.t_Int));
     f_double = fun (x: u8) -> x *! 2uy
   }
-
-let test
-      (#v_T: Type0)
-      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_TraitWithRequiresAndEnsures v_T)
-      (x: v_T)
-    : u8 = (f_method #v_T #FStar.Tactics.Typeclasses.solve x 99uy <: u8) -! 88uy
 '''
 "Attributes.Refined_arithmetic.fst" = '''
 module Attributes.Refined_arithmetic
@@ -466,12 +466,6 @@ module Attributes
 open Core
 open FStar.Mul
 
-type t_Foo = {
-  f_x:u32;
-  f_y:f_y: u32{f_y >. 3ul};
-  f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
-}
-
 let inlined_code__V: u8 = 12uy
 
 let issue_844_ (v__x: u8)
@@ -484,6 +478,12 @@ let issue_844_ (v__x: u8)
 
 let u32_max: u32 = 90000ul
 
+type t_Foo = {
+  f_x:u32;
+  f_y:f_y: u32{f_y >. 3ul};
+  f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
+}
+
 let swap_and_mut_req_ens (x y: u32)
     : Prims.Pure (u32 & u32 & u32)
       (requires x <. 40ul && y <. 300ul)