feat(rengine, lean): add rejection phase that ensures an expression is in the Lean do-notation DSL

[W95Psp]

Context

The Lean backend produces code that targets Lean's do-notation, providing handy ways to chain monadic let-bindings. This notation actually defines a small internal DSL with do-expressions, do-statements and normal lean-expressions (as a fallback). This PR adds a (rust-engine) phase that rejects interleavings of expressions and statements that are outside this DSL. Eventually, it should be removed in favor of a phase that automatically hoist out let-bindings and control flow operators, in order to always stay inside the DSL (see #1741).

This PR also updates some error messages.

Examples

The following is rejected:

let x = 1 + (if true { 0 } else { 1 });

error: [HAX0008] Explicit rejection by a phase in the Hax engine:
This interleaving of expression and statements does not fit in Lean's do-notation DSL.
You may try hoisting out let-bindings and control-flow.
See issue https://github.com/cryspen/hax/issues/1741

Note: the error was labeled with context `Engine phase (RejectNotDoLeanDSLVisitor)`.

  --> lean-tests/src/ite.rs:11:17
   |
11 |     let x = 1 + (if true { 0 } else { 1 });
   |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^
   |

Other cases can be found in tests/lean-tests/src/reject_do_dsl.rs

[maximebuyse]

I added some comments but this looks good!