Do not use the `Result` type for functions which syntactically never fail

[sonmarcho]

Do not use the `Result` type for functions which syntactically never fail

[sonmarcho]

@zhassan-aws you might be interested in this

[sonmarcho]

@msprotz @R1kM I'm interested in your feedback.

[msprotz]

I will read in more detail later but for now my feedback is that this needs to remain a modular, type-based analysis, so an attribute on the function seems like a nice way for the user to indicate that a more direct translation is in order, and will allow generating correct code from the caller's perspective without having to inspect the body of the callee.

For traits, this might require an attribute on the trait definition itself.

Thoughts?

[sonmarcho]

Using attributes to indicate the effect is indeed a general, modular way of directing the translation.
And I agree with the idea of annotating trait definitions, or rather trait methods.

For now I'm really hesitating between triggering the simplification with attributes only, or giving the possibility (for instance with a CLI option) of always simplifying when possible.

[zhassan-aws]

triggering the simplification with attributes only

One difficulty here would be for functions in external dependencies, which would not be possible/easy to annotate.

[msprotz]

What happens if the simplification criterion gets improved and starts detecting more functions? Would this break proofs that depended on the previous behavior?

[R1kM]

I like the idea of using attributes, as this also paves the way towards more expressive "effects".
Regarding your idea of simplifying through micro-passes in the pure model, wouldn't you need a whole-program analysis to do this? In this case, considering for now the single-crate case, could a first part of the analysis be performed during the SymbolicToPure translation (i.e., annotating functions with the can/cannot_fail attribute), to later be simplified in a modular fashion?

[sonmarcho]

triggering the simplification with attributes only

One difficulty here would be for functions in external dependencies, which would not be possible/easy to annotate.

Yes, that's an issue. But I was thinking that we could provide a file which describes the effects of the external dependencies, a bit like what we're doing today (though the behavior is hardcoded in ExtractBuiltin.ml at this point).

[sonmarcho]

I like the idea of using attributes, as this also paves the way towards more expressive "effects". Regarding your idea of simplifying through micro-passes in the pure model, wouldn't you need a whole-program analysis to do this? In this case, considering for now the single-crate case, could a first part of the analysis be performed during the SymbolicToPure translation (i.e., annotating functions with the can/cannot_fail attribute), to later be simplified in a modular fashion?

This is likely what would happen if we're using attributes.
But I'd rather not do too many analyses in SymbolicToPure because this file became a lot more complex than what I had expected, and is not really modular. There are actually severao simplifications which happen there that I would like to move to the micro-passes for this reason.

[sonmarcho]

What happens if the simplification criterion gets improved and starts detecting more functions? Would this break proofs that depended on the previous behavior?

Yes, it will likely break proofs. But how badly would it break the proofs, I'm not sure. On the other hand, if we (allow the user to) control the simplification with attributes, I think it's ok.