Add utility function to deal with mutual dependency across different modules

[W95Psp]

(this issue was extracted from https://github.com/hacspec/hax/issues/203#issuecomment-1637539912)

Rust modules are really about namespacing. Rust allows items to be mutually recursive across modules.

This is rarely allowed in other statically typed languages, and even less in proof assistants. Thus, we need a strategy for removing such recursive bundles that span across multiple modules.

Example

Situation A

mod a {
    pub fn f (x: u8) -> u8 {
        if x < 0 { x } else { super::b::f(x - 1) }
    }
}
mod b {
    pub fn f (x: u8) -> u8 {
        if x < 0 { x } else { super::a::f(x - 1) }
    }
}

In this case, we should probably transform to:

mod bundle_a_b {
    pub fn a_f (x: u8) -> u8 {
        if x < 0 { x } else { b_f(x - 1) }
    }
    pub fn b_f (x: u8) -> u8 {
        if x < 0 { x } else { a_f(x - 1) }
    }
}
mod a { pub fn f (x: u8) -> u8 { super::bundle_a_b::a_f(x) } }
mod b { pub fn f (x: u8) -> u8 { super::bundle_a_b::b_f(x) } }

Situation B

We can also write something like:

fn f() {}
mod b {
    use super::*;
    pub fn g() {super::f ()}
}
fn h() { b::g() }

Here we have:

• a dependency from b to a (a::b::g uses a::f);
• a dependency from a to b (f::h uses a::b::g)

In this case, we can either:

• make a bundle for f, g and h just like above;
• make a bundle only for f and g and use that in the rest of the top-level module.

Solution

We want our module-level dependency graph to be a tree. For this, we should identify every group of items that span across multiple modules and isolate them in newly named modules.

This is partially implemented by engine/lib/dependencies.ml, but we need to revisit it and test it heavily. This issue is blocking for extracting Core to anything (F*/Coq/whatever) useful.

[W95Psp]

I added some features to F* that make this much much easier, see https://github.com/FStarLang/FStar/pull/3369

[franziskuskiefer]

@W95Psp please look at this to see what it takes to get this fixed.

[maximebuyse]

I tried the current implementation. Here is a list of what doesn't work:

Situation A

The bundle is created but both functions are named f in it. And they are both declared as let rec. For the second one it should be and.

Situation B

There is no bundle.

[W95Psp]

Yes, the solutions I describe above were not easy to implement when items could not be renamed, that's why it's not used yet. With https://github.com/FStarLang/FStar/pull/3369, we can now introduce a new items in the AST of hax that says "use item module::X and expose it here named Y". I think the bundle code that exists already is more or less capable of doing what we want, but needs to be adapted.

@maximebuyse do you want to chat about it?