Cyclic dependency introduced by bundling with let open

[maximebuyse]

pub mod a {
    #[derive(Debug)]
    pub struct S {}
    pub struct Sa(super::b::Sb);
    impl std::fmt::Debug for Sa {
        fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
            write!(f, "{:?}", self.0)
        }
    }

}

pub mod b {
    pub struct Sb(super::a::S);
    impl std::fmt::Debug for Sb {
        fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
            write!(f, "{:?}", self.0)
        }
    }
}

Open this code snippet in the playground

In the situation above, the recursive bundle contains a let open for one of the original modules creating a cycle.

[W95Psp]

Can this be related to #1068?

[maximebuyse]

Can this be related to #1068?

I need to investigate more. This one is about impl_expr, I think it is more a problem of not renaming things. The other one is about actually moving definitions to the bundle so I think it is a bit different.

[maximebuyse]

I found a way to minimize even more:

pub mod a {
    #[derive(Debug)]
    pub struct S {}
   fn f(_x:super::b::Sb) {}

}

pub mod b {
    pub struct Sb(super::a::S);
    impl std::fmt::Debug for Sb {
        fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
            write!(f, "{:?}", self.0)
        }
    }
}

Open this code snippet in the playground

The problem seems to come from the impl_expr for the derive(Debug) for S

[maximebuyse]

So the problem is that we filter out automatically generated items in import_thir, including derived trait impls. Some impl_expr still refer to them but as they don't exist in the engine we don't move them to the bundle, so we don't rename the references to them, thus creating a fake implicit dependency.

[maximebuyse]

After discussing this, we should:

• Change the filtering to replace the method implementations by panics
• Not filter all generated code. We can add some filters (we should at least filter serde::{Serialize, Deserialize}). Eventually these filters should be configurable with the cli (with a good default value).

[maximebuyse]

Related issue: #108

[maximebuyse]

I am testing my implementation of this. One problem in the case of Debug is that Debug and Formatter both belong to core::fmt and have a method fmt which means we get #61. We could rename the method in one of them and also do the same renaming when we translate an implementation. But this is a bit of a hack...

[maximebuyse]

I am testing my implementation of this. One problem in the case of Debug is that Debug and Formatter both belong to core::fmt and have a method fmt which means we get #61. We could rename the method in one of them and also do the same renaming when we translate an implementation. But this is a bit of a hack...

Apart from that the current implementation works but with the false precondition for panic it will not be usable for proofs. We can try to find an alternative using vals (but it might depend if we want to extract interfaces only, or implementation too.

For some traits like Clone we have a custom definition without pre/post conditions which makes the generated code for impls incompatible with the trait definition. We could filter out impls of Clone but that would leave the potential problem of creating cyclic dependencies with impl_expr.

[maximebuyse]

I am testing my implementation of this. One problem in the case of Debug is that Debug and Formatter both belong to core::fmt and have a method fmt which means we get #61. We could rename the method in one of them and also do the same renaming when we translate an implementation. But this is a bit of a hack...

Apart from that the current implementation works but with the false precondition for panic it will not be usable for proofs. We can try to find an alternative using vals (but it might depend if we want to extract interfaces only, or implementation too.

For some traits like Clone we have a custom definition without pre/post conditions which makes the generated code for impls incompatible with the trait definition. We could filter out impls of Clone but that would leave the potential problem of creating cyclic dependencies with impl_expr.

After discussing this, the solution we should implement is: allow impls (and functions) to be opaque. Add the opaque flag to generated impls. This way we will extract them to let impl: ... = admit()

[maximebuyse]

The best solution to solve this right now is to filter out things only with late_skip instead of dropping them in import_thir. We might need to kill the methods body in import_thir to avoid problems, like derived (or at least a list of unsupported traits).

It would also help to rename everything that is directly under the namespace of bundled modules.