Xavier Denis

> My log above gives the commit of Creusot. Is it enough for the bug report ? That's perfect > If arbitrary expressions should be supported, then I expect that...

I think the problem here is actually the `if let`, which isn't handled in pearlite

This can be worked around by systematically running `cargo clean`. Perhaps a detail which is relevant is that this crashes on the *build.rs* file, which is annoying that its even...

I think realistically Creusot needs to at least heuristically add `inline_trivial` to certain definitions. Perhaps there's a more systematic approach we can take as well. I believe we have a...

> Probably the most principled way to fix this would be to encode invariants in a way which is much closer to Why3's type invariants. This would require eliminating clones...

The real solution is something we should have done a _long_ time ago. **Ghost could should be Rust code**.

In that world, none of these issues could occur and ghost code would have much clearer and safer semantics. Additional notions of specifications-in-your-code could be added separately from _ghost code_

> Well but then how do you call that? I don't know > Won't you have the same soundness problems? Maybe, but we can worry about that when we can...

> Or do you mean limiting ghost functions to only all rust expressions inside them? This would involve not allowing equality, quantifiers, and potentially the "logical reborrow/unnesting" (https://github.com/xldenis/creusot/pull/606) as I'm...

Hmm interesting question naively I would say *no* otherwise it greatly limits what you can do and breaks non-interference, but not consuming also seems precarious in it's own ways. What...