[F* lib] Tls codec panic freedom

[maximebuyse]

F* core lib changes necessary for panic freedom of TLS codec:

• Some additions, and corrections (like the error type of integer TryInto instances which can be Infallible or TryFromIntError depending on the integer types.
• Corrections for while loops and invariants
• F* backend change: distribute type coertions inside each component of a tuple instead of having a coertion on the tuple type (helps F* type checking)

[clementblaudeau]

Looks good. Two points might need to be documented :

1. Why do you need to replace some res by true ==> res ?
2. Why inverting condition and invariant in functionalize_loops ? It might affect other backends

[clementblaudeau]

What's the motivation here ?

[maximebuyse]

Sometimes there are computations in the loop condition that can be proven panic free only using the invariant, this means in our encoding the invariant should come first so that it can be assumed to hold inside the condition.

[clementblaudeau]

Understood. This will probably require some updates in the Lean Lib though (the Fold functions). Ping me if you want me to do it.

[maximebuyse]

This is only for while loops, the lean backend produces Rust_primitives.Hax.while_loop, but I don't find the definition in the Lean lib. Is it because it is just not defined?

[maximebuyse]

Looks good. Two points might need to be documented :

1. Why do you need to replace some `res` by `true ==> res` ?

2. Why inverting condition and invariant in `functionalize_loops` ? It might affect other backends

Thanks for the review. I answered in threads. I will probably remove the commented code, there are also some more things I want to add to this PR.