Stable topological sort using original order.

[maximebuyse]

Fixes #771

See #1151 (comment) for more context. The implementation of this PR:

• Maps the items dependency graph to one where vertices carry the index of each item in the items list (sorted by position in the user input)
• uses ocamlgraph stable topological sort to produce an ordering that respects the dependency relation and tries to respect the original order as much as possible
• Modifies this to make sure mutually recursive items are next to one another

[maximebuyse]

Libcrux CI job using this hax branch: https://github.com/cryspen/libcrux/actions/runs/12866379703/job/35868825565

[maximebuyse]

Libcrux CI job using this hax branch: https://github.com/cryspen/libcrux/actions/runs/12866379703/job/35868825565

This one failed because of a fstar::before, new job after moving it: https://github.com/cryspen/libcrux/actions/runs/12867238262/job/35871445523

[W95Psp]

Thanks, that looks good!
I only have a few nits :)

[W95Psp]

@maximebuyse I'm adding your PR to the merge queue
Please remove from queue if something is not ready :)

[karthikbhargavan]

has this been tested on libcrux?

[maximebuyse]

has this been tested on libcrux?

Yes, this works with this libcrux PR: cryspen/libcrux#759
Note that both PRs need each other which means we have to merge one with failed CI and then the other. Or find a way to place this fstar::before in a place that works with both orderings (main and this PR)

[maximebuyse]

I was surprised that we needed cryspen/libcrux#759 in libcrux because it was caused by the first item in a file being moved lower in the file with no apparent dependency justifying the move. The reason is that we are working with the global order of items across all modules. So there can be a situation like this:

Module a has two items f (depends on b::h) and g (in this order), module b has an item h.
The original order is and because of the dependency the stable topological global order we get is: a::g, b::h, a::f.
This means that if you look at module a, we swap f and g while we could just let them in their original order.
The solution for this is to do the sorting module by module. Ideally we would change the API of backends, giving them a set (or map) of sorted lists of items (modules). But for now we can keep the API, remove the sorting that happens before the backends, and call the sort on each module from the backends.

[maximebuyse]

I was surprised that we needed cryspen/libcrux#759 in libcrux because it was caused by the first item in a file being moved lower in the file with no apparent dependency justifying the move. The reason is that we are working with the global order of items across all modules. So there can be a situation like this:

Module a has two items f (depends on b::h) and g (in this order), module b has an item h. The original order is and because of the dependency the stable topological global order we get is: a::g, b::h, a::f. This means that if you look at module a, we swap f and g while we could just let them in their original order. The solution for this is to do the sorting module by module. Ideally we would change the API of backends, giving them a set (or map) of sorted lists of items (modules). But for now we can keep the API, remove the sorting that happens before the backends, and call the sort on each module from the backends.

I moved the sort to the backends to make it module-wise. This required a few additional changes:

• Fixing Crash with hax_lib::fstar::before in recursive bundle #1177 (This probably needs a better solution in Engine: rework global name representation #1199)
• Replacing Quote items before or after their item of reference when needed (they can be moved by the sorting, this was not a problem before as these items where inserted at the right spot, after sorting)

I started https://github.com/cryspen/libcrux/actions/runs/12891137700/job/35942373454 to test it on libcrux (main branch as it should now work!)

[maximebuyse]

I was surprised that we needed cryspen/libcrux#759 in libcrux because it was caused by the first item in a file being moved lower in the file with no apparent dependency justifying the move. The reason is that we are working with the global order of items across all modules. So there can be a situation like this:
Module a has two items f (depends on b::h) and g (in this order), module b has an item h. The original order is and because of the dependency the stable topological global order we get is: a::g, b::h, a::f. This means that if you look at module a, we swap f and g while we could just let them in their original order. The solution for this is to do the sorting module by module. Ideally we would change the API of backends, giving them a set (or map) of sorted lists of items (modules). But for now we can keep the API, remove the sorting that happens before the backends, and call the sort on each module from the backends.

I moved the sort to the backends to make it module-wise. This required a few additional changes:

* Fixing [Crash with `hax_lib::fstar::before` in recursive bundle #1177](https://github.com/cryspen/hax/issues/1177) (This probably needs a better solution in [Engine: rework global name representation #1199](https://github.com/cryspen/hax/pull/1199))

* Replacing `Quote` items before or after their item of reference when needed (they can be moved by the sorting, this was not a problem before as these items where inserted at the right spot, after sorting)

I started https://github.com/cryspen/libcrux/actions/runs/12891137700/job/35942373454 to test it on libcrux (main branch as it should now work!)

Unfortunately there are more bugs:

• The dependencies introduced by pre/post conditions are ignored (because the items of pre/post) are erased (late skip). This could be solved by sorting before erasing (but that means sorting before the backends...). A good way to do this could be to first sort compute a topological order on modules/namespaces, then order items inside each module and make a global order out of those two orders. This would work both for backends that flatten everything and for backends that have modules
• There is a crash in the libcrux job that I haven't investigated yet

[maximebuyse]

I was surprised that we needed cryspen/libcrux#759 in libcrux because it was caused by the first item in a file being moved lower in the file with no apparent dependency justifying the move. The reason is that we are working with the global order of items across all modules. So there can be a situation like this:
Module a has two items f (depends on b::h) and g (in this order), module b has an item h. The original order is and because of the dependency the stable topological global order we get is: a::g, b::h, a::f. This means that if you look at module a, we swap f and g while we could just let them in their original order. The solution for this is to do the sorting module by module. Ideally we would change the API of backends, giving them a set (or map) of sorted lists of items (modules). But for now we can keep the API, remove the sorting that happens before the backends, and call the sort on each module from the backends.

I moved the sort to the backends to make it module-wise. This required a few additional changes:

* Fixing [Crash with `hax_lib::fstar::before` in recursive bundle #1177](https://github.com/cryspen/hax/issues/1177) (This probably needs a better solution in [Engine: rework global name representation #1199](https://github.com/cryspen/hax/pull/1199))

* Replacing `Quote` items before or after their item of reference when needed (they can be moved by the sorting, this was not a problem before as these items where inserted at the right spot, after sorting)

I started https://github.com/cryspen/libcrux/actions/runs/12891137700/job/35942373454 to test it on libcrux (main branch as it should now work!)

Unfortunately there are more bugs:

* The dependencies introduced by pre/post conditions are ignored (because the items of pre/post) are erased (late skip). This could be solved by sorting before erasing (but that means sorting before the backends...). A good way to do this could be to first sort compute a topological order on modules/namespaces, then order items inside each module and make a global order out of those two orders. This would work both for backends that flatten everything and for backends that have modules

* There is a crash in the libcrux job that I haven't investigated yet

I implemented a new version running before late_skip (maybe it could even be a phase). I also fixed a few crashes due to new name clashes with Quote items. It seems to work well. Let's wait and see if libcrux succeeds: https://github.com/cryspen/libcrux/actions/runs/12908277957/job/35993474305

[maximebuyse]

If several hax_lib::fstar::after are attached to the same item, the order in which they are added to the F* is reversed compared to the previous behaviour. Libcrux relies on this order, so I changed in the libcrux source, let's see if this fixes CI: https://github.com/cryspen/libcrux/actions/runs/12910250039/job/35999838533

Example:

#[hax_lib::fstar::after("let x = ()")]
#[hax_lib::fstar::after("let y = ()")]
fn f() {}

Open this code snippet in the playground

The generated F* without this PR is:

let f (_: Prims.unit) : Prims.unit = ()

let y = ()

let x = ()

With this PR:

let f (_: Prims.unit) : Prims.unit = ()

let x = ()

let y = ()

[maximebuyse]

If several hax_lib::fstar::after are attached to the same item, the order in which they are added to the F* is reversed compared to the previous behaviour. Libcrux relies on this order, so I changed in the libcrux source, let's see if this fixes CI: https://github.com/cryspen/libcrux/actions/runs/12910250039/job/35999838533

Example:

#[hax_lib::fstar::after("let x = ()")]
#[hax_lib::fstar::after("let y = ()")]
fn f() {}

Open this code snippet in the playground

The generated F* without this PR is:

let f (_: Prims.unit) : Prims.unit = ()

let y = ()

let x = ()

With this PR:

let f (_: Prims.unit) : Prims.unit = ()

let x = ()

let y = ()

I made sure that before statements also come in the right order. Libcrux job: https://github.com/cryspen/libcrux/actions/runs/12911235259/job/36003170898

[maximebuyse]

@karthikbhargavan @W95Psp I think we are in a state where we can merge! With the changes in cryspen/libcrux#759 (swapping some fstar::before/after), lax-checking works for libcrux. I also tested on sandwich. Note that we will have to force the merge because of the changes needed in libcrux.

[W95Psp]

LGTM, just a few nits