[Lean] : support mutually recursion (between items, between modules, inside traits/impl)

[clementblaudeau]

Currently, the Lean backend assumes that the order on the items is compatible with the dependencies, both at top-level and within traits/impls. Therefore, it will produce invalid code when faced with mutual recursion.

Examples

Mutual recursion between items

fn f1(x:u32) -> u32 {
    if x < 10 {
        1
    } else {
        f2(x)
    }        
}

fn f2(x:u32) -> u32 {
    f1(x - 1)
}

Open this code snippet in the playground

Mutual recursion in traits/impls

trait T {
    fn f1(_: u32) -> u32;
    fn f2(_: u32) -> u32;
}

impl T for u32 {
    fn f1(x:u32) -> u32 {
        if x < 10 {
            Self::f2(x)
        } else {
            1
        }        
    }

    fn f2(x:u32) -> u32 {
        Self::f1(x - 1)
    }
}

Open this code snippet in the playground

Context

Rust allows mutual recursion between items, within traits/impls and between modules. By contrast, Lean only allows hierarchical dependencies, expect when using the explicit mutual keyword. To treat this properly, Hax needs three mechanisms :

1. handling of module-level dependencies by interleaving items from different modules. While the flexible namespace of Lean makes it easy, it raises some issues if we want to split the output in several files (file boundaries would not be based on modules).
2. handling of item-level mutual recursion by wrapping them in mutual blocks
3. handling of trait/impl internal dependencies by hoisting out as items.

(See https://github.com/cryspen/hax-evit/issues/24 - duplicate private fork issue)

Workarounds

• for true mutual-recursion : no fix in the rust code, manual edit of the Lean file to add the relevant mutual keywords
• for module-level dependencies : hoist out the functions in a separate module
• for trait/impls internal dependencies : hoist out the functions to the top-level